Relación 11 - Historial de revisiones

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

2018-07-16T08:16:11Z

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

2015-02-12T21:45:35Z

2015-02-06T10:16:36Z

2015-02-06T10:10:04Z

2015-01-29T07:49:58Z

2015-01-26T08:41:43Z

2015-01-26T08:21:34Z

2015-01-26T08:03:47Z

2015-01-18T15:22:30Z

2015-01-17T13:59:08Z

← Revisión anterior		Revisión del 08:16 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R11: Plegados de listas y de árboles *}		header {* R11: Plegados de listas y de árboles *}

@@ Línea 166: / Línea 166: @@
      using assoc by simp
 qed
 (*jeshorcob:

@@ Línea 282: / Línea 282: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 fun postOrdenAaux :: "['a arbol, 'a list] ⇒ 'a list" where
    "postOrdenAaux H xs = xs"

@@ Línea 264: / Línea 264: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden H = []"

@@ Línea 246: / Línea 246: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden H = []"

@@ Línea 110: / Línea 110: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 fun inversa_ac_aux :: "['a list, 'a list] ⇒ 'a list" where
    "inversa_ac_aux [] ys = ys"
 | "inversa_ac_aux (x#xs) ys = (inversa_ac_aux xs (x#ys))"
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 definition inversa_ac :: "'a list ⇒ 'a list" where
    "inversa_ac xs ≡ inversa_ac_aux xs []"
@@ Línea 134: / Línea 134: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 lemma suma_append [simp]:
    "suma (xs @ ys) = suma xs + suma ys"
 by (induct xs, simp_all)
 text {*

@@ Línea 16: / Línea 16: @@
 estar dada, es una errata. *)
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,juacorvic"
 fun suma :: "nat list ⇒ nat" where
    "suma [] = 0"

@@ Línea 169: / Línea 169: @@
 ademas la prueba queda mas corta *)
---"jeshorcob"
+--"jeshorcob,davoremar"
 definition neutr :: "['a ⇒ 'b ⇒ 'b, 'a] ⇒ bool" where
    "neutr f a == (∀ x. (f a x = x))"
---"jeshorcob"
+--"jeshorcob,davoremar"
 definition assoc :: "['a ⇒ 'a ⇒ 'a] ⇒ bool" where
    "assoc f == (∀ x y z. f (f x y) z = f x (f y z))"
@@ Línea 180: / Línea 180: @@
   cambias el enunciado por uno equivalente? *)
---"jeshorcob"
+--"jeshorcob,davoremar"
 lemma l2: "⟦neutr f a ; assoc f⟧
    ⟹ foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
@@ Línea 208: / Línea 208: @@
 *}
---"jeshorcob"
+--"jeshorcob,davoremar"
 lemma "prod (xs @ ys) = prod xs * prod ys"
 by (simp only: prod_def, rule l2, simp add: neutr_def, simp add: assoc_def)

@@ Línea 153: / Línea 153: @@
 lemma l1:
    assumes neutr: "(∀ x. (f a x = x))" and
-           assoc2: "(∀x y z. f (f x y) z = f x (f y z))"
+           assoc: "(∀x y z. f (f x y) z = f x (f y z))"
    shows "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
 proof (induct xs)
@@ Línea 176: / Línea 176: @@
 definition assoc :: "['a ⇒ 'a ⇒ 'a] ⇒ bool" where
    "assoc f == (∀ x y z. f (f x y) z = f x (f y z))"
 --"jeshorcob"
@@ Línea 181: / Línea 184: @@
    ⟹ foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
 by (induct xs, simp add: neutr_def, simp add: assoc_def)