Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
m |
m (Texto reemplazado: «isar» por «isabelle») |
||
| (No se muestran 49 ediciones intermedias de 10 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*) | + | 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*) | + | 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 73: | Línea 75: | ||
*} | *} | ||
| − | (* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar paupeddeg *) | + | (* 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 | 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 93: | Línea 98: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar paupeddeg*) | + | (* 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 | 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 126: | Línea 132: | ||
*} | *} | ||
| − | (* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar paupeddeg *) | + | (* 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 | 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 143: | 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 153: | 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 173: | 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 183: | 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 201: | Línea 213: | ||
done | done | ||
| − | (* pablucoto marpoldia1 jeamacpov paupeddeg*) | + | (* 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 211: | 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 223: | 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 260: | 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 290: | 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 299: | 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 309: | 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 329: | 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 339: | 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 348: | Línea 387: | ||
qed | qed | ||
| − | (* fraortmoy lucnovdos pabrodmac paupeddeg *) | + | (* fraortmoy lucnovdos pabrodmac paupeddeg marcarmor13 *) |
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 366: | 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 374: | 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 387: | 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 396: | 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 404: | 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 414: | 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 436: | Línea 496: | ||
qed | qed | ||
| − | (* pablucoto marpoldia1 jeamacpov paupeddeg *) | + | (* 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 445: | 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 454: | 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 472: | 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 480: | 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 486: | 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 493: | 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 511: | Línea 587: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal ferrenseg paupeddeg rubgonmar *) | + | (* 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 | 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 528: | Línea 607: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar *) | + | (* 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 | 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 537: | 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))" | ||
(* ivamenjim *) | (* ivamenjim *) | ||
| − | (* Metaejercicio de demostración. Llamando teorema_13 al teorema del ejercicio 13 *) | + | (* Metaejercicio de demostración. |
| + | Llamando teorema_13 al teorema del ejercicio 13 *) | ||
lemma "extremo_izquierda a = extremo_izquierda_1 a" | lemma "extremo_izquierda a = extremo_izquierda_1 a" | ||
| Línea 556: | Línea 639: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar *) | + | (* 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 | fun extremo_derecha :: "'a arbol ⇒ 'a" where | ||
"extremo_derecha (H x) = x" | "extremo_derecha (H x) = x" | ||
| Línea 569: | Línea 655: | ||
(* ivamenjim *) | (* ivamenjim *) | ||
| − | (* Metaejercicio de demostración. Llamando teorema_12 al teorema del ejercicio 12 *) | + | (* Metaejercicio de demostración. |
| + | 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 581: | 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 | ||
| − | (* danrodcha pablucoto crigomgom wilmorort juacabsou serrodcal rubgonmar *) | + | (* danrodcha pablucoto crigomgom wilmorort juacabsou serrodcal |
| + | rubgonmar jeamacpov marcarmor13*) | ||
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 606: | 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 621: | 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 631: | 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 652: | 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 662: | 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 677: | 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 707: | 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 733: | 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 742: | Línea 871: | ||
*} | *} | ||
| − | (* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov*) | + | (* 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 759: | 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 776: | 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 791: | 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 807: | 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 832: | 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 853: | 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 860: | 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 868: | 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 878: | 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 885: | 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 894: | Línea 1035: | ||
qed | qed | ||
| − | (* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou jeamacpov paupeddeg rubgonmar *) (*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 903: | 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 917: | 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 935: | 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 965: | 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 988: | 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 997: | 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 1011: | 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 1020: | Línea 1184: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou serrodcal jeamacpov paupeddeg rubgonmar *) | + | (* 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 1029: | 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 1044: | 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 1058: | 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 1065: | 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 1074: | 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 1104: | 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 1126: | 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 1134: | Línea 1333: | ||
*} | *} | ||
| − | (*crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar *) | + | (* 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 1159: | 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 1168: | 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 1185: | 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 1192: | Línea 1393: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou serrodcal jeamacpov paupeddeg rubgonmar *) (*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 1202: | 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 1212: | 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 1238: | 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 1247: | 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 1277: | 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 1298: | 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