2016-11-22T21:55:40Z

Danrodcha:

chapter {* R4: Cuantificadores sobre listas *}

theory R4_Cuantificadores_sobre_listas
imports Main
begin

(* Preguntaanaprarod: *)

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" (is "?P xs")
proof (induct xs)
show "?P []" 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
also have "… = algunos (P ∘ f) (x#xs)" by simp
finally show "algunos P (map f (x#xs)) = algunos (P ∘ f) (x#xs)" by simp
qed

(* no pilla bien los patrones en la inducción en xs y en el resultado de x#xs, es decir: *)

lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs" (* da error en la línea que usa la HI (no admite el by simp) *)
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
also have "… = algunos (P ∘ f) (x#xs)" by simp
finally show "?P (x#xs)" by simp (* no admite el by simp *)
qed

(* Me hace pensar que hay que usar otra regla cuando se usan patrones, pero en un ejercicio anterior (ver 5.2) me lo aceptaba... ¿Alguna idea de lo que pasa? *)

{* danrodcha: si quitas los patrones ya funciona xDD *}

{*danrodcha: si aumentas un poco los demostradores si sale: *}

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

Discusión:Relación 4

2016-11-22T21:55:00Z

Danrodcha:

Discusión:Relación 4

2016-11-22T21:54:02Z

Danrodcha:

2016-11-22T21:40:26Z

Danrodcha:

Relación 4

2016-11-22T21:38:40Z

Danrodcha:

<source lang="isar">
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 paupeddeg pablucoto crigomgom anaprarod serrodcal juacabsou rubgonmar josgarsan fraortmoy lucnovdos*)
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*}
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 paupeddeg pablucoto anaprarod serrodcal juacabsou rubgonmar josgarsan fraortmoy lucnovdos*}
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 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

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

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

{* wilmorort pablucoto crigomgom anaprarod juacabsou rubgonmar fraortmoy *}

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

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*}
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

{* anaprarod dancorgar *}
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*)

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

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

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

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

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 serrodcal anaprarod paupeddeg *)
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*)

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)

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

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

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

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 crigomgom serrodcal juacabsou rubgonmar josgarsan pablucoto*)
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 *)

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

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

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*)
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 marpoldia1 crigomgom rubgonmar wilmorort anaprarod
fraortmoy juacabsou paupeddeg josgarsan danrodcha*)

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 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
apply (induct xs)
apply auto
done

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

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

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

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

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

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

(* paupeddeg*)
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) = (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_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 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

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

(* ivamenjim migtermor marpoldia1 rubgonmar paupeddeg *)

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

(* ferrenseg crigomgom*)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

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

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

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

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

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

(* ivamenjim marpoldia1 *)

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

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

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

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

(* ivamenjim wilmorort migtermor marpoldia1 crigomgom rubgonmar paupeddeg*)

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

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

(* ivamenjim migtermor marpoldia1 crigomgom paupeddeg*)

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

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

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

(*crigomgom paupeddeg*)

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

end
</source>

Relación 4

2016-11-17T17:19:08Z

Danrodcha:

2016-11-11T23:53:58Z

Danrodcha:

<source lang="isar">
chapter {* R3: Razonamiento sobre programas *}

theory R3_Razonamiento_sobre_programas
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1.1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"

text {* ---------------------------------------------------------------
Ejercicio 1.2. Escribir la demostración detallada de
sumaImpares n = n*n
------------------------------------------------------------------- *}

-- "La demostración detallada es"
(* crigomgom fraortmoy marpoldia1 ivamenjim *)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0 * 0" by simp
next
fix n
assume HI: "sumaImpares n = n * n"
have "sumaImpares (Suc n) = sumaImpares n + 2*n + 1" by simp
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = Suc n * Suc n" by simp
finally show "sumaImpares (Suc n) = Suc n * Suc n" by simp
qed

(*danrodcha ; es la misma demostración que la anterior pero uso ?P para sustituir la propiedad.*)
lemma "sumaImpares n = n*n" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n
assume HI: "?P n"
have "sumaImpares (Suc n) = sumaImpares n + 2*n + 1" by simp
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = Suc n * Suc n" by simp
finally show "?P (Suc n)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 2.1. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 2"
| "sumaPotenciasDeDosMasUno (Suc n) =
sumaPotenciasDeDosMasUno n + 2^(n+1)"

text {* ---------------------------------------------------------------
Ejercicio 2.2. Escribir la demostración detallada de
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

(*crigomgom ivamenjim danrodcha*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2 ^ (0 + 1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2 ^ (n + 1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp
also have "... = 2 ^ (n + 1) + 2 ^ (n + 1)" using HI by simp
also have "... = 2 ^ ((Suc n) + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp
qed

(* fraortmoy *)
(* es la misma demostración, pero quise probar a delimitar lo que se usa en el "by simp" *)

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2 ^ (0 + 1)" by simp
next
fix n
assume H1:" sumaPotenciasDeDosMasUno n = 2 ^ (n + 1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n + 1)" by (simp only : sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2 ^ (n + 1) + 2 ^ (n + 1)" using H1 by simp
also have "... = 2 ^ (Suc n + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 3.1. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []"
| "copia (Suc n) x = x # copia n x"

text {* ---------------------------------------------------------------
Ejercicio 3.2. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 3.2. Demostrar detalladamente que todos los elementos de
(copia n x) son iguales a x.
------------------------------------------------------------------- *}

(* crigomgom *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y = x) (copia 0 x)" by simp
next
fix n
assume HI: "todos (λy. y = x) (copia n x)"
have "todos (λy. y = x) (copia (Suc n) x) = todos (λy. y = x) (x # (copia n x))" by simp
also have "... = ((x = x) ∧ (todos (λy. y = x) (copia n x)))" by simp
also have "... = True" using HI by simp
finally show "todos (λy. y = x) (copia (Suc n) x)" by simp
qed

(* fraortmoy *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
have "todos (λy. y = x) (copia 0 x) = todos (λy. y = x) []" by (simp only: copia.simps(1))
also have "... = True" by (simp only: todos.simps(1))
show "todos (λy. y = x) (copia 0 x)" by simp
next
fix n
assume H1 : " todos (λy. y = x) (copia n x) "
have "todos (λy. y = x) (copia (Suc n) x) = ((todos (λy. y = x) (x#[])) ∧ (todos (λy. y = x) (copia n x) )) " by simp
also have " ... = (todos (λy. y = x) (x#[]))" using H1 by simp
also have " ... = ((λy. y = x) x ∧ todos (λy. y = x) [])" by simp
also have " ... = True" by simp
finally show " todos (λy. y = x) (copia (Suc n) x)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 4.1. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"

text {* ---------------------------------------------------------------
Ejercicio 4.2. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
Indicación: La propiedad mult_Suc es
(Suc m) * n = n + m * n
Puede que se necesite desactivarla en un paso con
(simp del: mult_Suc)
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (x * Suc n)"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

(* fraortmoy *)
lemma fact: "factI' n x = x * factR n"
proof (induct n)
show "factI' 0 x = x * factR 0" by simp
next
fix n
assume H1 : "factI' n x = x * factR n"
have "factI' (Suc n) x = factI' n (x * Suc n)" by (simp only:factI'.simps(2))
also have "... = (x * Suc n) * factR n" using H1 by simp (* no entiendo por qué no hace esto bien y luego todo funciona *)
also have "... = x * factR (Suc n)" by (simp del: mult_Suc)
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 4.3. Escribir la demostración detallada de
factI n = factR n
------------------------------------------------------------------- *}

(* fraortmoy *)
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1" by simp
also have "... = 1 * factR n" by (simp add: fact)
finally show "factI n = factR n" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 5.1. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]"
| "amplia (x#xs) y = x # amplia xs y"

text {* ---------------------------------------------------------------
Ejercicio 5.2. Escribir la demostración detallada de
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

(* crigomgom fraortmoy *)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x # xs) y = x # (amplia xs y)" by simp
also have "... = x # (xs @ [y])" using HI by simp
also have "... = (x # xs) @ [y]" by simp
finally show "amplia (x # xs) y = (x # xs) @ [y]" by simp
qed

end
</source>