Relación 4

chapter {* R4: Cuantificadores sobre listas *}

theory R4_Cuantificadores_sobre_listas
imports Main 
begin

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

  Nota: La función todos es equivalente a la predefinida list_all. 
  --------------------------------------------------------------------- 
*}

(* danrodcha ivamenjim migtermor dancorgar wilmorort marpoldia1
   ferrenseg paupeddeg pablucoto crigomgom anaprarod serrodcal juacabsou
   rubgonmar josgarsan fraortmoy lucnovdos pabrodmac fracorjim1
   marcarmor13 jeamacpov antsancab1 *)   
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p []     = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. 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. 
  --------------------------------------------------------------------- 
*}

(* danrodcha ivamenjim migtermor dancorgar marpoldia1 ferrenseg
   wilmorort paupeddeg pablucoto crigomgom anaprarod serrodcal juacabsou
   rubgonmar josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 jeamacpov antsancab1*)  
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p []     = False"
| "algunos p (x#xs) = (p x ∨ algunos p xs)"

(* fracorjim1. En esta versión el procesamiento se detiene al encontrar
   una coincidencia *) 
fun algunos2  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos2 p [] = False"
| "algunos2 p (x#xs) = (if p x then True else algunos2 p xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

(* danrodcha ivamenjim migtermor dancorgar marpoldia1 ferrenseg
   wilmorort paupeddeg pablucoto anaprarod serrodcal juacabsou rubgonmar
   josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 jeamacpov antsancab1 *)  
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

(* fracorjim1 *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
apply (induct xs)
apply auto
done

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.2. Demostrar o refutar detalladamente
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

(* danrodcha fracorjim1 *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?R xs")
proof (induct xs)
  show "?R []" by simp
next
  fix a xs 
  assume HI: "?R xs"
  have "todos (λx. P x ∧ Q x) (a#xs) = 
        (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "… = (P a ∧ Q a ∧ (todos P xs ∧ todos Q xs))" 
    using HI by simp
  also have "… = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" by blast
  also have "… = (todos P (a#xs) ∧ todos Q (a#xs))" by simp
  finally show "?R (a#xs)" by simp
qed

(* Comentario: Uso de blast. *)

(* ivamenjim wilmorort serrodcal josgarsan*)
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 HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λx. P x ∧ Q x) (a # xs) = 
        (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" 
    using HI by simp
  finally show "todos (λx. P x ∧ Q x) (a # xs) = 
                (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

(* Comentario: Uso de auto. *)

(* dancorgar paupeddeg *)
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 y xs
  assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λx. P x ∧ Q x) (y#xs) = 
        ((P y ∧ Q y) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
  also have "… = ((P y ∧ Q y) ∧ (todos P xs ∧ todos Q xs))" 
    using HI by simp
  also have "… = ((P y ∧ todos P xs) ∧ (Q y ∧ todos Q xs))" by blast
  also have "… = ((todos P (y#xs)) ∧ (todos Q (y#xs)))" by simp
  finally show "todos (λx. P x ∧ Q x) (y#xs) = 
                (todos P (y#xs) ∧ todos Q (y#xs))" by simp
qed

(* migtermor *)
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 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)) = 
       (( P x ∧ Q x) ∧ (todos (λx. P x ∧ Q x) xs))"
   by (simp only: todos.simps(2))
 also have "… = ((P x ∧ Q x) ∧ (todos P xs ∧ todos Q xs))" 
   using HI by simp
 also have "… = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" 
   by arith
 also have "((P x ∧ Q x) ∧ (todos P xs ∧ todos Q xs)) = (((P x)∧(todos P xs)) ∧ ((Q x) ∧ (todos Q xs)))"
   by arith 
   (* Este paso es exactamente el mismo que el anterior, pero sin
      cualquiera de los dos no funciona el "finally show" *) 
 have "… = (((P x)∧(todos P xs))∧((Q x)∧(todos Q xs)))" by simp
 have "… = ((todos P (x#xs))∧(todos Q (x#xs)))" by simp
 finally show "(todos (λx. P x ∧ Q x) (x#xs)) = 
               ((todos P (x#xs)) ∧ (todos Q (x#xs)))" by simp 
qed

(* Comentarios: Ruptura de la cadena de igualdades y uso de arith. *)

(* marpoldia1 *)
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 HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" 
  have "todos (λx. P x ∧ Q x) (a # xs) =  
        ((P a ∧ Q a) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
  also have "... = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" by blast
  also have "... = (todos P (a#xs) ∧ todos Q (a#xs)) " by simp
 finally show "todos (λx. P x ∧ Q x) (a#xs) = 
               (todos P (a#xs) ∧ todos Q (a#xs))" by simp 
qed

(* ferrenseg *)
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 n xs
  assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λx. P x ∧ Q x) (n # xs) = 
        (P n ∧ Q n ∧ todos P xs ∧ todos Q xs)" using HI by simp
  also have "… = P n ∧ Q n ∧ todos P xs ∧ todos Q xs" by blast
  also have "⋯ = todos P (n # xs) ∧ todos Q (n # xs)" by simp 
  finally show "todos (λx. P x ∧ Q x) (n # xs) = todos P (n # xs) ∧ todos Q (n # xs)" by simp
oops

(* Comentario: Demostración incompleta. *)

(* lucnovdos *)
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 n xs
  assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" 
  have "todos (λx. P x ∧ Q x) (n # xs) =  
        ((P n ∧ Q n) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
  also have "... = ((P n ∧ todos P xs) ∧ (Q n ∧ todos Q xs))" by arith
  also have "... = ((todos P(n#xs)) ∧ (todos Q(n#xs)))" by simp
 finally show "todos (λx. P x ∧ Q x) (n#xs) = 
               (todos P (n#xs) ∧ todos Q (n#xs))" by simp 
qed

(* wilmorort pablucoto crigomgom anaprarod juacabsou rubgonmar fraortmoy
   marcarmor13 jeamacpov *)
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 HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λx. P x ∧ Q x) (a # xs) = 
        (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" 
    using HI by simp
  also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)"  by arith
  also have "... = (todos P (a # xs) ∧ todos Q (a # xs))" by simp 
    (* Este paso se puede obviar *)
  finally show "todos (λx. P x ∧ Q x) (a # xs) = 
                (todos P (a # xs) ∧ todos Q (a # xs))" by simp
qed

(* pabrodmac *)
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 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) = 
        (P x ∧ Q x  ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P x ∧ Q x  ∧ (todos P xs ∧ todos Q xs))" 
    using HI by simp
  also have "... = (P x ∧ todos P xs ∧ Q x ∧ todos Q xs)"  by arith
  finally show "todos (λx. P x ∧ Q x) (x#xs) = 
                (todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

(* antsancab1 *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?R xs")
proof (induct xs)
  show "?R []" by simp
next
  fix a xs
  assume HI: "?R xs"
  have "todos (λx. P x ∧ Q x) (a#xs) = (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" using HI by simp
  finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a#xs) ∧ todos Q (a#xs))" by auto
qe

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

(* danrodcha ivamenjim marpoldia1 migtermor ferrenseg wilmorort
   paupeddeg crigomgom anaprarod serrodcal juacabsou rubgonmar pablucoto
   fraortmoy josgarsan lucnovdos pabrodmac marcarmor13 jeamacpov antsancab1 *) 
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

(* anaprarod dancorgar fracorjim1 *)
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
apply (induct x)
apply auto
done

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.2. Demostrar o refutar detalladamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

(* ivamenjim ferrenseg wilmorort dancorgar fraortmoy josgarsan lucnovdos
 rubgonmar *) 
lemma todos_append:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next 
  fix a x
  assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
  have "todos P ((a#x) @ y) = (P a ∧ (todos P (x @ y)))" by simp
  also have "... = (P a ∧ (todos P x ∧ todos P y))" using HI by simp
  finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)" 
    by simp
qed

(* migtermor serrodcal antsancab1 *)
lemma todos_append1:
  "todos P (x @ y) = (todos P x ∧ todos P y)" (is "?P x")
proof (induct x)
  show "?P []" by simp
next 
  fix a x
  assume HI: "?P x"
  have "todos P ((a#x) @ y) = (P a ∧ (todos P (x @ y)))" by simp
  also have "… = (P a ∧ (todos P x ∧ todos P y))" using HI by simp
  finally show "?P (a#x)" by simp
qed  

(* marpoldia1 *)
lemma todos_append2:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
  fix a x
  assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
  have "todos P ((a # x) @ y) = todos P (a#(x@y))" by simp
  also have "... = (P a ∧ todos P (x @ y))" by simp
  also have "... = (P a ∧ (todos P x ∧ todos P y))" using HI by simp
  finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)" 
    by simp
qed

(* paupeddeg *)
lemma todos_append3:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
  fix a x
  assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
  have "todos P ((a # x) @ y) = todos P (a # (x @ y))" by simp
  also have "... = (todos P [a] ∧ todos P (x @ y)) " by simp
  also have "... = (todos P [a] ∧ (todos P x ∧ todos P y))" 
    using HI by simp
  finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)" 
    by simp
qed

(* crigomgom juacabsou anaprarod*)
lemma todos_append4:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
  fix x xs
  assume HI:"todos P (xs @ y) = (todos P xs ∧ todos P y)"
  have "todos P ((x # xs) @ y) = (P x ∧ todos P (xs @ y ))" by simp
  also have "... = (P x ∧ (todos P xs ∧ todos P y)) " using HI by simp
  also have "... = ((P x ∧ todos P xs) ∧ todos P y)" by simp
  finally show "todos P ((x # xs) @ y) = (todos P (x # xs) ∧ todos P y)" 
    by simp
qed

(* pablucoto marcarmor13 jeamacpov *)
lemma todos_append5:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x )
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
  assume HI:"todos P (x @ y) = (todos P x ∧ todos P y) " 
  have "todos P ((a # x) @ y) = ( P a ∧ todos P (x @ y))" by simp
  also have " ... =( P a ∧ (todos P x ∧ todos P y))" using HI by simp
  also have "... = (todos P (a#x) ∧ todos P y)" by simp
  finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)" 
    by auto
qed

(* Comentario: Uso de auto. *)

(* danrodcha fracorjim1 *)
lemma todos_append6:
  "todos P (x @ y) = (todos P x ∧ todos P y)" (is "?Q x")
proof (induct x)
  show "?Q []" by simp
next
fix x a assume HI: "?Q x"
  have "todos P ((a # x) @ y) = todos P (a # x @ y)" by simp
  also have "… = ((P a) ∧ todos P (x @ y))" by simp
  also have "… = ((P a) ∧ (todos P x ∧ todos P y))" using HI by simp
  also have "… = (todos P (a # x) ∧ todos P y)" by simp
  finally show "?Q (a # x)" by simp
qed

(* pabrodmac *)
lemma todos_append7:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next 
  fix a x
  assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)" 
  have "todos P ((a#x) @ y) = (P a ∧ todos P (x @ y))" by simp
  also have "... = (P a ∧ (todos P x ∧ todos P y))" using HI by simp
  finally show "todos P ((a#x) @ y) = (todos P (a#x) ∧ todos P y)" 
    by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.1. Demostrar o refutar automáticamente 
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

(* migtermor ivamenjim marpoldia1 serrodcal anaprarod paupeddeg
   dancorgar antsancab1 fracorjim1 *) 
lemma "todos P (rev xs) = todos P xs" 
apply (induct xs)
apply simp
apply (simp add: todos_append)
apply auto
done

(* ferrenseg crigomgom rubgonmar fraortmoy josgarsan danrodcha lucnovdos
   pabrodmac *) 
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)
 
(* wilmorort *)
lemma "todos P (rev xs) = todos P xs"
by (induct xs, simp, simp add: todos_append,auto)

(* Comentario: Pasos dentro de by *)

(* juacabsou *)
lemma "todos P (rev xs) = todos P xs"
apply (induct xs, simp, simp add: todos_append, auto) 
done

(* Comentario: Pasos dentro de apply *)

(* pablucoto marcarmor13 jeamacpov *)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto, simp_all add: todos_append) 

(* Comentario: Uso de simp_all *)  
  
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (simp_all add: todos_append, auto)

(* Comentario: Uso de add en simp_all *)  
  
text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.2. Demostrar o refutar detalladamente
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

(* migtermor *)
lemma auxiliar:
 "rev (a#xs) = rev xs @ [a]"
by auto

lemma "todos P (rev xs) = todos P xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by (simp only: rev.simps(1))
next 
  fix a xs
  assume HI: "?Q xs"
  have "todos P (rev (a#xs)) = (todos P (rev xs @ [a]))" 
    by (simp add: "auxiliar")
  have "… = ((todos P (rev xs)) ∧ (todos P [a]))" 
    by (simp add: todos_append)
  have "… =  (todos P (rev xs) ∧ P a)" by simp
  also have Aux: "… = (todos P xs ∧ P a)" using HI by simp
  have Aux1: "… = (P a ∧ todos P xs)" by arith
  have "(todos P (rev xs) ∧ P a) = (P a ∧ todos P xs)" 
    using Aux Aux1 by simp
  finally show "todos P (rev (a#xs)) = todos P (a#xs)" 
    by (simp add: todos_append)
qed

(* Comentarios: 
   + Ruptura de cadena de igualdades.
   + Uso de hechos auxiliares
   + Uso de arith
*)   

(* marpoldia1 ferrenseg crigomgom serrodcal juacabsou rubgonmar
   josgarsan pablucoto pabrodmac lucnovdos marcarmor13 jeamacpov *) 
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix a xs
  assume HI: "todos P (rev xs) = todos P xs"
  have "todos P (rev (a # xs)) = (todos P ((rev xs)@[a]))" by simp
  also have "... = (todos P (rev xs) ∧ todos P [a])" 
    by (simp add:todos_append)
  also have "... = (todos P xs ∧ P a)" using HI by simp
  also have "... = (P a ∧ todos P xs)" by arith
  also have "... = (todos P (a#xs))" by simp
  finally show "todos P (rev (a # xs)) = (todos P (a#xs))" by simp    
qed

(* ivamenjim *)
lemma "todos P (rev xs) = todos P xs" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next 
  fix a xs
  assume HI: "?P xs"
  have "todos P (rev (a # xs)) = (todos P ((rev xs)@[a]))" by simp
  also have "... = ((todos P (rev xs)) ∧ todos P [a])" 
    by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  also have "... = (todos P [a] ∧ todos P xs)" by arith
  finally show "todos P (rev (a # xs)) = todos P (a # xs)" by simp
qed

(* fraortmoy serrodcal *)
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  show "todos P (rev []) = todos P []" by simp
next
  fix a xs 
  assume H1: "todos P (rev xs) = todos P xs"
  have " todos P (rev (a # xs)) = todos P (rev xs @ [a])" by simp
  also have "… = (todos P (rev xs) ∧ todos P [a])" 
    by (simp add:todos_append)
  also have "… = (todos P xs ∧ todos P [a])" using H1 by simp
  also have "… = (todos P [a] ∧ todos P xs)" by arith
  finally show  "todos P (rev (a # xs)) = todos P (a#xs)" by simp
qed

(* paupeddeg dancorgar *)
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  show " todos P (rev []) = todos P []" by simp
next
  fix a xs
  assume HI: "todos P (rev xs) = todos P xs "
  have "todos P (rev (a # xs)) = todos P (rev(xs) @ [a])" by simp
  also have "... = (todos P (rev xs) ∧ todos P [a]) " 
    by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  also have "... = (todos P [a] ∧ todos P xs)" by arith
  also have "... = todos P ([a] @ xs)" by (simp add: todos_append)
  finally show "todos P (rev (a # xs)) = todos P (a # xs)" by simp
qed  

(* wilmorort *)
lemma "todos P (rev xs) = todos P xs" (is "?P xs")
proof (induct xs) 
  show "?P []" by simp 
next
  fix a xs
  assume HI: "?P xs"
  have "todos P (rev (a#xs)) = todos P ((rev xs) @ [a])" by simp
  also have "... = (todos P(rev xs) ∧ todos P [a])" 
    by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  also have "... = (todos P [a] ∧ todos P xs)" 
    by (simp add: HOL.conj_commute)
  also have "... = todos P([a]@(xs))" by (simp)
  finally show  "todos P (rev (a#xs))= todos P (a # xs)" by simp
qed

(* Comentario: Uso de HOL.conj_commute *)

(* anaprarod fracorjim1 *)  
(* es igual que las anteriores pero con el final también con patrones *)
lemma "todos P (rev xs) = todos P xs" (is "?P xs")
proof (induct xs)
  show "?P []" by auto
  next
  fix a xs
  assume HI: "?P xs"
  have "todos P (rev (a#xs)) = todos P (rev xs @ [a])" by simp
  also have "… = (todos P (rev xs) ∧ todos P [a])" 
    by (simp add: todos_append)
  also have "… = (todos P xs ∧ todos P [a])" using HI by simp
  also have "… = (todos P [a] ∧ todos P xs)" by arith
  also have "… = todos P (a#xs)" by simp
  finally show "?P (a # xs)" by simp
qed

(* danrodcha *)
lemma "todos P (rev xs) = todos P xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix a xs assume HI: "?Q xs"
  have "todos P (rev (a#xs)) = todos P ((rev xs) @ [a])" by simp
  also have "… = (todos P (rev xs) ∧ todos P [a])" 
    by (simp add:todos_append)
  also have "… = (todos P xs ∧ todos P [a])" using HI by simp
  also have "… = (todos P [a] ∧ todos P xs)" 
    by (simp add: HOL.conj_commute)
  also have "… = todos P (a # xs)" by simp
  finally show "?Q (a # xs)" by simp
qed

(* antsancab1 *)
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  show "todos P (rev[]) = todos P[]" by simp
next
  fix a xs
  assume HI: "todos P (rev xs) = todos P xs"
  have "todos P (rev(a#xs)) = todos P (rev xs @ [a])" by simp
  also have "... = (todos P (rev xs) ∧ todos P [a])" by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  also have "... = (todos P [a] ∧ todos P xs)" by arith
  also have "... = (todos P ([a] @ xs))" by (simp add: todos_append)
  also have "... = (todos P (a#xs))" by simp
  finally show "todos P (rev (a # xs)) = todos P (a # xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. 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)"
oops

(* migtermor ivamenjim ferrenseg paupeddeg crigomgom serrodcal wilmorort
   juacabsou rubgonmar anaprarod marpoldia1 fraortmoy josgarsan
   danrodcha pablucoto lucnovdos marcarmor13 jeamacpov antsancab1 fracorjim1 pabrodmac *)  
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)" 
quickcheck
oops
(* Quickcheck encuentra el siguiente contraejemplo: 
      P={a1}, Q={a2}, xs={a1,a2}. 
   En este ejemplo:
   · "algunos (λx. P x ∧ Q x) xs = False"
   · "(algunos P xs ∧ algunos Q xs) = True" *)

(* dancorgar *)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof -
  assume H1: "xs = [a, b]"
  assume H2: "P a = True"
  assume H3: "Q a = False"
  assume H4: "P b = False"
  assume H5: "Q b = True" 
  have F1: "(algunos P xs ∧ algunos Q xs) = True" 
    using H1 H2 H3 H4 H5 by simp
  have F2: "algunos (λx. P x ∧ Q x) xs = False" 
    using H1 H2 H3 H4 H5 by simp
  have "algunos (λx. P x ∧ Q x) xs ≠ (algunos P xs ∧ algunos Q xs)" 
    using F1 F2 by simp
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.1. Demostrar o refutar automáticamente 
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

(* ivamenjim migtermor marpoldia1 crigomgom rubgonmar wilmorort anaprarod 
   fraortmoy juacabsou paupeddeg josgarsan danrodcha pablucoto lucnovdos
   marcarmor13 jeamacpov antsancab1 pabrodmac *) 
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

(* ferrenseg *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) simp_all

(* anaprarod dancorgar serrodcal fracorjim1 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
apply (induct xs)
apply auto
done

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.2. Demostrar o refutar detalladamente
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

(* migtermor *)
lemma AUX: "algunos (λa. P (f a)) xs = algunos (P o f) xs"
by (induct xs) auto

lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix x xs
  assume HI: "?Q xs"
  have "algunos P (map f (x#xs)) = (algunos P ((f x)#(map f xs)))" 
    by simp
  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))" 
  proof (cases)
    assume C1: "(P (f x))"
    have Aux: "((P (f x)) ∨ (algunos P (map f xs))) = True" 
      using C1 by simp
    have  Aux1: "… = ((P (f x)) ∨ (algunos (P o f) xs))" 
      using C1 by simp 
    then show "((P (f x)) ∨ (algunos P (map f xs))) = 
               ((P (f x)) ∨ (algunos (P o f) xs))" 
      using Aux Aux1 by simp
  next
    assume C2: "¬(P (f x))"
    have Aux2: "((P (f x)) ∨ (algunos P (map f xs))) = 
                (algunos P (map f xs))" using C2 by simp
    have Aux3: "… = (algunos (P o f) xs)" using HI by (simp add: AUX)
    also have "… =  ((P (f x)) ∨ (algunos (P o f) xs))" 
      using C2 by simp
    then show "((P (f x)) ∨ (algunos P (map f xs))) = 
               ((P (f x)) ∨ (algunos (P o f) xs))" 
      using Aux2 Aux3 by simp
   qed
  also have "… = (((P o f) x) ∨ (algunos (P o f) xs))" by simp
  also have "… = (algunos (P o f) (x#xs))" by simp
  finally show "algunos P (map f (x#xs)) = (algunos (P o f) (x#xs))" 
    by simp
qed

(* Comentario: Se puede simplificar. *)

(* ferrenseg *)
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 x xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  show "algunos P (map f (x # xs)) = algunos (P ∘ f) (x # xs)"
  proof -
    have "algunos P (map f (x # xs)) = algunos P ((f x) # (map f xs))" 
      by simp
    also have "… = ((P (f x)) ∨ (algunos P (map f xs)))" by simp
    also have "… = (((P ∘ f) x) ∨ (algunos (P ∘ f) xs))" 
      using HI by simp
    also have "… = algunos (P ∘ f) (x # xs)" by simp
    finally show ?thesis by simp
  qed
qed

(* ivamenjim *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P ∘ f) []" by simp
next 
  fix a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a # xs)) = algunos P ((f a)#map f xs)" by simp
  also have "... = (algunos P (map f [a]) ∨ algunos P (map f xs))" 
    by simp 
  also have "... = (algunos P (map f [a]) ∨ algunos (P ∘ f) xs)" 
    using HI by simp 
  finally show "algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" 
    by simp
qed

(* crigomgom rubgonmar anaprarod marpoldia1 juacabsou danrodcha
   paupeddeg josgarsan lucnovdos pabrodmac *) 
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P ∘ f) []" by simp
next
  fix x xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (x # xs))  = algunos P ((f x) # (map f xs))" 
    by simp
  also have "... = (P (f x) ∨ algunos P (map f xs))" by simp
  also have "... = (P (f x) ∨ algunos (P ∘ f) xs)" using HI by simp
  also have "... = ((P ∘ f) x ∨ algunos (P ∘ f) xs)" by simp
  finally show "algunos P (map f (x # xs)) = algunos (P ∘ f) (x # xs)" 
    by simp
qed

(* wilmorort pablucoto marcarmor13 jeamacpov *)
lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs" )
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a # xs))  = (P (f a) ∨ algunos P (map f xs))"  
    by simp
  also have "... = (P (f a) ∨ algunos (P ∘ f) xs )" using HI by simp
  also have "... = ((P ∘ f) a ∨ algunos (P ∘ f)xs)" by simp
  finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" 
    by simp
qed

(* fraortmoy serrodcal *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P ∘ f) []"  by simp
next
  fix a xs
  assume H1: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have  "algunos P (map f (a # xs)) = 
         (algunos P (map f [a]) ∨ algunos P (map f xs))" by simp
  also have "… = (algunos (P ∘ f) [a] ∨  algunos (P ∘ f) xs )" 
    using H1 by simp
  also have "… = algunos (P ∘ f) (a#xs)" by simp
  finally show "algunos P (map f (a # xs)) = algunos (P ∘ f) (a#xs)" 
    by simp
qed

(* danrodcha fracorjim1 *)
lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix a xs assume HI: "?Q xs"
  have " algunos P (map f (a # xs)) = algunos P ((f a)#(map f xs))" 
    by simp
  also have "… = (P (f a) ∨ algunos P (map f xs))" by simp
  also have "… = (P (f a) ∨ algunos (P ∘ f) xs)" using HI by blast
  also have "… = ((P ∘ f) a ∨ algunos (P ∘ f) xs)"  by simp
  also have "… = algunos (P ∘ f) (a # xs)" by simp
  finally show "?Q (a # xs)" by blast
qed

(* dancorgar *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P o f) []" by simp
next
  fix x xs
  assume HI: "algunos P (map f xs) = algunos (P o f) xs"
  have "algunos P (map f (x#xs)) = ((P (f x)) ∨ (algunos P (map f xs)))" 
    by simp
  also have "… = ((P (f x)) ∨ (algunos (P o f) xs))" using HI by simp
  finally show "algunos P (map f (x#xs)) = algunos (P o f) (x#xs)" 
    by simp
qed

(* antsancab1 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P ∘ f) []" by simp
next
  fix a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a # xs)) = algunos P (f a # map f xs)" by simp
  also have "... = (P (f a) ∨ algunos P (map f xs))" by simp
  also have "... = (P (f a) ∨ algunos (P ∘ f) xs)" using HI by simp
  also have "... = algunos (P ∘ f) (a#xs)" by simp
  finally show "algunos P (map f (a # xs)) = algunos (P ∘ f) (a#xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.1. Demostrar o refutar automáticamente 
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

(* ivamenjim marpoldia1 paupeddeg crigomgom rubgonmar  wilmorort
   fraortmoy danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
   lucnovdos marcarmor13 jeamacpov antsancab1 pabrodmac *)  
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto

(* ferrenseg *)
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) simp_all

(* anaprarod fracorjim1 *)
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
apply (induct  xs)
apply auto
done

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.2. Demostrar o refutar detalladamente
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

(* ivamenjim ferrenseg marpoldia1 wilmorort dancorgar josgarsan
   juacabsou serrodcal lucnovdos rubgonmar *) 
lemma algunos_append:
  "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 HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  have "algunos P ((a # xs) @ ys) = (P a ∨ (algunos P (xs @ ys)))" 
    by simp
  also have "... = (P a ∨ (algunos P xs ∨ algunos P ys))" 
    using HI by simp
  finally show "algunos P ((a # xs) @ ys) = 
                (algunos P (a # xs) ∨ algunos P ys)" by simp
qed

(* migtermor crigomgom *)
lemma algunos_append2:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next 
  fix x xs
  assume HI: "?Q xs"
  have "algunos P ((x#xs) @ ys) = algunos P (x#(xs @ ys))" by simp
  also have "… = ((P x) ∨ (algunos P (xs @ ys)))" by simp
  also have "… = ((P x) ∨ (algunos P xs) ∨ (algunos P ys))" 
    using HI by simp
  also have "… = ((algunos P (x#xs)) ∨ (algunos P ys))" by simp
  finally show "algunos P ((x#xs) @ ys) = 
                (algunos P (x#xs) ∨ algunos P ys)" by simp
qed

(* paupeddeg*)
lemma algunos_append3:
  "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 HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  have "algunos P ((a # xs) @ ys) = 
        (algunos P [a] ∨ ( algunos P (xs @ ys)))" by simp
  also have "... = (algunos P [a] ∨ (algunos P xs ∨ algunos P ys))" 
    using HI by simp
  finally show "algunos P ((a # xs) @ ys) = 
                (algunos P (a # xs) ∨ algunos P ys)" by simp
qed

(* fraortmoy *)
lemma algunos_append4:
  "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 H1: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  have "algunos P ((a # xs) @ ys) = 
        (algunos P [a] ∨ algunos P (xs @ ys))" by simp
  also have "… = (algunos P [a] ∨ algunos P xs ∨ algunos P ys)" 
    using H1 by simp
  also have "… = ((algunos P [a] ∨ algunos P xs) ∨ algunos P ys)" 
    by simp
  also have "… = (algunos P (a#xs) ∨ algunos P ys)" by simp
  finally show "algunos P ((a # xs) @ ys) = 
                (algunos P (a#xs) ∨ algunos P ys)" by simp
qed

(* danrodcha pablucoto anaprarod marcarmor13 jeamacpov pabrodmac *)
lemma algunos_append5:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix a xs assume HI: "?Q xs"
  have "algunos P ((a#xs) @ ys) = algunos P (a#(xs @ ys))" by simp
  also have "… = (algunos P [a] ∨ algunos P (xs @ ys))" by simp
  also have "… = (algunos P [a] ∨ algunos P xs ∨ algunos P ys)" 
    using HI by simp
  also have "… = (algunos P (a # xs) ∨ algunos P ys)" by simp
  finally show "?Q (a # xs)" by simp
qed

(* antsancab1 *)
lemma algunos_append6: "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 HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  have "algunos P ((a # xs) @ ys) = (P a ∨ algunos P (xs @ ys))" by simp
  also have "... = (P a ∨ algunos P xs ∨ algunos P ys)" using HI by simp
  also have "... = (algunos P (a#xs) ∨ algunos P ys)" by simp
  finally show "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

(* ivamenjim migtermor marpoldia1 rubgonmar paupeddeg dancorgar
   anaprarod serrodcal antsancab1 fracorjim1 *) 
lemma "algunos P (rev xs) = algunos P xs"
apply (induct xs)
apply simp
apply (simp add: algunos_append)
apply auto
done

(* ferrenseg crigomgom danrodcha pablucoto josgarsan pabrodmac lucnovdos
   marcarmor13 jeamacpov *) 
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

(* wilmorort juacabsou *)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs,simp,simp add: algunos_append,auto) 

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.2. Demostrar o refutar detalladamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

(* migtermor *)
lemma auxiliar1:
 "rev (a#xs) = rev xs @ [a]"
by auto 

lemma "algunos P (rev xs) = algunos P xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix x xs
  assume HI: "?Q xs"
  have "algunos P (rev (x#xs)) = (algunos P (rev xs @ [x]))" 
    using auxiliar1 by simp
  also have "… = ((algunos P (rev xs)) ∨ (algunos P [x]))" 
    by (simp add: algunos_append)
  also have "… = ((P x) ∨ (algunos P (rev xs)))" by simp arith
  also have "… = ((P x) ∨ (algunos P xs))" using HI by simp
  finally show "algunos P (rev (x#xs)) = (algunos P (x#xs))" by simp
qed

(* ferrenseg *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix x xs
  assume HI: "algunos P (rev xs) = algunos P xs"
  show "algunos P (rev (x # xs)) = algunos P (x # xs)"
  proof -
    have "algunos P (rev (x # xs)) = algunos P ((rev xs) @ [x])" by simp
    also have "… = (algunos P (rev xs) ∨ algunos P [x])" 
      by (simp add: algunos_append)
    also have "… = (algunos P xs ∨ algunos P [x])" using HI by simp
    also have "… = (algunos P xs ∨ P x)" by simp
    also have "… = (P x ∨ algunos P xs)" by auto
    also have "… = algunos P (x # xs)" by simp
    finally show ?thesis by simp
  qed
qed
 
(* ivamenjim marpoldia1*)
lemma "algunos P (rev xs) = algunos P xs" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next 
  fix a xs
  assume HI: "?P xs"
  have "algunos P (rev (a # xs)) = (algunos P ((rev xs)@[a]))" by simp
  also have "... = ((algunos P (rev xs)) ∨ algunos P [a])" 
    by (simp add: algunos_append)
  also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
  also have "... = (algunos P [a] ∨ algunos P xs)" by arith
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

(* paupeddeg dancorgar serrodcal lucnovdos*)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume HI:"algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (a # xs)) = algunos P ((rev xs) @ [a])" by simp
  also have "... = ((algunos P (rev xs)) ∨ (algunos P [a]))" 
    by (simp add: algunos_append)
  also have "... = ((algunos P xs) ∨ (algunos P [a]))" using HI by simp
  also have "... = ((algunos P [a]) ∨ (algunos P xs))" by arith
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

(* crigomgom pablucoto anaprarod rubgonmar juacabsou marcarmor13 jeamacpov pabrodmac *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
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
  also have "... = (algunos P (rev xs) ∨ algunos P [x])"  
    by (simp add: algunos_append)
  also have "... = (algunos P xs  ∨ algunos P [x])" using HI by simp
  also have "... = (algunos P xs ∨ P x)" by simp
  also have "... = (P x ∨ algunos P xs)" by arith
  also have "... = algunos P (x#xs)" by simp
  finally show "algunos P (rev (x # xs)) = algunos P (x # xs)" by simp
qed

(*wilmorort*)
lemma "algunos P (rev xs) = algunos P xs"  (is "?P xs")
proof (induct xs) 
  show "?P []" by simp 
next
  fix a xs
  assume HI: "?P xs"
  have "algunos P (rev (a#xs)) = algunos P ((rev xs) @ [a])" by simp
  also have "... = (algunos P(rev xs) ∨ algunos P [a])" 
    by (simp add: algunos_append)
  also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
  also have "... = (algunos P [a] ∨ algunos P xs)" 
    by (simp add: HOL.disj_commute)
  also have "... = algunos P([a]@(xs))" by (simp)
  finally show  "algunos  P (rev (a#xs))= algunos P (a # xs)" by simp
qed

(* danrodcha *)
lemma "algunos P (rev xs) = algunos P xs" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix a xs assume HI: "?Q xs"
  have "algunos P (rev (a#xs)) = algunos P ((rev xs) @ [a])" by simp
  also have "… = (algunos P (rev xs) ∨ algunos P [a])" 
    by (simp add:algunos_append)
  also have "… = (algunos P xs ∨ algunos P [a])" using HI by simp
  also have "… = (algunos P [a] ∨ algunos P xs)" 
    by (simp add: HOL.disj_commute)
  also have "… = algunos P (a # xs)" by simp
  finally show "?Q (a # xs)" by simp
qed

(* antsancab1 *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume HI: "algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (a # xs)) = (algunos P ((rev xs) @ [a]))" by simp
  also have "... = (algunos P (rev xs) ∨ algunos P [a])" by (simp add:algunos_append)
  also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
  also have "... = (algunos P [a] ∨ algunos P xs)" by auto
  also have "... = algunos P (a#xs)" by simp
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. 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.
  --------------------------------------------------------------------- 
*}

(* migtermor *)
lemma "algunos (λx. P x ∨ Q x) xs = 
       ((algunos (λx. P x) xs) ∨ (algunos (λx. Q x) xs))"
by (induct xs) auto

lemma "algunos (λx. P x ∨ Q x) xs = 
       ((algunos (λx. P x) xs) ∨ (algunos (λx. Q x) xs))" (is "?R xs")
proof (induct xs)
  show "?R []" by simp
next
  fix x xs
  assume HI: "?R xs"
  have "algunos (λx. P x ∨ Q x) (x#xs) = 
        (((λx. P x ∨ Q x) x) ∨ (algunos (λx. P x ∨ Q x) xs))" by simp
  also have "… = ((P x ∨ Q x) ∨ (algunos (λx. P x ∨ Q x) xs))" by simp
  also have H1: "… = ((((λx. P x) x) ∨ (algunos (λx. P x) xs)) ∨ 
                       (((λx. Q x) x) ∨ (algunos (λx. Q x) xs)))"
    using HI by simp arith
  have H2: "… = ((algunos (λx. P x) (x#xs)) ∨ (algunos (λx. Q x) (x#xs)))" 
    by simp
  have C: "(algunos (λx. P x ∨ Q x) (x#xs)) = 
           ((algunos (λx. P x) (x#xs)) ∨ (algunos (λx. Q x) (x#xs)))" 
    using H1 H2 by simp
  finally show "(algunos (λx. P x ∨ Q x) (x#xs)) = 
                ((algunos (λx. P x) (x#xs)) ∨ (algunos (λx. Q x) (x#xs)))" 
    using C by simp
qed

(* CComentario: Ruptura de la cadena de igualdades. *)

(* ferrenseg *)
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 x xs
  assume HI: "algunos (λx. (P x ∨ Q x)) xs = (algunos P xs ∨ algunos Q xs)"
  show "algunos (λx. P x ∨ Q x) (x # xs) = 
        (algunos P (x # xs) ∨ algunos Q (x # xs))"
  proof -
    have "algunos (λx. P x ∨ Q x) (x # xs) = 
          ((P x) ∨ (Q x) ∨ algunos (λx. P x ∨ Q x) xs)" by simp
    also have "… = ((P x) ∨ (Q x) ∨ algunos P xs ∨ algunos Q xs)" 
      using HI by simp
    also have "… = (((P x) ∨ algunos P xs) ∨ ((Q x) ∨ algunos Q xs))" 
      by auto
    also have "… = (algunos P (x # xs) ∨ algunos Q (x # xs))" by simp
    finally show ?thesis by simp 
  qed
qed

(* Comentario: Uso de auto *)

(* ivamenjim marpoldia1 paupeddeg *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" 
by (induct xs) auto

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 HI: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
  have "algunos (λx. P x ∨ Q x) (a # xs) = 
        (P a ∨ Q a ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "... = (P a ∨ Q a ∨ algunos P xs ∨ algunos Q xs)" 
    using HI by simp
  finally show "algunos (λx. P x ∨ Q x) (a # xs) = 
                (algunos P (a # xs) ∨ algunos Q (a # xs))" by auto
qed

(* Comentario: Uso de auto *)

(* wilmorort danrodcha anaprarod juacabsou rubgonmar*)
lemma "algunos (λx. P x ∨ Q x) xs = 
       (¬todos(λx. ¬P x)xs ∨ ¬todos(λx. ¬Q x)xs)"
by (induct xs) auto

(* wilmorort *)
lemma "algunos (λx. P x ∨ Q x) xs = 
       (¬todos(λx. ¬P x)xs ∨ ¬todos(λx. ¬Q x)xs)"
      (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  have "algunos (λx. P x ∨ Q x) (a # xs) = 
        (P a ∨ Q a ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "... = (P a ∨ Q a ∨  
                    (¬ todos (λx. ¬ P x) xs ∨ ¬ todos (λx. ¬ Q x) xs))" 
    using HI by simp
  also have "... = (P a ∨ ¬ todos (λx. ¬ P x) xs ∨ 
                    Q a ∨  ¬ todos (λx. ¬ Q x) xs )" by arith
  finally show  "algunos (λx. P x ∨ Q x) (a # xs) = 
                 (~ todos (λx. ¬ P x) (a # xs) ∨ 
                   ~ todos (λx. ¬ Q x) (a # xs))" by simp
qed

(* danrodcha *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" 
      (is "?R xs")
proof (induct xs)
  show "?R []" by simp
next
  fix a xs assume HI: "?R xs"
    have 1:" (Q a ∨ algunos P xs) = (algunos P xs ∨ Q a)" 
      by (simp add: HOL.disj_commute)
    have "algunos (λx. P x ∨ Q x) (a # xs) = 
          (algunos P [a] ∨ algunos Q [a] ∨ algunos (λx. P x ∨ Q x) xs)" 
      by simp
    also have "… = (P a ∨ (Q a ∨ algunos P xs) ∨ algunos Q xs)" 
      using HI by simp
    also have "… = (P a ∨ algunos P xs ∨ Q a ∨ algunos Q xs)" 
      using 1 by simp
    also have "… = (algunos P (a # xs) ∨ algunos Q (a # xs))" by simp
    finally show "?R (a # xs)" by simp
qed

(* dancorgar *)
lemma "algunos (λx. P x ∧ Q x) xs ⟹ (algunos P xs ∧ algunos Q xs)"
apply (induct xs)
apply auto
done

(* dancorgar *)
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 xf xs
  assume HI: "algunos (λx. P x ∧ Q x) xs ⟹ (algunos P xs ∧ algunos Q xs)"
  have F1: "algunos (λx. P x ∧ Q x) (xf#xs) ⟹ 
            ((P xf ∧ Q xf) ∨ algunos (λx. P x ∧ Q x) xs)" by simp
  also have F2: "… ⟹ (P xf ∧ Q xf ∨ (algunos P xs ∧ algunos Q xs))" 
    using HI by simp
  have F3: "((P xf ∧ Q xf) ∨ (algunos P xs ∧ algunos Q xs)) ⟹ 
            ((P xf ∨ algunos P xs) ∧ (Q xf ∨ algunos Q xs))" by blast
  have F4: "((P xf ∨ algunos P xs) ∧ (Q xf ∨ algunos Q xs)) ⟹ 
     (algunos P (xf#xs) ∧ algunos Q (xf#xs))" by simp
  show "algunos (λx. P x ∧ Q x) (xf#xs) ⟹ 
        (algunos P (xf#xs) ∧ algunos Q (xf#xs))"
    using F1 F2 F3 F4 by blast
qed

(* pablucoto crigomgom serrodcal marcarmor13 jeamacpov pabrodmac *)
-- "Automatica"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto

-- "Detallada"
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 HI: " algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
  have "algunos (λx. P x ∨ Q x) (a # xs) = 
        (P a ∨ Q a ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "... = (P a ∨ Q a ∨ (algunos P xs ∨ algunos Q xs))" 
    using HI by simp
  also have "… = (((P a) ∨ algunos P xs) ∨ ((Q a) ∨ algunos Q xs))" 
    by arith 
  also have "… = (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
  finally show "algunos (λx. P x ∨ Q x) (a # xs) = 
                (algunos P (a # xs) ∨ algunos Q (a # xs)) " by simp
qed

(* anaprarod juacabsou rubgonmar *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" 
      (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix x xs
  assume HI: "?P xs"
  have "algunos (λx. P x ∨ Q x) (x#xs) =
        (P x ∨ Q x ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "… = (P x ∨ Q x ∨ algunos P xs ∨ algunos Q xs)" 
    using HI by simp
  also have "… = (P x ∨ algunos P xs ∨ Q x ∨ algunos Q xs)" by arith
  finally show "?P (x#xs)"  by simp
qed

(* antsancab1 *)
lemma "algunos(λx. P x ∨ Q x) xs = algunos(λx. P x) xs ∨ algunos(λx. Q x) xs"
by (induct xs) auto

lemma "algunos(λx. P x ∨ Q x) xs = (algunos(λx. P x) xs ∨ algunos(λx. Q x) xs)"
proof (induct xs)
  show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])" by simp
next
  fix a xs
  assume HI: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
  have "algunos (λx. P x ∨ Q x) (a # xs) = (P a ∨ Q a ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "... = (P a ∨ Q a ∨ algunos P xs ∨ algunos Q xs)" using HI by simp
  also have "... = (algunos P (a # xs) ∨ algunos Q (a # xs))" by auto
  finally show "algunos (λx. P x ∨ Q x) (a # xs) = (algunos P (a # xs) ∨ algunos Q (a # xs))" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.1. Demostrar o refutar automáticamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

(* ivamenjim wilmorort migtermor marpoldia1 crigomgom rubgonmar
   paupeddeg danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
   lucnovdos serrodcal marcarmor13 jeamacpov antsancab1 pabrodmac *)  
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto

(* ferrenseg *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) simp_all

(* anaprarod *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" 
apply (induct xs)
apply auto
done

     
text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.2. Demostrar o refutar datalladamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

(* ivamenjim migtermor marpoldia1 crigomgom paupeddeg josgarsan
   juacabsou serrodcal wilmorort *) 
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 HI: "algunos P xs = (¬ todos (λx. ¬ P x) xs)"
  have "algunos P (a # xs) = (P a ∨ (algunos P xs))" by simp
  also have "... = (P a ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
  finally show "algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" 
    by simp
qed

(* ferrenseg *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
  fix x xs
  assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  show "algunos P (x # xs) = (¬ todos (λx. (¬ P x)) (x # xs))"
  proof - 
    have "algunos P (x # xs) = ((P x) ∨ algunos P xs)" by simp
    also have "… = ((P x) ∨ ¬ todos (λx. (¬ P x)) xs)" using HI by simp
    also have "… = (¬ (¬ (P x) ∧ todos (λx. (¬ P x)) xs))" by simp
    also have "… = (¬ todos (λx. (¬ P x)) (x # xs))" by simp
    finally show ?thesis by simp
  qed
qed

(* danrodcha pablucoto anaprarod rubgonmar marcarmor13 jeamacpov pabrodmac *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?Q xs")
proof (induct xs)
  show "?Q []" by simp
next
  fix a xs assume HI: "?Q xs"
  have "algunos P (a # xs) = (P a ∨ algunos P xs)" by simp
  also have "… = (P a ∨ (¬ todos (λx. (¬ P x)) xs))" using HI by simp
  also have "… = (¬(¬(P a) ∧ todos(λx. (¬ P x)) xs))" by simp
  also have "… = (¬ todos(λx. (¬ P x)) (a # xs))" by simp
  finally show "?Q (a # xs)" by simp
qed

(* dancorgar*)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
  fix xf xs
  assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  have "algunos P (xf#xs) = ((P xf) ∨ algunos P xs)" by simp
  also have "… = ( (P xf) ∨ (¬ todos (λx. (¬ P x)) xs) )" 
    using HI by simp
  also have "… = (¬((¬P xf) ∧ (todos (λx. (¬ P x)) xs)))" by simp
  finally show "algunos P (xf#xs) = (¬todos (λx. (¬ P x)) (xf#xs))" 
    by simp
qed

(* lucnovdos*)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
  fix n xs
  assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  have "algunos P (n#xs) = ((P n) ∨ (algunos P xs))" by simp
  also have "… = ((P n) ∨ (¬ todos (λx. (¬ P x)) xs))" using HI by simp
  also have "… = (¬((¬P n) ∧  todos (λx. (¬ P x)) xs))" by simp
  also have "… = (¬ todos (λx. (¬ P x)) (n#xs))" by simp
  finally show "algunos P (n#xs) = (¬ todos (λx. (¬ P x)) (n#xs))" 
    by simp
qed

(* antsancab1 *)
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 HI: "algunos P xs = (¬ todos (λx. ¬ P x) xs)"
  have "algunos P (a # xs) = (P a ∨ algunos P xs)" by simp
  also have "... = (P a ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
  also have "... = (P a ∨ (¬ todos (λx. ¬ P x) (a#xs)))" by auto
  finally show "algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. Definir la funcion primitiva recursiva 
     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
  --------------------------------------------------------------------- 
*}

(* ivamenjim ferrenseg migtermor serrodcal crigomgom rubgonmar
   marpoldia1 paupeddeg danrodcha dancorgar pablucoto anaprarod
   juacabsou lucnovdos marcarmor13 wilmorort jeamacpov fracorjim1 pabrodmac *)  
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []     = False"
| "estaEn x (a#xs) = ((a = x) ∨ (estaEn x xs))"

value "estaEn (2::nat) [3,2,4] = True"
value "estaEn (1::nat) [3,2,4] = False"

(* antsancab1 *)
fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn1 x [] = False"
| "estaEn1 x (a#xs) = (if x = a then True else estaEn1 x xs )"   (* Se detiene al encontrar la primera coincidencia *)

value "estaEn1 (2::nat) [3,2,4] = True"
value "estaEn1 (1::nat) [3,2,4] = False"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

(* migtermor crigomgom  *)
lemma "estaEn x xs = (algunos (λa. a=x) xs)"
by (induct xs) auto

lemma auxiliar13:
 "(x=a) = ((λa. a=x) a)"
by auto

lemma "estaEn x xs = (algunos (λa. a=x) xs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  have "estaEn x (a#xs) = ((a=x) ∨ (estaEn x xs))" by simp
  also have H: "… = ((a=x) ∨ (algunos (λa. a=x) xs))" using HI by simp
  also have "… = (((λa. a=x) a) ∨ (algunos (λa. a=x) xs))" 
    using auxiliar13  by simp
  also have "… = (algunos (λa. a=x) (a#xs))" by simp
  have C: "estaEn x (a#xs) = (algunos (λa. a=x) (a#xs))" using H by simp 
  finally show "estaEn x (a#xs) = (algunos (λa. a=x) (a#xs))" 
    using C by simp
qed

(* Comentario: Ruptura de la cadena de igualdades. Se puede simplificar. *)

(* ferrenseg *)
lemma estaEn_algunos:
  "estaEn y xs = algunos (λx. x=y) xs"
by (induct xs) auto

lemma estaEn_algunos_2:
  "estaEn y xs = algunos (λx. x=y) xs"
proof (induct xs)
  show "estaEn y [] = algunos (λx. x=y) []" by simp
next
  fix x xs
  assume HI: "estaEn y xs = algunos (λx. x=y) xs"
  show "estaEn y (x # xs) = algunos (λx. x=y) (x # xs)"
  proof -
    have "estaEn y (x # xs) = (y=x ∨ estaEn y xs)" by simp
    also have "… = (y=x ∨ algunos (λx. x=y) xs)" using HI by simp
    also have "… = (x=y ∨ algunos (λx. x=y) xs)" by auto
    also have "… = algunos (λx. x=y) (x # xs)" by simp
    finally show ?thesis by simp
  qed
qed

(* Comentario: Uso de auto *)

(* crigomgom paupeddeg dancorgar juacabsou serrodcal lucnovdos wilmorort *)
lemma "estaEn a xs = algunos (λx. x = a) xs"
by (induct xs) auto

lemma "estaEn x xs = (algunos (λa. a=x) xs)" 
proof (induct xs)
  show " estaEn x [] = algunos (λa. a = x) []" by simp
next
  fix a xs
  assume HI: "estaEn x xs = algunos (λa. a = x) xs"
  have "estaEn x (a # xs) = (a = x ∨ estaEn x xs)" by simp
  also have "... = (a = x ∨ algunos (λa. a = x) xs)" using HI by simp
  finally show " estaEn x (a # xs) = algunos (λa. a = x) (a # xs)" 
    by simp
qed

(* ivamenjim marpoldia1 *)
lemma "estaEn x xs = algunos (λy. x=y) xs"
by (induct xs) auto

lemma "estaEn x xs = algunos (λy. x=y) xs"
proof (induct xs)
  show "estaEn x [] = algunos (op = x) []" by simp
next 
  fix a xs
  assume HI: "estaEn x xs = algunos (op = x) xs"
  have "estaEn x (a # xs) = ((a = x) ∨ (estaEn x xs))" by simp
  also have "... =  (a = x ∨ algunos (op = x) xs)" using HI by simp
  finally show " estaEn x (a # xs) = algunos (op = x) (a # xs)" by auto
qed

(* Comentarios:
   + Uso de (op = x)
   + Uso de auto
*)

(* danrodcha *)
lemma "estaEn a xs = algunos (op = a) xs"
by (induct xs) auto

(* danrodcha *)
lemma "estaEn a xs = algunos (op = a) xs"
proof (induct xs)
  show "estaEn a [] = algunos (op = a) []" by simp
next
  fix x xs 
  assume HI: "estaEn a xs = algunos (op = a) xs"
  have "estaEn a (x # xs) = ((x = a) ∨ (estaEn a xs))" by simp
  also have "… = (x = a ∨ algunos (op = a) xs)" using HI by simp
  also have "… = ((op = a) x ∨ algunos (op = a) xs)" 
    by (simp add:HOL.eq_commute)
  also have "… = algunos (op = a) (x # xs)" by simp
  finally show "estaEn a (x # xs) = algunos (op = a) (x # xs)" by simp
qed

(* pablucoto marcarmor13 jeamacpov pabrodmac *)
-- "Automatica"
lemma " estaEn y xs = algunos (λx. x=y) xs"
by (induct xs) auto

-- "Detallada"
lemma " estaEn y xs = algunos (λx. x=y) xs"
proof (induct xs)
  show "estaEn y [] = algunos (λx. x = y) []"  by simp
next
  fix a xs
  assume HI: " estaEn y xs = algunos (λx. x = y) xs "
  have "estaEn y (a # xs) = (y = a ∨ estaEn y xs)"  by simp 
  also have "... = (y = a ∨ algunos (λx. x = y) xs) " using HI by simp
  also have "… = (a=y ∨ algunos (λx. x=y) xs)" by auto
  also have "... = (algunos (λx. x = y) (a#xs))"  by simp
  finally show "estaEn y (a # xs) = algunos (λx. x = y) (a # xs) " 
    by simp
qed

(* Comentario: Uso de auto *)

(* anaprarod *)
(* Automática*)
lemma "estaEn a xs = algunos (λx. a=x) xs" (is "?P xs")
by (induct xs) auto

(* Detallada (igual que las anteriores pero obviando el paso previo al
   finally) *) 
lemma "estaEn a xs = algunos (λx. a=x) xs" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix x xs
  assume HI : "?P xs"
  have "estaEn a (x#xs) = (x=a ∨ estaEn a xs)" by simp
  also have "… = (x=a ∨ algunos (λx. a=x) xs)" using HI by simp
  also have "… = (a=x ∨ algunos (λx. a=x) xs)" using HI by auto
  finally show "?P (x#xs)" by simp
qed

(* Comentario: Uso de auto *)

(* antsancab1 *)
(* Demostrar que
algunos (λa. a=x) xs = estaEn x xs
es lo mismo que demostrar
lemma "estaEn a xs = algunos (λx. a=x) xs" *)

lemma "algunos (λa. a=x) xs = estaEn x xs"
by (induct xs) auto

lemma "algunos (λa. a=x) xs = estaEn x xs"
proof (induct xs)
  show "algunos (λa. a = x) [] = estaEn x []" by simp
next
  fix a xs
  assume HI: "algunos (λa. a = x) xs = estaEn x xs"
  have "algunos (λa. a = x) (a # xs) = ((λa. a = x) a ∨ algunos (λa. a = x) xs)" by simp
  also have "... = ((λa. a = x) a ∨ estaEn x xs)" using HI by simp
  also have "... = (estaEn x (a#xs))" by simp  (* no tengo claro cómo simplifica el "(λa. a = x) a" *)
  finally show "algunos (λa. a = x) (a # xs) = estaEn x (a # xs)" by simp
qed

end

(* fracorjim1 *)
lemma estaEnYAlgunos :
	"estaEn a xs = algunos (λx. x = a) xs" (is "?P a xs")
proof (induct xs)
	show "?P a []" by simp
next
	fix a x xs
	assume HI : "?P a xs"
	have "estaEn a (x#xs) = ((a = x) ∨ estaEn a xs)"
		by (simp only:estaEn.simps(2))
  also have "… = (a = x ∨ algunos (λx. x = a) xs)" using HI by simp
  also have "… = ((λx. x = a) x ∨ algunos (λx. x = a) xs)" by auto
  also have "… = algunos (λx. x = a) (x # xs)" by simp
  finally show "?P a (x#xs)" by simp
qed