Razonamiento automático (2013-14) Razonamiento automático (2013-14)

header {* R5: Cuantificadores sobre listas *}

theory R5
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. 
  --------------------------------------------------------------------- 
*}
-- "irealetei diecabmen1 pabflomar maresccas4 domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
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"

-- "diecabmen1"
value "algunos (λx. 1<length x) [[2,1,4],[3]]"
value "algunos (λx. 1<length x) [[],[3]]"

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. 
  --------------------------------------------------------------------- 
*}

-- "irealetei diecabmen1 pabflomar maresccas4 domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False"
 | "algunos p (x#xs) = (p x ∨ algunos p  (xs))" --"(xs)=xs  julrobrel"

value "algunos (λx. 1<length x) [[2,1,4],[3]]" -- "TRUE"
value "algunos (λx. 1<length x) [[],[3]]" -- "FALSE"

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

-- "irealetei diecabmen1 pabflomar domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

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

-- "irealetei pabflomar maresccas4 juaruipav domlloriv"
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

-- "diecabmen1 jaisalmen zoiruicha"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P 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 "?P (a#xs)" by auto
qed

--"marescpla"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P Q xs")
proof (induct xs)
show "?P Q []" by simp
next
fix x xs
assume HI: "?P 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)" using HI by simp
also have " ...= ((P x) ∧ (Q x) ∧ todos P xs ∧ todos Q xs) " by simp
also have "... =((P x) ∧ todos P xs ∧ (Q x)∧ todos Q xs)"  by auto
also have " ...= (todos P (x#xs)  ∧ todos Q (x#xs))" by simp
finally show "?P Q (x#xs)" by simp
qed

--"julrobrel: sin usar auto"
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) ∧ ((Q a) ∧ (todos P xs)) ∧ (todos Q xs))" by simp
  also have "...=((P a) ∧ ((todos P xs) ∧ (Q a)) ∧ (todos Q xs))" by (simp add:conj_commute)
  also have "...=((todos P [a]) ∧ (todos P xs) ∧ (todos Q [a]) ∧ (todos Q xs))" by simp
  finally show "todos (λx. P x ∧ Q x) (a#xs) = (todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

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

-- "irealetei diecabmen1 pabflomar maresccas4 domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x ) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.2. Demostrar o refutar detalladamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}
-- "irealetei pabflomar maresccas4 domllorv juaruipav julrobrel"
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

-- "diecabmen1 marescpla jaisalmen zoiruicha"
lemma todos_append: "todos P (x @ y) = (todos P x ∧ todos P y)" (is "?P x y")
proof (induct x)
  show "?P [] y" by simp
next
  fix a x
  assume HI: "?P x 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 "?P (a#x) y" by auto
qed

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

--"maresccas4 julrobrel"

lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (simp_all add:todos_append)
by auto

-- "diecabmen1 irealetei juaruipav domlloriv marescpla jaisalmen zoiruicha"
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

--"irealetei maresccas4"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
 show "todos P (rev []) = todos P []" by simp
next
 fix xs a
 assume HI:"todos P (rev xs) = todos P xs"
 have "todos P (rev (a # xs)) = todos P (rev xs @ [a])" by simp
 also have "... = ( P a ∧ todos P (rev xs))" by (simp add:todos_append) auto
 also have "... = ( P a ∧ todos P xs)" using HI by simp
 finally show "todos P (rev (a # xs))= todos P (a#xs)" by simp
qed
(* pabflomar: Irene, la primera línea es prescindible 
   irealetei: Ya pero lo veo más claro así ^_^O *)


-- "pabflomar domlloriv"
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)) = (P a ∧ todos P (rev xs))" by (simp add:todos_append) auto
  also have "... = (P a ∧ todos P xs)" using HI by simp
  finally show "todos P (rev (a # xs)) = todos P (a # xs)" by simp
qed

-- "diecabmen1 jaisalmen zoiruicha"
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
  finally show "?P (a#xs)" by auto
qed

-- "juaruipav marescpla"
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 auto
   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

--"ya veo que me he vuelto a complicar la vida (marescpla) jajaja"


--"julrobrel: sin usar auto"
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 @ rev [a])" by simp
  also have "...=(todos P (rev xs) ∧ todos P (rev [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 (simp add: conj_commute)
  also have "...=(todos P [a] ∧ todos P xs)" by simp
  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)
  --------------------------------------------------------------------- 
