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

Relación 7

2021-08-22T09:38:01Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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>

Misceláneas

2021-07-24T15:27:25Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
theory Tema8
imports Main Efficient_Nat
begin

header {* Misceláneas *}

text {*
Contenido:
* Definición del algoritmo de Huffman
* Definiciones inductivas
* Demostraciones por introducción
* Demostraciones por inducción sobre conjuntos inductivos
* Clases
* Subclase
* Instanciación de clases
* Ámbitos ("Locales")
* Demostraciones estructuradas: inducción y encadenamiento
* Un ejemplo elemental de álgebra
* Definición de clases
* Instanciación de clases
* Instancias recursivas
* Subclases
* Las clases de tipos como ámbitos
* Razonamiento abstracto
* Definiciones derivadas
* Analogía entre clases y functores
* Relaciones de subclase adicionales
* Otras cuestiones
* Clases de tipos y generación de código
* Inspección del universo de las clases de tipos
* Sledgehammer
* Refute
* Refutaciones en lógica proposicional
* Refutaciones en lógica de predicados
* Refutaciones con funciones e igualdad
* Ejemplos con listas
* Nitpick
* Refutación proposicional
* Skolemizaciónn
*}

section {* Definición del algoritmo de Huffman *}

text {*
Ejemplo de definición de tipo de datos recursivo: árboles binarios.
*}

datatype 'a arbol = Hoja nat 'a | Nodo nat "('a arbol)" "('a arbol)"

text {*
Ejemplo de definición primitiva recursiva sobre un tipo definido:
Definición del valor de un árbol.
*}

primrec "valor" where
"valor (Hoja n _) = n"
| "valor (Nodo n _ _) = n"

text {*
Ejemplo de definición no recursiva: Mezcla de dos árboles.
*}

definition "mezcla t1 t2 = Nodo (valor t1 + valor t2) t1 t2"

text {*
Definición de la inserción de un árbol en un bosque.
*}

fun ins where
"ins u (t#ts) = (if valor u ≤ valor t then u # t # ts else t # ins u ts)"
| "ins u [] = [u]"

text {*
Lema para usar en las demostraciones de terminación. En particular, en
la definición de creaArbol.
*}

lemma size_ins[termination_simp]: "size(ins u ts) = size ts + 1"
by (induct ts) simp_all

text {*
Creación de árboles a partir de listas
*}

fun creaArbol where
"creaArbol(t1#t2#ts) = creaArbol(ins (mezcla t1 t2) ts)"
| "creaArbol[t] = t"

text {*
Ejemplo de formas normales: creación de árboles de Huffman.
*}

value
"creaArbol[Hoja 3 a, Hoja 6 b, Hoja 12 c, Hoja 24 d]"

text {*
El árbol creado es
"Nodo 45 (Nodo 21 (Nodo 9 (Hoja 3 a) (Hoja 6 b)) (Hoja 12 c)) (Hoja 24 d)" *}

value
"creaArbol[Hoja 24 d, Hoja 6 b, Hoja 12 c, Hoja 3 a]"

text {*
El árbol creado es
"Nodo 45 (Nodo 15 (Hoja 12 c) (Hoja 3 a)) (Nodo 30 (Hoja 24 d) (Hoja 6 b))"
*}

section {* Definiciones inductivas *}

text {*
En esta sección vamos a trabajar con una gramática cuyo alfabeto consta de
dos símbolos: A y B. En primer lugar, se define el alfabeto (alfa)
como un tipo con dos elementos.
*}

datatype alfa = A | B

text {*
Se define la gramática S como el conjunto de las listas de elementos del
alfabeto generadas mediante las siguientes reglas:
· La lista vacía está en S,
· Si w está en S, entonces AwB también lo está.
· Si v y w están en S, entonces vw también lo está.
*}

inductive_set S :: "alfa list set" where
S1: "[] ∈ S"
| S2: "w ∈ S ⟹ [A] @ w @ [B] ∈ S"
| S3: "v ∈ S ⟹ w ∈ S ⟹ v @ w ∈ S"

subsection {* Demostraciones por introducción *}

text {*
La lista [A, B] está en S.
*}

lemma "[A, B] ∈ S"
proof -
have "[] ∈ S" by (rule S1)
hence "[A] @ [] @ [B] ∈ S" by (rule S2)
thus ?thesis by simp
qed

subsection {* Demostraciones por inducción sobre conjuntos inductivos *}

text {*
Ninguna palabra de la gramática empieze por B.
*}

lemma "w ∈ S ⟹ ¬ (∃v. w = B # v)"
proof (induct set:S)
case S1
thus ?case by simp
next
case S2
thus ?case by simp
next
case S3
thus ?case (* sledgehammer *) by (simp add: append_eq_Cons_conv)
qed

section {* Clases *}

text {*
El tutorial sobre clases está en la teoría Clases.thy.

La clase de los órdenes es la colección de los tipos que poseen una
relación ≼ verificando las siguientes propiedades
· reflexiva: x ≼ x
· transitiva: x ≼ y ⟹ y ≼ z ⟹ x ≼ z
· antisimétrica: x ≼ y ⟹ y ≼ x ⟹ x = y
*}

class orden =
fixes menor_ig :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50)
assumes refl: "x ≼ x"
and trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
and antisim: "x ≼ y ⟹ y ≼ x ⟹ x = y"

text {*
Ha generado los teoremas correspondientes a los axiomas. Pueden consultarse
mediante thm como se muestra a continuación.
*}

thm refl

text {*
Se inicia el contexto orden en el que se van a realizar definiciones y
demostraciones.
*}

context orden
begin

text {*
x es menor que y si x es menor o igual que y y no son iguales.
*}

definition menor :: "'a ⇒ 'a ⇒ bool" (infix "≺" 50)
where "x ≺ y ⟷ x ≼ y ∧ ¬ y ≼ x"

text {*
La relación menor es irreflexiva.
*}

lemma irrefl: "¬ x ≺ x"
by (auto simp:menor_def)

text {*
La relación menor es transitiva.
*}

lemma menor_trans: "x ≺ y ⟹ y ≺ z ⟹ x ≺ z"
by (auto simp:menor_def intro:trans)

text {*
La relación menor es asimétrica; es decir, si x ≺ y e y ≺ x, entonces
se verifica cualquier propiedad P.
*}

lemma asimetrica: "x ≺ y ⟹ y ≺ x ⟹ P"
by (auto simp:menor_def)

end

subsection {* Subclase *}

text {*
Un orden lineal es un orden en que cada par de elementos son comparables.
*}

class ordenLineal = orden +
assumes lineal: "x ≼ y ∨ y ≼ x"
begin

text {*
En los órdenes lineales se tiene que x ≺ y ∨ x=y ∨ y ≺ x.
*}

lemma "x ≺ y ∨ x=y ∨ y ≺ x"
using menor_def lineal antisim
by blast

end

subsection {* Instanciación de clases *}

text {*
El producto de dos órdenes es un orden.
*}

instantiation prod :: (orden, orden) orden
begin

inductive menor_ig_prod :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
menor_ig_fst: "x ≺ v ⟹ (x, y) ≼ (v, w)"
| menor_ig_snd: "x = v ⟹ y ≼ w ⟹ (x, y) ≼ (v, w)"

instance
proof
fix p :: "'a × 'b"
show "p ≼ p" by (cases p) (auto intro!: menor_ig_snd refl)
next
fix p q r :: "'a × 'b"
assume "p ≼ r" and "r ≼ q"
then show "p ≼ q"
by (induct p r rule:menor_ig_prod.induct)
(auto elim!:menor_ig_prod.cases
intro:menor_ig_fst menor_ig_snd trans menor_trans)
next
fix p q :: "'a × 'b"
assume "p ≼ q" and "q ≼ p"
then show "p = q"
by (induct p q rule:menor_ig_prod.induct)
(auto elim!:menor_ig_prod.cases
elim:asimetrica
intro:antisim
simp:irrefl)
qed

end

section {* Ámbitos ("Locales") *}

text {*
Un orden es una estructura con una relación reflexiva, transitiva y
antisimétrica.
*}

locale Orden =
fixes menor_ig :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
assumes refl: "x ⊑ x"
and trans: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
and antisim: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"

text {*
Los teoremas se diferencian por el nombre y el ámbito. Por ejemplo,
refl: ?x ≼ ?x
Orden.refl: Orden ?menor_ig ⟹ ?menor_ig ?x ?x
Orden_def: Orden ?menor_ig ≡
(∀x. ?menor_ig x x) ∧
(∀x y z. ?menor_ig x y ⟶ ?menor_ig y z ⟶ ?menor_ig x z) ∧
(∀x y. ?menor_ig x y ⟶ ?menor_ig y x ⟶ x = y)
*}

thm refl
thm Orden.refl
thm Orden_def

text {*
Un orden lineal es un orden en el que todos los pares de elementos son
comparables.
*}

locale OrdenLineal = Orden +
assumes lineal: "x ⊑ y ∨ y ⊑ x"

text {*
Los boooleanos está ordenados con el condicional.
*}

interpretation Orden_imp: Orden "op ⟶"
proof
fix P show "P ⟶ P" by blast
next
fix P Q R show "P ⟶ Q ⟹ Q ⟶ R ⟹ P ⟶ R" by blast
next
fix P Q show "P ⟶ Q ⟹ Q ⟶ P ⟹ P = Q" by blast
qed

thm dvd.order_trans
thm dvd.less_le_trans

text {*
Los naturales con la relación de divisibilidad es un conjunto ordenado.
*}

interpretation Orden_dvd: Orden "op dvd :: nat ⇒ nat ⇒ bool"
proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)

text {*
Ámbito de las funciones monótonas (ver la página 12 del tutorial de
locales).
*}

locale Mono =
le1: Orden le1 +
le2: Orden le2
for le1 (infix "⊑\<^isub>1" 50) and le2 (infix "⊑\<^isub>2" 50) +
fixes f :: "'a ⇒ 'b"
assumes mono: "x ⊑\<^isub>1 y ⟹ f(x) ⊑\<^isub>2 f(y)"

text {*
Si f es monótona, x ⊑\<^isub>1 y e y ⊑\<^isub>1 z, entonces f(x) ⊑\<^isub>2 f(z).
*}

lemma (in Mono) mono_trans:
assumes "x ⊑\<^isub>1 y" and "y ⊑\<^isub>1 z"
shows "f(x) ⊑\<^isub>2 f(z)"
proof -
have "x ⊑\<^isub>1 z" using assms and le1.trans by blast
thus "f(x) ⊑\<^isub>2 f(z)" using mono by simp
qed

text {*
El teorema generado se llama Mono.mono_trans.
*}

thm Mono.mono_trans

text {*
En el contexto Mono el nombre es mono_trans.
*}

context Mono begin thm mono_trans end

text {*
El predicado `ser par' es un operador monótono entre los naturales con la
relación de divisibilidad y los booleanos con el condicional; es decir,
x dvd y ⟹ 2 dvd x ⟶ 2 dvd y
*}

interpretation Mono "op dvd" "op ⟶" "λn::nat. 2 dvd n"
proof
fix x y :: nat
show "x dvd y ⟹ 2 dvd x ⟶ 2 dvd y"
proof
assume "x dvd y" and "2 dvd x"
thus "2 dvd y" using dvd.order_trans by blast
qed
qed

section {* Demostraciones estructuradas: inducción y encadenamiento *}

text {*
El siguiente ejemplo se encuentra en Wenzel2006 pp. 3--5 y el código
en Isar_Example/Puzzle.thy. Una demostración más actualizada se
encuentra en Nipkow2009 p.1 basada en la de Tao2006 pp. 34--36.
*}

theorem identity1:
fixes f :: "nat ⇒ nat"
assumes fff: "⋀n. f(f(n)) < f(Suc(n))"
shows "f(n) = n"
proof -
{ fix m n have key: "n ≤ m ⟹ n ≤ f(m)"
proof(induct n arbitrary: m)
case 0 show ?case by simp
next
case (Suc n)
have HI1: "⋀k. n ≤ k ⟹ n ≤ f k" using Suc by simp
have HI2: "Suc n ≤ m" using Suc by simp
hence "m ≠ 0" by simp
then obtain k where [simp]: "m = Suc k" by (metis not0_implies_Suc)
have "n ≤ k" using HI2 by simp
have "n ≤ f(k)" using Suc by simp
hence "n ≤ f(f(k))" using Suc by simp
also have "… < f(m)" using fff by simp
finally show ?case by simp
qed }
hence "⋀n. n ≤ f(n)" by simp
hence "⋀n. f(n) < f(Suc n)" by(metis fff order_le_less_trans)
hence "f(n) < n+1" by (metis fff lift_Suc_mono_less_iff[of f] Suc_eq_plus1)
with `n ≤ f(n)` show "f n = n" by arith
qed

section {* Un ejemplo elemental de álgebra *}

subsection {* Definición de clases *}

text {*
Un semigrupo es una estructura compuesta por un conjunto A y una
operación binaria en A.
*}

class semigrupo =
fixes mult :: "'a ⇒ 'a ⇒ 'a" (infixl "⊗" 70)
assumes asoc: "(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z )"

subsection {* Instanciación de clases *}

text {*
Los enteros con la suma forman un semigrupo.
*}

instantiation int :: semigrupo
begin
definition
mult_int_def: "i ⊗ j = i + (j ::int)"

instance proof
fix i j k :: "int"
have "(i + j ) + k = i + (j + k)" by simp
thus "(i ⊗ j ) ⊗ k = i ⊗ (j ⊗ k)" unfolding mult_int_def .
qed
end

text {*
Los naturales con la suma forman un semigrupo.
*}

instantiation nat :: semigrupo
begin
primrec mult_nat where
"(0::nat) ⊗ n = n"
| "Suc m ⊗ n = Suc (m ⊗ n)"

instance proof
fix m n q :: "nat"
show "m ⊗ n ⊗ q = m ⊗ (n ⊗ q)"
by (induct m) auto
qed
end

subsection {* Instancias recursivas *}

text {*
Si (A,⊗) y (B,⊗) son semigrupos, entonces ((A×B,⊗), donde el producto
se define por
(x,y)⊗(x',y') = (x⊗x',y⊗y'),
es un semigrupo.
*}

instantiation prod :: (semigrupo, semigrupo) semigrupo
begin

definition
mult_prod_def : "p1 ⊗ p2 = (fst p1 ⊗ fst p2, snd p1 ⊗ snd p2)"

instance proof
fix p1 p2 p3 :: "'a::semigrupo × 'b::semigrupo"
show "(p1 ⊗ p2) ⊗ p3 = p1 ⊗ (p2 ⊗ p3)"
unfolding mult_prod_def by (simp add: asoc)
qed
end

subsection {* Subclases *}

text {*
Un monoide izquierdo es un semigrupo con elemento neutro por la izquierda.
*}

class monoideI = semigrupo +
fixes neutro :: "'a" ("1")
assumes neutroI: "1 ⊗ x = x"

text {*
Los naturales y los enteros con la suma forman monoides por la izquierda.
*}

instantiation nat and int :: monoideI
begin

definition
neutro_nat_def : "1 = (0::nat)"

definition
neutro_int_def : "1 = (0::int)"

instance proof
fix n :: nat
show "1 ⊗ n = n" unfolding neutro_nat_def by simp
next
fix k :: int
show "1 ⊗ k = k" unfolding neutro_int_def mult_int_def by simp
qed
end

text {*
El producto de dos monoides por la izquierda es un monoide por la
izquierda, donde el neutro es el par formado por los elementos neutros.
*}

instantiation prod :: (monoideI , monoideI) monoideI
begin

definition
neutro_prod_def : "1 = (1, 1)"

instance proof
fix p :: "'a::monoideI × 'b::monoideI"
show "1 ⊗ p = p"
unfolding neutro_prod_def mult_prod_def by (simp add: neutroI)
qed
end

text {*
Un monoide es un monoide por la izquierda cuyo elemento neutro por la
izquierda lo es también por la derecha.
*}

class monoide = monoideI +
assumes neutro: "x ⊗ 1 = x"

text {*
Los naturales y los enteros con la suma son monoides.
*}

instantiation nat and int :: monoide
begin

instance proof
fix n :: nat
show "n ⊗ 1 = n"
unfolding neutro_nat_def by (induct n) simp_all
next
fix k :: int
show "k ⊗ 1 = k"
unfolding neutro_int_def mult_int_def by simp
qed
end

text {*
El producto de dos monoides es un monoide.
*}

instantiation prod :: (monoide, monoide) monoide
begin

instance proof
fix p :: "'a::monoide × 'b::monoide"
show "p ⊗ 1 = p"
unfolding neutro_prod_def mult_prod_def by (simp add: neutro)
qed
end

text {*
Un grupo es un monoide por la izquierda tal que todo elemento posee un
inverso por la izquierda.
*}

class grupo = monoideI +
fixes inverso :: "'a ⇒ 'a" ("(_⁻)" [1000] 999)
assumes inversoI: "x⁻ ⊗ x = 1"

text {*
Los enteros con la suma forman un grupo.
*}

instantiation int :: grupo
begin

definition
inverso_int_def: "i⁻ = -(i::int)"

instance proof
fix i :: "int"
have "-i + i = 0" by simp
then show "i⁻ ⊗ i = 1"
unfolding mult_int_def neutro_int_def inverso_int_def .
qed
end

section {* Las clases de tipos como ámbitos *}

subsection {* Razonamiento abstracto *}

text {*
En los grupos se verifica la propiedad cancelativa por la izquierda, i.e.
x ⊗ y = x ⊗ z ⟷ y = z
*}

lemma (in grupo) cancelativa_izq: "x ⊗ y = x ⊗ z ⟷ y = z"
proof
assume "x ⊗ y = x ⊗ z"
hence "x⁻ ⊗ (x ⊗ y) = x⁻ ⊗ (x ⊗ z)" by simp
hence "(x⁻ ⊗ x) ⊗ y = (x⁻ ⊗ x) ⊗ z" using asoc by simp
thus "y = z" using neutroI and inversoI by simp
next
assume "y = z"
thus "x ⊗ y = x ⊗ z" by simp
qed

thm Tema8.grupo.cancelativa_izq

text {*
Se genera el teorema Tema8b.grupo.cancelativa_izq
class.grupo ?mult ?neutro ?inverso ⟹
(?mult ?x ?y = ?mult ?x ?z) = (?y = ?z)

El teorema se aplica automáticamente a todas las instancias de la clase
grupo. Por ejemplo, a los enteros.
*}

subsection {* Definiciones derivadas *}

text {*
En los monoides se define la potencia natural por
· x^0=1
· x^{n+1}=x*x^n
*}

primrec (in monoide) potencia_nat :: "nat ⇒ 'a ⇒ 'a" where
"potencia_nat 0 x = 1"
| "potencia_nat (Suc n) x = x ⊗ potencia_nat n x"

subsection {* Analogía entre clases y functores *}

text {*
Las listas con la operación de concatenación y la lista vacía como elemento
neutro forman un monoide.
*}

interpretation list_monoide: monoide "append" "[]"
proof qed auto

text {*
Se pueden aplicar propiedades de los monides a las listas. Por ejemplo,
*}

lemma "append [] xs = xs"
by simp

text {*
(repite n xs) es la lista obtenida concatenando n veces la lista xs.
*}

primrec repite :: "nat ⇒ 'a list ⇒ 'a list" where
"repite 0 _ = []"
| "repite (Suc n) xs = xs @ repite n xs"

text {*
Las listas con la operación de concatenación y la lista vacía como elemento
neutro forman un monoide. Además, la potencia natural se intepreta como
repite.
*}

interpretation list_monoide: monoide "append" "[]" where
"monoide.potencia_nat append [] = repite"
proof -
interpret monoide "append" "[]" ..
show "monoide.potencia_nat append [] = repite"
proof
fix n
show "monoide.potencia_nat append [] n = repite n"
by (induct n) auto
qed
qed intro_locales

subsection {* Relaciones de subclase adicionales *}

text {*
Los grupos son monoides.
*}

subclass (in grupo) monoide
proof
fix x
have "x⁻ ⊗ (x ⊗ 1) = x⁻ ⊗ (x ⊗ (x⁻ ⊗ x))" using inversoI by simp
also have "... = (x⁻ ⊗ x) ⊗ (x⁻ ⊗ x)" using asoc [symmetric] by simp
also have "... = 1 ⊗ (x⁻ ⊗ x)" using inversoI by simp
also have "... = x⁻ ⊗ x" using neutroI by simp
finally have "x⁻ ⊗ (x ⊗ 1) = x⁻ ⊗ x" .
thus "x ⊗ 1 = x" using cancelativa_izq by simp
qed

text {*
La potencia entera en los grupos se define a partir de la potencia natural
como sigue:
· x^k = x^k si k ≥ 0
· x^k = (x^{-k})^{-1}, en caso contrario.
*}

definition (in grupo) potencia_entera :: "int ⇒ 'a ⇒ 'a" where
"potencia_entera k x =
(if k >= 0
then potencia_nat (nat k) x
else (potencia_nat (nat (- k)) x)⁻)"

section {* Otras cuestiones *}

subsection {* Clases de tipos y generación de código *}

text {*
Ejemplo para evaluar.
*}

definition ejemplo :: int where
"ejemplo = potencia_entera 10 (-2)"

text {*
Al evaluar la siguiente expresión se obtiene como valor -20.
*}

value "ejemplo"

text {*
Ejemplo de generación de código Haskell.
*}

export_code ejemplo
in Haskell file "codigoHaskell/"

text {*
El código Haskell se exporta en el fichero codigoHaskell/Tema8b.hs
*}

subsection {* Inspección del universo de las clases de tipos *}

text {*
Se puede obtener la lista de las clases con print_classes. Por
ejemplo, evaluando la siguiente expresión se obtiene
class semigrupo:
supersort: type
parameters:
mult :: 'a ⇒ 'a ⇒ 'a
instances:
int :: semigrupo, nat :: semigrupo,
prod :: (semigrupo, semigrupo) semigrupo

class monoideI:
supersort: semigrupo
parameters:
neutro :: 'a
instances:
int :: monoideI, nat :: monoideI, prod :: (monoideI, monoideI) monoideI

class monoide:
supersort: monoideI
instances: int :: monoide, nat :: monoide, prod :: (monoide, monoide) monoide

class grupo:
supersort: monoide
parameters:
inverso :: 'a ⇒ 'a
instances: int :: grupo
*}

print_classes

text {*
Se puede obtener el grafo de las clases con class_deps.
*}

class_deps

section {* Sledgehammer *}

text {*
Demostración con Sledgehammer de la paradoja del bebedor: ``hay una persona
en el bar, tal que si dicha persona bebe todos beben''.
*}
lemma "∃x. P x ⟶ (∀y. P y)"
by metis

section {* Refute *}

subsection {* Refutaciones en lógica proposicional *}

text {*
Ejemplo de refutación proposicional.
*}
lemma "P ⟷ Q"
refute
oops

text {*
El resultado obtenido es
*** Model found: ***
empty universe (no type variables in term)
Q: True
P: False
*}

subsubsection {* Refutaciones en lógica de predicados *}

text {*
Ejemplo de refutación en lógica de primer orden.
*}

lemma "(∃x. P x) ⟶ (∀x. P x)"
refute
oops

text {*
El resultado obtenido es
*** Model found: ***
Size of types: 'a: 2
P: {(a0, True), (a1, False)}
que da un contraejemplo cuyo universo es {a₀, a₁} y sólo se verifica
en a₀.
*}

text {*
Ejemplo de refutación en lógica de primer orden con relaciones binarias.
*}

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
refute
oops

text {*
El resultado obtenido es
*** Model found: ***
Size of types: 'a: 2, 'b: 2
P: {(a0, {(b0, True), (b1, False)}), (a1, {(b0, False), (b1, True)})}
que da un contraejemplo cuyo universo es {a₀, a₁, b₀, b₁} y P sólo se
verifica en {(a₀,b₁),(a₁,b₀)}.
*}

text {*
Conjetura: Toda relación reflexiva y simétrica es transitiva.
*}

lemma "⟦ ∀x. P x x; ∀x y. P x y ⟶ P y x ⟧ ⟹ P x y ⟶ P y z ⟶ P x z"
refute
oops

text {*
El resultado obtenido es
*** Model found: ***
Size of types: 'a: 3
z: a0
y: a2
x: a1
P: {(a0, {(a0, True), (a1, False), (a2, True)}),
(a1, {(a0, False), (a1, True), (a2, True)}),
(a2, {(a0, True), (a1, True), (a2, True)})}
que da un contraejemplo cuyo universo es {a₀, a₁, a₂} y P sólo se
verifica en
{(a₀,a₀),(a₀,a₁),(a₀,a₂),(a₁,a₀),(a₁,a₁),(a₂,a₀),(a₂,a₂)}.
Entonces P es reflexiva y simétrica, pero no es transitiva porque
se tiene que P(a₂,a₀) y P(a₀,a₁) y no se verifica P(a₂,a₁).
*}

subsubsection {* Refutaciones con funciones e igualdad *}

text {*
En los siguientes ejemplos se consideran símbolos de función y el de
igualdad.

Ejemplo de fallo en la refutación de la paradoja del mentiroso.
*}

lemma "∃x. f x = g x ⟶ f = g"
refute [maxsize=4]
apply (auto simp add: ext)
done

text {*
Refutación de una versión incorrecta de la paradoja del bebedor.
*}

lemma "(∃x. f x = g x) ⟶ f = g"
refute
oops

text {*
Se obtiene
*** Model found: ***
Size of types: 'a: 2, 'b: 2
g: {(a0, b1), (a1, b1)}
f: {(a0, b0), (a1, b1)}
*}

text {*
La composición de funciones es conmutativa.
*}

lemma "f (g x) = g (f x)"
refute
oops

text {*
Se obtiene
*** Model found: ***
Size of types: 'a: 2
x: a0
g: {(a0, a1), (a1, a0)}
f: {(a0, a1), (a1, a1)}
*}

text {*
Toda función suprayectiva tiene inversa.
*}

lemma "(∀y. ∃x. y = f x) ⟶ (∃g. ∀x. g (f x) = x)"
refute
oops

text {*
Se obtiene
*** Model found: ***
Size of types: 'a: 1, 'b: 2
f: {(b0, a0), (b1, a0)}
*}

text {*
Toda función que tiene inversa es suprayectiva.
*}

lemma "(∃g. ∀x. g (f x) = x) ⟶ (∀y. ∃x. y = f x)"
refute
oops

text {*
Se obtiene
*** Model found: ***
Size of types: 'b: 1, 'a: 2
f: {(b0, a1)}
*}

subsection {* Ejemplos con listas *}

text {*
La concatenación de listas es conmutativa.
*}

lemma "xs @ ys = ys @ xs"
refute
oops

text {*
Se obtiene
*** Model found: ***
Size of types: 'a list: 3, 'a: 2
ys: [a0]
xs: [a1]
*}

section {* Nitpick *}

text {*
Notas:
· Nitpick es un generador de contraejemplos.
· Los ejemplos están elegidos de Nitpick_Examples.thy.
· Para los ejemplos de Nitpick se deshabilita el QuicCheck automático.
· Nitpick va a usar MiniSATJNI con una hebra.
*}
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]

subsection {* Refutación proposicional *}

lemma "P ⟷ Q"
nitpick
oops

text {*
Se obtiene
Nitpick found a counterexample:
Free variables:
P = True
Q = False
*}

subsection {* Skolemizaciónn *}

text {*
Conjetura: Las funciones que tienen inversa son suprayectivas.
*}

lemma "∃g. ∀x. g (f x) = x ⟹ ∀y. ∃x. y = f x"
nitpick
oops

text {*
Se obtiene
Nitpick found a counterexample for card 'a = 2 and card 'b = 1:

Free variable:
f = (λx. _)(b\<^bsub>1\<^esub> := a\<^bsub>1\<^esub>)
Skolem constants:
g = (λx. _)(a\<^bsub>1\<^esub> := b\<^bsub>1\<^esub>, a\<^bsub>2\<^esub> := b\<^bsub>1\<^esub>)
y = a\<^bsub>2\<^esub>
Significa que que Nitpick ha encontrado un contraejemplo donde
· A={a\<^bsub>1\<^esub>,a\<^bsub>2\<^esub>}
· B={b\<^bsub>1\<^esub>}
· f: B → A tal que f(b\<^sub>1)=a\<^sub>1
Entonces, f tiene inversa (la función g: A → B tal que g(a\<^sub>1)=b\<^sub>1 y
g(a\<^sub>2)=b\<^sub>1), pero no es suprayectiva (el elemento a\<^sub>2 no tiene antiimagen).
*}

end
</source>

Relación 6

2021-07-24T15:21:41Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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 5

2018-07-16T07:51:51Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

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

theory Relacion_5
imports Main
begin

section {* Menor posición válida *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (menorValida p xs) es el índice del primer elemento de una
lista xs que satisface el predicado p y es la longitud de xs si
ningún elemento satisface el predicado p. Por ejemplo,
menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1] = 2
menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5
menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
---------------------------------------------------------------------
*}

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

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
lista syss ningún elemento satisface el predicado dado.
---------------------------------------------------------------------
*}

lemma "menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5"
by auto

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
entonces ninguno de los primeros n elementos de la lista xs verifica
la propiedad P.
---------------------------------------------------------------------
*}

{* Una posible opcion inicial es poner un ejemplo en el que no se cumpla
e intentar sacar un contraejemplo
*}

lemma "menorValida (λx. 4<x) [1::nat, 2, 3, 4, 7] = 5"
quickcheck
oops

{* Duda: Utilizando la palabra clave "quickcheck" el sistema avisa de que
ha encontrado un contraejemplo, pero no muestra nada, ¿ha encontrado
realmente un contraejemplo? *}

text {*
---------------------------------------------------------------------
Ejercicio 4. ¿Cómo se puede relacionar
"menorValida (λ x. P x ∨ Q x) xs"
con
"menorValida P xs" y "menorValida Q xs"?
¿Se puede decir algo parecido con la conjunción de P y Q?
Prueba tus conjeturas.
---------------------------------------------------------------------
*}

text {*
La relación es la siguiente: La menor posición de los elementos que
verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
los elementos que verifican P y de la menor posición de los elementos
que verifican Q.
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre
"menorValida P xs" y "menorValida Q xs"?
---------------------------------------------------------------------
*}

end
</source>

Rel 9

2018-07-16T07:51:39Z

Jalonso:

<source lang="isabelle">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
oops

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
oops

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
oops

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
oops

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 2

2018-07-16T07:51:39Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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
next
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

text {*
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

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

text {*
Comentario de J.A. Alonso: ¿Cómo se calcula un contraejemplo con Isabelle?
*}

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

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

text {*
Comentario de J.A. Alonso: ¿Cómo se calcula un contraejemplo con Isabelle?

Simplemente ejecutando un lema o teorema para el cual se pueda encontrar un
contraejemplo, isabelle automáticamente te lo mostrará. Para que el sistema
calcule un contraejemplo directamente también es posible utilizar la palabra
reservada "refute"
*}

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

end
</source>

Rel 7

2018-07-16T07:51:11Z

Jalonso:

Relación 1

2018-07-16T07:50:54Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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 ej1_d1: "A ⟶ A"
by (rule imp_refl)

-- "Se puede hacer automáticamente"
lemma ej1_d2: "A ⟶ A"
by auto

-- "Otra forma (más explicita)"
lemma ej1_d3: "A ⟶ A"
proof (rule impI)
assume 1: "A"
qed

lemma ej2_d1:
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

text {*
El ejercicio anterior hecho de un modo automático (dado que no es
posible hacerlo por auto, es un buen candidato a que lo resuelvan
otros demostradores automáticos proposicionales
*}

lemma ej2_d2:
assumes 1:"A ∧ B"
shows "B ∧ A"
by (metis 1)

text {*
Comentario de J.A. Alonso: El ejercicio 2 puede resolverse por
auto.
*}

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

-- "Otra versión"
lemma ej3_d2: "A ∧ B ⟶ A ∨ B"
proof
assume 1: "A ∧ B"
from 1 have 2: "A" by (rule conjunct1)
from 2 show "A ∨ B" by (rule disjI1)
qed

lemma ej4_d1:
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

-- "Otra forma (más explícita)"
lemma ej4_d2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
assume 1: "(A ∨ B) ∨ C"
show "A ∨ (B ∨ C)"
proof -
note 1
moreover{
assume 2: "A ∨ B"
have "A ∨ (B ∨ C)"
proof -
note 2
moreover{
assume 3: "A"
from 3 have 4:"A ∨ (B ∨ C)" by (rule disjI1)
}
moreover{
assume 5:"B"
from 5 have 6: "B ∨ C" by (rule disjI1)
from 6 have 7: "A ∨ (B ∨ C)" by (rule disjI2)
}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed
}
moreover{
assume 8: "C"
from 8 have 9: "B ∨ C" by (rule disjI2)
from 9 have "A ∨ (B ∨ C)" by (rule disjI2)
}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed
qed

text {*
Comentario de J.A. Alonso: El enunciado de ej4_d2 no es exactamente
el mismo que el original y la demostración es demasiado larga.
*}

text {*
La versión anterior de la propiedad asociativa de la disyunción (es
decir, en forma de proposición implicativa) demostrada de forma muy
automática y breve.
*}

lemma ej4_d3: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
by auto

text {*
Comentario de J.A. Alonso: El enunciado de ej4_d3 no es exactamente
el mismo que el original.
*}

-- "Otra versión. la sentencia note no es necesaria."
lemma ej4_d4: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
assume 1: "(A ∨ B) ∨ C"
moreover
{ assume 4: "(A ∨ B)"
moreover
{ assume 5: "A"
from 5 have 6: "A ∨ (B ∨ C)" by (rule disjI1)}
moreover
{ assume 7: "B"
from 7 have 8: "(B ∨ C)" by (rule disjI1)
from 8 have 9: "A ∨ (B ∨ C)" by (rule disjI2)}
ultimately have "A ∨ (B ∨ C)" by (rule disjE)}
moreover
{ assume 2: "C"
from 2 have 3: "(B ∨ C)" by (rule disjI2)
from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed

text {*
Comentario de J.A. Alonso: El enunciado de ej4_d4 no es exactamente
el mismo que el original y la demostración es demasiado larga.
*}

lemma ej5_aux:
assumes "A"
shows "B ⟶ A"
using assms
by simp

lemma ej5_d1: "A ⟶ (B ⟶ A)"
proof
assume 1: "A"
from 1 show "B ⟶ A" by (rule ej5_aux)
qed

text {*
Comentario de J.A. Alonso: En la prueba anterior puede eliminarse la
etiqueta.
*}

-- "Éste también se puede obtener de forma totalmente automática."
lemma ej5_d2: "A ⟶ (B ⟶ A)"
by auto

lemma ej6_d1: "(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

-- "Por simplificación es inmediata su justificación"
lemma ej6_d2: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
by auto

lemma ej7_d1: "(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

-- "Por simplificación es inmediata su justificación"
lemma ej7_d2: "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
by simp

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

-- "Está claro que éste sale por auto y por simp"
lemma ej8_d2: "¬¬A ⟶ A"
by simp

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

text {*
Comentario de J.A. Alonso: Puede demostrase sin etiquetas.
*}

lemma MT: -- "ej10"
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 ej11_d1: "(¬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 ej12_d1: "((A ⟶ B) ⟶ A) ⟶ A"
proof
assume 1: "(A ⟶ B) ⟶ A"
have 8: "¬¬A"
proof (rule notI)
assume 2: "¬A"
have 3: "A ⟶ B"
proof (rule impI)
assume 4: "A"
from 2 and 4 show "B" by (rule notE)
qed
from 1 and 3 have 5: "A" by (rule mp)
from 2 and 5 show False by (rule notE)
qed
from 8 show "A" by (rule notnotD)
qed

-- "Éste sale por auto pero no por el método simp"
lemma ej12_d2: "((A ⟶ B) ⟶ A) ⟶ A"
by auto

lemma ej13_d1: "A ∨ ¬A"
proof cases
assume "A" thus ?thesis ..
next
assume "¬A" thus ?thesis ..
qed

-- "Demostración aún más corta y automática"
lemma ej13_d2: "A ∨ ¬A"
by simp

lemma ej14_d1: "(¬(A ∧ B)) = (¬A ∨ ¬B)"
proof
{
assume 1: "¬(A ∧ B)"
have 2: "¬A ∨ A" by (rule excluded_middle)
thus "¬A ∨ ¬B"
proof (rule disjE)
{ assume 3: "¬A"
thus "¬A ∨ ¬B" by (rule disjI1) }
next
{ assume 4: "A"
have 5: "¬B ∨ B" by (rule excluded_middle)
thus "¬A ∨ ¬B"
proof (rule disjE)
{assume 6: "¬B"
thus "¬A ∨ ¬B" by (rule disjI2) }
next
{assume 7: "B"
from 4 and 7 have 8: "A ∧ B" by (rule conjI)
from 1 and 8 show "¬A ∨ ¬B" by (rule notE) }
qed
}
qed
}
next
{ assume 1: "¬A ∨ ¬B"
show "¬(A ∧ B)"
proof (rule notI)
assume 2: "A ∧ B"
from 1 have 3:"¬A ∨ ¬B" .
moreover
{ assume 4: "¬A"
from 2 have 5:"A" by (rule conjunct1)
from 4 and 5 have False by (rule notE) }
moreover
{ assume 6: "¬B"
from 2 have 7: "B" by (rule conjunct2)
from 6 and 7 have False by (rule notE) }
ultimately show False by (rule disjE)
qed
}
qed

-- "Si no queremos entrar en detalles lo podríamos mandar a la 'maza'"
lemma ej14_d2: "(¬(A ∧ B)) = (¬A ∨ ¬B)"
by metis

end
</source>

Rel 6

2018-07-16T07:50:53Z

Jalonso:

Rel 11

2018-07-16T07:50:42Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
header {* Razonamiento sobre programas en Isabelle *}

theory Relacion_11
imports Main Efficient_Nat
begin

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

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 3. 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 (2,3) = (3,2)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 5. 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 [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 14. 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 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 17. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

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

text {* ---------------------------------------------------------------
Ejercicio 23. 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]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 26. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 28. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 30. 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 2 = [2,2,2]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. 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
Nota; La conjunción se representa por ∧
------------------------------------------------------------------ *}

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

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

text {* ---------------------------------------------------------------
Ejercicio 34. Se considera la siguiente definición iterativa de la
función factorial
factI :: Integer -> Integer
factI n = factI' n 1

factI' :: Integer -> Integer -> Integer
factI' 0 x = x -- factI'.1
factI' (n+1) x = factI' n (n+1)*x -- factI'.2
Comprobar con QuickCheck que factI y factR son equivalentes sobre los
números naturales.
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
y, como corolario, que
factI n = factR n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 36. 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 [2,5] 3 = [2,5,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

end
</source>

Relación 3

2018-07-16T07:50:35Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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]"
proof (induct xs)
show "snoc [] a = [] @ [a]" by simp
next
fix b xs
assume HI: "snoc xs a = xs @ [a]"
thus "snoc (b # xs) a = (b # xs) @ [a]"
proof -
have "snoc (b # xs) a = b#(snoc xs a)" by simp
also have "... = b#(xs @ [a])" using HI by simp
also have "... = (b#xs) @ [a]" by simp
finally show ?thesis .
qed
qed

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"
by (simp add:snoc_append)

-- "La demostración estructurada del teorema es"
theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
proof -
have "rev(x#xs)=(rev xs) @ [x]" by simp
also have "... = snoc (rev xs) x" by (simp add:snoc_append)
finally show ?thesis .
qed

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

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

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

primrec algunos :: "('a => bool) => 'a list => bool" where
"algunos P [] = False"
| "algunos P (x#xs) = (P x ∨ algunos P xs)"

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)"
by (induct xs) auto

-- "La demostración estructurada es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume 1: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
thus "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))"
proof -
have 2: "todos (λx. P x ∧ Q x) (a # xs) = ((P a ∧ Q a) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
also have 3: "... = ((P a ∧ Q a) ∧ (todos P xs ∧ todos Q xs))" using 1 by simp
also have 4: "... = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" by blast
also have 5: "... = ((todos P (a # xs) ∧ todos Q (a # xs)))" by simp
finally show ?thesis .
qed
qed

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)"
by (induct x) auto

-- "La demostración estructurada es"
lemma todos_append [simp]:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x y
assume 1: "todos P (x @ y) = (todos P x ∧ todos P y)"
thus "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
proof -
have "(todos P ((a # x) @ y)) = (P a ∧ todos P (x @ y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using 1 by simp
also have "... = (todos P (a #x) ∧ todos P y)" by simp
finally show ?thesis .
qed
qed

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"
by (induct xs) auto

-- "La demostración estructurada es"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix a xs
assume 1: "todos P (rev xs) = todos P xs"
thus "todos P (rev (a # xs)) = todos P (a # xs)"
proof -
have "todos P (rev (a # xs)) = todos P (rev (xs) @ [a])" by simp
also have "... = (todos P (rev (xs)) ∧ todos P [a])" by simp
also have "... = (todos P xs ∧ todos P [a])" using 1 by simp
also have "... = (todos P [a] ∧ todos P xs)" by blast
also have "... = todos P ([a] @ xs)" by simp
also have "... = todos P (a # xs)" by simp
finally show ?thesis .
qed
qed

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 que encuentra Quickcheck es (retocando su codificación
para que no haya problemas al exportarlo a Isabelle):
P = {a1}
Q = {a2}
xs = [a1, a2]
El contraejemplo que encuentra Nitpick se aparta del anterior en algunos
detalles:
P = {a1, a2}
Q = {a3}
xs = [a3, a2]
Refute sin embargo agota el tiempo sin llegar a encontrar un contraejemplo.
*}

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"
by (induct xs) auto

-- "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)"
by (induct xs) auto

-- "La demostración estructurada es"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
fix a xs
assume 1: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
thus "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)"
proof -
have "algunos P ((a # xs) @ ys) = (P a ∨ algunos P (xs @ ys))" by simp
also have "... = (P a ∨ (algunos P xs ∨ algunos P ys))" using 1 by simp
also have "... = ((P a ∨ algunos P xs) ∨ algunos P ys)" by blast
also have "... = (algunos P (a#xs) ∨ algunos P ys)" by simp
finally show ?thesis .
qed
qed

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"
by (induct xs) (auto simp add:algunos_append)

-- "La demostración estructurada es"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show " algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume 1: "algunos P (rev xs) = algunos P xs"
thus "algunos P (rev (a # xs)) = algunos P (a # xs)"
proof -
have "algunos P (rev (a # xs)) = algunos P (rev (xs) @ [a])" by simp
also have "... = (algunos P (rev (xs)) ∨ algunos P ([a]))" by (simp add:algunos_append)
also have "... = (algunos P xs ∨ algunos P [a])" using 1 by simp
also have "... = (algunos P [a] ∨ algunos P xs)" by blast
also have "... = algunos P (a # xs)" by simp
finally show ?thesis .
qed
qed

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)"
by (induct xs) auto

-- "De forma estructurada"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])" by simp
next
fix a xs
assume 1: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
thus "algunos (λx. P x ∨ Q x) (a # xs) = (algunos P (a # xs) ∨ algunos Q (a # xs))"
proof -
have "algunos (λx. P x ∨ Q x) (a # xs) = ((P a ∨ Q a) ∨ (algunos (λx. P x ∨ Q x) xs))" by simp
also have "... = ((P a ∨ Q a) ∨ (algunos P xs ∨ algunos Q xs))" using 1 by auto
also have "... = ((P a ∨ algunos P xs) ∨ (Q a ∨ algunos Q xs))" by auto
also have "... = (algunos P (a # xs) ∨ algunos Q (a # xs))" by auto
finally show ?thesis by auto
qed
qed

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)"
by (induct xs) auto

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

primrec estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"

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

text {*
Solución: La relación es:
"estaEn x xs ⟶ algunos (λx. True ) xs".
En efecto,
*}

lemma "estaEn x xs ⟶ algunos (λx. True ) xs"
by (induct xs arbitrary: x) auto

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

primrec sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = True"
| "sinDuplicados (a#xs) = ((¬ (estaEn a xs)) ∧ sinDuplicados xs)"

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

primrec borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (a#xs) =
(if estaEn a xs
then borraDuplicados xs
else (a#borraDuplicados xs))"

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

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

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

-- "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"
by (induct xs) auto

-- "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)"
by (induct xs arbitrary: x) (auto simp add: estaEn_borraDuplicados_auto)

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

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

text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocando su
codificación para que no haya problemas al exportarlo a Isabelle):
xs = [a1, a2, a1].
En este caso Nitpick encuentra el mismo contraejemplo.
Por su parte, Refute de nuevo no encuentra contraejemplo alguno.
*}

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

end
</source>

Rel 5

2018-07-16T07:50:34Z

Jalonso:

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

theory Relacion_5
imports Main
begin

section {* Menor posición válida *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (menorValida p xs) es el índice del primer elemento de una
lista xs que satisface el predicado p y es la longitud de xs si
ningún elemento satisface el predicado p. Por ejemplo,
menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1] = 2
menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5
menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
lista syss ningún elemento satisface el predicado dado.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
entonces ninguno de los primeros n elementos de la lista xs verifica
la propiedad P.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. ¿Cómo se puede relacionar
"menorValida (λ x. P x ∨ Q x) xs"
con
"menorValida P xs" y "menorValida Q xs"?
¿Se puede decir algo parecido con la conjunción de P y Q?
Prueba tus conjeturas.
---------------------------------------------------------------------
*}

text {*
La relación es la siguiente: La menor posición de los elementos que
verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
los elementos que verifican P y de la menor posición de los elementos
que verifican Q.
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre
"menorValida P xs" y "menorValida Q xs"?
---------------------------------------------------------------------
*}

end
</source>

Rel 4

2018-07-16T07:50:14Z

Jalonso:

<source lang="isabelle">
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]
---------------------------------------------------------------------
*}

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

-- "La demostración automática es"
lemma sust_append_auto:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
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)"
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)"
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"
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.
---------------------------------------------------------------------
*}

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

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"
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"
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 1a

2018-07-16T07:50:07Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

En esta teoría se presentan los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro [http://www.cs.bham.ac.uk/research/projects/lics Logic in Computer Science] y, más concretamente, a la forma como se explica en la asignatura de [http://www.cs.us.es/~jalonso/cursos/li-10 Lógica informática] y que puede verse en
las [http://www.cs.us.es/~jalonso/cursos/li-10/temas/tema-2.pdf transparencias del tema 2].

La página al lado de cada teorema indica la página de las anteriorestransparencias donde se encuentra la demostración.

<source lang="isabelle">
header {* Deducción natural proposicional *}

theory LogicaProposicional
imports Main
begin

section {* Reglas de la conjunción *}

text {*
La regla de introducción de la conjunción es
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
Las reglas de eliminación de la conjunción son
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
*}

lemma -- "p. 4"
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ r" using 3 2 by (rule conjI)
qed

lemma
assumes 1: "(p ∧ q) ∧ r" and
2: "s ∧ t"
shows "q ∧ s"
proof -
have 3: "p ∧ q" using 1 by (rule conjunct1)
have 4: "q" using 3 by (rule conjunct2)
have 5: "s" using 2 by (rule conjunct1)
show "q ∧ s" using 4 5 by (rule conjI)
qed

section {* Reglas de la doble negación *}

text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P
Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
. notnotI: P ⟹ ¬¬ P
que, de momento, no detallamos su demostración.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma -- "p. 5"
assumes 1: "p" and
2: "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show "¬¬p ∧ r" using 3 5 by (rule conjI)
qed

section {* Regla de eliminación del condicional *}

text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}

lemma -- "p. 6"
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 by (rule mp)
qed

lemma -- "p. 6"
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 by (rule mp)
have 5: "q ⟶ r" using 3 1 by (rule mp)
show "r" using 5 4 by (rule mp)
qed

section {* Regla derivada del modus tollens *}

text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
sin, de momento, detallar su demostración.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma -- "p. 7"
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof -
have 4: "q ⟶ r" using 1 2 by (rule mp)
show "¬q" using 4 3 by (rule mt)
qed

lemma -- "p. 7"
assumes 1: "¬p ⟶ q" and
2: "¬q"
shows "p"
proof -
have 3: "¬¬p" using 1 2 by (rule mt)
show "p" using 3 by (rule notnotD)
qed

lemma
assumes 1: "p ⟶ ¬q" and
2: "q"
shows "¬p"
proof -
have 3: "¬¬q" using 2 by (rule notnotI)
show "¬p" using 1 3 by (rule mt)
qed

section {* Regla de introducción del condicional *}

text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{ assume 3: "¬q"
have "¬p" using 1 3 by (rule mt)
} thus "¬q ⟶ ¬p" by (rule impI)
qed

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume 3: "¬q"
show "¬p" using 1 3 by (rule mt)
qed

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume 3: "¬q"
show "¬p" using 1 3 by (rule mt)
qed

lemma -- "p. 9"
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt)
} thus "p ⟶ ¬¬q" by (rule impI)
qed

lemma -- "p. 9"
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof (rule impI)
assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
show "¬¬q" using 1 3 by (rule mt)
qed

lemma -- "p. 9"
"p ⟶ p"
proof (rule impI)
qed

lemma -- "p. 10"
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
{ assume 1: "q ⟶ r"
{ assume 2: "¬q ⟶ ¬p"
{ assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
have "r" using 1 6 by (rule mp)
} hence "p ⟶ r" by (rule impI)
} hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI)
} thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

lemma -- "p. 10"
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 by (rule mp)
qed
qed
qed

lemma
assumes 1: "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
show "q ⟶ r"
proof (rule impI)
assume 3: "q"
have 4: "p ∧ q" using 2 3 by (rule conjI)
show "r" using 1 4 by (rule mp)
qed
qed

lemma
assumes 1: "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p" using 2 by (rule conjunct1)
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 by (rule conjunct2)
show "r" using 4 5 by (rule mp)
qed

lemma
assumes 1: "p ⟶ q"
shows "p ∧ r ⟶ q ∧ r"
proof (rule impI)
assume 2: "p ∧ r"
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 by (rule conjunct2)
show "q ∧ r" using 4 5 by (rule conjI)
qed

section {* Reglas de la disyunción *}

text {*
Las reglas de la introducción de la disyunción son
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
La regla de elimación de la disyunción es
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
*}

lemma -- "p. 11"
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1
proof (rule disjE)
{ assume 2: "p"
show "q ∨ p" using 2 by (rule disjI2) }
next
{ assume 3: "q"
show "q ∨ p" using 3 by (rule disjI1) }
qed

lemma -- "p. 12"
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2: "p ∨ q"
thus "p ∨ r"
proof (rule disjE)
{ assume 3: "p"
show "p ∨ r" using 3 by (rule disjI1) }
next
{ assume 4: "q"
have 5: "r" using 1 4 by (rule mp)
show "p ∨ r" using 5 by (rule disjI2) }
qed
qed

lemma
assumes 1: "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
{ assume 2: "p ∨ q"
thus "p ∨ (q ∨ r)"
proof (rule disjE)
{ assume 3: "p"
show "p ∨ (q ∨ r)" using 3 by (rule disjI1) }
next
{ assume 4: "q"
have 5: "q ∨ r" using 4 by (rule disjI1)
show "p ∨ (q ∨ r)" using 5 by (rule disjI2) }
qed }
next
{ assume 6: "r"
have 7: "q ∨ r" using 6 by (rule disjI2)
show "p ∨ (q ∨ r)" using 7 by (rule disjI2) }
qed

lemma
assumes 1: "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2: "p" using 1 ..
have "q ∨ r" using 1 ..
thus "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
{ assume 3: "q"
have "p ∧ q" using 2 3 by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1) }
next
{ assume 4: "r"
have "p ∧ r" using 2 4 by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2) }
qed
qed

section {* Regla de copia *}

lemma -- "p. 13"
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof
assume "q"
show "p" using 1 by this
qed
qed

lemma -- "p. 13"
"p ⟶ (q ⟶ p)"
proof
assume "p"
thus "q ⟶ p" by (rule impI)
qed

section {* Reglas de la negación *}

text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}

lemma -- "p. 15"
assumes 1: "¬p ∨ q"
shows "p ⟶ q"
proof
assume 2: "p"
note 1
thus "q"
proof (rule disjE)
{ assume 3: "¬p"
show "q" using 3 2 by (rule notE) }
next
{ assume "q"
thus "q" by this}
qed
qed

lemma -- "p. 16"
assumes 1: "p ⟶ q" and
2: "p ⟶ ¬q"
shows "¬p"
proof (rule notI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "¬q" using 2 3 by (rule mp)
show False using 5 4 by (rule notE)
qed

lemma
assumes 1: "p ⟶ ¬p"
shows "¬p"
proof (rule notI)
assume 2: "p"
have 3: "¬p" using 1 2 by (rule mp)
show False using 3 2 by (rule notE)
qed

lemma
assumes 1: "p ∧ ¬q ⟶ r" and
2: "¬r" and
3: "p"
shows "q"
proof -
have "¬¬q"
proof (rule notI)
assume 4: "¬q"
have 5: "p ∧ ¬q" using 3 4 by (rule conjI)
have 6: "r" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
thus "q" by (rule notnotD)
qed

lemma
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof (rule notI)
assume 4: "q"
have 5: "q ⟶ r" using 1 2 by (rule mp)
have 6: "r" using 5 4 by (rule mp)
show False using 3 6 by (rule notE)
qed

section {* Reglas del bicondicional *}

text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
*}

lemma -- "p. 17"
"(p ∧ q) = (q ∧ p)"
proof (rule iffI)
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ p" using 3 2 by (rule conjI) }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 by (rule conjunct1)
have 6: "p" using 4 by (rule conjunct2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

lemma -- "p. 18"
assumes 1: "p = q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof (rule disjE)
{ assume 3: "p"
have 4: "q" using 1 3 by (rule iffD1)
show "p ∧ q" using 3 4 by (rule conjI) }
next
{ assume 5: "q"
have 6: "p" using 1 5 by (rule iffD2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

section {* Reglas derivadas *}

subsection {* Regla del modus tollens *}

lemma -- "p. 20"
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof (rule notI)
assume 3: "F"
have 4: "G" using 1 3 by (rule mp)
show False using 2 4 by (rule notE)
qed

subsection {* Regla de la introducción de la doble negación *}

lemma -- "p. 21"
assumes 1: "F"
shows "¬¬F"
proof (rule notI)
assume 2: "¬F"
show False using 2 1 by (rule notE)
qed

subsection {* Regla de reducción al absurdo *}

lemma -- "p. 22"
assumes 1: "¬F ⟶ False"
shows "F"
proof -
have 2: "¬¬F"
proof (rule notI)
assume 3: "¬F"
show False using 1 3 by (rule mp)
qed
show "F" using 2 by (rule notnotD)
qed

text {*
La regla de reducción al absurdo en Isabelle se correponde con la
regla de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}

subsection {* Ley del tercio excluso *}

text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
Puede demostrarse como se muestra a continuación.
*}

lemma -- "p. 23"
"F ∨ ¬F"
proof (rule ccontr)
assume 1: "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume 2: "F"
hence 3: "F ∨ ¬F" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
qed
qed
qed

lemma -- "p. 24"
assumes 1: "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ q"
proof (rule disjE)
{ assume "¬p"
thus "¬p ∨ q" by (rule disjI1) }
next
{ assume 2: "p"
have "q" using 1 2 by (rule mp)
thus "¬p ∨ q" by (rule disjI2) }
qed
qed

end
</source>

Rel 3

2018-07-16T07:49:51Z

Jalonso:

Relación 11

2018-07-16T07:49:51Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
header {* Razonamiento sobre programas en Isabelle *}

theory Relacion_11
imports Main Efficient_Nat
begin

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

primrec suma :: "nat list ⇒ nat" where
"suma [] = 0"
| "suma (x#xs) = x + suma xs"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by auto

text {* ---------------------------------------------------------------
Ejercicio 3. 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 (2,3) = (3,2)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 5. 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 [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by auto

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

text{*

primrec repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
|"repite(suc n) x = x#(repite n x)"

despues de muchas pruebas no entiendo por que no la acepta.
*}

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
oops

text{*
refute no es capaz de encontrar nada para refutarlo. Es obvio, nada mas cargar el lemma quickcheck te da un contraejemplo.
*}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 14. 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 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

text{*

me ocurre lo mismo que con la funcion repite del ejercicio 7, hay algo que no se hacer bien.

primrec coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge 0 xs = []"
|"coge (suc n) (x#xs) = x#(coge n xs)"

*}

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 17. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

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

text {* ---------------------------------------------------------------
Ejercicio 23. 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]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 26. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 28. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 30. 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 2 = [2,2,2]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. 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
Nota; La conjunción se representa por ∧
------------------------------------------------------------------ *}

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

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

text {* ---------------------------------------------------------------
Ejercicio 34. Se considera la siguiente definición iterativa de la
función factorial
factI :: Integer -> Integer
factI n = factI' n 1

factI' :: Integer -> Integer -> Integer
factI' 0 x = x -- factI'.1
factI' (n+1) x = factI' n (n+1)*x -- factI'.2
Comprobar con QuickCheck que factI y factR son equivalentes sobre los
números naturales.
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
y, como corolario, que
factI n = factR n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 36. 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 [2,5] 3 = [2,5,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

end
</source>

Rel 8

2018-07-16T07:49:38Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Relación 9

2018-07-16T07:49:29Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1b:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_5:
assumes 1: "p⟶(q⟶r)"
shows "q⟶(p⟶r)"
oops

lemma ejercicio_6:
assumes 1: "p⟶(q⟶r)"
shows "(p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
assumes 1: "p"
shows "q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
assumes 1: "p⟶q"
shows "(q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
assumes 1: "p⟶(q⟶(r⟶s))"
shows "r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
assumes 1: "(p⟶q)⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_13:
assumes 1: "p" and
2: "q"
shows "p∧q"
oops

lemma ejercicio_14:
assumes 1: "p∧q"
shows "p"
oops

lemma ejercicio_15:
assumes 1: "p∧q"
shows "q"
oops

lemma ejercicio_16:
assumes 1: "p∧(q∧r)"
shows "(p∧q)∧r"
oops

lemma ejercicio_17:
assumes 1: "(p∧q)∧r"
shows "p∧(q∧r)"
oops

lemma ejercicio_18:
assumes 1: "p∧q"
shows "p⟶q"
oops

lemma ejercicio_19:
assumes 1: "(p⟶q)∧(p⟶r)"
shows "p⟶q∧r"
oops

lemma ejercicio_20:
assumes 1: "p⟶q∧r"
shows "(p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
assumes 1: "p⟶(q⟶r)"
shows "p∧q⟶r"
oops

lemma ejercicio_22:
assumes 1: "p∧q⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_23:
assumes 1: "(p⟶q)⟶r"
shows "p∧q⟶r"
oops

lemma ejercicio_24:
assumes 1: "p∧(q⟶r)"
shows "(p⟶q)⟶r"
oops

lemma ejercicio_25:
assumes 1: "p"
shows "p∨q"
oops

lemma ejercicio_26:
assumes 1: "q"
shows "p∨q"
oops

lemma ejercicio_27:
assumes 1: "p∨q"
shows "q∨p"
oops

lemma ejercicio_28:
assumes 1: "q⟶r"
shows "p∨q⟶p∨r"
oops

lemma ejercicio_29:
assumes 1: "p∨p"
shows "p"
oops

lemma ejercicio_30:
assumes 1: "p"
shows "p∨p"
oops

lemma ejercicio_31:
assumes 1: "p∨(q∨r)"
shows "(p∨q)∨r"
oops

lemma ejercicio_32:
assumes 1: "(p∨q)∨r"
shows "p∨(q∨r)"
oops

lemma ejercicio_33:
assumes 1: "p∧(q∨r)"
shows "(p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
assumes 1: "(p∧q)∨(p∧r)"
shows "p∧(q∨r)"
oops

lemma ejercicio_35:
assumes 1: "p∨(q∧r)"
shows "(p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
assumes 1: "(p∨q)∧(p∨r)"
shows "p∨(q∧r)"
oops

lemma ejercicio_37:
assumes 1: "(p⟶r)∧(q⟶r)"
shows "p∨q⟶r"
oops

lemma ejercicio_38:
assumes 1: "p∨q⟶r"
shows "(p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
assumes 1: "p"
shows "¬¬p"
oops

lemma ejercicio_40:
assumes 1: "¬p"
shows "p⟶q"
oops

lemma ejercicio_41:
assumes 1: "p⟶q"
shows "¬q⟶¬p"
oops

lemma ejercicio_42:
assumes 1: "p∨q" and
2: "¬q"
shows "p"
oops

lemma ejercicio_43:
assumes 1: "p∨q" and
2: "¬p"
shows "q"
oops

lemma ejercicio_44:
assumes 1: "p∨q"
shows "¬(¬p∧¬q)"
oops

lemma ejercicio_45:
assumes 1: "p∧q"
shows "¬(¬p∨¬q)"
oops

lemma ejercicio_46:
assumes 1: "¬(p∨q)"
shows "¬p∧¬q"
oops

lemma ejercicio_47:
assumes 1: "¬p∧¬q"
shows "¬(p∨q)"
oops

lemma ejercicio_48:
assumes 1: "¬p∨¬q"
shows "¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
assumes 1: "p∧¬p"
shows "q"
oops

lemma ejercicio_51:
assumes 1: "¬¬p"
shows "p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
assumes 1: "¬q⟶¬p"
shows "p⟶q"
oops

lemma ejercicio_55:
assumes 1: "¬(¬p∧¬q)"
shows "p∨q"
oops

lemma ejercicio_56:
assumes 1: "¬(¬p∨¬q)"
shows "p∧q"
oops

lemma ejercicio_57:
assumes 1: "¬(p∧q)"
shows "¬p∨¬q"
oops

lemma ejercicio_58:
"(p⟶q)∨(q⟶p)"
oops

end
</source>

Rel 2

2018-07-16T07:49:28Z

Jalonso:

Deducción natural en lógica de primer orden con Isabelle/Isar

2018-07-16T07:48:47Z

Jalonso:

En esta teoría se presenta una formalización en Isabelle/Isar de los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro [http://www.cs.bham.ac.uk/research/projects/lics Logic in Computer Science] y, más concretamente, a la forma como se explica en la asignatura de [http://www.cs.us.es/~jalonso/cursos/li-10 Lógica informática] y que puede verse en las [http://www.cs.us.es/~jalonso/cursos/li-10/temas/tema-7.pdf transparencias del tema 7].

La páginas en los teorema indican la página de las anteriores transparencias donde se encuentra la demostración.
<source lang="isabelle">
header {* Deducción natural en la lógica de primer orden *}

theory LogicaDePrimerOrden
imports Main
begin

section {* Reglas del cuantificador universal *}

text {*
La regla de eliminación del cuantificador universal es
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
La regla de introducción del cuantificador universal es
· allE: (⋀x. P x) ⟹ ∀x. P x
*}

lemma -- "p. 10"
assumes 1: "P(c)" and
2: "∀x. P(x) ⟶ ¬Q(x)"
shows "¬Q(c)"
proof (rule notI)
assume 3: "Q(c)"
have "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
hence "¬Q(c)" using 1 by (rule mp)
thus False using 3 by (rule notE)
qed

lemma -- "p. 11"
assumes 1: "∀x. P(x) ⟶ Q(x)" and
2: "∀x. P(x)"
shows "∀x. Q(x)"
proof (rule allI)
fix x
have 3: "P(x) ⟶ Q(x)" using 1 by (rule allE)
have 4: "P(x)" using 2 by (rule allE)
show "Q(x)" using 3 4 by (rule mp)
qed

section {* Reglas del cuantificador existencial *}

text {*
La regla de eliminación del cuantificador existencial es
· exI: P x ⟹ ∃x. P x
La regla de introducción del cuantificador existencial es
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma -- "p. 12"
assumes 1: "∀x. P(x)"
shows "∃x. P(x)"
proof -
have 2: "P(x)" using 1 by (rule allE)
show "∃x. P(x)" using 2 by (rule exI)
qed

lemma -- "p. 12"
assumes 1: "∀x. P(x)"
shows "∃x. P(x)"
proof (rule exI)
show "P(x)" using 1 by (rule allE)
qed

lemma -- "p. 12"
assumes 1: "∀x. P(x)"
shows "∃x. P(x)"
proof
show "P(x)" using 1 ..
qed

lemma -- "p. 13"
assumes 1: "∀x. P(x) ⟶ Q(x)" and
2: "∃x. P(x)"
shows "∃x. Q(x)"
proof -
obtain "a" where 3: "P(a)" using 2 by (rule exE)
have 4: "P(a) ⟶ Q(a)" using 1 by (rule allE)
have 5: "Q(a)" using 4 3 by (rule mp)
show "∃x. Q(x)" using 5 by (rule exI)
qed

lemma
assumes 1: "∀x. Q(x) ⟶ R(x)" and
2: "∃x. P(x) ∧ Q(x)"
shows "∃x. P(x) ∧ R(x)"
proof -
obtain x where 3: "P(x) ∧ Q(x)" using 2 by (rule exE)
have 5: "P(x)" using 3 by (rule conjunct1)
have 6: "Q(x) ⟶ R(x)" using 1 by (rule allE)
have 7: "Q(x)" using 3 by (rule conjunct2)
have 8: "R(x)" using 6 7 by (rule mp)
have 9: "P(x) ∧ R(x)" using 5 8 by (rule conjI)
show "∃x. P(x) ∧ R(x)" using 9 by (rule exI)
qed

lemma
assumes 1: "∃x. P(x)" and
2: "∀x.∀y. P(x) ⟶ Q(y)"
shows "∀y. Q(y)"
proof (rule allI)
fix y
obtain x where 3: "P(x)" using 1 by (rule exE)
have 4: "∀y. P(x) ⟶ Q(y)" using 2 by (rule allE)
have 5: "P(x) ⟶ Q(y)" using 4 by (rule allE)
show "Q(y)" using 5 3 by (rule mp)
qed

section {* Equivalencias *}

-- "p. 15"
lemma equivalencia_1a1:
assumes 1: "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume 2: "¬(∃x. ¬P(x))"
note 1
thus False
proof (rule notE)
show "∀x. P(x)"
proof (rule allI)
fix x
show "P(x)"
proof (rule ccontr)
assume 3: "¬P(x)"
have 4: "∃x. ¬P(x)" using 3 by (rule exI)
show False using 2 4 by (rule notE)
qed
qed
qed
qed

-- "p. 16"
lemma equivalencia_1a2:
assumes 1: "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof (rule ccontr)
assume 2: "¬¬(∀x. P(x))"
obtain x where 3: "¬P(x)" using 1 by (rule exE)
have 4: "∀x. P(x)" using 2 by (rule notnotD)
have 5: "P(x)" using 4 by (rule allE)
show False using 3 5 by (rule notE)
qed

-- "p. 17"
theorem equivalencia_1a:
"(¬(∀x. P(x))) = (∃x. ¬P(x))"
proof (rule iffI)
{ assume "¬(∀x. P x)"
thus "∃x. ¬P x" by (rule equivalencia_1a1)}
next
{ assume "∃x. ¬P x"
thus "¬(∀x. P x)" by (rule equivalencia_1a2) }
qed

-- "p. 18"
lemma equivalencia_3a1:
assumes 1: "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
show "∀x. P(x)"
proof (rule allI)
fix x
have 2: "P(x) ∧ Q(x)" using 1 by (rule allE)
show "P(x)" using 2 by (rule conjunct1)
qed
next
show "∀x. Q(x)"
proof (rule allI)
fix x
have 3: "P(x) ∧ Q(x)" using 1 by (rule allE)
show "Q(x)" using 3 by (rule conjunct2)
qed
qed

-- "p. 19"
lemma equivalencia_3a2:
assumes 1: "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof (rule allI)
fix x
have 2: "∀x. P(x)" using 1 by (rule conjunct1)
have 3: "∀x. Q(x)" using 1 by (rule conjunct2)
have 4: "P(x)" using 2 by (rule allE)
have 5: "Q(x)" using 3 by (rule allE)
show "P(x) ∧ Q(x)" using 4 5 by (rule conjI)
qed

-- "p. 20"
lemma equivalencia_3a:
"(∀x. P(x) ∧ Q(x)) = ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
{ assume "∀x. P(x) ∧ Q(x)"
thus "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule equivalencia_3a1) }
next
{ assume "(∀x. P(x)) ∧ (∀x. Q(x))"
thus "∀x. P(x) ∧ Q(x)" by (rule equivalencia_3a2) }
qed

-- "p. 21"
lemma equivalencia_3b1:
assumes 1: "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using 1
proof (rule disjE)
{ assume "∃x. P(x)"
then obtain x where "P(x)" by (rule exE)
hence "P(x) ∨ Q(x)" by (rule disjI1)
thus "∃x. P(x) ∨ Q(x)" by (rule exI) }
next
{ assume "∃x. Q(x)"
then obtain x where "Q(x)" by (rule exE)
hence "P(x) ∨ Q(x)" by (rule disjI2)
thus "∃x. P(x) ∨ Q(x)" by (rule exI) }
qed

-- "p. 22"
lemma equivalencia_3b2:
assumes 1: "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain x where 2: "P(x) ∨ Q(x)" using 1 by (rule exE)
thus "(∃x. P(x)) ∨ (∃x. Q(x))"
proof (rule disjE)
{ assume "P(x)"
hence "∃x. P(x)" by (rule exI)
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1) }
next
{ assume "Q(x)"
hence "∃x. Q(x)" by (rule exI)
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2) }
qed
qed

-- "p. 23"
lemma equivalencia_3b:
"((∃x. P(x)) ∨ (∃x. Q(x))) = (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
{ assume "(∃x. P(x)) ∨ (∃x. Q(x))"
thus "∃x. P(x) ∨ Q(x)" by (rule equivalencia_3b1) }
next
{ assume "∃x. P(x) ∨ Q(x)"
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule equivalencia_3b2) }
qed

-- "p. 24"
lemma equivalencia_4b1:
assumes 1: "∃x.∃y. P x y"
shows "∃y.∃x. P x y"
proof -
obtain x where "∃y. P x y" using 1 by (rule exE)
then obtain y where "P x y" by (rule exE)
hence "∃x. P x y" by (rule exI)
thus "∃y.∃x. P x y" by (rule exI)
qed

-- "p. 25"
theorem equivalencia_4b:
"(∃x.∃y. P x y) = (∃y.∃x. P x y)"
proof (rule iffI)
{ assume "∃x.∃y. P x y"
thus "∃y.∃x. P x y" by (rule equivalencia_4b1) }
next
{assume "∃y.∃x. P x y"
thus "∃x.∃y. P x y" by (rule equivalencia_4b1) }
qed

end
</source>

Relación 4

2018-07-16T07:48:47Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
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)"
---------------------------------------------------------------------
*}

text {*
--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_borra_auto: "borraTodas x (borra x xs) = borraTodas x xs"
by (induct xs) auto

-- "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)"
by (induct xs) auto

-- "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)"
by (induct xs arbitrary: ) (auto simp add: borraTodas_borra_auto)

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

text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocándolo para que no dé
problemas al exportarlo a Isabelle):
y = a1
x = a2
xs = [a1]
El contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
x = a1
xs = [a2]
y = a2
Análogamente, el contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
y: a0
x: a1
xs: [a0]
*}

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

text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocándolo para que no dé
problemas al exportarlo a Isabelle):
y = a1
x = a2
xs = [a1]
El contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
x = a1
xs = [a2]
y = a2
Análogamente, el contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
y: a0
x: a1
xs: [a0]
*}

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"
by (induct zs) auto

-- "La demostración estructurada es"
theorem sust_borraTodas:
"sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
show "sust x y (borraTodas x []) = borraTodas x []" by auto
next
show "⋀a zs. sust x y (borraTodas x zs) = borraTodas x zs ⟹
sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)" by auto
qed

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

text {*
Para este ejercicio quickcheck encuentra el siguiente contraejemplo:
zs = [0]
z = 1
y = 1
x = 0
*}

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_append_auto:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs) auto

-- "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)"
by (induct xs arbitrary: x) (auto simp add: borraTodas_append_auto)

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

end
</source>

Relación 10

2018-07-16T07:48:15Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional y de primer
orden:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

Deducción natural en lógica proposicional con Isabelle/Isar

2018-07-16T07:48:14Z

Jalonso:

Relación 8

2018-07-16T07:48:14Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

<source lang="isabelle">
theory Relacion_8
imports Main Efficient_Nat Relacion_3
begin

section {* Suma y aplanamiento de listas *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
suma :: "nat list ⇒ nat"
tal que (suma xs) es la suma de los elementos de la lista de números
naturales xs. Por ejemplo,
suma [3::nat,2,4] = 9
---------------------------------------------------------------------
*}

primrec suma :: "nat list ⇒ nat" where
"suma [] = 0"
| "suma (x#xs) = x + suma xs"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
aplana :: "'a list list ⇒ 'a list"
tal que (aplana xss) es la obtenida concatenando los miembros de la
lista de listas "xss". Por ejemplo,
aplana [[2,3], [4,5], [7,9]] = [2,3,4,5,7,9]
---------------------------------------------------------------------
*}

primrec aplana :: "'a list list ⇒ 'a list" where
"aplana [] = []"
| "aplana (xs#xss) = xs @ aplana xss"

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
length (aplana xs) = suma (map length xs)
---------------------------------------------------------------------
*}

text {*
La igualdad propuesta es verdadera y se puede demostrar
de forma automática como sigue.
*}

lemma "length (aplana xs) = suma (map length xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}

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

text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
aplana (xs @ ys) = (aplana xs) @ (aplana ys)
---------------------------------------------------------------------
*}

lemma "aplana (xs @ ys) = (aplana xs) @ (aplana ys)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
aplana (map rev (rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}

text {*
El ejercicio debería de comenzar de la siguiente manera:
*}
lemma "aplana (map rev (rev xs)) = rev (aplana xs)"
proof (induct xs)
show "aplana (map rev (rev [])) = rev (aplana [])" by simp
next
fix b xs
assume HI: "aplana (map rev (rev xs)) = rev (aplana xs)"
thus "aplana (map rev (rev (b # xs))) = rev (aplana (b # xs))"
proof -
oops

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
aplana (rev (map rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar
list_all (list_all P) xs = list_all P (aplana xs)
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar
aplana (rev xs) = aplana xs
---------------------------------------------------------------------
*}

lemma "aplana (rev xs) = aplana xs"
quickcheck
oops

text {* El contraejemplo encontrado es xs = [[2], [1, 2]]. Esto tiene
sentido ya que el orden influye en la funcion aplanar *}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar
suma (rev xs) = suma xs
---------------------------------------------------------------------
En cambio este ejercicio respecto al anterior tiene sentido que haya
que demostrarlo, ya que el orden en la suma no afecta, por lo que no se
encontrará ningún contra ejemplo.
*}

lemma "suma (rev xs) = suma xs"
proof (induct xs)
show "suma (rev []) = suma []" by simp
next
fix b xs
assume HI: "suma (rev xs) = suma xs"
thus "suma (rev (b # xs)) = suma (b # xs)"
proof -
oops
text{*
En teoria debería de continuarse con una sentencia parecida a la siguiente:
have "suma (rev (b # xs)) = suma (rev [b] @ xs)" by auto
*}

text {*
---------------------------------------------------------------------
Ejercicio 11. Buscar un predicado P para que se verifique la siguiente
propiedad
list_all P xs ⟶ length xs ≤ suma xs
---------------------------------------------------------------------
*}

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

text {*
---------------------------------------------------------------------
Ejercicio 13. Redefinir, usando la función list_all, la función
algunos. Llamar la nueva función algunos2 y demostrar que es
equivalente a algunos.
---------------------------------------------------------------------
*}

text {*
La siguiente definición se construye utilizando la palabra reservada
"definition". Aunque se trata de una función recursiva primitiva no
es necesario utilizar la palabra reservada "primrec" porque la función
"list_all" está definida recursivamente o en la cadena de definiciones de
la que depende, hay una función definida recursivamente.
*}

definition algunos2 :: "('a => bool) => 'a list => bool" where
"algunos2 P xs ≡ ¬ list_all (λx. ¬ P x) xs"

end
</source>

Rel 1

2018-07-16T07:48:01Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Rel 10

2018-07-16T07:47:34Z

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

MediaWiki:Common.css

2018-07-16T07:42:13Z

Jalonso: Página creada con «/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */ @import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");»

/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */
@import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");

MediaWiki:Sidebar

2013-02-24T17:38:44Z

Jalonso:

* navigation
** Razonamiento automático|Inicial
** recentchanges-url|recentchanges

MediaWiki:Sidebar

2013-02-24T17:38:11Z

Jalonso:

* navigation
** Razonamiento automático|Inicial
** recentchanges-url|recentchanges
** helppage|help
* SEARCH
* LANGUAGES

Ejercicios de "Razonamiento automático (2011-12)"

2013-02-24T17:24:26Z

Jalonso: Página creada con ' __NOTOC__ == Ejercicios de "Razonamiento automático" == === Ejemplos === * Deducción natural en lógica proposicional con Isabelle/Isar. * [[Deducción natural en lógic...'

__NOTOC__
== Ejercicios de "Razonamiento automático" ==

=== Ejemplos ===
* [[Deducción natural en lógica proposicional con Isabelle/Isar]].
* [[Deducción natural en lógica de primer orden con Isabelle/Isar]].

=== Relaciones de ejercicios ===

==== Ejercicios de deducción natural ====
* '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1|Enunciado]]).
* '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2|Enunciado]]).

==== Razonamiento por inducción sobre listas ====
* '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3|Enunciado]]).
* '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4|Enunciado]]).
* '''Relación 5''': Menor posición válida. ([[Rel_5|Enunciado]]).
* '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]]).
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]]).
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]]).

==== Ejercicios complementarios ====
* '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]]).
* '''Relación 10''': Deducción natural en lógica de primer orden. ([[Rel_10|Enunciado]]).
* '''Relación 11''': Razonamiento sobre programas. ([[Rel_11|Enunciado]]).

Rel 3

2012-02-11T07:23:14Z

Jalonso:

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

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

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

MediaWiki:Mainpage

2012-02-02T18:58:27Z

Jalonso:

Razonamiento automático

MediaWiki:Sidebar

2012-02-02T18:54:37Z

Jalonso:

* navigation
** Razonamiento automático|Inicial
** recentchanges-url|recentchanges
** helppage|help
* SEARCH
* TOOLBOX
* LANGUAGES

Razonamiento automático

2012-02-02T18:54:09Z

Jalonso: Razonamiento automático (2010-11) trasladada a Razonamiento automático

Razonamiento automático (2010-11)

2012-02-02T18:54:09Z

Jalonso: Razonamiento automático (2010-11) trasladada a Razonamiento automático

#REDIRECCIÓN [[Razonamiento automático]]

Razonamiento automático

2012-02-02T18:44:21Z

Jalonso:

Razonamiento automático

2012-02-02T18:43:40Z

Jalonso:

== Ejercicios de "Razonamiento automático" ==

=== Ejemplos ===
* [[Deducción natural en lógica proposicional con Isabelle/Isar]].
* [[Deducción natural en lógica de primer orden con Isabelle/Isar]].

=== Relaciones de ejercicios ===

==== Ejercicios de deducción natural ====
* '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1|Enunciado]]).
* '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2|Enunciado]]).

==== Razonamiento por inducción sobre listas ====
* '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3|Enunciado]]).
* '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4|Enunciado]]).
* '''Relación 5''': Menor posición válida. ([[Rel_5|Enunciado]]).
* '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]]).
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]]).
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]]).

==== Ejercicios complementarios ====
* '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]]).
* '''Relación 10''': Deducción natural en lógica de primer orden. ([[Rel_10|Enunciado]]).
* '''Relación 11''': Razonamiento sobre programas. ([[Rel_11|Enunciado]]).

Razonamiento automático

2012-02-02T18:43:20Z

Jalonso:

== Ejercicios de "Razonamiento automático"

=== Ejemplos ===
* [[Deducción natural en lógica proposicional con Isabelle/Isar]].
* [[Deducción natural en lógica de primer orden con Isabelle/Isar]].

=== Relaciones de ejercicios ===

==== Ejercicios de deducción natural ====
* '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1|Enunciado]]).
* '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2|Enunciado]]).

==== Razonamiento por inducción sobre listas ====
* '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3|Enunciado]]).
* '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4|Enunciado]]).
* '''Relación 5''': Menor posición válida. ([[Rel_5|Enunciado]]).
* '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]]).
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]]).
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]]).

==== Ejercicios complementarios ====
* '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]]).
* '''Relación 10''': Deducción natural en lógica de primer orden. ([[Rel_10|Enunciado]]).
* '''Relación 11''': Razonamiento sobre programas. ([[Rel_11|Enunciado]]).

Relación 9

2011-03-24T09:38:42Z

Jalonso:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1b:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_5:
assumes 1: "p⟶(q⟶r)"
shows "q⟶(p⟶r)"
oops

lemma ejercicio_6:
assumes 1: "p⟶(q⟶r)"
shows "(p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
assumes 1: "p"
shows "q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
assumes 1: "p⟶q"
shows "(q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
assumes 1: "p⟶(q⟶(r⟶s))"
shows "r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
assumes 1: "(p⟶q)⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_13:
assumes 1: "p" and
2: "q"
shows "p∧q"
oops

lemma ejercicio_14:
assumes 1: "p∧q"
shows "p"
oops

lemma ejercicio_15:
assumes 1: "p∧q"
shows "q"
oops

lemma ejercicio_16:
assumes 1: "p∧(q∧r)"
shows "(p∧q)∧r"
oops

lemma ejercicio_17:
assumes 1: "(p∧q)∧r"
shows "p∧(q∧r)"
oops

lemma ejercicio_18:
assumes 1: "p∧q"
shows "p⟶q"
oops

lemma ejercicio_19:
assumes 1: "(p⟶q)∧(p⟶r)"
shows "p⟶q∧r"
oops

lemma ejercicio_20:
assumes 1: "p⟶q∧r"
shows "(p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
assumes 1: "p⟶(q⟶r)"
shows "p∧q⟶r"
oops

lemma ejercicio_22:
assumes 1: "p∧q⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_23:
assumes 1: "(p⟶q)⟶r"
shows "p∧q⟶r"
oops

lemma ejercicio_24:
assumes 1: "p∧(q⟶r)"
shows "(p⟶q)⟶r"
oops

lemma ejercicio_25:
assumes 1: "p"
shows "p∨q"
oops

lemma ejercicio_26:
assumes 1: "q"
shows "p∨q"
oops

lemma ejercicio_27:
assumes 1: "p∨q"
shows "q∨p"
oops

lemma ejercicio_28:
assumes 1: "q⟶r"
shows "p∨q⟶p∨r"
oops

lemma ejercicio_29:
assumes 1: "p∨p"
shows "p"
oops

lemma ejercicio_30:
assumes 1: "p"
shows "p∨p"
oops

lemma ejercicio_31:
assumes 1: "p∨(q∨r)"
shows "(p∨q)∨r"
oops

lemma ejercicio_32:
assumes 1: "(p∨q)∨r"
shows "p∨(q∨r)"
oops

lemma ejercicio_33:
assumes 1: "p∧(q∨r)"
shows "(p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
assumes 1: "(p∧q)∨(p∧r)"
shows "p∧(q∨r)"
oops

lemma ejercicio_35:
assumes 1: "p∨(q∧r)"
shows "(p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
assumes 1: "(p∨q)∧(p∨r)"
shows "p∨(q∧r)"
oops

lemma ejercicio_37:
assumes 1: "(p⟶r)∧(q⟶r)"
shows "p∨q⟶r"
oops

lemma ejercicio_38:
assumes 1: "p∨q⟶r"
shows "(p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
assumes 1: "p"
shows "¬¬p"
oops

lemma ejercicio_40:
assumes 1: "¬p"
shows "p⟶q"
oops

lemma ejercicio_41:
assumes 1: "p⟶q"
shows "¬q⟶¬p"
oops

lemma ejercicio_42:
assumes 1: "p∨q" and
2: "¬q"
shows "p"
oops

lemma ejercicio_43:
assumes 1: "p∨q" and
2: "¬p"
shows "q"
oops

lemma ejercicio_44:
assumes 1: "p∨q"
shows "¬(¬p∧¬q)"
oops

lemma ejercicio_45:
assumes 1: "p∧q"
shows "¬(¬p∨¬q)"
oops

lemma ejercicio_46:
assumes 1: "¬(p∨q)"
shows "¬p∧¬q"
oops

lemma ejercicio_47:
assumes 1: "¬p∧¬q"
shows "¬(p∨q)"
oops

lemma ejercicio_48:
assumes 1: "¬p∨¬q"
shows "¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
assumes 1: "p∧¬p"
shows "q"
oops

lemma ejercicio_51:
assumes 1: "¬¬p"
shows "p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
assumes 1: "¬q⟶¬p"
shows "p⟶q"
oops

lemma ejercicio_55:
assumes 1: "¬(¬p∧¬q)"
shows "p∨q"
oops

lemma ejercicio_56:
assumes 1: "¬(¬p∨¬q)"
shows "p∧q"
oops

lemma ejercicio_57:
assumes 1: "¬(p∧q)"
shows "¬p∨¬q"
oops

lemma ejercicio_58:
"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-24T09:38:20Z

Jalonso:

<source lang=isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1b:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_5:
assumes 1: "p⟶(q⟶r)"
shows "q⟶(p⟶r)"
oops

lemma ejercicio_6:
assumes 1: "p⟶(q⟶r)"
shows "(p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
assumes 1: "p"
shows "q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
assumes 1: "p⟶q"
shows "(q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
assumes 1: "p⟶(q⟶(r⟶s))"
shows "r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
assumes 1: "(p⟶q)⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_13:
assumes 1: "p" and
2: "q"
shows "p∧q"
oops

lemma ejercicio_14:
assumes 1: "p∧q"
shows "p"
oops

lemma ejercicio_15:
assumes 1: "p∧q"
shows "q"
oops

lemma ejercicio_16:
assumes 1: "p∧(q∧r)"
shows "(p∧q)∧r"
oops

lemma ejercicio_17:
assumes 1: "(p∧q)∧r"
shows "p∧(q∧r)"
oops

lemma ejercicio_18:
assumes 1: "p∧q"
shows "p⟶q"
oops

lemma ejercicio_19:
assumes 1: "(p⟶q)∧(p⟶r)"
shows "p⟶q∧r"
oops

lemma ejercicio_20:
assumes 1: "p⟶q∧r"
shows "(p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
assumes 1: "p⟶(q⟶r)"
shows "p∧q⟶r"
oops

lemma ejercicio_22:
assumes 1: "p∧q⟶r"
shows "p⟶(q⟶r)"
oops

lemma ejercicio_23:
assumes 1: "(p⟶q)⟶r"
shows "p∧q⟶r"
oops

lemma ejercicio_24:
assumes 1: "p∧(q⟶r)"
shows "(p⟶q)⟶r"
oops

lemma ejercicio_25:
assumes 1: "p"
shows "p∨q"
oops

lemma ejercicio_26:
assumes 1: "q"
shows "p∨q"
oops

lemma ejercicio_27:
assumes 1: "p∨q"
shows "q∨p"
oops

lemma ejercicio_28:
assumes 1: "q⟶r"
shows "p∨q⟶p∨r"
oops

lemma ejercicio_29:
assumes 1: "p∨p"
shows "p"
oops

lemma ejercicio_30:
assumes 1: "p"
shows "p∨p"
oops

lemma ejercicio_31:
assumes 1: "p∨(q∨r)"
shows "(p∨q)∨r"
oops

lemma ejercicio_32:
assumes 1: "(p∨q)∨r"
shows "p∨(q∨r)"
oops

lemma ejercicio_33:
assumes 1: "p∧(q∨r)"
shows "(p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
assumes 1: "(p∧q)∨(p∧r)"
shows "p∧(q∨r)"
oops

lemma ejercicio_35:
assumes 1: "p∨(q∧r)"
shows "(p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
assumes 1: "(p∨q)∧(p∨r)"
shows "p∨(q∧r)"
oops

lemma ejercicio_37:
assumes 1: "(p⟶r)∧(q⟶r)"
shows "p∨q⟶r"
oops

lemma ejercicio_38:
assumes 1: "p∨q⟶r"
shows "(p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
assumes 1: "p"
shows "¬¬p"
oops

lemma ejercicio_40:
assumes 1: "¬p"
shows "p⟶q"
oops

lemma ejercicio_41:
assumes 1: "p⟶q"
shows "¬q⟶¬p"
oops

lemma ejercicio_42:
assumes 1: "p∨q" and
2: "¬q"
shows "p"
oops

lemma ejercicio_43:
assumes 1: "p∨q" and
2: "¬p"
shows "q"
oops

lemma ejercicio_44:
assumes 1: "p∨q"
shows "¬(¬p∧¬q)"
oops

lemma ejercicio_45:
assumes 1: "p∧q"
shows "¬(¬p∨¬q)"
oops

lemma ejercicio_46:
assumes 1: "¬(p∨q)"
shows "¬p∧¬q"
oops

lemma ejercicio_47:
assumes 1: "¬p∧¬q"
shows "¬(p∨q)"
oops

lemma ejercicio_48:
assumes 1: "¬p∨¬q"
shows "¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
assumes 1: "p∧¬p"
shows "q"
oops

lemma ejercicio_51:
assumes 1: "¬¬p"
shows "p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
assumes 1: "¬q⟶¬p"
shows "p⟶q"
oops

lemma ejercicio_55:
assumes 1: "¬(¬p∧¬q)"
shows "p∨q"
oops

lemma ejercicio_56:
assumes 1: "¬(¬p∨¬q)"
shows "p∧q"
oops

lemma ejercicio_57:
assumes 1: "¬(p∧q)"
shows "¬p∨¬q"
oops

lemma ejercicio_58:
"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 11

2011-03-15T05:26:51Z

Jalonso: Página creada con '<source lang="isar"> header {* Razonamiento sobre programas en Isabelle *} theory Relacion_11 imports Main Efficient_Nat begin text {* ----------------------------------------...'

<source lang="isar">
header {* Razonamiento sobre programas en Isabelle *}

theory Relacion_11
imports Main Efficient_Nat
begin

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

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 3. 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 (2,3) = (3,2)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 5. 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 [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 14. 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 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 17. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

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

text {* ---------------------------------------------------------------
Ejercicio 23. 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]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 26. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 28. 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 30. 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 2 = [2,2,2]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. 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
Nota; La conjunción se representa por ∧
------------------------------------------------------------------ *}

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

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

text {* ---------------------------------------------------------------
Ejercicio 34. Se considera la siguiente definición iterativa de la
función factorial
factI :: Integer -> Integer
factI n = factI' n 1

factI' :: Integer -> Integer -> Integer
factI' 0 x = x -- factI'.1
factI' (n+1) x = factI' n (n+1)*x -- factI'.2
Comprobar con QuickCheck que factI y factR son equivalentes sobre los
números naturales.
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
y, como corolario, que
factI n = factR n
------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------
Ejercicio 36. 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 [2,5] 3 = [2,5,3]
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

end
</source>

Rel 11

2011-03-15T05:26:17Z

Razonamiento automático

2011-03-15T05:25:17Z

Jalonso: /* Ejercicios complementarios */

== Razonamiento automático (2010-11) ==

=== Ejemplos ===
* [[Deducción natural en lógica proposicional con Isabelle/Isar]].
* [[Deducción natural en lógica de primer orden con Isabelle/Isar]].

=== Relaciones de ejercicios ===

==== Ejercicios de deducción natural ====
* '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1|Enunciado]] y [[Relación 1|Solución]]).
* '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2|Enunciado]] y [[Relación 2|Solución]]).

==== Razonamiento por inducción sobre listas ====
* '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3|Enunciado]] y [[Relación 3|Solución]]).
* '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4|Enunciado]] y [[Relación 4|Solución]]).
* '''Relación 5''': Menor posición válida. ([[Rel_5|Enunciado]] y [[Relación 5|Solución]]).
* '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]] y [[Relación 6|Solución]]).
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]] y [[Relación 7|Solución]]).
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]] y [[Relación 8|Solución]]).

==== Ejercicios complementarios ====
* '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]] y [[Relación 9|Solución]]).
* '''Relación 10''': Deducción natural en lógica de primer orden. ([[Rel_10|Enunciado]] y [[Relación 10|Solución]]).
* '''Relación 11''': Razonamiento sobre programas. ([[Rel_11|Enunciado]] y [[Relación 11|Solución]]).

Relación 10

2011-03-15T05:14:41Z

Jalonso: Página creada con '<source lang="isar"> theory Relacion_10 imports Main begin section {* Deducción natural de primer orden *} text {* Los ejercicios de esta relación deben de resolverse usan...'

<source lang="isar">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional y de primer
orden:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

Rel 10

2011-03-15T05:14:13Z

Jalonso: Protegió «Rel 10» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Rel 10

2011-03-15T05:13:56Z

Jalonso:

Rel 10

2011-03-15T05:13:09Z

Jalonso:

<source lang="isar">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional y de primer orden:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

Rel 10

2011-03-15T05:11:42Z

<source lang="isar">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
y se primer orden
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

Razonamiento automático

2011-03-15T05:10:46Z

Jalonso: /* Ejercicios complementarios */

Relación 9

2011-03-14T20:57:47Z

Jalonso: Página creada con '<source lang="isar"> theory Relacion_9 imports Main begin section {* Deducción natural proposicional *} text {* Los ejercicios de esta relación deben de resolverse usando ...'

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
oops

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
oops

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
oops

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
oops

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>