T4

<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 </isabelle>