*}

--"irealetei"
(*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
--"Me da que esto es falso"
qed*)



(* irealetei: Me ha gustado la solución de maresccas4 diecabmen1 y me uno *)
(* juaruipav: Antes de empezar la demostración, quickcheck te avisa del contraejemplo*)
-- "maresccas4 diecabmen1 irealetei pabflomar juaruipav domlloriv marescpla julrobrel jaisalmen zoiruicha"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops
(* Contraejemplo:
  P = {a⇣1}
  Q = {a⇣2}
  xs = {a⇣1, a⇣2}
*)

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

-- "irealetei maresccas4 pabflomar domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

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

-- "irealetei diecabmen1 maresccas4 juaruipav domlloriv marescpla"
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 "... = ((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

-- "pabflomar"
(* pabflomar: A mi al menos me resulta más cómoda mi versión, con menos "pasos intermedios" *)

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)) = (P (f a) ∨ algunos P (map f xs))" by simp
  also have "... = (P (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


--"julrobrel"
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 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
  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)
  --------------------------------------------------------------------- 
*}

-- "irealetei diecabmen1 maresccas4 pabflomar domlloriv juaruipav marescpla julrobrel jaisalmen zoiruicha"
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto

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

-- "irealetei maresccas4 pabflomar juaruipav domlloriv marescpla julrobrel"
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

-- "diecabmen1 jaisalmen zoiruicha"
lemma algunos_append:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?P xs ys")
proof (induct xs)
  show "?P [] ys" by simp
next
  fix a xs
  assume HI: "?P xs ys"
  have "algunos P ((a#xs) @ ys) = algunos P (a # xs @ ys) " by simp
  also have "… = (P a ∨ algunos P (xs @ ys))" by simp
  also have "… = (P a ∨ algunos P xs ∨ algunos P ys)" using HI by simp
  finally show "?P (a#xs) ys" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}
 
-- "irealetei diecabmen1 pabflomar juaruipav domlloriv marescpla julrobrel jaisalmen zoiruicha"
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add:algunos_append)

-- "maresccas4"

lemma "algunos P (rev xs) = algunos P xs"
apply (induct xs)
apply (simp_all add:algunos_append)
by auto

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

--"irealetei maresccas4 domlloriv"
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 "... = (P a ∨ algunos P (rev xs))" by (simp add:algunos_append) auto
  also have "... = (P a ∨ algunos P xs)" using HI by simp
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

-- "pabflomar"
(* ṕabflomar: Yo sigo empeñado en lo mismo, la primera linea sobra, ¿qué mas da el orden en el que verifiques el primer elemento de una lista?*)
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)) = (P a ∨ algunos P (rev xs))" by (simp add:algunos_append) auto
  also have "... =  (P a ∨  algunos P xs)" using HI by simp
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

-- "diecabmen1 marescpla jaisalmen zoiruicha"
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
  finally show "?P (a#xs)" by auto
qed

-- "juaruipav"
(* juaruipav: Versión con más "pasos intermedios" (eso que no le gusta a pabflomar),
yo lo veo más útil a la hora de interpretar el código. En otro caso utilizariamos la versión automática *)

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 add:todos_append)
   also have "...= algunos P (a#xs)" by simp
   finally show "algunos P (rev (a # xs)) = algunos P (a#xs)" by simp
  qed

--"julrobrel: sin auto"
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 (simp add:disj_commute)
  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.
  --------------------------------------------------------------------- 
*}

--"irealetei diecabmen1 maresccas4 marescpla julrobrel domlloriv  jaisalmen zoiruicha"
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
  also have "... = (P a  ∨ algunos P xs ∨ Q a ∨ algunos Q xs)" by auto
  finally show " algunos (λx. P x ∨ Q x) (a # xs) = (algunos P (a # xs) ∨ algunos Q (a # xs))" by simp
qed

