Relación 7 - Historial de revisiones

WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»

2018-09-09T11:53:14Z

Texto reemplazado: «"isar"» por «"isabelle"»

Marnajgom en 11:29 4 dic 2014

2014-12-04T11:29:09Z

Domcadgom en 11:18 4 dic 2014

2014-12-04T11:18:17Z

Carvelcab en 20:58 3 dic 2014

2014-12-03T20:58:42Z

Carvelcab en 20:56 3 dic 2014

2014-12-03T20:56:11Z

Juacorvic en 10:00 3 dic 2014

2014-12-03T10:00:42Z

Juacorvic en 09:58 3 dic 2014

2014-12-03T09:58:54Z

Juacorvic en 09:57 3 dic 2014

2014-12-03T09:57:38Z

Juacorvic en 09:56 3 dic 2014

2014-12-03T09:56:08Z

Juacorvic en 09:49 3 dic 2014

2014-12-03T09:49:41Z

← Revisión anterior		Revisión del 11:53 9 sep 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R7: Recorridos de árboles *}		header {* R7: Recorridos de árboles *}

@@ Línea 36: / Línea 36: @@
 *}
---"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom, marnajgom"
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 58: / Línea 58: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 77: / Línea 77: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
 fun inOrden :: "'a arbol ⇒ 'a list" where
    "inOrden (H x) = [x]"
@@ Línea 95: / Línea 95: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 131: / Línea 131: @@
 qed
--- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)"
 lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 182: / Línea 182: @@
 qed
--- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)"
 lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 proof  (induct a)
@@ Línea 230: / Línea 230: @@
 qed
--- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)"
 theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 265: / Línea 265: @@
   |"raiz (N x _ _ ) = x"
---"juacorvic,carvelcab"
+--"juacorvic,carvelcab, marnajgom"
 fun raiz2 :: "'a arbol ⇒ 'a" where
     "raiz2 (H x) = x"
@@ Línea 287: / Línea 287: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 304: / Línea 304: @@
 *}
---"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom, marnajgom"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 384: / Línea 384: @@
 *}
---"jeshorcob,davoremar,juacorvic, domcadgom"
+--"jeshorcob,davoremar,juacorvic, domcadgom, marnajgom"
 (*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
 theorem "hd (inOrden a) = extremo_izquierda a"
@@ Línea 439: / Línea 439: @@
 by (induct a, simp_all)
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, marnajgom"
 theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 535: / Línea 535: @@
 qed
---"carvelcab, domcadgom"
+--"carvelcab, domcadgom,marnajgom"
 theorem "hd (preOrden a) = raiz a" (is "?P a")
@@ Línea 560: / Línea 560: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
 theorem "hd (inOrden a) = raiz a"
 quickcheck
@@ Línea 616: / Línea 616: @@
 qed
---"carvelcab, domcadgom"
+--"carvelcab, domcadgom,marnajgom"
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 36: / Línea 36: @@
 *}
---"jeshorcob,davoremar,juacorvic, carvelcab"
+--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 58: / Línea 58: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 77: / Línea 77: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 fun inOrden :: "'a arbol ⇒ 'a list" where
    "inOrden (H x) = [x]"
@@ Línea 95: / Línea 95: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 131: / Línea 131: @@
 qed
--- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
 lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 161: / Línea 161: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 lemma "postOrden (espejo a) = rev (preOrden a)"
 by (induct a, simp_all)
@@ Línea 182: / Línea 182: @@
 qed
--- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
 lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 proof  (induct a)
@@ Línea 210: / Línea 210: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 theorem "inOrden (espejo a) = rev (inOrden a)"
 by (induct a, simp_all)
@@ Línea 230: / Línea 230: @@
 qed
--- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)"
+-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
 theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 260: / Línea 260: @@
    ---------------------------------------------------------------------
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar, domcadgom"
 fun raiz :: "'a arbol ⇒ 'a" where
    "raiz (H x) = x"
@@ Línea 287: / Línea 287: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 304: / Línea 304: @@
 *}
