Mjoseh: Página creada con « chapter ‹ R10: Razonamiento sobre programas en Isabelle/HOL › theory R10_sol imports Main begin text ‹ -------------------------------…»

2020-05-05T06:46:33Z

Página creada con «<source lang = "isabelle"> chapter ‹ R10: Razonamiento sobre programas en Isabelle/HOL › theory R10_sol imports Main begin text ‹ -------------------------------…»

Página nueva

<source lang = "isabelle">
chapter ‹ R10: Razonamiento sobre programas en Isabelle/HOL ›

theory R10_sol
imports Main
begin

text ‹ ---------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
(*) automática
(*) detallada (bien declarativa o aplicativa)
------------------------------------------------------------------ ›

text ‹---------------------------------------------------------------
Ejercicio 1.1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------›

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"

value "sumaImpares 5" ― ‹= 25›

text ‹---------------------------------------------------------------
Ejercicio 1.2. Demostrar que
sumaImpares n = n*n
-------------------------------------------------------------------›

― ‹Demostración automática:›
lemma "sumaImpares n = n*n"
by (induct n) simp_all

― ‹Demostración estructurada:›
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0 * 0" by simp
next
fix n
assume HI: "sumaImpares n = n * n"
have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" by simp
also have "... = n*n + (2*n+1)" using HI by simp
also have "... = Suc n * Suc n" by simp
finally show "sumaImpares (Suc n) = Suc n * Suc n" by simp
qed

― ‹Demostración detallada declarativa:›
lemma "sumaImpares n = n*n"
proof (induct n)
have "sumaImpares 0 = 0"
by (simp only: sumaImpares.simps(1))
also have "... = 0*0"
by (simp only: mult_0)
finally show "sumaImpares 0 = 0*0"
by this
next
fix n
assume HI: "sumaImpares n = n*n"
have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"
by (simp only: sumaImpares.simps(2))
also have "... = n*n+(2*n+1)"
by (simp only: HI)
also have "... = n*(n+1)+1*(n+1)"
by (simp only: add_mult_distrib2)
also have "... = (n+1)*(n+1)"
by (simp only: add_mult_distrib)
also have "... = (Suc n)*(Suc n)"
by (simp only: Suc_eq_plus1)
finally show "sumaImpares (Suc n) = (Suc n)*(Suc n)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma sumaImpares_d:
"sumaImpares n = n*n"
apply (induct n)
apply (simp only: sumaImpares.simps(1))
apply (simp only: sumaImpares.simps(2))
apply (simp only:mult_Suc_right)
apply (simp only:mult_Suc)
done

text ‹ ---------------------------------------------------------------
Ejercicio 2.1. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ ›

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 2"
| "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)"

value "sumaPotenciasDeDosMasUno 3" ― ‹= 16›

text ‹ ---------------------------------------------------------------
Ejercicio 2.2. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- ›

― ‹Demostración automática:›
lemma
"sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) simp_all

