Razonamiento automático (2013-14) - Contribuciones del usuario [es]

Relación 12

2014-03-10T01:14:56Z

Zoiruicha:

<source lang="isar">
header {* R12: Representación de fórmulas proposicionales mediante
polinomios *}

theory R12
imports Main
begin

text {*
El objetivo de esta relación es definir un procedimiento para
transformar fórmulas proposicionales (construidas con ⊤, ∧ y ⊕) en
polinomios de la forma
(p₁ ∧ … ∧ pₙ) ⊕ … ⊕ (q₁ ∧ … ∧ qₘ)
y demostrar que, para cualquier interpretación I, el valor de las
fórmulas coincide con la de su correspondiente polinomio. *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Las fórmulas proposicionales pueden definirse mediante
las siguientes reglas:
· ⊤ es una fórmula proposicional
· Las variables proposicionales p_1, p_2, … son fórmulas
proposicionales,
· Si F y G son fórmulas proposicionales, entonces (F ∧ G) y (F ⊕ G)
también lo son.
donde ⊤ es una fórmula que siempre es verdadera, ∧ es la conjunción y
⊕ es la disyunción exclusiva.

Definir el tipo de datos form para representar las fórmulas
proposicionales usando
· T en lugar de ⊤,
· (Var i) en lugar de p_i,
· (And F G) en lugar de (F ∧ G) y
· (Xor F G) en lugar de (F ⊕ G).
------------------------------------------------------------------ *}

datatype form = T | Var nat | And form form | Xor form form

text {*
---------------------------------------------------------------------
Ejercicio 2. Los siguientes ejemplos de fórmulas
form1 = p0 ⊕ ⊤
form2 = (p0 ⊕ p1) ⊕ (p0 ∧ p1)
es usará en lo que sigue.
------------------------------------------------------------------ *}

abbreviation form1 :: "form" where
"form1 ≡ Xor (Var 0) T"
abbreviation form2 :: "form" where
"form2 ≡ Xor (Xor (Var 0) (Var 1)) (And (Var 0) (Var 1))"

text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
xor :: bool ⇒ bool ⇒ bool
tal que (xor p q) es el valor de la disyunción exclusiva de p y q. Por
ejemplo,
xor False True = True
------------------------------------------------------------------ *}

--"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla"
-- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva"
-- "jaisalmen: de la definicion de xor: p xor q = ( p∧¬ q) or (¬ p ∧ q)"
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor x y ≡ (x∧¬y)∨(¬x∧y)"

text {*
---------------------------------------------------------------------
Ejercicio 4. Una interpretación es una aplicación de los naturales en
los booleanos. Definir las siguientes interpretaciones
| p0 | p1 | p2 | p3 | ...
int1 | F | F | F | F | ...
int2 | F | V | F | F | ...
int3 | V | F | F | F | ...
int3 | V | V | F | F | ...
------------------------------------------------------------------ *}

abbreviation int1 :: "nat ⇒ bool" where
"int1 x ≡ False"
abbreviation int2 :: "nat ⇒ bool" where
"int2 ≡ int1 (1 := True)"
abbreviation int3 :: "nat ⇒ bool" where
"int3 ≡ int1 (0 := True)"
abbreviation int4 :: "nat ⇒ bool" where
"int4 ≡ int1 (0 := True, 1 := True)"

text {*
---------------------------------------------------------------------
Ejercicio 5. Dada una interpretación I, el valor de de una fórmula F
repecto de I, I(F), se define por
· T, si F es ⊤;
· I(n), si F es p_n;
· I(G) ∧ I(H), si F es (G ∧ H);
· I(G) ⊕ I(H), si F es (G ⊕ H).

Definir la función
valorF :: (nat ⇒ bool) ⇒ form ⇒ bool
tal que (valorF i f) es el valor de la fórmula f respecto de la
interpretación i. Por ejemplo,
valorF int1 form1 = True
valorF int3 form1 = False
valorF int1 form2 = False
valorF int2 form2 = True
valorF int3 form2 = True
valorF int4 form2 = True
--------------------------------------------------------------------- *}

--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
"valorF i T = True"
| "valorF i (Var n) = i n"
| "valorF i (And G H) = ((valorF i G) ∧ (valorF i H))"
| "valorF i (Xor G H) = xor (valorF i G) (valorF i H)"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un monomio es una lista de números naturales y se puede
interpretar como la conjunción de variables proposionales cuyos
índices son los números de la lista. Por ejemplo, el monomio [0,2,1]
se interpreta como la fórmula (p0 ∧ p2 ∧ p1).

Definir la función
formM :: nat list ⇒ form
tal que (formM m) es la fórmula correspondiente al monomio. Por
ejemplo,
formM [0,2,1] = And (Var 0) (And (Var 2) (And (Var 1) T))
--------------------------------------------------------------------- *}

--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
fun formM :: "nat list ⇒ form" where
"formM [] = T"
| "formM (x#xs) = And (Var x) (formM xs)"

value "formM [0,2,1]"

text {*
---------------------------------------------------------------------
Ejercicio 7. Definir, por recursión, la función
valorM :: (nat ⇒ bool) ⇒ nat list ⇒ bool
tal que (valorM i m) es el valor de la fórmula representada por el
monomio m en la interpretación i. Por ejemplo,
valorM int1 [0,2,1] = False
valorM (int1(0:=True,1:=True,2:=True)) [0,2,1] = True
Demostrar que, para toda interpretación i y todo monomio m, se tiene
que
valorM i m = valorF i (formM m)
--------------------------------------------------------------------- *}

--"diecabmen1 irealetei maresccas4 marescpla"
fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where
"valorM i [] = True"
| "valorM i (x#xs) = ((valorF i (Var x)) ∧ (valorM i xs))" --"Aquí he quitado algún paréntesis, pero la solución es, en esencia, la misma."

value "valorM int1 [0,2,1]"
value "valorM (int1(0:=True,1:=True,2:=True)) [0,2,1]"

--"diecabmen1 irealetei"
lemma correccion_valorM:
"valorM i m = valorF i (formM m)"
by (induct m) auto

--"diecabmen1"
lemma correccion_valorM2:
"valorM i m = valorF i (formM m)" (is "?P i m")
proof (induct m)
show "?P i []" by simp
next
fix a m
assume HI: "?P i m"
then show "?P i (a#m)" by simp
qed

--"irealetei maresccas4 marescpla"
lemma correccion_valorM_detalle:
"valorM i m = valorF i (formM m)"
proof (induct m)
show "valorM i [] = valorF i (formM [])" by simp
next
fix a m
assume HI:"valorM i m = valorF i (formM m)"
have "valorM i (a # m) = (valorF i (Var a) ∧ valorM i m)" by simp
also have "... = (valorF i (Var a) ∧ valorF i (formM m))" using HI by simp
also have "... = valorF i (formM (a # m))" by simp
finally show "valorM i (a # m) = valorF i (formM (a # m))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Un polinomio es una lista de monomios y se puede
interpretar como la disyunción exclusiva de los monomios. Por ejemplo,
el polinomio [[0,2,1],[1,3]] se interpreta como la fórmula
(p0 ∧ p2 ∧ p1) ⊕ (p1 ∧ p3).

