Relación 4
De Razonamiento automático (2018-19)
Revisión del 13:15 13 dic 2018 de Cammonagu (discusión | contribuciones)
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.
---------------------------------------------------------------------
*}
(* manperjim pabalagon alfmarcua josgomrom4 aribatval cammonagu raffergon2*)
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.
---------------------------------------------------------------------
*}
(* manperjim pabalagon alfmarcua josgomrom4 cammonagu aribatval raffergon2*)
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)
---------------------------------------------------------------------
*}
(* manperjim pabalagon alfmarcua josgomrom4 cammonagu raffergon2*)
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)
---------------------------------------------------------------------
*}
(* pabalagon *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P P Q xs")
proof (induct xs)
fix P Q
show "?P P Q []" by simp
next
fix a xs
assume HI: "?P P 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 (simp add: HOL.conj_comms)
also have "... = (todos P (a#xs) ∧ (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
(* alfmarcua *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P xs")
proof (induct xs)
have "todos (λx. P x ∧ Q x) [] = (True)" by (simp only: todos.simps(1))
also have "... = (True ∧ True)" by (simp only: conj_absorb)
also have "... = (todos P [] ∧ todos Q [])" by (simp only: todos.simps(1))
finally show "?P []" .
next
fix x xs
assume HI: "?P 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))" by (simp only: HI)
also have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" by (simp only: HOL.conj_comms)
also have "... = (todos P (x # xs) ∧ todos Q (x # xs))" by (simp only: todos.simps(2))
finally show "?P (x#xs)" .
qed
(* josgomrom4 raffergon2 cammonagu *)
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
text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}
(* manperjim pabalagon alfmarcua josgomrom4 aritbatval cammonagu raffergon2*)
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)
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 raffergon2 cammonagu*)
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
(* alfmarcua *)
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)" (is "?P x")
proof (induct x)
have "todos P ([] @ y) = todos P y" by (simp only: append_Nil)
also have "... = (True ∧ todos P y)" by (simp only: simp_thms(22))
also have "... = (todos P [] ∧ todos P y)" by (simp only: todos.simps(1))
finally show "?P []" .
next
fix a x
assume HI:"?P x"
have "todos P ((a # x) @ y) = todos P (a # (x @ y))"
by (simp only:List.append.append_Cons)
also have "... = (P a ∧ todos P (x @ y))" by (simp only: todos.simps(2))
also have "... = (P a ∧ todos P x ∧ todos P y)" by (simp only:HI)
also have "... = ((P a ∧ todos P x) ∧ todos P y)" by (simp only:HOL.conj_assoc)
also have "... = (todos P (a#x) ∧ todos P y)" by (simp only: todos.simps(2))
finally show "?P (a#x)" .
qed
text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua aribatval cammonagu raffergon2*)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (simp_all add: HOL.conj_comms todos_append)
text {*
---------------------------------------------------------------------
Ejercicio 5.2. Demostrar o refutar detalladamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 raffergon2 cammonagu*)
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 xs ∧ P a)" by simp
also have "... = (P a ∧ todos P xs)" by (simp add: HOL.conj_comms)
finally show "todos P (rev (a#xs)) = todos P (a#xs)" by simp
qed
(* alfmarcua *)
lemma "todos P (rev xs) = todos P xs" (is "?P xs")
proof (induct xs)
show "?P []" by (simp only: rev.simps(1))
next
fix a xs
assume HI:"?P xs"
have "todos P (rev (a # xs)) = todos P (rev xs @ [a])" by (simp only: rev.simps(2))
also have "... = (todos P (rev xs) ∧ todos P [a])" by (simp only: todos_append)
also have "... = (todos P xs ∧ todos P [a])" by (simp only: HI)
also have "... = (todos P (a#[]) ∧ todos P xs)" by (simp only: HOL.conj_comms)
also have "... = ((P a ∧ True) ∧ todos P xs)" by (simp only: todos.simps)
also have "... = (P a ∧ todos P xs)" by (simp only: HOL.simp_thms(21))
also have "... = todos P (a#xs)" by (simp only: todos.simps(2))
finally show "?P (a#xs)" .
qed
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}
(* pabalagon *)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
nitpick
oops
(* Contraejemplo *)
value "algunos (λx. even x ∧ odd x) [1, 2::nat] ≠
algunos even [1, 2::nat] ∧ algunos odd [1, 2::nat]"
(* alfmarcua raffergon2 cammonagu*)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops
text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar detalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}
(* pabalagon cammonagu*)
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
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
(* josgomrom4 *)
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
(* alfmarcua *)
lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs")
proof (induct xs)
have "algunos P (map f []) = algunos P []" by (simp only: List.list.map(1))
also have "... = algunos (P o f) []" by (simp only: algunos.simps(1))
finally show "?P []" .
next
fix a xs
assume HI:"?P xs"
have "algunos P (map f (a # xs)) = algunos P (f a # map f xs)" by (simp only: List.list.map(2))
also have "... = (P (f a) ∨ algunos P (map f xs))" by (simp only: algunos.simps(2))
also have "... = (P (f a) ∨ algunos (P o f) xs)" by (simp only:HI)
also have "... = ((P o f) a ∨ algunos (P o f) xs)" by (simp only: Fun.comp_apply)
also have "... = algunos (P o f) (a#xs)" by (simp only: algunos.simps(2))
finally show "?P (a#xs)" .
qed
text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
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)
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 raffergon2 cammonagu*)
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
(* alfmarcua *)
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?P xs")
proof (induct xs)
have "algunos P ([] @ ys) = algunos P ys" by (simp only: append_Nil)
also have "... = (False ∨ algunos P ys)" by (simp only: simp_thms(32))
also have "... = (algunos P [] ∨ algunos P ys)" by (simp only: algunos.simps(1))
finally show "?P []" .
next
fix a xs
assume HI:"?P xs"
have "algunos P ((a # xs) @ ys) = algunos P (a # (xs @ ys))"
by (simp only:List.append.append_Cons)
also have "... = (P a ∨ algunos P (xs @ ys))" by (simp only: algunos.simps(2))
also have "... = (P a ∨ algunos P xs ∨ algunos P ys)" by (simp only:HI)
also have "... = ((P a ∨ algunos P xs) ∨ algunos P ys)" by (simp only:HOL.disj_assoc)
also have "... = (algunos P (a#xs) ∨ algunos P ys)" by (simp only: algunos.simps(2))
finally show "?P (a#xs)" .
qed
text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (simp_all add: HOL.disj_comms algunos_append)
text {*
---------------------------------------------------------------------
Ejercicio 9.2. Demostrar o refutar detalladamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}
(* pabalagon *)
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 xs ∨ P a)" by simp
also have "... = (P a ∨ algunos P xs)" by (simp add: HOL.disj_comms)
finally show "algunos P (rev (a#xs)) = algunos P (a#xs)" by simp
qed
(* josgomrom4 raffergon2 cammonagu*)
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
(* alfmarcua *)
lemma "algunos P (rev xs) = algunos P xs" (is "?P xs")
proof (induct xs)
show "?P []" by (simp only: rev.simps(1))
next
fix a xs
assume HI:"?P xs"
have "algunos P (rev (a # xs)) = algunos P (rev xs @ [a])" by (simp only: rev.simps(2))
also have "... = (algunos P (rev xs) ∨ algunos P [a])" by (simp only: algunos_append)
also have "... = (algunos P xs ∨ algunos P [a])" by (simp only: HI)
also have "... = (algunos P (a#[]) ∨ algunos P xs)" by (simp only: HOL.disj_comms)
also have "... = ((P a ∨ False) ∨ algunos P xs)" by (simp only: algunos.simps)
also have "... = (P a ∨ algunos P xs)" by (simp only: HOL.simp_thms(31))
also have "... = algunos P (a#xs)" by (simp only: algunos.simps(2))
finally show "?P (a#xs)" .
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.
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto
(* pabalagon josgomrom4 cammonagu*)
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 (simp add: HOL.disj_comms)
finally show "algunos (λx. P x ∨ Q x) (a#xs) = (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed
(* alfmarcua *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" (is "?P xs")
proof (induct xs)
show "?P []" by (simp only: algunos.simps(1) HOL.simp_thms(33))
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 only: algunos.simps(2))
also have "... = ((P a ∨ Q a) ∨ algunos P xs ∨ algunos Q xs)" by (simp only: HI)
also have "... = ((P a ∨ algunos P xs) ∨ Q a ∨ algunos Q xs)"
by (simp only: HOL.disj_assoc HOL.disj_comms)
also have "... = (algunos P (a # xs) ∨ algunos Q (a # xs))" by (simp only: algunos.simps(2))
finally show "?P (a#xs)" .
qed
text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
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)
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 cammonagu*)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
have "algunos P [] = False" by simp
also have "... = (¬ todos (λx. (¬ P x)) [])" by simp
finally show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
fix a xs
assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
have "(¬ todos (λx. (¬ P x)) (a#xs)) = (¬ ((¬ P a) ∧ todos (λx. (¬ P x)) xs))" by simp
also have "... = (P a ∨ ¬ todos (λx. (¬ P x)) xs)" by simp
also have "... = (P a ∨ algunos P xs)" using HI by simp
finally show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))" by simp
qed
(* alfmarcua *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?P xs")
proof (induct xs)
have "algunos P [] = False" by (simp only:algunos.simps(1))
also have "... = (¬ True)" by (simp only: HOL.simp_thms(7))
also have "... = (¬ todos (λx. (¬ P x)) [])" by (simp only: todos.simps(1))
finally show "?P []" .
next
fix a xs
assume HI:"?P xs"
have "algunos P (a # xs) = (P a ∨ algunos P xs)" by (simp only: algunos.simps(2))
also have "... = (P a ∨ ¬ todos (λx. (¬ P x)) xs)" by (simp only: HI)
also have "... = (¬ ¬ P a ∨ ¬ todos (λx. (¬ P x)) xs)" by (simp only: HOL.simp_thms(1))
also have "... = (¬ (¬ P a ∧ todos (λx. (¬ P x)) xs))" by (simp only: HOL.de_Morgan_conj)
also have "... = (¬ todos (λx. (¬ P x)) (a#xs))" by (simp only: todos.simps(2))
finally show "?P (a#xs)" .
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
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False" |
"estaEn x (y#xs) = (x=y ∨ estaEn x xs)"
text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}
(* manperjim pabalagon josgomrom4 alfmarcua cammonagu*)
lemma "estaEn x xs = algunos (λa. x=a) xs"
by (induct xs) auto
(* pabalagon josgomrom4 cammonagu*)
lemma "estaEn x xs = algunos (λa. x=a) xs"
proof (induct xs)
show "estaEn x [] = algunos (λa. x=a) []" by simp
next
fix y xs
assume HI: "estaEn x xs = algunos (λa. x=a) xs"
have "estaEn x (y#xs) = (x=y ∨ estaEn x xs)" by simp
also have "... = (x=y ∨ algunos (λa. x=a) xs)" using HI by simp
finally show "estaEn x (y#xs) = algunos (λa. x=a) (y#xs)" by simp
qed
(* alfmarcua *)
lemma "estaEn x xs = algunos (λk. x=k) xs" (is "?P xs")
proof (induct xs)
show "?P []" by (simp only: estaEn.simps(1) algunos.simps(1))
next
fix a xs
assume HI:"?P xs"
have "estaEn x (a # xs) = (x=a ∨ estaEn x xs)" by (simp only: estaEn.simps(2))
also have "... = (x=a ∨ algunos (λk. x=k) xs)" by (simp only: HI)
(* also have "... = ((λk. x=k) a ∨ algunos (λk. x=k) xs)" by (simp only:HOL.simp_thms(6)) *)
also have "... = algunos (λk. x=k) (a#xs)" by (simp only: algunos.simps(2))
finally show "?P (a#xs)" .
qed
end