Relación 6

2016-12-04T08:41:56Z

Crigomgom:

Relación 6

2016-12-03T11:30:22Z

Crigomgom:

2016-11-25T10:45:56Z

Crigomgom:

Relación 4

2016-11-23T09:46:38Z

Relación 3

2016-11-12T09:04:29Z

Crigomgom:

<source lang="isar">
chapter {* R3: Razonamiento sobre programas *}

theory R3_Razonamiento_sobre_programas
imports Main
begin

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
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"

text {* ---------------------------------------------------------------
Ejercicio 1.2. Escribir la demostración detallada de
sumaImpares n = n*n
------------------------------------------------------------------- *}

-- "La demostración detallada es"
(* crigomgom fraortmoy marpoldia1 ivamenjim *)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0 * 0" by simp
next
fix n
assume HI: "sumaImpares n = n * n"
have "sumaImpares (Suc n) = sumaImpares n + 2*n + 1" by simp
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = Suc n * Suc n" by simp
finally show "sumaImpares (Suc n) = Suc n * Suc n" by simp
qed

(*danrodcha ; es la misma demostración que la anterior pero uso ?P para sustituir la propiedad.*)
lemma "sumaImpares n = n*n" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n
assume HI: "?P n"
have "sumaImpares (Suc n) = sumaImpares n + 2*n + 1" by simp
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = Suc n * Suc n" by simp
finally show "?P (Suc n)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 2.1. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 2"
| "sumaPotenciasDeDosMasUno (Suc n) =
sumaPotenciasDeDosMasUno n + 2^(n+1)"

text {* ---------------------------------------------------------------
Ejercicio 2.2. Escribir la demostración detallada de
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

(*crigomgom ivamenjim danrodcha*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2 ^ (0 + 1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2 ^ (n + 1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp
also have "... = 2 ^ (n + 1) + 2 ^ (n + 1)" using HI by simp
also have "... = 2 ^ ((Suc n) + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp
qed

(* fraortmoy *)
(* es la misma demostración, pero quise probar a delimitar lo que se usa en el "by simp" *)

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2 ^ (0 + 1)" by simp
next
fix n
assume H1:" sumaPotenciasDeDosMasUno n = 2 ^ (n + 1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n + 1)" by (simp only : sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2 ^ (n + 1) + 2 ^ (n + 1)" using H1 by simp
also have "... = 2 ^ (Suc n + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp
qed

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

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []"
| "copia (Suc n) x = x # copia n x"

text {* ---------------------------------------------------------------
Ejercicio 3.2. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
------------------------------------------------------------------ *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

text {* ---------------------------------------------------------------
Ejercicio 3.2. Demostrar detalladamente que todos los elementos de
(copia n x) son iguales a x.
------------------------------------------------------------------- *}

(* crigomgom *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y = x) (copia 0 x)" by simp
next
fix n
assume HI: "todos (λy. y = x) (copia n x)"
have "todos (λy. y = x) (copia (Suc n) x) = todos (λy. y = x) (x # (copia n x))" by simp
also have "... = ((x = x) ∧ (todos (λy. y = x) (copia n x)))" by simp
also have "... = True" using HI by simp
finally show "todos (λy. y = x) (copia (Suc n) x)" by simp
qed

(* fraortmoy *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
have "todos (λy. y = x) (copia 0 x) = todos (λy. y = x) []" by (simp only: copia.simps(1))
also have "... = True" by (simp only: todos.simps(1))
show "todos (λy. y = x) (copia 0 x)" by simp
next
fix n
assume H1 : " todos (λy. y = x) (copia n x) "
have "todos (λy. y = x) (copia (Suc n) x) = ((todos (λy. y = x) (x#[])) ∧ (todos (λy. y = x) (copia n x) )) " by simp
also have " ... = (todos (λy. y = x) (x#[]))" using H1 by simp
also have " ... = ((λy. y = x) x ∧ todos (λy. y = x) [])" by simp
also have " ... = True" by simp
finally show " todos (λy. y = x) (copia (Suc n) x)" by simp
qed

(*danrodcha*)
lemma "todos (λy. y=x) (copia n x)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n
assume HI: "?P n"
have "todos (λy. y=x) (copia (Suc n) x) = todos (λy. y=x) (x # copia n x)" by simp
also have "... = ((λy. y=x) x ∧ todos (λy. y=x) (copia n x))" by simp
also have "... = todos (λy. y=x) (copia n x)" by simp
finally show "?P (Suc n)" using HI by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 4.1. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"

text {* ---------------------------------------------------------------
Ejercicio 4.2. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
Indicación: La propiedad mult_Suc es
(Suc m) * n = n + m * n
Puede que se necesite desactivarla en un paso con
(simp del: mult_Suc)
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (x * Suc n)"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

(* fraortmoy , danrodcha*)
lemma fact: "factI' n x = x * factR n"
proof (induct n)
show "factI' 0 x = x * factR 0" by simp
next
fix n
assume H1 : "factI' n x = x * factR n"
have "factI' (Suc n) x = factI' n (x * Suc n)" by (simp only:factI'.simps(2))
also have "... = (x * Suc n) * factR n" using H1 by simp (* no entiendo por qué no hace esto bien y luego todo funciona *)
also have "... = x * factR (Suc n)" by (simp del: mult_Suc)
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed

(* crigomgom *)
lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "⋀x. factI' n x = x * factR n"
show "⋀x. factI' (Suc n) x = x * factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
also have "... = (x * Suc n) * factR n" using HI by simp
also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc)
also have "... = x * factR (Suc n)" by simp
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 4.3. Escribir la demostración detallada de
factI n = factR n
------------------------------------------------------------------- *}

(* fraortmoy danrodcha *)
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1" by simp
also have "... = 1 * factR n" by (simp add: fact)
finally show "factI n = factR n" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 5.1. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]"
| "amplia (x#xs) y = x # amplia xs y"

text {* ---------------------------------------------------------------
Ejercicio 5.2. Escribir la demostración detallada de
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

(* crigomgom fraortmoy *)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x # xs) y = x # (amplia xs y)" by simp
also have "... = x # (xs @ [y])" using HI by simp
also have "... = (x # xs) @ [y]" by simp
finally show "amplia (x # xs) y = (x # xs) @ [y]" by simp
qed

(*danrodcha*)
lemma "amplia xs y = xs @ [y]" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
have "amplia (x # xs) y = x # amplia xs y" by simp
also have "... = (x # xs) @ [y]" using HI by simp
finally show "?P (x#xs)" by simp
qed

end
</source>

2016-10-29T10:39:32Z

Crigomgom:

<source lang="isar">
chapter {* R1: Programación funcional en Isabelle *}

theory R1
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 0. Definir, por recursión, la función
factorial :: nat ⇒ nat
tal que (factorial n) es el factorial de n. Por ejemplo,
factorial 4 = 24
------------------------------------------------------------------- *}

(* danrodcha, anaprarod, ivamenjim, serrodcal*)
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1"
| "factorial (Suc n) = (Suc n) * factorial n"

(*wilmorort, pablucoto,marcarmor13, crigomgom*)
fun factorial1 :: "nat ⇒ nat" where
"factorial1 0 = 1 "
| "factorial1 n = n * factorial1(n-1)"

value "factorial 4" -- "24"

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
------------------------------------------------------------------- *}

(*wilmorort*)
(* Para usar las lista en forma de [a,b,c] *)

translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"

(*wilmorort, serrodcal,crigomgom*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0" |
"longitud (x # xs) = 1 + longitud xs "

(*pablucoto*)
fun longitud0 :: "'a list ⇒ nat " where
" longitud0 [] = 0"
|"longitud0 xs = 1 + longitud0 ((butlast xs)) "

fun longitud0_1 :: "'a list ⇒ nat " where
"longitud0_1 xs = (if xs =[] then 0 else 1 + longitud0_1((butlast xs))) "

(*marcarmor13*)
fun longitud1 :: "'a list ⇒ nat" where
"longitud1 [] = 0 "
| "longitud1 xs = (1+ longitud2 (tl xs))"

(*danrodcha*)
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = 0"
| "longitud2 (x#xs) = Suc (longitud2 xs)"

(*serrodcal*)
fun longitud3 :: "'a list ⇒ nat" where
"longitud xs = length (xs)"

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)
------------------------------------------------------------------ *}

(*wilmorort,marcarmor13,danrodcha,crigomgom*)
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x) "

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]
------------------------------------------------------------------ *}

(*wilmorort*)
(* @ :: "'a list => 'a list => 'a list", función agregación definida
en Theory Main, concatena dos listas: [a,b] @ [c,d] = [a,b,c,d] *)
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []" |
"inversa (x # xs) = (inversa xs)@(x#[]) "

(*marcarmor13*)
fun inversa1 :: "'a list ⇒ 'a list" where
"inversa1 [] = []"
| "inversa1 xs = inversa1 (tl xs)@ ((hd xs)#[])"

(*danrodcha*)
(* es igual que inversa sustituyendo x#[] por [x] *)
fun inversa2 :: "'a list ⇒ 'a list" where
"inversa2 [] = []"
| "inversa2 (x#xs) = (inversa2 xs)@[x] "

(*danrodcha*)
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []"
| "inversa3 (x#xs) = concat [(inversa3 xs),[x]] "

(*crigomgom*)
fun inversa4 :: "'a list ⇒ 'a list" where
"inversa4 [] = []" |
"inversa4 xs = (last xs)#(inversa4(butlast xs)) "

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]
------------------------------------------------------------------ *}