---"jeshorcob,davoremar,juacorvic, carvelcab"
+--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 318: / Línea 318: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 (*jeshorcob: al intentar hacer la prueba automática, el sistema se
 pregunta por el caso en el que la lista sea vacía. Debemos indicar que
@@ Línea 325: / Línea 325: @@
 by (induct a, simp_all)
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, domcadgom"
 theorem "last (inOrden a) = extremo_derecha a"
 by (induct a, simp_all add: a1)
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, domcadgom"
 lemma  "inOrden a ≠ []"
 proof (induct a)
@@ Línea 340: / Línea 340: @@
 qed
---"jeshorcob,davoremar,carvelcab"
+--"jeshorcob,davoremar,carvelcab, domcadgom"
 theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
 proof (induct a)
@@ Línea 384: / Línea 384: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, domcadgom"
 (*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
 theorem "hd (inOrden a) = extremo_izquierda a"
 by (induct a, simp_all add: a1)
---"jeshorcob,davoremar,carvelcab"
+--"jeshorcob,davoremar,carvelcab, domcadgom"
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)
@@ Línea 435: / Línea 435: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, domcadgom"
 theorem "hd (preOrden a) = last (postOrden a)"
 by (induct a, simp_all)
@@ Línea 475: / Línea 475: @@
 qed
---"carvelcab"
+--"carvelcab, domcadgom"
 theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
@@ Línea 499: / Línea 499: @@
 *}
---"jeshorcob,davoremar,carvelcab"
+--"jeshorcob,davoremar,carvelcab, domcadgom"
 theorem "hd (preOrden a) = raiz a"
 by (induct a, simp_all)
@@ Línea 535: / Línea 535: @@
 qed
---"carvelcab"
+--"carvelcab, domcadgom"
 theorem "hd (preOrden a) = raiz a" (is "?P a")
@@ Línea 560: / Línea 560: @@
 *}
---"jeshorcob,davoremar,juacorvic,carvelcab"
+--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
 theorem "hd (inOrden a) = raiz a"
 quickcheck
@@ Línea 579: / Línea 579: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar, domcadgom"
 theorem "last (postOrden a) = raiz a"
 by (induct a, simp_all)
@@ Línea 616: / Línea 616: @@
 qed
---"carvelcab"
+--"carvelcab, domcadgom"
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 474: / Línea 474: @@
      last (postOrden (N a1 a2 a3))" by simp
 qed
 theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
@@ Línea 532: / Línea 534: @@
    finally show "hd (preOrden (N a1 a2 a3)) = raiz (N a1 a2 a3)" by simp
 qed
 theorem "hd (preOrden a) = raiz a" (is "?P a")
@@ Línea 612: / Línea 616: @@
 qed
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 36: / Línea 36: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, carvelcab"
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 58: / Línea 58: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 77: / Línea 77: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 fun inOrden :: "'a arbol ⇒ 'a list" where
    "inOrden (H x) = [x]"
@@ Línea 95: / Línea 95: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 110: / Línea 110: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 lemma  "preOrden (espejo a) = rev (postOrden a)"
 by (induct a, simp_all)
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 161: / Línea 161: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 lemma "postOrden (espejo a) = rev (preOrden a)"
 by (induct a, simp_all)
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 210: / Línea 210: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 theorem "inOrden (espejo a) = rev (inOrden a)"
 by (induct a, simp_all)
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 265: / Línea 265: @@
   |"raiz (N x _ _ ) = x"
---"juacorvic"
+--"juacorvic,carvelcab"
 fun raiz2 :: "'a arbol ⇒ 'a" where
     "raiz2 (H x) = x"
@@ Línea 287: / Línea 287: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 304: / Línea 304: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic, carvelcab"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 318: / Línea 318: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 (*jeshorcob: al intentar hacer la prueba automática, el sistema se
 pregunta por el caso en el que la lista sea vacía. Debemos indicar que
@@ Línea 340: / Línea 340: @@
 qed
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
 proof (induct a)
@@ Línea 389: / Línea 389: @@
 by (induct a, simp_all add: a1)
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)
@@ Línea 475: / Línea 475: @@
 qed
 text {*
@@ Línea 483: / Línea 497: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,carvelcab"
 theorem "hd (preOrden a) = raiz a"
 by (induct a, simp_all)
@@ Línea 519: / Línea 533: @@
 qed
 text {*
@@ Línea 527: / Línea 556: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,carvelcab"
 theorem "hd (inOrden a) = raiz a"
 quickcheck
@@ Línea 583: / Línea 612: @@
 qed
 end
 </source>

@@ Línea 368: / Línea 368: @@
    then have "... = extremo_derecha a3" using h2 by simp
    thus "last (inOrden(N a1 a2 a3))=extremo_derecha(N a1 a2 a3)" by simp
-qde
+qed
 oops
@@ Línea 561: / Línea 561: @@
 qed
--"juacorvic"
+--"juacorvic"
 (*Muy detallada*)
 theorem "last (postOrden a) = raiz a"

@@ Línea 559: / Línea 559: @@
    also have "... = x" by simp
    finally show "?P (N x y z)" by simp
 qed
 end
 </source>