Relación 1 - Historial de revisiones

Pedrosrei en 15:23 19 feb 2013

2013-02-19T15:23:26Z

Mostrar los cambios

Pedrosrei en 16:08 17 feb 2013

2013-02-17T16:08:48Z

Pedrosrei en 16:07 17 feb 2013

2013-02-17T16:07:42Z

Jalonso en 16:56 28 nov 2012

2012-11-28T16:56:32Z

Jalonso: Página creada con ' header {* Definición de funciones } theory Definicion_de_funciones imports Main begin text { ---------------------------------------------------------...'

2012-11-27T16:12:56Z

Página creada con '<source lang="isar"> header {* Definición de funciones *} theory Definicion_de_funciones imports Main begin text {* ---------------------------------------------------------...'

Página nueva

<source lang="isar">
header {* Definición de funciones *}

theory Definicion_de_funciones
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

@@ Línea 42: / Línea 42: @@
 fun inversa :: "'a list ⇒ 'a list" where
    "inversa [] = []"
-  |"inversa (x#xs) = conc (inversa xs) [x]
+  |"inversa (x#xs) = conc (inversa xs) [x]"
 value "inversa [a,d,c]" -- "= [c,d,a]"
@@ Línea 71: / Línea 71: @@
    "conc [] ys = ys"
   |"conc xs [] = xs"
-  |"conc (x#xs) ys = (x#(conc xs ys))
+  |"conc (x#xs) ys = (x#(conc xs ys))"
 value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
@@ Línea 85: / Línea 85: @@
    "coge 0 xs = []"
   |"coge _ [] = []"
-  |"coge (Suc n) (x#xd) = conc [x] (coge n xs)
+  |"coge (Suc n) (x#xd) = conc [x] (coge n xs)"
 value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
@@ Línea 108: / Línea 108: @@
       esVacia :: 'a list ⇒ bool
    tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
-     esVacia []  = True
+    esVacia []  = True
-     esVacia [1] = False
+    esVacia [1] = False
    ------------------------------------------------------------------ *}

@@ Línea 14: / Línea 14: @@
 fun longitud :: "'a list ⇒ nat" where
-   "longitud xs = undefined"
+   "longitud [] = 0"
 value "longitud [4,2,5]" -- "= 3"
@@ Línea 27: / Línea 28: @@
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
-   "intercambia (x,y) = undefined"
+   "intercambia (x,y) = (y,x)"
 value "intercambia (u,v)" -- "= (v,u)"
@@ Línea 40: / Línea 41: @@
 fun inversa :: "'a list ⇒ 'a list" where
-   "inversa xs = undefined"
+   "inversa [] = []"
 value "inversa [a,d,c]" -- "= [c,d,a]"
@@ Línea 53: / Línea 55: @@
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
-  "repite n x = undefined"
+    "repite 0 x = []"
 value "repite 3 a" -- "= [a,a,a]"
@@ Línea 66: / Línea 69: @@
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
-   "conc xs ys = undefined"
+   "conc [] ys = ys"
+ |"conc xs [] = xs"
 value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
@@ Línea 79: / Línea 83: @@
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
-   "coge n xs = undefined"
+   "coge 0 xs = []"
 value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
@@ Línea 92: / Línea 98: @@
 fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
-   "elimina n xs = undefined"
+   "elimina 0 xs = xs"
 value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"
@@ Línea 105: / Línea 113: @@
 fun esVacia :: "'a list ⇒ bool" where
-   "esVacia xs = undefined"
+   "esVacia [] = True"
 value "esVacia []"  -- "= True"
@@ Línea 119: / Línea 128: @@
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
-   "inversaAcAux xs ys = undefined"
+   "inversaAcAux xs [] = xs"
 fun inversaAc :: "'a list ⇒ 'a list" where
-   "inversaAc xs = undefined"
+   "inversaAc xs = inversaAcAux [] xs"
 value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"
@@ Línea 134: / Línea 144: @@
 fun sum :: "nat list ⇒ nat" where
-   "sum xs = undefined"
+   "sum [] = 0"
 value "sum [3,2,5]" -- "= 10"
@@ Línea 147: / Línea 158: @@
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
-   "map f xs = undefined"
+   "map f [] = []"
 value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"