Relación 2 - Historial de revisiones

Jalonso en 18:38 14 jul 2018

2018-07-14T18:38:27Z

Jospermon1 en 11:52 1 mar 2018

2018-03-01T11:52:27Z

Jalonso: Desprotegió «Relación 2»

2018-02-10T05:41:26Z

Desprotegió «Relación 2»

Jalonso en 09:05 9 nov 2017

2017-11-09T09:05:05Z

Jalonso: Protegió «Relación 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2017-11-09T08:53:09Z

Protegió «Relación 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Cesgongut en 06:22 9 nov 2017

2017-11-09T06:22:33Z

Jescudero en 01:54 9 nov 2017

2017-11-09T01:54:20Z

Jescudero en 01:48 9 nov 2017

2017-11-09T01:48:07Z

Rafferrod en 23:19 8 nov 2017

2017-11-08T23:19:16Z

Jescudero en 21:59 8 nov 2017

2017-11-08T21:59:27Z

← Revisión anterior		Revisión del 18:38 14 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}		chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}

@@ Línea 17: / Línea 17: @@
 (* anddonram  edupalhid macmerflo luicedval rafcabgon jescudero
-    davperriv diwu2 rafferrod *)
+    davperriv diwu2 rafferrod jospermon1 *)
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0"
@@ Línea 37: / Línea 37: @@
 (* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
-    jescudero rafferrod*)
+    jescudero rafferrod jospermon1*)
 lemma "sumaImpares n = n*n"
    by(induct n) simp_all
@@ Línea 58: / Línea 58: @@
 (* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
-    jescudero rafferrod cesgongut *)
+    jescudero rafferrod cesgongut jospermon1*)
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
     "sumaPotenciasDeDosMasUno 0 = 1 + 1"
@@ Línea 71: / Línea 71: @@
 (* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
-    jescudero rafferrod cesgongut*)
+    jescudero rafferrod cesgongut jospermon1*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    by(induct n) simp_all
@@ Línea 84: / Línea 84: @@
 (* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
-    jescudero rafferrod cesgongut *)
+    jescudero rafferrod cesgongut jospermon1*)
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []"
@@ Línea 102: / Línea 102: @@
 (* anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod
-    jescudero cesgongut *)
+    jescudero cesgongut jospermon1*)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p []     = True"
@@ Línea 121: / Línea 121: @@
 (* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
-    rafferrod jescudero cesgongut *)
+    rafferrod jescudero cesgongut jospermon1*)
 lemma "todos (λy. y=x) (copia n x)"
    by (induct n) simp_all
@@ Línea 137: / Línea 137: @@
 (* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
-    rafferrod jescudero cesgongut *)
+    rafferrod jescudero cesgongut jospermon1*)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y     = [y]"

@@ Línea 16: / Línea 16: @@
    ------------------------------------------------------------------ *}
-(* anddonram  edupalhid macmerflo luicedval rafcabgon jescudero davperriv diwu2 rafferrod *)
+(* anddonram  edupalhid macmerflo luicedval rafcabgon jescudero
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0"
@@ Línea 34: / Línea 35: @@
       sumaImpares n = n*n
    ------------------------------------------------------------------- *}
 (* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod*)
 lemma "sumaImpares n = n*n"
    by(induct n) simp_all
@@ Línea 54: / Línea 57: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut *)
+(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
     "sumaPotenciasDeDosMasUno 0 = 1 + 1"
-|  "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno n"
+ |  "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno n"
 value "sumaPotenciasDeDosMasUno 3 = 16"
@@ Línea 66: / Línea 70: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut*)
+(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    by(induct n) simp_all
@@ Línea 78: / Línea 83: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut*)
+(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []"
@@ Línea 95: / Línea 101: @@
    ----------------------------------------------------------------- *}
-(*anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
+(* anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
-   "todos p [] = True"
+   "todos p []     = True"
 | "todos p (x#xs) = (p x ∧ todos p xs)"
@@ Línea 104: / Línea 111: @@
 (* edupalhid *)
+fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
-fun todos' :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
+  "todos2 p []     = True" |
-    "todos' p [] = True" |
+  "todos2 p (x#xs) = (if p x then todos2 p xs else False)"
 text {* ---------------------------------------------------------------
@@ Línea 114: / Línea 120: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
+(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
 lemma "todos (λy. y=x) (copia n x)"
    by (induct n) simp_all
-−
 text {* ---------------------------------------------------------------
    Ejercicio 4.1. Definir, recursivamente y sin usar (@), la función
@@ Línea 126: / Línea 136: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
+(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
-   "amplia [] y = [y]"
+   "amplia [] y     = [y]"
-| "amplia (x#xs) y = x#amplia xs y "
+| "amplia (x#xs) y = x # amplia xs y"
 value "amplia [d,a] t = [d,a,t]"
@@ Línea 138: / Línea 149: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
+(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
 lemma "amplia xs y = xs @ [y]"
    by (induct xs) simp_all

@@ Línea 16: / Línea 16: @@
    ------------------------------------------------------------------ *}
-(* anddonram  edupalhid macmerflo luicedval rafcabgon jescudero davperriv diwu2 rafferrod*)
+(* anddonram  edupalhid macmerflo luicedval rafcabgon jescudero davperriv diwu2 rafferrod *)
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0"
@@ Línea 22: / Línea 22: @@
 value "sumaImpares 5 = 25"
 text {* ---------------------------------------------------------------
@@ Línea 30: / Línea 37: @@
 lemma "sumaImpares n = n*n"
    by(induct n) simp_all
 text {* ---------------------------------------------------------------
@@ Línea 40: / Línea 54: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod*)
+(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut *)
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
     "sumaPotenciasDeDosMasUno 0 = 1 + 1"
@@ Línea 52: / Línea 66: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod*)
+(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    by(induct n) simp_all
@@ Línea 64: / Línea 78: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod*)
+(*anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2 jescudero rafferrod cesgongut*)
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []"
@@ Línea 81: / Línea 95: @@
    ----------------------------------------------------------------- *}
+(*anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True"
@@ Línea 101: / Línea 114: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero*)
+(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
 lemma "todos (λy. y=x) (copia n x)"
    by (induct n) simp_all
@@ Línea 113: / Línea 126: @@
    ------------------------------------------------------------------ *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero*)
+(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y = [y]"
@@ Línea 125: / Línea 138: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero*)
+(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero cesgongut*)
 lemma "amplia xs y = xs @ [y]"
    by (induct xs) simp_all

@@ Línea 82: / Línea 82: @@
-(*anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod*)
+(*anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero*)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True"
@@ Línea 101: / Línea 101: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod*)
+(*anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2 rafferrod jescudero*)
 lemma "todos (λy. y=x) (copia n x)"
    by (induct n) simp_all

← Revisión anterior	Revisión del 05:41 10 feb 2018
(Sin diferencias)

← Revisión anterior	Revisión del 08:53 9 nov 2017
(Sin diferencias)