Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle») |
|||
| (No se muestran 46 ediciones intermedias de 7 usuarios) | |||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
chapter {* R6: Recorridos de árboles *} | chapter {* R6: Recorridos de árboles *} | ||
| Línea 23: | Línea 23: | ||
(* ivamenjim marpoldia1 manmorjim1 bowma migtermor wilmorort | (* ivamenjim marpoldia1 manmorjim1 bowma migtermor wilmorort | ||
juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg | juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg | ||
| − | crigomgom danrodcha jeamacpov marcarmor13 *) | + | crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy |
| + | 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 41: | Línea 42: | ||
(* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor | (* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor | ||
| − | wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg marcarmor13*) | + | 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)" | ||
(* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg | (* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg | ||
| − | rubgonmar paupeddeg *) | + | 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 76: | 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*) | + | 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 98: | Línea 100: | ||
(* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy | (* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy | ||
migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac | migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac | ||
| − | ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13*) | + | ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan |
| − | + | 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 134: | 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*) | + | 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 151: | Línea 150: | ||
*} | *} | ||
| − | (* ivamenjim migtermor wilmorort juacabsou serrodcal *) | + | (* 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 161: | 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 181: | 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 191: | 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 209: | 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 219: | 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 231: | 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 268: | 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 298: | 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 307: | Línea 333: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal *) | + | (* 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 317: | 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 337: | 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 347: | 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 359: | 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 374: | 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 382: | 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 395: | 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 404: | 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 412: | Línea 460: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal *) | + | (* 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 422: | 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 444: | 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 453: | 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 462: | Línea 517: | ||
qed | qed | ||
| − | (* lucnovdos pabrodmac paupeddeg *) | + | (* lucnovdos pabrodmac paupeddeg fraortmoy *) |
theorem "inOrden (espejo a) = rev (inOrden a)" | theorem "inOrden (espejo a) = rev (inOrden a)" | ||
by (induct a) auto | by (induct a) auto | ||
(* pabrodmac *) | (* pabrodmac *) | ||
| − | |||
lemma | lemma | ||
fixes a ::"'b arbol" | fixes a ::"'b arbol" | ||
| Línea 480: | 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 488: | 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 494: | 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 501: | 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 | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | 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 | qed | ||
| Línea 521: | 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*) | + | 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 540: | Línea 609: | ||
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | ||
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 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 549: | 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 571: | Línea 641: | ||
(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto | ||
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 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 587: | 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 597: | 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 623: | 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 638: | 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 648: | 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 669: | 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 679: | 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 694: | 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 *) | + | (* pabrodmac fraortmoy *) |
| − | |||
lemma Aux_ej12: "inOrden a ≠ []" | lemma Aux_ej12: "inOrden a ≠ []" | ||
by (induct a) auto | by (induct a) auto | ||
| − | (* pabrodmac *) | + | (* 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 724: | 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 750: | Línea 824: | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | 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 | qed | ||
| Línea 759: | 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 776: | 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 793: | 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 808: | 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 824: | 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 849: | 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 870: | 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 877: | Línea 990: | ||
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 {* | text {* | ||
| Línea 885: | 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 895: | 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 902: | 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 911: | 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 920: | 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 934: | 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 952: | 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 *) | + | (* 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 982: | 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 1005: | Línea 1132: | ||
qed | qed | ||
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 {* | text {* | ||
| Línea 1014: | 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 1028: | 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 1037: | 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 1046: | 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 1061: | 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 1075: | 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 1082: | 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 1091: | 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 | ||
qed | qed | ||
| − | (* pabrodmac paupeddeg *) | + | (* 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 1121: | 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 1143: | Línea 1292: | ||
qed | qed | ||
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 {* | text {* | ||
| Línea 1151: | Línea 1333: | ||
*} | *} | ||
| − | (*crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13 *) | + | (* 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 1176: | 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 1185: | 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 1202: | 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 1209: | 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 1219: | 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 1229: | 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 1255: | 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 1264: | 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*) | + | (* 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 1294: | 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 1315: | Línea 1509: | ||
qed | qed | ||
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 | 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