Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle») |
|||
| (No se muestran 92 ediciones intermedias de 16 usuarios) | |||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
chapter {* R6: Recorridos de árboles *} | chapter {* R6: Recorridos de árboles *} | ||
| Línea 21: | Línea 21: | ||
*} | *} | ||
| − | (* ivamenjim marpoldia1 manmorjim1 bowma migtermor wilmorort juacabsou serrodcal pabrodmac*) | + | (* 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" | datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol" | ||
| Línea 38: | Línea 41: | ||
*} | *} | ||
| − | (* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos serrodcal pabrodmac *) | + | (* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor |
| + | 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 *) | + | (* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg |
| + | 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 69: | Línea 75: | ||
*} | *} | ||
| − | (* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac *) | + | (* 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 89: | Línea 98: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac *) | + | (* 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 122: | Línea 132: | ||
*} | *} | ||
| − | (* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1 pablucoto bowma fraortmoy migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac *) | + | (* 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 139: | 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 149: | 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 *) | + | (* 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 169: | 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 179: | 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 197: | Línea 213: | ||
done | done | ||
| − | (* pablucoto marpoldia1*) | + | (* 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 207: | 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 219: | 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 256: | 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 | ||
| + | |||
| + | (* 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 | qed | ||
| Línea 270: | 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 280: | 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 300: | Línea 366: | ||
qed | qed | ||
| − | (* pablucoto marpoldia1*) | + | (* 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 310: | 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 319: | Línea 387: | ||
qed | qed | ||
| − | (* fraortmoy lucnovdos pabrodmac*) | + | (* 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 337: | 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 | ||
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 {* | text {* | ||
| Línea 351: | 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 361: | 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 383: | Línea 496: | ||
qed | qed | ||
| − | (* pablucoto marpoldia1 *) | + | (* 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 392: | 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 401: | Línea 517: | ||
qed | qed | ||
| − | (* lucnovdos pabrodmac *) | + | (* 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 419: | 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 | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | 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 | qed | ||
| Línea 435: | Línea 587: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal*) | + | (* 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 452: | Línea 607: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou serrodcal pabrodmac *) | + | (* 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 461: | 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 480: | Línea 639: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 wilmorort lucnovdos juacabsou pabrodmac *) | + | (* 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 493: | 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 505: | 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 *) | + | (* 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 530: | 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 *) | + | (* 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 545: | 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 555: | 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 576: | 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 586: | 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 601: | 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 631: | 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 | ||
| + | |||
| + | (* 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 | qed | ||
| Línea 646: | Línea 871: | ||
*} | *} | ||
| − | (* danrodcha pablucoto crigomgom juacabsou*) | + | (* 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 663: | 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 680: | 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 695: | 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 *) | + | (* 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 711: | 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 *) | + | (* 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 736: | 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 | ||
| + | |||
| + | (* 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 | 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 752: | 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 762: | 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 769: | 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 778: | Línea 1035: | ||
qed | qed | ||
| − | (* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou *) (*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 787: | 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 801: | 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 *) | + | (* 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 819: | 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 *) | + | (* 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 847: | Línea 1106: | ||
finally show ?thesis . | finally show ?thesis . | ||
qed | 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 | qed | ||
| Línea 858: | 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 872: | Línea 1175: | ||
qed | qed | ||
| − | (* danrodcha *) | + | (* 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 881: | Línea 1184: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou *) | + | (* 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 890: | 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 905: | 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 919: | 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 926: | 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 935: | 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 fraortmoy *) | ||
| + | theorem "hd (preOrden a) = raiz a" | ||
| + | by (induct a) auto | ||
(* pabrodmac *) | (* 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" | theorem "hd (preOrden a) = raiz a" | ||
| − | by (induct 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 952: | Línea 1333: | ||
*} | *} | ||
| − | (*crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos juacabsou *) | + | (* 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 977: | 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 986: | Línea 1368: | ||
*} | *} | ||
| − | (* danrodcha *) | + | (* 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 1003: | 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 1010: | Línea 1393: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos juacabsou *) (*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 1020: | 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 1030: | 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 1056: | 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 1065: | 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 | ||
| + | |||
| + | (* 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 | 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