Ver el código de «Rel 10 (sol)»

<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>