Definir la función
formP :: nat list list ⇒ form
tal que (formP p) es la fórmula correspondiente al polinomio p. Por
ejemplo,
formP [[1,2],[3]]
= Xor (And (Var 1) (And (Var 2) T)) (Xor (And (Var 3) T) (Xor T T))
--------------------------------------------------------------------- *}

--"diecabmen1 irealetei maresccas4 marescpla"
fun formP :: "nat list list ⇒ form" where
"formP [] = Xor T T"
| "formP (x#xs) = Xor (formM x) (formP xs)"

value "formP [[1,2],[3]]"

text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
valorP :: (nat ⇒ bool) ⇒ nat list list ⇒ bool
tal que (valorP i p) es el valor de la fórmula representada por el
polinomio p en la interpretación i. Por ejemplo,
valorP (int1(1:=True,3:=True)) [[0,2,1],[1,3]] = True
Demostrar que, para toda interpretación i y todo polinomio p, se tiene
que
valorM i p = valorF i (formP p)
--------------------------------------------------------------------- *}

--"diecabmen1 irealetei"
fun valorP :: "(nat ⇒ bool) ⇒ nat list list ⇒ bool" where
"valorP i [] = xor True True"
| "valorP i (x#xs) = xor (valorM i x) (valorP i xs)"

value "valorP (int1(1:=True,3:=True)) [[0,2,1],[1,3]]"
lemma correccion_valorP:
"valorP i p = valorF i (formP p)"
by (induct p) (auto simp add:correccion_valorM)

-- "irealetei"
lemma correccion_valorP_detalle:
"valorP i p = valorF i (formP p)"
proof (induct p)
show "valorP i [] = valorF i (formP [])" by simp
next
fix a p
assume HI:"valorP i p = valorF i (formP p)"
have "valorP i (a # p) = xor (valorM i a) (valorP i p)" by simp
also have "... = xor (valorF i (formM a)) (valorP i p) " by (simp add:correccion_valorM)
also have "... = xor (valorF i (formM a)) (valorF i (formP p))" using HI by simp
also have "... = valorF i (formP (a # p))" by simp
finally show " valorP i (a # p) = valorF i (formP (a # p))" by simp
qed

-- "maresccas4"
fun valorP4 :: "(nat ⇒ bool) ⇒ nat list list ⇒ bool" where
"valorP4 i [] = False"
| "valorP4 i (x#xs) = xor (valorM i x) (valorP4 i xs)"

value "valorP4 (int1(1:=True,3:=True)) [[0,2,1],[1,3]]"

lemma correccion_valorP4:
"valorP4 i p = valorF i (formP p)"
proof (induct p)
show "valorP4 i [] = valorF i (formP [])" by (simp add:xor_def)
next
fix x xs
assume HI: "valorP4 i xs = valorF i (formP xs)"
have "valorP4 i (x#xs) = xor (valorM i x) (valorP4 i xs)" by simp
also have "... = xor (valorM i x) (valorF i (formP xs))" using HI by simp
also have "... = valorF i (Xor (formM x) (formP xs))" by (simp add: correccion_valorM)
also have "... = valorF i (formP (x#xs))" by simp
finally show "valorP4 i (x#xs) = valorF i (formP (x#xs))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
productoM :: nat list ⇒ nat list list ⇒ nat list list
tal que (productoM m p) es el producto del monomio p por el polinomio
p. Por ejemplo,
productoM [1,3] [[1,2,4],[7],[4,1]]
= [[1,3,1,2,4],[1,3,7],[1,3,4,1]]
--------------------------------------------------------------------- *}

--"diecabmen1"
fun productoM :: "nat list ⇒ nat list list ⇒ nat list list" where
"productoM m [] = []"
| "productoM m (x#xs) = [m@x] @ (productoM m xs)"

--"irealetei maresccas4"
fun productoM2 :: "nat list ⇒ nat list list ⇒ nat list list" where
"productoM2 m [] = []"
| "productoM2 m (a#ns) = (m@a)#(productoM2 m ns)"

value "productoM [1,3] [[1,2,4],[7],[4,1]]"

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que, en cualquier interpretación i, el valor
de la concatenación de dos monomios es la conjunción de sus valores.
--------------------------------------------------------------------- *}

--"diecabmen1"
lemma valorM_conc:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)" (is "?P i xs ys")
proof (induct xs)
show "?P i [] ys" by simp
next
fix a xs
assume HI: "?P i xs ys"
then show "?P i (a#xs) ys" by simp
qed

--"irealetei maresccas4"
lemma valorM_conc_auto:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
by (induct xs) auto

lemma valorM_conc_detalle:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
proof (induct xs)
show "valorM i ([] @ ys) = (valorM i [] ∧ valorM i ys)" by simp
next
fix a xs
assume HI:"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
have "valorM i ((a # xs) @ ys) = (valorF i (Var a) ∧ valorM i (xs @ ys))" by simp
also have "... = (valorF i (Var a) ∧ (valorM i xs ∧ valorM i ys))" using HI by simp
also have "... = (valorM i (a # xs) ∧ valorM i ys)" by simp
finally show "valorM i ((a # xs) @ ys) = (valorM i (a # xs) ∧ valorM i ys)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar que, en cualquier interpretación i, el valor
del producto de un monomio por un polinomio es la conjunción de sus
valores.
--------------------------------------------------------------------- *}

--"irealetei"

lemma xor_compl: "xor (a ∧ p) (a ∧ q) = (a ∧ (xor p q))"
proof -
have "xor (a ∧ p) (a ∧ q) = (((a ∧ p) ∧ ¬(a ∧ q)) ∨ (¬(a ∧ p) ∧ (a ∧ q)))" by (simp add:xor_def)
also have "... = (a ∧ ((p ∧ ¬q) ∨ (¬p ∧ q)))" by auto
also have "... = (a ∧ (xor p q))" by (simp add:xor_def)
finally show "xor (a ∧ p) (a ∧ q) = (a ∧ (xor p q))" by simp
qed

-- "No me hacía falta definir el xor_neg, anterior, que es como matar moscas a cañonazos"
lemma correccion_productoM:
"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
proof (induct p)
have "valorP i (productoM m []) = valorP i []" by simp
also have "... = (valorM i m ∧ valorP i [])" by (simp add:xor_def)
then show "valorP i (productoM m []) = (valorM i m ∧ valorP i [])" by simp
next
fix a p
assume HI:"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
have "valorP i (productoM m (a # p)) = valorP i ((m@a)#(productoM m p))" by simp
also have "... = xor (valorM i (m@a)) (valorP i (productoM m p))" by simp
also have "... = xor (valorM i (m@a)) (valorM i m ∧ valorP i p)" using HI by simp
also have "... = xor (valorM i m ∧ valorM i a) (valorM i m ∧ valorP i p)" by (simp add:valorM_conc)
also have "... = (valorM i m ∧ xor (valorM i a) (valorP i p))" by (simp add:xor_compl)
also have "... = (valorM i m ∧ valorP i (a # p))" by simp
finally show "valorP i (productoM m (a # p)) = (valorM i m ∧ valorP i (a # p))" by simp
qed

lemma correccion_productoM_auto:
"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
by (induct p) (auto simp add:xor_def valorM_conc xor_compl)

-- "maresccas4"
lemma lema1: "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))"
proof (cases a)
assume H: "a"
then show "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))" by simp
next
assume H: "¬a"
then show "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))" by (simp add: xor_def)
qed

lemma correccion_productoM:
"valorP4 i (productoM m p) = (valorM i m ∧ valorP4 i p)"
proof (induct p)
show "valorP4 i (productoM m []) = (valorM i m ∧ valorP4 i [])" by simp
next
fix p px
assume HI: "valorP4 i (productoM m px) = (valorM i m ∧ valorP4 i px)"
have "valorP4 i (productoM m (p#px)) = valorP4 i ((m@p) # productoM m px)" by simp
also have "... = xor (valorF i (formM (m@p))) (valorP4 i (productoM m px))" by (simp add: correccion_valorM)
also have "... = xor (valorF i (formM (m@p))) (valorM i m ∧ valorP4 i px)" using HI by simp
also have "... = xor (valorM i (m @ p)) (valorM i m ∧ valorP4 i px)" by (simp add: correccion_valorM)
also have "... = xor (valorM i m ∧ valorM i p) (valorM i m ∧ valorP4 i px)" by (simp add: valorM_conc)
also have "... = (valorM i m ∧ (xor (valorM i p) (valorP4 i px)))" by (simp add: lema1)
also have "... = (valorM i m ∧ valorP4 i (p#px))" by simp
finally show "valorP4 i (productoM m (p#px)) = (valorM i m ∧ valorP4 i (p#px))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 13. Definir la función
producto :: nat list list ⇒ nat list list ⇒ nat list list
tal que (producto p q) es el producto de los polinomios p y q. Por
ejemplo,
producto [[1,3],[2]] [[1,2,4],[7],[4,1]]
= [[1,3,1,2,4],[1,3,7],[1,3,4,1],[2,1,2,4],[2,7],[2,4,1]]
--------------------------------------------------------------------- *}

--"irealetei: tenía una de más que no valía para nada, se me queda igual que maresccas4"

fun producto :: "nat list list ⇒ nat list list ⇒ nat list list" where
"producto [] q = []"
| "producto (a1 # p) (q) = (productoM a1 q)@(producto p q)"

value "producto [[1,3],[2]] [[1,2,4],[7],[4,1]]"

-- "maresccas4"
fun producto4 :: "nat list list ⇒ nat list list ⇒ nat list list" where
"producto [] q = []"
| "producto (m#p) q = (productoM m q) @ (producto p q)"

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que, en cualquier interpretación i, el valor
de la concatenación de dos polinomios es la disyunción exclusiva de
sus valores.
--------------------------------------------------------------------- *}

-- "maresccas4 irealetei"

-- "Si me da tiempo, intentaré probar este lema. Irealetei: lo estoy intentando pero me he quedado en: '((a ∧ (¬b ∨ c) ∧ (b∨¬c)) ∨ (¬a ∧ ((b∧¬c) ∨ (¬b∧c ))))' y me va a petar el cerebro..."

lemma lema2: "xor a (xor b c) = xor (xor a b) c"
by (auto simp add: xor_def)

-- "Me ha dado tiempo. De forma análoga al lema1"
lemma lema2_simp: "xor a (xor b c) = xor (xor a b) c"
proof (cases a)
assume "a"
show "xor a (xor b c) = xor (xor a b) c"
proof (cases b)
assume "b"
then show "xor a (xor b c) = xor (xor a b) c" using `a` by (simp add: xor_def)
next
assume "¬b"
then show "xor a (xor b c) = xor (xor a b) c" by (simp add: xor_def)
qed
next
assume "¬a"
show "xor a (xor b c) = xor (xor a b) c"
proof (cases b)
assume "b"
then show "xor a (xor b c) = xor (xor a b) c" using `¬a`by (simp add: xor_def)
next
assume "¬b"
then show "xor a (xor b c) = xor (xor a b) c" by (simp add: xor_def)
qed
qed

lemma valorP_conc:
"valorP4 i (xs @ ys) = (xor (valorP4 i xs) (valorP4 i ys))"
proof (induct xs)
show "valorP4 i ([] @ ys) = (xor (valorP4 i []) (valorP4 i ys))" by (simp add: xor_def)
next
fix x xs
assume HI: "valorP4 i (xs @ ys) = (xor (valorP4 i xs) (valorP4 i ys))"
have "valorP4 i ((x#xs) @ ys) = valorP4 i (x # (xs@ys))" by simp
also have "... = xor (valorM i x) (valorP4 i (xs@ys))" by simp
also have "... = xor (valorM i x) (xor (valorP4 i xs) (valorP4 i ys))" using HI by simp
also have "... = xor (xor (valorM i x) (valorP4 i xs)) (valorP4 i ys)" by (simp add: lema2)
also have "... = xor (valorP4 i (x#xs)) (valorP4 i ys)" by simp
finally show "valorP4 i ((x#xs) @ ys) = (xor (valorP4 i (x#xs)) (valorP4 i ys))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar que, en cualquier interpretación i, el valor
del producto de dos polinomios es la conjunción de sus valores.
--------------------------------------------------------------------- *}

-- "maresccas4 irealetei"

-- "Es fácil ver que este lema es análogo al demostrado lema1"
lemma lema3: "xor (a ∧ c) (b ∧ c) = ((xor a b) ∧ c)"
by (auto simp add: xor_def)

lemma correccion_producto:
"valorP4 i (producto4 p q) = (valorP4 i p ∧ valorP4 i q)"
proof (induct p)
show "valorP4 i (producto4 [] q) = (valorP4 i [] ∧ valorP4 i q)" by simp
next
fix m p
assume HI: "valorP4 i (producto4 p q) = (valorP4 i p ∧ valorP4 i q)"
have "valorP4 i (producto4 (m#p) q) = valorP4 i ((productoM m q) @ (producto4 p q))" by simp
also have "... = (xor (valorP4 i (productoM m q)) (valorP4 i (producto4 p q)))" by (simp add: valorP_conc)
also have "... = (xor (valorP4 i (productoM m q)) (valorP4 i p ∧ valorP4 i q))" using HI by simp
also have "... = (xor (valorM i m ∧ valorP4 i q) (valorP4 i p ∧ valorP4 i q))" by (simp add: correccion_productoM)
also have "... = ((xor (valorM i m) (valorP4 i p)) ∧ valorP4 i q)" by (simp add: lema3)
also have "... = (valorP4 i (m#p) ∧ valorP4 i q)" by simp
finally show "valorP4 i (producto4 (m#p) q) = (valorP4 i (m#p) ∧ valorP4 i q)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 16. Definir la función
polinomio :: form ⇒ nat list list
tal que (polinomio f) es el polinomio que representa la fórmula f. Por
ejemplo,
polinomio (Xor (Var 1) (Var 2)) = [[1],[2]]
polinomio (And (Var 1) (Var 2)) = [[1,2]]
polinomio (Xor (Var 1) T) = [[1],[]]
polinomio (And (Var 1) T) = [[1]]]
polinomio (And (Xor (Var 1) (Var 2)) (Var 3)) = [[1,3],[2,3]]
polinomio (Xor (And (Var 1) (Var 2)) (Var 3)) = [[1,2],[3]]
--------------------------------------------------------------------- *}

-- "maresccas4 irealetei"

fun polinomio :: "form ⇒ nat list list" where
"polinomio T = [[]]"
| "polinomio (Var a) = [[a]]"
| "polinomio (And G H) = producto4 (polinomio G) (polinomio H)"
| "polinomio (Xor G H) = (polinomio G) @ (polinomio H)"

value "polinomio (Xor (Var 1) (Var 2))"
value "polinomio (And (Var 1) (Var 2))"
value "polinomio (Xor (Var 1) T)"
value "polinomio (And (Var 1) T)"
value "polinomio (And (Xor (Var 1) (Var 2)) (Var 3))"
value "polinomio (Xor (And (Var 1) (Var 2)) (Var 3))"

text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar que, en cualquier interpretación i, el valor
de f es igual que el de su polinomio.
--------------------------------------------------------------------- *}

-- "maresccas4 irealetei"

theorem correccion_polinomio:
"valorF i f = valorP4 i (polinomio f)"
proof (induct f)
show "valorF i T = valorP4 i (polinomio T)" by (simp add: xor_def)
next
fix a
show "valorF i (Var a) = valorP4 i (polinomio (Var a))" by (simp add: xor_def)
next
fix G H
assume H1: "valorF i G = valorP4 i (polinomio G)"
assume H2: "valorF i H = valorP4 i (polinomio H)"
have "valorF i (And G H) = (valorF i G ∧ valorF i H)" by simp
also have "... = ((valorP4 i (polinomio G)) ∧ (valorP4 i (polinomio H)))" using H1 H2 by simp
also have "... = valorP4 i (producto4 (polinomio G) (polinomio H))" by (simp add: correccion_producto)
also have "... = valorP4 i (polinomio (And G H))" by simp
finally show "valorF i (And G H) = valorP4 i (polinomio (And G H))" by simp
next
fix G H
assume H1: "valorF i G = valorP4 i (polinomio G)"
assume H2: "valorF i H = valorP4 i (polinomio H)"
have "valorF i (Xor G H) = xor (valorF i G) (valorF i H)" by simp
also have "... = xor (valorP4 i (polinomio G)) (valorP4 i (polinomio H))" using H1 H2 by simp
also have "... = valorP4 i ((polinomio G) @ (polinomio H))" by (simp add: valorP_conc)
also have "... = valorP4 i (polinomio (Xor G H))" by simp
finally show "valorF i (Xor G H) = valorP4 i (polinomio (Xor G H))" by simp
qed

end
</source>

Relación 10

2014-03-10T01:06:06Z

Zoiruicha:

<source lang="isar">
header {* R10: Deducción natural proposicional *}

theory R10
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional.

Los ejercicios son los de la asignatura de "Lógica informática" que se
encuentran en http://goo.gl/yrPLn

Las reglas básicas de la deducción natural son las siguientes:
· 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
· excluded_middle: ¬P ∨ P
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

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

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

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}

--"marescpla, pabflomar, jaisalmen, zoiruicha"

lemma 01:
assumes 1: "p ∨ q"
and 2: "¬q"
shows "p"
using 1
proof (rule disjE)
{assume "p"
then show "p".}
next
{assume "q"
with 2 show "p" by (rule notE)}
qed

--"diecabmen1 maresccas4 domlloriv"
lemma Ejercicio_1:
assumes "p ∨ q"
"¬q"
shows "p"
using assms(1)
proof (rule disjE)
assume "p"
then show "p" .
next
assume "q"
with `¬q` show "p" ..
qed

--"juaruipav, julrobrel"
lemma ej1_juaruipav:
assumes 1:"p ∨ q"
and 2: "¬q"
shows "p"
using 1
proof
assume 3:"p"
then show "p" .
next
assume 4:"q"
show "p" using 2 4 by (rule notE)
qed

--"irealetei, julrobrel"
lemma ej1_auto:
assumes 1:"p ∨ q"
assumes 2:"¬q"
shows "p"
using assms by auto

lemma ej1:
assumes 1:"p ∨ q"
assumes 2:"¬q"
shows "p"
proof -
note 1
moreover
{assume "p"
then have "p" .}
moreover
{assume 3:"q"
have "p" using 2 3 ..}
ultimately show "p" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

--"marescpla, pabflomar,jaisalmen, zoiruicha"

lemma 02:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule ccontr)
assume "¬¬(¬p ∨ ¬q)"
then have 1: "(¬p ∨ ¬q)" by (rule notnotD)
show "False"
using 1
proof (rule disjE)
{assume I: "¬p"
have "p" using assms(1) by (rule conjunct1)
with I show "False"..}
{assume II: "¬q"
have "q" using assms(1) by (rule conjunct2)
with II show "False" ..}
qed
qed

--"diecabmen1 maresccas4 domlloriv"
lemma Ejercicio_2:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume 1: "¬p ∨ ¬q"
show False
using 1
proof (rule disjE)
assume "¬p"
have "p" using assms ..
with `¬p` show False ..
next
assume "¬q"
have "q" using assms ..
with `¬q` show False ..
qed
qed

--"juaruipav"

lemma ej2_juaruipav:
assumes 1:"p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume 2: "¬ p ∨ ¬ q"
show "False"
using 2
proof
assume 3: "¬q"
have 4:"q" using 1 by (rule conjunct2)
show "False" using 3 4 by (rule notE)
next
assume 5: "¬p"
have 6:"p" using 1 by (rule conjunct1)
show "False" using 5 6 by (rule notE)
qed
qed

--"irealetei, julrobrel"
lemma ej2_auto:
assumes 1:"p ∧ q"
shows "¬(¬p ∨ ¬q)"
using assms by auto

lemma ej2:
assumes 1:"p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
moreover
{assume 2:"¬p"
have 3:"p" using 1 ..
have "False" using 2 3 ..}
moreover
{assume 2:"¬q"
have 3:"q" using 1 ..
have "False" using 2 3 ..}
ultimately show "False" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

-- "maresccas4"
lemma
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
{ assume "p"
then have "p ∨ q" ..
with `¬(p ∨ q)` have False ..}
thus "¬p" ..
next
{ assume "q"
then have "p ∨ q" ..
with `¬(p ∨ q)` have False ..}
thus "¬q" ..
qed

-- "diecabmen1 pabflomar domlloriv"
lemma Ejercicio_3:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof -
{ assume "p"
then have "p ∨ q" ..
with assms have False ..}
then have "¬p" ..
{ assume "q"
then have "p ∨ q" ..
with assms have False ..}
then have "¬q" ..
with `¬p` show "¬p ∧ ¬q" ..
qed

--"marescpla,jaisalmen, zoiruicha"
lemma 03:
assumes 1:"¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof (rule ccontr)
{assume "¬¬p"
then have "p" by (rule notnotD)
then have "p ∨ q" by (rule disjI1)
with 1 show "False" ..}
qed
show "¬q"
proof (rule ccontr)
{assume "¬¬q"
then have "q" by (rule notnotD)
then have "p ∨ q" by (rule disjI2)
with 1 show "False" ..}
qed
qed

--"juaruipav"

lemma ej3_juaruipav:
assumes 1: " ¬(p ∨ q)"
shows " ¬p ∧ ¬q"
proof
{assume 2:"p"
have 3: "p∨q" using 2 by (rule disjI1)
have 4: "False" using 1 3 by (rule notE)}
then show "¬p" ..
next
{assume 5:"q"
have 6: "p∨q" using 5 by (rule disjI2)
have 7: "False" using 1 6 by (rule notE)}
then show "¬q" ..
qed

--"irealetei, julrobrel"
lemma ej3_auto:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
using assms by auto

lemma ej3:
assumes 0:"¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
{assume "p"
then have 2:"p ∨ q" ..
have "False" using 0 2 ..}
then show "¬p" ..
next
{assume "q"
then have 2:"p ∨ q" ..
have "False" using 0 2 ..}
then show "¬q" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

-- "maresccas4"
lemma
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
show False
using `p ∨ q`
proof
assume "p"
have "¬p" using `¬p ∧ ¬q` ..
thus False using `p` ..
next
assume "q"
have "¬q" using `¬p ∧ ¬q` ..
thus False using `q` ..
qed
qed

-- "diecabmen1 domlloriv,jaisalmen, zoiruicha"
lemma Ejercicio_4:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
show False
using `p ∨ q`
proof
assume "p"
have "¬p" using assms ..
then show False using `p` ..
next
assume "q"
have "¬q" using assms ..
then show False using `q` ..
qed
qed

--"marescpla"
lemma 04:
assumes 1:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule ccontr)
have 2: "¬p" using 1 by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
assume "¬¬(p ∨ q)"
then have 4:"(p ∨ q)" by (rule notnotD)
then show False
proof (rule disjE)
note 4
{assume "p"
with 2 show False ..}
{assume "q"
with 3 show False ..}
qed
qed

-- "pabflomar"

lemma ej4_pfm:
assumes 0:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume 1:"p ∨ q"
show False
using 1
proof
assume 1:"p"
have 2: "¬p" using 0 by (rule conjunct1)
then show False using `p` ..
next
assume 1:"q"
have 2: "¬q" using 0 by (rule conjunct2)
then show False using `q` ..
qed
qed

--"juaruipav, julrobrel"
lemma ej4_juaruipav:
assumes 1:" ¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume 2: " p ∨ q"
show "False"
using 2
proof
assume 3:"p"
have 4:"¬p" using 1 by (rule conjunct1)
show "False" using 4 3 by (rule notE)
next
assume 5:"q"
have 6:"¬q" using 1 by (rule conjunct2)
show "False" using 6 5 by (rule notE)
qed
qed

--"irealetei"
lemma ej4_auto:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
using assms by auto

lemma ej4:
assumes 0:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
moreover
{assume 1:"p"
have "¬p" using 0 ..
then have "False" using 1 ..}
moreover
{assume 1:"q"
have "¬q" using 0 ..
then have "False" using 1 ..}
ultimately show "False" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

-- "maresccas4 diecabmen1 domlloriv, julrobrel,jaisalmen, zoiruicha"
lemma
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
show False
using `¬p ∨ ¬q`
proof
assume "¬p"
have "p" using `p ∧ q` ..
with `¬p`show False ..
next
assume "¬q"
have "q" using `p ∧ q` ..
with `¬q` show False ..
qed
qed

--"marescpla"

lemma 05:
assumes 1:"¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule ccontr)
assume "¬¬(p ∧ q)"
then have 4:"(p ∧ q)" by (rule notnotD)
have p using 4 by (rule conjunct1)
have q using 4 by (rule conjunct2)
show False
using 1
proof (rule disjE)
{assume "¬p"
then show False using `p` ..}
{assume "¬q"
then show False using `q`..}
qed
qed

-- "pabflomar"
lemma ej5_pfm:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
show False
using `¬p ∨ ¬q`
proof
assume "¬p"
have "p" using `p ∧ q` by (rule conjunct1)
with `¬p` show False by (rule notE)
next
assume "¬q"
have "q" using `p ∧ q` by (rule conjunct2)
with `¬q` show False by (rule notE)
qed
qed

--"juaruipav"
lemma ej5_juaruipav:
assumes 1:"¬p ∨ ¬q"
shows " ¬(p ∧ q)"
using 1
proof
assume 2: "¬p"
show "¬ (p ∧ q)"
proof
assume 3: " p ∧ q"
have 4:"p" using 3 by (rule conjunct1)
show "False " using 2 4 by (rule notE)
qed
next
assume 5: "¬q"
show "¬ (p ∧ q)"
proof
assume 6: " p ∧ q"
have 7:"q" using 6 by (rule conjunct2)
show "False " using 5 7 by (rule notE)
qed

qed

--"irealetei"
lemma ej5_auto:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
using assms by auto

lemma ej5:
assumes 0:"¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume 1:"p ∧ q"
have 2:"p" using 1 ..
have 3:"q" using 1 ..
show "False" using 0
proof
assume "¬p"
then show "False" using 2 ..
next
assume "¬q"
then show "False" using 3 ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv,jaisalmen, zoiruicha"
lemma Ejercicio_6:
shows "((p ⟶ q) ⟶ p) ⟶ p"
proof
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
with `(p ⟶ q) ⟶ p` have "¬(p ⟶ q)" by (rule mt)
{ assume "p"
with `¬p` have False ..
then have "q" ..}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` show False ..
qed
qed

--"marescpla"

lemma 06:
"((p ⟶ q) ⟶ p) ⟶ p"
proof
assume 1: "((p ⟶ q) ⟶ p)"
show "p"
proof(rule ccontr)
assume "¬p"
with 1 have 2: "¬(p⟶q)" by (rule mt)
then show "False"
proof
{assume "p"
with `¬p` have "q" by (rule notE)}
then show "(p⟶q)" by (rule impI)
qed
qed
qed

--"irealetei, julrobrel"
lemma ej6_auto:"((p ⟶ q) ⟶ p) ⟶ p"
using assms by auto

lemma ej6:"((p ⟶ q) ⟶ p) ⟶ p"
proof
assume 1:"(p ⟶ q)⟶p"
show "p"
proof (rule ccontr)
assume 2:"¬p"
have 4:"¬(p⟶q)" using 1 2 by (rule mt)
{assume 5:"p"
have "False" using 2 5 ..
then have "q" ..}
then have 6:"p⟶q" ..
show "False" using 4 6 ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "diecabmen1 pabflomar"
lemma Ejercicio_7:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
{ assume "¬q"
with assms have "¬p" ..
then have False using `p` ..}
then show "q" by (rule ccontr)
qed

--"marescpla,jaisalmen, zoiruicha"
lemma 07:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume 1: "p"
{assume "¬q"
with assms have "¬p" ..
then have "False" using 1 ..}
then have "¬¬q" by (rule notI)
then show "q" by (rule notnotD)}
qed

-- "maresccas4"
lemma
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
then have "¬¬p" by (rule notnotI)
with assms(1) have "¬¬q" by (rule mt)
then show "q" by (rule notnotD)
qed

--"juaruipav, julrobrel, domlloriv"

lemma ej7_juaruipav:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have 4: "¬¬q" using 1 3 by (rule mt)
show "q" using 4 by (rule notnotD)
qed

--"irealetei"
lemma ej7_auto:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
using assms by auto

lemma ej7:
assumes 0:"¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume 1:"p"
then have 2:"¬¬p" by (rule notnotI)
have "¬¬q" using 0 2 by (rule mt)
then have "q" by (rule notnotD)}
then show "p ⟶ q" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_8:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" ..
{ assume "p"
then have "p ∨ q" ..}
{ assume "¬p"
have "¬q ∨ q" ..
{ assume "q"
then have "p ∨ q" ..}
{ assume "¬q"
with `¬p` have "¬p ∧ ¬q" ..
with assms have False ..
then have "p ∨ q" ..}
with `¬q ∨ q` have "p ∨ q" using `q ⟹ p ∨ q` ..}
with `¬p ∨ p` show "p ∨ q" using `p ⟹ p ∨ q` ..
qed

--"marescpla pabflomar (No se usar otro lema sin usar el simp) maresccas4 (rule 03, en lugar de simp)"
{* Marco lleva razón. GRACIAS!!! *}

lemma 08:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
then have "¬p ∧ ¬q" by (rule 03)
with assms show "False" ..
qed

--"irealetei, julrobrel"
lemma ej8_auto:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
using assms by auto

lemma ej8:
assumes 0:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
{assume 1:"¬(p ∨ q)"
have 2:"¬p ∧ ¬q" using 1 by (rule ej3)
have "False" using 0 2 ..}
then show "p ∨ q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "diecabmen1, maresccas4 domlloriv"
lemma Ejercicio_9:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
{ assume "¬p"
then have "¬p ∨ ¬q" ..
with assms have False ..}
then show "p" by (rule ccontr)
{ assume "¬q"
then have "¬p ∨ ¬q" ..
with assms have False ..}
then show "q" by (rule ccontr)
qed

-- "pabflomar, marescpla"

lemma ej9_pfm:
assumes " ¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
have 1: "¬¬p ∧ ¬¬q" using assms by (rule ej3_pfm)
have 2: "¬¬p" using 1 by (rule conjunct1)
have 3: "¬¬q" using 1 by (rule conjunct2)
show "p" using 2 by (rule notnotD)
show "q" using 3 by (rule notnotD)
qed

--"juaruipav"
lemma ej9_juaruipav:
assumes 1: " ¬(¬p ∨ ¬q)"
shows " p ∧ q"
proof
have 2:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
have "(¬¬p)" using 2 by (rule conjunct1)
then show "p" by (rule notnotD)
next
have 3:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
have "(¬¬q)" using 3 by (rule conjunct2)
then show "q" by (rule notnotD)
qed

--"irealetei, julrobrel"
lemma ej9_auto:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
using assms by auto

lemma ej9:
assumes 0:"¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
{assume "¬p"
then have 1:"¬p ∨ ¬q" ..
have "False" using 0 1 ..}
then show "p" by (rule ccontr)
next
{assume "¬q"
then have 1:"¬p ∨ ¬q" ..
have "False" using 0 1 ..}
then show "q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
-- "pabflomar, julrobrel, juaruipav, domlloriv"
lemma ej10_pfm:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume 1:"¬ (¬ p ∨ ¬ q)"
show False
proof -
have "p ∧ q" using 1 by (rule ej9_pfm)
with assms show False by (rule notE)
qed
qed

-- "diecabmen1"
lemma Ejercicio_10:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨ p" ..
{ assume "p"
have "¬q ∨ q" ..
{ assume "q"
with `p` have "p ∧ q" ..
with assms have False ..
then have "¬p ∨ ¬q" ..}
{ assume "¬q"
then have "¬p ∨ ¬q" ..}
with `¬q ∨ q` have "¬p ∨ ¬q" using `q ⟹ ¬ p ∨ ¬ q` ..}
{ assume "¬p"
then have "¬p ∨ ¬q" ..}
with `¬p ∨ p` show "¬p ∨ ¬q" using ` p ⟹ ¬ p ∨ ¬ q` ..
qed

-- "maresccas4"
lemma a10:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
{ assume "¬p"
then have "¬p ∨ ¬q" ..
with `¬(¬p ∨ ¬q)` have False ..}
hence "¬¬p" ..
thus "p" by (rule notnotD)
{ assume "¬q"
then have "¬p ∨ ¬q" ..
with `¬(¬p ∨ ¬q)` have False ..}
hence "¬¬q" ..
thus "q" by (rule notnotD)
qed

lemma 10:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
then have "p ∧ q" by (rule a10)
with assms(1) show False ..
qed

text {* -----
Ejercicio 9 haciendo uso del Ejercicio 10
----------*}
lemma
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule ccontr)
assume "¬(p ∧ q)"
then have "¬p ∨ ¬q" by (rule 10)
with assms(1) show False ..
qed

--"marescpla"

lemma 10:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
then have 1:"p ∧ q" by (rule 09)
with assms show "False" ..
qed

--"irealetei"
lemma ej10_auto:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
using assms by auto

lemma ej10:
assumes 0:"¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
{assume 1:"¬(¬p ∨ ¬q)"
have 2:"p ∧ q" using 1 by (rule ej9)
have 3:"False" using 0 2 .. }
then show "¬p ∨ ¬q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_11:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬(p ⟶ q) ∨ (p ⟶ q)" ..
{ assume "(p ⟶ q)"
then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
{ assume "¬(p ⟶ q)"
{ assume "q"
{ assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` have False ..
then have "p" ..}
then have "q ⟶ p" ..
then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
with `¬(p ⟶ q) ∨ (p ⟶ q)` show "(p ⟶ q) ∨ (q ⟶ p)" using `p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p)` ..
qed

-- "maresccas4"
lemma
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
show "(p ⟶ q) ∨ (q ⟶ p)"
using 1
proof
assume "p ⟶ q"
then show "(p ⟶ q) ∨ (q ⟶ p)" ..
next
{ assume "¬(p ⟶ q)"
{ assume "q"
{ assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` have False ..
then have "p" .. }
then have "q ⟶ p" ..
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
qed
qed

-- "pabflomar, julrobrel"
{* Sólo cambia respecto de marco en el cambio del . por by this *}
lemma
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
show "(p ⟶ q) ∨ (q ⟶ p)"
using 1
proof
assume "p ⟶ q"
then show "(p ⟶ q) ∨ (q ⟶ p)" ..
next
{ assume "¬(p ⟶ q)"
{ assume "q"
{ assume "p"
have "q" using `q` by this
}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` have False ..
then have "p" ..
}
then have "q ⟶ p" ..
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
qed
qed

-- "irealetei domlloriv juaruipav"

lemma ej11_auto:"(p ⟶ q) ∨ (q ⟶ p)"
using assms by auto

lemma ej11:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have 1:"¬(p ⟶ q) ∨ (p ⟶ q) " by (rule excluded_middle)
then show "(p ⟶ q) ∨ (q ⟶ p)"
proof
note 1
moreover
{assume "p⟶q"
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
moreover
{assume 2:"¬(p ⟶ q)"
{assume 3:"q"
{assume "p"
have "q" using 3 .}
then have 4:"p⟶q" ..
have "False" using 2 4 ..
then have "p" ..}
then have "q⟶p" ..
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
qed
qed

end
</source>

Relación 2

2013-11-21T12:08:06Z

Zoiruicha:

<source lang="isar">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

-- "maresccas4 pabflomar"

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

value "sumaImpares 5" -- "= 25"

-- "diecabmen1 irealetei juaruipav domlloriv, marescpla"
thm nat.induct
fun sumaImpares2 :: "nat ⇒ nat" where
"sumaImpares2 0 = 0"
| "sumaImpares2 (Suc n) = (2*n + 1) + sumaImpares2 n" <-- "yo he puesto el +1 con un Suc (marescpla)"

value "sumaImpares2 5" -- "= 25"

-- "jaisalmen zoiruicha"
fun sumaImpares3 :: "nat ⇒ nat" where
"sumaImpares3 0 = 0"
| "sumaImpares3 (n) = (2 * n) - 1 + sumaImpares3 (n - 1)"

value "sumaImpares 5" -- "= 25"

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

-- "maresccas4,juaruipav domlloriv pabflomar, marescpla"

lemma "sumaImpares n = n*n"
by (induct n) auto

-- "diecabmen1 irealetei"

lemma "sumaImpares2 n = n*n"
by (induct n) auto

-- "jaisalmen zoiruicha"
lemma "sumaImpares3 n = n*n"
by (induct n) auto

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

-- "maresccas4 diecabmen1 irealetei domlloriv pabflomar, marescpla"

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

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

-- "juaruipav"
fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno2 0 = 2"
| "sumaPotenciasDeDosMasUno2 (Suc n) = 2*sumaPotenciasDeDosMasUno2 n"

value "sumaPotenciasDeDosMasUno2 3" -- "= 16"

-- "jaisalmen zoiruicha"
fun sumaPotenciasDeDosMasUno3 :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno3 0 = 2"
| "sumaPotenciasDeDosMasUno3 (n) = 2^n + sumaPotenciasDeDosMasUno3(n - 1)"

value "sumaPotenciasDeDosMasUno3 3" -- "= 16"

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

-- "maresccas4 diecabmen1 irealetei juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) auto

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

-- "maresccas4 irealetei domlloriv juaruipav pabflomar, marescpla"

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

value "copia 3 x" -- "= [x,x,x]"

-- "diecabmen1"

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

value "copia2 3 x" -- "= [x,x,x]"

-- "jaisalmen zoiruicha"
fun copia3 :: "nat ⇒ 'a ⇒ 'a list" where
"copia3 0 x = []"
| "copia3 n x = x # (copia3 (n- 1) x)"

value "copia3 3 x" -- "= [x,x,x]"

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

-- "maresccas4 irealetei diecabmen1 juaruipav pabflomar jaisalmen, marescpla zoiruicha"

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

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

-- "domlloriv"
fun todos2 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
"todos2 p [] = True"
| "todos2 p (x#xs) = ((p x) \<and> todos2 p xs)"

value "todos2 (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos2 (λx. x>(2::nat)) [2,6,4]" -- "= False""

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

-- "maresccas4,juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"

lemma "todos (λy. y=x) (copia n x)"
by (induct n) auto

-- "diecabmen1"
lemma "todos (λy. y=x) (copia2 n x)"
by (induct n) auto

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

-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar, marescpla"

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
|"factR (Suc n) = (Suc n) * factR n" <--"creo que no hacen falta los paréntesis del 2º suc (marescpla)"

value "factR 4" -- "= 24"

-- "jaisalmen zoiruicha"
fun factR2 :: "nat ⇒ nat" where
"factR2 0 = 1"
| "factR2 (n) = n * factR2 (n - 1)"

value "factR2 4" -- "= 24"

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

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

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

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

value "factI 4" -- "= 24"

-- "maresccas4 irealetei diecabmen1 juaruipav domlloriv pabflomar jaisalmen, marescpla zoiruicha"

lemma fact: "factI' n x = x * factR n"
by (induct n arbitrary: x) auto

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

-- "maresccas4 diecabmen1 juaruipav pabflomar jaisalmen zoiruicha" "no lo entiendo (marescpla)"

corollary "factI n = factR n"
by (simp add: fact)

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

-- "maresccas4,juaruipav domlloriv jaisalmen zoiruicha"

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

value "amplia [d,a] t" -- "= [d,a,t]"

-- "irealetei diecabmen1"

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

value "amplia2 [d,a] t" -- "= [d,a,t]"

-- "pabflomar, marescpla" ¿Sería mejor poner los paréntesis en la llamada a amplia como hace maresccas4?
fun amplia3 :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia3 [] y = [y]"
| "amplia3 (x#xs) y = x # amplia3 xs y"

value "amplia3 [d,a] t" -- "= [d,a,t]"

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

-- "maresccas4, juaruipav domlloriv pabflomar jaisalmen zoiruicha"

lemma "amplia xs y = xs @ [y]"
by (induct xs) auto

-- "irealetei diecabmen1" (* Es igual que la de maresccas4, pero lo pego para que compile*)

lemma "amplia2 xs y = xs @ [y]"
by (induct xs) auto

end

</source>

Relación 1

2013-11-21T12:00:40Z

Zoiruicha:

<source lang="isar">

header {* R1: Programación funcional en Isabelle *}

theory R1
imports Main
begin

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

-- "antmacrui maresccas4 diecabmen1 juaruipav marescpla"
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1"
| "factorial (Suc n) = Suc n * factorial n"

value "factorial 4" -- "24"

-- "irealetei domlloriv"
fun factorial2 :: "nat ⇒ nat" where
"factorial2 (0::nat)= (1::nat)"
| "factorial2 n = n * factorial2 (n - 1)"

value "factorial2 4" -- "24"

-- "julrobrel"
fun factorial3 :: "nat ⇒ nat" where
"factorial3 0 = 1"
| "factorial3 n = factorial3 (n - 1) * n"

value "factorial3 4" -- "24"

-- "jaisalmen zoiruicha"
fun factorial4 :: "nat ⇒ nat" where
"factorial4 0 = 1"
| "factorial4 (n) = n * factorial4 (n- 1)"

value "factorial4 4" -- "24

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

-- "maresccas4 domlloriv"
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x # xs) = Suc (longitud xs)"

value "longitud [4,2,5]" -- "= 3"

-- "irealetei pabflomar julrobrel juaruipav"
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = (0::nat)"
| "longitud2 xs = 1 + longitud2 (tl xs) "

value "longitud2 [4,2,5]" -- "= 3"

-- "diecabmen1"
fun longitud3 :: "'a list ⇒ nat" where
"longitud3 [] = 0"
| "longitud3 (head#tail) = 1 + longitud3 tail"

value "longitud3 [4,2,5]" -- "= 3"

-- "marescpla"
fun longitud4 :: "'a list ⇒ nat" where
"longitud4 [] = 0"|
"longitud4 xs = 1 + longitud4 (tl xs) "

value "longitud4 [4,2,5]" -- "= 3"

-- ""jaisalmen zoiruicha"
fun longitud5 :: "'a list ⇒ nat" where
"longitud5 [] = 0"
| "longitud5 (x#a) = 1 + longitud5 a"

value "longitud5 [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

-- "maresccas4 pabflomar"
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia p = (snd p, fst p)"

value "intercambia (u,v)" -- "= (v,u)"

-- "irealetei diecabmen1 domlloriv julrobrel juaruipav marescpla jaisalmen"
fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia2 (x,y) = (y,x)"

value "intercambia2 (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

-- "maresccas4 diecabmen1 domlloriv julrobrel juaruipav"
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ (x#[])"

value "inversa [a,d,c]" -- "= [c,d,a]"

-- "irealetei pabflomar"
fun inversa2 :: "'a list ⇒ 'a list" where
"inversa2 [] = [] "
| "inversa2 xs = inversa2 (tl xs) @ (hd xs#[])"

value "inversa2 [a,d,c]" -- "= [c,d,a]"

-- "jaisalmen zoiruicha"
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []"
| "inversa3 (x#a) = inversa3 a @ [x]"

value "inversa3 [a,d,c]" -- "= [c,d,a]"

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

-- "maresccas4 julrobrel juaruipav marescpla"
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"|
"repite (Suc n) x = x # repite n x"

value "repite 3 a" -- "= [a,a,a]"

-- "irealetei"
fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
"repite2 (0::nat) x = []"
| "repite2 n x = x#(repite2 (n - 1) x) "

value "repite2 3 a" -- "= [a,a,a]"

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

value "repite3 3 a" -- "= [a,a,a]"

-- "domlloriv pabflomar jaisalmen zoiruicha"
fun repite4 :: "nat ⇒ 'a ⇒ 'a list" where
"repite4 0 x = []"
| "repite4 n x = x# repite4 (n - 1) x"

value "repite4 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

-- "maresccas4 julrobrel"
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # conc xs ys"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

-- irealetei
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 xs [] = xs"
| "conc2 xs ys = hd ys # conc2 xs (tl ys)"

value "conc2 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

-- "diecabmen1 domlloriv pabflomar juaruipav"
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 xs ys = xs@ys"

value "conc3 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

-- "marescpla"
fun conc4 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc4 [] [] = []"|
"conc4 [] ys = (hd ys) # conc4 [] (tl ys)"|
"conc4 xs ys = (hd xs) # conc4 (tl xs) ys"

value "conc4 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

-- "jaisalmen zoiruicha"
fun conc5 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc5 [] ys = ys"
| "conc5 xs [] = xs"
| "conc5 (x#xs) ys = x # conc5 xs ys"

value "conc5 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

-- "maresccas4 diecabmen1 domlloriv"
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge 0 xs = []"
| "coge n [] = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

-- "irealetei"
fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge2 0 xs = []"
| "coge2 n xs = (hd xs) # (coge2 (n - 1) (tl xs))"

-- "pabflomar"
fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge3 0 xs = []"
| "coge3 n xs = (hd xs) # (coge3 (n - 1) (tl xs))"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

-- "julrobrel,juaruipav"
fun coge4 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge4 0 xs = []"
|"coge4 (Suc n) [] = []"
|"coge4 (Suc n) (x#xs) = x # (coge4 n xs)"

value "coge4 2 [a,c,d,b,e]" -- "= [a,c]"

-- "marescpla"
fun coge5 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge5 0 xs = []"|
"coge5 (Suc n) xs = hd xs # coge5 n (tl xs)"

value "coge5 2 [a,c,d,b,e]" -- "= [a,c]"

-- "jaisalmen zoiruicha"
fun coge6 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge6 0 xs = []"
| "coge6 n [] = []"
| "coge6 n (x#xs) = x # (coge6 (n-(1::nat)) xs)"

value "coge6 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

-- "maresccas4 domlloriv"
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina 0 xs = xs"
| "elimina n [] = []"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

-- "irealetei pabflomar"
fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
" elimina2 0 xs = xs "
| "elimina2 n xs = elimina2 (n - 1) (tl xs)"

value "elimina2 2 [a,c,d,b,e]" -- "= [d,b,e]"

-- "diecabmen1"
fun elimina3 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina3 0 xs = xs"
| "elimina3 n [] = []"
| "elimina3 n (x#xs) = elimina3 (n - 1) xs"

value "elimina3 2 [a,c,d,b,e]" -- "= [d,b,e]"

-- "julrobrel, juaruipav"
fun elimina4 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina4 0 xs = xs"
|"elimina4 (Suc n) [] = []"
|"elimina4 (Suc n) (x#xs) = (elimina4 n xs)"

value "elimina4 2 [a,c,d,b,e]" -- "= [d,b,e]"

-- "marescpla"
fun elimina5 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina5 0 xs = xs"|
"elimina5 (Suc n) xs = elimina5 n (tl xs)"

value "elimina5 2 [a,c,d,b,e]"

-- "jaisalmen zoiruicha"
fun elimina6 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina6 0 xs = xs"
| "elimina6 n [] = []"
| "elimina6 n (x#xs) = elimina6 (n-(1::nat)) xs"

value "elimina6 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

-- "maresccas4"
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

-- "irealetei domlloriv pabflomar julrobrel juaruipav marescpla"
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 [] = True"|
"esVacia2 xs = False"

value "esVacia2 []" -- "= True"
value "esVacia2 [1]" -- "= False"

-- "diecabmen1"
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 xs = (if xs = [] then True else False)"

value "esVacia3 []" -- "= True"
value "esVacia3 [1]" -- "= False"

-- "jaisalmen zoiruicha"
fun esVacia4 :: "'a list ⇒ bool" where
"esVacia4 x = (if longitud(x)=0 then True else False)"

value "esVacia4 []" -- "= True"
value "esVacia4 [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

-- "maresccas4 domlloriv"
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]"

-- "irealetei"
fun inversaAc2Aux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAc2Aux xs [] = xs"
| "inversaAc2Aux xs ys = inversaAc2Aux ((hd ys) # xs) (tl ys)"

fun inversaAc2 :: "'a list ⇒ 'a list" where
"inversaAc2 xs = inversaAc2Aux [] xs"

value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]"

-- "diecabmen1 julrobrel,juaruipav"
fun inversaAc3Aux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAc3Aux xs ys = xs@ys"

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

value "inversaAc3 [a,c,b,e]" -- "= [e,b,c,a]"
-- "pabflomar"
fun inversaAcAux4 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux4 [] ys = ys"
| "inversaAcAux4 xs ys = inversaAcAux4 (tl xs) ((hd xs) # ys)"

fun inversaAc4 :: "'a list ⇒ 'a list" where
"inversaAc4 xs = inversaAcAux4 xs []"

value "inversaAc4 [a,c,b,e]" -- "= [e,b,c,a]"

-- "marescpla"
fun inversaAcAux5 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux5 [] ys = ys"|
"inversaAcAux5 xs ys = inversaAcAux5 (elimina 1 xs) (conc (coge 1 xs) ys)"

fun inversaAc5 :: "'a list ⇒ 'a list" where
"inversaAc5 xs = inversaAcAux5 xs []"

value "inversaAc5 [a,c,b,e]" -- "= [e,b,c,a]"

-- "jaisalmen"
fun inverseAcAux6 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inverseAcAux6 xs ys = xs@ys"

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

value "inversaAc6 [a,c,b,e]" -- "= [e,b,c,a]"

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

-- "maresccas4 diecabmen1 domlloriv julrobrel juaruipav jaisalmen zoiruicha"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

-- "irealetei pabflomar marescpla"
fun sum2 :: "nat list ⇒ nat" where
"sum2 [] = 0"
|"sum2 xs = hd xs + sum2 (tl xs)"

value "sum2 [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

-- "maresccas4 domlloriv julrobrel juaruipav"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

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

-- "irealetei pabflomar"
fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map2 f [] = []"
|"map2 f xs = f(hd xs) # map2 f (tl xs)"

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

-- "diecabmen1"
fun map3 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map3 f [] = []"
| "map3 f (x#xs) = ((f x)#[]) @ (map3 f xs)"

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

-- "marescpla"
fun map4 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map4 f [] = []"|
"map4 f xs = value f (coge 1 xs) # map4 f (elimina 1 xs)"

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

-- "jaisalmen zoiruicha"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map5 f [] = []"
| "map5 f (x#xs) = f(x) # map5 f xs "

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

end
</source>