Razonamiento automático (2018-19) - Contribuciones del usuario [es]

Relación 8

2019-03-01T13:16:01Z

Josgomrom4:

<source lang="isabelle">
chapter {* R8: Gramáticas libres de contexto *}

theory R8_Gramaticas_libre_de_contexto
imports Main
begin

text {*
En esta relación se definen dos gramáticas libres de contexto y se
demuestra que son equivalentes. Además, se define por recursión una
función para reconocer las palabras de la gramática y se demuestra que
es correcta y completa. *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Una gramática libre de contexto para las expresiones
parentizadas es
S ⟶ ε | '(' S ')' | SS
definir inductivamente la gramática S usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}

datatype alfabeto = A | B

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

text {*
---------------------------------------------------------------------
Ejercicio 2. Otra gramática libre de contexto para las expresiones
parentizadas es
T ⟶ ε | T '(' T ')'
definir inductivamente la gramática T usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}

inductive_set T :: "alfabeto list set" where
T1: "[] ∈ T"
| T2: "v ∈ T ⟹ w ∈ T ⟹ v @ [A] @ w @ [B] ∈ T"

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que T está contenido en S.
------------------------------------------------------------------ *}

(* benber alfmarcua antramhur josgomrom4 *)
lemma T_en_S:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S"
proof (induction rule: T.induct)
show "[] ∈ S" by (rule S1)
next
fix v w
assume "w ∈ S"
hence "[A] @ w @ [B] ∈ S" by (rule S2)
moreover assume "v ∈ S"
ultimately show "v @ [A] @ w @ [B] ∈ S" using S3 by simp
qed
thus ?thesis using assms .
qed

(* cammonagu *)
declare S1 [iff] S2[intro!,simp]

(* cammonagu *)
declare T1 [iff]

(* cammonagu *)
lemma T2ImpS: "w ∈ T ⟹ w ∈ S"
apply (erule T.induct)
apply simp
apply (blast intro: S3)
done

(* cammonagu *)
lemma T_en_S1:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S" using assms by (rule T2ImpS)
thus ?thesis using assms .
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S está contenido en T.
------------------------------------------------------------------ *}

(* benber *)
lemma S_en_T:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w

have "[] ∈ T" by (rule T1)
moreover assume "w ∈ T"
ultimately have "[] @ [A] @ w @ [B] ∈ T" by (rule T2)
thus "[A] @ w @ [B] ∈ T" by simp
next
fix v w
assume "v ∈ T"
moreover assume "w ∈ T"
moreover have "⟦v ∈ T; w ∈ T⟧ ⟹ v @ w ∈ T" for v w
proof (induction "length w + length v"
arbitrary: w v
rule: less_induct)
case IH: less

show "v @ w ∈ T"
proof (cases w rule: T.cases)
show "w ∈ T" using `w ∈ T`.
next
assume "w = []"
thus "v @ w ∈ T" using `v ∈ T` by simp
next
fix w1 w2
assume "w1 ∈ T" and "w2 ∈ T"
assume "w = w1 @ [A] @ w2 @ [B]"
hence 1: "v @ w = v @ w1 @ [A] @ w2 @ [B]" by simp

have "length w1 < length w" using `w = w1 @ [A] @ w2 @ [B]`
by simp
hence "length v + length w1 < length v + length w" by simp
moreover note `v ∈ T`
moreover note `w1 ∈ T`
ultimately have "v @ w1 ∈ T" using IH by simp
moreover note `w2 ∈ T`
ultimately have "(v @ w1) @ [A] @ w2 @ [B] ∈ T" by (rule T2)
thus "v @ w ∈ T" using 1 by simp
qed
qed
ultimately show "v @ w ∈ T" by simp
qed

(* alfmarcua antramhur josgomrom4 *)
lemma S_en_T_2:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w
assume "w ∈ T"
have "[] @ [A] @ w @ [B] ∈ T" using T1 `w ∈ T` by (rule T2)
then show "[A] @ w @ [B] ∈ T" by (simp only: List.append.append_Nil)
next
fix w v
assume "v ∈ T"
show "w ∈ T ⟹ v @ w ∈ T"
proof (induction rule: T.induct)
show "v @ [] ∈ T" using `v ∈ T`
by (simp only: List.append.right_neutral)
next
fix va w
have "v @ va ∈ T ⟹ w ∈ T ⟹ (v @ va) @ [A] @ w @ [B] ∈ T "
by (rule T2)
then show "v @ va ∈ T ⟹ w ∈ T ⟹ v @ va @ [A] @ w @ [B] ∈ T "
by (simp only: List.append_assoc)
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S y T son iguales.
------------------------------------------------------------------ *}

(* benber cammonagu antramhur josgomrom4 *)
lemma S_igual_T:
"S = T"
using T_en_S S_en_T by auto

(* alfmarcua *)
lemma S_igual_T_2:
"S = T"
proof (rule equalityI)
show "S ⊆ T" using S_en_T by (rule subsetI)
next
show "T ⊆ S" using T_en_S by (rule subsetI)
qed

text {*
---------------------------------------------------------------------
Ejercicio 5. En lugar de una gramática, se puede usar el siguiente
procedimiento para determinar si la cadena es una sucesión de
paréntesis bien balanceada: se recorre la cadena de izquierda a
derecha contando cuántos paréntesis de necesitan para que esté bien
balanceada. Si el contador al final de la cadena es 0, la cadena está
bien balanceada.

Definir la función
balanceada :: alfabeto list ⇒ bool
tal que (balanceada w) se verifica si w está bien balanceada. Por
ejemplo,
balanceada [A,A,B,B] = True
balanceada [A,B,A,B] = True
balanceada [A,B,B,A] = False
Indicación: Definir balanceada usando la función auxiliar
balanceada_aux :: alfabeto list ⇒ nat ⇒ bool
tal que (balanceada_aux w 0) se verifica si w está bien balanceada.
------------------------------------------------------------------ *}

(* benber alfmarcua antramhur josgomrom4 *)
(* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
"balanceada_aux [] 0 = True"
| "balanceada_aux [] (Suc n) = False"
| "balanceada_aux (B#w) 0 = False"
| "balanceada_aux (B#w) (Suc n) = balanceada_aux w n"
| "balanceada_aux (A#w) n = balanceada_aux w (Suc n)"

fun balanceada :: "alfabeto list ⇒ bool" where
"balanceada w = balanceada_aux w 0"

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
gramática S; es decir,
w ∈ S ⟹ balanceada w
------------------------------------------------------------------ *}

(* benber *)
lemma balanceada_correcto_aux1:
"balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)"
proof (induction w arbitrary: n)
case Nil
assume "balanceada_aux [] n"
thus ?case by simp
next
case IS: (Cons x w)
show ?case
proof (cases x)
case A
note `balanceada_aux (x#w) n`
hence "balanceada_aux (A#w) n" using `x = A` by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@[B]) (Suc (Suc n))" using IS.IH by simp
hence "balanceada_aux ((A#w)@[B]) (Suc n)" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp

show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@[B]) (Suc m)" using IS.IH by simp
hence "balanceada_aux (w@[B]) n" using `n = Suc m` by simp
hence "balanceada_aux (B#(w@[B])) (Suc n)" by simp
thus ?thesis using `x = B` by simp
qed
qed
qed

lemma balanceada_correcto_aux2:
assumes "balanceada v"
shows "balanceada_aux w n ⟹ balanceada_aux (w @ v) n"
proof (induction w arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux.elims by auto
thus ?case using assms by simp
next
case IS: (Cons x w)
show "balanceada_aux ((x#w)@v) n"
proof (cases x)
case A
hence "balanceada_aux (A#w) n" using IS.prems by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@v) (Suc n)" using IS.IH by simp
hence "balanceada_aux (A#(w@v)) n" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp

show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@v) m" using IS.IH by simp
hence "balanceada_aux (B#(w@v)) (Suc m)" by simp
thus ?thesis using `x = B` `n = Suc m` by simp
qed
qed
qed

lemma balanceada_correcto:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada [] = balanceada_aux [] 0" by simp
also have "..." by simp
finally show ?case.
next
case S2
fix w
assume "balanceada w"
hence "balanceada_aux w 0" by simp
hence "balanceada_aux (w@[B]) 1" using balanceada_correcto_aux1
by simp
hence "balanceada_aux ([A] @ w @ [B]) 0" by simp
thus "balanceada ([A] @ w @ [B])" by simp
next
case S3
thus ?case using balanceada_correcto_aux2 by auto
qed

