Mjoseh: Protegió «T4 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-06-01T10:33:40Z

Protegió «T4 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « theory T4_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-----------…»

2020-06-01T10:29:44Z

Página creada con «<source lang = "isabelle"> theory T4_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-----------…»

Página nueva

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

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

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

text ‹-----------------------------------------------------------------
Se define 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]
---------------------------------------------------------------------›

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

text ‹------------------------------------------------------------------
Ejercicio. Demostrar que
length (elimina n xs) ≤ length xs - n
---------------------------------------------------------------------›

― ‹Por inducción en n y xs según el esquema elimina.induct›

― ‹Estructurada›
lemma "length (elimina n xs) ≤ length xs"
proof(induct n xs rule :elimina.induct)
show "⋀n. length (elimina n []) ≤ length []" by simp
next
show "⋀v va. length (elimina 0 (v # va)) ≤ length (v # va)"
by simp
next
show "⋀n x xs.
length (elimina n xs) ≤ length xs ⟹
length (elimina (Suc n) (x # xs)) ≤ length (x # xs)"
by simp
qed

― ‹Automática›
lemma "length (elimina n xs) ≤ length xs"
by (induct n xs rule :elimina.induct) simp_all

― ‹Declarativa detallada›

lemma "length (elimina n xs) ≤ length xs"
proof(induct n xs rule :elimina.induct)
fix n ::"nat"
show "length (elimina n []) ≤ length []"
by (simp only: elimina.simps(1) list.size(3))
next
fix x::"'a" and xs::"'a list"
show "length (elimina 0 (x # xs)) ≤ length (x #xs)"
by (simp only: elimina.simps(2) list.size(2))
next
fix n ::"nat" and x::"'a" and xs::"'a list"
assume H:"length (elimina n xs) ≤ length xs"
have "length(elimina (Suc n) (x#xs)) = length(elimina n xs)"
by (simp only: elimina.simps(3))
also have "… ≤ length xs"
using H by (simp only:)
also have "… ≤ length (x#xs)"
by (simp only: list.size(4))
finally show "length(elimina (Suc n) (x#xs)) ≤ length (x#xs)".
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs"
apply (induct n xs rule :elimina.induct)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2))
apply (simp only: elimina.simps(3))
apply (simp only: list.size)
done

― ‹Por inducción en n con xs arbitrario›

― ‹Auxiliar›
lemma elimina0: "elimina 0 xs = xs"
apply (cases xs)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2))
done

― ‹Estructurada›
lemma "length (elimina n xs) ≤ length xs - n"
proof (induct n arbitrary: xs)
show "⋀xs. length (elimina 0 xs) ≤ length xs - 0"
by (simp only: elimina0)
next
fix n :: nat and xs :: "'a list"
assume HI: "⋀xs:: 'a list. length (elimina n xs) ≤ length xs - n"
show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case (Cons a list)
then show ?thesis using HI by simp
qed
qed

― ‹Declarativa detallada›
lemma "length (elimina n xs) ≤ length xs - n"
proof (induct n arbitrary: xs)
fix xs :: "'a list"
show "length (elimina 0 xs) ≤ length xs - 0"
by (simp only: elimina0 list.size(3))
next
fix n :: nat and xs :: "'a list"
assume HI: "⋀xs:: 'a list. length (elimina n xs) ≤ length xs - n"
show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
proof (cases xs)
assume "xs = []"
then have "elimina (Suc n) xs = elimina (Suc n) []"
by (rule arg_cong)
also have "… = []"
by (simp only: elimina.simps(1))
finally have "elimina (Suc n) xs = []"
by this
then have "length (elimina (Suc n) xs) = 0"
by (simp only: list.size(3))
then show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
by (simp only: list.size(3))
next
fix y:: "'a" and ys :: "'a list"
assume 1: "xs = y # ys"
have 2: "length (elimina n ys) ≤ length ys - n"
using HI by this
have "length (elimina (Suc n) xs) = length (elimina (Suc n) (y#ys))"
using 1 by (rule arg_cong)
also have "… = length (elimina n ys)"
by (simp only: elimina.simps(3))
also have "… ≤ length ys - n"
using 2 by (simp only:)
also have "… = 1 + length ys - (Suc n)"
by (simp only: diff_Suc_Suc)
also have "… = length (y#ys) - (Suc n)"
by (simp only: list.size(4))
also have "… = length xs - (Suc n)"
using 1 by (simp only: list.size(4))
finally show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
by this
qed
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs - n"
apply (induct n arbitrary: xs)
apply (simp only: elimina0)
apply (case_tac xs)
apply (simp only: elimina.simps)
apply (simp only: list.size(3))
apply (simp only: elimina.simps(3))
apply (simp only: list.size(4))
apply (simp only: add_Suc_right)
apply (simp only: add.right_neutral)
apply (simp only: diff_Suc_Suc)
done

