Relación 4
De Razonamiento automático (2016-17)
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