Relación 3 - Historial de revisiones

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

2018-09-09T08:30:56Z

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

Carvelcab en 15:49 13 nov 2014

2014-11-13T15:49:40Z

Danrodcha en 14:49 13 nov 2014

2014-11-13T14:49:48Z

Jalonso en 12:22 13 nov 2014

2014-11-13T12:22:26Z

Mostrar los cambios

Javrodviv1 en 11:50 13 nov 2014

2014-11-13T11:50:30Z

Pedrosrei en 20:29 12 nov 2014

2014-11-12T20:29:25Z

Domcadgom en 20:28 12 nov 2014

2014-11-12T20:28:03Z

Jeshorcob en 18:54 12 nov 2014

2014-11-12T18:54:05Z

Jeshorcob en 18:53 12 nov 2014

2014-11-12T18:53:26Z

Pedrosrei en 12:21 12 nov 2014

2014-11-12T12:21:51Z

← Revisión anterior		Revisión del 08:30 9 sep 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R3: Razonamiento sobre programas en Isabelle/HOL *}		header {* R3: Razonamiento sobre programas en Isabelle/HOL *}

@@ Línea 14: / Línea 14: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic jeshorcob domcadgom danrodcha carvelcab"
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0"
@@ Línea 47: / Línea 47: @@
    done
--- "davoremar juacorvic jeshorcob danrodcha"
+-- "davoremar juacorvic jeshorcob danrodcha carvelcab"
 lemma "sumaImpares n = n*n"
@@ Línea 61: / Línea 61: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha carvelcab"
 lemma "sumaImpares n = n*n"
@@ Línea 84: / Línea 84: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha carvelcab"
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
@@ Línea 97: / Línea 97: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic jeshorcob danrodcha"
+-- "davoremar juacorvic jeshorcob danrodcha carvelcab"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 by (induct n) auto
@@ Línea 111: / Línea 111: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha carvelcab"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 134: / Línea 134: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha carvelcab"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []"
@@ Línea 151: / Línea 151: @@
    ----------------------------------------------------------------- *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha carvelcab"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p []     = True"
@@ Línea 171: / Línea 171: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic jeshorcob danrodcha"
+-- "davoremar juacorvic jeshorcob danrodcha carvelcab"
 lemma "todos (λy. y=x) (copia n x)"
 by (induct n) auto
@@ Línea 210: / Línea 210: @@
 qed
--- "danrodcha"
+-- "danrodcha carvelcab"
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 231: / Línea 231: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom carvelcab"
 fun factR :: "nat ⇒ nat" where
    "factR 0 = 1"
@@ Línea 272: / Línea 272: @@
    la dejas sin tocar, o como solemos decir: "sea un x cualquiera..." *)
--- "davoremar jeshorcob domcadgom"
+-- "davoremar jeshorcob domcadgom carvelcab"
 lemma fact: "factI' n x = x * factR n"
 proof (induct n arbitrary: x)
@@ Línea 358: / Línea 358: @@
 qed
--- "davoremar juacorvic jeshorcob"
+-- "davoremar juacorvic jeshorcob carvelcab"
 corollary "factI n = factR n"
 proof -
@@ Línea 388: / Línea 388: @@
    ------------------------------------------------------------------ *}
--- "davoremar marnajgom jeshorcob domcadgom"
+-- "davoremar marnajgom jeshorcob domcadgom carvelcab"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y     = [y]"
@@ Línea 400: / Línea 400: @@
    ------------------------------------------------------------------- *}
--- "davoremar"
+-- "davoremar carvelcab"
 lemma "amplia xs y = xs @ [y]"
 by (induct xs) auto
@@ Línea 414: / Línea 414: @@
 qed
--- "davoremar marnajgom jeshorcob domcadgom"
+-- "davoremar marnajgom jeshorcob domcadgom carvelcab"
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 14: / Línea 14: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic jeshorcob domcadgom"
+-- "davoremar juacorvic jeshorcob domcadgom danrodcha"
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0"
@@ Línea 47: / Línea 47: @@
    done
--- "davoremar juacorvic jeshorcob"
+-- "davoremar juacorvic jeshorcob danrodcha"
 lemma "sumaImpares n = n*n"
@@ Línea 61: / Línea 61: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
 lemma "sumaImpares n = n*n"
@@ Línea 84: / Línea 84: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
@@ Línea 97: / Línea 97: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic jeshorcob"
+-- "davoremar juacorvic jeshorcob danrodcha"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 by (induct n) auto
@@ Línea 111: / Línea 111: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 134: / Línea 134: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []"
@@ Línea 151: / Línea 151: @@
    ----------------------------------------------------------------- *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom danrodcha"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p []     = True"
@@ Línea 171: / Línea 171: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic jeshorcob"
+-- "davoremar juacorvic jeshorcob danrodcha"
 lemma "todos (λy. y=x) (copia n x)"
 by (induct n) auto
@@ Línea 208: / Línea 208: @@
    also have "...= todos (λy. y=x)[x]" using HI by simp
    finally show "todos (λy. y=x) (copia (Suc n) x)" using HI by simp
 qed

@@ Línea 15: / Línea 15: @@
 (* Pedrosrei: como no veo a nadie animarse pongo las dos primeras a ver si sirve de ayuda: *)
--- "davoremar juacorvic jeshorcob domcadgom"
+-- "davoremar juacorvic jeshorcob domcadgom javrodviv1"
 fun sumaImpares :: "nat ⇒ nat" where
@@ Línea 61: / Línea 61: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 lemma "sumaImpares n = n*n"
@@ Línea 84: / Línea 84: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
@@ Línea 113: / Línea 113: @@
 qed
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
@@ Línea 135: / Línea 135: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 153: / Línea 153: @@
    ----------------------------------------------------------------- *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
@@ Línea 178: / Línea 178: @@
 by (induct n) auto
--- "davoremar marnajgom jeshorcob domcadgom"
+-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"
 lemma "todos (λy. y=x) (copia n x)"
@@ Línea 220: / Línea 220: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom jeshorcob domcadgom"
+-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"
 fun factR :: "nat ⇒ nat" where
@@ Línea 357: / Línea 357: @@
 qed
--- "marnajgom"
+-- "marnajgom javrodviv1"
 corollary "factI n = factR n"
 proof (induct n)
@@ Línea 379: / Línea 379: @@
    ------------------------------------------------------------------ *}
--- "davoremar marnajgom jeshorcob domcadgom"
+-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 407: / Línea 407: @@
 qed
--- "davoremar marnajgom jeshorcob domcadgom"
+-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"
 lemma "amplia xs y = xs @ [y]"

@@ Línea 158: / Línea 158: @@
    "todos p [] = True"
 | "todos p (x#xs) = ((p x) ∧ (todos p xs))"
 (* jeshorcob: me gustaría saber por qué es necesario poner el paréntesis en la definición(2) *)
 value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"

@@ Línea 30: / Línea 30: @@
    "sumaImpares3 n = foldr (λ x y. y + (2 * x) + 1) (upt 0  n) 0"
-(* Esta definición en principio es más eficiente pero a la hora de demostrar se complica todo. Estaría bien si en clase pudieramos explicar si se puede demostrar el lema usando esta definición de manera sencilla o explicar un poco cómo iría la prueba *)
+(* Esta definición en principio es más eficiente pero a la hora de
 value "sumaImpares 5" -- "= 25"

@@ Línea 15: / Línea 15: @@
 (* Pedrosrei: como no veo a nadie animarse pongo las dos primeras a ver si sirve de ayuda: *)
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 fun sumaImpares :: "nat ⇒ nat" where
@@ Línea 26: / Línea 26: @@
 | "sumaImpares2 (Suc n) = (Suc n)+ n + sumaImpares2 n"
 value "sumaImpares 5" -- "= 25"
@@ Línea 39: / Línea 44: @@
 done
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 lemma "sumaImpares n = n*n"
@@ Línea 53: / Línea 58: @@
 qed
--- "davoremar juacorvic marnajgom"
+-- "davoremar juacorvic marnajgom jeshorcob"
 lemma "sumaImpares n = n*n"
@@ Línea 76: / Línea 81: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom"
+-- "davoremar juacorvic marnajgom jeshorcob"
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
@@ Línea 89: / Línea 94: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 by (induct n) auto
--- "davoremar juacorvic marnajgom"
+-- "jeshorcob"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
@@ Línea 116: / Línea 132: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom"
+-- "davoremar juacorvic marnajgom jeshorcob"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 134: / Línea 150: @@
    ----------------------------------------------------------------- *}
--- "davoremar juacorvic marnajgom"
+-- "davoremar juacorvic marnajgom jeshorcob"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True"
 | "todos p (x#xs) = ((p x) ∧ (todos p xs))"
 value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
@@ Línea 148: / Línea 166: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 lemma "todos (λy. y=x) (copia n x)"
 by (induct n) auto
--- "davoremar marnajgom"
+-- "davoremar marnajgom jeshorcob"
 lemma "todos (λy. y=x) (copia n x)"
@@ Línea 167: / Línea 185: @@
--- "juacorvic"
+-- "juacorvic jeshorcob"
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 195: / Línea 213: @@
    ------------------------------------------------------------------ *}
--- "davoremar juacorvic marnajgom"
+-- "davoremar juacorvic marnajgom jeshorcob"
 fun factR :: "nat ⇒ nat" where
@@ Línea 225: / Línea 243: @@
 value "factI 4" -- "= 24"
--- "davoremar"
+-- "davoremar jeshorcob"
 lemma fact1: "factI' n x = x* factR n"
 by (induct n arbitrary: x) auto
@@ Línea 236: / Línea 254: @@
 tocar, o como solemos decir: "sea un x cualquiera..."
 *)
--- "davoremar"
+-- "davoremar jeshorcob"
 lemma fact: "factI' n x = x * factR n"
@@ Línea 311: / Línea 329: @@
    ------------------------------------------------------------------- *}
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 corollary "factI n = factR n"
@@ Línea 323: / Línea 341: @@
 qed
--- "davoremar juacorvic"
+-- "davoremar juacorvic jeshorcob"
 corollary "factI n = factR n"
@@ Línea 354: / Línea 372: @@
    ------------------------------------------------------------------ *}
--- "davoremar marnajgom"
+-- "davoremar marnajgom jeshorcob"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 382: / Línea 400: @@
 qed
--- "davoremar marnajgom"
+-- "davoremar marnajgom jeshorcob"
 lemma "amplia xs y = xs @ [y]"

@@ Línea 396: / Línea 396: @@
 qed
+(*Pedrosrei: las variables son mudas. Da igual 'a' que 'x', del mismo modo que da igual en papel el nombre de
 -- "juacorvic" (* Demostración idéntica a 'davoremar' pero el sistema me sugirió usar 'a' en vez de 'x' *)
 lemma "amplia xs y = xs @ [y]"