Razonamiento automático (2017-18) - Contribuciones del usuario [es]

Relación 7

2018-03-01T12:06:58Z

Jospermon1:

<source lang="isar">
chapter {* R7: Deducción natural proposicional en Isabelle/HOL *}

theory R7_Deduccion_natural_proposicional
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

(* edupalhid *)
lemma notnotE: "¬¬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
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

(*anddonram*)
lemma ej_1:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
show 3: "q"
proof (rule ccontr)
assume 4: "¬q"
have 5: "¬p" using 1 4 by (rule impE)
then show False using 2 by (rule notE)
qed
qed

(*luicedval cesgongut oscgonesc diwu2 rafcabgon jescudero rafferrod macmerflo davperriv jospermon1*)
lemma ej_1_2:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have 4: "¬¬q" using 1 3 by (rule mt)
have 5: "q" using 4 by (rule notnotD) }
thus "p ⟶ q" by (rule impI)
qed

(* edupalhid*)
lemma ej_1_3:
assumes "¬q⟶¬p"
shows "p⟶q"
proof(rule impI)
assume 1:"p"
show "q"
proof-
have 2:"¬¬p" using 1 by (rule notnotI)
have "¬¬q" using assms(1) 2 by (rule mt)
then show "q" by (rule notnotE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

(*anddonram luicedval oscgonesc diwu2 rafcabgon jescudero davperriv macmerflo jospermon1*)
lemma l_e_m:
"F ∨ ¬F"
by auto

lemma ej_2:
assumes 1:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
{
assume 2: "q"
show "p ∨ q" using 2 by (rule disjI2)
}
moreover{
assume 4:"¬q"
show "p ∨ q"
proof(rule disjI1)
show "p"
proof (rule ccontr)
assume 5:"¬p"
then have "¬p ∧ ¬q" using 4 by (rule conjI)
with 1 show False by (rule notE)
qed
qed
}
moreover
show 1: "q ∨ ¬q" by (rule l_e_m)
qed

(* cesgongut *)
lemma conjnotDM1:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
have "p"
proof (rule ccontr)
assume "¬p"
have "q"
proof (rule ccontr)
assume "¬q"
have "¬p ∧ ¬q" using `¬p` `¬q` ..
then show False using assms by contradiction
qed
then have "p ∨ q" by (rule disjI2)
then show False using `¬(p ∨ q)` by contradiction
qed
then have "p ∨ q" by (rule disjI1)
then show False using `¬(p ∨ q)` by contradiction
qed

(* edupalhid *)

lemma ej_2_2:
assumes 1:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (cases)
assume "p"
then show "p ∨ q" by (rule disjI1)
next
assume "¬p"
then have "q" using 1 by simp
then show "p ∨ q" by (rule disjI2)
qed

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

(*anddonram luicedval cesgongut oscgonesc diwu2 rafcabgon jescudero rafferrod macmerflo davperriv jospermon1*)
lemma ej_3:
assumes 1:" ¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
show "p"
proof (rule ccontr)
assume "¬p"
then have "(¬p ∨ ¬q)" by (rule disjI1)
with 1 show False by (rule notE)
qed
next
show "q"
proof (rule ccontr)
assume "¬q"
then have "(¬p ∨ ¬q)" by (rule disjI2)
with 1 show False by (rule notE)
qed
qed

(* edupalhid *)
lemma ej_3_2:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
{ assume "¬p"
hence "¬p ∨ ¬q" by (rule disjI1)
with assms have False by (rule notE)}
then show "p" by (rule ccontr)
{ assume "¬q"
hence "¬p ∨ ¬q" by (rule disjI2)
with assms have False by (rule notE)}
then show "q" by (rule ccontr)
qed

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

(*anddonram luicedval rafcabgon jescudero rafferrod davperriv macmerflo jospermon1*)
lemma ej_4:
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof(rule disjE)
{
assume 2:"p"
show "¬p ∨ ¬q"
proof (rule disjI2)
show "¬q"
proof (rule notI)
assume "q"
with 2 have "p∧q" by (rule conjI)
with 1 show False by (rule notE)
qed
qed
}
moreover
{
assume "¬p"
then show "¬p ∨ ¬q" by (rule disjI1)
}
moreover
show 1: "p ∨ ¬p" by (rule l_e_m)
qed

(* cesgongut oscgonesc diwu2 edupalhid*)
lemma conjDM1:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
then have "p ∧ q" by (rule ej_3)
with assms show False by (rule notE)
qed

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

(*anddonram luicedval oscgonesc diwu2 rafcabgon rafferrod macmerflo davperriv jospermon1*)
lemma ej_5:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)

{
assume 2: "q"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof(rule disjI1)
show "p ⟶ q" using 2 by (rule impI)
qed
}
moreover{
assume 4:" ¬q"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof(rule disjI2)
show "q ⟶ p"
proof (rule impI)
assume 5:"q"
with 4 show "p" by (rule notE)
qed
qed
}
moreover
show 1: "q ∨ ¬q" by (rule l_e_m)
qed

(* cesgongut *)
lemma disjDM1:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p" proof (rule notI)
assume "p"
then have "p ∨ q" ..
then show False using assms by contradiction
qed
show "¬q" proof (rule notI)
assume "q"
then have "p ∨ q" ..
then show False using assms by contradiction
qed
qed