--"marescpla: encima de largo, me da error xD pero bueno"
lemma "algunos (λx. P x ∨ Q x) xs = algunos (λx. P x) xs ∨ algunos (λx. Q x) 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) = ((λx. P x ∨ Q x) x ∨ algunos (λx. P x ∨ Q x) xs)" by (simp only: algunos.simps(2))
also have "... = ((λx. P x ∨ Q x) x ∨ algunos (λx. P x) xs ∨ algunos (λx. Q x) xs)"using HI by simp
also have "...=((P x)  ∨ (Q x) ∨ algunos (λx. P x) xs ∨ algunos (λx. Q x) xs)" by simp
also have "...=((P x) ∨ algunos (λx. P x) xs ∨ (Q x) ∨ algunos (λx. Q x) xs)" by auto
also have "...=(algunos (λx. P x) (x#xs) ∨ algunos (λx. Q x) (x#xs))" by simp
finally show "?P (x#xs)" by auto
qed

--"julrobrel: sin usar 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)=(algunos (λx. P x ∨ Q x) [a] ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "...=(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 ∨ (Q a ∨ algunos P xs) ∨ algunos Q xs)" by simp
  also have "...=(P a ∨ (algunos P xs ∨ Q a) ∨ algunos Q xs)" by (simp add:disj_commute)
  also have "...=(P a ∨ algunos P xs ∨ Q a ∨ algunos Q xs)" by simp
  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)
  --------------------------------------------------------------------- 
*}

-- "irealetei diecabmen1 maresccas4 juaruipav pabflomar marescpla julrobrel domlloriv jaisalmen zoiruicha"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto

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

--"irealetei maresccas4 domlloriv"
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) xs))" by simp
  also have "... = (¬(¬P a ∧ todos (λx. ¬ P x) xs))" by simp
  finally show "algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" by simp
qed

-- "diecabmen1 marescpla jaisalmen zoiruicha"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P 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 "?P (a#xs)" by simp
qed

-- "juaruipav pabflomar"
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
   
--"julrobrel"  
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) = (algunos 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
  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
  --------------------------------------------------------------------- 
*}

--"irealetei diecabmen1 maresccas4 pabflomar marescpla julrobrel domlloriv juaruipav"
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"

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

fun igual :: "'a ⇒ 'a ⇒ bool" where
"igual x y = (x=y)"


lemma "(algunos (igual x) xs) = (estaEn x xs)"
by (induct xs) auto

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

-- "diecabmen1 marescpla julrobrel domlloriv juaruipav"
lemma "estaEn a xs = algunos (λx. (x=a)) xs"
by (induct xs) auto

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

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

-- "pabflomar"
(* Equivalente a la de diecabmen1, sin predicados.*)

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

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

--"julrobrel: sin usar auto"
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) = (algunos 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
  finally show "algunos P (a # xs) =(¬ (todos (λx. (¬ P x)) (a#xs)))" by simp
qed

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 14. Definir la función primitiva recursiva 
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
*}

-- "diecabmen1"
fun sinDuplicados' :: "'a ⇒'a list ⇒ bool" where
  "sinDuplicados' a [] = True"
| "sinDuplicados' a (x#xs) = (a≠x ∧ sinDuplicados' a xs)"

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

value "sinDuplicados [1::nat,4,2]"
value "sinDuplicados [1::nat,4,2,4]"

-- "maresccas4 pabflomar marescpla julrobrel domlloriv irealetei juaruipav"
fun sinDuplicados2 :: "'a list ⇒ bool" where
  "sinDuplicados [] = True"
| "sinDuplicados (x#xs) = (¬estaEn x xs ∧ sinDuplicados xs)"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 15. Definir la función primitiva recursiva 
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida 
  remdups. 
  --------------------------------------------------------------------- 
*}

-- "diecabmen1"
fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if x ∈ set xs then borraDuplicados xs else x#borraDuplicados xs)"

value " borraDuplicados [1::nat,2,4,2,3]"

-- "maresccas4 irealetei pabflomar marescpla julrobrel domlloriv juaruipav"
fun borraDuplicados2 :: "'a list ⇒ 'a list" where
  "borraDuplicados2 [] = []"
| "borraDuplicados2 (x#xs) = (if estaEn x xs then borraDuplicados2 xs else x # borraDuplicados2 xs)"

(* irealetei: así tambien lo hice, pero no me terminaba de gustar y lo cambié usando el "if"*)
fun borraDuplicados3 :: "'a list => 'a list" where
  "borraDuplicados3 [] = []"
| "borraDuplicados3 (x#xs) = (case estaEn x xs of True => borraDuplicados3 xs | False => x#borraDuplicados3 xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 16.1. Demostrar o refutar automáticamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

-- "diecabmen1 maresccas4 irealetei pabflomar marescpla domlloriv julrobrel juaruipav"

lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 16.2. Demostrar o refutar detalladamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

-- "diecabmen1"
lemma length_borraDuplicados2:
  "length (borraDuplicados xs) ≤ length xs" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  have "length (a#xs) = Suc 0  + length xs" by simp
  also have "length (borraDuplicados (a#xs)) = length (if a ∈ set xs then borraDuplicados xs else a#borraDuplicados xs)" by simp
  have "length xs ≤ Suc 0  + length xs" using HI by simp
  have "length (a#borraDuplicados xs) ≤ Suc 0  + length xs "using HI by simp
  finally show "?P (a#xs)" by simp
qed

-- "maresccas4 irealetei marescpla domlloriv pabflomar juaruipav"
(* pabflomar: A la hora de fijar x y xs no es necesario especificar los tipos.*)
lemma
  "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
 show "length (borraDuplicados []) ≤ length []" by simp
next  
 fix x :: "'a"
 fix xs :: "'a list"
 assume HI: "length (borraDuplicados xs) ≤ length xs"
 have "length (borraDuplicados (x#xs)) ≤ 1 +  length (borraDuplicados xs)" by simp
 also have "... ≤ 1 + length xs" using HI by simp
 finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)" by simp
qed

--"julrobrel"
lemma "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next
  fix a xs
  assume HI:"length (borraDuplicados xs) ≤ length xs"
  have "length (borraDuplicados (a # xs)) ≤ 1 + length (borraDuplicados (xs))" by simp
  also have "...≤ 1 + length xs" using HI by simp
  finally show "length (borraDuplicados (a # xs)) ≤ length (a#xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 17.1. Demostrar o refutar automáticamente 
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

-- "maresccas4 irealetei marescpla diecabmen1 julrobrel domlloriv juaruipav"
lemma "estaEn a (borraDuplicados2 xs) = estaEn a xs"
by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 17.2. Demostrar o refutar detalladamente
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

-- "maresccas4"
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados2 xs) = estaEn a xs"
proof (induct xs)
 show "estaEn a (borraDuplicados2 []) = estaEn a []" by simp
next 
 fix x xs
 assume HI: "estaEn a (borraDuplicados2 xs) = estaEn a xs"
 have "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (if estaEn x xs then borraDuplicados2 xs else x # borraDuplicados2 xs)" by simp
 also have "... = (if estaEn x xs then estaEn a (borraDuplicados2 xs) else estaEn a (x#borraDuplicados2 xs))" by simp
 also have "... = (if estaEn x xs then estaEn a xs else (x=a ∨ estaEn a xs))" using HI by simp
 also have "... = (if estaEn x xs then estaEn a xs else estaEn a (x#xs))" by simp
 finally show "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (x#xs)" by auto
qed

-- "maesccas4 irealetei diecabmen1 domlloriv marescpla juaruipav"
lemma estaEn_borraDuplicados_porCasos:
 "estaEn a (borraDuplicados2 xs) = estaEn a xs"
proof (induct xs)
 show "estaEn a (borraDuplicados2 []) = estaEn a []" by simp
next
 fix x xs
 assume HI: "estaEn a (borraDuplicados2 xs) = estaEn a xs"
 show "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (x#xs)"
 proof (cases)
  assume "estaEn x xs"
  then have "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (borraDuplicados2 xs)" by simp
  also have "...= estaEn a xs" using HI by simp
  finally show "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (x#xs)" by auto
 next
  assume "¬estaEn x xs"
  then have "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (x#borraDuplicados2 xs)" by simp
  also have "...= (x = a ∨ estaEn a (borraDuplicados2 xs))" by simp
  finally show "estaEn a (borraDuplicados2 (x#xs)) = estaEn a (x#xs)" using HI by simp
 qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.1. Demostrar o refutar automáticamente 
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

-- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav"
lemma "sinDuplicados (borraDuplicados xs)"
by  (induct xs) (auto simp add: estaEn_borraDuplicados)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.2. Demostrar o refutar detalladamente
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