― ‹Demostración estructurada:›
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) =
sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp
also have "... = 2^(n+1) + 2^(n+1)" using HI by simp
also have "... = 2 ^ (Suc n + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
have "sumaPotenciasDeDosMasUno 0 = 2"
by (simp only: sumaPotenciasDeDosMasUno.simps(1))
also have "... = 2^1"
by (simp only: monoid_mult_class.power_one_right)
also have "... = 2^(0+1)"
by (simp only: add_0)
finally show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)"
by this
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) =
sumaPotenciasDeDosMasUno n + 2^(n+1)"
by (simp only: sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2^(n+1)+2^(n+1)"
by (simp only: HI)
also have "... = 2^(n+1)*2"
by (simp only: mult_2_right)
also have "... = 2^(Suc(n+1))"
by (simp only: power_Suc2)
also have "... = 2^((Suc n)+1)"
by (simp only: Suc_eq_plus1)
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^((Suc n)+1)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma sumaPotenciasDeDosMasUno_d:
"sumaPotenciasDeDosMasUno n = 2^(n+1)"
apply (induct n)
apply (simp only: sumaPotenciasDeDosMasUno.simps(1))
apply (simp only:plus_nat.add_0)
apply (simp only: power_one_right)
apply (simp only: sumaPotenciasDeDosMasUno.simps(2))
apply (simp only:Suc_eq_plus1 )
apply (simp only: power_add)
apply (simp only: power_one_right)
done

text ‹ ---------------------------------------------------------------
Ejercicio 3. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ ›

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []"
| "copia (Suc n) x = x # copia n x"

value "copia 3 x" ― ‹= [x,x,x]›

text ‹ ---------------------------------------------------------------
Ejercicio 4. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- ›

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

value "todos (λx. x>(1::nat)) [2,6,4]" ― ‹= True›
value "todos (λx. x>(2::nat)) [2,6,4]" ― ‹= False›

text ‹ ---------------------------------------------------------------
Ejercicio 5. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- ›

― ‹Demostración automática:›
lemma "todos (λy. y=x) (copia n x)"
by (induct n) simp_all

―‹Demostración estructurada:›
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)"
by simp
next
fix n
assume "todos (λy. y = x) (copia n x)"
then show "todos (λy. y = x) (copia (Suc n) x)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
have "todos (λy. y=x) []"
by (simp only: todos.simps(1))
then show "todos (λy. y=x) (copia 0 x)"
by (simp only: copia.simps(1))
next
fix n
assume HI: "todos (λy. y = x) (copia n x)"
then have "todos (λy. y = x) (x # copia n x)"
by (simp only: todos.simps(2))
then show "todos (λy. y = x) (copia (Suc n) x)"
by (simp only: copia.simps(2))
qed

― ‹Demostración detallada aplicativa:›
lemma todos_copia_d:
"todos (λy. y=x) (copia n x)"
apply (induct n)
apply (simp only: copia.simps(1))
apply (simp only:todos.simps(1))
apply (simp only: copia.simps(2))
apply (simp only:todos.simps(2))
done

text ‹ ---------------------------------------------------------------
Ejercicio 6.1. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ ›

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]"
| "amplia (x#xs) y = x # amplia xs y"

value "amplia [d,a] t" ― ‹= [d,a,t]›

text ‹ ---------------------------------------------------------------
Ejercicio 6.2, Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- ›

― ‹Demostración automática:›
lemma "amplia xs y = xs @ [y]"
by (induct xs) simp_all

― ‹Demostración estructurada:›
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x # xs) y = x # amplia xs y" by simp
also have "... = x # (xs @ [y])" using HI by simp
also have "... = (x # xs) @ [y]" by simp
finally show "amplia (x # xs) y = (x # xs) @ [y]" by simp
qed

― ‹Demostración detallada declarativa:›
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
have "amplia [] y = [y]"
by (simp only: amplia.simps(1))
also have "... = [] @ [y]"
by (simp only: append_Nil)
finally show "amplia [] y = [] @ [y]"
by this
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x#xs) y = x # amplia xs y"
by (simp only: amplia.simps(2))
also have "... = x # (xs @ [y])"
by (simp only: HI)
also have "... = (x # xs) @ [y]"
by (simp only: append_Cons)
finally show "amplia (x#xs) y = (x # xs) @ [y]"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma amplia_append_d: "amplia xs y = xs @ [y]"
apply (induct xs)
apply (simp only: amplia.simps(1))
apply (simp only: append.simps(1))
apply (simp only: amplia.simps(2))
apply (simp only: append.simps(2))
done

text ‹
---------------------------------------------------------------------
Ejercicio 7. Definir la función
algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (algunos p xs) se verifica si algunos elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
algunos (λx. 1<length x) [[2,1,4],[3]]
¬algunos (λx. 1<length x) [[],[3]]"

Nota: La función algunos es equivalente a la predefinida list_ex.
---------------------------------------------------------------------
›

fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
| "algunos p (x#xs) = ((p x) ∨ (algunos p xs))"

text ‹
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
›
― ‹Demostración automática:›
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

― ‹Demostración estructurada:›
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])"
by simp
next
fix a xs
assume "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
then show "todos (λx. P x ∧ Q x) (a#xs) = (todos P (a#xs) ∧ todos Q (a#xs))"
by auto
qed

