Relación 8 - Historial de revisiones

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

2018-07-16T15:46:16Z

Texto reemplazado: «isar» por «isabelle»

2014-03-08T15:12:55Z

2014-03-07T02:35:29Z

2014-03-07T02:28:38Z

2014-01-16T11:29:26Z

2014-01-16T11:09:22Z

2014-01-16T11:05:15Z

2014-01-16T10:03:16Z

2014-01-16T09:35:03Z

2014-01-16T09:23:47Z

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R8: Árboles binarios completos *}		header {* R8: Árboles binarios completos *}

@@ Línea 188: / Línea 188: @@
 by (induct n) auto
---"irealetei, diecabmen1, maresccas4"
+--"irealetei, diecabmen1, maresccas4 domlloriv"
 (*irealetei: casi me estalla el cerebro con esta demo, gracias a Marco que me dio una pista hace un par de días sobre que el había usado el assumes. La automática se me queda a medias.*)
 lemma 00:

@@ Línea 253: / Línea 253: @@
 (*he conseguido hacer uno!! bieeeeeeeen!!"*)
 lemma relaccion_hojas_nodo:"hojas (a) = size (a) + 1"
 by (induct a) auto
@@ Línea 284: / Línea 289: @@
 --"julrobrel: la relacion entre la profundidad y el numero de nodos es (nodos+1=2^profundidad)"
 lemma "Suc(size (abc n))=2^(profundidad (abc n))"
 by (induct n) auto
@@ Línea 320: / Línea 329: @@
 lemma profundidad_lemma: "profundidad_jrr (abc n) = n"
 by (induct n) auto
 lemma "es_abc_jrr n (abc n)"
@@ Línea 360: / Línea 374: @@
 by (induct a) auto
---"irealetei maresccas4 domlloriv marescpla"
+--"irealetei maresccas4 domlloriv marescpla jaisalmen zoiruicha"
 lemma "es_abc profundidad a ⟹ a = abc (profundidad a)" by (induct a) auto
 text {*
@@ Línea 386: / Línea 399: @@
 *)
--- "irealetei maresccas4 domlloriv"
+-- "irealetei maresccas4 domlloriv jaisalmen zoiruicha"
 lemma "es_abc f a = es_abc size a"
 quickcheck

@@ Línea 40: / Línea 40: @@
 | "hojas (N i d) = hojas i + hojas d"
---"julrobrel maresccas4"
+--"julrobrel maresccas4 jaisalmen zoiruicha"
 fun hojas_jrr :: "arbol => nat" where
     "hojas_jrr H = 1"                     --"julrobrel: minima diferencia con la anterior"
@@ Línea 80: / Línea 80: @@
    "profundidad_jrr H = 0"
   |"profundidad_jrr (N i d) = Suc (maximo (profundidad_jrr i) (profundidad_jrr d))" --"julrobrel: En realidad al ser arboles completos no deberia hacer falta el maximo"
 value "profundidad (N (N H H) (N H H))" -- "= 2"
@@ Línea 107: / Línea 113: @@
 *}
---"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv marescpla pabflomar"
+--"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv marescpla pabflomar jaisalmen zoiruicha"
 fun abc :: "nat ⇒ arbol" where
    "abc 0 = H"
@@ Línea 128: / Línea 134: @@
 *}
---"diecabmen1 irealetei juaruipav maresccas4 domlloriv marescpla pabflomar"
+--"diecabmen1 irealetei juaruipav maresccas4 domlloriv marescpla pabflomar jaisalmem zoiruicha"
 fun es_abc :: "(arbol => 'a) => arbol => bool" where
    "es_abc f H = True"
@@ Línea 178: / Línea 184: @@
 *}
 --"julrobrel: en un arbol binario completo la profundidad y las hojas estan relacionadas por la siguiente igualdad (hojas = 2^profundidad)"
 lemma "(hojas (abc n))=2^(profundidad (abc n))"
 by (induct n) auto