-- "maresccas4"
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados2 xs)"
proof (induct xs)
 show "sinDuplicados (borraDuplicados2 [])" by simp
next
 fix x :: "'a"
 fix xs :: "'a list"
 assume HI: "sinDuplicados (borraDuplicados2 xs)"
 have "sinDuplicados (borraDuplicados2 (x#xs)) = sinDuplicados ((if estaEn x xs then borraDuplicados2 xs else x # borraDuplicados2 xs))" by simp
 also have "...= (if estaEn x xs then sinDuplicados (borraDuplicados2 xs) else sinDuplicados (x#borraDuplicados2 xs))" by simp
 also have "...= (if estaEn x xs then sinDuplicados (borraDuplicados2 xs) else (¬estaEn x (borraDuplicados2 xs) ∧ sinDuplicados (borraDuplicados2 xs)))" by simp
 also have "...= (if estaEn x xs then sinDuplicados (borraDuplicados2 xs) else (¬estaEn x xs ∧ sinDuplicados (borraDuplicados2 xs)))" by (simp add: estaEn_borraDuplicados)
 then show "sinDuplicados (borraDuplicados2 (x#xs))" using HI by (simp add: estaEn_borraDuplicados)
qed

lemma sinDuplicados_borraDuplicados_porCasos:
  "sinDuplicados (borraDuplicados2 xs)"
proof (induct xs)
 show "sinDuplicados (borraDuplicados2 [])" by simp
next
 fix x :: "'a"
 fix xs :: "'a list"
 assume HI: "sinDuplicados (borraDuplicados2 xs)"
 show "sinDuplicados (borraDuplicados2 (x#xs))"
 proof (cases)
  assume h1: "estaEn x xs"
  have "sinDuplicados (borraDuplicados2 (x#xs)) = sinDuplicados ((if estaEn x xs then borraDuplicados2 xs else x # borraDuplicados2 xs))" by simp
  also have "...= sinDuplicados (borraDuplicados2 xs)" using  h1 by simp
  finally show "sinDuplicados (borraDuplicados2 (x#xs))" using HI  by simp
 next
  assume h2: "¬estaEn x xs"
  have "sinDuplicados (borraDuplicados2 (x#xs)) = sinDuplicados ((if estaEn x xs then borraDuplicados2 xs else x # borraDuplicados2 xs))" by simp
  also have "...= sinDuplicados (x#borraDuplicados2 xs)" using h2 by simp
  also have "...= (¬estaEn x xs ∧ sinDuplicados (borraDuplicados2 xs))" by (simp add: estaEn_borraDuplicados)
  also have "...= sinDuplicados (borraDuplicados2 xs)" using  h2 by simp
  finally show "sinDuplicados (borraDuplicados2 (x#xs))" using HI by simp
 qed
qed

--"irealetei diecabmen1 domlloriv marescpla juaruipav"
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
proof (induct xs)
  show "sinDuplicados (borraDuplicados [])" by simp
next
  fix a::"'a"
  fix xs::"'a list"
  assume HI:"sinDuplicados (borraDuplicados xs)"
  show "sinDuplicados (borraDuplicados (a # xs))"
  proof (cases)
    assume "estaEn a xs"
    then have "sinDuplicados (borraDuplicados (a # xs)) = sinDuplicados (borraDuplicados xs)" by simp
    also have "... = True" using HI by simp
    finally show "sinDuplicados (borraDuplicados (a # xs))" by simp
  next
    assume HI2:"¬estaEn a xs"
    then have "sinDuplicados (borraDuplicados (a # xs)) = sinDuplicados (a # borraDuplicados xs)" by simp
    also have "... = (¬estaEn a (borraDuplicados xs) ∧ sinDuplicados(borraDuplicados xs))" by simp
    also have "... = (¬estaEn a (borraDuplicados xs) ∧ True)" using HI by simp
    also have "...= (¬estaEn a xs)" by (simp add:estaEn_borraDuplicados)
    finally show "sinDuplicados (borraDuplicados (a # xs))" using HI2 by simp
  qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 19. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

-- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav"
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
quickcheck
oops
(* Contraejemplo:
  xs = {a⇣1, a⇣2, a⇣1}
*)

end