Diferencia entre revisiones de «Relación 4»
De Razonamiento automático (2016-17)
(Página creada con 'chapter {* R4: Cuantificadores sobre listas *} theory R4_Cuantificadores_sobre_listas imports Main begin (* Preguntaanaprarod: *) text {* -------------------------------...') |
|||
| (No se muestran 5 ediciones intermedias del mismo usuario) | |||
| Línea 14: | Línea 14: | ||
*} | *} | ||
| − | lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs") | + | lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs") |
| − | proof (induct xs) | + | proof (induct xs) |
| − | + | show "?P []" by simp | |
next | next | ||
fix x xs | 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 | + | qed |
(* no pilla bien los patrones en la inducción en xs y en el resultado de x#xs, es decir: *) | (* no pilla bien los patrones en la inducción en xs y en el resultado de x#xs, es decir: *) | ||
| Línea 45: | Línea 45: | ||
(* 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? *) | (* 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 | ||
Revisión actual del 23:55 22 nov 2016
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