Relación 2 - Historial de revisiones

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

2018-07-16T15:46:13Z

Texto reemplazado: «isar» por «isabelle»

Jalonso: Desprotegió «Relación 2»

2014-01-22T18:23:54Z

Desprotegió «Relación 2»

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

2013-12-07T07:56:31Z

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

Zoiruicha en 12:08 21 nov 2013

2013-11-21T12:08:06Z

Marescpla en 11:34 21 nov 2013

2013-11-21T11:34:51Z

Jaisalmen en 02:06 21 nov 2013

2013-11-21T02:06:38Z

Jaisalmen en 02:05 21 nov 2013

2013-11-21T02:05:15Z

Jaisalmen en 01:50 21 nov 2013

2013-11-21T01:50:39Z

Jaisalmen en 01:48 21 nov 2013

2013-11-21T01:48:20Z

Jaisalmen en 01:41 21 nov 2013

2013-11-21T01:41:51Z

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

@@ Línea 30: / Línea 30: @@
 value "sumaImpares2 5" -- "= 25"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun sumaImpares3 :: "nat ⇒ nat" where
    "sumaImpares3 0 = 0"
@@ Línea 53: / Línea 53: @@
 by (induct n) auto
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 lemma "sumaImpares3 n = n*n"
 by (induct n) auto
@@ Línea 81: / Línea 81: @@
 value "sumaPotenciasDeDosMasUno2 3" -- "= 16"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun sumaPotenciasDeDosMasUno3 :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno3 0 = 2"
@@ Línea 93: / Línea 93: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 diecabmen1 irealetei juaruipav domlloriv pabflomar jaisalmen, marescpla"
+-- "maresccas4 diecabmen1 irealetei juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
@@ Línea 122: / Línea 122: @@
 value "copia2 3 x" -- "= [x,x,x]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun copia3 :: "nat ⇒ 'a ⇒ 'a list" where
    "copia3 0 x = []"
@@ Línea 139: / Línea 139: @@
    ----------------------------------------------------------------- *}
--- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen, marescpla"
+-- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen, marescpla zoiruicha"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
@@ Línea 161: / Línea 161: @@
    ------------------------------------------------------------------- *}
--- "maresccas4,juaruipav domlloriv pabflomar jaisalmen, marescpla"
+-- "maresccas4,juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"
 lemma "todos (λy. y=x) (copia n x)"
@@ Línea 185: / Línea 185: @@
 value "factR 4" -- "= 24"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun factR2 :: "nat ⇒ nat" where
    "factR2 0 = 1"
@@ Línea 214: / Línea 214: @@
 value "factI 4" -- "= 24"
--- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen, marescpla"
+-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"
 lemma fact: "factI' n x = x * factR n"
@@ Línea 224: / Línea 224: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen" "no lo entiendo (marescpla)"
+-- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen zoiruicha" "no lo entiendo (marescpla)"
 corollary "factI n = factR n"
@@ Línea 237: / Línea 237: @@
    ------------------------------------------------------------------ *}
--- "maresccas4,juaruipav domlloriv jaisalmen"
+-- "maresccas4,juaruipav domlloriv jaisalmen zoiruicha"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 266: / Línea 266: @@
    ------------------------------------------------------------------- *}
--- "maresccas4, juaruipav domlloriv pabflomar jaisalmen"
+-- "maresccas4, juaruipav domlloriv pabflomar jaisalmen zoiruicha"
 lemma "amplia xs y = xs @ [y]"

@@ Línea 22: / Línea 22: @@
 value "sumaImpares 5" -- "= 25"
--- "diecabmen1 irealetei juaruipav domlloriv"
+-- "diecabmen1 irealetei juaruipav domlloriv, marescpla"
 thm nat.induct
 fun sumaImpares2 :: "nat ⇒ nat" where
    "sumaImpares2 0 = 0"
-| "sumaImpares2 (Suc n) = (2*n + 1) + sumaImpares2 n"
+| "sumaImpares2 (Suc n) = (2*n + 1) + sumaImpares2 n" <-- "yo he puesto el +1 con un Suc (marescpla)"
 value "sumaImpares2 5" -- "= 25"
@@ Línea 36: / Línea 36: @@
 value "sumaImpares 5" -- "= 25"
 text {* ---------------------------------------------------------------
@@ Línea 42: / Línea 43: @@
    ------------------------------------------------------------------- *}
--- "maresccas4,juaruipav domlloriv pabflomar"
+-- "maresccas4,juaruipav domlloriv pabflomar, marescpla"
 lemma "sumaImpares n = n*n"