― ‹Demostración detallada declarativa:›
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
have "todos (λx. P x ∧ Q x) [] = True"
by (simp only: todos.simps(1))
also have "... = (True ∧ True)"
by (simp only: conj_absorb)
also have "... = (todos P [] ∧ todos Q [])"
by (simp only: todos.simps(1))
finally show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])"
by this
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) = ((λx. P x ∧ Q x) x ∧ todos (λx. P x ∧ Q x) xs)"
by (simp only: todos.simps(2))
also have "... = ((λx. P x ∧ Q x) x ∧ (todos P xs ∧ todos Q xs))"
by (simp only: HI)
also have "... = (P x ∧ Q x ∧ todos P xs ∧ todos Q xs)"
by (simp only: conj_assoc)
also have "... = (P x ∧ todos P xs ∧ Q x ∧ todos Q xs)"
by (simp only: conj_left_commute)
also have "... = ((P x ∧ todos P xs) ∧ Q x ∧ todos Q xs)"
by (simp only: conj_assoc)
also have "... = (todos P (x#xs) ∧ Q x ∧ todos Q xs)"
by (simp only: todos.simps(2))
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))"
by (simp only: todos.simps(2))
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma todos_conj_a:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
apply (induct xs)
apply (simp only: todos.simps(1))
apply (simp only: conj_absorb)
apply (simp only: todos.simps(2))
apply (simp only: conj_assoc)
apply (simp only: conj_left_commute)
done

text ‹
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar
todos P (xs @ ys) = (todos P xs ∧ todos P ys)
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
by (induct xs) simp_all

― ‹Demostración estructurada:›
lemma todos_append_e:
"todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
proof (induct xs)
show "todos P ([] @ ys) = (todos P [] ∧ todos P ys)"
by simp
next
fix a xs
assume "todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
then show "todos P ((a#xs) @ ys) = (todos P (a#xs) ∧ todos P ys)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma todos_append_d:
"todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
proof (induct xs)
have "todos P ([] @ ys) = todos P ys"
by (simp only: append.simps(1))
also have "... = (True ∧ todos P ys)"
by (simp only: simp_thms(22))
also have "... = (todos P [] ∧ todos P ys)"
by (simp only: todos.simps(1))
finally show "todos P ([] @ ys) = (todos P [] ∧ todos P ys)"
by this
next
fix a xs
assume HI:"todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
have "todos P ((a#xs) @ ys) = (todos P (a#(xs @ ys)))"
by (simp only: append.simps(2))
also have "... = (P a ∧ todos P (xs @ ys))"
by (simp only: todos.simps(2))
also have "... = (P a ∧ todos P xs ∧ todos P ys)"
by (simp only: HI)
also have "... = ((P a ∧ todos P xs) ∧ todos P ys)"
by (simp only: conj_assoc)
also have "... = (todos P (a#xs) ∧ todos P ys)"
by (simp only: todos.simps(2))
finally show "todos P ((a#xs) @ ys) = (todos P (a#xs) ∧ todos P ys)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma todos_append_a: "todos P (xs @ ys) = (todos P xs ∧ todos P ys)"
apply (induct xs)
apply (simp only: append.simps(1))
apply (simp only: todos.simps(1))
apply (simp only: simp_thms(22))
apply (simp only: append.simps(2))
apply (simp only: todos.simps(2))
apply (simp only: conj_assoc)
done

text ‹
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append_d)

― ‹Demostración estructurada:›
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []"
by simp
next
fix a xs
assume "todos P (rev xs) = todos P xs"
then show "todos P (rev (a#xs)) = todos P (a#xs)"
by (auto simp add: todos_append_d)
qed