(* alfmarcua antramhur josgomrom4 *)
lemma balanceada_correcto_aux3:
shows "balanceada_aux v m ⟹
balanceada_aux w n ⟹
balanceada_aux (v @ w) (m+n)"
proof (induction v arbitrary: n m)
case Nil
then show ?case
proof (cases m)
case 0
then have "balanceada_aux w (m + n)" using Nil.prems(2)
by (simp only:Groups.monoid_add_class.add.left_neutral)
then show ?thesis by (simp only:List.append.append_Nil)
next
case (Suc mm)
then have "False" using Nil.prems(1)
by (simp only: balanceada_aux.simps(2))
then show ?thesis ..
qed
next
case IS:(Cons a v)
show "balanceada_aux ((a # v) @ w) (m + n)"
proof (cases a)
define k :: nat where "k = m + 1"
case A
then have "balanceada_aux v k" using `k = m + 1` IS.prems(1)
by simp
then have "balanceada_aux (v @ w) (k + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (v @ w) (Suc(m + n))" using `k = m + 1`
by simp
then have "balanceada_aux (A # (v @ w)) (m + n)"
by (simp only: balanceada_aux.simps(5))
then show ?thesis using `a = A`
by (simp only:List.append.append_Cons)
next
case B
then show ?thesis
proof (cases m)
case 0
then have "False" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(3))
then show ?thesis ..
next
case (Suc mm)
hence "balanceada_aux v mm" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (v @ w) (mm + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (B # (v @ w)) (Suc (mm + n))"
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (B # (v @ w)) (m + n)"
using `m = Suc mm` by (simp only: Nat.plus_nat.add_Suc)
then show ?thesis using `a=B`
by (simp only:List.append.append_Cons)
qed
qed
qed

lemma balanceada_correcto_2:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then show ?case by (simp only: balanceada.simps)
next
case (S2 w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then have 2:"balanceada_aux (B#[]) (Suc 0)"
by (simp only: balanceada_aux.simps(4))
have "balanceada_aux w 0 ⟹
balanceada_aux [B] (Suc 0) ⟹
balanceada_aux (w @ [B]) (0+Suc 0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (w @ [B]) (Suc 0)" using 1 2
by (simp only:Groups.monoid_add_class.add.left_neutral)
then have "balanceada_aux (A # (w @ [B])) 0"
by (simp only: balanceada_aux.simps(5))
then have "balanceada_aux ([A] @ w @ [B]) 0"
by (simp only: List.append_Cons List.append_Nil)
then show ?case by (simp only: balanceada.simps)
next
case (S3 v w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have 2:"balanceada_aux v 0" using S3(3)
by (simp only: balanceada.simps)
have "balanceada_aux v 0 ⟹
balanceada_aux w 0 ⟹
balanceada_aux (v @ w) (0+0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (v @ w) 0" using 1 2
by (simp only:Groups.monoid_add_class.add.right_neutral)
then show ?case by (simp only: balanceada.simps)
qed

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que balanceada es un reconocedor completo de
la gramática S; es decir,
balanceada w ⟹ w ∈ S
------------------------------------------------------------------ *}

(* benber *)
lemma balanceada_aux_unico:
"⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l
proof (induction w arbitrary: k l)
case Nil
hence "k = 0 ∧ l = 0" using balanceada_aux.elims by auto
thus ?case by simp
next
case IS: (Cons x w')
show ?case
proof (cases x)
case A
thus ?thesis using IS by auto
next
case B
show ?thesis
proof (cases k)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc k')
hence "balanceada_aux w' k'" using IS.prems `x = B` by simp

show ?thesis
proof (cases l)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc l')
hence "balanceada_aux w' l'" using IS.prems `x = B` by simp
thus ?thesis
using `balanceada_aux w' k'` IS.IH `k = Suc k'` `l = Suc l'`
by auto
qed
qed
qed
qed

lemma balanceada_completo_aux1:
"⟦balanceada (x # w @ [y]);
⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶ ¬ (balanceada v)⟧
⟹ x = A ∧ y = B ∧ balanceada w"
proof -
assume "balanceada (x # w @ [y])"
hence bal: "balanceada_aux ( x # w @ [y] ) 0" by simp

assume postfix_con: "⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶
¬ (balanceada v)"

have "x = A"
proof (rule ccontr)
assume "x ≠ A"
hence "x = B" using alfabeto.exhaust by blast
thus "False" using bal by simp
qed

have hl1: "balanceada_aux (w @ [y]) n ⟹ y = B" for w y n
proof (induction w arbitrary: n)
case IB: Nil
show "y = B"
proof (rule ccontr)
assume "y ≠ B"
hence "y = A" using alfabeto.exhaust by blast
thus "False" using IB by simp
qed
next
case IS: (Cons x w)
hence "balanceada_aux (x # w @ [y]) n" by simp
hence "∃m. balanceada_aux (w @ [y]) m" using balanceada_aux.elims(2)
by blast (* SH'd *)
thus "y = B" using IS.IH by auto
qed

have "y = B" using bal hl1[of "(x#w)"] by simp
hence "balanceada_aux (w @ [B]) 1" using bal `x = A` by simp

have hl2: "balanceada_aux (x#w) n ⟹ ∃m. balanceada_aux w m"
for x w n
proof (cases x)
case A
moreover assume "balanceada_aux (x#w) n"
ultimately show ?thesis by auto
next
case B
moreover assume "balanceada_aux (x#w) n"
ultimately have "balanceada_aux (B#w) n" by simp
thus ?thesis by (cases n) auto
qed

have "⟦balanceada_aux w n; u @ v = w⟧ ⟹ ∃ m. balanceada_aux v m"
for u v w n
proof (induction w arbitrary: u v n)
case Nil
hence "v = []" by simp
hence "balanceada_aux v 0" by simp
thus ?case ..
next
case IS: (Cons x w')
then obtain m where mDef: "balanceada_aux w' m" using hl2 by blast

show ?case
proof (cases u)
case Nil
hence "balanceada_aux v n" using IS by simp
thus ?thesis ..
next
case (Cons y u')
hence "w' = u' @ v" using IS.prems by simp
thus ?thesis using IS.IH mDef by simp
qed
qed
moreover have "balanceada_aux (w @ [B]) 1" using bal `x = A` `y = B`
by simp
ultimately have "u @ v = (w @ [B]) ⟹ ∃m. balanceada_aux v m"
for u v by auto
moreover {
fix u v
have 1: "⟦u' ≠ []; v ≠ []; u' @ v = (x # w @ [y])⟧ ⟹
¬(balanceada v)" for u'
using postfix_con by auto
have "⟦v ≠ []; (x#u) @ v = (x # w @ [y])⟧ ⟹ ¬(balanceada v)"
using 1[of "x#u"] by simp
hence "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹ ¬(balanceada_aux v 0)"
using `y = B` by simp
}
ultimately have hl3: "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹
∃m. balanceada_aux v (Suc m)" for u v
by (metis zero_induct) (* SH'd *)

have hl4: "⟦balanceada_aux (v @ [B]) (Suc n); ⋀s t. v = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)⟧
⟹ balanceada_aux v n" for v n
proof (induction v arbitrary: n)
case Nil
hence "balanceada_aux [B] (Suc n)" by simp
thus "balanceada_aux [] n" by simp
next
case IS: (Cons x v')

have "x#v' = [x] @ v'" by simp
then obtain m where mDef: "balanceada_aux (v' @ [B]) (Suc m)"
using IS.prems by blast
moreover have v'Postf: "⋀s t. v' = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)"
using IS.prems by auto
ultimately have "balanceada_aux v' m" using IS.IH by simp

show ?case
proof (cases x)
case A
hence "balanceada_aux ((A # v') @ [B]) (Suc n)" using IS.prems
by simp
hence "balanceada_aux (v' @ [B]) (Suc (Suc n))" by simp
hence "balanceada_aux v' (Suc n)" using IS.IH v'Postf by simp
thus ?thesis using `x = A` by simp
next
case B
hence "balanceada_aux ((B # v') @ [B]) (Suc n)" using IS.prems
by simp
hence 1: "balanceada_aux ( v' @ [B]) n" using IS.prems by simp

have "n = Suc m" using 1 mDef balanceada_aux_unico by simp
thus "balanceada_aux (x # v') n"
using `balanceada_aux v' m` `x = B` by simp
qed
qed
moreover note `balanceada_aux (w @ [B]) 1`
moreover have "w = s @ t ⟹ ∃m. balanceada_aux (t @ [B]) (Suc m)"
for s t using hl3 by simp
ultimately have "balanceada_aux w 0" by simp
thus "x = A ∧ y = B ∧ balanceada w" using `x = A` `y = B`by simp
qed

lemma balanceada_completo_aux2:
assumes "balanceada (u @ v)" and "¬ balanceada u"
shows "¬ balanceada v"
proof -
have "⟦balanceada_aux (u @ v) n; balanceada v⟧ ⟹ balanceada_aux u n"
for n
proof (induction u arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux_unico by simp
thus ?case by simp
next
case IS: (Cons x u')
show ?case
proof (cases x)
case A
hence "balanceada_aux (A # u' @ v) n" using IS.prems by simp
hence "balanceada_aux (u' @ v) (Suc n)" by simp
hence "balanceada_aux u' (Suc n)" using `balanceada v` IS.IH
by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B # u' @ v) n" using IS.prems by simp
then obtain m where "Suc m = n" by (cases n) auto
hence "balanceada_aux (B # u' @ v) (Suc m)" using 1 by simp
hence "balanceada_aux u' m" using `balanceada v` IS.IH by simp
hence "balanceada_aux (B # u') n" using `Suc m = n` by auto
thus ?thesis using `x = B` by simp
qed
qed
thus ?thesis using assms by auto
qed

lemma balanceada_completo:
assumes "balanceada w"
shows "w ∈ S"
proof -
have "balanceada w ⟹ w ∈ S"
proof (induction "length w" arbitrary: w rule: less_induct)
case IS: less

show ?case
proof (cases w)
case Nil
thus ?thesis using S1 by simp
next
case (Cons x w')
show ?thesis
proof (cases w')
case Nil
hence "¬ balanceada (x#w')" by (cases x) auto
hence "False" using `w = x # w'`IS.prems by simp
thus ?thesis ..
next
case (Cons y w'')
show ?thesis
proof cases
assume "∃u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
then obtain u v where "w = u @ v" and
"u ≠ []" and
"v ≠ []" and
"balanceada u"
and "balanceada v" by blast

have "u ∈ S" using `w = u @ v` `v ≠ []` `balanceada u` IS
by simp
moreover have "v ∈ S"
using `w = u @ v` `u ≠ []` `balanceada v` IS by simp
ultimately show "w ∈ S" using S3 `w = u @ v` by simp
next
assume "∄u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
hence 1: "⟦u @ v = w; u ≠ []; v ≠ []; balanceada u⟧ ⟹
¬ balanceada v" for u v by auto

have "w = x # y # w''" using `w = x # w'` `w' = y # w''`
by simp
moreover have "∃ u z. y # w'' = u @ [z]"
proof -
have "∃ u y. (x :: alfabeto) # v = u @ [y]" for x v
proof (induction v arbitrary: x)
case Nil
have "x # [] = [] @ [x]" by simp
thus ?case by simp
next
case IS: (Cons z v')
then obtain u' y' where "z # v' = u' @ [y']" by blast
hence "x # z # v' = x # u' @ [y']" using IS by simp
thus ?case by simp
qed
thus ?thesis by simp
qed
ultimately have "∃ u z. w = x # u @ [z]" by auto
then obtain u z where "w = x # u @ [z]" by blast
hence "balanceada (x # u @ [z])" using `balanceada w` by simp
moreover have "⟦s ≠ []; t ≠ []; s @ t = x # u @ [z]⟧ ⟹
¬ balanceada t" for s t
proof (cases "balanceada s")
case True
moreover assume "s ≠ []"
moreover assume "t ≠ []"
moreover assume "s @ t = x # u @ [z]"
ultimately show ?thesis using 1 `w = x # u @ [z]` by auto
next
case False

assume "s @ t = x # u @ [z]"
hence "x # u @ [z] = s @ t" ..
thus ?thesis
using balanceada_completo_aux2
`balanceada w`
`¬ balanceada s`
`w = x # u @ [z]`
by simp
qed
ultimately have "x = A" and "z = B" and "balanceada u"
using balanceada_completo_aux1[of x u z] by auto
moreover have "u ∈ S"
using `w = x # u @ [z]` IS `balanceada u` by simp
hence "x # u @ [z] ∈ S" using S2 `u ∈ S` `x = A` `z = B`
by simp
thus "w ∈ S" using `w = x # u @ [z]` by simp
qed
qed
qed
qed
thus ?thesis using assms .
qed

end
</source>

Relación 8

2019-03-01T13:13:16Z

Josgomrom4:

<source lang="isabelle">
chapter {* R8: Gramáticas libres de contexto *}

theory R8_Gramaticas_libre_de_contexto
imports Main
begin

text {*
En esta relación se definen dos gramáticas libres de contexto y se
demuestra que son equivalentes. Además, se define por recursión una
función para reconocer las palabras de la gramática y se demuestra que
es correcta y completa. *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Una gramática libre de contexto para las expresiones
parentizadas es
S ⟶ ε | '(' S ')' | SS
definir inductivamente la gramática S usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}

datatype alfabeto = A | B

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

text {*
---------------------------------------------------------------------
Ejercicio 2. Otra gramática libre de contexto para las expresiones
parentizadas es
T ⟶ ε | T '(' T ')'
definir inductivamente la gramática T usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}

inductive_set T :: "alfabeto list set" where
T1: "[] ∈ T"
| T2: "v ∈ T ⟹ w ∈ T ⟹ v @ [A] @ w @ [B] ∈ T"

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que T está contenido en S.
------------------------------------------------------------------ *}

(* benber alfmarcua antramhur josgomrom4 *)
lemma T_en_S:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S"
proof (induction rule: T.induct)
show "[] ∈ S" by (rule S1)
next
fix v w
assume "w ∈ S"
hence "[A] @ w @ [B] ∈ S" by (rule S2)
moreover assume "v ∈ S"
ultimately show "v @ [A] @ w @ [B] ∈ S" using S3 by simp
qed
thus ?thesis using assms .
qed

(* cammonagu *)
declare S1 [iff] S2[intro!,simp]

(* cammonagu *)
declare T1 [iff]

(* cammonagu *)
lemma T2ImpS: "w ∈ T ⟹ w ∈ S"
apply (erule T.induct)
apply simp
apply (blast intro: S3)
done

(* cammonagu *)
lemma T_en_S1:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S" using assms by (rule T2ImpS)
thus ?thesis using assms .
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S está contenido en T.
------------------------------------------------------------------ *}

(* benber *)
lemma S_en_T:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w

have "[] ∈ T" by (rule T1)
moreover assume "w ∈ T"
ultimately have "[] @ [A] @ w @ [B] ∈ T" by (rule T2)
thus "[A] @ w @ [B] ∈ T" by simp
next
fix v w
assume "v ∈ T"
moreover assume "w ∈ T"
moreover have "⟦v ∈ T; w ∈ T⟧ ⟹ v @ w ∈ T" for v w
proof (induction "length w + length v"
arbitrary: w v
rule: less_induct)
case IH: less

show "v @ w ∈ T"
proof (cases w rule: T.cases)
show "w ∈ T" using `w ∈ T`.
next
assume "w = []"
thus "v @ w ∈ T" using `v ∈ T` by simp
next
fix w1 w2
assume "w1 ∈ T" and "w2 ∈ T"
assume "w = w1 @ [A] @ w2 @ [B]"
hence 1: "v @ w = v @ w1 @ [A] @ w2 @ [B]" by simp

have "length w1 < length w" using `w = w1 @ [A] @ w2 @ [B]`
by simp
hence "length v + length w1 < length v + length w" by simp
moreover note `v ∈ T`
moreover note `w1 ∈ T`
ultimately have "v @ w1 ∈ T" using IH by simp
moreover note `w2 ∈ T`
ultimately have "(v @ w1) @ [A] @ w2 @ [B] ∈ T" by (rule T2)
thus "v @ w ∈ T" using 1 by simp
qed
qed
ultimately show "v @ w ∈ T" by simp
qed

(* alfmarcua antramhur *)
lemma S_en_T_2:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w
assume "w ∈ T"
have "[] @ [A] @ w @ [B] ∈ T" using T1 `w ∈ T` by (rule T2)
then show "[A] @ w @ [B] ∈ T" by (simp only: List.append.append_Nil)
next
fix w v
assume "v ∈ T"
show "w ∈ T ⟹ v @ w ∈ T"
proof (induction rule: T.induct)
show "v @ [] ∈ T" using `v ∈ T`
by (simp only: List.append.right_neutral)
next
fix va w
have "v @ va ∈ T ⟹ w ∈ T ⟹ (v @ va) @ [A] @ w @ [B] ∈ T "
by (rule T2)
then show "v @ va ∈ T ⟹ w ∈ T ⟹ v @ va @ [A] @ w @ [B] ∈ T "
by (simp only: List.append_assoc)
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S y T son iguales.
------------------------------------------------------------------ *}

(* benber cammonagu antramhur josgomrom4 *)
lemma S_igual_T:
"S = T"
using T_en_S S_en_T by auto

(* alfmarcua *)
lemma S_igual_T_2:
"S = T"
proof (rule equalityI)
show "S ⊆ T" using S_en_T by (rule subsetI)
next
show "T ⊆ S" using T_en_S by (rule subsetI)
qed

text {*
---------------------------------------------------------------------
Ejercicio 5. En lugar de una gramática, se puede usar el siguiente
procedimiento para determinar si la cadena es una sucesión de
paréntesis bien balanceada: se recorre la cadena de izquierda a
derecha contando cuántos paréntesis de necesitan para que esté bien
balanceada. Si el contador al final de la cadena es 0, la cadena está
bien balanceada.

Definir la función
balanceada :: alfabeto list ⇒ bool
tal que (balanceada w) se verifica si w está bien balanceada. Por
ejemplo,
balanceada [A,A,B,B] = True
balanceada [A,B,A,B] = True
balanceada [A,B,B,A] = False
Indicación: Definir balanceada usando la función auxiliar
balanceada_aux :: alfabeto list ⇒ nat ⇒ bool
tal que (balanceada_aux w 0) se verifica si w está bien balanceada.
------------------------------------------------------------------ *}

(* benber alfmarcua antramhur josgomrom4 *)
(* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
"balanceada_aux [] 0 = True"
| "balanceada_aux [] (Suc n) = False"
| "balanceada_aux (B#w) 0 = False"
| "balanceada_aux (B#w) (Suc n) = balanceada_aux w n"
| "balanceada_aux (A#w) n = balanceada_aux w (Suc n)"

fun balanceada :: "alfabeto list ⇒ bool" where
"balanceada w = balanceada_aux w 0"

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
gramática S; es decir,
w ∈ S ⟹ balanceada w
------------------------------------------------------------------ *}

(* benber *)
lemma balanceada_correcto_aux1:
"balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)"
proof (induction w arbitrary: n)
case Nil
assume "balanceada_aux [] n"
thus ?case by simp
next
case IS: (Cons x w)
show ?case
proof (cases x)
case A
note `balanceada_aux (x#w) n`
hence "balanceada_aux (A#w) n" using `x = A` by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@[B]) (Suc (Suc n))" using IS.IH by simp
hence "balanceada_aux ((A#w)@[B]) (Suc n)" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp

show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@[B]) (Suc m)" using IS.IH by simp
hence "balanceada_aux (w@[B]) n" using `n = Suc m` by simp
hence "balanceada_aux (B#(w@[B])) (Suc n)" by simp
thus ?thesis using `x = B` by simp
qed
qed
qed

lemma balanceada_correcto_aux2:
assumes "balanceada v"
shows "balanceada_aux w n ⟹ balanceada_aux (w @ v) n"
proof (induction w arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux.elims by auto
thus ?case using assms by simp
next
case IS: (Cons x w)
show "balanceada_aux ((x#w)@v) n"
proof (cases x)
case A
hence "balanceada_aux (A#w) n" using IS.prems by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@v) (Suc n)" using IS.IH by simp
hence "balanceada_aux (A#(w@v)) n" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp

show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@v) m" using IS.IH by simp
hence "balanceada_aux (B#(w@v)) (Suc m)" by simp
thus ?thesis using `x = B` `n = Suc m` by simp
qed
qed
qed

lemma balanceada_correcto:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada [] = balanceada_aux [] 0" by simp
also have "..." by simp
finally show ?case.
next
case S2
fix w
assume "balanceada w"
hence "balanceada_aux w 0" by simp
hence "balanceada_aux (w@[B]) 1" using balanceada_correcto_aux1
by simp
hence "balanceada_aux ([A] @ w @ [B]) 0" by simp
thus "balanceada ([A] @ w @ [B])" by simp
next
case S3
thus ?case using balanceada_correcto_aux2 by auto
qed

(* alfmarcua antramhur josgomrom4 *)
lemma balanceada_correcto_aux3:
shows "balanceada_aux v m ⟹
balanceada_aux w n ⟹
balanceada_aux (v @ w) (m+n)"
proof (induction v arbitrary: n m)
case Nil
then show ?case
proof (cases m)
case 0
then have "balanceada_aux w (m + n)" using Nil.prems(2)
by (simp only:Groups.monoid_add_class.add.left_neutral)
then show ?thesis by (simp only:List.append.append_Nil)
next
case (Suc mm)
then have "False" using Nil.prems(1)
by (simp only: balanceada_aux.simps(2))
then show ?thesis ..
qed
next
case IS:(Cons a v)
show "balanceada_aux ((a # v) @ w) (m + n)"
proof (cases a)
define k :: nat where "k = m + 1"
case A
then have "balanceada_aux v k" using `k = m + 1` IS.prems(1)
by simp
then have "balanceada_aux (v @ w) (k + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (v @ w) (Suc(m + n))" using `k = m + 1`
by simp
then have "balanceada_aux (A # (v @ w)) (m + n)"
by (simp only: balanceada_aux.simps(5))
then show ?thesis using `a = A`
by (simp only:List.append.append_Cons)
next
case B
then show ?thesis
proof (cases m)
case 0
then have "False" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(3))
then show ?thesis ..
next
case (Suc mm)
hence "balanceada_aux v mm" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (v @ w) (mm + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (B # (v @ w)) (Suc (mm + n))"
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (B # (v @ w)) (m + n)"
using `m = Suc mm` by (simp only: Nat.plus_nat.add_Suc)
then show ?thesis using `a=B`
by (simp only:List.append.append_Cons)
qed
qed
qed

lemma balanceada_correcto_2:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then show ?case by (simp only: balanceada.simps)
next
case (S2 w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then have 2:"balanceada_aux (B#[]) (Suc 0)"
by (simp only: balanceada_aux.simps(4))
have "balanceada_aux w 0 ⟹
balanceada_aux [B] (Suc 0) ⟹
balanceada_aux (w @ [B]) (0+Suc 0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (w @ [B]) (Suc 0)" using 1 2
by (simp only:Groups.monoid_add_class.add.left_neutral)
then have "balanceada_aux (A # (w @ [B])) 0"
by (simp only: balanceada_aux.simps(5))
then have "balanceada_aux ([A] @ w @ [B]) 0"
by (simp only: List.append_Cons List.append_Nil)
then show ?case by (simp only: balanceada.simps)
next
case (S3 v w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have 2:"balanceada_aux v 0" using S3(3)
by (simp only: balanceada.simps)
have "balanceada_aux v 0 ⟹
balanceada_aux w 0 ⟹
balanceada_aux (v @ w) (0+0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (v @ w) 0" using 1 2
by (simp only:Groups.monoid_add_class.add.right_neutral)
then show ?case by (simp only: balanceada.simps)
qed

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que balanceada es un reconocedor completo de
la gramática S; es decir,
balanceada w ⟹ w ∈ S
------------------------------------------------------------------ *}

(* benber *)
lemma balanceada_aux_unico:
"⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l
proof (induction w arbitrary: k l)
case Nil
hence "k = 0 ∧ l = 0" using balanceada_aux.elims by auto
thus ?case by simp
next
case IS: (Cons x w')
show ?case
proof (cases x)
case A
thus ?thesis using IS by auto
next
case B
show ?thesis
proof (cases k)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc k')
hence "balanceada_aux w' k'" using IS.prems `x = B` by simp

show ?thesis
proof (cases l)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc l')
hence "balanceada_aux w' l'" using IS.prems `x = B` by simp
thus ?thesis
using `balanceada_aux w' k'` IS.IH `k = Suc k'` `l = Suc l'`
by auto
qed
qed
qed
qed

lemma balanceada_completo_aux1:
"⟦balanceada (x # w @ [y]);
⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶ ¬ (balanceada v)⟧
⟹ x = A ∧ y = B ∧ balanceada w"
proof -
assume "balanceada (x # w @ [y])"
hence bal: "balanceada_aux ( x # w @ [y] ) 0" by simp

assume postfix_con: "⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶
¬ (balanceada v)"

have "x = A"
proof (rule ccontr)
assume "x ≠ A"
hence "x = B" using alfabeto.exhaust by blast
thus "False" using bal by simp
qed

have hl1: "balanceada_aux (w @ [y]) n ⟹ y = B" for w y n
proof (induction w arbitrary: n)
case IB: Nil
show "y = B"
proof (rule ccontr)
assume "y ≠ B"
hence "y = A" using alfabeto.exhaust by blast
thus "False" using IB by simp
qed
next
case IS: (Cons x w)
hence "balanceada_aux (x # w @ [y]) n" by simp
hence "∃m. balanceada_aux (w @ [y]) m" using balanceada_aux.elims(2)
by blast (* SH'd *)
thus "y = B" using IS.IH by auto
qed

have "y = B" using bal hl1[of "(x#w)"] by simp
hence "balanceada_aux (w @ [B]) 1" using bal `x = A` by simp

have hl2: "balanceada_aux (x#w) n ⟹ ∃m. balanceada_aux w m"
for x w n
proof (cases x)
case A
moreover assume "balanceada_aux (x#w) n"
ultimately show ?thesis by auto
next
case B
moreover assume "balanceada_aux (x#w) n"
ultimately have "balanceada_aux (B#w) n" by simp
thus ?thesis by (cases n) auto
qed

have "⟦balanceada_aux w n; u @ v = w⟧ ⟹ ∃ m. balanceada_aux v m"
for u v w n
proof (induction w arbitrary: u v n)
case Nil
hence "v = []" by simp
hence "balanceada_aux v 0" by simp
thus ?case ..
next
case IS: (Cons x w')
then obtain m where mDef: "balanceada_aux w' m" using hl2 by blast

show ?case
proof (cases u)
case Nil
hence "balanceada_aux v n" using IS by simp
thus ?thesis ..
next
case (Cons y u')
hence "w' = u' @ v" using IS.prems by simp
thus ?thesis using IS.IH mDef by simp
qed
qed
moreover have "balanceada_aux (w @ [B]) 1" using bal `x = A` `y = B`
by simp
ultimately have "u @ v = (w @ [B]) ⟹ ∃m. balanceada_aux v m"
for u v by auto
moreover {
fix u v
have 1: "⟦u' ≠ []; v ≠ []; u' @ v = (x # w @ [y])⟧ ⟹
¬(balanceada v)" for u'
using postfix_con by auto
have "⟦v ≠ []; (x#u) @ v = (x # w @ [y])⟧ ⟹ ¬(balanceada v)"
using 1[of "x#u"] by simp
hence "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹ ¬(balanceada_aux v 0)"
using `y = B` by simp
}
ultimately have hl3: "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹
∃m. balanceada_aux v (Suc m)" for u v
by (metis zero_induct) (* SH'd *)

have hl4: "⟦balanceada_aux (v @ [B]) (Suc n); ⋀s t. v = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)⟧
⟹ balanceada_aux v n" for v n
proof (induction v arbitrary: n)
case Nil
hence "balanceada_aux [B] (Suc n)" by simp
thus "balanceada_aux [] n" by simp
next
case IS: (Cons x v')

have "x#v' = [x] @ v'" by simp
then obtain m where mDef: "balanceada_aux (v' @ [B]) (Suc m)"
using IS.prems by blast
moreover have v'Postf: "⋀s t. v' = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)"
using IS.prems by auto
ultimately have "balanceada_aux v' m" using IS.IH by simp

show ?case
proof (cases x)
case A
hence "balanceada_aux ((A # v') @ [B]) (Suc n)" using IS.prems
by simp
hence "balanceada_aux (v' @ [B]) (Suc (Suc n))" by simp
hence "balanceada_aux v' (Suc n)" using IS.IH v'Postf by simp
thus ?thesis using `x = A` by simp
next
case B
hence "balanceada_aux ((B # v') @ [B]) (Suc n)" using IS.prems
by simp
hence 1: "balanceada_aux ( v' @ [B]) n" using IS.prems by simp

have "n = Suc m" using 1 mDef balanceada_aux_unico by simp
thus "balanceada_aux (x # v') n"
using `balanceada_aux v' m` `x = B` by simp
qed
qed
moreover note `balanceada_aux (w @ [B]) 1`
moreover have "w = s @ t ⟹ ∃m. balanceada_aux (t @ [B]) (Suc m)"
for s t using hl3 by simp
ultimately have "balanceada_aux w 0" by simp
thus "x = A ∧ y = B ∧ balanceada w" using `x = A` `y = B`by simp
qed

lemma balanceada_completo_aux2:
assumes "balanceada (u @ v)" and "¬ balanceada u"
shows "¬ balanceada v"
proof -
have "⟦balanceada_aux (u @ v) n; balanceada v⟧ ⟹ balanceada_aux u n"
for n
proof (induction u arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux_unico by simp
thus ?case by simp
next
case IS: (Cons x u')
show ?case
proof (cases x)
case A
hence "balanceada_aux (A # u' @ v) n" using IS.prems by simp
hence "balanceada_aux (u' @ v) (Suc n)" by simp
hence "balanceada_aux u' (Suc n)" using `balanceada v` IS.IH
by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B # u' @ v) n" using IS.prems by simp
then obtain m where "Suc m = n" by (cases n) auto
hence "balanceada_aux (B # u' @ v) (Suc m)" using 1 by simp
hence "balanceada_aux u' m" using `balanceada v` IS.IH by simp
hence "balanceada_aux (B # u') n" using `Suc m = n` by auto
thus ?thesis using `x = B` by simp
qed
qed
thus ?thesis using assms by auto
qed

lemma balanceada_completo:
assumes "balanceada w"
shows "w ∈ S"
proof -
have "balanceada w ⟹ w ∈ S"
proof (induction "length w" arbitrary: w rule: less_induct)
case IS: less

show ?case
proof (cases w)
case Nil
thus ?thesis using S1 by simp
next
case (Cons x w')
show ?thesis
proof (cases w')
case Nil
hence "¬ balanceada (x#w')" by (cases x) auto
hence "False" using `w = x # w'`IS.prems by simp
thus ?thesis ..
next
case (Cons y w'')
show ?thesis
proof cases
assume "∃u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
then obtain u v where "w = u @ v" and
"u ≠ []" and
"v ≠ []" and
"balanceada u"
and "balanceada v" by blast

have "u ∈ S" using `w = u @ v` `v ≠ []` `balanceada u` IS
by simp
moreover have "v ∈ S"
using `w = u @ v` `u ≠ []` `balanceada v` IS by simp
ultimately show "w ∈ S" using S3 `w = u @ v` by simp
next
assume "∄u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
hence 1: "⟦u @ v = w; u ≠ []; v ≠ []; balanceada u⟧ ⟹
¬ balanceada v" for u v by auto

have "w = x # y # w''" using `w = x # w'` `w' = y # w''`
by simp
moreover have "∃ u z. y # w'' = u @ [z]"
proof -
have "∃ u y. (x :: alfabeto) # v = u @ [y]" for x v
proof (induction v arbitrary: x)
case Nil
have "x # [] = [] @ [x]" by simp
thus ?case by simp
next
case IS: (Cons z v')
then obtain u' y' where "z # v' = u' @ [y']" by blast
hence "x # z # v' = x # u' @ [y']" using IS by simp
thus ?case by simp
qed
thus ?thesis by simp
qed
ultimately have "∃ u z. w = x # u @ [z]" by auto
then obtain u z where "w = x # u @ [z]" by blast
hence "balanceada (x # u @ [z])" using `balanceada w` by simp
moreover have "⟦s ≠ []; t ≠ []; s @ t = x # u @ [z]⟧ ⟹
¬ balanceada t" for s t
proof (cases "balanceada s")
case True
moreover assume "s ≠ []"
moreover assume "t ≠ []"
moreover assume "s @ t = x # u @ [z]"
ultimately show ?thesis using 1 `w = x # u @ [z]` by auto
next
case False

assume "s @ t = x # u @ [z]"
hence "x # u @ [z] = s @ t" ..
thus ?thesis
using balanceada_completo_aux2
`balanceada w`
`¬ balanceada s`
`w = x # u @ [z]`
by simp
qed
ultimately have "x = A" and "z = B" and "balanceada u"
using balanceada_completo_aux1[of x u z] by auto
moreover have "u ∈ S"
using `w = x # u @ [z]` IS `balanceada u` by simp
hence "x # u @ [z] ∈ S" using S2 `u ∈ S` `x = A` `z = B`
by simp
thus "w ∈ S" using `w = x # u @ [z]` by simp
qed
qed
qed
qed
thus ?thesis using assms .
qed

end
</source>

Relación 7

2019-02-13T17:52:34Z

Josgomrom4:

<source lang="isabelle">
chapter {* R7: Deducción natural de primer orden *}

theory R7_Deduccion_natural_de_primer_orden
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, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· 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

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
*}

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

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

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

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule ccontr)
assume "∄x. P a ⟶ Q x"

have "P a ⟶ (∃x. P a ⟶ Q x)"
proof
assume "P a"
with assms have "∃x. Q x" by (rule mp)
moreover have "⋀x. Q x ⟹ ∃x'. P a ⟶ Q x'"
proof -
fix x
assume "Q x"
hence "P a ⟶ Q x" by (rule impI)
thus "∃x'. P a ⟶ Q x'" by (rule exI)
qed
ultimately show "∃x. P a ⟶ Q x" by (rule exE)
qed
moreover note `∄x. P a ⟶ Q x`
ultimately have "¬(P a)" by (rule mt)

have "¬(P a) ⟶ (∃x. P a ⟶ Q x)"
proof
fix x
assume "¬(P a)"
have "P a ⟶ Q x"
proof
assume "P a"
with `¬(P a)` have "False" by (rule notE)
thus "Q x" by (rule FalseE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed
moreover note `∄x. P a ⟶ Q x`
ultimately have "¬¬(P a)" by (rule mt)
moreover note `¬(P a)`
ultimately show "False" by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
assume 1: "¬(p ∨ ¬p)"
have 2: "¬p" proof (rule notI)
assume p hence 3: "p ∨ ¬p" by (rule disjI1)
show "False" using 1 3 by (rule notE)
qed
have 4: "p ∨ ¬p" using 2 by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed

lemma ejercicio_1:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule disjE)
show "P a ∨ ¬ P a" by (rule ejercicio_52)
next
assume "P a"
have "∃x. Q x" using assms `P a` by (rule mp)
then obtain b where "Q b" by (rule exE)
have "P a ⟹ Q b" using `P a` `Q b` by simp
have "P a ⟶ Q b" using `P a ⟹ Q b` by (rule impI)
then show "∃x. P a ⟶ Q x" by (rule exI)
next
assume "¬ P a"
fix b
have "P a ⟶ Q b"
proof (rule impI)
assume "P a"
with `¬(P a)` have "False" by (rule notE)
then show "Q b" by (rule FalseE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_1:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule disjE)
show "¬P a ∨ P a" by (rule excluded_middle)
next
fix b
assume 3: "¬P a"
have "P a ⟶ Q b" proof (rule impI)
assume 4: "P a" show "Q b" using 3 4 by (rule notE)
qed
thus ?thesis by (rule exI)
next
assume 1: "P a"
have "∃x. Q x" using assms(1) 1 by (rule mp)
then obtain b where 2: "Q b" by (rule exE)
have "P a ⟶ Q b" proof (rule impI)
assume "P a" show "Q b" using 2 .
qed
thus ?thesis by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes A1: "∀x y z. R x y ∧ R y z ⟶ R x z"
and A2: "∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
{
fix x y
{
assume "R x y"
have "¬ (R y x)"
proof (rule ccontr)
assume "¬ ¬ (R y x)"
hence "R y x" by (rule notnotD)

note `∀x y z. R x y ∧ R y z ⟶ R x z`
moreover have "∀ y z. R x y ∧ R y z ⟶ R x z ⟹ False"
proof -
assume "∀ y z. R x y ∧ R y z ⟶ R x z"
moreover have "∀ z. R x y ∧ R y z ⟶ R x z ⟹ False"
proof -
assume "∀ z. R x y ∧ R y z ⟶ R x z"
moreover have "R x y ∧ R y x ⟶ R x x ⟹ False"
proof -
assume "R x y ∧ R y x ⟶ R x x"
moreover {
note `R x y`
moreover note `R y x`
ultimately have "R x y ∧ R y x" by (rule conjI)
}
ultimately have "R x x" by (rule mp)

note `∀x. ¬(R x x)`
moreover {
assume "¬(R x x)"
moreover note `R x x`
ultimately have "False" by (rule notE)
}
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
}
hence "R x y ⟶ ¬ (R y x)" by (rule impI)
}
hence "⋀x. ∀y. R x y ⟶ ¬ (R y x)" by (rule allI)
thus ?thesis by (rule allI)
qed

(* alfmarcua *)
lemma ejercicio_2:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix a
show "∀y. R a y ⟶ ¬ R y a"
proof (rule allI, rule impI)
fix b
assume "R a b"
show "¬ R b a"
proof (rule notI)
assume "R b a"
have "R a b ∧ R b a" using `R a b` `R b a` by (rule conjI)
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
then have "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
then have "R a b ∧ R b a ⟶ R a a" by (rule allE)
then have "R a a" using `R a b ∧ R b a` by (rule mp)
have "¬ (R a a)" using assms(2) by (rule allE)
then show False using `R a a` by (rule notE)
qed
qed
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_2:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix a
show "∀y. R a y ⟶ ¬(R y a)"
proof (rule allI)
fix b
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
have 2: "¬(R a a)" using assms(2) by (rule allE)
show "R a b ⟶ ¬(R b a)" proof (rule impI)
assume 3: "R a b"
show "¬(R b a)"
proof (rule ccontr)
assume "¬¬R b a"
hence 4: "R b a" by (rule notnotD)
have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
have 6: "R a a" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
qed
qed
qed

(* pabalagon *)
lemma ejercicio_2_2:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
{ fix a
{ fix b
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
have 2: "¬(R a a)" using assms(2) by (rule allE)
have "R a b ⟶ ¬(R b a)" proof (rule impI)
assume 3: "R a b"
show "¬(R b a)"
proof (rule ccontr)
assume "¬¬R b a"
hence 4: "R b a" by (rule notnotD)
have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
have 6: "R a a" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
qed}
hence "∀y. R a y ⟶ ¬(R y a)" by (rule allI)}
thus "∀x y. R x y ⟶ ¬(R y x)" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

(* benber pabbergue*)
(* No es cierto si el universo consiste en más que un objeto. En ese caso, asignar la igualdad (=) a P
es un contraejemplo. *)

(* alfmarcua *)
lemma ejercicio_3:
"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
oops

(* pabalagon pabbergue josgomrom4 *)
text{*
Contraejemplo en los naturales, para todo x existe y tal que x < y, pero no
existe y tal que para todo x, x < y
*}
lemma ejercicio_3: "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
------------------------------------------------------------------ *}

(* benber *)
lemma "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof
assume "∃y. ∀x. P x y"
moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y'. P x y'"
proof
fix x y
assume "∀x'. P x' y"
hence "P x y" by (rule allE)
thus "∃y'. P x y'" by (rule exI)
qed
ultimately show "∀x. ∃y. P x y" by (rule exE)
qed

(* alfmarcua *)
lemma ejercicio_4:
"(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI, rule allI)
fix a
assume "∃y. ∀x. P x y"
then obtain b where "∀x. P x b" by (rule exE)
then have "P a b" by (rule allE)
then show "∃y. P a y" by (rule exI)
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_4: "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI)
assume "∃y. ∀x. P x y"
moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y. P x y"
proof
fix x0 y0
assume "∀x. P x y0"
hence "P x0 y0" by (rule allE)
thus "∃y. P x0 y" by (rule exI)
qed
ultimately show "∀x. ∃y. P x y" by (rule exE)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes A1: "∀ x. P a x x"
and A2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof
from A2
have "∀y z. P a y z ⟶ P (f a) y (f z)" by (rule allE)
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
moreover have "P a (f a) (f a)" using A1 by (rule allE)
ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed

(* alfmarcua *)
lemma ejercicio_5:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof (rule exI, rule mp)
show "P a (f a) (f a)" using assms(1) by (rule allE)
next
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
then show "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_5:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof (rule exI)
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
moreover have "P a (f a) (f a)" using assms(1) by (rule allE)
ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}

(* benber alfmarcua *)
lemma
assumes "∀y. Q a y"
and "∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof
have "Q a a" using `∀y. Q a y` by (rule allE)
moreover have "Q a (s (s a))" using `∀y. Q a y` by (rule allE)
ultimately show "Q a a ∧ Q a (s (s a))" by (rule conjI)
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_6:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof (rule exI)
have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
moreover have "Q a (s a)" using assms(1) by (rule allE)
ultimately have "Q (s a) (s (s a))" by (rule mp)
with `Q a (s a)` show "Q a (s a) ∧ Q (s a) (s (s a))" by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
Or : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

(* benber alfmarcua pabalagon marfruman1 josgomrom4 *)
lemma
assumes "A ∨ P ⟶ R ∧ F"
and "F ∨ N ⟶ Or"
shows "A ⟶ Or"
proof
assume "A"
hence "A ∨ P" by (rule disjI1)
with `A ∨ P ⟶ R ∧ F` have "R ∧ F" by (rule mp)
hence "F" by (rule conjunct2)
hence "F ∨ N" by (rule disjI1)
with `F ∨ N ⟶ Or` show "Or" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes "A ⟶ (M ⟷ ¬B)"
and "A ∨ B"
shows "¬B ⟶ M"
proof
assume "¬B"
note `A ∨ B`
moreover {
assume "A"
with `A ⟶ (M ⟷ ¬B)` have "M ⟷ ¬B" by (rule mp)
hence "¬B ⟹ M" by (rule iffD2)
hence "M" using `¬B` .
}
moreover {
note `¬B`
moreover assume "B"
ultimately have "M" by (rule notE)
}
ultimately show "M" by (rule disjE)
qed

(* alfmarcua marfruman1 *)
lemma ejercicio_8:
assumes "A ∧ ¬ B ⟶ M"
"A ∨ B"
shows "¬ B ⟶ M"
proof (rule impI)
assume "¬B"
show "M" using assms(2)
proof (rule disjE)
assume "A"
then have "A ∧ ¬ B" using `¬ B` by (rule conjI)
show "M" using assms(1) `A ∧ ¬ B` by (rule mp)
next
assume "B"
show "M" using `¬ B` `B` by (rule notE)
qed
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_8:
assumes "A ⟶ (M ⟷ ¬B)"
"A ∨ B"
shows "¬B ⟶ M"
using assms(2) proof (rule disjE)
assume 1: A
have 2: "M ⟷ ¬B" using assms(1) 1 by (rule mp)
show "¬B ⟶ M" proof (rule impI)
assume 3: "¬B" show M using 2 3 by (rule iffD2)
qed
next
assume 4: B
show ?thesis proof (rule impI)
assume "¬B" thus M using 4 by (rule notE)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
la corrección, del siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes "∀x. ¬ R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof -
have 0: "p ∨ ¬ p" for p
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
moreover {
have "p"
proof (rule ccontr)
assume "¬ p"
hence "p ∨ ¬ p" by (rule disjI2)
with `¬ (p ∨ ¬ p)` show "False" by (rule notE)
qed
hence "p ∨ ¬ p" by (rule disjI1)
}
ultimately show "False" by (rule notE)
qed

have "¬ R x ⟶ R (p x)" for x using assms(1) by (rule allE)
hence 1: "¬ R x ⟹ R (p x)" for x by (rule mp)

have 2: "⟦R y; ¬ R (p y)⟧ ⟹ ?thesis" for y
proof
assume "R y"
assume "¬ R (p y)"
hence "R (p (p y))" by (rule 1)
with `R y` show "R y ∧ R (p (p y))" by (rule conjI)
qed

have 3: "R y ⟹ ?thesis" for y
proof -
assume "R y"

have "R (p y) ∨ ¬ R (p y)" by (rule 0)
moreover {
assume "R (p y)"
have "R (p (p y)) ∨ ¬ R (p (p y))" by (rule 0)
moreover {
assume "R (p (p y))"
with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
hence ?thesis by (rule exI)
}
moreover {
assume "¬ R (p (p y))"
with `R (p y)` have ?thesis by (rule 2)
}
ultimately have ?thesis by (rule disjE)
}
moreover {
assume "¬ R (p y)"
with `R y` have ?thesis by (rule 2)
}
ultimately show ?thesis by (rule disjE)
qed

fix y
have "R y ∨ ¬ R y" by (rule 0)
moreover {
assume "R y"
hence ?thesis by (rule 3)
}
moreover {
assume "¬ R y"
hence "R (p y)" by (rule 1)
hence ?thesis by (rule 3)
}
ultimately show ?thesis by (rule disjE)
qed

(* alfmarcua *)
lemma ejercicio_9:
assumes "∀ x. ¬ R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof (rule disjE, rule ejercicio_52)
have prelemma:"(∃y. ¬ R (p y)) ⟶ ?thesis"
proof (rule impI)
assume "∃y. ¬ R (p y)"
then obtain b where "¬ R (p b)" by (rule exE)
have "¬ R (p b) ⟶ R (p (p b))" using assms by (rule allE)
then have "R (p (p b))" using `¬ R (p b)` by (rule mp)
have "¬ R b ⟶ R (p b)" using assms by (rule allE)
then have "¬¬ R b" using `¬ R (p b)` by (rule mt)
then have "R b" by (rule notnotD)
then have "R b ∧ R (p (p b))" using `R (p (p b))` by (rule conjI)
then show "∃x. R x ∧ R (p (p x))" by (rule exI)
qed

fix a
show "R (p a) ⟹ ?thesis"
proof (rule disjE, rule ejercicio_52)
assume "R (p a)"
show "R (p (p a)) ⟹ ?thesis"
proof (rule disjE, rule ejercicio_52)
assume "R (p (p (p a)))"
have "R (p a) ∧ R (p (p (p a)))" using `R (p a)` `R (p (p (p a)))` by (rule conjI)
then show ?thesis by (rule exI)
next
assume "¬ R (p (p (p a)))"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed
next
assume "¬ R (p (p a))"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed

assume "¬ R (p a)"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed

(* pabalagon marfruman1 josgomrom4 *)
lemma ejercicio_9:
assumes "∀x. ¬R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof -
fix y
have s1: "⟦¬R (p y)⟧ ⟹ ?thesis" for y proof (rule exI)
assume 2: "¬R (p y)"
have "¬R (p y) ⟶ R (p (p y))" using assms(1) by (rule allE)
hence 3: "R (p (p y))" using 2 by (rule mp)
have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
hence "¬¬R y" using 2 by (rule mt)
hence "R y" by (rule notnotD)
thus "R y ∧ R (p (p y))" using 3 by (rule conjI)
qed
have s2: "R y ⟹ ?thesis" for y proof -
assume 2: "R y"
have "¬R (p y) ∨ R (p y)" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume 3: "¬R (p y)" thus ?thesis by (rule s1)
next
assume 4: "R (p y)"
have "¬R (p (p y)) ∨ R (p (p y))" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume "¬R (p (p y))" thus ?thesis by (rule s1)
next
assume "R (p (p y))"
with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
thus ?thesis by (rule exI)
qed
qed
qed
have "¬R y ∨ R y" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume 2: "R y" thus ?thesis by (rule s2)
next
assume 4: "¬R y"
have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
hence "R (p y)" using 4 by (rule mp)
thus ?thesis by (rule s2)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) Formalizar, y decidir
la corrección, del siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes "∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)"
and "∀x. E x ⟶ ¬ Ap j x"
shows "(∃x. E x ∧ N x) ⟶ ¬ Af j"
proof
assume "∃x. E x ∧ N x"

show "¬ Af j"
proof (rule ccontr)
assume "¬ ¬ Af j"
hence "Af j" by (rule notnotD)

note `∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)`
hence "Af j ⟶ (∀x. E x ⟶ Ap j x)" by (rule allE)
moreover note `Af j`
ultimately have "∀x. E x ⟶ Ap j x" by (rule mp)

note `∃x. E x ∧ N x`
moreover have "E x ∧ N x ⟹ False" for x
proof -
assume "E x ∧ N x"
hence "E x" by (rule conjunct1)

note `∀x. E x ⟶ Ap j x`
hence "E x ⟶ Ap j x" by (rule allE)
hence "Ap j x" using `E x` by (rule mp)

note `∀x. E x ⟶ ¬ Ap j x`
hence "E x ⟶ ¬ Ap j x" by (rule allE)
hence "¬ Ap j x" using `E x` by (rule mp)
thus "False" using `Ap j x` by (rule notE)
qed
ultimately show "False" by (rule exE)
qed
qed

(* alfmarcua marfruman1 *)
lemma ejercicio_10:
assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
"∀y. E y ⟶ ¬ Ap j y"
shows "(∃y. E y ∧ N y) ⟶ ¬ Af j"
proof (rule impI)
assume "∃x. E x ∧ N x"
then obtain a where "E a ∧ N a" by (rule exE)
then have "E a" by (rule conjunct1)
show "¬ Af j"
proof (rule notI, rule notE)
assume "Af j"
then show "Af j ∧ E a" using `E a` by (rule conjI)
next
have "E a ⟶ ¬ Ap j a" using assms(2) by (rule allE)
then have "¬ Ap j a" using `E a` by (rule mp)
have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
then have "Af j ∧ E a ⟶ Ap j a" by (rule allE)
then show "¬ (Af j ∧ E a)" using `¬ Ap j a` by (rule mt)
qed
qed

(* pabalagon josgomrom4 *)
lemma ejercicio_10:
assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
"∀x y. x = j ∧ E y ⟶ ¬(Ap x y)"
shows "(∃ x. (E x ∧ N x)) ⟶ ¬(Af j)"
proof (rule impI)
assume 1: "∃x. E x ∧ N x"
show "¬(Af j)" proof (rule ccontr)
fix a
assume "¬¬Af j" hence 2: "Af j" by (rule notnotD)
obtain a where 3: "E a ∧ N a" using 1 by (rule exE)
hence 4: "E a" by (rule conjunct1)
have 5: "N a" using 3 by (rule conjunct2)
have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
hence 6: "Af j ∧ E a ⟶ Ap j a" by (rule allE)
have 7: "Af j ∧ E a" using 2 4 by (rule conjI)
have 8: "Ap j a" using 6 7 by (rule mp)
have "∀y. j = j ∧ E y ⟶ ¬(Ap j y)" using assms(2) by (rule allE)
hence 9: "j = j ∧ E a ⟶ ¬(Ap j a)" by (rule allE)
have "j = j" by (rule refl)
hence 10: "j = j ∧ E a" using 4 by (rule conjI)
have "¬(Ap j a)" using 9 10 by (rule mp)
thus False using 8 by (rule notE)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

(* benber *)
lemma
assumes A1: "∀x. P x ⟶ R x"
and A2: "∀x. P x ⟶ (¬(Q x) ⟶ R x)"
and "¬(R a)"
shows "P a ⟶ Q a"
proof
have "P a ⟶ (¬(Q a) ⟶ R a)" using A2 by (rule allE)
moreover assume "P a"
ultimately have "¬(Q a) ⟶ R a" by (rule mp)

show "Q a"
proof (rule ccontr)
assume "¬(Q a)"
with `¬(Q a) ⟶ R a` have "R a" by (rule mp)
with `¬(R a)` show "False" by (rule notE)
qed
qed

(* alfmarcua *)
lemma ejercicio_11:
assumes "∄x. P x ∧ R x"
"∀x. P x ∧ (¬ Q x) ⟶ R x"
shows "P a ⟶ Q a"
proof (rule impI, rule ccontr)
assume "P a" "¬ Q a"
then have "P a ∧ (¬ Q a)" by (rule conjI)
have "P a ∧ (¬ Q a) ⟶ R a" using assms(2) by (rule allE)
then have "R a" using `P a ∧ (¬ Q a)` by (rule mp)
have "P a ∧ R a" using `P a` `R a` by (rule conjI)
then have "∃x. P x ∧ R x" by (rule exI)
show False using assms(1) `∃x. P x ∧ R x` by (rule notE)
qed

(* pabalagon marfruman1 josgomrom4 *)
lemma ejercicio_11:
assumes "¬(∃x. P x ∧ R x)"
"∀x. P x ∧ ¬Q x ⟶ R x"
shows "P a ⟶ Q a"
proof (rule impI)
assume 1: "P a"
show "Q a" proof (rule ccontr)
assume 2: "¬Q a"
have 3: "P a ∧ ¬Q a" using 1 2 by (rule conjI)
have 4: "P a ∧ ¬ Q a ⟶R a" using assms(2) by (rule allE)
hence 5: "R a" using 3 by (rule mp)
have 6: "P a ∧ R a" using 1 5 by (rule conjI)
hence 7: "∃x. P x ∧ R x" by (rule exI)
show False using assms(1) 7 by (rule notE)
qed
qed

end
</source>

Relación 6

2019-02-13T17:42:09Z

Josgomrom4:

<source lang="isabelle">
chapter {* R6: Deducción natural proposicional *}

theory R6_Deduccion_natural_proposicional
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

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

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

section {* Implicaciones *}

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

(* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar gleherlop giafus1
marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed

(* benber alfmarcua *)
lemma ejercicio_1_1:
assumes "p ⟶ q"
"p"
shows "q"
using assms by (rule mp)

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 chrgencar giafus1
marfruman1 alfmarcua enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_2:
assumes 1: "p ⟶ q" and
2: "q ⟶ r" and
3: "p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed

(* benber *)
lemma ejercicio_2_1:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using `p ⟶ q` `p` by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 chrgencar giafus1
marfruman1 alfmarcua enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_3:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"
proof -
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_3_1:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show "r" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2 gleherlop giafus1
marfruman1 alfmarcua enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_4:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{ assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
thus "p ⟶ r" by (rule impI)
qed

(* benber *)
lemma ejercicio_4_1:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof
assume p
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 giafus1 gleherlop
marfruman1 alfmarcua enrparalv chrgencar pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_5:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
show "r" using 4 2 by (rule mp)
qed
qed

(* benber josgomrom4 cammonagu *)
lemma ejercicio_5_1:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
thus "r" using `q` by (rule mp)
qed
qed

(* pabalagon *)
lemma ejercicio_5_2:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{ assume 2: "q"
{ assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)}
hence "p ⟶ r" by (rule impI)
}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1
marfruman1 alfmarcua enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_6:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed

(* benber josgomrom4 *)
lemma ejercicio_6_1:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ⟶ q` `p` have "q" by (rule mp)
ultimately show "r" by (rule mp)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_7:
assumes 1: "p"
shows "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed

(* benber cammonagu chrgencar *)
lemma ejercicio_7_1:
assumes "p"
shows "q ⟶ p"
proof
show "p" using `p` .
qed

(* alfmarcua *)
lemma ejercicio_7_2:
assumes "p"
shows "q ⟶ p"
using assms by (rule impI)

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
qed

(* benber cammonagu gleherlop chrgencar alfmarcua *)
lemma ejercicio_8_1:
"p ⟶ (q ⟶ p)"
using ejercicio_7_1 by (rule impI)

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv gleherlop antramhur alikan hugrubsan *)
lemma ejercicio_9:
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
qed

(* benber josgomrom4 cammonagu chrgencar pabbergue *)
lemma ejercicio_9_1:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof
assume "q ⟶ r"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_10:
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume 2: "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume 3: "q"
show "p ⟶ s"
proof (rule impI)
assume 4: "p"
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
show "s" using 6 2 by (rule mp)
qed
qed
qed

(* benber josgomrom4 cammonagu chrgencar giafus1 *)
lemma ejercicio_10_1:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q ⟶ (p ⟶ s)"
proof
assume "q"
show "p ⟶ s"
proof
assume "p"
with `p ⟶ (q ⟶ (r ⟶ s))`
have "q ⟶ (r ⟶ s)" by (rule mp)
hence "r ⟶ s" using `q` by (rule mp)
thus "s" using `r` by (rule mp)
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua chrgencar pabbergue alikan hugrubsan *)
lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
qed

(* pabalagon raffergon2 marfruman1 enrparalv antramhur *)
lemma ejercicio_11_2:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
qed

(* benber *)
lemma ejercicio_11_1:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume p
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show r by (rule mp)
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_12:
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"
proof (rule impI)
assume 5: "p"
show "q" using 3 by this
qed
show "r" using 1 4 by (rule mp)
qed
qed

(* benber josgomrom4 cammonagu giafus1 alfmarcua chrgencar *)
lemma ejercicio_12_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed
qed

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
using assms(1, 2) by (rule conjI)

(* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar gleherlop pabbergue antramhur hugrubsan *)
lemma ejercicio_13_1:
assumes "p"
"q"
shows "p ∧ q"
using assms by (rule conjI)

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

(* pabalagon josgomrom4 *)
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
using assms(1) by (rule conjunct1)

(* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar pabbergue gleherlop antramhur hugrubsan *)
lemma ejercicio_14_1:
assumes "p ∧ q"
shows "p"
using assms by (rule conjunct1)

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 *)
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
using assms(1) by (rule conjunct2)

(* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar pabbergue antramhur gleherlop hugrubsan *)
lemma ejercicio_15_1:
assumes "p ∧ q"
shows "q"
using assms by (rule conjunct2)

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur hugrubsan *)
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∧ r" using assms(1) by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "p ∧ q" using 1 3 by (rule conjI)
show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
qed

(* benber *)
lemma ejercicio_16_1:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof - (* TODO? *)
have "q ∧ r" using assms by (rule conjunct2)

have "p" using assms by (rule conjunct1)
moreover have "q" using `q ∧ r` by (rule conjunct1)
ultimately have "p ∧ q" by (rule conjI)
moreover have "r" using `q ∧ r` by (rule conjunct2)
ultimately show "(p ∧ q) ∧ r" by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_17:
assumes 1: "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have 2: "r" using 1 by (rule conjunct2)
have 3: "p ∧ q" using 1 by (rule conjunct1)
have 4: "p" using 3 by (rule conjunct1)
have 5: "q" using 3 by (rule conjunct2)
have 6: "q ∧ r" using 5 2 by (rule conjI)
show ?thesis using 4 6 by (rule conjI)
qed

(* benber *)
lemma ejercicio_17_1:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have "p ∧ q" using assms by (rule conjunct1)

have "p" using `p ∧ q` by (rule conjunct1)
moreover have "q ∧ r"
proof (rule conjI)
show "q" using `p ∧ q` by (rule conjunct2)
next
show "r" using assms by (rule conjunct2)
qed
ultimately show ?thesis by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

(* pabalagon raffergon2 marfruman1*)
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms(1) by (rule conjunct2)
qed

(* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_18_1:
assumes "p ∧ q"
shows "p ⟶ q"
proof
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using 1 by (rule conjunct1)
have 4: "p ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 3 2 by (rule mp)
have 6: "r" using 4 2 by (rule mp)
show "q ∧ r" using 5 6 by (rule conjI)
qed

(* benber cammonagu *)
lemma ejercicio_19_1:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume p
show "q ∧ r"
proof
have "p ⟶ q" using assms by (rule conjunct1)
thus "q" using `p` by (rule mp)
next
have "p ⟶ r" using assms by (rule conjunct2)
thus "r" using `p` by (rule mp)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_20:
assumes 1: "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "q" using 3 by (rule conjunct1)
qed
show "p ⟶ r"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "r" using 3 by (rule conjunct2)
qed
qed

(* benber *)
lemma ejercicio_20_1:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
show "p ⟶ q"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "q" by (rule conjunct1)
qed
next
show "p ⟶ r"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "r" by (rule conjunct2)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_21:
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

(* benber *)
lemma ejercicio_21_1:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ∧ q` have "q" by (rule conjunct2)
ultimately show "r" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_22:
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

(* benber *)
lemma ejercicio_22_1:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
with `p` have "p ∧ q" by (rule conjI)
with `p ∧ q ⟶ r` show "r" by (rule mp)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_23:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using 2 by (rule conjunct2)
qed
show "r" using 1 3 by (rule mp)
qed

(* benber *)
lemma ejercicio_23_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "q" by (rule conjunct2)
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_24:
assumes 1: "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume 2: "p ⟶ q"
have 3: "p" using 1 by (rule conjunct1)
have 4: "q ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 2 3 by (rule mp)
show 6: "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_24_1:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
have "q ⟶ r" using assms by (rule conjunct2)

assume "p ⟶ q"
moreover have "p" using assms by (rule conjunct1)
ultimately have "q" by (rule mp)
with `q ⟶ r` show r by (rule mp)
qed

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1 alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
using assms(1) by (rule disjI1)

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
using assms(1) by (rule disjI2)

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_27:
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1 proof (rule disjE)
assume 2: "p" thus "q ∨ p" by (rule disjI2)
next
assume 3: "q" thus "q ∨ p" by (rule disjI1)
qed

(* benber alfmarcua gleherlop *)
lemma ejercicio_27_1:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms .
moreover have "p ⟹ q ∨ p" by (rule disjI2)
moreover have "q ⟹ q ∨ p" by (rule disjI1)
ultimately show "q ∨ p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar gleherlop alfmarcua pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_28:
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2: "p ∨ q" show "p ∨ r" using 2
proof (rule disjE)
assume 3: p thus "p ∨ r" by (rule disjI1)
next
assume 4: q have r using 1 4 by (rule mp)
thus "p ∨ r" by (rule disjI2)
qed
qed

(* benber *)
lemma ejercicio_28_1:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
moreover have "p ⟹ p ∨ r" by (rule disjI1)
moreover have "q ⟹ p ∨ r"
proof (rule disjI2)
assume "q"
with `q ⟶ r` show "r" by (rule mp)
qed
ultimately show "p ∨ r" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

(* pabalagon marfruman1 *)
lemma ejercicio_29:
assumes 1: "p ∨ p"
shows "p"
using 1 proof (rule disjE)
assume "p" thus "p" .
next
assume "p" thus "p" .
qed

(* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_29_1:
assumes "p ∨ p"
shows "p"
using assms by (rule disjE)

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

(* pabalagon manperjim benber josgomrom4 raffergon2 marfruman1 chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
using assms(1) by (rule disjI1)

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_31:
assumes 1: "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r" (is "?R")
using 1 proof (rule disjE)
assume "p" hence "p ∨ q" by (rule disjI1)
thus ?R by (rule disjI1)
next
assume "q ∨ r" thus ?R
proof (rule disjE)
assume "q" hence "p ∨ q" by (rule disjI2)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "r" thus ?thesis by (rule disjI2)
qed
qed

(* benber *)
lemma ejercicio_31_1:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have "p ∨ (q ∨ r)" using assms .
moreover {
assume "p"
hence "p ∨ q" by (rule disjI1)
hence "(p ∨ q) ∨ r" by (rule disjI1)
}
moreover {
assume "q ∨ r"
moreover {
assume "q"
hence "p ∨ q" by (rule disjI2)
hence "(p ∨ q) ∨ r" by (rule disjI1)
}
moreover {
assume "r"
hence "(p ∨ q) ∨ r" by (rule disjI2)
}
ultimately have "(p ∨ q) ∨ r" by (rule disjE)
}
ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_32:
assumes 1: "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1 proof (rule disjE)
assume "p ∨ q" thus ?thesis
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume q hence "q ∨ r" by (rule disjI1)
thus ?thesis by (rule disjI2)
qed
next
assume r hence "q ∨ r" by (rule disjI2)
thus ?thesis by (rule disjI2)
qed

(* benber *)
lemma ejercicio_32_1:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
proof -
have "(p ∨ q) ∨ r" using assms .
moreover {
assume "p ∨ q"
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "q"
hence "q ∨ r" by (rule disjI1)
hence ?thesis by (rule disjI2)
}
ultimately have ?thesis by (rule disjE)
}
moreover {
assume "r"
hence "q ∨ r" by (rule disjI2)
hence ?thesis by (rule disjI2)
}
ultimately show ?thesis by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop alfmarcua pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_33:
assumes 1: "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2: p using 1 by (rule conjunct1)
show ?thesis
proof (rule disjE)
assume 3: q have "p ∧ q" using 2 3 by (rule conjI)
thus ?thesis by (rule disjI1)
next
assume 4: r have "p ∧ r" using 2 4 by (rule conjI)
thus ?thesis by (rule disjI2)
next
show "q ∨ r" using 1 by (rule conjunct2)
qed
qed

(* benber *)
lemma ejercicio_33_1:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have "p" using assms by (rule conjunct1)

have "q ∨ r" using assms by (rule conjunct2)
moreover {
assume "q"
with `p` have "p ∧ q" by (rule conjI)
hence ?thesis by (rule disjI1)
}
moreover {
assume "r"
with `p` have "p ∧ r" by (rule conjI)
hence ?thesis by (rule disjI2)
}
ultimately show ?thesis by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms(1) proof (rule disjE)
assume 2: "p ∧ q" hence q by (rule conjunct2)
hence 3: "q ∨ r" by (rule disjI1)
have p using 2 by (rule conjunct1)
thus ?thesis using 3 by (rule conjI)
next
assume 4: "p ∧ r" hence r by (rule conjunct2)
hence 5: "q ∨ r" by (rule disjI2)
have p using 4 by (rule conjunct1)
thus ?thesis using 5 by (rule conjI)
qed

(* benber *)
lemma ejercicio_34_1:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have "(p ∧ q) ∨ (p ∧ r)" using assms .
moreover {
assume "p ∧ q"
hence "p" by (rule conjunct1)
moreover {
have "q" using `p ∧ q` by (rule conjunct2)
hence "q ∨ r" by (rule disjI1)
}
ultimately have ?thesis by (rule conjI)
}
moreover {
assume "p ∧ r"
hence "p" by (rule conjunct1)
moreover {
have "r" using `p ∧ r` by (rule conjunct2)
hence "q ∨ r" by (rule disjI2)
}
ultimately have ?thesis by (rule conjI)
}
ultimately show ?thesis by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms(1) proof (rule disjE)
assume 1: p hence 2: "p ∨ r" by (rule disjI1)
have "p ∨ q" using 1 by (rule disjI1)
thus ?thesis using 2 by (rule conjI)
next
assume 3: "q ∧ r" hence r by (rule conjunct2)
hence 4: "p ∨ r" by (rule disjI2)
have q using 3 by (rule conjunct1)
hence "p ∨ q" by (rule disjI2)
thus ?thesis using 4 by (rule conjI)
qed

(* benber *)
lemma ejercicio_35_1:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have "p ∨ (q ∧ r)" using assms .
moreover {
assume "p"
hence "p ∨ q" by (rule disjI1)
moreover have "p ∨ r" using `p` by (rule disjI1)
ultimately have ?thesis by (rule conjI)
}
moreover {
assume "q ∧ r"
{
have "q" using `q ∧ r` by (rule conjunct1)
hence "p ∨ q" by (rule disjI2)
}
moreover {
have "r" using `q ∧ r` by (rule conjunct2)
hence "p ∨ r" by (rule disjI2)
}
ultimately have ?thesis by (rule conjI)
}
ultimately show ?thesis by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_36:
assumes 1: "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have 2: "p ∨ q" using 1 by (rule conjunct1)
have 3: "p ∨ r" using 1 by (rule conjunct2)
show ?thesis using 2
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume 4: q show ?thesis using 3
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume 5: r have "q ∧ r" using 4 5 by (rule conjI)
thus ?thesis by (rule disjI2)
qed
qed
qed

(* benber *)
lemma ejercicio_36_1:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p ∨ q" using assms by (rule conjunct1)
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "q"
have "p ∨ r" using assms by (rule conjunct2)
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "r"
with `q` have "q ∧ r" by (rule conjI)
hence ?thesis by (rule disjI2)
}
ultimately have ?thesis by (rule disjE)
}
ultimately show ?thesis by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_37:
assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
have 2: "p ⟶ r" using 1 by (rule conjunct1)
have 3: "q ⟶ r" using 1 by (rule conjunct2)
assume 4: "p ∨ q" show "r" using 4
proof (rule disjE)
assume 5: "p" show "r" using 2 5 by (rule mp)
next
assume 6: "q" show "r" using 3 6 by (rule mp)
qed
qed

(* benber *)
lemma ejercicio_37_1:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
assume "p ∨ q"
moreover {
have "p ⟶ r" using assms by (rule conjunct1)
moreover assume "p"
ultimately have "r" by (rule mp)
}
moreover {
have "q ⟶ r" using assms by (rule conjunct2)
moreover assume "q"
ultimately have "r" by (rule mp)
}
ultimately show "r" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan *)
lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
show "p ⟶ r"
proof (rule impI)
assume "p" hence 1: "p ∨ q" by (rule disjI1)
show "r" using assms(1) 1 by (rule mp)
qed
next
show "q ⟶ r"
proof (rule impI)
assume q hence 2: "p ∨ q" by (rule disjI2)
show r using assms(1) 2 by (rule mp)
qed
qed

(* benber *)
lemma ejercicio_38_1:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
show "p ⟶ r"
proof
assume "p"
hence "p ∨ q" by (rule disjI1)
with assms show "r" by (rule mp)
qed
next
show "q ⟶ r"
proof
assume "q"
hence "p ∨ q" by (rule disjI2)
with assms show "r" by (rule mp)
qed
qed

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

(* pabalagon manperjim benber josgomrom4 raffergon2 gleherlop marfruman1 chrgencar alfmarcua pabbergue enrparalv hugrubsan *)
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
using assms(1) by (rule notnotI)

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue gleherlop enrparalv hugrubsan *)
lemma ejercicio_40:
assumes 1: "¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: p show q using 1 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_40_1:
assumes "¬p"
shows "p ⟶ q"
proof
assume "p"
with `¬p` show "q" by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv hugrubsan *)
lemma ejercicio_41:
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
qed

(* benber *)
lemma ejercicio_41_1:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with `p ⟶ q` show "¬p" by (rule mt)
qed

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

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv hugrubsan *)
lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
using assms(1) proof (rule disjE)
assume "p" thus "p" .
next
assume 2: "q" show "p" using assms(2) 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_42_1:
assumes "p∨q"
"¬q"
shows "p"
proof -
note `p ∨ q`
moreover have "p ⟹ p" .
moreover {
assume "q"
with `¬q` have "p" by (rule notE)
}
ultimately show "p" by (rule disjE)
qed

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

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv hugrubsan *)
lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1) proof (rule disjE)
assume 1: "p" show "q" using assms(2) 1 by (rule notE)
next
assume "q" thus "q" .
qed

(* benber *)
lemma ejercicio_43_1:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
note `p ∨ q`
moreover {
assume "p"
with `¬p` have "q" by (rule notE)
}
moreover have "q ⟹ q" .
ultimately show "q" by (rule disjE)
qed

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

(* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue hugrubsan *)
lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule notI)
assume 1: "¬p ∧ ¬q" hence 2: "¬p" by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
show "False"
using assms(1) proof (rule disjE)
assume 4: "p" show ?thesis using 2 4 by (rule notE)
next
assume 5: "q" show ?thesis using 3 5 by (rule notE)
qed
qed

(* benber alfmarcua *)
lemma ejercicio_44_1:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof
assume "¬p ∧ ¬q"

note `p ∨ q`
moreover {
from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
moreover assume "p"
ultimately have "False" by (rule notE)
}
moreover {
from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
moreover assume "q"
ultimately have "False" by (rule notE)
}
ultimately show "False" by (rule disjE)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue hugrubsan *)
lemma ejercicio_45:
assumes 1: "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume 2: "¬p ∨ ¬q" have 3: "p" using 1 by (rule conjunct1)
have 4: "q" using 1 by (rule conjunct2)
show "False" using 2
proof (rule disjE)
assume "¬p" thus ?thesis using 3 by (rule notE)
next
assume "¬q" thus ?thesis using 4 by (rule notE)
qed
qed

(* benber alfmarcua *)
lemma ejercicio_45_1:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
moreover {
assume "¬p"
moreover have "p" using `p ∧ q` by (rule conjunct1)
ultimately have "False" by (rule notE)
}
moreover {
assume "¬q"
moreover have "q" using `p ∧ q` by (rule conjunct2)
ultimately have "False" by (rule notE)
}
ultimately show False by (rule disjE)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue hugrubsan *)
lemma ejercicio_46:
assumes 1: "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
assume p hence 2: "p ∨ q" by (rule disjI1)
show False using 1 2 by (rule notE)
qed
show "¬q"
proof (rule notI)
assume q hence 3: "p ∨ q" by (rule disjI2)
show False using 1 3 by (rule notE)
qed
qed

(* benber *)
lemma ejercicio_46_1:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof (rule ccontr)
assume "¬¬p"
hence "p" by (rule notnotD)
hence "p ∨ q" by (rule disjI1)
with assms show "False" by (rule notE)
qed
next
show "¬q"
proof (rule ccontr)
assume "¬¬q"
hence "q" by (rule notnotD)
hence "p ∨ q" by (rule disjI2)
with assms show "False" by (rule notE)
qed
qed

(* alfmarcua *)
lemma ejercicio_46_2:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
have "p ⟹ p ∨ q" by (rule disjI1)
then have "p ⟶ p ∨ q" by (rule impI)
then show "¬ p" using assms by (rule mt)
next
have "q ⟹ p ∨ q" by (rule disjI2)
then have "q ⟶ p ∨ q" by (rule impI)
then show "¬ q" using assms by (rule mt)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 pabbregue hugrubsan *)
lemma ejercicio_47:
assumes 1: "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
have 2: "¬p" using 1 by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
assume 4: "p ∨ q"
show False
using 4 proof (rule disjE)
assume 5: p show ?thesis using 2 5 by (rule notE)
next
assume 6: q show ?thesis using 3 6 by (rule notE)
qed
qed

(* benber gleherlop *)
lemma ejercicio_47_1:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
thus "False" using assms by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_47_2:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
have "¬ p" using assms by (rule conjunct1)
have "¬ q" using assms by (rule conjunct2)
assume "p ∨ q"
then have "q" using `¬ p` by (rule ejercicio_43)
show False using `¬ q` `q` by (rule notE)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 pabbergue hugrubsan *)
lemma ejercicio_48:
assumes 1: "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule notI)
assume 2: "p ∧ q" hence 3: p by (rule conjunct1)
have 4: q using 2 by (rule conjunct2)
show False
using 1 proof (rule disjE)
assume "¬p" thus ?thesis using 3 by (rule notE)
next
assume "¬q" thus ?thesis using 4 by (rule notE)
qed
qed

(* benber alfmarcua gleherlop *)
lemma ejercicio_48_1:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
thus "False" using assms by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop hugrubsan *)
lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof (rule notI)
assume 1: "p ∧ ¬p" hence 2: p by (rule conjunct1)
have "¬p" using 1 by (rule conjunct2)
thus "False" using 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_49_1:
"¬(p ∧ ¬p)"
proof
assume "p ∧ ¬p"
hence "¬p" by (rule conjunct2)
moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
ultimately show "False" by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop alfmarcua enrparalv pabbergue hugrubsan *)
lemma ejercicio_50:
assumes 1: "p ∧ ¬p"
shows "q"
proof (rule notE)
show p using 1 by (rule conjunct1)
show "¬p" using 1 by (rule conjunct2)
qed

(* benber *)
lemma ejercicio_50_1:
assumes "p ∧ ¬p"
shows "q"
proof -
have "¬p" using `p ∧ ¬p` by (rule conjunct2)
moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
ultimately show "q" by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

(* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop alfmarcua enrparalv pabbergue hugrubsan *)
lemma ejercicio_51:
assumes "¬¬p"
shows "p"
using assms(1) by (rule notnotD)

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 pabbergue*)
lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
assume 1: "¬(p ∨ ¬p)"
have 2: "¬p" proof (rule notI)
assume p hence 3: "p ∨ ¬p" by (rule disjI1)
show "False" using 1 3 by (rule notE)
qed
have 4: "p ∨ ¬p" using 2 by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed

(* benber *)
lemma ejercicio_52_1:
"p ∨ ¬p"
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
hence "¬p" by (rule conjunct1)
moreover {
have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
hence "p" by (rule notnotD)
}
ultimately show "False" by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_52_2:
"p ∨ ¬p"
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
then have "¬ p ∧ ¬¬ p" by (rule ejercicio_46)
then show False by (rule ejercicio_50)
qed

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue *)
lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume 1: "(p ⟶ q) ⟶ p"
show p proof (rule ccontr)
assume 2: "¬p"
have 3: "¬(p ⟶ q)" using 1 2 by (rule mt)
have 4: "p ⟶ q" proof (rule impI)
assume 5: p show q using 2 5 by (rule notE)
qed
show False using 3 4 by (rule notE)
qed
qed

(* benber *)
lemma ejercicio_53_1:
"((p ⟶ q) ⟶ p) ⟶ p"
proof
assume "(p ⟶ q) ⟶ p"
have "p ∨ ¬p" by (rule ejercicio_52_1)
moreover have "p ⟹ p" .
moreover {
assume "¬ p"
hence "p ⟶ q" by (rule ejercicio_40_1)
with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
}
ultimately show "p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue *)
lemma ejercicio_54:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt)
thus "q" by (rule notnotD)
qed

(* benber alfmarcua *)
lemma ejercicio_54_1:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus "q" by (rule notnotD)
qed

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

(* pabalagon marfruman1*)
lemma ejercicio_55:
assumes 1: "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume 2: "¬(p ∨ q)"
have 3: "p"
proof (rule ccontr)
assume 4: "¬p"
have 5: "q"
proof (rule ccontr)
assume 6: "¬q" have 7: "¬p ∧ ¬q" using 4 6 by (rule conjI)
show False using 1 7 by (rule notE)
qed
have 8: "p ∨ q" using 5 by (rule disjI2)
show False using 2 8 by (rule notE)
qed
have 9: "p ∨ q" using 3 by (rule disjI1)
show False using 2 9 by (rule notE)
qed

(* benber alfmarcua josgomrom4 manperjim pabbergue *)
lemma ejercicio_55_1:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
with assms show False by (rule notE)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue *)
lemma ejercicio_56:
assumes 1: "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
show 3: p
proof (rule ccontr)
assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
show False using 1 4 by (rule notE)
qed
show 5: q
proof (rule ccontr)
assume "¬q" hence 6: "¬p ∨ ¬q" by (rule disjI2)
show False using 1 6 by (rule notE)
qed
qed

(* benber alfmarcua *)
lemma ejercicio_56_1:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof -
have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
hence "¬¬p" by (rule conjunct1)
hence "p" by (rule notnotD)
moreover {
have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
hence "q" by (rule notnotD)
}
ultimately show "p ∧ q" by (rule conjI)
qed

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

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue *)
lemma ejercicio_57:
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume 2: "¬(¬p ∨ ¬q)"
show False using 1
proof (rule notE)
show 3: "p ∧ q"
proof (rule conjI)
show p
proof (rule ccontr)
assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
show False using 2 4 by (rule notE)
qed
next
show q
proof (rule ccontr)
assume "¬q" hence 5: "¬p ∨ ¬q" by (rule disjI2)
show False using 2 5 by (rule notE)
qed
qed
qed
qed

(* benber alfmarcua *)
lemma ejercicio_57_1:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
hence "p ∧ q" by (rule ejercicio_56_1)
with assms show "False" by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 marfruman1 pabbergue *)
lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "(p ⟶ q) ∨ ¬(p ⟶ q)" proof (rule ccontr)
assume 1: "¬((p ⟶ q) ∨ ¬(p ⟶ q))"
have 2: "¬(p ⟶ q)" proof (rule notI)
assume "p ⟶ q"
hence 3: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
hence 4: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed
thus ?thesis proof (rule disjE)
assume "p ⟶ q" thus ?thesis by (rule disjI1)
next
assume 1: "¬(p ⟶ q)"
have "q ⟶ p" proof (rule impI)
assume 2: q
have 3: "p ⟶ q" proof (rule impI)
assume p show q using 2 .
qed
show p using 1 3 by (rule notE)
qed
thus ?thesis by (rule disjI2)
qed
qed

(* pabalagon gleherlop *)
lemma ejercicio_58_2:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume 1: "¬((p ⟶ q) ∨ (q ⟶ p))"
hence 1: "(p ∧ ¬q) ∧ (q ∧ ¬p)" by simp
hence "p ∧ ¬q" ..
hence 2: p ..
have "q ∧ ¬p" using 1 ..
hence 3: "¬p" ..
show False using 3 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_58_1:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)

