Relación 8 - Historial de revisiones

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

2018-09-10T09:55:27Z

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

2015-01-18T14:52:46Z

2014-12-18T12:09:38Z

2014-12-18T08:26:42Z

2014-12-18T08:25:26Z

2014-12-18T08:18:58Z

2014-12-18T08:15:14Z

2014-12-18T08:01:52Z

2014-12-17T11:10:05Z

2014-12-17T08:42:49Z

← Revisión anterior		Revisión del 09:55 10 sep 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 297: / Línea 297: @@
 by (induct a, simp_all)
--- "jeshorcob, carvelcab"
+-- "jeshorcob, carvelcab,davoremar"
 lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
 by (induct a, auto simp add: a1)
@@ Línea 335: / Línea 335: @@
      using a1 a2 es_abc.simps(2) by blast
 qed
 text {*
@@ Línea 509: / Línea 519: @@
 lemma rel_size_igualdad: " es_abc size  a = es_abc hojas a"
 by (induct a, simp_all add: l_hojas_size)
 text {*
@@ Línea 607: / Línea 625: @@
 lemma "es_abc profundidad a = es_abc size a"
 using completo1 rel_size_igualdad by simp_all
 text {*

@@ Línea 713: / Línea 713: @@
 lemma "es_abc medida a = es_abc size a"
 quickcheck
+oops
 (*Contraejemplo
 value "es_abc medida (N H (N H H))" (*devuelve true*)

@@ Línea 584: / Línea 584: @@
      es_abc profundidad a ⟷ es_abc size  a
-Nota: Para apartado 7 uso demostración de "jeshorcob y carvelcab", que
+Nota: Aplico demostración de "domcadgom" de apartado 7, que
 no he conseguido reproducir *)
 lemma "es_abc profundidad a = es_abc size a"
-using profundidad_y_hojas_completo rel_size_igualdad by simp_all
+using completo1 rel_size_igualdad by simp_all

@@ Línea 663: / Línea 663: @@
 *}
 --"Pedrosrei:"
-lemma "es_abc f = es_abc nodos
+lemma "es_abc f = es_abc nodos"
 quickcheck
 oops

@@ Línea 702: / Línea 702: @@
 quickcheck
 oops
 end
 </source>

@@ Línea 650: / Línea 650: @@
 --"davoremar, domcadgom"
 lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
 by (induct a, simp_all)

@@ Línea 600: / Línea 600: @@
 apply (induct n, auto) done
---"jeshorcob,davoremar, domcadgom,carvelcab"
+--"jeshorcob,davoremar, domcadgom,carvelcab,juacorvic"
 lemma "es_abc f (abc n)"
 by (induct n, simp_all)
@@ Línea 616: / Línea 616: @@
    finally show "?P (Suc n)" by simp
 qed
 text {*

← Revisión anterior		Revisión del 08:42 17 dic 2014
Línea 572:		Línea 572:
	corollary completo3: "es_abc profundidad a = es_abc size a"		corollary completo3: "es_abc profundidad a = es_abc size a"
	using completo1 completo2 by simp		using completo1 completo2 by simp
		+
		+
		+
		+	--"juacorvic"
		+	(*
		+	1.- En apartado 7 se demuestra que:
		+	es_abc profundidad a ⟷ es_abc hojas a
		+	2.- En apartado 8 se demuestra que:
		+	es_abc hojas a ⟷ es_abc size a
		+	3.- Luego podremos demostrar usando las anteriores:
		+	es_abc profundidad a ⟷ es_abc size a
		+
		+	Nota: Para apartado 7 uso demostración de "jeshorcob y carvelcab", que
		+	no he conseguido reproducir *)
		+	lemma "es_abc profundidad a = es_abc size a"
		+	using profundidad_y_hojas_completo rel_size_igualdad by simp_all
		+