Relación 7

2011-03-02T11:21:11Z

Jgalanp:

<source lang="isar">
header {* 7ª relación de ejercicios *}

theory Relacion_7_sol
imports Main Efficient_Nat
begin

section {* Contador de occurrencias *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
veces :: "'a ⇒ 'a list ⇒ nat"
tal que (veces x ys) es el número de occurrencias del elemento x en la
lista ys. Por ejemplo,
veces (2::nat) [2,1,2,5,2] = 3
---------------------------------------------------------------------
*}

primrec veces :: "'a ⇒ 'a list ⇒ nat" where
"veces x [] = 0"
| "veces x (y#ys) = (if x = y then 1 + veces x ys else veces x ys)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
veces a (xs @ ys) = veces a xs + veces a ys
---------------------------------------------------------------------
*}

lemma "veces a (xs @ ys) = veces a xs + veces a ys"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
veces a xs = veces a (rev xs)
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
"veces a xs ≤ length xs".
---------------------------------------------------------------------
*}

lemma "veces a xs ≤ length xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 5. Sabiendo que la función map aplica una función a todos los
elementos de una lista:
map f [x\<^isub>1,…,x\<^isub>n] = [f x\<^isub>1,…,f x\<^isub>n],
demostrar o refutar
veces a (map f xs) = veces (f a) xs
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 6. La función
filter :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
está definida por
filter P [] = []
filter P (x # xs) = (if P x then x # filter P xs else filter P xs)
Encontrar una expresión e que no contenga filter tal que se verifique
la siguiente propiedad:
veces a (filter P xs) = e
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Usando veces, definir la función
borraDups :: "'a list ⇒ bool"
tal que (borraDups xs) es la lista obtenida eliminando los elementos
duplicados de la lista xs. Por ejemplo,
borraDups [1::nat,2,4,2,3] = [1,4,2,3]

Nota: La función borraDups es equivalente a la predefinida remdups.
---------------------------------------------------------------------
*}

text {*
El tipo correspondiente al conjunto imagen de la función definida
no coincide con el indicado en la declaración de tipos del enunciado,
dado que en él aparece erróneamente la salida de tipo bool, mientras
que del resto del texto se deduce que la salida es una lista de
elementos de tipo 'a.
*}

primrec borraDups :: "'a list ⇒ 'a list" where
"borraDups [] = []"
| "borraDups (x#xs) = (if veces x xs > 0 then borraDups xs else (x#borraDups xs))"

text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "borraDups [1::nat,2,4,2,3]"
*}

text {*
---------------------------------------------------------------------
Ejercicio 8. Encontrar una expresión e que no contenga la función
borraDups tal que se verifique
veces x (borraDups xs) = e
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 9. Usando la función "veces", definir la función
distintos :: "'a list ⇒ bool"
tal que (distintos xs) se verifica si cada elemento de xs aparece tan
solo una vez. Por ejemplo,
distintos [1,4,3]
¬ distintos [1,4,1]

Nota: La función "distintos" es equivalente a la predefinida "distinct".
---------------------------------------------------------------------
*}

primrec distintos :: "'a list ⇒ bool" where
"distintos [] = True"
| "distintos (x#xs) = (if veces x xs > 0 then False else distintos xs)"

text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "distintos [1::nat,4,1]"
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el valor de "borraDups" verifica "distintos".
---------------------------------------------------------------------
*}

end
</source>

Relación 7

2011-03-02T10:40:11Z

Jgalanp:

<source lang="isar">
header {* 7ª relación de ejercicios *}

theory Relacion_7_sol
imports Main Efficient_Nat
begin

section {* Contador de occurrencias *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
veces :: "'a ⇒ 'a list ⇒ nat"
tal que (veces x ys) es el número de occurrencias del elemento x en la
lista ys. Por ejemplo,
veces (2::nat) [2,1,2,5,2] = 3
---------------------------------------------------------------------
*}

primrec veces :: "'a ⇒ 'a list ⇒ nat" where
"veces x [] = 0"
| "veces x (y#ys) = (if x = y then 1 + veces x ys else veces x ys)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
veces a (xs @ ys) = veces a xs + veces a ys
---------------------------------------------------------------------
*}

lemma "veces a (xs @ ys) = veces a xs + veces a ys"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
veces a xs = veces a (rev xs)
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
"veces a xs ≤ length xs".
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Sabiendo que la función map aplica una función a todos los
elementos de una lista:
map f [x\<^isub>1,…,x\<^isub>n] = [f x\<^isub>1,…,f x\<^isub>n],
demostrar o refutar
veces a (map f xs) = veces (f a) xs
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 6. La función
filter :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
está definida por
filter P [] = []
filter P (x # xs) = (if P x then x # filter P xs else filter P xs)
Encontrar una expresión e que no contenga filter tal que se verifique
la siguiente propiedad:
veces a (filter P xs) = e
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Usando veces, definir la función
borraDups :: "'a list ⇒ bool"
tal que (borraDups xs) es la lista obtenida eliminando los elementos
duplicados de la lista xs. Por ejemplo,
borraDups [1::nat,2,4,2,3] = [1,4,2,3]

Nota: La función borraDups es equivalente a la predefinida remdups.
---------------------------------------------------------------------
*}

text {*
El tipo correspondiente al conjunto imagen de la función definida
no coincide con el indicado en la declaración de tipos del enunciado,
dado que en él aparece erróneamente la salida de tipo bool, mientras
que del resto del texto se deduce que la salida es una lista de
elementos de tipo 'a.
*}

primrec borraDups :: "'a list ⇒ 'a list" where
"borraDups [] = []"
| "borraDups (x#xs) = (if veces x xs > 0 then borraDups xs else (x#borraDups xs))"

text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "borraDups [1::nat,2,4,2,3]"
*}

text {*
---------------------------------------------------------------------
Ejercicio 8. Encontrar una expresión e que no contenga la función
borraDups tal que se verifique
veces x (borraDups xs) = e
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 9. Usando la función "veces", definir la función
distintos :: "'a list ⇒ bool"
tal que (distintos xs) se verifica si cada elemento de xs aparece tan
solo una vez. Por ejemplo,
distintos [1,4,3]
¬ distintos [1,4,1]

Nota: La función "distintos" es equivalente a la predefinida "distinct".
---------------------------------------------------------------------
*}

primrec distintos :: "'a list ⇒ bool" where
"distintos [] = True"
| "distintos (x#xs) = (if veces x xs > 0 then False else distintos xs)"

text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "distintos [1::nat,4,1]"
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el valor de "borraDups" verifica "distintos".
---------------------------------------------------------------------
*}

end
</source>

Relación 6

2011-03-02T09:53:15Z

Jgalanp:

<source lang="isar">
header {* 6ª relación de ejercicios *}

theory Relacion_6
imports Main
begin

section {* Número de elementos válidos *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (cuentaP Q xs) es el número de elementos de la lista xs que
satisfacen el predicado Q. Por ejemplo,
cuentaP (λx. 2<x) [1,3,4,0,5] = 3
---------------------------------------------------------------------
*}

primrec cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
"cuentaP Q [] = 0"
| "cuentaP Q (x#xs) = (if Q x then 1 + cuentaP Q xs else cuentaP Q xs)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys*
---------------------------------------------------------------------
*}

text {*
Se puede demostrar tal como se indica a continuación
*}

lemma "cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys"
by (induct xs arbitrary: ys) auto

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que el número de elementos de una lista que
cumplen una determinada propiedad es el mismo que el de esa lista
invertida.
---------------------------------------------------------------------
*}

text {*
Para demostrar el resultado propuesto en este ejercicio
he necesitado formular y demostrar un lema auxiliar.
*}

lemma cuentaP_almoh_snoc: "cuentaP Q (x#xs)= cuentaP Q (snoc xs x)"(is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
thus "?P (x#xs)"
proof (cases "Q x")
case True thus "?thesis" using HI by auto
next
case False thus "?thesis" using HI by auto
qed
qed

text {*
En la demostración de este resultado, además del lema
auxiliar anterior, he debido introducir en las líneas
2 y 10 una proposición teoremática adicional sin la
cual el sistema no me aceptaba el razonamiento indicado.
*}

lemma "cuentaP Q xs = cuentaP Q (inversa xs)" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume 1: "?P xs"
thus "?P (x#xs)"
proof (cases "Q x")
case True thus "?thesis"
proof -
have 2: "snoc (inversa xs) x = (inversa xs) @ [x]" by (rule snoc_append)
from True have 3: "cuentaP Q (x#xs) = 1 + cuentaP Q xs" by auto
also have 4: "... = 1 + cuentaP Q (inversa xs)" using 1 by auto
also have 5: "... = cuentaP Q (x#(inversa xs))" using 1 and True by auto
also have 6: "... = cuentaP Q (snoc (inversa xs) x)" by (rule cuentaP_almoh_snoc)
also have 7: "... = cuentaP Q ((inversa xs) @ [x])" using 2 by auto
also have 8: "... = cuentaP Q (inversa (x#xs))" by auto
finally show 9: "cuentaP Q (x#xs) = cuentaP Q (inversa (x#xs))" by auto
qed
next
case False thus "?thesis"
proof -
have 10: "snoc (inversa xs) x = (inversa xs) @ [x]" by (rule snoc_append)
from False have 11: "cuentaP Q (x#xs) =cuentaP Q xs" by auto
also have 12: "... = cuentaP Q (inversa xs)" using 1 by auto
also have 13: "... = cuentaP Q (x#(inversa xs))" using 1 and False by auto
also have 14: "... = cuentaP Q (snoc (inversa xs) x)" by (rule cuentaP_almoh_snoc)
also have 15: "... = cuentaP Q ((inversa xs) @ [x])" using 10 by auto
also have 16: "... = cuentaP Q (inversa (x#xs))" by auto
finally show 16: "cuentaP Q (x#xs) = cuentaP Q (inversa (x#xs))" by auto
qed
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Encontrar y demostrar una relación entre las funciones
filter y cuentaP.
---------------------------------------------------------------------
*}

text {*
Relación: El número de elementos de xs que cumplen la propiedad P será el número de elementos
que contendrá la lista resultante de aplicar el filtro P sobre xs.
*}

lemma "cuentaP P xs = length (filter P xs)"
by (induct xs) auto

end
</source>

Relación 1

2011-02-01T16:52:46Z

Jgalanp:

<source lang="isar">
header {* 1ª relación de ejercicios *}

theory Relacion_1
imports Main
begin

text {*
---------------------------------------------------------------------
Demostrar los siguientes lemas usando sólo las reglas básicas de
deducción natural de la lógica proposicional.
---------------------------------------------------------------------
*}

lemma I: "A ⟶ A"
by (rule imp_refl)

lemma
assumes 1:"A ∧ B"
shows "B ∧ A"
proof -
from 1 have 2:"A" by (rule conjunct1)
from 1 have 3:"B" by (rule conjunct2)
from 3 2 show "B ∧ A" by (rule conjI)
qed

lemma "A ∧ B ⟶ A ∨ B"
proof
assume "A ∧ B"
hence "A" ..
thus "A ∨ B" ..
qed

lemma
assumes 1:"(A ∨ B) ∨ C"
shows "A ∨ ( B ∨ C)"
proof -
note 1
moreover
{ assume 2: "C"
from 2 have 3:"B ∨ C" by (rule disjI2)
from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
moreover
{ assume 4: "A ∨ B"
from 4 have "(A ∨ B) ∨ C" by (rule disjI1) }
ultimately show "A ∨ (B ∨ C) " by (simp)
qed

lemma K: "A ⟶ (B ⟶ A)"
oops
lemma "(A ⟶ (B ⟶C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
proof
assume 1:"A ⟶ (B ⟶ C)"
show "(A ⟶ B) ⟶ (A ⟶C)"
proof
assume 2:"(A ⟶ B)"
show "A ⟶C"
proof
assume 3:"A"
from 2 3 have 4:"B" by (rule mp)
from 1 3 have 5:"B ⟶ C" by (rule mp)
from 5 4 show "C" by (rule mp)
qed
qed
qed

lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
proof
assume 1:"(A ⟶ B)"
show "((B ⟶ C) ⟶ (A ⟶ C))"
proof
assume 2:"(B ⟶ C)"
show "(A ⟶ C)"
proof
assume 3:"A"
from 1 3 have 4:"B" by (rule mp)
from 2 4 show "C" by (rule mp)
qed
qed
qed

lemma "¬¬A ⟶ A"
proof
assume 1:"¬¬A"
from 1 show "A" by (rule notnotD)
qed

lemma "A ⟶ ¬¬A"
proof
assume 1:"A"
from 1 show "¬¬A" by (rule contrapos_pn)
qed

lemma MT:
assumes 1:"F ⟶ G" and 2:"¬G"
shows "¬F"
proof (rule notI)
assume 3:"F"
from 1 and 3 have 4:"G" by (rule mp)
from 2 and 4 show False by (rule notE)
qed

lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
proof
assume 1:"(¬A ⟶ B)"
show "(¬B ⟶ A)"
proof
assume 2:"¬B"
from 1 2 have 3:"¬¬A" by (rule MT)
from 3 show "A" by (rule notnotD)
qed
qed

lemma "((A ⟶ B) ⟶ A) ⟶ A"
oops

lemma "A ∨ ¬A"
oops

lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
oops

end
</source>

Relación 1

2011-02-01T16:02:07Z

Jgalanp: