Razonamiento automático (2010-11) - Contribuciones del usuario [es]

Relación 7

2011-03-04T17:32:49Z

Palmagroblanco:

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

lemma "veces a (map f xs) = veces (f a) xs"
quickcheck
oops

text{*
El contraejemplo encontrado es el siguiente:
xs = [1]
f = (λx. 0)(1 := 0, 0 := 0)
a = 0

Esto es: 0 = f(1) pero f(0) ≠ 1
*}

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

lemma "veces a (filter P xs) = (if P a then veces a xs else 0)"
by (induct xs) auto

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

lemma "veces x (borraDups xs) = (if (veces x xs) >= 1 then 1 else 0)"
by (induct xs) auto

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

lemma "(distintos xs) ⟶ ((length xs) = (length (borraDups xs)))"
by (induct xs) auto

text{*
Si xs verifica el predicado distintos, entonces el tamaño de xs debe de ser el mismo
antes y despues de borrar los duplcados.
*}

end
</source>

Relación 7

2011-03-03T17:40:25Z

Palmagroblanco:

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

lemma "veces a (map f xs) = veces (f a) xs"
quickcheck
oops

text{*
El contraejemplo encontrado es el siguiente:
xs = [1]
f = (λx. 0)(1 := 0, 0 := 0)
a = 0

Esto es: 0 = f(1) pero f(0) ≠ 1
*}

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

lemma "veces a (filter P xs) = (if P a then veces a xs else 0)"
by (induct xs) auto

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

lemma "veces x (borraDups xs) = (if (veces x xs) \<ge> 1 then 1 else 0)"
by (induct xs) auto

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

lemma "(distintos xs) ⟶ ((length xs) = (length (borraDups xs)))"
by (induct xs) auto

text{*
Si xs verifica el predicado distintos, entonces el tamaño de xs debe de ser el mismo
antes y despues de borrar los duplcados.
*}

end
</source>

Relación 3

2011-02-07T10:56:21Z

Palmagroblanco:

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

theory Relacion_3
imports Main
begin

section {* Cons inverso *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir recursivamente la función
snoc :: "'a list ⇒ 'a ⇒ 'a list"
tal que (snoc xs a) es la lista obtenida al añadir el elemento a al
final de la lista xs. Por ejemplo,
value "snoc [2,5] (3::int)" == [2,5,3]

Nota: No usar @.
---------------------------------------------------------------------
*}

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

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar el siguiente teorema
snoc xs a = xs @ [a]
---------------------------------------------------------------------
*}

-- "La demostración automática del lema es"
lemma "snoc xs a = xs @ [a]"
by (induct xs) auto

-- "La demostración estructurada del lema es"
lemma snoc_append: "snoc xs a = xs @ [a]"
oops

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar el siguiente teorema
rev (x # xs) = snoc (rev xs) x"
---------------------------------------------------------------------
*}

-- "La demostración automática del teorema es"
theorem rev_cons_auto: "rev (x # xs) = snoc (rev xs) x"
oops

-- "La demostración estructurada del teorema es"
theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
oops

section {* Cuantificadores sobre listas *}

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
todos (λx. 1<length x) [[2,1,4],[1,3]]
¬ todos (λx. 1<length x) [[2,1,4],[3]]

Nota: La función todos es equivalente a la predefinida list_all.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (algunos p xs) se verifica si algunos elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
algunos (λx. 1<length x) [[2,1,4],[3]]
¬ algunos (λx. 1<length x) [[],[3]]"

Nota: La función algunos es equivalente a la predefinida list_ex.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
oops

-- "La demostración estructurada es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar:
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
oops

-- "La demostración estructurada es"
lemma todos_append [simp]:
"todos P (x @ y) = (todos P x ∧ todos P y)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos P (rev xs) = todos P xs"
oops

-- "La demostración estructurada es"
lemma "todos P (rev xs) = todos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}

-- "Se busca un contraejemplo con nitpick"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
oops

text {*
El contraejemplo encontrado es
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar:
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (map f xs) = algunos (P ∘ f) xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar o refutar:
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

-- "La demostración estructurada es"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar:
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (rev xs) = algunos P xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 13. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
---------------------------------------------------------------------
*}

text {*
Solución: La ecuación se verifica eligiendo como Z el término
algunos P xs ∨ algunos Q xs
En efecto,
*}

lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
oops

-- "De forma estructurada"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar:
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

-- "La demostración estructurada es"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la funcion primitiva recursiva
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 16. Expresar la relación existente entre estaEn y algunos.
---------------------------------------------------------------------
*}

text {*
Solución: La relación es

En efecto,
*}

text {*
---------------------------------------------------------------------
Ejercicio 17. Definir la función primitiva recursiva
sinDuplicados :: 'a list ⇒ bool
tal que (sinDuplicados xs) se verifica si la lista xs no contiene
duplicados. Por ejemplo,
sinDuplicados [1::nat,4,2] = True
sinDuplicados [1::nat,4,2,4] = False
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 18. Definir la función primitiva recursiva
borraDuplicados :: 'a list ⇒ bool
tal que (borraDuplicados xs) es la lista obtenida eliminando los
elementos duplicados de la lista xs. Por ejemplo,
borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

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

text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar o refutar:
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "length (borraDuplicados xs) ≤ length xs"
oops

-- "La demostración estructurada es"
lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 20. Demostrar o refutar:
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma estaEn_borraDuplicados_auto:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

-- "La demostración estructurada es"
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 21. Demostrar o refutar:
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

-- "La demostración automática"
lemma "sinDuplicados (borraDuplicados xs)"
oops

-- "La demostración estructurada es"
lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 22. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops

end
</source>

Relación 1

2011-02-01T16:38:35Z

Palmagroblanco:

<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"
oops

lemma "A ⟶ ¬¬A"
oops

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

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

lemma "A ∨ ¬A"
oops

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

end
</source>

Relación 1

2011-02-01T16:37:13Z

Palmagroblanco:

<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 S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
oops

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"
oops

lemma "A ⟶ ¬¬A"
oops

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

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

lemma "A ∨ ¬A"
oops

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

end
</source>

Relación 1

2011-02-01T16:36:10Z

Palmagroblanco:

<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 "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
oops

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

lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
oops

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"
oops

lemma "A ⟶ ¬¬A"
oops

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

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

lemma "A ∨ ¬A"
oops

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

end
</source>

Usuario:Palmagroblanco

2011-02-01T16:32:47Z

Palmagroblanco: Página creada con 'Pedro Almagro Blanco'

Pedro Almagro Blanco