T4 sol

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