Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
| (No se muestran 2 ediciones intermedias de otro usuario) | |||
| Línea 1: | Línea 1: | ||
| − | + | <source lang="isar"> | |
| − | |||
| − | |||
| − | |||
| − | |||
(* paupeddeg *) | (* paupeddeg *) | ||
| Línea 16: | Línea 12: | ||
fix a1 assume HI1: "preOrden (espejo a1) = rev (postOrden a1)" | fix a1 assume HI1: "preOrden (espejo a1) = rev (postOrden a1)" | ||
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 a2) (espejo a1))" by simp |
| + | |||
| + | (* crigomgom *) | ||
| + | (*Puesto que da error en los tipos, lo que se me ocurre que podría solucionar el error es fijar el tipo de x1a, a1 y a2 *) | ||
| + | |||
| + | 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 :: "'b" | ||
| + | fix a1 :: "'b arbol" | ||
| + | fix a2 :: "'b arbol" | ||
| + | assume HI1: "preOrden (espejo a1) = rev (postOrden a1)" | ||
| + | assume HI2: "preOrden (espejo a2) = rev (postOrden a2)" | ||
| + | |||
| + | have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a2) (espejo a1))" by simp | ||
| + | oops | ||
| − | + | </source> | |
Revisión actual del 14:29 9 dic 2016
(* 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 a2) (espejo a1))" by simp
(* crigomgom *)
(*Puesto que da error en los tipos, lo que se me ocurre que podría solucionar el error es fijar el tipo de x1a, a1 y a2 *)
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 :: "'b"
fix a1 :: "'b arbol"
fix a2 :: "'b arbol"
assume HI1: "preOrden (espejo a1) = rev (postOrden a1)"
assume HI2: "preOrden (espejo a2) = rev (postOrden a2)"
have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a2) (espejo a1))" by simp
oops