Relación 1 - Historial de revisiones

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

2018-09-09T08:08:55Z

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

Pedrosrei en 15:01 6 nov 2014

2014-11-06T15:01:20Z

Jalonso en 05:45 6 nov 2014

2014-11-06T05:45:13Z

Jalonso en 05:40 6 nov 2014

2014-11-06T05:40:17Z

Mostrar los cambios

Pedrosrei en 17:52 5 nov 2014

2014-11-05T17:52:54Z

Pedrosrei en 17:32 5 nov 2014

2014-11-05T17:32:43Z

Davoremar en 20:21 4 nov 2014

2014-11-04T20:21:04Z

Juacorvic en 11:06 4 nov 2014

2014-11-04T11:06:13Z

Juacorvic en 10:59 4 nov 2014

2014-11-04T10:59:44Z

Juacorvic en 10:56 4 nov 2014

2014-11-04T10:56:53Z

← Revisión anterior		Revisión del 08:08 9 sep 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R1: Programación funcional en Isabelle *}		header {* R1: Programación funcional en Isabelle *}

@@ Línea 236: / Línea 236: @@
 value "elimina 7 [a,c,d,b,e]" -- "= []"
-(* Comentario:
+(* Pedrosrei:
    Bien al eliminar un caso. Es preferible usar (Suc n) a n-1 para evitar
    problemas de tipo en demostraciones futuras. *)
@@ Línea 290: / Línea 290: @@
 value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"
-(* Comentario:
+(* Pedrosrei:
    Navaja de Ockham de nuevo, será muy útil cuando empiecen las
    demostraciones sobre las funciones. *)
@@ Línea 318: / Línea 318: @@
 value "sum [3,2,5] = 10"
-(* Comentario:
+(* Pedrosrei:
    Esta definición aprovecha una batería enorme de resultados que
    Isabelle posee sobre la suma (op +) al emplear foldr y ser
@@ Línea 351: / Línea 351: @@
 value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]"
-(* Mismo comentario.
+(* Pedrosrei: Mismo comentario.
    Añado 2 tras la función para evitar errores de carga. *)

@@ Línea 49: / Línea 49: @@
 (* Pedrosrei a juacorvic:
-    Resulta innecesario recurrir a la función cola si se puede definir de  la misma forma con el constructor (#) *)
+    Resulta innecesario recurrir a la función cola si se puede definir de
 text {* ---------------------------------------------------------------
@@ Línea 95: / Línea 96: @@
 (* Pedrosrei: Es preferible recurrir al menor número posible de
-   funciones auxiliares cuando más adelante sea necesario probar proposiciones sobre las funciones que definimos. Añado ahora un ejemplo de esto mismo:
+   funciones auxiliares cuando más adelante sea necesario probar
-   Si queremos definir mejor (más estrictamente) la función, tendremos que recurrir a los comandos primrec o function en estos casos, la importancia de simplificar la definición mediante el empleo de constructores definidos en lugar de funciones es crucial. Por poner el ejemplo de esta función:
+   Si queremos definir mejor (más estrictamente) la función, tendremos
      function inversa4 :: "'a list ⇒ 'a list" where
@@ Línea 105: / Línea 112: @@
      termination by size_change
-   en cambio, si nos trasladamos a las versiones 2 y 3 la prueba de la     totalidad no es trivial y requeriría un gasto de tiempo inútil. *)
+   en cambio, si nos trasladamos a las versiones 2 y 3 la prueba de la
 text {* ---------------------------------------------------------------
@@ Línea 130: / Línea 139: @@
 (* Pedrosrei:
-   Esta definición posee un error, el caso segundo debe tener  el mismo nombre que el primero y operar, de lo contrario usa otras funciones ajenas. *)
+   Esta definición posee un error, el caso segundo debe tener
 -- "davoremar"
@@ Línea 204: / Línea 215: @@
 (* Pedrosrei:
-   Además de por las razones dadas en funciones anteriores, es preferible la primera definición de la misma al eliminar salidas de error cuando n es mayor al tamaño de la lista *)
+   Además de por las razones dadas en funciones anteriores, es preferible
 text {* ---------------------------------------------------------------
@@ Línea 224: / Línea 237: @@
 (* Comentario:
-   Bien al eliminar un caso. Es preferible usar (Suc n) a n-1 para evitar problemas de tipo en demostraciones futuras. *)
+   Bien al eliminar un caso. Es preferible usar (Suc n) a n-1 para evitar
 -- "juacorvic"
@@ Línea 277: / Línea 291: @@
 (* Comentario:
-   Navaja de Ockham de nuevo, será muy útil cuando empiecen las demostraciones sobre las funciones. *)
+   Navaja de Ockham de nuevo, será muy útil cuando empiecen las
    -- "juacorvic"
@@ Línea 304: / Línea 319: @@
 (* Comentario:
-   Esta definición aprovecha una batería enorme de resultados que Isabelle posee sobre la suma (op +) al emplear foldr y ser reconocible para el sistema *)
+   Esta definición aprovecha una batería enorme de resultados que
 -- "jeshorcob"

@@ Línea 129: / Línea 129: @@
 value "repite2 3 a" -- "= [a,a,a]"
 -- "davoremar"
 fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 158: / Línea 160: @@
 | "conc3 xs ys =  (hd xs)#(conc3 (tl xs) ys)"
 -- "davoremar"
 fun conc4 :: "'a list ⇒ 'a list ⇒ 'a list" where
@@ Línea 173: / Línea 176: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob,javrodviv1","danrodcha", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab,davoremar"
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge _ [] = []"
@@ Línea 184: / Línea 187: @@
 |  "coge2 n xs = (hd xs) # coge2 (n - 1) (tl xs)"
 value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
@@ Línea 195: / Línea 200: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab,davoremar"
 fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina _ [] = []"
@@ Línea 201: / Línea 206: @@
   |"elimina (Suc m) (x#xs) = elimina m xs"
+-- "Bien al eliminar un caso. Es preferible usar (Suc n) a n-1 para evitar problemas de tipo en demostraciones futuras."
 -- "juacorvic"
 fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
@@ Línea 217: / Línea 222: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,carvelcab,davoremar"
 fun esVacia :: "'a list ⇒ bool" where
    "esVacia [] = True"
@@ Línea 238: / Línea 243: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","danrodcha", "davoremar"
+-- "jeshorcob,danrodcha,davoremar"
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux [] ys = ys"
   |"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"
--- "jeshorcob","danrodcha", "davoremar"
+-- "jeshorcob,danrodcha,davoremar"
 fun inversaAc :: "'a list ⇒ 'a list" where
    "inversaAc xs = inversaAcAux xs []"
 -- "juacorvic"
 fun inversaAcAux2 :: "'a list ⇒ 'a list ⇒ 'a list" where
@@ Línea 253: / Línea 259: @@
 fun inversaAc2 :: "'a list ⇒ 'a list" where
    "inversaAc2 xs = inversaAcAux2 xs []"
@@ Línea 264: / Línea 271: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab,davoremar"
 fun sum :: "nat list ⇒ nat" where
    "sum [] = 0"
   |"sum (x#xs) = x + sum xs"
 -- "jeshorcob"
 fun sum2 :: "nat list ⇒ nat" where
@@ Línea 288: / Línea 297: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab,davoremar"
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map f [] = []"
   |"map f (x#xs) = (f x)#(map f xs)"
 -- "juacorvic"
-fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
+fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
-    "map f [] =  []"
+    "map2 f [] =  []"
-|  "map f xs = (f (hd xs)) # (map f (tl xs))"
+|  "map2 f xs = (f (hd xs)) # (map2 f (tl xs))"

@@ Línea 35: / Línea 35: @@
    ------------------------------------------------------------------- *}
--- "jeshorcob","javrodviv1","danrodcha", "juacorvic", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1,danrodcha, juacorvic, carvelcab, davoremar"
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0"
@@ Línea 47: / Línea 47: @@
 | "longitud2 xs = 1 + longitud2 (tl (xs))"
 value "longitud2 [4,2,5]" -- "= 3"
@@ Línea 58: / Línea 62: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "juacorvic", "davoremar"
+-- "jeshorcob, javrodviv1, danrodcha, carvelcab, juacorvic, davoremar"
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 87: / Línea 91: @@
   | "inversa3 xs =  inversa3(tl xs)@ (hd xs#[])"
 value "inversa [a,d,c]" -- "= [c,d,a]"
@@ Línea 98: / Línea 115: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "juacorvic"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab,juacorvic"
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = []"
@@ Línea 127: / Línea 144: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "juacorvic"
+-- "jeshorcob,javrodviv1,danrodcha,carvelcab, juacorvic"
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc [] ys = ys"
@@ Línea 156: / Línea 173: @@
    ------------------------------------------------------------------ *}
--- "jeshorcob","javrodviv1","danrodcha", "carvelcab", "davoremar"
+-- "jeshorcob,javrodviv1","danrodcha", "carvelcab", "davoremar"
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge _ [] = []"

@@ Línea 243: / Línea 243: @@
 fun sum2 :: "nat list ⇒ nat" where
    "sum2 xs = foldr (op +) xs 0"
 value "sum [3,2,5]" -- "= 10"