(*wilmorort,marcarmor13*)
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = [] " |
"repite n x = x # (repite(n-1) x) "

(*danrodcha*)
fun repite1 :: "nat ⇒ 'a ⇒ 'a list" where
"repite1 0 x = []"
| "repite1 (Suc n) x = x#(repite1 n x)"

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]
------------------------------------------------------------------ *}

(*marcarmor13*)
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = xs@ys"

(*danrodcha*)
fun conc1 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc1 [] ys = ys"
| "conc1 xs [] = xs" (*esta no hace falta*)
| "conc1 (x#xs) ys = x#(conc1 xs ys)"

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]
------------------------------------------------------------------ *}
(*marcarmor13*)
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge 0 xs = []"
| "coge n xs = (hd xs)#(coge (n-1) (tl xs)) "

(*danrodcha*)
fun coge1 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge1 0 _ = []"
| "coge1 _ [] = []"
| "coge1 (Suc n) (x#xs) = x#(coge1 n xs)"

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]
------------------------------------------------------------------ *}
(*marcarmor13*)
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina 0 xs = xs"
| "elimina n xs = (elimina (n-1) (tl xs ))"

(*danrodcha*)
fun elimina1 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina1 0 xs = xs"
| "elimina1 _ [] = []"
| "elimina1 (Suc n) (x#xs) = elimina1 n xs"

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
------------------------------------------------------------------ *}

(*marcarmor13, rubgonmar, danrodcha*)
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True "
| "esVacia xs = False"

(*danrodcha*)
fun esVacia1 :: "'a list ⇒ bool" where
"esVacia1 xs = (xs = [])"

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]
------------------------------------------------------------------ *}

(*rubgonmar,marcarmor13*)
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux xs ys = inversaAcAux (tl xs) (hd xs#ys) "

(*danrodcha*)
fun inversaAcAux1 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux1 [] ys = ys"
| "inversaAcAux1 (x#xs) ys = inversaAcAux1 xs (x#ys)"

(*rubgonmar, danrodcha*)
fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

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
------------------------------------------------------------------ *}

(*rubgonmar,marcarmor13*)
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
|"sum xs = hd xs + sum (tl xs)"

(*danrodcha*)
fun sum1 :: "nat list ⇒ nat" where
"sum1 [] = 0"
| "sum1 (x#xs) = x + sum1 xs"

(*danrodcha*)
fun sum2 :: "nat list ⇒ nat" where
"sum2 xs = fold (op +) xs 0"

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]
------------------------------------------------------------------ *}

(*rubgonmar,marcarmor13*)
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f xs = f(hd xs)#map f (tl xs)"

(*wilmorort, danrodcha*)
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
|"map f (x # xs) = f x # map f xs" (*yo pondría paréntesis, pero sin
ellos lo entiende*)

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

end
</source>