Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle») |
|||
| (No se muestran 127 ediciones intermedias de 20 usuarios) | |||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
chapter {* R6: Recorridos de árboles *} | chapter {* R6: Recorridos de árboles *} | ||
| Línea 16: | Línea 16: | ||
c g | c g | ||
/ \ / \ | / \ / \ | ||
| − | a d f | + | a d f 3 |
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))". | se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))". | ||
--------------------------------------------------------------------- | --------------------------------------------------------------------- | ||
*} | *} | ||
| − | (* ivamenjim marpoldia1 manmorjim1 bowma migtermor *) | + | (* 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 *) | + | (* 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 *) | + | (* 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 *) | + | (* 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 *) | + | (* 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 *) | + | (* 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 *) | + | (* 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 168: | 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 178: | 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 196: | 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 206: | 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 218: | 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*) | ||
lemma "preOrden (espejo a) = rev (postOrden a)" | lemma "preOrden (espejo a) = rev (postOrden a)" | ||
by (induct a) auto | 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 {* | text {* | ||
| Línea 248: | Línea 333: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor *) | + | (* 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 258: | 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 277: | 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 287: | 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 296: | Línea 387: | ||
qed | qed | ||
| − | (* fraortmoy *) | + | (* 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*) | ||
| + | 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 {* | text {* | ||
| Línea 307: | Línea 460: | ||
*} | *} | ||
| − | (* ivamenjim crigomgom bowma migtermor *) | + | (* 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 317: | 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 339: | 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 348: | 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 | ||
also have "... = rev (inOrden (N x i d))" by simp | also have "... = rev (inOrden (N x i d))" by simp | ||
finally show "?P (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 | qed | ||
| Línea 366: | Línea 587: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 *) | + | (* 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 383: | Línea 607: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 *) | + | (* 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 392: | 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 411: | Línea 639: | ||
*} | *} | ||
| − | (* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto migtermor marpoldia1 *) | + | (* 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 424: | 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 436: | 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 *) | + | (* 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 461: | 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 476: | 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 486: | 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 | ||
| + | |||
| + | (* 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 | qed | ||
| Línea 500: | 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 515: | 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 "… = extremo_derecha d" using | + | also have "… = last (inOrden d)" using AUX by simp |
| − | finally show "?P (N | + | 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 | qed | ||
| Línea 528: | Línea 871: | ||
*} | *} | ||
| − | (* danrodcha pablucoto crigomgom*) | + | (* 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 545: | Línea 889: | ||
qed | qed | ||
| − | (* bowma *) | + | (* 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 562: | 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 577: | 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 *) | + | (* 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 593: | 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 | ||
| + | |||
| + | (* 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 | 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 {* | text {* | ||
| Línea 606: | Línea 1009: | ||
*} | *} | ||
| − | (* danrodcha *) | + | (* 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 616: | 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 623: | 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 632: | Línea 1035: | ||
qed | qed | ||
| − | (* pablucoto crigomgom bowma *) (*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 641: | 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 655: | 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 673: | 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 | ||
| + | |||
| + | (* 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 | 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 {* | text {* | ||
| Línea 686: | 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 700: | 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 709: | Línea 1184: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim *) | + | (* 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 718: | 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 733: | 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 747: | 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 754: | 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 763: | 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 | ||
| + | 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 | finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp | ||
qed | qed | ||
| Línea 775: | Línea 1333: | ||
*} | *} | ||
| − | (*crigomgom pablucoto bowma migtermor ivamenjim *) | + | (* 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 *) | ||
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 800: | 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 809: | 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 826: | 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 833: | Línea 1393: | ||
qed | qed | ||
| − | (* pablucoto crigomgom ivamenjim *) (*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 843: | 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 853: | 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 879: | 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 888: | 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