Discusión:Relación 2 - Historial de revisiones

Jalonso: /* Pregunta de Wilmorort */

2016-11-06T07:08:17Z

‎Pregunta de Wilmorort

Manmorjim1 en 17:32 5 nov 2016

2016-11-05T17:32:56Z

Jalonso en 16:39 4 nov 2016

2016-11-04T16:39:25Z

Wilmorort en 08:08 4 nov 2016

2016-11-04T08:08:38Z

Wilmorort en 08:07 4 nov 2016

2016-11-04T08:07:12Z

Wilmorort en 08:06 4 nov 2016

2016-11-04T08:06:00Z

Wilmorort en 08:04 4 nov 2016

2016-11-04T08:04:33Z

Wilmorort en 08:03 4 nov 2016

2016-11-04T08:03:47Z

Wilmorort: Página creada con ' chapter {* R2: Razonamiento sobre programas en Isabelle/HOL } theory R2 imports Main begin declare names_short text { ---------------------------...'

2016-11-04T07:59:51Z

Página creada con ' <source lang="isar"> chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *} theory R2 imports Main begin declare names_short text {* ---------------------------...'

Página nueva

<source lang="isar">
chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
imports Main
begin

declare [[names_short]]

text {* ---------------------------------------------------------------
Ejercicio 1.1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

(*Notar: Por la propiedad de Gauss se puede deducir que:
la suma de los n numeros impares es igual a la suma de los
n y n-1 numeros consecutivos*)
fun suma :: "nat ⇒ nat" where
"suma 0 = 0"|
"suma n = n + suma(n-1)"

fun sumaImpares1 :: "nat ⇒ nat" where
"sumaImpares1 0 = 0" |
"sumaImpares1 n = suma(n) + suma(n-1)"

value "sumaImpares1 3 = 9 "

lemma aux1 : "suma(Suc n) + suma(n) = (n+1) + suma(n) + n + suma(n-1)"
apply (induct n)
apply auto
done

lemma aux2: "(n+1) + suma(n) + n + suma(n-1) = (n+1) + n + sumaImpares1 n "
apply (induct n)
apply auto
done

text {* ---------------------------------------------------------------
Ejercicio 1.2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

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

lemma "sumaImpares1 n = n*n"
proof (induct n)
show "sumaImpares1 0 = 0*0" by simp
next
fix n
assume HI:"sumaImpares1 n = n*n"
have "sumaImpares1 (Suc n) = suma(Suc n) + suma(n)" by simp
have "suma(Suc n) + suma(n) = (n+1) + suma(n) + n + suma(n-1)" using
"aux1" by simp
also have "... = (n+1) + n + sumaImpares1 n " using "aux2" by simp
also have "... = 2*n +1 + n*n" using HI by simp
also have "... = (n+1)*(n+1)" by simp
finally show "sumaImpares1 (Suc n) = Suc n * Suc n" by simp
qed

end
</source>

@@ Línea 51: / Línea 51: @@
    y se tiene que hacer una demostración detallada ???
    ------------------------------------------------------------------- *}
 text {* ---------------------------------------------------------------
    Creo que no funcionaba porque al usar una funcion auxiliar en tu definicion
-   de sumaImpares te queda por demostrar la propiedad de esa funcion. Es decir, si aplicas
+   de sumaImpares te queda por demostrar la propiedad de esa funcion. Es decir,
-  induccion en "n+1" te quedaría por demostrar:
+  si aplicas induccion en "n+1" te quedaría por demostrar:
-  (n+1)+(suma n)+(suma n) = (n+1)(n+1)
+     (n+1)+(suma n)+(suma n) = (n+1)(n+1)
-  (suma n) + (suma n) = n*n + n
+     (suma n) + (suma n) = n*n + n
-   Asi que lo he demostrado anteriormente y he usado ese teorema en la demostracion
+   Asi que lo he demostrado anteriormente y he usado ese teorema en la
+  demostracion
    ------------------------------------------------------------------- *}
 lemma sumAux: "(suma n) + (suma n) = n + n * n"
 apply (induct n)

@@ Línea 51: / Línea 51: @@
    y se tiene que hacer una demostración detallada ???
    ------------------------------------------------------------------- *}
 (*----------------------ERROR ----------------------------------------*)
-lemma "summaImpares1 n = n*n"
+lemma "sumaImpares1 n = n*n"
 apply (induct n)
-apply auto  (*Error*)
+apply auto
 (*--------------------------------------------------------------------*)

← Revisión anterior		Revisión del 16:39 4 nov 2016
Línea 1:		Línea 1:
		+	== Pregunta de Wilmorort ==
		+
	<source lang="isar">		<source lang="isar">
	chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}		chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}

@@ Línea 49: / Línea 49: @@
    y se tiene que hacer una demostración detallada ???
    ------------------------------------------------------------------- *}
-−
 lemma "summaImpares1 n = n*n"
 apply (induct n)
 apply auto  (*Error*)
+(*--------------------------------------------------------------------*)
 lemma "sumaImpares1 n = n*n"

@@ Línea 46: / Línea 46: @@
    ------------------------------------------------------------------- *}
 text {* ---------------------------------------------------------------
-   Por que no funciona demostrar con el siguiente algoritmo y se tiene
+   Por que no funciona demostrar con el siguiente algoritmo by(induct n) auto
-      que hacer una demostracion detallada ???
+  y se tiene que hacer una demostración detallada ???
    ------------------------------------------------------------------- *}

@@ Línea 1: / Línea 1: @@
 <source lang="isar">
 chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}
@@ Línea 47: / Línea 46: @@
    ------------------------------------------------------------------- *}
-text {* ---------------------------------------------------------------*}
+text {* ---------------------------------------------------------------
+  '''Por que no funciona demostrar con el siguiente algoritmo y se tiene
 lemma "sumaImpares1 n = n*n"