← Revisión anterior		Revisión del 11:29 16 ene 2014
Línea 217:		Línea 217:

	oops		oops
		+
		+
		+
		+	-- "pabflomar"
		+
		+	lemma "(hojas (abc n))= 2^(profundidad_pfm (abc n))"
		+	proof (induct n)
		+	show " hojas (abc 0) = 2 ^ profundidad_pfm (abc 0)" by simp
		+	next
		+	fix n
		+	assume HI: " hojas (abc n) = 2 ^ profundidad_pfm (abc n)"
		+	then have " hojas (abc (Suc n)) = 2 * hojas (abc n)" by simp
		+	also have "... = 2 * (2 ^ profundidad_pfm (abc n))" using HI by simp
		+	finally show "hojas (abc (Suc n)) = 2 ^ profundidad_pfm (abc (Suc n))" by simp
		+	qed

	text {*		text {*

@@ Línea 35: / Línea 35: @@
 *}
---"diecabmen1 irealetei juaruipav domlloriv marescpla"
+--"diecabmen1 irealetei juaruipav domlloriv marescpla pabflomar"
 fun hojas :: "arbol => nat" where
    "hojas H = Suc 0"
@@ Línea 65: / Línea 65: @@
 | "profundidad (N i d) = (if profundidad i > profundidad d then Suc (profundidad i) else Suc (profundidad d))"
---"julrobrel"
+--"julrobrel pabflomar"
 fun maximo :: "nat => nat => nat" where
    "maximo a b = (if a < b then b else a)"
 value "maximo 3 4" -- "=4"
@@ Línea 102: / Línea 107: @@
 *}
---"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv marescpla"
+--"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv marescpla pabflomar"
 fun abc :: "nat ⇒ arbol" where
    "abc 0 = H"
@@ Línea 123: / Línea 128: @@
 *}
---"diecabmen1 irealetei juaruipav maresccas4 domlloriv marescpla"
+--"diecabmen1 irealetei juaruipav maresccas4 domlloriv marescpla pabflomar"
 fun es_abc :: "(arbol => 'a) => arbol => bool" where
    "es_abc f H = True"

@@ Línea 365: / Línea 365: @@
 (*f = λx. a
 a = N H (N H H)*)
 end
 </source>

@@ Línea 35: / Línea 35: @@
 *}
---"diecabmen1 irealetei juaruipav"
+--"diecabmen1 irealetei juaruipav domlloriv"
 fun hojas :: "arbol => nat" where
    "hojas H = Suc 0"
@@ Línea 83: / Línea 83: @@
---"irealetei maresccas4"
+--"irealetei maresccas4 domlloriv"
 fun profundidad3 :: "arbol => nat" where
    "profundidad3 (H) = 0"
@@ Línea 100: / Línea 100: @@
 *}
---"diecabmen1, julrobrel irealetei juaruipav maresccas4"
+--"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv"
 fun abc :: "nat ⇒ arbol" where
    "abc 0 = H"
@@ Línea 121: / Línea 121: @@
 *}
---"diecabmen1 irealetei juaruipav maresccas4"
+--"diecabmen1 irealetei juaruipav maresccas4 domlloriv"
 fun es_abc :: "(arbol => 'a) => arbol => bool" where
    "es_abc f H = True"
@@ Línea 221: / Línea 221: @@
 by (induct n) auto
--- "irealetei maresccas4 diecabmen1"
+-- "irealetei maresccas4 diecabmen1 domlloriv"
 (*he conseguido hacer uno!! bieeeeeeeen!!"*)
 lemma relaccion_hojas_nodo:"hojas (a) = size (a) + 1"
@@ Línea 331: / Línea 331: @@
 by (induct a) auto
---"irealetei maresccas4"
+--"irealetei maresccas4 domlloriv"
 lemma "es_abc profundidad a ⟹ a = abc (profundidad a)" by (induct a) auto
@@ Línea 356: / Línea 356: @@
 *)
--- "irealetei maresccas4"
+-- "irealetei maresccas4 domlloriv"
 lemma "es_abc f a = es_abc size a"
 quickcheck