@@ Línea 65: / Línea 66: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 diecabmen1 irealetei domlloriv pabflomar"
+-- "maresccas4 diecabmen1 irealetei domlloriv pabflomar, marescpla"
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
@@ Línea 92: / Línea 93: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 diecabmen1 irealetei juaruipav domlloriv pabflomar jaisalmen"
+-- "maresccas4 diecabmen1 irealetei juaruipav domlloriv pabflomar jaisalmen, marescpla"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
@@ Línea 105: / Línea 106: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 irealetei domlloriv juaruipav pabflomar"
+-- "maresccas4 irealetei domlloriv juaruipav pabflomar, marescpla"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 138: / Línea 139: @@
    ----------------------------------------------------------------- *}
--- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen"
+-- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen, marescpla"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
@@ Línea 160: / Línea 161: @@
    ------------------------------------------------------------------- *}
--- "maresccas4,juaruipav domlloriv pabflomar jaisalmen"
+-- "maresccas4,juaruipav domlloriv pabflomar jaisalmen, marescpla"
 lemma "todos (λy. y=x) (copia n x)"
@@ Línea 176: / Línea 177: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar"
+-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar, marescpla"
 fun factR :: "nat ⇒ nat" where
    "factR 0 = 1"
-   |"factR (Suc n) = (Suc n) * factR n"
+   |"factR (Suc n) = (Suc n) * factR n" <--"creo que no hacen falta los paréntesis del 2º suc (marescpla)"
 value "factR 4" -- "= 24"
@@ Línea 213: / Línea 214: @@
 value "factI 4" -- "= 24"
--- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen"
+-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen, marescpla"
 lemma fact: "factI' n x = x * factR n"
@@ Línea 223: / Línea 224: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen"
+-- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen" "no lo entiendo (marescpla)"
 corollary "factI n = factR n"
@@ Línea 252: / Línea 253: @@
 value "amplia2 [d,a] t" -- "= [d,a,t]"
--- "pabflomar" ¿Sería mejor poner los paréntesis en la llamada a amplia como hace maresccas4?
+-- "pabflomar, marescpla" ¿Sería mejor poner los paréntesis en la llamada a amplia como hace maresccas4?
 fun amplia3 :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia3 [] y = [y]"

@@ Línea 81: / Línea 81: @@
 -- "jaisalmen"
-fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
+fun sumaPotenciasDeDosMasUno3 :: "nat ⇒ nat" where
-   "sumaPotenciasDeDosMasUno 0 = 2"
+   "sumaPotenciasDeDosMasUno3 0 = 2"
-|  "sumaPotenciasDeDosMasUno (n) = 2^n + sumaPotenciasDeDosMasUno(n - 1)"
+|  "sumaPotenciasDeDosMasUno3 (n) = 2^n + sumaPotenciasDeDosMasUno3(n - 1)"
-value "sumaPotenciasDeDosMasUno2 3" -- "= 16"
+value "sumaPotenciasDeDosMasUno3 3" -- "= 16"
 text {* ---------------------------------------------------------------

@@ Línea 138: / Línea 138: @@
    ----------------------------------------------------------------- *}
--- "maresccas4 irealetei diecabmen1 juaruipav pabflomar "
+-- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
@@ Línea 160: / Línea 160: @@
    ------------------------------------------------------------------- *}
--- "maresccas4,juaruipav domlloriv pabflomar"
+-- "maresccas4,juaruipav domlloriv pabflomar jaisalmen"
 lemma "todos (λy. y=x) (copia n x)"
@@ Línea 183: / Línea 183: @@
 value "factR 4" -- "= 24"
 text {* ---------------------------------------------------------------
@@ Línea 206: / Línea 213: @@
 value "factI 4" -- "= 24"
--- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar"
+-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen"
 lemma fact: "factI' n x = x * factR n"
@@ Línea 216: / Línea 223: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 diecabmen1 juaruipav pabflomar"
+-- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen"
 corollary "factI n = factR n"
@@ Línea 229: / Línea 236: @@
    ------------------------------------------------------------------ *}
--- "maresccas4,juaruipav domlloriv"
+-- "maresccas4,juaruipav domlloriv jaisalmen"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 258: / Línea 265: @@
    ------------------------------------------------------------------- *}
--- "maresccas4, juaruipav domlloriv pabflomar"
+-- "maresccas4, juaruipav domlloriv pabflomar jaisalmen"
 lemma "amplia xs y = xs @ [y]"

← Revisión anterior	Revisión del 18:23 22 ene 2014
(Sin diferencias)

← Revisión anterior	Revisión del 07:56 7 dic 2013
(Sin diferencias)

← Revisión anterior		Revisión del 01:50 21 nov 2013
Línea 120:		Línea 120:

	value "copia2 3 x" -- "= [x,x,x]"		value "copia2 3 x" -- "= [x,x,x]"
		+
		+	-- "jaisalmen"
		+	fun copia3 :: "nat ⇒ 'a ⇒ 'a list" where
		+	"copia3 0 x = []"
		+	\| "copia3 n x = x # (copia3 (n- 1) x)"
		+
		+	value "copia3 3 x" -- "= [x,x,x]"

	text {* ---------------------------------------------------------------		text {* ---------------------------------------------------------------