have "p ∨ ¬p" by (rule ejercicio_52_1)
moreover {
assume "p"
hence "q ⟶ p" by (rule ejercicio_7_1)

have "¬(q ⟶ p)" using 1 by (rule conjunct2)
hence "False" using `q ⟶ p` by (rule notE)
}
moreover {
assume "¬p"
hence "p ⟶ q" by (rule ejercicio_40_1)

have "¬(p ⟶ q)" using 1 by (rule conjunct1)
hence "False" using `p ⟶ q` by (rule notE)
}
ultimately show "False" by (rule disjE)
moreover {
assume "p"
hence "q ⟶ p" by (rule ejercicio_7_1)

have "¬(q ⟶ p)" using 1 by (rule conjunct2)
hence "False" using `q ⟶ p` by (rule notE)
}
qed

(* alfmarcua *)
lemma ejercicio_58_3:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
show "p ∨ ¬ p" by (rule ejercicio_52)
next
assume "¬p"
then have "p ⟶ q" by (rule ejercicio_40)
then show ?thesis by (rule disjI1)
next
assume "p"
then have "q ⟶ p" by (rule ejercicio_7)
then show ?thesis by (rule disjI2)
qed

end
</source>

Relación 6

2019-01-16T19:27:53Z

Josgomrom4:

