Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
(Página creada con '(* paupeddeg *) (* Tengo un problema con el ejercicio 6. Me aparece que hay algo incorrecto desde las primeras líneas de la demostración, pero al comparar con otras soluciones...') |
|||
| Línea 1: | Línea 1: | ||
| + | chapter {* R6: Recorridos de árboles *} | ||
| + | |||
| + | theory R6_Recorridos_de_arboles | ||
| + | imports Main | ||
| + | begin | ||
| + | |||
(* paupeddeg *) | (* paupeddeg *) | ||
(* Tengo un problema con el ejercicio 6. Me aparece que hay algo incorrecto desde las primeras líneas de la demostración, pero al comparar con otras soluciones no veo la diferencia salvo que yo no he usado patrones *) | (* Tengo un problema con el ejercicio 6. Me aparece que hay algo incorrecto desde las primeras líneas de la demostración, pero al comparar con otras soluciones no veo la diferencia salvo que yo no he usado patrones *) | ||
| Línea 11: | Línea 17: | ||
fix a2 assume HI2: "preOrden (espejo a2) = rev (postOrden a2)" | fix a2 assume HI2: "preOrden (espejo a2) = rev (postOrden a2)" | ||
have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a1) (espejo a2))" by simp | have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a1) (espejo a2))" by simp | ||
| + | |||
| + | end | ||
Revisión del 20:52 6 dic 2016
chapter {* R6: Recorridos de árboles *}
theory R6_Recorridos_de_arboles imports Main begin
(* paupeddeg *) (* Tengo un problema con el ejercicio 6. Me aparece que hay algo incorrecto desde las primeras líneas de la demostración, pero al comparar con otras soluciones no veo la diferencia salvo que yo no he usado patrones *)
lemma "preOrden (espejo a) = rev (postOrden a)" proof (induct a)
fix x show "preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
fix x1a fix a1 assume HI1: "preOrden (espejo a1) = rev (postOrden a1)" fix a2 assume HI2: "preOrden (espejo a2) = rev (postOrden a2)" have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a1) (espejo a2))" by simp
end