― ‹Demostración detallada declarativa:›
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []"
by (simp only: rev.simps(1))
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P (rev xs@[x])"
by (simp only: rev.simps(2))
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp only: todos_append_d)
also have "... = (todos P xs ∧ todos P [x])"
by (simp only: HI)
also have "... = (todos P [x] ∧ todos P xs)"
by (simp only: conj_commute)
also have "... = (todos P ([x]@xs))"
by (simp only: todos_append_d)
also have "... = (todos P (x#xs))"
by (simp only: append.simps)
finally show "todos P (rev (x#xs)) = todos P (x#xs)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma todos_rev_d: "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (simp only: rev.simps(1))
apply (simp only: rev.simps(2))
apply (simp only: todos_append_d)
apply (simp only: todos.simps(2))
apply (simp only: todos.simps(1))
apply (simp only: simp_thms(21))
apply (simp only: conj_commute)
done

text ‹
---------------------------------------------------------------------
Ejercicio 11. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
›

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text ‹

Quickcheck found a counterexample:
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
Evaluated terms:
algunos (λx. P x ∧ Q x) xs = False
algunos P xs ∧ algunos Q xs = True
›

text ‹
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) simp_all

― ‹Demostración estructurada:›
lemma "algunos P (map f xs) = algunos (P ∘ f) xs"
proof (induct xs)
show "algunos P (map f []) = algunos (P ∘ f) []"
by simp
next
fix a xs
assume "algunos P (map f xs) = algunos (P ∘ f) xs"
then show "algunos P (map f (a#xs)) = algunos (P ∘ f) (a#xs)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
have "algunos P (map f []) = algunos P []"
by (simp only: list.map(1))
also have "... = algunos (P o f) []"
by (simp only: algunos.simps(1))
finally show "algunos P (map f []) = algunos (P o f) []"
by this
next
fix x xs
assume HI: "algunos P (map f xs) = algunos (P o f) xs"
have "algunos P (map f (x#xs)) = algunos P ((f x) # (map f xs))"
by (simp only: list.map(2))
also have "... = (P (f x) ∨ algunos P (map f xs))"
by (simp only: algunos.simps(2))
also have "... = (P (f x) ∨ algunos (P o f) xs)"
by (simp only: HI)
also have "... = ((P o f) x ∨ algunos (P o f) xs)"
by (simp only: o_apply)
also have "... = algunos (P o f) (x#xs)"
by (simp only: algunos.simps(2))
finally show "algunos P (map f (x#xs)) = algunos (P o f) (x#xs)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma algunos_map_e: "algunos P (map f xs) = algunos (P o f) xs"
apply (induct xs)
apply (simp only: list.map(1))
apply (simp only: algunos.simps(1))
apply (simp only: list.map(2))
apply (simp only: algunos.simps(2))
apply (rule iffI)
apply (erule disjE)
apply (rule disjI1)
apply (simp only: o_apply)
apply (rule disjI2, assumption)
apply (erule disjE)
apply (rule disjI1)
apply (simp only: o_apply)
apply (rule disjI2, assumption)
done

text ‹
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) simp_all