― ‹Demostración por inducción en xs con n arbitrario›

― ‹Estructurada›

lemma "length (elimina n xs) ≤ length xs"
proof (induct xs arbitrary: n)
show "⋀n. length (elimina n []) ≤ length []" by simp
next
fix n::"nat" and x::'a and xs:: "'a list"
assume HI: " ⋀n. length (elimina n xs) ≤ length xs"
show "length (elimina n (x# xs)) ≤ length (x#xs)"
proof(cases n)
case 0
then show ?thesis by simp
next
case (Suc nat)
then show ?thesis using HI
by (metis elimina.simps(3) list.size(4) trans_le_add1)
qed
qed

― ‹Declarativa detallada›

lemma "length (elimina n xs) ≤ length xs"
proof (induct xs arbitrary: n)
fix n::"nat"
show "length (elimina n []) ≤ length []"
by (simp only: elimina.simps(1) list.size)
next
fix n::"nat" and x::'a and xs:: "'a list"
assume HI: " ⋀n. length (elimina n xs) ≤ length xs"
show "length (elimina n (x# xs)) ≤ length (x#xs)"
proof(cases n)
assume "n=0"
then have "(elimina n (x# xs)) =(x#xs)"
by (simp only: elimina.simps(2))
then have "length (elimina n (x# xs)) = length (x#xs)"
by (rule arg_cong)
then show "length (elimina n (x# xs)) ≤ length (x#xs)"
by (simp only: order_refl)
next
fix m:: nat
assume "n=(Suc m)"
then have "length (elimina n (x# xs)) =
length (elimina (Suc m) (x# xs))"
by (rule arg_cong)
also have "… =length (elimina m xs)"
by (simp only: elimina.simps(3))
also have "… ≤ length xs" using HI by (simp only:)
also have "… ≤ 1+length xs " by (simp only: le_add1)
also have "…≤ length (x#xs)" by (simp only: list.size)
finally show "length (elimina n (x# xs))≤length (x#xs)"
by (simp only:)
qed
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs - n"
apply (induct xs arbitrary: n)
apply (simp only: elimina.simps(1) list.size)
apply (case_tac n)
apply (simp only: elimina.simps(2) list.size)
apply (simp only: elimina.simps(3) list.size)
apply (simp only:add_Suc_right)
apply (simp only:add.right_neutral)
apply (simp only: diff_Suc_Suc)
done

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que si se verifica
∀x. (P x ⟶ (∃y. Q y))
entonces se verifica
∀x. ∃y. (P x ⟶ Q y)

Nota: Hacer la demostración de forma detallada. Es opcional hacerla
de forma declarativa o aplicativa.
--------------------------------------------------------------------›

― ‹Demostración declarativa detallada›

lemma
fixes P Q :: "'b ⇒ bool"
assumes "∀x. ∃y. (P x ⟶ Q y)"
shows "∀x. (P x ⟶ (∃y. Q y))"
proof (rule allI)
fix x
show "P x ⟶ (∃y. Q y)"
proof (rule impI)
assume "P x"
have " ∃y. (P x ⟶ Q y)"
using assms by (rule allE)
then obtain b where "P x ⟶ Q b"
by (rule exE)
then have "Q b"
using ‹P x› by (rule mp)
then show "∃y. Q y"
by (rule exI)
qed
qed

― ‹Demostración aplicativa detallada›

lemma
"∀x. (P x ⟶ (∃y. Q y)) ⟹ ∀x. ∃y. (P x ⟶ Q y)"
apply(rule allI)
apply(erule_tac x = x in allE)
apply(case_tac "P x")
apply(drule mp, assumption)
apply(erule exE)
apply (rule_tac x = y in exI)
apply(rule impI, assumption)
apply (rule exI)
apply(rule impI)
apply(erule notE, assumption)
done

end
</source>

← Revisión anterior	Revisión del 10:33 1 jun 2020
(Sin diferencias)

T4 sol - Historial de revisiones

Mjoseh: Protegió «T4 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « theory T4_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-----------…»