lemma notimpD1:
assumes "¬(p ⟶ q)"
shows "p ∧ ¬q"
proof
show "¬q" proof (rule notI)
assume "q"
have "p ⟶ q" proof (rule impI)
assume "p"
show "q" proof (rule ccontr)
assume "¬q"
then show False using `q` by contradiction
qed
qed
then show False using assms by contradiction
qed
next
show "p" proof (rule ccontr)
assume "¬p"
have "p ⟶ q" proof (rule impI)
assume "p"
show "q" proof (rule ccontr)
assume "¬q"
show False using `p` `¬p` by contradiction
qed
qed
then show False using assms by contradiction
qed
qed

lemma ej5b: "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume "¬?thesis"
then have "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule disjDM1)
then have "¬(p ⟶ q)" ..
then have "p ∧ ¬q" by (rule notimpD1)
then have "p" ..
have "¬(q ⟶ p)" using `¬(p ⟶ q) ∧ ¬(q ⟶ p)` ..
then have "q ∧ ¬p" by (rule notimpD1)
then have "¬p" ..
then show False using `p` by contradiction
qed

(*edupalhid*)
lemma ej_5c:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof(cases)
assume "(p ⟶ q)"
then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)
next
assume "¬ (p ⟶ q)"
then have 1:"¬(¬p∨q)" using equiv by simp
have "p∧¬q" using 1 by auto
then have "q ⟶ p" by auto
then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)
qed
end
</source>

Relación 5

2018-03-01T11:57:02Z

Jospermon1:

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

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
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]
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
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]
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
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))
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
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)
---------------------------------------------------------------------
*}

(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod jospermon1*)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a) auto

lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d 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 i) @ (postOrden d) @ [x])" by simp
finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp
qed

(*anddonram*)
lemma
fixes a :: "'b arbol"
shows "preOrden (espejo a) = rev (postOrden a)"
proof (induct a)
(*Si no pones el tipo da un warning. ¿Por qué?*)
fix x::'b
show " preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
fix x1a
(*Si no pones el tipo da un error. ¿Por qué?*)
fix a1:: "'b arbol"
assume H1:" preOrden (espejo a1) = rev (postOrden a1)"
fix a2:: "'b arbol"
assume H2:" preOrden (espejo a2) = rev (postOrden a2)"
have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = [x1a] @ (preOrden (espejo a2)) @ (preOrden (espejo a1)) " by simp
also have "... = [x1a] @ rev (postOrden a2) @ rev (postOrden a1) " using H1 H2 by simp
also have "... = rev( (postOrden a1) @ (postOrden a2) @ [x1a]) " by simp
finally show "preOrden (espejo (N x1a a1 a2)) = rev (postOrden (N x1a a1 a2)) "
by simp
qed

(* cesgongut *)
(* creo que es lo mismo que luicedval et al. *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "… = rev (postOrden (N x i d))" using h1 h2 by simp
finally show ?thesis .
qed
qed

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

(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1 *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) auto

lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. postOrden (espejo (H x)) = rev (preOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d 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(x # (preOrden i) @ (preOrden d))" by simp
finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" by simp
qed

(*anddonram*)
lemma
fixes a :: "'b arbol"
shows "postOrden (espejo a) = rev (preOrden a)"
proof (induct a)
fix x::'b
show "postOrden (espejo (H x)) = rev (preOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"postOrden (espejo a1) = rev (preOrden a1)"
fix a2:: "'b arbol"
assume H2:"postOrden (espejo a2) = rev (preOrden a2)"
have "postOrden (espejo (N x1a a1 a2)) = postOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = (postOrden (espejo a2)) @ (postOrden (espejo a1)) @ [x1a] " by simp
also have "... = rev (preOrden a2) @ rev (preOrden a1) @ [x1a]" using H1 H2 by simp
also have "... = rev([x1a] @ (preOrden a1) @ (preOrden a2) ) " by simp
finally show "postOrden (espejo (N x1a a1 a2)) = rev (preOrden (N x1a a1 a2))"
by simp
qed

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

(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto

theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. inOrden (espejo (H x)) = rev (inOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d 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( (inOrden i) @ x # (inOrden d)) " by simp
finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" by simp
qed

(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "inOrden (espejo a) = rev (inOrden a)"
proof (induct a)
fix x::'b
show "inOrden (espejo (H x)) = rev (inOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" inOrden (espejo a1) = rev (inOrden a1)"
fix a2:: "'b arbol"
assume H2:" inOrden (espejo a2) = rev (inOrden a2)"
have "inOrden (espejo (N x1a a1 a2)) = inOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = (inOrden (espejo a2)) @ [x1a]@ (inOrden (espejo a1)) " by simp
also have "... = rev (inOrden a2) @ [x1a] @ rev (inOrden a1) " using H1 H2 by simp
also have "... = rev((inOrden a1) @ [x1a] @ (inOrden a2) ) " by simp
finally show " inOrden (espejo (N x1a a1 a2)) = rev (inOrden (N x1a a1 a2))"
by simp
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
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
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
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
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
---------------------------------------------------------------------
*}

(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
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
---------------------------------------------------------------------
*}

(*anddonram*)
lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
theorem
fixes a :: "'b arbol"
shows "last (inOrden a) = extremo_derecha a"
proof (induct a)
fix x::'b
show "last (inOrden (H x)) = extremo_derecha (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"last (inOrden a1) = extremo_derecha a1"
fix a2:: "'b arbol"
assume H2:"last (inOrden a2) = extremo_derecha a2"
have "last (inOrden (N x1a a1 a2)) = last( (inOrden a1) @ [x1a] @ (inOrden a2)) "
by simp
also have "... = last( [x1a] @ inOrden a2) " by simp
also have "... = last (inOrden a2) " by (simp add:inOrdenNoVacio)
also have "... = extremo_derecha a2 " using H2 by simp
finally show "last (inOrden (N x1a a1 a2)) = extremo_derecha (N x1a a1 a2)"
by simp
qed

(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
(* Créditos Andrés, no sabía como hacerlo *)

theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i
fix d assume H1: "?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:inOrdenNoVacio)
also have "... = extremo_derecha d" using H1 by simp
finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" by simp
qed

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

(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "hd (inOrden a) = extremo_izquierda a"
proof (induct a)
fix x::'b
show "hd (inOrden (H x)) = extremo_izquierda (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" hd (inOrden a1) = extremo_izquierda a1"
fix a2:: "'b arbol"
assume H2:" hd (inOrden a2) = extremo_izquierda a2"
have "hd (inOrden (N x1a a1 a2)) = hd ( (inOrden a1) @ [x1a] @ (inOrden a2)) "
by simp
also have "... = hd (inOrden a1) " by (simp add:inOrdenNoVacio)
also have "... = extremo_izquierda a1 " using H1 by simp
finally show " hd (inOrden (N x1a a1 a2)) = extremo_izquierda (N x1a a1 a2)"
by simp
qed

(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d
have "hd (inOrden (N x i d)) = hd (inOrden i @ x # inOrden d)" by simp
also have "... = hd (inOrden i)" by (simp add:inOrdenNoVacio)
also have "... = extremo_izquierda i" using H1 by simp
finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)" by simp
qed

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

(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "hd (preOrden a) = last (postOrden a)"
proof (induct a)
fix x::'b
show "hd (preOrden (H x)) = last (postOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"hd (preOrden a1) = last (postOrden a1)"
fix a2:: "'b arbol"
assume H2:"hd (preOrden a2) = last (postOrden a2)"
have "hd (preOrden (N x1a a1 a2)) = hd ( [x1a] @ (preOrden a1) @ (preOrden a2)) "
by simp
also have "... = x1a " by simp
also have "... = last ((preOrden a1) @ (preOrden a2)@ [x1a])" by simp
finally show "hd (preOrden (N x1a a1 a2)) = last (postOrden (N x1a a1 a2))"
by simp
qed

(* luicedval rafcabgon rafferrod*)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
also have "... = last (postOrden d @ postOrden i @ [x])" by simp
finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))" by simp
qed

(* edupalhid *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed

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

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

(*anddonram diwu2 *)
theorem "hd (preOrden a) = raiz a"
proof (induct a)
fix x::'b
show "hd (preOrden (H x)) = raiz (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" hd (preOrden a1) = raiz a1"
fix a2:: "'b arbol"
assume H2:" hd (preOrden a2) = raiz a2"
have "hd (preOrden (N x1a a1 a2)) = hd ( [x1a] @ (preOrden a1) @ (preOrden a2)) "
by simp
also have "... = x1a " by simp
finally show "hd (preOrden (N x1a a1 a2)) = raiz (N x1a a1 a2)"
by simp
qed

(* luicedval rafcabgon macmerflo rafferrod cesgongut jospermon1*)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed

(* edupalhid *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed

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

(*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*
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
*)

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

(*anddonram*)
theorem "last (postOrden a) = raiz a"
proof (induct a)
fix x::'b
show "last (postOrden (H x)) = raiz (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"last (postOrden a1) = raiz a1 "
fix a2:: "'b arbol"
assume H2:"last (postOrden a2) = raiz a2"
have " last (postOrden (N x1a a1 a2)) = last ( (preOrden a1) @ (preOrden a2)@[x1a] ) "
by simp
also have "... = x1a " by simp
finally show " last (postOrden (N x1a a1 a2)) = raiz (N x1a a1 a2)"
by simp
qed

(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod cesgongut jospermon1*)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])" by simp
also have "... = last (postOrden d @ [x])" by simp
also have "... = x" by simp
finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed

(* edupalhid *)
theorem "last (postOrden a) = raiz a"
apply (induct a)
apply simp
apply simp
done
end

(* edupalhid *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
show "?P (N x i d)" by simp
qed

</source>

Relación 2

2018-03-01T11:52:27Z

Jospermon1:

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

(* anddonram edupalhid macmerflo luicedval rafcabgon jescudero
davperriv diwu2 rafferrod jospermon1 *)
fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = 2*(Suc n) - 1 + sumaImpares n"

value "sumaImpares 5 = 25"

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

value "sumaImpares2 5 = 25"

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

(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
jescudero rafferrod jospermon1*)
lemma "sumaImpares n = n*n"
by(induct n) simp_all

(* cesgongut *)
lemma "sumaImpares2 n = n*n"
apply (induct n)
apply simp
apply simp
done

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

(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
jescudero rafferrod cesgongut jospermon1*)
fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 1 + 1"
| "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno n"

value "sumaPotenciasDeDosMasUno 3 = 16"

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

(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
jescudero rafferrod cesgongut jospermon1*)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by(induct 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]
------------------------------------------------------------------ *}

(* anddonram edupalhid macmerflo luicedval rafcabgon davperriv diwu2
jescudero rafferrod cesgongut jospermon1*)
fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []"
| "copia (Suc n) x= x # copia n x"

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

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

(* anddonram luicedval macmerflo rafcabgon davperriv diwu2 rafferrod
jescudero cesgongut jospermon1*)
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

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

(* edupalhid *)
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p [] = True" |
"todos2 p (x#xs) = (if p x then todos2 p xs else False)"

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

(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
rafferrod jescudero cesgongut jospermon1*)
lemma "todos (λy. y=x) (copia n x)"
by (induct n) simp_all

lemma "todos2 (λy. y=x) (copia n x)"
by (induct 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]
------------------------------------------------------------------ *}

(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
rafferrod jescudero cesgongut jospermon1*)
fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]"
| "amplia (x#xs) y = x # amplia xs y"

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

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

(* anddonram edupalhid luicedval macmerflo rafcabgon davperriv diwu2
rafferrod jescudero cesgongut *)
lemma "amplia xs y = xs @ [y]"
by (induct xs) simp_all

end
</source>

Relación 4

2018-03-01T11:48:55Z

Jospermon1:

<source lang="isar">
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.
---------------------------------------------------------------------
*}

(* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
macmerflo rafferrod jospermon1*)
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

value "todos (λx. 1<length x) [[2,1,4],[1,3::nat]] = True"
value " ¬todos (λx. 1<length x) [[2,1,4],[3::nat]] = True"

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

(* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
macmerflo rafferrod jospermon1*)
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
| "algunos p (x#xs) = (p x ∨ algunos p xs)"

value " algunos (λx. 1<length x) [[2::nat,1,4],[3]] = True"
value " ¬algunos (λx. 1<length x) [[],[3::nat]] = True"

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}
(* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
macmerflo rafferrod jospermon1*)
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)
---------------------------------------------------------------------
*}

(* anddonram [conmutatividad and porque no sé hacerlo de otra forma] *)
lemma and_comm: "(a ∧ b) = (b ∧ a)"
by (cases a) auto

(* anddonram diwu2 *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos 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 ∧ Q a ∧ todos Q xs ∧ todos P xs)"
by (simp add: and_comm)
also have "... = (P a ∧ todos Q (a # xs) ∧ todos P xs)" by simp
also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)"
by (simp add: and_comm)
finally show "todos (λx. P x ∧ Q x) (a # xs) =
(todos P (a # xs) ∧ todos Q (a # xs))"
by simp
qed

(* edupalhid *)
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

(* rafferrod *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos 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 auto
finally show "todos (λx. P x ∧ Q x) (a#xs) =
(todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

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

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

(* anddonram edupalhid cesgongut luicedval jescudero rafcabgon diwu2
macmerflo cesgongut rafferrod jospermon1*)
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)
---------------------------------------------------------------------
*}

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
cesgongut rafferrod jospermon1*)
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

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

(*anddonram*)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (simp_all add: todos_append and_comm)

(* edupalhid diwu2 macmerflo rafferrod *)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

(* cesgongut *)
lemma "todos P (rev xs) = todos P xs"
using todos_append by (induct xs) auto

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

(* anddonram diwu2 *)
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
finally show "todos P (rev (a # xs)) = todos P (a # xs)"
by (simp add: and_comm)
qed

(* edupalhid *)
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 ∧ P a)" using HI by simp
also have "... = (P a ∧ todos P xs)" by arith
also have "... = (todos P (a#xs))" by simp
finally show "todos P (rev (a # xs)) = (todos P (a#xs))" by simp
qed

(* rafferrod cesgongut *)
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 [a] ∧ todos P xs)" by auto (*/ blast *)
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)
---------------------------------------------------------------------
*}

(* anddonram Contraejemplo*)
value "let xs=[True,False]
in (algunos (λx. (λx. (x=False)) x ∧ (λx. x) x) xs =
(algunos (λx. (x=False)) xs ∧ algunos (λx. x) xs))"

(* edupalhid diwu2 rafferrod cesgongut jospermon1*)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

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

(* anddonram edupalhid jescudero luicedval rafcabgon diwu2 macmerflo
cesgongut rafferrod jospermon1*)
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
rafferrod jospermon1*)
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 a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = algunos P (f a#map f xs)" by simp
also have "... = ((P ∘ f) a ∨ algunos P (map f xs))" by simp
also have "... = ((P ∘ f) a ∨ algunos (P ∘ f) xs) " using HI by simp
finally show "algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)"
by simp
qed

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
cesgongut rafferrod jospermon1*)
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)
---------------------------------------------------------------------
*}

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
cesgongut rafferrod jospermon1*)
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
---------------------------------------------------------------------
*}

(* anddonram [conmutatividad or porque no sé hacerlo de otra forma] *)
lemma or_comm: "(a ∨ b) = (b ∨ a)"
by (cases a) auto

(* anddonram *)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (simp_all add: algunos_append or_comm)

(* edupalhid diwu2 rafferrod*)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

(* cesgongut *)
lemma "algunos P (rev xs) = algunos P xs"
using algunos_append by (induct xs) auto

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

(* anddonram diwu2 *)
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 ∨ P a)" using HI by simp
also have "... = (P a ∨ algunos P xs)" by (simp add:or_comm)
finally show " algunos P (rev (a # xs)) = algunos P (a # xs) "
by simp
qed

(* edupalhid *)
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

(* rafferrod cesgongut *)
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 auto (*/ blast *)
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.
---------------------------------------------------------------------
*}

(* anddonram edupalhid diwu2 jescudero macmerflo rafferrod rafcabgon jospermon1*)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto

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

(* edupalhid *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
(is "?T xs")
proof (induct xs)
show "?T []" by simp
next
fix a xs assume HI: "?T xs"
have p1:" (Q a ∨ algunos P xs) = (algunos P xs ∨ Q a)"
by (simp add: HOL.disj_commute)
have "algunos (λx. P x ∨ Q x) (a # xs) =
(algunos P [a] ∨ algunos 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)"
using p1 by simp
also have "… = (algunos P (a # xs) ∨ algunos Q (a # xs))" by simp
finally show "?T (a # xs)" by simp
qed

(* rafferrod *)
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 auto
finally show "algunos (λx. P x ∨ Q x) (a#xs) =
(algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed

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

lemma "algunos (λx. P x ∨ Q x) xs = algunos (λx. Q x ∨ P x) xs"
proof (induct xs)
show "algunos (λx. P x ∨ Q x) [] = algunos (λx. Q x ∨ P x) []" by simp
next
fix h xs
assume HI: "algunos (λx. P x ∨ Q x) xs = algunos (λx. Q x ∨ P x) xs"
have "algunos (λx. P x ∨ Q x) (h#xs)
= ((λx. P x ∨ Q x) h ∨ algunos (λx. P x ∨ Q x) xs)" by simp
also have "… = ((λx. P x ∨ Q x) h ∨ algunos (λx. Q x ∨ P x) xs)" using HI by simp
also have "… = ((λx. Q x ∨ P x) h ∨ algunos (λx. Q x ∨ P x) xs)" by blast
also have "… = algunos (λx. Q x ∨ P x) (h#xs)" by (simp add: algunos_append)
finally show "algunos (λx. P x ∨ Q x) (h#xs)
= algunos (λx. Q x ∨ P x) (h#xs)" by simp
qed

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

(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon macmerflo jospermon1*)
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)
---------------------------------------------------------------------
*}

(*anddonram edupalhid diwu2 rafferrod cesgongut macmerflo *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
fix a xs
assume HI:"algunos P xs = (¬ todos (λx. ¬ P x) xs)"
have "algunos P (a # xs) =(P a ∨ algunos P xs)" by simp
also have "... = (P a ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
also have "... = (¬ (¬ P a ∧ todos (λx. ¬ P x) xs))" 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
---------------------------------------------------------------------
*}

(* anddonram edupalhd luicedval rafcabgon diwu2 jescudero macmerflo
cesgongut rafferrod jospermon1*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = ((a=x) ∨ estaEn x xs)"

value " estaEn (2::nat) [3,2,4] = True"
value " estaEn (1::nat) [3,2,4] = False"

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
cesgongut rafferrod jospermon1*)
lemma "estaEn x xs=algunos (λy.(y=x)) xs"
by (induct xs) auto

(* anddonram edupalhid luicedval rafcabgon jescudero macmerflo cesgongut
rafferrod *)
lemma "estaEn x xs=algunos (λy.(y=x)) xs"
proof (induct xs)
show "estaEn x []=algunos (λy.(y=x)) []" by simp
next
fix a xs
assume HI:"estaEn x xs = algunos (λy. y = x) xs"
have "estaEn x (a # xs) =((a=x) ∨ estaEn x xs)" by simp
also have "... = ((a=x) ∨ algunos (λy. y = x) xs)" using HI by simp
finally show "estaEn x (a # xs) = algunos (λy. y = x) (a # xs)" by simp
qed

end
</source>

Relación 1

2018-02-28T18:10:02Z

Jospermon1:

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

(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2
jospermon1 macmerflo*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0" |
"longitud (x#xs) = 1 + longitud xs "

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

(* davperriv *)
fun longitud3 :: "'a list ⇒ nat" where
"longitud3 [] = 0"
| "longitud3 xs = 1 + longitud3 (butlast xs)"

value "longitud [a,b,c] = 3"
value "longitud (x#(y#(z#[])))"

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 jescudero
rafferrod davperriv macmerflo jospermon1*)
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

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

(* edupalhid cesgongut rafcabgon diwu2 jescudero jospermon1*)
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []" |
"inversa (x#xs) = inversa xs @[x] "

(* anddonram *)
fun conc1 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc1 [] b = b"
| "conc1 (x#xs) b = x # conc1 xs b"

value "conc1 [1::int,2] [3] = [1,2,3]"
value "conc1 [1::int,2] [] = [1,2]"

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

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

(* luicedval *)
fun cuantos :: "'a list ⇒ nat" where
"cuantos [] = 0" |
"cuantos (x#xs) = 1 + cuantos xs"

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

fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []" |
"inversa3 xs = invertir (cuantos xs) xs"

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

(* rafferrod davperriv macmerflo *)
fun inversa4 :: "'a list ⇒ 'a list" where
"inversa4 [] = []" |
"inversa4 x = (last x) # (inversa4 (butlast x))"

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
davperriv macmerflo jospermon1*)
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []" |
"repite n x = x # repite (n-1) x"

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

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

(* edupalhid anddonram cesgongut luicedval rafferrod macmerflo jospermon1*)
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys" |
"conc (x#xs) ys = x # conc xs ys"

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

(* rafcabgon diwu2 *)
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 [] [] = []" |
"conc2 xs ys = xs @ ys"

(* Comentario: El objetivo es mostrar la definición de @ *)

(* jescudero *)
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys" |
"conc3 xs [] = xs" |
"conc3 (x#xs) (y#ys) = x # (y # (conc3 xs ys))"

(* Comentario: Se puede simplificar. *)

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

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2
rafferrod macmerflo *)
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []" |
"coge 0 xs = []" |
"coge n (x#xs) = x # coge (n-1) xs "

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

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

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

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero macmerflo jospermon1*)
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina 0 xs = xs" |
"elimina n [] = []" |
"elimina n (x#xs) = elimina (n-1) xs"

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

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

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

(* edupalhid jescudero*)
fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = (if xs = [] then True else False)"

(* anddonram diwu2 *)
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 x = (x=[])"

(* cesgongut luicedval rafcabgon rafferrod davperriv macmerflo*)
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 [] = True" |
"esVacia3 xs = False"

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

(* edupalhid anddonram rafcabgon diwu2 rafferrod davperriv *)
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 []"

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

(* Comentario: Se puede simplificar. *)

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

value "inversaAc [a,c,b,e] = [e,b,c,a]"

(* luicedval *)
fun elementos :: "'a list ⇒ nat" where
"elementos [] = 0" |
"elementos (x#xs) = 1 + elementos xs"

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

fun inversaAc3 :: "'a list ⇒ 'a list" where
"inversaAc3 xs = inversaAcAux3 (elementos xs) xs"

value "inversaAc3 [a,c,b,e] = [e,b,c,a]"
value "inversaAc3 [] = []"

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

(* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero macmerflo jospermon1*)
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
|"sum (x#xs) = x+sum xs"

(* davperriv *)
fun sum2 :: "nat list ⇒ nat" where
"sum2 [] = 0" |
"sum2 xs = (hd xs) + sum2 (tl xs)"

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

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

(* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero macmerflo jospermon1*)
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
|"map f (x#xs) = f x # (map f xs)"

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

value "map (λx. x+1) [3::nat,2,4]=[4,3,5]"

end
</source>

Relación 6

2018-01-17T23:59:26Z

Jospermon1:

<source lang="isar">
chapter {* R7: Árboles binarios completos *}

theory R7_Arboles_binarios_completos
imports Main
begin

text {*
En esta relación se piden demostraciones automáticas (lo más cortas
posibles). Para ello, en algunos casos es necesario incluir lemas
auxiliares (que se demuestran automáticamente) y usar ejercicios
anteriores.

---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}

datatype arbol = H | N arbol arbol

value "N (N H H) (N H H) = (N (N H H) (N H H) :: arbol)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}
(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun hojas :: "arbol => nat" where
"hojas H = 1"
| "hojas (N x y) =hojas x + hojas y"

value "hojas (N (N H H) (N H H)) = 4"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N x y) = Suc (max (profundidad x) (profundidad y))"

value "profundidad (N (N H H) (N H H)) = 2"

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

value "abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).

Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N i d) =((f i = f d) ∧ (es_abc f i) ∧ (es_abc f d))"

value "es_abc profundidad (abc 4) = True"

text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}

value "size (N (N H H) (N H H)) = 3"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H))) = 7"

text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv jospermon1*)
(* blast no funciona, ¿cómo eliminar la conjunción sin recurrir a auto? *)
lemma hojas_prof:
"es_abc profundidad a ⟶ hojas a = 2^profundidad a"
by (induct a) auto
theorem comp_p_h: "es_abc profundidad a = es_abc hojas a"
by (induct a) (auto simp add: hojas_prof)

lemma abc_profundidad_hojas:
"es_abc profundidad a ⟶ hojas a = 2 ^ profundidad a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i assume HIi: "?P i"
fix d assume HId: "?P d"
show "?P (N i d)" using HIi HId by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv jospermon1*)
lemma hojas_size:
" es_abc hojas a ⟶ hojas a = Suc (size a)"
by (induct a) auto

theorem comp_h_s: "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add: hojas_size )

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon*)
theorem "es_abc profundidad a = es_abc size a"
by (simp_all add:comp_p_h comp_h_s)

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
theorem "es_abc f (abc n) "
by (induct n) auto

(* cesgongut *)
theorem "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix a assume HI: "?P a"
show "?P (Suc a)" using HI by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es igual a
(abc (profundidad a)).
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc macmerflo diwu2 rafcabgon*)
theorem "es_abc profundidad a =(a=abc (profundidad a)) "
by (induct a) auto

(* edupalhid *)
lemma
assumes "es_abc profundidad a"
shows "a = (abc (profundidad a))"
using assms
by (induct a) auto

(* cesgongut *)
theorem "es_abc profundidad a ⟶ a = (abc (profundidad a))" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i assume HIi: "?P i"
fix d assume HId: "?P d"
show "?P (N i d)" using HIi HId by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}

(*anddonram(mas o menos llegué a la conclusión de que f(H)=f(N i d) ) luicedval edupalhid rafcabgon cesgongut davperriv *)
fun funcion :: "arbol => nat" where
"funcion H = 1"
| "funcion (N x y) = funcion x "

theorem "es_abc size a = es_abc funcion a"
quickcheck
oops

end
</source>

Relación 6

2018-01-17T23:58:57Z

Jospermon1:

<source lang="isar">
chapter {* R7: Árboles binarios completos *}

theory R7_Arboles_binarios_completos
imports Main
begin

text {*
En esta relación se piden demostraciones automáticas (lo más cortas
posibles). Para ello, en algunos casos es necesario incluir lemas
auxiliares (que se demuestran automáticamente) y usar ejercicios
anteriores.

---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}

datatype arbol = H | N arbol arbol

value "N (N H H) (N H H) = (N (N H H) (N H H) :: arbol)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}
(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod*)
fun hojas :: "arbol => nat" where
"hojas H = 1"
| "hojas (N x y) =hojas x + hojas y"

value "hojas (N (N H H) (N H H)) = 4"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N x y) = Suc (max (profundidad x) (profundidad y))"

value "profundidad (N (N H H) (N H H)) = 2"

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

value "abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).

Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N i d) =((f i = f d) ∧ (es_abc f i) ∧ (es_abc f d))"

value "es_abc profundidad (abc 4) = True"

text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}

value "size (N (N H H) (N H H)) = 3"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H))) = 7"

text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv jospermon1*)
(* blast no funciona, ¿cómo eliminar la conjunción sin recurrir a auto? *)
lemma hojas_prof:
"es_abc profundidad a ⟶ hojas a = 2^profundidad a"
by (induct a) auto
theorem comp_p_h: "es_abc profundidad a = es_abc hojas a"
by (induct a) (auto simp add: hojas_prof)

lemma abc_profundidad_hojas:
"es_abc profundidad a ⟶ hojas a = 2 ^ profundidad a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i assume HIi: "?P i"
fix d assume HId: "?P d"
show "?P (N i d)" using HIi HId by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv jospermon1*)
lemma hojas_size:
" es_abc hojas a ⟶ hojas a = Suc (size a)"
by (induct a) auto

theorem comp_h_s: "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add: hojas_size )

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon*)
theorem "es_abc profundidad a = es_abc size a"
by (simp_all add:comp_p_h comp_h_s)

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
theorem "es_abc f (abc n) "
by (induct n) auto

(* cesgongut *)
theorem "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix a assume HI: "?P a"
show "?P (Suc a)" using HI by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es igual a
(abc (profundidad a)).
---------------------------------------------------------------------
*}

(*anddonram luicedval oscgonesc macmerflo diwu2 rafcabgon*)
theorem "es_abc profundidad a =(a=abc (profundidad a)) "
by (induct a) auto

(* edupalhid *)
lemma
assumes "es_abc profundidad a"
shows "a = (abc (profundidad a))"
using assms
by (induct a) auto

(* cesgongut *)
theorem "es_abc profundidad a ⟶ a = (abc (profundidad a))" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i assume HIi: "?P i"
fix d assume HId: "?P d"
show "?P (N i d)" using HIi HId by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}

(*anddonram(mas o menos llegué a la conclusión de que f(H)=f(N i d) ) luicedval edupalhid rafcabgon cesgongut davperriv *)
fun funcion :: "arbol => nat" where
"funcion H = 1"
| "funcion (N x y) = funcion x "

theorem "es_abc size a = es_abc funcion a"
quickcheck
oops

end
</source>

Relación 3

2017-11-30T07:23:05Z

Jospermon1:

<source lang="isar">
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"
(* anddonram edupalhid rafcabgon luicedval jescudero macmerflo diwu2
rafferrod cesgongut jospermon1 *)
lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0*0" by simp
next
fix n
assume HI: "sumaImpares n=n*n"
have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" by simp
also have "... = n*n + (2*n+1)" using HI 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)
------------------------------------------------------------------- *}

(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod jospermon1 *)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
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
also have "... = 2^(n+1) + 2^(n+1)" using HI by simp
also have "... = 2^((n+1)+1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)"
by simp
qed

(* rafcabgon cesgongut *)
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
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
also have "... = 2^(n+1) + 2^(n+1)" using HI by simp
also have "... = 2^((Suc n) + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)"
by simp
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.
------------------------------------------------------------------- *}

(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)" by simp
next
fix n
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 "... = todos (λy. y=x) (copia n x) " by simp
show "todos (λy. y=x) (copia (Suc n) x)" using HI by simp
qed

(* rafferrod *)
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)" by simp
next
fix n
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
also have "... = True" using HI by simp
finally show "todos (λy. y=x) (copia (Suc n) x)" 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"

(* anddonram rafferrod *)
lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "⋀x. factI' n x = x * factR n"
fix x
have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
also have "... = (x * Suc n) * factR n" using HI by simp
also have "... = x * (Suc n * factR n)" by (simp del:mult_Suc)
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed

(* edupalhid rafcabgon luicedval macmerflo diwu2 jescudero jospermon1 *)
lemma fact': "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. 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
also have "... = (x * Suc n) * factR n" using HI by simp
also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc)
also have "... = x * factR (Suc n)" by simp
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed
qed

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

(* anddonram edupalhid rafcabgon luicedval macmerflo diwu2 jescudero
rafferrod jospermon1 *)
corollary "factI n = factR n"
proof -
fix n
have "factI n = factI' n 1" by simp
also have "... = 1 * factR n" by (simp add:fact)
finally show "factI n = factR n" by simp
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]
------------------------------------------------------------------- *}

(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 *)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
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
also have "... = a # (xs @[y]) " using HI by simp
also have "... =(a # xs) @[y] " using HI by simp
finally show "amplia (a#xs) y= (a # xs) @[y]" by simp
qed

(* edupalhid *)
lemma "amplia xs y = xs @ [y]" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
have "amplia (x # xs) y = x # amplia xs y" by simp
also have "... = (x # xs) @ [y]" using HI by simp
finally show "?P (x#xs)" by simp
qed

end
</source>

Relación 1

2017-11-02T10:46:43Z

Jospermon1:

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

(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2 davperriv jospermon1*)
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0" |
"longitud (x#xs) = 1 + longitud xs "

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

value "longitud [a,b,c] = 3"
value "longitud (x#(y#(z#[])))"

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 jescudero
rafferrod davperriv*)
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

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

(* edupalhid cesgongut rafcabgon diwu2 jescudero*)
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []" |
"inversa (x#xs) = inversa xs @[x] "

(* anddonram *)
fun conc1 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc1 [] b = b"
| "conc1 (x#xs) b = x # conc1 xs b"

value "conc1 [1::int,2] [3] = [1,2,3]"
value "conc1 [1::int,2] [] = [1,2]"

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

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

(* luicedval *)
fun cuantos :: "'a list ⇒ nat" where
"cuantos [] = 0" |
"cuantos (x#xs) = 1 + cuantos xs"

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

fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []" |
"inversa3 xs = invertir (cuantos xs) xs"

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

(* rafferrod *)
fun inversa4 :: "'a list ⇒ 'a list" where
"inversa4 [] = []" |
"inversa4 x = (last x) # (inversa4 (butlast x))"

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod *)
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []" |
"repite n x = x # repite (n-1) x"

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

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

(* edupalhid anddonram cesgongut luicedval rafferrod *)
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys" |
"conc (x#xs) ys = x # conc xs ys"

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

(* rafcabgon diwu2 *)
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 [] [] = []" |
"conc2 xs ys = xs @ ys"

(* Comentario: El objetivo es mostrar la definición de @ *)

(* jescudero *)
fun conc3 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys" |
"conc3 xs [] = xs" |
"conc3 (x#xs) (y#ys) = x # (y # (conc3 xs ys))"

(* Comentario: Se puede simplificar. *)

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod *)
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []" |
"coge 0 xs = []" |
"coge n (x#xs) = x # coge (n-1) xs "

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

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

(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero*)
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina 0 xs = xs" |
"elimina n [] = []" |
"elimina n (x#xs) = elimina (n-1) xs"

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

(* edupalhid jescudero*)
fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = (if xs = [] then True else False)"

(* anddonram diwu2 *)
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 x = (x=[])"

(* cesgongut luicedval rafcabgon rafferrod *)
fun esVacia3 :: "'a list ⇒ bool" where
"esVacia3 [] = True" |
"esVacia3 xs = False"

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

(* edupalhid anddonram rafcabgon diwu2 rafferrod *)
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 []"

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

(* Comentario: Se puede simplificar. *)

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

value "inversaAc [a,c,b,e] = [e,b,c,a]"

(* luicedval *)
fun elementos :: "'a list ⇒ nat" where
"elementos [] = 0" |
"elementos (x#xs) = 1 + elementos xs"

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

fun inversaAc3 :: "'a list ⇒ 'a list" where
"inversaAc3 xs = inversaAcAux3 (elementos xs) xs"

value "inversaAc3 [a,c,b,e] = [e,b,c,a]"
value "inversaAc3 [] = []"

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

(* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero*)
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
|"sum (x#xs) = x+sum xs"

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

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

(* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
jescudero*)
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
|"map f (x#xs) = f x # (map f xs)"

value "map (λx. x+1) [3::nat,2,4]=[4,3,5]"

end
</source>