Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle») |
|||
| (No se muestran 21 ediciones intermedias de 6 usuarios) | |||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
chapter {* R6: Recorridos de árboles *} | chapter {* R6: Recorridos de árboles *} | ||
| Línea 24: | Línea 24: | ||
juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg | juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg | ||
crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy | crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy | ||
| − | dancorgar fracorjim1*) | + | dancorgar fracorjim1 anaprarod antsancab1 *) |
datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol" | datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol" | ||
| Línea 42: | Línea 42: | ||
(* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor | (* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor | ||
| − | wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg marcarmor13 josgarsan | + | wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg |
| − | + | marcarmor13 josgarsan dancorgar anaprarod antsancab1 *) | |
fun preOrden :: "'a arbol ⇒ 'a list" where | fun preOrden :: "'a arbol ⇒ 'a list" where | ||
| − | "preOrden (H t) = [t]" | + | "preOrden (H t) = [t]" |
| "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)" | | "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)" | ||
| Línea 52: | Línea 52: | ||
rubgonmar paupeddeg fracorjim1 *) | rubgonmar paupeddeg fracorjim1 *) | ||
fun preOrden1 :: "'a arbol ⇒ 'a list" where | fun preOrden1 :: "'a arbol ⇒ 'a list" where | ||
| − | "preOrden1 (H x) = [x]" | + | "preOrden1 (H x) = [x]" |
| − | | "preOrden1 (N x i d) = x#preOrden1 i @ preOrden1 d" | + | | "preOrden1 (N x i d) = x # preOrden1 i @ preOrden1 d" |
value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h))) | value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h))) | ||
| Línea 78: | Línea 78: | ||
pablucoto bowma fraortmoy migtermor wilmorort lucnovdos | pablucoto bowma fraortmoy migtermor wilmorort lucnovdos | ||
juacabsou serrodcal pabrodmac ferrenseg jeamacpov | juacabsou serrodcal pabrodmac ferrenseg jeamacpov | ||
| − | rubgonmar paupeddeg marcarmor13 josgarsan dancorgar *) | + | rubgonmar paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *) |
fun postOrden :: "'a arbol ⇒ 'a list" where | fun postOrden :: "'a arbol ⇒ 'a list" where | ||
| − | "postOrden (H t) = [t]" | + | "postOrden (H t) = [t]" |
| "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]" | | "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]" | ||
| Línea 101: | Línea 101: | ||
migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac | migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac | ||
ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan | ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan | ||
| − | dancorgar *) | + | dancorgar anaprarod antsancab1 *) |
| − | |||
fun inOrden :: "'a arbol ⇒ 'a list" where | fun inOrden :: "'a arbol ⇒ 'a list" where | ||
| − | "inOrden (H t) = [t]" | + | "inOrden (H t) = [t]" |
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)" | | "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)" | ||
| − | + | (* danrodcha manmorjim1 fracorjim1 *) | |
| − | (* danrodcha manmorjim1 *) | ||
fun inOrden1 :: "'a arbol ⇒ 'a list" where | fun inOrden1 :: "'a arbol ⇒ 'a list" where | ||
| − | "inOrden1 (H t) = [t]" | + | "inOrden1 (H t) = [t]" |
| "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d" | | "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d" | ||
| Línea 137: | Línea 135: | ||
pablucoto bowma fraortmoy migtermor wilmorort lucnovdos | pablucoto bowma fraortmoy migtermor wilmorort lucnovdos | ||
juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar | juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar | ||
| − | paupeddeg marcarmor13 josgarsan dancorgar *) | + | paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *) |
| − | |||
fun espejo :: "'a arbol ⇒ 'a arbol" where | fun espejo :: "'a arbol ⇒ 'a arbol" where | ||
| − | "espejo (H t) = H t" | + | "espejo (H t) = H t" |
| "espejo (N t i d) = N t (espejo d) (espejo i)" | | "espejo (N t i d) = N t (espejo d) (espejo i)" | ||
value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h))) | value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h))) | ||
= N e (N g (H h) (H f)) (N c (H d) (H a))" | = N e (N g (H h) (H f)) (N c (H d) (H a))" | ||
| − | |||
text {* | text {* | ||
| Línea 154: | Línea 150: | ||
*} | *} | ||
| − | (* ivamenjim migtermor wilmorort juacabsou serrodcal dancorgar *) | + | (* ivamenjim migtermor wilmorort juacabsou serrodcal dancorgar josgarsan |
| − | + | *) | |
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 164: | Línea 160: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp | + | have "preOrden (espejo (N x i d)) = |
| − | also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))" by simp | + | preOrden (N x (espejo d) (espejo i))" by simp |
| − | also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" using h1 h2 by simp | + | also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))" |
| − | finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp | + | by simp |
| − | + | also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" | |
| + | using h1 h2 by simp | ||
| + | finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" | ||
| + | by simp | ||
qed | qed | ||
| − | (* danrodcha paupeddeg *) | + | (* danrodcha paupeddeg anaprarod *) |
lemma "preOrden (espejo a) = rev (postOrden a)" | lemma "preOrden (espejo a) = rev (postOrden a)" | ||
by (induct a) simp_all | by (induct a) simp_all | ||
| − | (* danrodcha crigomgom*) | + | |
| − | lemma " | + | (* danrodcha crigomgom fracorjim1 *) |
| + | lemma "preOrden1 (espejo a) = rev (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
fix x | fix x | ||
| Línea 184: | Línea 184: | ||
assume HIi: "?P i" | assume HIi: "?P i" | ||
assume HId: "?P d" | assume HId: "?P d" | ||
| − | have " | + | have "preOrden1 (espejo (N x i d)) = |
| + | preOrden1 (N x (espejo d) (espejo i))" | ||
by (simp only: espejo.simps(2)) | by (simp only: espejo.simps(2)) | ||
| − | also have "… = x# | + | also have "… = x#preOrden1 (espejo d) @ preOrden1 (espejo i)" |
| − | by (simp only: | + | by (simp only: preOrden1.simps(2)) |
also have"… = x#rev (postOrden d) @ rev (postOrden i)" | also have"… = x#rev (postOrden d) @ rev (postOrden i)" | ||
using HIi HId by simp | using HIi HId by simp | ||
| Línea 194: | Línea 195: | ||
qed | qed | ||
| − | (* danrodcha fraortmoy *) | + | (* danrodcha fraortmoy anaprarod *) |
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 212: | Línea 213: | ||
done | done | ||
| − | (* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13*) | + | (* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *) |
| − | |||
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 222: | Línea 222: | ||
assume h1: "?P i" | assume h1: "?P i" | ||
assume h2: "?P d" | assume h2: "?P d" | ||
| − | have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp | + | have "preOrden (espejo (N x i d)) = |
| − | also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))" by simp | + | preOrden (N x (espejo d) (espejo i))" by simp |
| − | also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" using h1 h2 by simp | + | also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))" |
| + | by simp | ||
| + | also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" | ||
| + | using h1 h2 by simp | ||
also have "... = [x] @ rev (postOrden i @ postOrden d)" by simp | also have "... = [x] @ rev (postOrden i @ postOrden d)" by simp | ||
also have "... = rev ( postOrden i @ postOrden d @ [x] ) " by simp | also have "... = rev ( postOrden i @ postOrden d @ [x] ) " by simp | ||
| Línea 234: | Línea 237: | ||
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?p a") | lemma "preOrden (espejo a) = rev (postOrden a)" (is "?p a") | ||
proof (induct a) | proof (induct a) | ||
| − | fix t | + | fix t |
| − | show "?p (H t)" by simp | + | show "?p (H t)" by simp |
| − | (* Aquí si le diga "preOrden (espejo (H t)) = rev (postOrden (H t))",isabelle dice: | + | (* Aquí si le diga "preOrden (espejo (H t)) = rev (postOrden (H t))", |
| − | proof (prove) | + | isabelle dice: |
| − | goal (1 subgoal): | + | proof (prove) |
| − | + | goal (1 subgoal): | |
| − | Introduced fixed type variable(s): 'b in "t__" | + | 1. preOrden (espejo (H t)) = rev (postOrden (H t)) |
| − | No entiendo porqué *) | + | Introduced fixed type variable(s): 'b in "t__" |
| + | No entiendo porqué *) | ||
next | next | ||
| − | fix t i d | + | fix t i d |
| − | assume H1: "?p i" | + | assume H1: "?p i" |
| − | assume H2: "?p d" | + | assume H2: "?p d" |
| − | have "preOrden (espejo (N t i d)) = preOrden (N t (espejo d) (espejo i))" by simp | + | have "preOrden (espejo (N t i d)) = |
| − | also have "... = [t] @ (preOrden (espejo d)) @ (preOrden (espejo i))" by simp | + | preOrden (N t (espejo d) (espejo i))" by simp |
| − | also have "... = [t] @ rev (postOrden d) @ rev (postOrden i)" using H1 H2 by simp | + | also have "... = [t] @ (preOrden (espejo d)) @ (preOrden (espejo i))" |
| − | finally show "?p (N t i d)" by simp | + | by simp |
| + | also have "... = [t] @ rev (postOrden d) @ rev (postOrden i)" | ||
| + | using H1 H2 by simp | ||
| + | finally show "?p (N t i d)" by simp | ||
qed | qed | ||
| + | |||
| + | (* Comentario sobre tipo inducido. *) | ||
(* fraortmoy lucnovdos pabrodmac*) | (* fraortmoy lucnovdos pabrodmac*) | ||
| − | |||
lemma "preOrden (espejo a) = rev (postOrden a)" | lemma "preOrden (espejo a) = rev (postOrden a)" | ||
by (induct a) auto | by (induct a) auto | ||
(*pabrodmac*) | (*pabrodmac*) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 271: | Línea 278: | ||
show "?P (N x i d)" | show "?P (N x i d)" | ||
proof - | proof - | ||
| − | have "preOrden (espejo (N x i d)) = preOrden(N x (espejo d) (espejo i))" by simp | + | have "preOrden (espejo (N x i d)) = |
| − | also have "… = [x]@rev(postOrden d)@rev(postOrden i)" using h1 h2 by simp | + | preOrden(N x (espejo d) (espejo i))" by simp |
| + | also have "… = [x]@rev(postOrden d)@rev(postOrden i)" | ||
| + | using h1 h2 by simp | ||
also have "… = rev(postOrden (N x i d))" by simp | also have "… = rev(postOrden (N x i d))" by simp | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | qed | ||
qed | qed | ||
| − | |||
(* ferrenseg rubgonmar *) | (* ferrenseg rubgonmar *) | ||
| − | |||
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 301: | Línea 308: | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | qed | ||
| + | qed | ||
| + | |||
| + | (* antsancab1 *) | ||
| + | (* Le he puesto el nombre para utilizarlo en la siguiente demostración *) | ||
| + | lemma pre_es_rev_post: "preOrden (espejo a) = rev (postOrden a)" (is "?P a") | ||
| + | proof (induct a) | ||
| + | fix x | ||
| + | show "?P (H x)" by simp | ||
| + | next | ||
| + | fix x | ||
| + | fix i assume H1: "?P i" | ||
| + | fix d assume H2: "?P d" | ||
| + | have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp | ||
| + | also have "... = [x] @ preOrden (espejo d) @ preOrden (espejo i)" by simp | ||
| + | also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" using H1 H2 by simp | ||
| + | finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp | ||
qed | qed | ||
| Línea 310: | Línea 333: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal dancorgar *) | + | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal |
| − | + | dancorgar josgarsan antsancab1 *) | |
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 320: | Línea 343: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "postOrden (espejo (N x i d)) = postOrden (N x (espejo d) (espejo i))" by simp | + | have "postOrden (espejo (N x i d)) = |
| − | also have "... = (postOrden (espejo d)) @ (postOrden (espejo i)) @ [x]" by simp | + | postOrden (N x (espejo d) (espejo i))" by simp |
| − | also have "... = rev (preOrden d) @ rev (preOrden i) @ [x]" using h1 h2 by simp | + | also have "... = (postOrden (espejo d)) @ (postOrden (espejo i)) @ [x]" |
| − | finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" by simp | + | by simp |
| − | + | also have "... = rev (preOrden d) @ rev (preOrden i) @ [x]" | |
| − | + | using h1 h2 by simp | |
| + | finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" | ||
| + | by simp | ||
| + | (* "?p (N x i d)" más corto *) | ||
qed | qed | ||
| − | (* danrodcha fraortmoy *) | + | (* danrodcha fraortmoy anaprarod *) |
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 340: | Línea 366: | ||
qed | qed | ||
| − | (* pablucoto marpoldia1 jeamacpov paupeddeg rubgonmar *) | + | (* pablucoto marpoldia1 jeamacpov paupeddeg rubgonmar anaprarod *) |
| − | |||
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 350: | Línea 375: | ||
assume H1: "?P i" | assume H1: "?P i" | ||
assume H2: "?P d" | assume H2: "?P d" | ||
| − | have " postOrden (espejo (N x i d)) = postOrden ( N x (espejo d) (espejo i)) " by simp | + | have " postOrden (espejo (N x i d)) = |
| − | also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x] | + | postOrden ( N x (espejo d) (espejo i)) " by simp |
| − | also have "... = rev (preOrden d) @ rev (preOrden i) @ [x] " using H1 H2 by simp | + | also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x]" |
| + | by simp | ||
| + | also have "... = rev (preOrden d) @ rev (preOrden i) @ [x] " | ||
| + | using H1 H2 by simp | ||
also have "... = rev (preOrden d) @ rev (x # preOrden i)" by simp | also have "... = rev (preOrden d) @ rev (x # preOrden i)" by simp | ||
also have "... = rev (x # preOrden i @ preOrden d)" by simp | also have "... = rev (x # preOrden i @ preOrden d)" by simp | ||
| Línea 362: | Línea 390: | ||
lemma "postOrden (espejo a) = rev (preOrden a)" | lemma "postOrden (espejo a) = rev (preOrden a)" | ||
by (induct a) auto | by (induct a) auto | ||
| + | |||
| + | (* anaprarod *) | ||
| + | lemma "postOrden (espejo a) = rev (preOrden a)" | ||
| + | by (induct a) simp_all | ||
(*pabrodmac*) | (*pabrodmac*) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 377: | Línea 408: | ||
show "?P (N x i d)" | show "?P (N x i d)" | ||
proof - | proof - | ||
| − | have "postOrden (espejo (N x i d)) = postOrden(N x (espejo d) (espejo i))" by simp | + | have "postOrden (espejo (N x i d)) = |
| − | also have "… =rev(preOrden d)@rev(preOrden i)@[x]" using h1 h2 by simp | + | postOrden(N x (espejo d) (espejo i))" by simp |
| − | also have "… =rev(preOrden (N x i d))" by simp | + | also have "… = rev (preOrden d) @ rev (preOrden i) @ [x]" |
| + | using h1 h2 by simp | ||
| + | also have "… = rev (preOrden (N x i d))" by simp | ||
finally show ?thesis. | finally show ?thesis. | ||
qed | qed | ||
| Línea 385: | Línea 418: | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| − | |||
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 398: | Línea 430: | ||
have "postOrden (espejo (N x l r)) = | have "postOrden (espejo (N x l r)) = | ||
postOrden (N x (espejo r) (espejo l))" by simp | postOrden (N x (espejo r) (espejo l))" by simp | ||
| − | also have "… = postOrden (espejo r) @ postOrden (espejo l) @ [x]" by simp | + | also have "… = postOrden (espejo r) @ postOrden (espejo l) @ [x]" |
| + | by simp | ||
also have "… = rev (preOrden r) @ rev (preOrden l) @ [x]" | also have "… = rev (preOrden r) @ rev (preOrden l) @ [x]" | ||
| − | + | using H1 H2 by simp | |
also have "… = rev (preOrden l @ preOrden r) @ [x]" by simp | also have "… = rev (preOrden l @ preOrden r) @ [x]" by simp | ||
also have "… = rev ([x] @ preOrden l @ preOrden r)" by simp | also have "… = rev ([x] @ preOrden l @ preOrden r)" by simp | ||
| Línea 407: | Línea 440: | ||
qed | qed | ||
qed | qed | ||
| + | |||
| + | (* antsancab1 *) | ||
| + | (* Después de hacerlo como en la anterior demostración se me ocurrió cómo | ||
| + | relacionar ambas demostraciones. | ||
| + | Como hemos demostrado que | ||
| + | preOrden (espejo a) = rev (postOrden a) | ||
| + | a la inversa también queda demostrado *) | ||
| + | lemma "postOrden (espejo a) = rev (preOrden a)" | ||
| + | apply (induct a) | ||
| + | apply simp | ||
| + | apply (simp add:pre_es_rev_post) | ||
| + | done | ||
text {* | text {* | ||
| Línea 415: | Línea 460: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal dancorgar *) | + | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal |
| − | + | dancorgar josgarsan antsancab1 *) | |
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 425: | Línea 470: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))" by simp | + | have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))" |
| − | also have "... = (inOrden (espejo d)) @ [x] @ (inOrden (espejo i))" by simp | + | by simp |
| − | also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)" using h1 h2 by simp | + | also have "... = (inOrden (espejo d)) @ [x] @ (inOrden (espejo i))" |
| − | finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" by simp | + | by simp |
| + | also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)" | ||
| + | using h1 h2 by simp | ||
| + | finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" | ||
| + | by simp | ||
qed | qed | ||
| − | (* danrodcha *) | + | (* danrodcha anaprarod *) |
theorem "inOrden (espejo a) = rev (inOrden a)" | theorem "inOrden (espejo a) = rev (inOrden a)" | ||
by (induct a) simp_all | by (induct a) simp_all | ||
| − | (* danrodcha *) | + | (* danrodcha anaprarod *) |
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 447: | Línea 496: | ||
qed | qed | ||
| − | (* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13*) | + | (* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *) |
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 456: | Línea 505: | ||
assume HI1: "?P i" | assume HI1: "?P i" | ||
assume HI2: "?P d" | assume HI2: "?P d" | ||
| − | have " inOrden (espejo (N x i d)) = inOrden ( N x (espejo d) (espejo i) )" by simp | + | have "inOrden (espejo (N x i d)) = |
| − | also have "... = inOrden (espejo d) @ [x] @ inOrden (espejo i) " by simp | + | inOrden ( N x (espejo d) (espejo i) )" by simp |
| − | also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)" using HI1 HI2 by simp | + | also have "... = inOrden (espejo d) @ [x] @ inOrden (espejo i)" |
| + | by simp | ||
| + | also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)" | ||
| + | using HI1 HI2 by simp | ||
also have "... = rev (x # inOrden d ) @ rev (inOrden i)" by simp | also have "... = rev (x # inOrden d ) @ rev (inOrden i)" by simp | ||
also have "... = rev ( inOrden i @ x # inOrden d) " by simp | also have "... = rev ( inOrden i @ x # inOrden d) " by simp | ||
| Línea 470: | Línea 522: | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 483: | Línea 534: | ||
show "?P (N x i d)" | show "?P (N x i d)" | ||
proof - | proof - | ||
| − | have "inOrden (espejo (N x i d)) = inOrden(N x (espejo d) (espejo i))" by simp | + | have "inOrden (espejo (N x i d)) = |
| + | inOrden(N x (espejo d) (espejo i))" by simp | ||
also have "… =rev(inOrden d)@[x]@rev(inOrden i)" using h1 h2 by simp | also have "… =rev(inOrden d)@[x]@rev(inOrden i)" using h1 h2 by simp | ||
also have "… =rev(inOrden (N x i d))" by simp | also have "… =rev(inOrden (N x i d))" by simp | ||
| Línea 491: | Línea 543: | ||
(* ferrenseg rubgonmar *) | (* ferrenseg rubgonmar *) | ||
| − | |||
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 497: | Línea 548: | ||
show "?P (H x)" by simp | show "?P (H x)" by simp | ||
next | next | ||
| − | fix x | + | fix x l r |
assume H1: "?P l" | assume H1: "?P l" | ||
assume H2: "?P r" | assume H2: "?P r" | ||
| Línea 504: | Línea 555: | ||
have "inOrden (espejo (N x l r)) = | have "inOrden (espejo (N x l r)) = | ||
inOrden (N x (espejo r) (espejo l))" by simp | inOrden (N x (espejo r) (espejo l))" by simp | ||
| − | also have "… = inOrden (espejo r) @ [x] @ inOrden (espejo l)" by simp | + | also have "… = inOrden (espejo r) @ [x] @ inOrden (espejo l)" |
| + | by simp | ||
also have "… = rev (inOrden r) @ [x] @ rev (inOrden l)" | also have "… = rev (inOrden r) @ [x] @ rev (inOrden l)" | ||
| − | + | using H1 H2 by simp | |
also have "… = rev (inOrden l @ [x] @ inOrden r)" by simp | also have "… = rev (inOrden l @ [x] @ inOrden r)" by simp | ||
also have "… = rev (inOrden (N x l r))" by simp | also have "… = rev (inOrden (N x l r))" by simp | ||
| Línea 522: | Línea 574: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" using h1 h2 by simp | + | show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" |
| + | using h1 h2 by simp | ||
qed | qed | ||
| Línea 536: | Línea 589: | ||
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | ||
migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal | migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal | ||
| − | ferrenseg paupeddeg rubgonmar jeamacpov marcarmor13 fraortmoy *) | + | ferrenseg paupeddeg rubgonmar jeamacpov marcarmor13 fraortmoy |
| + | fracorjim1 josgarsan dancorgar anaprarod antsancab1 *) | ||
fun raiz :: "'a arbol ⇒ 'a" where | fun raiz :: "'a arbol ⇒ 'a" where | ||
| − | "raiz (H x) = x" | + | "raiz (H x) = x" |
| "raiz (N x i d) = x" | | "raiz (N x i d) = x" | ||
| Línea 556: | Línea 610: | ||
migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal | migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal | ||
pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 | pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 | ||
| − | fraortmoy *) | + | fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *) |
fun extremo_izquierda :: "'a arbol ⇒ 'a" where | fun extremo_izquierda :: "'a arbol ⇒ 'a" where | ||
| − | "extremo_izquierda (H x) = x" | + | "extremo_izquierda (H x) = x" |
| "extremo_izquierda (N x i d) = extremo_izquierda i" | | "extremo_izquierda (N x i d) = extremo_izquierda i" | ||
| Línea 565: | Línea 619: | ||
(* bowma *) | (* bowma *) | ||
fun extremo_izquierda_1 :: "'a arbol ⇒ 'a" where | fun extremo_izquierda_1 :: "'a arbol ⇒ 'a" where | ||
| − | "extremo_izquierda_1 (H t) = t" | + | "extremo_izquierda_1 (H t) = t" |
| "extremo_izquierda_1 (N t i d) = hd (inOrden (N t i d))" | | "extremo_izquierda_1 (N t i d) = hd (inOrden (N t i d))" | ||
| Línea 588: | Línea 642: | ||
migtermor marpoldia1 wilmorort lucnovdos juacabsou pabrodmac | migtermor marpoldia1 wilmorort lucnovdos juacabsou pabrodmac | ||
serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 | serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 | ||
| − | fraortmoy | + | fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *) |
fun extremo_derecha :: "'a arbol ⇒ 'a" where | fun extremo_derecha :: "'a arbol ⇒ 'a" where | ||
"extremo_derecha (H x) = x" | "extremo_derecha (H x) = x" | ||
| Línea 604: | Línea 658: | ||
Llamando teorema_12 al teorema del ejercicio 12 *) | Llamando teorema_12 al teorema del ejercicio 12 *) | ||
| + | (* | ||
lemma "extremo_derecha a = extremo_derecha_1 a" | lemma "extremo_derecha a = extremo_derecha_1 a" | ||
by (induct a, simp_all add: aux_ej12_1 teorema_12) | by (induct a, simp_all add: aux_ej12_1 teorema_12) | ||
| + | *) | ||
text {* | text {* | ||
| Línea 614: | Línea 670: | ||
*} | *} | ||
| − | (* danrodcha *) | + | (* danrodcha anaprarod *) |
lemma aux_ej12: "inOrden a ≠ []" | lemma aux_ej12: "inOrden a ≠ []" | ||
apply (induct a) | apply (induct a) | ||
| − | apply simp | + | apply simp (* poniendo simp_all se agrupan estos dos *) |
apply simp | apply simp | ||
done | done | ||
| Línea 640: | Línea 696: | ||
(* ivamenjim *) | (* ivamenjim *) | ||
| − | |||
lemma aux_ej12_1: "inOrden a ≠ []" | lemma aux_ej12_1: "inOrden a ≠ []" | ||
by (induct a) simp_all | by (induct a) simp_all | ||
| − | (* ivamenjim marpoldia1 paupeddeg *) | + | (* ivamenjim marpoldia1 paupeddeg anaprarod antsancab1 *) |
(* Igual que la anterior, pero poniendo solo by simp en el primer have *) | (* Igual que la anterior, pero poniendo solo by simp en el primer have *) | ||
| − | |||
theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 655: | Línea 709: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "last (inOrden (N x i d)) = last ((inOrden i) @ [x] @ (inOrden d))" by simp | + | have "last (inOrden (N x i d)) = |
| + | last ((inOrden i) @ [x] @ (inOrden d))" by simp | ||
also have "... = last (inOrden d)" by (simp add: aux_ej12_1) | also have "... = last (inOrden d)" by (simp add: aux_ej12_1) | ||
also have "... = extremo_derecha d" using h2 by simp | also have "... = extremo_derecha d" using h2 by simp | ||
| − | finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" by simp | + | finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" |
| + | by simp | ||
qed | qed | ||
| Línea 665: | Línea 721: | ||
theorem "last (inOrden a) = extremo_derecha a" (is "?p a") | theorem "last (inOrden a) = extremo_derecha a" (is "?p a") | ||
proof (induct a) | proof (induct a) | ||
| − | fix t | + | fix t |
| − | show "?p (H t)" by simp | + | show "?p (H t)" by simp |
next | next | ||
| − | fix t i d | + | fix t i d |
| − | assume HI: "?p d" | + | assume HI: "?p d" |
| − | have "last (inOrden (N t i d)) = last (inOrden i @ [t] @ inOrden d)" by simp | + | have "last (inOrden (N t i d)) = last (inOrden i @ [t] @ inOrden d)" |
| − | also have "... = last (inOrden d)" by (simp add:aux_ej12) | + | by simp |
| − | also have "... = extremo_derecha d" using HI by simp | + | also have "... = last (inOrden d)" by (simp add:aux_ej12) |
| − | finally show "?p (N t i d)" by simp | + | also have "... = extremo_derecha d" using HI by simp |
| + | finally show "?p (N t i d)" by simp | ||
qed | qed | ||
| Línea 686: | Línea 743: | ||
fix i d ::"'a arbol" | fix i d ::"'a arbol" | ||
assume HI: "last (inOrden d) = extremo_derecha d" | assume HI: "last (inOrden d) = extremo_derecha d" | ||
| − | have "last (inOrden (N x i d)) = last ((inOrden i) @ [x] @ (inOrden d))" by simp | + | have "last (inOrden (N x i d)) = |
| + | last ((inOrden i) @ [x] @ (inOrden d))" by simp | ||
also have "… = last (inOrden d)" by (simp add: aux_ej12) | also have "… = last (inOrden d)" by (simp add: aux_ej12) | ||
also have "… = extremo_derecha d" using HI by simp | also have "… = extremo_derecha d" using HI by simp | ||
also have "… = extremo_derecha (N x i d)" by simp | also have "… = extremo_derecha (N x i d)" by simp | ||
| − | finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" by simp | + | finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" |
| + | by simp | ||
qed | qed | ||
| Línea 696: | Línea 755: | ||
theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| − | + | fix h | |
| − | + | show "?P (H h)" by simp | |
next | next | ||
| − | + | fix n i | |
| − | + | fix d assume HId: "?P d" | |
| − | + | have AUX: "¬ (inOrden d = [])" (is "?Q d") | |
proof (induct d) | proof (induct d) | ||
fix hd | fix hd | ||
| Línea 711: | Línea 770: | ||
show "?Q (N nd id dd)" using HIid HIdd by simp | show "?Q (N nd id dd)" using HIid HIdd by simp | ||
qed | qed | ||
| − | + | have "last (inOrden (N n i d)) = last (inOrden i @[n]@inOrden d)" | |
| − | + | by simp | |
| − | + | also have "… = last (inOrden d)" using AUX by simp | |
| − | + | also have "… = extremo_derecha d" using HId by simp | |
| + | finally show "?P (N n i d)" by simp | ||
qed | qed | ||
(* pabrodmac fraortmoy *) | (* pabrodmac fraortmoy *) | ||
| − | |||
lemma Aux_ej12: "inOrden a ≠ []" | lemma Aux_ej12: "inOrden a ≠ []" | ||
by (induct a) auto | by (induct a) auto | ||
(* pabrodmac fraortmoy *) | (* pabrodmac fraortmoy *) | ||
| − | |||
theorem "last (inOrden a) = extremo_derecha a" | theorem "last (inOrden a) = extremo_derecha a" | ||
by (induct a)(auto simp add: Aux_ej12) | by (induct a)(auto simp add: Aux_ej12) | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 741: | Línea 798: | ||
show "?P (N x i d)" | show "?P (N x i d)" | ||
proof - | proof - | ||
| − | have "last (inOrden (N x i d)) = | + | have "last (inOrden (N x i d)) = last((inOrden i)@ [x] @ (inOrden d))" |
| − | also have "… =last(inOrden d)" by (simp add: Aux_ej12) | + | by simp |
| + | also have "… = last(inOrden d)" by (simp add: Aux_ej12) | ||
also have "… = extremo_derecha d" using h1 h2 by simp | also have "… = extremo_derecha d" using h1 h2 by simp | ||
also have "… = extremo_derecha (N x i d)" by simp | also have "… = extremo_derecha (N x i d)" by simp | ||
finally show ?thesis . | finally show ?thesis . | ||
| − | qed | + | qed |
qed | qed | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| − | |||
theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 770: | Línea 827: | ||
(* fraortmoy *) | (* fraortmoy *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 782: | Línea 838: | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12) | show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12) | ||
| + | qed | ||
| + | |||
| + | (* dancorgar *) | ||
| + | theorem "last (inOrden a) = extremo_derecha a" (is "?P a") | ||
| + | proof (induct a) | ||
| + | fix t | ||
| + | show "?P (H t)" by simp | ||
| + | next | ||
| + | fix t i d | ||
| + | assume H2: "?P d" | ||
| + | have "last (inOrden (N t i d)) = last ((inOrden i)@[t]@(inOrden d))" | ||
| + | by simp | ||
| + | also have "… = last (inOrden d)" | ||
| + | proof (induct d) | ||
| + | fix x | ||
| + | show "last (inOrden i @ [t] @ inOrden (H x)) = last (inOrden (H x))" | ||
| + | by simp | ||
| + | next | ||
| + | fix x1a d1 d2 | ||
| + | show "last (inOrden i @ [t] @ inOrden (N x1a d1 d2)) = | ||
| + | last (inOrden (N x1a d1 d2))" by simp | ||
| + | qed | ||
| + | finally show "last (inOrden (N t i d)) = extremo_derecha (N t i d)" | ||
| + | using H2 by simp | ||
qed | qed | ||
| Línea 791: | Línea 871: | ||
*} | *} | ||
| − | (* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov marcarmor13 *) | + | (* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov |
| + | marcarmor13 *) | ||
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 808: | Línea 889: | ||
qed | qed | ||
| − | (* bowma lucnovdos *) | + | (* bowma lucnovdos dancorgar anaprarod *) |
theorem "hd (inOrden a) = extremo_izquierda a" (is "?p a") | theorem "hd (inOrden a) = extremo_izquierda a" (is "?p a") | ||
proof (induct a) | proof (induct a) | ||
| − | fix t | + | fix t |
| − | show "?p (H t)" by simp | + | show "?p (H t)" by simp |
next | next | ||
| − | fix t i d | + | fix t i d |
| − | assume HI: "?p i" | + | assume HI: "?p i" |
| − | have "hd (inOrden (N t i d)) = hd (inOrden i @ [t] @ inOrden d)" by simp | + | have "hd (inOrden (N t i d)) = hd (inOrden i @ [t] @ inOrden d)" |
| − | also have "… = hd (inOrden i)" by (simp add: aux_ej12) | + | by simp |
| − | also have "… = extremo_izquierda i" using HI by simp | + | also have "… = hd (inOrden i)" by (simp add: aux_ej12) |
| − | finally show "?p (N t i d)" by simp | + | also have "… = extremo_izquierda i" using HI by simp |
| + | finally show "?p (N t i d)" by simp | ||
qed | qed | ||
| Línea 825: | Línea 907: | ||
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| − | + | fix h | |
| − | + | show "?P (H h)" by simp | |
next | next | ||
| − | + | fix n d | |
| − | + | fix i assume HId: "?P i" | |
| − | + | have AUX: "¬ (inOrden i = [])" (is "?Q i") | |
proof (induct i) | proof (induct i) | ||
fix hi | fix hi | ||
| Línea 840: | Línea 922: | ||
show "?Q (N ni ii di)" using HIid HIdd by simp | show "?Q (N ni ii di)" using HIid HIdd by simp | ||
qed | qed | ||
| − | + | have "hd (inOrden (N n i d)) = hd (inOrden i @[n]@inOrden d)" by simp | |
| − | + | also have "… = hd (inOrden i)" using AUX by simp | |
| − | + | also have "… = extremo_izquierda i" using HId by simp | |
| − | + | finally show "?P (N n i d)" by simp | |
qed | qed | ||
| − | (* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar *) | + | (* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar antsancab1 *) |
| − | |||
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 856: | Línea 937: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))" by simp | + | have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))" |
| + | by simp | ||
also have "... = hd (inOrden i)" by (simp add: aux_ej12_1) | also have "... = hd (inOrden i)" by (simp add: aux_ej12_1) | ||
also have "... = extremo_izquierda i" using h1 by simp | also have "... = extremo_izquierda i" using h1 by simp | ||
| − | finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)" by simp | + | finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)" |
| + | by simp | ||
qed | qed | ||
(* pabrodmac paupeddeg*) | (* pabrodmac paupeddeg*) | ||
| − | |||
theorem "hd (inOrden a) = extremo_izquierda a" | theorem "hd (inOrden a) = extremo_izquierda a" | ||
by (induct a)(auto simp add: Aux_ej12) | by (induct a)(auto simp add: Aux_ej12) | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 881: | Línea 962: | ||
show "?P (N x i d)" | show "?P (N x i d)" | ||
proof - | proof - | ||
| − | have "hd (inOrden (N x i d)) = hd((inOrden i)@ [x] @ (inOrden d))" by simp | + | have "hd (inOrden (N x i d)) = hd((inOrden i)@ [x] @ (inOrden d))" |
| + | by simp | ||
also have "… = hd (inOrden i)" by (simp add: Aux_ej12) | also have "… = hd (inOrden i)" by (simp add: Aux_ej12) | ||
also have "… = extremo_izquierda i" using h1 h2 by simp | also have "… = extremo_izquierda i" using h1 h2 by simp | ||
also have "… = extremo_izquierda (N x i d)" by simp | also have "… = extremo_izquierda (N x i d)" by simp | ||
finally show ?thesis . | finally show ?thesis . | ||
| − | qed | + | qed |
qed | qed | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| − | |||
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 902: | Línea 983: | ||
have "hd (inOrden (N x l r)) = | have "hd (inOrden (N x l r)) = | ||
hd (inOrden l @ [x] @ inOrden r)" by simp | hd (inOrden l @ [x] @ inOrden r)" by simp | ||
| − | also have "… = hd (inOrden l)" by (simp add: | + | also have "… = hd (inOrden l)" by (simp add: Aux_ej12) |
also have "… = extremo_izquierda l" using HI by simp | also have "… = extremo_izquierda l" using HI by simp | ||
also have "… = extremo_izquierda (N x l r)" by simp | also have "… = extremo_izquierda (N x l r)" by simp | ||
| Línea 928: | Línea 1009: | ||
*} | *} | ||
| − | (* danrodcha pabrodmac *) | + | (* danrodcha pabrodmac dancorgar anaprarod *) |
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 938: | Línea 1019: | ||
(* danrodcha *) | (* danrodcha *) | ||
| − | theorem "hd ( | + | theorem "hd (preOrden1 a) = last (postOrden a)" (is "?P a") |
proof (induct a) | proof (induct a) | ||
fix x | fix x | ||
| Línea 945: | Línea 1026: | ||
assume HIi: "?P i" | assume HIi: "?P i" | ||
assume HId: "?P d" | assume HId: "?P d" | ||
| − | have "hd ( | + | have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)" |
| − | by (simp only: | + | by (simp only: preOrden1.simps(2)) |
also have "… = x" by simp | also have "… = x" by simp | ||
also have "… = last (postOrden i @ postOrden d @ [x])" by simp | also have "… = last (postOrden i @ postOrden d @ [x])" by simp | ||
| Línea 954: | Línea 1035: | ||
qed | qed | ||
| − | (* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou jeamacpov paupeddeg rubgonmar marcarmor13*) (*Similar al anterior*) | + | (* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou |
| + | jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) | ||
| + | (*Similar al anterior*) | ||
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 963: | Línea 1046: | ||
assume HI1: "?P i" | assume HI1: "?P i" | ||
assume HI2: "?P d" | assume HI2: "?P d" | ||
| − | have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" by simp | + | have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" |
| + | by simp | ||
also have "... = x" by simp | also have "... = x" by simp | ||
also have "... = last ( postOrden i @ postOrden d @ [x]) " by simp | also have "... = last ( postOrden i @ postOrden d @ [x]) " by simp | ||
| Línea 977: | Línea 1061: | ||
next | next | ||
fix n i d | fix n i d | ||
| − | have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = hd ([n]@preOrden i@preOrden d)" | + | have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = |
| − | + | hd ([n]@preOrden i@preOrden d)" by simp | |
| − | (* Si no especifico que i y d son árboles, salta un error de tipo. Supongo que será por | + | (* Si no especifico que i y d son árboles, salta un error de tipo. |
| − | + | Supongo que será por no haber asumido hipótesis sobre ellos *) | |
also have "… = last (postOrden (N n i d))" by simp | also have "… = last (postOrden (N n i d))" by simp | ||
show "?P (N n i d)" by simp | show "?P (N n i d)" by simp | ||
qed | qed | ||
| − | (* ivamenjim serrodcal *) | + | (* ivamenjim serrodcal antsancab1 *) |
| − | |||
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 995: | Línea 1078: | ||
fix i assume h1: "?P i" | fix i assume h1: "?P i" | ||
fix d assume h2: "?P d" | fix d assume h2: "?P d" | ||
| − | have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" by simp | + | have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" |
| + | by simp | ||
also have "... = hd ([x])" by simp | also have "... = hd ([x])" by simp | ||
| − | finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))" by simp | + | finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))" |
| + | by simp | ||
qed | qed | ||
(* pabrodmac paupeddeg fraortmoy *) | (* pabrodmac paupeddeg fraortmoy *) | ||
| − | |||
theorem "hd (preOrden a) = last (postOrden a)" | theorem "hd (preOrden a) = last (postOrden a)" | ||
by (induct a) auto | by (induct a) auto | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 1025: | Línea 1108: | ||
qed | qed | ||
| − | (*Me he dado cuenta que no es necesario asumir ninguna hipótesis de inducción puesto que no es necesario utilizarlas, así que no se si está bien hecho puesto que no se aplicaría inducción *) | + | (* Me he dado cuenta que no es necesario asumir ninguna hipótesis de |
| + | inducción puesto que no es necesario utilizarlas, así que no se si | ||
| + | está bien hecho puesto que no se aplicaría inducción *) | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| − | + | theorem "hd (preOrden a) = last (postOrden a)" (is "?P a") | |
| − | theorem "hd (preOrden a) = last (postOrden a)"(is "?P a") | ||
proof (cases a) | proof (cases a) | ||
fix x | fix x | ||
| Línea 1048: | Línea 1132: | ||
qed | qed | ||
qed | qed | ||
| − | |||
(* fraortmoy *) | (* fraortmoy *) | ||
| Línea 1077: | Línea 1160: | ||
(* danrodcha *) | (* danrodcha *) | ||
| − | theorem "hd ( | + | theorem "hd (preOrden1 a) = raiz a" (is "?P a") |
proof (induct a) | proof (induct a) | ||
fix x | fix x | ||
show "?P (H x)" by simp | show "?P (H x)" by simp | ||
| + | next | ||
fix x i d | fix x i d | ||
assume HIi: "?P i" | assume HIi: "?P i" | ||
assume HId: "?P d" | assume HId: "?P d" | ||
| − | have "hd ( | + | have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)" |
| − | by (simp only: | + | by (simp only: preOrden1.simps(2)) |
also have "… = x" by simp | also have "… = x" by simp | ||
also have "… = raiz (N x i d)" by simp | also have "… = raiz (N x i d)" by simp | ||
| Línea 1091: | Línea 1175: | ||
qed | qed | ||
| − | (* danrodcha pabrodmac *) | + | (* danrodcha pabrodmac dancorgar anaprarod *) |
theorem "hd (preOrden a) = raiz a" (is "?P a") | theorem "hd (preOrden a) = raiz a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 1100: | Línea 1184: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13*) | + | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos |
| + | juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) | ||
theorem "hd (preOrden a) = raiz a" (is "?P a") | theorem "hd (preOrden a) = raiz a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 1109: | Línea 1194: | ||
assume HI1: " ?P i" | assume HI1: " ?P i" | ||
assume HI2: " ?P d" | assume HI2: " ?P d" | ||
| − | have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d) " by simp | + | have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d) " |
| + | by simp | ||
also have "... = x" by simp | also have "... = x" by simp | ||
also have "... = raiz (N x i d)" by simp | also have "... = raiz (N x i d)" by simp | ||
| Línea 1124: | Línea 1210: | ||
fix t i d | fix t i d | ||
assume HI: "?p i" | assume HI: "?p i" | ||
| − | have "hd (preOrden (N t i d)) = hd ([t] @ preOrden i @ preOrden d)" by simp | + | have "hd (preOrden (N t i d)) = hd ([t] @ preOrden i @ preOrden d)" |
| + | by simp | ||
also have "… = t" by simp | also have "… = t" by simp | ||
also have "… = last (postOrden i @ postOrden d @ [t])" by simp | also have "… = last (postOrden i @ postOrden d @ [t])" by simp | ||
| Línea 1138: | Línea 1225: | ||
next | next | ||
fix n i d | fix n i d | ||
| − | have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = hd ([n]@preOrden i@preOrden d)" | + | have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = |
| − | + | hd ([n]@preOrden i@preOrden d)" by simp | |
also have "… = raiz (N n i d)" by simp | also have "… = raiz (N n i d)" by simp | ||
finally show "?P (N n i d)" by simp | finally show "?P (N n i d)" by simp | ||
| Línea 1145: | Línea 1232: | ||
(* ivamenjim: sin usar patrones *) | (* ivamenjim: sin usar patrones *) | ||
| − | |||
theorem "hd (preOrden a) = raiz a" | theorem "hd (preOrden a) = raiz a" | ||
proof (induct a) | proof (induct a) | ||
| Línea 1154: | Línea 1240: | ||
fix i ::"'a arbol" assume h1: "hd (preOrden i) = raiz i" | fix i ::"'a arbol" assume h1: "hd (preOrden i) = raiz i" | ||
fix d ::"'a arbol" assume h2: "hd (preOrden d) = raiz d" | fix d ::"'a arbol" assume h2: "hd (preOrden d) = raiz d" | ||
| − | have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" by simp | + | have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" |
| + | by simp | ||
also have "... = hd ([x])" by simp | also have "... = hd ([x])" by simp | ||
finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp | finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp | ||
| Línea 1160: | Línea 1247: | ||
(* pabrodmac paupeddeg fraortmoy *) | (* pabrodmac paupeddeg fraortmoy *) | ||
| − | |||
theorem "hd (preOrden a) = raiz a" | theorem "hd (preOrden a) = raiz a" | ||
by (induct a) auto | by (induct a) auto | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 1184: | Línea 1269: | ||
qed | qed | ||
| − | (*Me he dado cuenta que no es necesario asumir ninguna hipótesis de inducción puesto que no es necesario utilizarlas, así que no se si está bien hecho puesto que no se aplicaría inducción *) | + | (* Me he dado cuenta que no es necesario asumir ninguna hipótesis de |
| + | inducción puesto que no es necesario utilizarlas, así que no se si | ||
| + | está bien hecho puesto que no se aplicaría inducción *) | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| − | |||
theorem "hd (preOrden a) = raiz a" (is "?P a") | theorem "hd (preOrden a) = raiz a" (is "?P a") | ||
proof (cases a) | proof (cases a) | ||
| Línea 1206: | Línea 1292: | ||
qed | qed | ||
qed | qed | ||
| − | |||
(* fraortmoy *) | (* fraortmoy *) | ||
| Línea 1225: | Línea 1310: | ||
qed | qed | ||
| + | (* antsancab1 *) | ||
| + | theorem "hd (preOrden a) = raiz a" (is "?P a") | ||
| + | proof (induct a) | ||
| + | fix x | ||
| + | show "?P (H x)" by simp | ||
| + | next | ||
| + | fix x | ||
| + | fix i assume H1: "?P i" | ||
| + | fix d assume H2: "?P d" | ||
| + | have "hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" by simp | ||
| + | also have "... = hd [x]" by simp | ||
| + | also have "... = raiz (H x)" by simp | ||
| + | also have "... = raiz (N x i d)" by simp (* estos dos últimos no eran necesarios pero me queda más claro *) | ||
| + | finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp | ||
| + | qed | ||
text {* | text {* | ||
| Línea 1233: | Línea 1333: | ||
*} | *} | ||
| − | (*crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 fraortmoy *) | + | (* crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos |
| + | juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar | ||
| + | marcarmor13 fraortmoy dancorgar anaprarod antsancab1 *) | ||
theorem "hd (inOrden a) = raiz a" | theorem "hd (inOrden a) = raiz a" | ||
quickcheck | quickcheck | ||
oops | oops | ||
| − | (* danrodcha: | + | (* danrodcha anaprarod: |
Auto Quickcheck found a counterexample: | Auto Quickcheck found a counterexample: | ||
| − | a = N | + | a = N a1 (H a2) (H a1) |
Evaluated terms: | Evaluated terms: | ||
| − | hd (inOrden a) = | + | hd (inOrden a) = a2 |
| − | raiz a = | + | raiz a = a1 *) |
(* ivamenjim marpoldia1 *) | (* ivamenjim marpoldia1 *) | ||
| − | |||
theorem "hd (inOrden a) = raiz a" (is "?P a") | theorem "hd (inOrden a) = raiz a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 1258: | Línea 1359: | ||
also have "... = hd (inOrden i)" by (simp add: aux_ej12_1) | also have "... = hd (inOrden i)" by (simp add: aux_ej12_1) | ||
(* Perdemos la x, luego se refuta el enunciado del teorema *) | (* Perdemos la x, luego se refuta el enunciado del teorema *) | ||
| − | + | oops | |
text {* | text {* | ||
| Línea 1267: | Línea 1368: | ||
*} | *} | ||
| − | (* danrodcha pabrodmac*) | + | (* danrodcha pabrodmac dancorgar anaprarod *) |
theorem "last (postOrden a) = raiz a" (is "?P a") | theorem "last (postOrden a) = raiz a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
| Línea 1284: | Línea 1385: | ||
assume HIi: "?P i" | assume HIi: "?P i" | ||
assume HId: "?P d" | assume HId: "?P d" | ||
| − | have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])" | + | have "last (postOrden (N x i d)) = |
| + | last (postOrden i @ postOrden d @ [x])" | ||
by (simp only: postOrden.simps(2)) | by (simp only: postOrden.simps(2)) | ||
also have "… = x" by simp | also have "… = x" by simp | ||
| Línea 1291: | Línea 1393: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 *) (*Similar al anterior*) | + | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos |
| − | + | juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) | |
| + | (* Similar al anterior *) | ||
theorem "last (postOrden a) = raiz a" (is "?P a") | theorem "last (postOrden a) = raiz a" (is "?P a") | ||
proof (induct a ) | proof (induct a ) | ||
| Línea 1301: | Línea 1404: | ||
assume HI1: "?P i" | assume HI1: "?P i" | ||
assume HI2: "?P d" | assume HI2: "?P d" | ||
| − | have "last (postOrden (N x i d)) = last ( postOrden i @ postOrden d @ [x])" by simp | + | have "last (postOrden (N x i d)) = |
| + | last ( postOrden i @ postOrden d @ [x])" by simp | ||
also have "... = x" by simp | also have "... = x" by simp | ||
also have "... = raiz (N x i d) " by simp | also have "... = raiz (N x i d) " by simp | ||
| Línea 1311: | Línea 1415: | ||
theorem "last (postOrden a) = raiz a" (is "?p a") | theorem "last (postOrden a) = raiz a" (is "?p a") | ||
proof (induct a) | proof (induct a) | ||
| − | fix t | + | fix t |
| − | show "?p (H t)" by simp | + | show "?p (H t)" by simp |
next | next | ||
| − | fix t i d | + | fix t i d |
| − | assume "?p i" | + | assume "?p i" |
| − | (* si quito este supuesto, hay error pero no sé dónde se lo está usando *) | + | (* si quito este supuesto, hay error pero no sé dónde se lo está |
| − | have "last (postOrden (N t i d)) = last (postOrden i @ postOrden d @ [t])" by simp | + | usando *) |
| − | also have "... = t" by simp | + | have "last (postOrden (N t i d)) = |
| − | also have "... = raiz (N t i d)" by simp | + | last (postOrden i @ postOrden d @ [t])" by simp |
| − | finally show "?p (N t i d)" by simp | + | also have "... = t" by simp |
| + | also have "... = raiz (N t i d)" by simp | ||
| + | finally show "?p (N t i d)" by simp | ||
qed | qed | ||
| + | (* | ||
| + | Comentario de antsancab1: | ||
| + | No tengo muy claro por qué es, pero si en lugar de utilizar ?p al final lo pones completo: | ||
| + | finally show "last (postOrden (N t i d)) = raiz (N t i d)" by simp | ||
| + | No devuelve ningún error. No se si será que después de ?p espera un único elemento | ||
| + | *) | ||
(* migtermor *) | (* migtermor *) | ||
| Línea 1337: | Línea 1449: | ||
(* ivamenjim: sin usar patrones *) | (* ivamenjim: sin usar patrones *) | ||
| − | |||
theorem "last (postOrden a) = raiz a" | theorem "last (postOrden a) = raiz a" | ||
proof (induct a) | proof (induct a) | ||
| Línea 1346: | Línea 1457: | ||
fix i::"'a arbol" assume h1: "last (postOrden i) = raiz i" | fix i::"'a arbol" assume h1: "last (postOrden i) = raiz i" | ||
fix d::"'a arbol" assume h2: "last (postOrden d) = raiz d" | fix d::"'a arbol" assume h2: "last (postOrden d) = raiz d" | ||
| − | have "last (postOrden (N x i d)) = last ((postOrden i) @ (postOrden d) @ [x])" by simp | + | have "last (postOrden (N x i d)) = |
| + | last ((postOrden i) @ (postOrden d) @ [x])" by simp | ||
also have "... = last ([x])" by simp | also have "... = last ([x])" by simp | ||
finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp | finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp | ||
qed | qed | ||
| − | (*pabrodmac paupeddeg fraortmoy*) | + | (* pabrodmac paupeddeg fraortmoy *) |
| − | |||
theorem "last (postOrden a) = raiz a" | theorem "last (postOrden a) = raiz a" | ||
by (induct a) auto | by (induct a) auto | ||
| − | (*pabrodmac*) | + | (* pabrodmac *) |
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 1376: | Línea 1486: | ||
qed | qed | ||
| − | (*Me he dado cuenta que no es necesario asumir ninguna hipótesis de inducción puesto que no es necesario utilizarlas, así que no se si está bien hecho puesto que no se aplicaría inducción *) | + | (* Me he dado cuenta que no es necesario asumir ninguna hipótesis de |
| + | inducción puesto que no es necesario utilizarlas, así que no se si | ||
| + | está bien hecho puesto que no se aplicaría inducción *) | ||
(* ferrenseg *) | (* ferrenseg *) | ||
| Línea 1416: | Línea 1528: | ||
end | end | ||
| + | |||
| + | (* antsancab1 *) | ||
| + | theorem "last (postOrden a) = raiz a" (is "?P a") | ||
| + | proof (induct a) | ||
| + | fix x | ||
| + | show "?P (H x)" by simp | ||
| + | next | ||
| + | fix x | ||
| + | fix i assume H1: "?P i" | ||
| + | fix d assume H2: "?P d" | ||
| + | have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])" by simp | ||
| + | also have "... = last [x]" by simp | ||
| + | also have "... = x" by simp | ||
| + | also have "... = raiz (H x)" by simp | ||
| + | also have "... = raiz (N x i d)" by simp | ||
| + | finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp | ||
| + | qed | ||
| + | |||
</source> | </source> | ||
Revisión actual del 13:11 16 jul 2018
chapter {* R6: Recorridos de árboles *}
theory R6_Recorridos_de_arboles
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información en los nodos y en las hojas.
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
a d f 3
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
---------------------------------------------------------------------
*}
(* ivamenjim marpoldia1 manmorjim1 bowma migtermor wilmorort
juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg
crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy
dancorgar fracorjim1 anaprarod antsancab1 *)
datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"
value "N e (N c (H a) (H d)) (N g (H f) (H h))"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
preOrden :: "'a arbol ⇒ 'a list"
tal que (preOrden a) es el recorrido pre orden del árbol a. Por
ejemplo,
preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}
(* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor
wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg
marcarmor13 josgarsan dancorgar anaprarod antsancab1 *)
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden (H t) = [t]"
| "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)"
(* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg
rubgonmar paupeddeg fracorjim1 *)
fun preOrden1 :: "'a arbol ⇒ 'a list" where
"preOrden1 (H x) = [x]"
| "preOrden1 (N x i d) = x # preOrden1 i @ preOrden1 d"
value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]"
value "preOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]"
(* danrodcha *)
lemma "preOrden a = preOrden1 a"
by (induct a) simp_all
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
postOrden :: "'a arbol ⇒ 'a list"
tal que (postOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}
(* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1
pablucoto bowma fraortmoy migtermor wilmorort lucnovdos
juacabsou serrodcal pabrodmac ferrenseg jeamacpov
rubgonmar paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden (H t) = [t]"
| "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]"
value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
inOrden :: "'a arbol ⇒ 'a list"
tal que (inOrden a) es el recorrido in orden del árbol a. Por
ejemplo,
inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]
---------------------------------------------------------------------
*}
(* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy
migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac
ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan
dancorgar anaprarod antsancab1 *)
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H t) = [t]"
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)"
(* danrodcha manmorjim1 fracorjim1 *)
fun inOrden1 :: "'a arbol ⇒ 'a list" where
"inOrden1 (H t) = [t]"
| "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d"
value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]"
value "inOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]"
(* manmorjim1 *)
lemma "inOrden t = inOrden1 t"
apply (induct t)
apply auto
done
text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
espejo :: "'a arbol ⇒ 'a arbol"
tal que (espejo a) es la imagen especular del árbol a. Por ejemplo,
espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))
---------------------------------------------------------------------
*}
(* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1
pablucoto bowma fraortmoy migtermor wilmorort lucnovdos
juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar
paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)
fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H t) = H t"
| "espejo (N t i d) = N t (espejo d) (espejo i)"
value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que
preOrden (espejo a) = rev (postOrden a)
---------------------------------------------------------------------
*}
(* ivamenjim migtermor wilmorort juacabsou serrodcal dancorgar josgarsan
*)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))"
by simp
also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)"
using h1 h2 by simp
finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))"
by simp
qed
(* danrodcha paupeddeg anaprarod *)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a) simp_all
(* danrodcha crigomgom fracorjim1 *)
lemma "preOrden1 (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "preOrden1 (espejo (N x i d)) =
preOrden1 (N x (espejo d) (espejo i))"
by (simp only: espejo.simps(2))
also have "… = x#preOrden1 (espejo d) @ preOrden1 (espejo i)"
by (simp only: preOrden1.simps(2))
also have"… = x#rev (postOrden d) @ rev (postOrden i)"
using HIi HId by simp
also have "… = rev (postOrden (N x i d))" by simp
finally show "?P (N x i d)" by simp
qed
(* danrodcha fraortmoy anaprarod *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
show "?P (N x i d)" using HIi HId by simp
qed
(* bowma *)
lemma "preOrden (espejo a) = rev (postOrden a)"
apply (induct a)
apply simp_all
done
(* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume h1: "?P i"
assume h2: "?P d"
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))"
by simp
also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)"
using h1 h2 by simp
also have "... = [x] @ rev (postOrden i @ postOrden d)" by simp
also have "... = rev ( postOrden i @ postOrden d @ [x] ) " by simp
also have "... = rev (postOrden (N x i d)) " by simp
finally show "?P (N x i d)" by simp
qed
(* bowma *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?p a")
proof (induct a)
fix t
show "?p (H t)" by simp
(* Aquí si le diga "preOrden (espejo (H t)) = rev (postOrden (H t))",
isabelle dice:
proof (prove)
goal (1 subgoal):
1. preOrden (espejo (H t)) = rev (postOrden (H t))
Introduced fixed type variable(s): 'b in "t__"
No entiendo porqué *)
next
fix t i d
assume H1: "?p i"
assume H2: "?p d"
have "preOrden (espejo (N t i d)) =
preOrden (N t (espejo d) (espejo i))" by simp
also have "... = [t] @ (preOrden (espejo d)) @ (preOrden (espejo i))"
by simp
also have "... = [t] @ rev (postOrden d) @ rev (postOrden i)"
using H1 H2 by simp
finally show "?p (N t i d)" by simp
qed
(* Comentario sobre tipo inducido. *)
(* fraortmoy lucnovdos pabrodmac*)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a) auto
(*pabrodmac*)
lemma
fixes a ::"'b arbol"
shows "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "preOrden (espejo (N x i d)) =
preOrden(N x (espejo d) (espejo i))" by simp
also have "… = [x]@rev(postOrden d)@rev(postOrden i)"
using h1 h2 by simp
also have "… = rev(postOrden (N x i d))" by simp
finally show ?thesis .
qed
qed
(* ferrenseg rubgonmar *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x l r
assume H1: "?P l"
assume H2: "?P r"
show "?P (N x l r)"
proof -
have "preOrden (espejo (N x l r)) =
preOrden (N x (espejo r) (espejo l))" by simp
also have "… = x # (preOrden (espejo r) @ preOrden (espejo l))" by simp
also have "… = x # (rev (postOrden r) @ rev (postOrden l))"
using H1 H2 by simp
also have "… = x # rev (postOrden l @ postOrden r)" by simp
also have "… = rev ((postOrden l) @ (postOrden r) @ [x])" by simp
also have "… = rev (postOrden (N x l r))" by simp
finally show ?thesis .
qed
qed
(* antsancab1 *)
(* Le he puesto el nombre para utilizarlo en la siguiente demostración *)
lemma pre_es_rev_post: "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp
also have "... = [x] @ preOrden (espejo d) @ preOrden (espejo i)" by simp
also have "... = [x] @ rev (postOrden d) @ rev (postOrden i)" using H1 H2 by simp
finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
dancorgar josgarsan antsancab1 *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "postOrden (espejo (N x i d)) =
postOrden (N x (espejo d) (espejo i))" by simp
also have "... = (postOrden (espejo d)) @ (postOrden (espejo i)) @ [x]"
by simp
also have "... = rev (preOrden d) @ rev (preOrden i) @ [x]"
using h1 h2 by simp
finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))"
by simp
(* "?p (N x i d)" más corto *)
qed
(* danrodcha fraortmoy anaprarod *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
show "?P (N x i d)" using HIi HId by simp
qed
(* pablucoto marpoldia1 jeamacpov paupeddeg rubgonmar anaprarod *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
assume H2: "?P d"
have " postOrden (espejo (N x i d)) =
postOrden ( N x (espejo d) (espejo i)) " by simp
also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x]"
by simp
also have "... = rev (preOrden d) @ rev (preOrden i) @ [x] "
using H1 H2 by simp
also have "... = rev (preOrden d) @ rev (x # preOrden i)" by simp
also have "... = rev (x # preOrden i @ preOrden d)" by simp
also have "... = rev (preOrden (N x i d)) " by simp
finally show "?P (N x i d)" by simp
qed
(* fraortmoy lucnovdos pabrodmac paupeddeg marcarmor13 *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) auto
(* anaprarod *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) simp_all
(*pabrodmac*)
lemma
fixes a ::"'b arbol"
shows "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "postOrden (espejo (N x i d)) =
postOrden(N x (espejo d) (espejo i))" by simp
also have "… = rev (preOrden d) @ rev (preOrden i) @ [x]"
using h1 h2 by simp
also have "… = rev (preOrden (N x i d))" by simp
finally show ?thesis.
qed
qed
(* ferrenseg *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x l r
assume H1: "?P l"
assume H2: "?P r"
show "?P (N x l r)"
proof -
have "postOrden (espejo (N x l r)) =
postOrden (N x (espejo r) (espejo l))" by simp
also have "… = postOrden (espejo r) @ postOrden (espejo l) @ [x]"
by simp
also have "… = rev (preOrden r) @ rev (preOrden l) @ [x]"
using H1 H2 by simp
also have "… = rev (preOrden l @ preOrden r) @ [x]" by simp
also have "… = rev ([x] @ preOrden l @ preOrden r)" by simp
also have "… = rev (preOrden (N x l r))" by simp
finally show ?thesis .
qed
qed
(* antsancab1 *)
(* Después de hacerlo como en la anterior demostración se me ocurrió cómo
relacionar ambas demostraciones.
Como hemos demostrado que
preOrden (espejo a) = rev (postOrden a)
a la inversa también queda demostrado *)
lemma "postOrden (espejo a) = rev (preOrden a)"
apply (induct a)
apply simp
apply (simp add:pre_es_rev_post)
done
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
dancorgar josgarsan antsancab1 *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))"
by simp
also have "... = (inOrden (espejo d)) @ [x] @ (inOrden (espejo i))"
by simp
also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)"
using h1 h2 by simp
finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))"
by simp
qed
(* danrodcha anaprarod *)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) simp_all
(* danrodcha anaprarod *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
show "?P (N x i d)" using HIi HId by simp
qed
(* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x) " by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
have "inOrden (espejo (N x i d)) =
inOrden ( N x (espejo d) (espejo i) )" by simp
also have "... = inOrden (espejo d) @ [x] @ inOrden (espejo i)"
by simp
also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)"
using HI1 HI2 by simp
also have "... = rev (x # inOrden d ) @ rev (inOrden i)" by simp
also have "... = rev ( inOrden i @ x # inOrden d) " by simp
also have "... = rev (inOrden (N x i d))" by simp
finally show "?P (N x i d)" by simp
qed
(* lucnovdos pabrodmac paupeddeg fraortmoy *)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "inOrden (espejo (N x i d)) =
inOrden(N x (espejo d) (espejo i))" by simp
also have "… =rev(inOrden d)@[x]@rev(inOrden i)" using h1 h2 by simp
also have "… =rev(inOrden (N x i d))" by simp
finally show ?thesis .
qed
qed
(* ferrenseg rubgonmar *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x l r
assume H1: "?P l"
assume H2: "?P r"
show "?P (N x l r)"
proof -
have "inOrden (espejo (N x l r)) =
inOrden (N x (espejo r) (espejo l))" by simp
also have "… = inOrden (espejo r) @ [x] @ inOrden (espejo l)"
by simp
also have "… = rev (inOrden r) @ [x] @ rev (inOrden l)"
using H1 H2 by simp
also have "… = rev (inOrden l @ [x] @ inOrden r)" by simp
also have "… = rev (inOrden (N x l r))" by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))"
using h1 h2 by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
raiz :: "'a arbol ⇒ 'a"
tal que (raiz a) es la raiz del árbol a. Por ejemplo,
raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
---------------------------------------------------------------------
*}
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto
migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal
ferrenseg paupeddeg rubgonmar jeamacpov marcarmor13 fraortmoy
fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
| "raiz (N x i d) = x"
value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e"
text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
extremo_izquierda :: "'a arbol ⇒ 'a"
tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
a. Por ejemplo,
extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
---------------------------------------------------------------------
*}
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto
migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal
pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x"
| "extremo_izquierda (N x i d) = extremo_izquierda i"
value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a"
(* bowma *)
fun extremo_izquierda_1 :: "'a arbol ⇒ 'a" where
"extremo_izquierda_1 (H t) = t"
| "extremo_izquierda_1 (N t i d) = hd (inOrden (N t i d))"
(* ivamenjim *)
(* Metaejercicio de demostración.
Llamando teorema_13 al teorema del ejercicio 13 *)
lemma "extremo_izquierda a = extremo_izquierda_1 a"
by (induct a, simp_all add: aux_ej12_1 teorema_13)
text {*
---------------------------------------------------------------------
Ejercicio 11. Definir la función
extremo_derecha :: "'a arbol ⇒ 'a"
tal que (extremo_derecha a) es el nodo más a la derecha del árbol
a. Por ejemplo,
extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
---------------------------------------------------------------------
*}
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto
migtermor marpoldia1 wilmorort lucnovdos juacabsou pabrodmac
serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x"
| "extremo_derecha (N x i d) = extremo_derecha d"
value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h"
(* bowma *)
fun extremo_derecha_1 :: "'a arbol ⇒ 'a" where
"extremo_derecha_1 (H t) = t"
| "extremo_derecha_1 (N t i d) = last (inOrden (N t i d))"
(* ivamenjim *)
(* Metaejercicio de demostración.
Llamando teorema_12 al teorema del ejercicio 12 *)
(*
lemma "extremo_derecha a = extremo_derecha_1 a"
by (induct a, simp_all add: aux_ej12_1 teorema_12)
*)
text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
last (inOrden a) = extremo_derecha a
---------------------------------------------------------------------
*}
(* danrodcha anaprarod *)
lemma aux_ej12: "inOrden a ≠ []"
apply (induct a)
apply simp (* poniendo simp_all se agrupan estos dos *)
apply simp
done
(* danrodcha pablucoto crigomgom wilmorort juacabsou serrodcal
rubgonmar jeamacpov marcarmor13*)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "last (inOrden (N x i d)) = last (inOrden i @ [x] @ inOrden d)"
by (simp only: inOrden.simps(2))
also have "… = last (inOrden d)" by (simp add: aux_ej12)
also have "… = extremo_derecha d" using HId by simp
also have "… = extremo_derecha (N x i d)" by simp
finally show "?P (N x i d)" by simp
qed
(* ivamenjim *)
lemma aux_ej12_1: "inOrden a ≠ []"
by (induct a) simp_all
(* ivamenjim marpoldia1 paupeddeg anaprarod antsancab1 *)
(* Igual que la anterior, pero poniendo solo by simp en el primer have *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "last (inOrden (N x i d)) =
last ((inOrden i) @ [x] @ (inOrden d))" by simp
also have "... = last (inOrden d)" by (simp add: aux_ej12_1)
also have "... = extremo_derecha d" using h2 by simp
finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)"
by simp
qed
(* bowma *)
(* Casi lo mismo que el anterior,pero no hace falta suponer "?p i" *)
theorem "last (inOrden a) = extremo_derecha a" (is "?p a")
proof (induct a)
fix t
show "?p (H t)" by simp
next
fix t i d
assume HI: "?p d"
have "last (inOrden (N t i d)) = last (inOrden i @ [t] @ inOrden d)"
by simp
also have "... = last (inOrden d)" by (simp add:aux_ej12)
also have "... = extremo_derecha d" using HI by simp
finally show "?p (N t i d)" by simp
qed
(* lucnovdos*)
(* El mismo que el anterior,pero sin usar patrones *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
fix x ::"'a"
show "last (inOrden (H x)) = extremo_derecha (H x)" by simp
next
fix x ::"'a"
fix i d ::"'a arbol"
assume HI: "last (inOrden d) = extremo_derecha d"
have "last (inOrden (N x i d)) =
last ((inOrden i) @ [x] @ (inOrden d))" by simp
also have "… = last (inOrden d)" by (simp add: aux_ej12)
also have "… = extremo_derecha d" using HI by simp
also have "… = extremo_derecha (N x i d)" by simp
finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)"
by simp
qed
(* migtermor *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix h
show "?P (H h)" by simp
next
fix n i
fix d assume HId: "?P d"
have AUX: "¬ (inOrden d = [])" (is "?Q d")
proof (induct d)
fix hd
show "?Q (H hd)" by simp
next
fix nd
fix id assume HIid: "?Q id"
fix dd assume HIdd: "?Q dd"
show "?Q (N nd id dd)" using HIid HIdd by simp
qed
have "last (inOrden (N n i d)) = last (inOrden i @[n]@inOrden d)"
by simp
also have "… = last (inOrden d)" using AUX by simp
also have "… = extremo_derecha d" using HId by simp
finally show "?P (N n i d)" by simp
qed
(* pabrodmac fraortmoy *)
lemma Aux_ej12: "inOrden a ≠ []"
by (induct a) auto
(* pabrodmac fraortmoy *)
theorem "last (inOrden a) = extremo_derecha a"
by (induct a)(auto simp add: Aux_ej12)
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "last (inOrden (N x i d)) = last((inOrden i)@ [x] @ (inOrden d))"
by simp
also have "… = last(inOrden d)" by (simp add: Aux_ej12)
also have "… = extremo_derecha d" using h1 h2 by simp
also have "… = extremo_derecha (N x i d)" by simp
finally show ?thesis .
qed
qed
(* ferrenseg *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x l r
assume HI: "?P r"
show "?P (N x l r)"
proof -
have "last (inOrden (N x l r)) =
last (inOrden r @ [x] @ inOrden r)" by simp
also have "… = last (inOrden r)" by (simp add: inOrden)
also have "… = extremo_derecha r" using HI by simp
also have "… = extremo_derecha (N x l r)" by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
lemma
fixes a ::"'b arbol"
shows "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12)
qed
(* dancorgar *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix t
show "?P (H t)" by simp
next
fix t i d
assume H2: "?P d"
have "last (inOrden (N t i d)) = last ((inOrden i)@[t]@(inOrden d))"
by simp
also have "… = last (inOrden d)"
proof (induct d)
fix x
show "last (inOrden i @ [t] @ inOrden (H x)) = last (inOrden (H x))"
by simp
next
fix x1a d1 d2
show "last (inOrden i @ [t] @ inOrden (N x1a d1 d2)) =
last (inOrden (N x1a d1 d2))" by simp
qed
finally show "last (inOrden (N t i d)) = extremo_derecha (N t i d)"
using H2 by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}
(* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov
marcarmor13 *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "hd (inOrden (N x i d)) = hd (inOrden i @ [x] @ inOrden d)"
by (simp only: inOrden.simps(2))
also have "… = hd (inOrden i)" by (simp add: aux_ej12)
also have "… = extremo_izquierda i" using HIi by simp
also have "… = extremo_izquierda (N x i d)" by simp
finally show "?P (N x i d)" by simp
qed
(* bowma lucnovdos dancorgar anaprarod *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?p a")
proof (induct a)
fix t
show "?p (H t)" by simp
next
fix t i d
assume HI: "?p i"
have "hd (inOrden (N t i d)) = hd (inOrden i @ [t] @ inOrden d)"
by simp
also have "… = hd (inOrden i)" by (simp add: aux_ej12)
also have "… = extremo_izquierda i" using HI by simp
finally show "?p (N t i d)" by simp
qed
(* migtermor *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix h
show "?P (H h)" by simp
next
fix n d
fix i assume HId: "?P i"
have AUX: "¬ (inOrden i = [])" (is "?Q i")
proof (induct i)
fix hi
show "?Q (H hi)" by simp
next
fix ni
fix ii assume HIid: "?Q ii"
fix di assume HIdd: "?Q di"
show "?Q (N ni ii di)" using HIid HIdd by simp
qed
have "hd (inOrden (N n i d)) = hd (inOrden i @[n]@inOrden d)" by simp
also have "… = hd (inOrden i)" using AUX by simp
also have "… = extremo_izquierda i" using HId by simp
finally show "?P (N n i d)" by simp
qed
(* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar antsancab1 *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))"
by simp
also have "... = hd (inOrden i)" by (simp add: aux_ej12_1)
also have "... = extremo_izquierda i" using h1 by simp
finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)"
by simp
qed
(* pabrodmac paupeddeg*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a)(auto simp add: Aux_ej12)
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "hd (inOrden (N x i d)) = hd((inOrden i)@ [x] @ (inOrden d))"
by simp
also have "… = hd (inOrden i)" by (simp add: Aux_ej12)
also have "… = extremo_izquierda i" using h1 h2 by simp
also have "… = extremo_izquierda (N x i d)" by simp
finally show ?thesis .
qed
qed
(* ferrenseg *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x l r
assume HI: "?P l"
show "?P (N x l r)"
proof -
have "hd (inOrden (N x l r)) =
hd (inOrden l @ [x] @ inOrden r)" by simp
also have "… = hd (inOrden l)" by (simp add: Aux_ej12)
also have "… = extremo_izquierda l" using HI by simp
also have "… = extremo_izquierda (N x l r)" by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume h1: "?P i"
assume h2: "?P d"
show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12)
qed
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}
(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
show "?P (N x i d)" by simp
qed
(* danrodcha *)
theorem "hd (preOrden1 a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
by (simp only: preOrden1.simps(2))
also have "… = x" by simp
also have "… = last (postOrden i @ postOrden d @ [x])" by simp
also have "… = last (postOrden (N x i d))"
by (simp only: postOrden.simps(2))
finally show "?P (N x i d)" by simp
qed
(* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou
jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *)
(*Similar al anterior*)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)"
by simp
also have "... = x" by simp
also have "... = last ( postOrden i @ postOrden d @ [x]) " by simp
also have "... = last ( postOrden (N x i d) )" by simp
finally show "?P (N x i d)" by simp
qed
(* migtermor *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix h
show "?P (H h)" by simp
next
fix n i d
have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) =
hd ([n]@preOrden i@preOrden d)" by simp
(* Si no especifico que i y d son árboles, salta un error de tipo.
Supongo que será por no haber asumido hipótesis sobre ellos *)
also have "… = last (postOrden (N n i d))" by simp
show "?P (N n i d)" by simp
qed
(* ivamenjim serrodcal antsancab1 *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))"
by simp
also have "... = hd ([x])" by simp
finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))"
by simp
qed
(* pabrodmac paupeddeg fraortmoy *)
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a) auto
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "hd (preOrden (N x i d) )= x" by simp
also have "… = last (postOrden (N x i d))" by simp
finally show ?thesis .
qed
qed
(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
inducción puesto que no es necesario utilizarlas, así que no se si
está bien hecho puesto que no se aplicaría inducción *)
(* ferrenseg *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (cases a)
fix x
assume "a = H x"
then show "?P a" by simp
next
fix x l r
assume H: "a = N x l r"
show "?P a"
proof -
have "hd (preOrden a) = hd (preOrden (N x l r))" using H by simp
also have "… = hd (x # (preOrden l @ preOrden r))" by simp
also have "… = x" by simp
also have "… = last (postOrden l @ postOrden r @ [x])" by simp
also have "… = last (postOrden (N x l r))" by simp
also have "… = last (postOrden a)" using H by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
theorem "hd (preOrden a) = last (postOrden a)"
apply (induct a)
apply simp
apply simp
done
(* fraortmoy *)
(* como ya se ha comentado antes, no se usan hipótesis de inducción *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}
(* danrodcha *)
theorem "hd (preOrden1 a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
by (simp only: preOrden1.simps(2))
also have "… = x" by simp
also have "… = raiz (N x i d)" by simp
finally show "?P (N x i d)" by simp
qed
(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
show "?P (N x i d)" by simp
qed
(* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos
juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: " ?P i"
assume HI2: " ?P d"
have " hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d) "
by simp
also have "... = x" by simp
also have "... = raiz (N x i d)" by simp
finally show " ?P (N x i d)" by simp
qed
(* bowma *)
(* similar al anterior pero sin suponer "?p d" *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?p a")
proof (induct a)
fix t
show "?p (H t)" by simp
next
fix t i d
assume HI: "?p i"
have "hd (preOrden (N t i d)) = hd ([t] @ preOrden i @ preOrden d)"
by simp
also have "… = t" by simp
also have "… = last (postOrden i @ postOrden d @ [t])" by simp
also have "… = last (postOrden (N t i d))" by simp
finally show "?p (N t i d)" by simp
qed
(* migtermor *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix h
show "?P (H h)" by simp
next
fix n i d
have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) =
hd ([n]@preOrden i@preOrden d)" by simp
also have "… = raiz (N n i d)" by simp
finally show "?P (N n i d)" by simp
qed
(* ivamenjim: sin usar patrones *)
theorem "hd (preOrden a) = raiz a"
proof (induct a)
fix x ::"'a"
show "hd (preOrden (H x)) = raiz (H x)" by simp
next
fix x ::"'a"
fix i ::"'a arbol" assume h1: "hd (preOrden i) = raiz i"
fix d ::"'a arbol" assume h2: "hd (preOrden d) = raiz d"
have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))"
by simp
also have "... = hd ([x])" by simp
finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed
(* pabrodmac paupeddeg fraortmoy *)
theorem "hd (preOrden a) = raiz a"
by (induct a) auto
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "hd (preOrden (N x i d) )= x" by simp
also have "… = raiz (N x i d)" by simp
finally show ?thesis .
qed
qed
(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
inducción puesto que no es necesario utilizarlas, así que no se si
está bien hecho puesto que no se aplicaría inducción *)
(* ferrenseg *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (cases a)
fix x
assume "a = H x"
then show "?P a" by simp
next
fix x l r
assume H: "a = N x l r"
show "?P a"
proof -
have "hd (preOrden a) = hd (preOrden (N x l r))" using H by simp
also have "… = hd (x#(preOrden l @ preOrden r))" by simp
also have "… = x" by simp
also have "… = raiz (N x l r)" by simp
also have "… = raiz a" using H by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
theorem "hd (preOrden a) = raiz a"
apply (induct a)
apply simp
apply simp
done
(* fraortmoy *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed
(* antsancab1 *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" by simp
also have "... = hd [x]" by simp
also have "... = raiz (H x)" by simp
also have "... = raiz (N x i d)" by simp (* estos dos últimos no eran necesarios pero me queda más claro *)
finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}
(* crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos
juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar
marcarmor13 fraortmoy dancorgar anaprarod antsancab1 *)
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(* danrodcha anaprarod:
Auto Quickcheck found a counterexample:
a = N a1 (H a2) (H a1)
Evaluated terms:
hd (inOrden a) = a2
raiz a = a1 *)
(* ivamenjim marpoldia1 *)
theorem "hd (inOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))" by simp
also have "... = hd (inOrden i)" by (simp add: aux_ej12_1)
(* Perdemos la x, luego se refuta el enunciado del teorema *)
oops
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}
(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
show "?P (N x i d)" by simp
qed
(* danrodcha *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
assume HIi: "?P i"
assume HId: "?P d"
have "last (postOrden (N x i d)) =
last (postOrden i @ postOrden d @ [x])"
by (simp only: postOrden.simps(2))
also have "… = x" by simp
also have "… = raiz (N x i d)" by (simp only: raiz.simps(2))
finally show "?P (N x i d)" by simp
qed
(* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos
juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *)
(* Similar al anterior *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a )
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
have "last (postOrden (N x i d)) =
last ( postOrden i @ postOrden d @ [x])" by simp
also have "... = x" by simp
also have "... = raiz (N x i d) " by simp
finally show " ?P (N x i d)" by simp
qed
(* bowma *)
(* También sin usar el supuesto "?p d" *)
theorem "last (postOrden a) = raiz a" (is "?p a")
proof (induct a)
fix t
show "?p (H t)" by simp
next
fix t i d
assume "?p i"
(* si quito este supuesto, hay error pero no sé dónde se lo está
usando *)
have "last (postOrden (N t i d)) =
last (postOrden i @ postOrden d @ [t])" by simp
also have "... = t" by simp
also have "... = raiz (N t i d)" by simp
finally show "?p (N t i d)" by simp
qed
(*
Comentario de antsancab1:
No tengo muy claro por qué es, pero si en lugar de utilizar ?p al final lo pones completo:
finally show "last (postOrden (N t i d)) = raiz (N t i d)" by simp
No devuelve ningún error. No se si será que después de ?p espera un único elemento
*)
(* migtermor *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix h
show "?P (H h)" by simp
next
fix n i d
have "last (postOrden (N n (i :: 'a arbol) (d :: 'a arbol))) =
last (postOrden i@postOrden d@[n])" by simp
also have "… = raiz (N n i d)" by simp
finally show "?P (N n i d)" by simp
qed
(* ivamenjim: sin usar patrones *)
theorem "last (postOrden a) = raiz a"
proof (induct a)
fix x::"'a"
show "last (postOrden (H x)) = raiz (H x)" by simp
next
fix x::"'a"
fix i::"'a arbol" assume h1: "last (postOrden i) = raiz i"
fix d::"'a arbol" assume h2: "last (postOrden d) = raiz d"
have "last (postOrden (N x i d)) =
last ((postOrden i) @ (postOrden d) @ [x])" by simp
also have "... = last ([x])" by simp
finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed
(* pabrodmac paupeddeg fraortmoy *)
theorem "last (postOrden a) = raiz a"
by (induct a) auto
(* pabrodmac *)
lemma
fixes a ::"'b arbol"
shows "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "last (postOrden (N x i d))= x" by simp
also have "… = raiz (N x i d)" by simp
finally show ?thesis .
qed
qed
(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
inducción puesto que no es necesario utilizarlas, así que no se si
está bien hecho puesto que no se aplicaría inducción *)
(* ferrenseg *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (cases a)
fix x
assume "a = H x"
then show "?P a" by simp
next
fix x l r
assume H: "a = N x l r"
show "?P a"
proof -
have "last (postOrden a) = last (postOrden (N x l r))" using H by simp
also have "… = last (postOrden l @ preOrden r @ [x])" by simp
also have "… = x" by simp
also have "… = raiz a" using H by simp
finally show ?thesis .
qed
qed
(* fraortmoy *)
theorem "last (postOrden a) = raiz a"
apply (induct a)
apply simp
apply simp
done
(* fraortmoy *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed
end
(* antsancab1 *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])" by simp
also have "... = last [x]" by simp
also have "... = x" by simp
also have "... = raiz (H x)" by simp
also have "... = raiz (N x i d)" by simp
finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed