Enrique Sarrión:

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

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 {*
---------------------------------------------------------------------
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".
---------------------------------------------------------------------
*}

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

end
</source>

2011-02-14T18:34:58Z

Enrique Sarrión:

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

theory Relacion_4
imports Main
begin

section {* Sustitución, inversión y eliminación *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list"
tal que (sust x y zs) es la lista obtenida sustituyendo cada
occurrencia de x por y en la lista zs. Por ejemplo,
sust (1::nat) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]
---------------------------------------------------------------------
*}

primrec sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"sust x y [] = []"
| "sust x y (w#zs) = (if w=x then y#(sust x y zs) else w#(sust x y zs))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
---------------------------------------------------------------------
*}

--Usando la sentencia refute puede obtenerse un contraejemplo fácilmente.
Además, al ejecutarse con la aplicación, ya directamente propone un contraejemplo.

-- "La demostración automática es"
lemma sust_append_auto:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
refute
oops

-- "La demostración estructurada es"
lemma sust_append:
"sust x y (xs @ ys) = (sust x y xs)@(sust x y ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
rev (sust x y zs) = sust x y (rev zs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "rev(sust x y zs) = sust x y (rev zs)"
refute
oops

-- "La demostración estructurada es"
theorem rev_sust:
"rev (sust x y zs) = sust x y (rev zs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
sust x y (sust u v zs) = sust u v (sust x y zs)
---------------------------------------------------------------------
*}

theorem "sust x y (sust u v zs) = sust u v (sust x y zs)"
refute
oops

text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar:
sust y z (sust x y zs) = sust x z zs
---------------------------------------------------------------------
*}

theorem "sust y z (sust x y zs) = sust x z zs"
refute
oops

text {*
---------------------------------------------------------------------
Ejercicio 6. Definir la función
borra :: "'a ⇒ 'a list ⇒ 'a list"
tal que (borra x ys) es la lista obtenida borrando la primera
ocurrencia del elemento x en la lista ys. Por ejemplo,
borra (2::nat) [1,2,3,2] = [1,3,2]

Nota: La función borra es equivalente a la predefinida remove1.
---------------------------------------------------------------------
*}

primrec borra :: "'a ⇒ 'a list ⇒ 'a list" where
"borra x [] = []"
| "borra x (w#ys) = (if x=w then ys else (w#(borra x ys)))"

text {*
---------------------------------------------------------------------
Ejercicio 7. Definir la función
borraTodas :: "'a ⇒ 'a list ⇒ 'a list"
tal que (borraTodas x ys) es la lista obtenida borrando todas las
ocurrencias del elemento x en la lista ys. Por ejemplo,
borraTodas (2::nat) [1,2,3,2] = [1,3]
---------------------------------------------------------------------
*}

primrec borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
"borraTodas x [] = []"
| "borraTodas x (w#ys) = (if x=w then (borraTodas x ys) else (w#(borraTodas x ys)))"

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
borra x (borraTodas x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borra x (borraTodas x xs) = borraTodas x xs"
refute
oops

-- "La demostración estructurada es"
theorem "borra x (borraTodas x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar:
borraTodas x (borraTodas x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borraTodas x xs) = borraTodas x xs"
refute
oops

-- "La demostración estructurada es"
theorem "borraTodas x (borraTodas x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar:
borraTodas x (borra x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borra x xs) = borraTodas x xs"
oops

-- "La demostración estructurada es"
theorem borraTodas_borra:
"borraTodas x (borra x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar o refutar:
borra x (borra y xs) = borra y (borra x xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borra x (borra y xs) = borra y (borra x xs)"
oops

-- "La demostración estructurada es"
theorem "borra x (borra y xs) = borra y (borra x xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar el teorema:
borraTodas x (borra y xs) = borra y (borraTodas x xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
oops

-- "La demostración estructurada es"
theorem "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar:
borra y (sust x y xs) = borra x xs
---------------------------------------------------------------------
*}

theorem "borra y (sust x y xs) = borra x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar:
borraTodas y (sust x y xs) = borraTodas x xs"
---------------------------------------------------------------------
*}

theorem "borraTodas y (sust x y xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar:
sust x y (borraTodas x zs) = borraTodas x zs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "sust x y (borraTodas x zs) = borraTodas x zs"
oops

-- "La demostración estructurada es"
theorem sust_borraTodas:
"sust x y (borraTodas x zs) = borraTodas x zs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar:
sust x y (borraTodas z zs) = borraTodas z (sust x y zs)
---------------------------------------------------------------------
*}

theorem "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar:
rev (borra x xs) = borra x (rev xs)
---------------------------------------------------------------------
*}

theorem "rev (borra x xs) = borra x (rev xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18. Demostrar o refutar el teorema:
borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
oops

-- "La demostración estructurada es"
lemma borraTodas_append:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar o refutar el teorema:
rev (borraTodas x xs) = borraTodas x (rev xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

-- "La demostración estructurada es"
theorem "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

end
</source>

Relación 2

2011-02-14T18:03:52Z

Enrique Sarrión:

Relación 2

2011-02-14T17:57:25Z

Enrique Sarrión:

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

theory Relacion_2
imports Main
begin

text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional y de la lógica
de predicados (allI, allE, exI y exE).
*}

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof (rule impI)
assume 1: "∃x. ∀y. P x y"
show "∀y. ∃x. P x y"
proof (rule allI)
from 1 obtain "x" where 2: "∀y. P x y" by (rule exE)
fix y
from 2 have 3: "P x y" by (rule allE)
from 3 show 4: "∃x. P x y" by (rule exI)
qed
qed

lemma "(∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"
proof
{ assume 1: "∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have "P a ⟶ Q" using 1 by (rule allE)
thus "Q" using `P a` by (rule mp)
qed }
next
{ assume 2: "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof
fix a
show "P a ⟶ Q"
proof
assume "P a"
hence 3: "∃x. P x" by (rule exI)
from 2 and 3 show "Q" by (rule mp)
qed
qed }
qed

lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
proof
{ assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
show "(∀ x. (P x ∧ Q x))"
proof (rule allI)
from 1 have 2: "(∀ x. P x)" by (rule conjE)
from 1 have 3: "(∀ x. Q x)" by (rule conjE)
fix a
from 2 have 4: "P a" by (rule allE)
from 3 have 5: "Q a" by (rule allE)
from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
qed }
next
{ assume 7: "∀ x. (P x ∧ Q x)"
show "(∀ x. P x) ∧ (∀ x. Q x)"
proof
{ show "(∀ x. P x)"
proof (rule allI)
fix a
from 7 have 8: "P a ∧ Q a" by (rule allE)
from 8 show "P a" by (rule conjE)
qed }

{ show "(∀ x. Q x)"
proof (rule allI)
fix a
from 7 have 9: "P a ∧ Q a" by (rule allE)
from 9 show "Q a" by (rule conjE)
qed }
qed }
qed

lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
oops
-- "Esta fórmula de la lógica de predicados es falsa.
La implicación de izquierda a derecha sí es cierta
y a continuación la probamos:"
lemma "((∀ x. P x) ∨ (∀ x. Q x)) ⟶ (∀ x. (P x ∨ Q x))"
proof (rule impI)
assume 1: "(∀ x. P x) ∨ (∀ x. Q x)"
show "∀ x. (P x ∨ Q x)"
proof (rule allI)
fix x
note 1
moreover{
assume 11: "∀ x. P x"
from 11 have 111: "P x" by (rule allE)
from 111 have "P x ∨ Q x" by (rule disjI1)}
moreover{
assume 12: "∀ x. Q x"
from 12 have 121: "Q x" by (rule allE)
from 121 have "P x ∨ Q x" by (rule disjI2)}
ultimately show "(P x ∨ Q x)" by (rule disjE)
qed
qed

-- "La implicación de derecha a izquierda es falsa
y a continuación construimos un contraejemplo.
Supongamos un modelo en el que fuese verdadera:
(∀ x. (P x ∨ Q x)) ∧ (∃x. ¬P x ) ∧ (∃x. ¬Q x),
lo cual equivale a
(∀ x. (P x ∨ Q x)) ∧ ¬(∀ x. P x ) ∧ ¬(∀ x. Q x)
y esto es contradictorio con
(∀ x. P x) ∨ (∀ x. Q x). Un ejemplo en lenguaje
natural que ilustra esto es el siguiente:todos
los números reales son algebraicos o trascendentes,
pero de ello no podemos concluir que o bien todos
los números reales son algebraicos o bien todos los
números reales son trascendentes."

lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
proof
{assume 1:"((∃ x. P x) ∨ (∃ x. Q x))"
show "(∃ x. (P x ∨ Q x))"
proof -
note 1
moreover
{ assume 2: "(∃ x. P x)"
obtain a where 3: "P a" using 2 by (rule exE)
from 3 have 4: "P a ∨ Q a" ..
from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
moreover
{ assume 2: "(∃ x. Q x)"
obtain a where 3: "Q a" using 2 by (rule exE)
from 3 have 4: "P a ∨ Q a" ..
from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
ultimately show "(∃ x. (P x ∨ Q x))" by (rule disjE)
qed}
next
{assume 1:"(∃ x. (P x ∨ Q x))"
obtain a where 2: "P a ∨ Q a" using 1 by (rule exE)
show "((∃ x. P x) ∨ (∃ x. Q x))" using 2
proof
{ assume 3: "P a"
from 3 have 4: "(∃ x. P x)" by (rule exI)
from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
{ assume 3: "Q a"
from 3 have 4: "(∃ x. Q x)" by (rule exI)
from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
qed }
qed

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
-- "Esta fórmula de la lógica de predicados es falsa
y a continuación construimos un contraejemplo.
Supongamos un modelo en el que fuese verdadera:
(∀x. ∃y. P x y) ∧ (∀x. (P x x)) ∧ (∀x. ∀y. ((¬( x = y)) ⟶ ¬(P y x))) ∧
∧ (∃x. ∃y. (¬(x = y)))
y esto es contradictorio con (∃y. ∀x. P x y).
Si interpretamos P como <<tener exactamente los
mismos padres y los mismos hermanos que>> es obvio
que la implicación es falsa. Un contraejemplo más
conocido que se obtiene interpretando P como la
relación <<menor o igual que>> sobre los números
reales, de modo que el antecedente indicaría que
dichos números no están acotados superiormente,
mientras que el consecuente indicaría que el
conjunto de los reales tiene al menos una cota superior."

-- "La forma más corta y más automática es la que sigue"
lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
by auto

-- "RELACIÓN DE EJERCICIOS COMPLETADA"
end
</source>