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*}
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p xs =   "todos p []     = True"
| "todos p (x#xs) = (p x ∧ todos p xs)""

(* ivamenjim migtermor dancorgar wilmorort marpoldia1 ferrenseg *)
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*}
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
   "algunos p []     = False"
| "algunos p (x#xs) = (p x ∨ algunos 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*}
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)
  --------------------------------------------------------------------- 
*}

{*danrodcha*}
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q 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

(* ivamenjim wilmorort *)

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

(* dancorgar *)
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

(* 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
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}
{*danrodcha ivamenjim marpoldia1 migtermor ferrenseg*}
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)
  --------------------------------------------------------------------- 
*}

(* ivamenjim ferrenseg *)

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

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_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) = 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

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

lemma "todos P (rev xs) = todos P xs"
oops

(* migtermor ivamenjim marpoldia1 *)
lemma "todos P (rev xs) = todos P xs" 
apply (induct xs)
apply simp
apply (simp add: todos_append)
apply auto
done

(* ferrenseg *)

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

lemma "todos P (rev xs) = todos P xs"
oops

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


(* marpoldia1 ferrenseg *)
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

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


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

(* ivamenjim migtermor *)

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

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

lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

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

(* 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
  qed
qed

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

(* ivamenjim *)

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

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

(* ivamenjim ferrenseg *)

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

lemma algunos_append:
  "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

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

(* ivamenjim migtermor ferrenseg *)

lemma "algunos P (rev xs) = algunos P xs"
apply (induct xs)
apply simp
apply (simp add: algunos_append)
apply auto
done

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

lemma "algunos P (rev xs) = algunos P xs"
oops

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


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

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

(* ivamenjim wilmorort ferrenseg migtermor *)

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

(* ivamenjim migtermor *)

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

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

(* migtermor *)

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


end