― ‹Demostración estructurada:›
lemma algunos_append_e:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)"
by simp
next
fix a xs
assume "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
then show "algunos P ((a#xs) @ ys) = (algunos P (a#xs) ∨ algunos P ys)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma algunos_append_d:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
have "algunos P ([] @ ys) = (algunos P ys)"
by (simp only: append_Nil)
also have "... = (False ∨ algunos P ys)"
by (simp only: simp_thms(32))
also have "... = (algunos P [] ∨ algunos P ys)"
by (simp only: algunos.simps(1))
finally show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)"
by this
next
fix x xs
assume HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((x#xs) @ ys) = algunos P (x#(xs @ ys))"
by (simp only: append_Cons)
also have "... = (P x ∨ algunos P (xs @ ys))"
by (simp only: algunos.simps(2))
also have "... = (P x ∨ algunos P xs ∨ algunos P ys)"
by (simp only: HI)
also have "... = ((P x ∨ algunos P xs) ∨ algunos P ys)"
by (simp only: disj_assoc)
also have "... = (algunos P (x#xs) ∨ algunos P ys)"
by (simp only: algunos.simps(2))
finally show "algunos P ((x#xs) @ ys) =
(algunos P (x#xs) ∨ algunos P ys)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma algunos_append_a:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
apply (induct xs)
apply (simp only: algunos.simps(1))
apply (simp only: append.simps(1))
apply (simp only: simp_thms(32))
apply (simp only: append_Cons)
apply (simp only: algunos.simps(2))
apply (simp only: disj_assoc)
done

text ‹
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append_d)

― ‹Demostración estructurada:›
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []"
by simp
next
fix a xs
assume "algunos P (rev xs) = algunos P xs"
then show "algunos P (rev (a#xs)) = algunos P (a#xs)"
by (auto simp add: algunos_append_d)
qed

― ‹Demostración detallada declarativa:›
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []"
by (simp only: rev.simps(1))
next
fix x xs
assume HI: "algunos P (rev xs) = algunos P xs"
have "algunos P (rev (x#xs)) = algunos P (rev xs @ [x])"
by (simp only: rev.simps(2))
also have "... = (algunos P (rev xs) ∨ algunos P [x])"
by (simp only: algunos_append_d)
also have "... = (algunos P xs ∨ algunos P [x])"
by (simp only: HI)
also have "... = (algunos P xs ∨ P x ∨ algunos P [])"
by (simp only: algunos.simps(2))
also have "... = (algunos P xs ∨ P x ∨ False)"
by (simp only: algunos.simps(1))
also have "... = (algunos P xs ∨ P x)"
by (simp only: simp_thms(31))
also have "... = (P x ∨ algunos P xs)"
by (simp only: disj_commute)
also have "... = algunos P (x#xs)"
by (simp only: algunos.simps(2))
finally show "algunos P (rev (x#xs)) = algunos P (x#xs)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma algunos_rev_e:
"algunos P (rev xs) = algunos P xs"
apply (induct xs)
apply (simp only: rev.simps(1))
apply (simp only: rev.simps(2))
apply (simp only: algunos.simps(2))
apply (simp only: algunos_append_d)
apply (simp only: algunos.simps(2))
apply (simp only: algunos.simps(1))
apply (simp only: simp_thms(31))
apply (simp only: disj_commute)
done

text ‹
---------------------------------------------------------------------
Ejercicio 15. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
›

text ‹Solución: La ecuación se verifica eligiendo como Z el término
algunos P xs ∨ algunos Q xs
En efecto,›

― ‹Demostración automatica:›
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto

― ‹Demostración estructurada:›
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])"
by simp
next
fix a xs
assume "algunos (λx. (P x ∨ Q x)) xs = (algunos P xs ∨ algunos Q xs)"
then show "algunos (λx. P x ∨ Q x) (a#xs) =
(algunos P (a#xs) ∨ algunos Q (a#xs))"
by auto
qed

― ‹Demostración detallada declarativa:›
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
have "algunos (λx. P x ∨ Q x) [] = False"
by (simp only: algunos.simps(1))
also have "... = (False ∨ False)"
by (simp only: simp_thms(31))
also have "... = (algunos P [] ∨ False)"
by (simp only: algunos.simps(1))
also have "... = (algunos P [] ∨ algunos Q [])"
by (simp only: algunos.simps(1))
finally show "algunos (λx. P x ∨ Q x) [] =
(algunos P [] ∨ algunos Q [])"
by this
next
fix x xs
assume HI:"algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
have "algunos (λx. P x ∨ Q x) (x#xs) =((P x ∨ Q x) ∨ algunos (λx. P x ∨ Q x) xs)"
by (simp only: algunos.simps(2))
also have "... = ((P x ∨ Q x) ∨ algunos P xs ∨ algunos Q xs)"
by (simp only: HI)
also have "... = (P x ∨ Q x ∨ algunos P xs ∨ algunos Q xs)"
by (simp only: disj_assoc)
also have "... = (P x ∨ algunos P xs ∨ Q x ∨ algunos Q xs)"
by (simp only: disj_left_commute)
also have "... = ((P x ∨ algunos P xs) ∨ (Q x ∨ algunos Q xs))"
by (simp only: disj_assoc)
also have "... = (algunos P (x#xs) ∨ algunos Q (x#xs))"
by (simp only: algunos.simps(2))
finally show "algunos (λx. P x ∨ Q x) (x#xs) =
(algunos P (x#xs) ∨ algunos Q (x#xs))"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
apply (induct xs)
apply (simp only: algunos.simps(1))
apply (simp only: simp_thms(31))
apply (simp only: algunos.simps(2))
apply (simp only: disj_assoc)
apply (simp only: disj_comms)
done

text ‹
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma algunos_no_todos_d:
"algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) simp_all

― ‹Demostración estructurada:›
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show "algunos P [] = (¬ todos (λx. (¬ P x)) [])"
by simp
next
fix a xs
assume "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
then show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show "algunos P [] = (¬ todos (λx. (¬ P x)) [])"
by (simp only: algunos.simps(1)
todos.simps(1)
not_True_eq_False)
next
fix a xs
assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))"
proof -
have "algunos P (a#xs) = ((P a) ∨ algunos P xs)"
by (simp only: algunos.simps(2))
also have "… = ((P a) ∨ ¬ todos (λx. (¬ P x)) xs)" using HI
by (simp only: todos.simps(2))
also have "… = (¬ (¬ (P a) ∧ todos (λx. (¬ P x)) xs))"
by (simp only: de_Morgan_conj not_not)
also have "… = (¬ todos (λx. (¬ P x)) (a#xs))"
by (simp only: de_Morgan_conj todos.simps(2))
finally show ?thesis by this
qed
qed

― ‹Demostración detallada aplicativa:›
lemma algunos_no_todos_e:
"algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
apply (induct xs)
apply (simp only: algunos.simps(1))
apply (simp only: todos.simps(1))
apply (simp only:not_True_eq_False)
apply (simp only: algunos.simps(2))
apply (simp only: todos.simps(2))
apply (simp only: de_Morgan_conj)
apply (simp only: not_not)
done

text ‹
---------------------------------------------------------------------
Ejercicio 17.1. Definir la función
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

text ‹
---------------------------------------------------------------------
Ejercicio 17.2. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
›

text ‹Solución: La relación es
estaEn y xs = algunos (λx. x=y) xs
En efecto,›

― ‹Demostración automática:›
lemma "estaEn x xs = algunos (λy. y=x) xs"
by (induct xs) auto

― ‹Demostración estructurada:›
lemma "estaEn x xs = algunos (λy. y=x) xs"
proof (induct xs)
show "estaEn x [] = algunos (λy. y=x) []"
by simp
next
fix a xs
assume HI: "estaEn x xs = algunos (λy. y=x) xs"
have "estaEn x (a#xs) = algunos (λy. y=x) (a#xs)"
using HI by simp
then show "estaEn x (a#xs) = algunos (λy. y=x) (a#xs)"
by simp
qed

― ‹Demostración detallada declarativa:›
lemma "estaEn x xs = algunos (λy. y=x) xs"
proof (induct xs)
have "estaEn x [] = False"
by (simp only: estaEn.simps(1))
also have "... = algunos (λy. y=x) []"
by (simp only: algunos.simps(1))
finally show "estaEn x [] = algunos (λy. y=x) []"
by this
next
fix a xs
assume HI: "estaEn x xs = algunos (λy. y=x) xs"
have "estaEn x (a#xs) = ((a=x) ∨ estaEn x xs)"
by (simp only: estaEn.simps(2))
also have "... = ((a=x) ∨ algunos (λy. y=x) xs) "
using HI by (simp only :)
also have "... = algunos (λy. y=x) (a#xs)"
by (simp only: algunos.simps(2))
finally show "estaEn x (a#xs) = algunos (λy. y=x) (a#xs)"
by this
qed

― ‹Demostración detallada aplicativa:›
lemma "estaEn x xs = algunos (λy. y=x) xs"
apply (induct xs)
apply (simp only:estaEn.simps(1))
apply (simp only:algunos.simps(1))
apply (simp only:estaEn.simps(2))
apply (simp only:algunos.simps(2))
done

end

</source>

Rel 10 (sol) - Historial de revisiones

Mjoseh: Protegió «Rel 10 (sol)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R10: Razonamiento sobre programas en Isabelle/HOL › theory R10_sol imports Main begin text ‹ -------------------------------…»

← Revisión anterior	Revisión del 06:46 5 may 2020
(Sin diferencias)