Relación 6

2019-01-15T11:08:38Z

Josgomrom4:

Relación 5

2018-12-20T10:02:56Z

Josgomrom4:

<source lang="isabelle">
chapter {* R5: Recorridos de árboles *}

theory R5_Recorridos_de_arboles
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información en los nodos y en las hojas.
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
a d f h
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
---------------------------------------------------------------------
*}

datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"

value "N e (N c (H a) (H d)) (N g (H f) (H h))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
preOrden :: "'a arbol ⇒ 'a list"
tal que (preOrden a) es el recorrido pre orden del árbol a. Por
ejemplo,
preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 aribatval benber josgomrom4 *)
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden (H x) = [x]" |
"preOrden (N x i d) = x # preOrden i @ preOrden d"

value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]"

text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
postOrden :: "'a arbol ⇒ 'a list"
tal que (postOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 aribatval benber josgomrom4 *)
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden (H x) = [x]" |
"postOrden (N x i d) = postOrden i @ postOrden d @ [x]"

value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
inOrden :: "'a arbol ⇒ 'a list"
tal que (inOrden a) es el recorrido in orden del árbol a. Por
ejemplo,
inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 aribatval benber josgomrom4 *)
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H x) = [x]" |
"inOrden (N x i d) = inOrden i @ [x] @ inOrden d"

value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]"

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
espejo :: "'a arbol ⇒ 'a arbol"
tal que (espejo a) es la imagen especular del árbol a. Por ejemplo,
espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 aribatval benber josgomrom4 *)
fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H x) = H x" |
"espejo (N x i d) = N x (espejo d) (espejo i)"

value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que
preOrden (espejo a) = rev (postOrden a)
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 josgomrom4 *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
assume H2: "?P d"
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "... = x # preOrden (espejo d) @ preOrden (espejo i)" by simp
also have "... = x # rev (postOrden d) @ rev (postOrden i)"
using H1 H2 by simp
also have "... = rev (postOrden d @ [x]) @ rev (postOrden i)" by simp
also have "... = rev (postOrden i @ postOrden d @ [x])" by simp
finally show "?P (N x i d)" by simp
qed

(* benber *)
lemma "preOrden (espejo a) = rev (postOrden a)"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)

have "preOrden (espejo (N v l r)) = preOrden (N v (espejo r) (espejo l))" by simp
also have "... = v # (preOrden (espejo r)) @ (preOrden (espejo l))" by simp
also have "... = v # rev (postOrden r) @ rev (postOrden l)" using IS.IH by simp
also have "... = rev ((postOrden l) @ (postOrden r) @ [v])" by simp
also have "... = rev (postOrden (N v l r))" by simp
finally show ?case .
qed

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i" and H2: "?P d"
have "postOrden (espejo (N x i d)) =
postOrden (N x (espejo d) (espejo i))" by simp
also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x]"
by simp
also have "... = rev (preOrden d) @ rev (preOrden i) @ [x]"
using H1 H2 by simp
also have "... = rev (preOrden i @ preOrden d) @ rev [x]" by simp
also have "... = rev (x # preOrden i @ preOrden d)" by simp
finally show "?P (N x i d)" by simp
qed

(* raffergon2 *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
assume H2: "?P d"
have "postOrden (espejo (N x i d)) = postOrden (N x (espejo d) (espejo i))" by simp
also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x]"
by simp
also have "... = rev(preOrden d) @ rev (preOrden i) @ [x]"
using H1 H2 by simp
also have "... = rev(preOrden d) @ rev (x # preOrden i)" by simp
also have "... = rev(x # preOrden i @ preOrden d)" by simp
finally show "?P (N x i d)" by simp
qed

(* benber *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induction a) auto

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i" and H2: "?P d"
have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))"
by simp
also have "... = inOrden (espejo d) @ [x] @ inOrden (espejo i)" by simp
also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)"
using H1 H2 by simp
also have "... = rev (inOrden i @ [x] @ inOrden d)" by simp
finally show "?P (N x i d)" by simp
qed

(* raffergon2 *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
assume H2: "?P d"

have "inOrden (espejo (N x i d)) = inOrden(N x (espejo d) (espejo i))" by simp
also have "... = inOrden (espejo d) @ [x] @ inOrden (espejo i)" by simp
also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)"
using H1 H2 by simp
also have "... = rev(x # inOrden d) @ rev (inOrden i)" by simp
also have "... = rev(inOrden i @ x # inOrden d)" by simp
finally show "?P (N x i d)" by simp
qed

(* benber *)
theorem "inOrden (espejo a) = rev (inOrden a)"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)

have "inOrden (espejo (N v l r)) = inOrden (N v (espejo r) (espejo l))" by simp
also have "... = (inOrden (espejo r)) @ [v] @ (inOrden (espejo l))" by simp
also have "... = (rev (inOrden r)) @ [v] @ (rev (inOrden l))" using IS.IH by simp
also have "... = rev ((inOrden l) @ [v] @ (inOrden r))" by simp
also have"... = rev (inOrden (N v l r))" by simp
finally show ?case .
qed

text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
raiz :: "'a arbol ⇒ 'a"
tal que (raiz a) es la raiz del árbol a. Por ejemplo,
raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 aribatval benber josgomrom4 *)
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x" |
"raiz (N x i d) = x"

value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e"

text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
extremo_izquierda :: "'a arbol ⇒ 'a"
tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
a. Por ejemplo,
extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 benber josgomrom4 *)
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x" |
"extremo_izquierda (N x i d) = extremo_izquierda i"

value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a"

text {*
---------------------------------------------------------------------
Ejercicio 11. Definir la función
extremo_derecha :: "'a arbol ⇒ 'a"
tal que (extremo_derecha a) es el nodo más a la derecha del árbol
a. Por ejemplo,
extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
---------------------------------------------------------------------
*}

(* pabalagon raffergon2 benber josgomrom4 *)
fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x" |
"extremo_derecha (N x i d) = extremo_derecha d"

value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h"

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
last (inOrden a) = extremo_derecha a
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma inOrdenNotNil: "inOrden a ≠ []" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
have "?P (N x i d) = ((inOrden i @ [x] @ inOrden d) ≠ [])" by simp
also have "... = ((inOrden i ≠ []) ∨ ([x] ≠ []) ∨ (inOrden d ≠ []))" by simp
also have "... = ([x] ≠ [])" by simp
finally show "?P (N x i d)" by simp
qed

theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI: "?P d"
have "last (inOrden (N x i d)) = last (inOrden i @ [x] @ inOrden d)" by simp
also have "... = last (x # inOrden d)" by simp
also have "... = last (inOrden d)" by (simp add: inOrdenNotNil)
also have "... = extremo_derecha d" using HI by simp
also have "... = extremo_derecha (N x i d)" by simp
finally show "?P (N x i d)" .
qed

(* benber *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)

have 1: "last (xs@ys) = last ys" if "ys ≠ []" for xs ys :: "'a list"
proof (induction xs)
case Nil
show ?case by simp
next
case IS: (Cons x xs)
have "last ((x#xs)@ys) = last (x#(xs@ys))" by simp
also have "... = last (xs @ ys)" using `ys ≠ []` by simp
also have "... = last ys" using IS.IH by simp
finally show ?case .
qed

have 2: "inOrden a ≠ []" for a :: "'a arbol"
by (induction a) auto

have "last (inOrden (N v l r)) = last ( (inOrden l) @ [v] @ (inOrden r) )" by simp
also have "... = last (inOrden r)" using 1 2 by auto
also have "... = extremo_derecha r" using IS.IH by simp
also have "... = extremo_derecha (N v l r)" by simp
finally show ?case .
qed

text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x::'a
have "hd (inOrden (H x)) = hd [x]" by simp
also have "... = x" by simp
also have "... = extremo_izquierda (H x)" by simp
finally show "?P (H x)" .
next
fix x i d
assume HI: "?P i"
have "hd (inOrden (N x i d)) = hd (inOrden i @ [x] @ inOrden d)" by simp
also have "... = hd ((inOrden i @ [x]) @ inOrden d)" by simp
also have "... = hd (inOrden i)" by (simp add: inOrdenNotNil)
also have "... = extremo_izquierda i" using HI by simp
also have "... = extremo_izquierda (N x i d)" by simp
finally show "?P (N x i d)" .
qed

(* benber *)
theorem "hd (inOrden a) = extremo_izquierda a"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)
moreover have "inOrden a ≠ []" for a :: "'a arbol"
by (induction a) auto
ultimately show ?case by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
theorem hdPreOrden_lastPostOrden:
"hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x::'a
fix i d
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
also have "... = last [x]" by simp
also have "... = last (postOrden i @ postOrden d @ [x])" by simp
finally show "?P (N x i d)" by simp
qed

(* benber *)
theorem "hd (preOrden a) = last (postOrden a)"
by (cases a) auto

text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
theorem hdPreOrden_raiz: "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x::'a
fix i d
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
finally show "?P (N x i d)" by (simp only: raiz.simps(2))
qed

(* benber *)
theorem "hd (preOrden a) = raiz a"
by (cases a) auto

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}

(* pabalagon *)
theorem "hd (inOrden a) = raiz a"
quickcheck
(*
Quickcheck found a counterexample:
a = N a⇩1 (H a⇩2) (H a⇩1)
Evaluated terms:
hd (inOrden a) = a⇩2
raiz a = a⇩1 *)
oops

(* benber josgomrom4 *)
(* El teorema no es cierto para arboles sobre numeros naturales *)
theorem "¬(∀ a :: nat arbol. hd (inOrden a) = raiz a)"
proof -
let ?a = "(N 0 (H 1) (H 2)) :: nat arbol"
have "hd (inOrden ?a) = 1" by simp
moreover have "raiz ?a = 0" by simp
ultimately have "hd (inOrden ?a) ≠ raiz ?a" by simp
hence "∃ a :: nat arbol. hd (inOrden a) ≠ raiz a" by (simp only: exI)
thus ?thesis by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
theorem "last (postOrden a) = raiz a"
proof -
have "last (postOrden a) = hd (preOrden a)"
by (simp add: hdPreOrden_lastPostOrden)
also have "... = raiz a" by (simp add: hdPreOrden_raiz)
finally show "?thesis" .
qed

(* benber *)
theorem "last (postOrden a) = raiz a"
by (cases a) auto

end
</source>

Relación 4

2018-12-09T10:53:35Z

Josgomrom4:

<source lang="isabelle">
chapter {* R4: Cuantificadores sobre listas *}

theory R4_Cuantificadores_sobre_listas
imports Main
begin

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

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

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

(* pabalagon alfmarcua josgomrom4 *)
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False" |
"algunos p (x#xs) = (p x ∨ algunos p xs)"

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

(* pabalagon alfmarcua josgomrom4 *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

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

(* pabalagon *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P P Q xs")
proof (induct xs)
fix P Q
show "?P P Q []" by simp
next
fix a xs
assume HI: "?P P Q xs"
have "todos (λx. P x ∧ Q x) (a#xs) = ((P a ∧ Q a) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" using HI by simp
also have "... = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" by (simp add: HOL.conj_comms)
also have "... = (todos P (a#xs) ∧ (Q a ∧ todos Q xs))" by simp
finally show "todos (λx. P x ∧ Q x) (a#xs) = (todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

(* alfmarcua *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P xs")
proof (induct xs)
have "todos (λx. P x ∧ Q x) [] = (True)" by (simp only: todos.simps(1))
also have "... = (True ∧ True)" by (simp only: conj_absorb)
also have "... = (todos P [] ∧ todos Q [])" by (simp only: todos.simps(1))
finally show "?P []" .
next
fix x xs
assume HI: "?P xs"
have "todos (λx. P x ∧ Q x) (x # xs) = ((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs)"
by (simp only: todos.simps(2))
also have "... = ((P x ∧ Q x) ∧ (todos P xs ∧ todos Q xs))" by (simp only: HI)
also have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" by (simp only: HOL.conj_comms)
also have "... = (todos P (x # xs) ∧ todos Q (x # xs))" by (simp only: todos.simps(2))
finally show "?P (x#xs)" .
qed

(* josgomrom4 *)
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 n xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (n # xs) =
((P n ∧ Q n) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
also have "... = ((P n ∧ todos P xs) ∧ (Q n ∧ todos Q xs))" by arith
also have "... = ((todos P(n#xs)) ∧ (todos Q(n#xs)))" by simp
finally show "todos (λx. P x ∧ Q x) (n#xs) =
(todos P (n#xs) ∧ todos Q (n#xs))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

(* pabalagon alfmarcua josgomrom4 *)
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

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

(* pabalagon josgomrom4 *)
lemma todos_append:
"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
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
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 HI by simp
finally show "todos P ((a#x) @ y) = (todos P (a#x) ∧ todos P y)" by simp
qed

(* alfmarcua *)
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)" (is "?P x")
proof (induct x)
have "todos P ([] @ y) = todos P y" by (simp only: append_Nil)
also have "... = (True ∧ todos P y)" by (simp only: simp_thms(22))
also have "... = (todos P [] ∧ todos P y)" by (simp only: todos.simps(1))
finally show "?P []" .
next
fix a x
assume HI:"?P x"
have "todos P ((a # x) @ y) = todos P (a # (x @ y))"
by (simp only:List.append.append_Cons)
also have "... = (P a ∧ todos P (x @ y))" by (simp only: todos.simps(2))
also have "... = (P a ∧ todos P x ∧ todos P y)" by (simp only:HI)
also have "... = ((P a ∧ todos P x) ∧ todos P y)" by (simp only:HOL.conj_assoc)
also have "... = (todos P (a#x) ∧ todos P y)" by (simp only: todos.simps(2))
finally show "?P (a#x)" .
qed

text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (simp_all add: HOL.conj_comms todos_append)

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

(* pabalagon josgomrom4 *)
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (a#xs)) = todos P ((rev xs) @ [a])" by simp
also have "... = (todos P (rev xs) ∧ todos P [a])" by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
also have "... = (todos P xs ∧ P a)" by simp
also have "... = (P a ∧ todos P xs)" by (simp add: HOL.conj_comms)
finally show "todos P (rev (a#xs)) = todos P (a#xs)" by simp
qed

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

(* pabalagon *)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
nitpick
oops

(* Contraejemplo *)
value "algunos (λx. even x ∧ odd x) [1, 2::nat] ≠
algunos even [1, 2::nat] ∧ algunos odd [1, 2::nat]"

text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

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

(* pabalagon *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show "algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a#xs)) = (P (f a) ∨ algunos P (map f xs))" by simp
also have "... = (P (f a) ∨ algunos (P ∘ f) xs)" using HI by simp
also have "... = ((P ∘ f) a ∨ algunos (P ∘ f) xs)" by simp
finally show "algunos P (map f (a#xs)) = algunos (P ∘ f) (a#xs)" by simp
qed

(* josgomrom4 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show "algunos P (map f []) = algunos (P o f) []" by simp
next
fix x xs
assume HI: "algunos P (map f xs) = algunos (P o f) xs"
have "algunos P (map f (x#xs)) = (P (f x) ∨ algunos P (map f xs))"
by simp
also have "... = (P (f x) ∨ algunos (P o f) xs)" using HI by simp
finally show "algunos P (map f (x#xs)) = algunos (P o f) (x#xs)"
by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto

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

(* pabalagon josgomrom4 *)
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 HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
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 HI by simp
finally show "algunos P ((a#xs) @ ys) = (algunos P (a#xs) ∨ algunos P ys)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (simp_all add: HOL.disj_comms algunos_append)

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

(* pabalagon *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI: "algunos P (rev xs) = algunos P xs"
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 HI by simp
also have "... = (algunos P xs ∨ P a)" by simp
also have "... = (P a ∨ algunos P xs)" by (simp add: HOL.disj_comms)
finally show "algunos P (rev (a#xs)) = algunos P (a#xs)" by simp
qed

(* josgomrom4 *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI:"algunos P (rev xs) = algunos P xs"
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 HI by simp
also have "... = ((algunos P [a]) ∨ (algunos P xs))" by arith
finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto

(* pabalagon josgomrom4 *)
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 HI: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
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 HI by simp
also have "... = (P a ∨ algunos P xs ∨ Q a ∨ algunos Q xs)" by (simp add: HOL.disj_comms)
finally show "algunos (λx. P x ∨ Q x) (a#xs) = (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto

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

(* pabalagon josgomrom4 *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
have "algunos P [] = False" by simp
also have "... = (¬ todos (λx. (¬ P x)) [])" by simp
finally show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
fix a xs
assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
have "(¬ todos (λx. (¬ P x)) (a#xs)) = (¬ ((¬ P a) ∧ todos (λx. (¬ P x)) xs))" by simp
also have "... = (P a ∨ ¬ todos (λx. (¬ P x)) xs)" by simp
also have "... = (P a ∨ algunos P xs)" using HI by simp
finally show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))" by simp
qed

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

(* pabalagon josgomrom4 *)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False" |
"estaEn x (y#xs) = (x=y ∨ estaEn x xs)"

text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}

(* pabalagon josgomrom4 *)
lemma "estaEn x xs = algunos (λa. x=a) xs"
by (induct xs) auto

(* pabalagon josgomrom4 *)
lemma "estaEn x xs = algunos (λa. x=a) xs"
proof (induct xs)
show "estaEn x [] = algunos (λa. x=a) []" by simp
next
fix y xs
assume HI: "estaEn x xs = algunos (λa. x=a) xs"
have "estaEn x (y#xs) = (x=y ∨ estaEn x xs)" by simp
also have "... = (x=y ∨ algunos (λa. x=a) xs)" using HI by simp
finally show "estaEn x (y#xs) = algunos (λa. x=a) (y#xs)" by simp
qed

end
</source>

Relación 3

2018-11-28T18:34:01Z

Josgomrom4:

<source lang="isabelle">
chapter {* R3: Razonamiento sobre programas *}

theory R3_Razonamiento_sobre_programas
imports Main
begin

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

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

text {* ---------------------------------------------------------------
Ejercicio 1.2. Escribir la demostración detallada de
sumaImpares n = n*n
------------------------------------------------------------------- *}

(* "La demostración detallada es" *)

(* benber *)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0*0" by (simp only: sumaImpares.simps(1))
next
fix n
assume HI: "sumaImpares n = n*n"
have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" by (simp only: sumaImpares.simps(2))
also have "... = n*n + (2*n+1)" by (simp only: HI)
also have "... = n*n + (n+n+1)" by (simp only:)
also have "... = n*n + n + n + 1" by (simp only:)
also have "... = n*n + n*1 + n + 1" by (simp only:)
also have "... = n*(n+1) + n + 1" by (simp only: Nat.add_mult_distrib2)
also have "... = n*(n+1) + (n+1)" by (simp only:)
also have "... = (n+1)*n + (n+1)" by (simp only: Groups.ab_semigroup_mult_class.mult.commute)
also have "... = (n+1)*n + (n+1)*1" by (simp only: Nat.nat_mult_1_right)
also have "... = (n+1)*(n+1)" by (simp only: Nat.add_mult_distrib2)
also have "... = (Suc n) * (Suc n)" by (simp only: Nat.Suc_eq_plus1)
finally show "sumaImpares (Suc n) = (Suc n) * (Suc n)" .
qed

(* pabalagon josgomrom4 *)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0*0" by (simp only: sumaImpares.simps(1))
next
fix n
assume HI: "sumaImpares n = n*n"
have "sumaImpares (Suc n) = sumaImpares n + 2 * n + 1" by (simp only: sumaImpares.simps(2))
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = n*n + n + n + 1" by (simp only: Nat.add_mult_distrib)
also have "... = (n+1)*n + (n + 1)" by (simp only: Nat.add_mult_distrib)
also have "... = (n+1)*n + (n + 1)*1" by (simp only: Nat.nat_mult_1_right)
also have "... = (n+1)*(n+1)" by (simp only: Nat.add_mult_distrib2)
finally show "sumaImpares (Suc n) = (Suc n)*(Suc n)"
by (simp only: Nat.Suc_eq_plus1)
qed

(*marfruman1 raffergon2 aribatval*)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0*0" by (simp only: sumaImpares.simps(1))
next
fix n
assume HI: "sumaImpares n = n*n"
have "sumaImpares (Suc n) = sumaImpares n + 2*n +1" by (simp only: sumaImpares.simps(2))
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = (Suc n)*(Suc n)" by simp
finally show "sumaImpares (Suc n) = (Suc n)*(Suc n)" by simp
qed

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

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

text {* ---------------------------------------------------------------
Ejercicio 2.2. Escribir la demostración detallada de
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

(* benber josgomrom4 *)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
have "sumaPotenciasDeDosMasUno 0 = 2" by (simp only: sumaPotenciasDeDosMasUno.simps(1))
also have "... = 2^(0+1)" by simp
finally show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" .
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)"
by (simp only: sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2^(n+1) + 2^(n+1)" by (simp only: HI)
also have "... = 2 * 2^(n+1)" by (simp only:)
also have "... = 2 * 2^(Suc n)" by (simp only: Nat.Suc_eq_plus1)
also have "... = 2^(Suc (Suc n))" by (simp only: Power.power_class.power.power_Suc)
also have "... = 2^((Suc n)+1)" by (simp only: Nat.Suc_eq_plus1)
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^((Suc n)+1)" .
qed

(*marfruman1*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
have "sumaPotenciasDeDosMasUno 0 = 2" by (simp only: sumaPotenciasDeDosMasUno.simps(1))
also have "... = 2^(0+1)" by simp
finally show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) =
sumaPotenciasDeDosMasUno n + 2^(n+1)"
by (simp only: sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2^(n+1)+2^(n+1)" using HI by simp
also have "... =2*2^(n+1)" by simp
also have "... = 2^((Suc n)+1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^((Suc n)+1)"
by simp
qed

(* pabalagon raffergon2 aribatval*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
have "sumaPotenciasDeDosMasUno 0 = 2"
by (simp only: sumaPotenciasDeDosMasUno.simps(1))
also have "... = 2^1" by (simp only: Power.power_one_right)
finally show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by (simp only: Nat.add_0)
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)"
by (simp only: sumaPotenciasDeDosMasUno.simps(2))
also have "... = 2^(n+1) + 2^(n+1)" by (simp only: HI)
also have "... = 2*2^(n+1)" by (simp only: Nat.add_mult_distrib)
also have "... = 2*2^(Suc n)" by (simp only: Nat.Suc_eq_plus1)
also have "... = 2^(Suc n)*2^1" by (simp only: Power.power_one_right)
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)" by (simp only: Power.power_add)
qed

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

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

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

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

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

(* benber raffergon2 aribatval josgomrom4 *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
fix x :: 'a
have "todos (λy. y=x) (copia 0 x) = todos (λy. y=x) []" by (simp only: copia.simps(1))
also have "..." by (simp only: todos.simps(1))
finally show "todos (λy. y = x) (copia 0 x)" .
next
fix x :: 'a
fix n :: nat
assume HI: "todos (λy. y = x) (copia n x)"
have "( todos (λy. y = x) (copia (Suc n) x) ) = (todos (λy. y = x) (x # copia n x))"
by (simp only: copia.simps(2))
also have "... = ( ( (λy. y = x) x ) ∧ todos (λy. y = x) (copia n x) )"
by (simp only: todos.simps(2))
also have "..." by (simp only: HI)
finally show "todos (λy. y = x) (copia (Suc n) x)" .
qed

(* pabalagon *)
lemma "todos (λy. y=x) (copia n x)"
proof (induction n)
fix x:: 'a
have "todos (λy. y=x) (copia 0 x) = todos (λy. y=x) []" by simp
also have "..." by simp
finally show "todos (λy. y=x) (copia 0 x)" .
next
fix x:: 'a
fix n:: nat
assume HI: "todos (λy. y=x) (copia n x)"
have "todos (λy. y=x) (copia (Suc n) x) = todos (λy. y=x) (x#(copia n x))" by simp
also have "... = ((λy. y=x) x ∧ todos (λy. y=x) (copia n x))" by simp
finally show "todos (λy. y=x) (copia (Suc n) x)" using HI by simp
qed

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

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"

text {* ---------------------------------------------------------------
Ejercicio 4.2. 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
Indicación: La propiedad mult_Suc es
(Suc m) * n = n + m * n
Puede que se necesite desactivarla en un paso con
(simp del: mult_Suc)
------------------------------------------------------------------- *}

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

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

(* benber *)
lemma fact: "factI' n x = x * factR n"
proof -
(* Reformulación para aplicar la hipótesis inductiva con un valor distinto de x. *)
have "∀x. factI' n x = x * factR n"
proof (induct n)
show "∀x. factI' 0 x = x * factR 0"
proof
fix x
have "factI' 0 x = x" by (simp only: factI'.simps(1))
also have "... = x * 1" by (simp only:)
also have "... = x * factR 0" by (simp only: factR.simps(1))
finally show "factI' 0 x = x * factR 0" .
qed
next
show "⋀n. ∀x. factI' n x = x * factR n ⟹ ∀x. factI' (Suc n) x = x * factR (Suc n)"
proof
fix x
fix n
assume HI: "∀y. factI' n y = y * factR n"
have "factI' (Suc n) x = factI' n (x * Suc n)" by (simp only: factI'.simps(2))
also have "... = (x * Suc n) * factR n" by (simp only: HI)
also have "... = x * factR (Suc n)" by (simp only: factR.simps(2))
finally show "factI' (Suc n) x = x * factR (Suc n)" .
qed
qed
thus "factI' n x = x * factR n" by simp
qed

(* pabalagon raffergon2 aribatval josgomrom4*)
lemma fact: "factI' n x = x * factR n"
proof (induction n arbitrary: x)
fix x
have "factI' 0 x = x" by simp
also have "... = x * 1" by simp
finally show "factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "⋀x. factI' n x = x * factR n"
show "⋀x. factI' (Suc n) x = x * factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x * Suc n)" by (simp only: factI'.simps(2))
also have "... = x * Suc n * factR n" using HI by simp
finally show "factI' (Suc n) x = x*factR (Suc n)" by (simp only: factR.simps(2))
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 4.3. Escribir la demostración detallada de
factI n = factR n
------------------------------------------------------------------- *}

(* benber *)
corollary "factI n = factR n"
proof -
fix n
have "factI n = factI' n 1" by (simp only: factI.simps(1))
also have "... = 1 * factR n" by (simp only: fact)
also have "... = factR n" by (simp only: Groups.mult_1)
finally show "factI n = factR n" .
qed

(* pabalagon raffergon2 josgomrom4 *)
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1" by (simp only: factI.simps(1))
also have "... = 1*factR n" using fact by simp
finally show "factI n = factR n" by (simp only: mult_1)
qed

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

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

text {* ---------------------------------------------------------------
Ejercicio 5.2. Escribir la demostración detallada de
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

(* benber aribatval*)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
have "amplia [] y = [y]" by (simp only: amplia.simps(1))
also have "... = [] @ [y]" by (simp only: List.append.left_neutral)
finally show "amplia [] y = [] @ [y]" .
next
fix x
fix xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x#xs) y = x # amplia xs y" by (simp only: amplia.simps(2))
also have "... = x # (xs @ [y])" by (simp only: HI)
also have "... = (x#xs) @ [y]" by (simp only: List.append.append_Cons)
finally show "amplia (x#xs) y = (x#xs) @ [y]" .
qed

(*marfruman1 raffergon2*)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
have "amplia [] y = [y]" by (simp only: amplia.simps(1))
also have "... = [] @ [y]" by simp
finally show "amplia [] y = [] @ [y]" by simp
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x#xs) y = x# amplia xs y" by (simp only: amplia.simps(2))
also have "... = x# (xs @ [y])" using HI by simp
also have "... = (x#xs) @ [y]" by simp
finally show "amplia (x#xs) y =(x#xs) @ [y]" by simp
qed

(* pabalagon josgomrom4 *)
lemma "amplia xs y = xs @ [y]"
proof (induction xs)
have "amplia [] y = [y]" by (simp only: amplia.simps(1))
show "amplia [] y = [] @ [y]" by simp
next
fix a xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (a#xs) y = a # amplia xs y" by (simp only: amplia.simps(2))
also have "... = a # (xs @ [y])" using HI by simp
finally show "amplia (a#xs) y = (a#xs) @ [y]" by simp
qed

end
</source>

Relación 2

2018-11-21T12:35:32Z

Josgomrom4:

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

theory R2_Razonamiento_automatico_sobre_programas
imports Main
begin

declare [[names_short]]

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 *)
fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0" |
"sumaImpares n = 2*n-1 + sumaImpares (n-1)"

{* josgomrom4 *}
fun sumaImpares2 :: "nat ⇒ nat" where
"sumaImpares2 0 = 0" |
"sumaImpares2 (Suc n) = 2*n + 1 + sumaImpares2 n"

value "sumaImpares 1 = 1"
value "sumaImpares 3 = 9"
value "sumaImpares 5 = 25"

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

(* pabalagon cammonagu juacanrod josgomrom4 *)
lemma "sumaImpares n = n*n"
apply(induction n)
apply auto
done

(* pabalagon *)
lemma "sumaImpares n = n*n"
apply(induction n)
apply simp
apply simp
done

(* pabalagon *)
lemma "sumaImpares n = n*n"
by (induction n) simp_all

(* alfmarcua raffergon2 *)
lemma "sumaImpares n = n*n"
by (induction n) auto

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

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

{* juacanrod josgomrom4 *}
fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno2 0 = 2" |
"sumaPotenciasDeDosMasUno2 (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno2 n"

(* alfmarcua raffergon2 *)
fun sumaPotenciasDeDosMasUno3 :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno3 0 = 2" |
"sumaPotenciasDeDosMasUno3 n = 2^n + sumaPotenciasDeDosMasUno3 (n-1)"

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
apply(induction n)
apply auto
done

(* pabalagon *)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induction n) simp_all

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

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

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

(* alfmarcua raffergon2*)
fun copia3 :: "nat ⇒ 'a ⇒ 'a list" where
"copia3 0 x = []" |
"copia3 n x = x#(copia (n-1) x)"

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4 *)
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True" |
"todos p (x#xs) = (p x ∧ todos p xs)"

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4 *)
lemma "todos (λy. y=x) (copia n x)"
apply(induction n)
apply auto
done

(* pabalagon *)
lemma "todos (λy. y=x) (copia n x)"
by (induction n) simp_all

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4 *)
fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]" |
"amplia (x#xs) y = x # amplia xs y"

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

(* pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4 *)
lemma "amplia xs y = xs @ [y]"
apply(induction xs)
apply auto
done

(* pabalagon *)
lemma "amplia xs y = xs @ [y]"
by (induction xs) simp_all

end
</source>

Relación 1

2018-11-10T22:21:01Z

Josgomrom4:

<source lang="isabelle">
chapter {* R1: Programación funcional en Isabelle *}

theory R1_Programacion_funcional_en_Isabelle
imports Main
begin

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 [a,b,c] = 3
------------------------------------------------------------------- *}

(* cammonagu pabalagon raffergon2*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0 "
| "longitud (x#xs) = 1 + longitud xs "
2
value "longitud [a,b,c] = 3"

{* juacanrod *}
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = 0" |
"longitud2 (x#xs) = 1 + longitud2(xs)"

(* josgomrom4 *)
fun longitud3 :: "'a list ⇒ nat" where
"longitud3 [] = 0" |
"longitud3 x = 1 + longitud3 (tl x)"

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

(* pabalagon cammonagu raffergon2*)

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

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

{* juacanrod *}
fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia2 (x,y) = (y, x)"

(* josgomrom4 *)
fun intercambia3 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia3 xs =(snd xs, fst xs) "

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

(* pabalagon *)

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

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = aux xs []"

(* pabalagon raffergon2 cammonagu josgomrom4 *)

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

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

{* juacanrod *}
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []" |
"inversa3 (xs) = inversa3(tl xs) @ [ hd (xs)]"

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

(* pabalagon *)

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

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

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

{* juacanrod *}
fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
"repite3 0 a = []" |
"repite3 n a = [a] @ repite3 (n-1) a"

value "repite3 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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 josgomrom4 *)

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

(* cammonagu *)
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 ys [] = ys" |
"conc2 xs (y#ys) = xs @y # ys"

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

{* juacanrod *}
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys" |
"conc3 xs ys = [hd (xs)] @ conc3 (tl (xs)) ys"

value "conc3 [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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 *)

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

(* cammonagu josgomrom4 *)
fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge2 0 xs = []" |
"coge2 n [] = []" |
"coge2 n (x#xs) = x # coge2 (n-1) xs"

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

{* juacanrod *}
fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge3 0 xs = []" |
"coge3 n xs = [hd (xs)] @ coge3 (n-1) (tl (xs))"

value "coge3 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]
------------------------------------------------------------------ *}

(* pabalagon *)

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

(* raffergon2 cammonagu josgomrom4 *)

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

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

{* juacanrod *}
fun elimina3 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina3 0 xs = xs" |
"elimina3 n xs = elimina3 (n-1) (tl xs)"

value "elimina3 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 [a] = False
------------------------------------------------------------------ *}

(* pabalagon raffergon2 josgomrom4*)

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True" |
"esVacia xs = False"

(* cammonagu *)

fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 xs = (longitud xs =0)"

value "esVacia [a] = False"
value "esVacia2[a] = False"

{* juacanrod *}
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 xs = (length xs = 0)"

value "esVacia3 [a] = 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]
------------------------------------------------------------------ *}

(* pabalagon cammonagu josgomrom4 *)

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 "inversaAc [a,c,b,e] = [e,b,c,a]"

{* juacanrod *}
fun inversaAcAux2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux2 [] ys = ys" |
"inversaAcAux2 xs ys = inversaAcAux2 (tl xs) ([hd xs]) @ ys"

value "inversaAcAux2 [a,b,c] []"

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

value "inversaAc2 [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
------------------------------------------------------------------ *}

(* pabalagon raffergon2 josgomrom4*)

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

(* cammonagu *)

fun sum2:: "nat list ⇒ nat" where
"sum2 [] = 0" |
"sum2 [x] = x" |
"sum2 (x#xs) = x + sum xs"

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

{* juacanrod *}
fun sum3 :: "nat list ⇒ nat" where
"sum3 [] = 0" |
"sum3 xs = (hd xs) + sum3 (tl xs)"

value "sum3 [3,2,5,1]"

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

(* pabalagon raffergon2 cammonagu josgomrom4*)

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

{* juacanrod *}
fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map2 f [] = []" |
"map2 f (x#xs) = [(f x)] @ map2 f xs"

value "map2 (λn. Suc n) [2,3,4,5]"

end
</source>

Relación 1

2018-11-10T21:29:22Z

Josgomrom4:

<source lang="isabelle">
chapter {* R1: Programación funcional en Isabelle *}

theory R1_Programacion_funcional_en_Isabelle
imports Main
begin

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 [a,b,c] = 3
------------------------------------------------------------------- *}

(* cammonagu pabalagon raffergon2*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0 "
| "longitud (x#xs) = 1 + longitud xs "
2
value "longitud [a,b,c] = 3"

{* juacanrod *}
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = 0" |
"longitud2 (x#xs) = 1 + longitud2(xs)"

(* josgomrom4 *)
fun longitud3 :: "'a list ⇒ nat" where
"longitud3 [] = 0" |
"longitud3 x = 1 + longitud3 (tl x)"

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

(* pabalagon cammonagu raffergon2*)

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

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

{* juacanrod *}
fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia2 (x,y) = (y, x)"

(* josgomrom4 *)
fun intercambia3 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia3 xs =(snd xs, fst xs) "

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

(* pabalagon *)

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

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = aux xs []"

(* pabalagon raffergon2 cammonagu *)

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

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

{* juacanrod *}
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []" |
"inversa3 (xs) = inversa3(tl xs) @ [ hd (xs)]"

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

(* pabalagon *)

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

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

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

{* juacanrod *}
fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
"repite3 0 a = []" |
"repite3 n a = [a] @ repite3 (n-1) a"

value "repite3 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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 *)

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

(* cammonagu *)
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 ys [] = ys" |
"conc2 xs (y#ys) = xs @y # ys"

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

{* juacanrod *}
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys" |
"conc3 xs ys = [hd (xs)] @ conc3 (tl (xs)) ys"

value "conc3 [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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 *)

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

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

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

{* juacanrod *}
fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge3 0 xs = []" |
"coge3 n xs = [hd (xs)] @ coge3 (n-1) (tl (xs))"

value "coge3 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]
------------------------------------------------------------------ *}

(* pabalagon *)

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

(* raffergon2 cammonagu *)

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

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

{* juacanrod *}
fun elimina3 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina3 0 xs = xs" |
"elimina3 n xs = elimina3 (n-1) (tl xs)"

value "elimina3 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 [a] = False
------------------------------------------------------------------ *}

(* pabalagon raffergon2*)

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True" |
"esVacia xs = False"

(* cammonagu *)

fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 xs = (longitud xs =0)"

value "esVacia [a] = False"
value "esVacia2[a] = False"

{* juacanrod *}
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 xs = (length xs = 0)"

value "esVacia3 [a] = 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]
------------------------------------------------------------------ *}

(* pabalagon cammonagu*)

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 "inversaAc [a,c,b,e] = [e,b,c,a]"

{* juacanrod *}
fun inversaAcAux2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux2 [] ys = ys" |
"inversaAcAux2 xs ys = inversaAcAux2 (tl xs) ([hd xs]) @ ys"

value "inversaAcAux2 [a,b,c] []"

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

value "inversaAc2 [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
------------------------------------------------------------------ *}

(* pabalagon raffergon2*)

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

(* cammonagu *)

fun sum2:: "nat list ⇒ nat" where
"sum2 [] = 0" |
"sum2 [x] = x" |
"sum2 (x#xs) = x + sum xs"

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

{* juacanrod *}
fun sum3 :: "nat list ⇒ nat" where
"sum3 [] = 0" |
"sum3 xs = (hd xs) + sum3 (tl xs)"

value "sum3 [3,2,5,1]"

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

(* pabalagon raffergon2 cammonagu*)

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

{* juacanrod *}
fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map2 f [] = []" |
"map2 f (x#xs) = [(f x)] @ map2 f xs"

value "map2 (λn. Suc n) [2,3,4,5]"

end
</source>

Relación 1

2018-11-10T21:23:07Z

Josgomrom4:

<source lang="isabelle">
chapter {* R1: Programación funcional en Isabelle *}

theory R1_Programacion_funcional_en_Isabelle
imports Main
begin

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 [a,b,c] = 3
------------------------------------------------------------------- *}

(* cammonagu pabalagon raffergon2*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0 "
| "longitud (x#xs) = 1 + longitud xs "
2
value "longitud [a,b,c] = 3"

{* juacanrod *}
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = 0" |
"longitud2 (x#xs) = 1 + longitud2(xs)"

(* josgomrom4 *)
fun longitud3 :: "'a list ⇒ nat" where
"longitud3 [] = 0" |
"longitud3 x = 1 + longitud3 (tl x)"

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

(* pabalagon cammonagu raffergon2*)

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

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

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

(* pabalagon *)

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

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = aux xs []"

(* pabalagon raffergon2 cammonagu *)

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

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

{* juacanrod *}
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []" |
"inversa3 (xs) = inversa3(tl xs) @ [ hd (xs)]"

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

(* pabalagon *)

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

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

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

{* juacanrod *}
fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
"repite3 0 a = []" |
"repite3 n a = [a] @ repite3 (n-1) a"

value "repite3 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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 *)

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

(* cammonagu *)
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 ys [] = ys" |
"conc2 xs (y#ys) = xs @y # ys"

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

{* juacanrod *}
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys" |
"conc3 xs ys = [hd (xs)] @ conc3 (tl (xs)) ys"

value "conc3 [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]
------------------------------------------------------------------ *}

(* pabalagon raffergon2 *)

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

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

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

{* juacanrod *}
fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge3 0 xs = []" |
"coge3 n xs = [hd (xs)] @ coge3 (n-1) (tl (xs))"

value "coge3 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]
------------------------------------------------------------------ *}

(* pabalagon *)

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

(* raffergon2 cammonagu *)

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

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

{* juacanrod *}
fun elimina3 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina3 0 xs = xs" |
"elimina3 n xs = elimina3 (n-1) (tl xs)"

value "elimina3 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 [a] = False
------------------------------------------------------------------ *}

(* pabalagon raffergon2*)

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True" |
"esVacia xs = False"

(* cammonagu *)

fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 xs = (longitud xs =0)"

value "esVacia [a] = False"
value "esVacia2[a] = False"

{* juacanrod *}
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 xs = (length xs = 0)"

value "esVacia3 [a] = 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]
------------------------------------------------------------------ *}

(* pabalagon cammonagu*)

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 "inversaAc [a,c,b,e] = [e,b,c,a]"

{* juacanrod *}
fun inversaAcAux2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux2 [] ys = ys" |
"inversaAcAux2 xs ys = inversaAcAux2 (tl xs) ([hd xs]) @ ys"

value "inversaAcAux2 [a,b,c] []"

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

value "inversaAc2 [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
------------------------------------------------------------------ *}

(* pabalagon raffergon2*)

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

(* cammonagu *)

fun sum2:: "nat list ⇒ nat" where
"sum2 [] = 0" |
"sum2 [x] = x" |
"sum2 (x#xs) = x + sum xs"

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

{* juacanrod *}
fun sum3 :: "nat list ⇒ nat" where
"sum3 [] = 0" |
"sum3 xs = (hd xs) + sum3 (tl xs)"

value "sum3 [3,2,5,1]"

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

(* pabalagon raffergon2 cammonagu*)

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

{* juacanrod *}
fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map2 f [] = []" |
"map2 f (x#xs) = [(f x)] @ map2 f xs"

value "map2 (λn. Suc n) [2,3,4,5]"

end
</source>