Theory ND

subsection‹Natural Deduction›

theory ND
imports Formulas
begin

inductive ND :: "'a formula set ⇒ 'a formula ⇒ bool" (infix ‹⊢› 30) where
Ax: "F ∈ Γ ⟹ Γ ⊢ F" |
NotE: "⟦Γ ⊢ Not F; Γ ⊢ F ⟧ ⟹ Γ ⊢ ⊥" |
NotI: "F ▹ Γ ⊢ ⊥ ⟹ Γ ⊢ Not F" |
CC: "Not F▹ Γ ⊢ ⊥ ⟹ Γ ⊢ F" |
AndE1: "Γ ⊢ And F G ⟹ Γ ⊢ F" |
AndE2: "Γ ⊢ And F G ⟹ Γ ⊢ G" |
AndI: "⟦ Γ ⊢ F; Γ ⊢ G ⟧ ⟹ Γ ⊢ And F G" |
OrI1: "Γ ⊢ F ⟹ Γ ⊢ Or F G" |
OrI2: "Γ ⊢ G ⟹ Γ ⊢ Or F G" |
OrE: "⟦ Γ ⊢ Or F G; F▹Γ ⊢ H; G▹Γ ⊢ H ⟧ ⟹ Γ ⊢ H" |
ImpI: "F ▹ Γ ⊢ G ⟹ Γ ⊢ Imp F G" |
ImpE: "⟦ Γ ⊢ Imp F G; Γ ⊢ F ⟧ ⟹ Γ ⊢ G"

(* Note that this is not a positive inductive definition because the
predicate occurs negatively in many rules:
inductive ND :: "form ⇒ bool" ("⊢ _" [30] 30) where
NotE: "⟦⊢ Not F; ⊢ F ⟧ ⟹ ⊢ ⊥" |
NotI: "⟦⊢ F ⟹ ⊢ ⊥⟧ ⟹ ⊢ Not F" |
CC: "⟦⊢ Not F ⟹ ⊢ ⊥⟧ ⟹ ⊢ F" |
AndE1: "⊢ And F G ⟹ ⊢ F" |
AndE2: "⊢ And F G ⟹ ⊢ G" |
AndI: "⟦ ⊢ F; ⊢ G ⟧ ⟹ ⊢ And F G" |
OrI1: "⊢ F ⟹ ⊢ Or F G" |
OrI2: "⊢ G ⟹ ⊢ Or F G" |
OrE: "⟦ ⊢ Or F G; ⊢ F ⟹ ⊢ H; ⊢ G ⟹ ⊢ H ⟧ ⟹ ⊢ H" |
ImpI: "⟦⊢ F ⟹ ⊢ G⟧ ⟹ ⊢ Imp F G" |
ImpE: "⟦ ⊢ Imp F G; ⊢ F ⟧ ⟹ ⊢ G"
*)

lemma Weaken: "⟦ Γ ⊢ F; Γ ⊆ Γ' ⟧ ⟹ Γ' ⊢ F"
proof(induct arbitrary: Γ' rule: ND.induct)
  case (NotI F Γ) thus ?case using ND.NotI by auto
next
  case Ax thus ?case by(blast intro: ND.Ax)
next
  case NotE thus ?case by(blast intro: ND.NotE)
next
  case CC thus ?case using ND.CC by blast
next
  case AndE1 thus ?case using ND.AndE1 by metis
next
  case AndE2 thus ?case using ND.AndE2 by metis
next
  case AndI thus ?case by (simp add: ND.AndI)
next
  case OrI1 thus ?case using ND.OrI1 by blast
next
  case OrI2 thus ?case using ND.OrI2 by blast
next
  case (OrE Γ F G H) show ?case apply(insert OrE.prems)
    apply(rule ND.OrE[of Γ' F G]) 
      apply(rule OrE.hyps(2)[OF OrE.prems]) 
     apply(rule OrE.hyps(4); blast)
    apply(rule OrE.hyps(6); blast)
  done
next
  case ImpI thus ?case using ND.ImpI by blast
next
  case ImpE thus ?case using ND.ImpE by metis
qed

lemma BotE (* ex falso *): "Γ ⊢ ⊥ ⟹ Γ ⊢ F"
  by (meson CC subset_insertI Weaken)

lemma Not2E: "Not(Not F)▹ Γ ⊢ F"
  by (metis CC ND.Ax NotE insertI1 insert_commute)

lemma Not2I: "F▹Γ ⊢ Not(Not F)"
  by (metis CC ND.Ax NotE insertI1 insert_commute)

lemma Not2IE: "F▹Γ ⊢ G ⟹ Not (Not F)▹ Γ ⊢ G"
  by (meson ImpE ImpI Not2E Weaken subset_insertI)

lemma NDtrans: "Γ ⊢ F ⟹ F▹ Γ ⊢ G ⟹ Γ ⊢ G"
  using ImpE ImpI by blast

lemma AndL_sim: "F ▹ G ▹ Γ ⊢ H ⟹ And F G ▹ Γ ⊢ H"
  apply(drule Weaken[where Γ' = "And F G ▹ F ▹ G ▹ Γ"])
   apply blast
by (metis AndE1 AndE2 ND.Ax NDtrans insertI1 insert_commute)

lemma NotSwap: "Not F▹ Γ ⊢ G ⟹ Not G▹ Γ ⊢ F"
  using CC NotE insert_commute subset_insertI Weaken by (metis Ax insertI1)
lemma AndR_sim: "⟦ Not F▹ Γ ⊢ H; Not G▹ Γ ⊢ H ⟧ ⟹ Not(And F G)▹ Γ ⊢ H"
  using AndI NotSwap by blast

lemma OrL_sim: "⟦ F▹ Γ ⊢ H; G▹Γ ⊢ H ⟧ ⟹ F ❙∨ G▹ Γ ⊢ H"
  using Weaken[where Γ' = "F▹ Or F G▹ Γ"] Weaken[where Γ' = "G▹ Or F G▹ Γ"]
  by (meson ND.Ax OrE insertI1 insert_mono subset_insertI)

lemma OrR_sim: "⟦ ❙¬ F▹ ❙¬ G▹ Γ ⊢ ⊥⟧ ⟹ ❙¬ (G ❙∨ F)▹ Γ ⊢ ⊥"
proof -
  assume "❙¬ F ▹ ❙¬ G ▹ Γ ⊢ ⊥"
  then have "⋀f. f ▹ ❙¬ F ▹ ❙¬ G ▹ Γ ⊢ ⊥" by (meson Weaken subset_insertI)
  then have "⋀f. ❙¬ G ▹ ❙¬ (f ❙∨ F) ▹ Γ ⊢ ⊥" by (metis NDtrans Not2E NotSwap OrI2 insert_commute)
  then show ?thesis by (meson NDtrans Not2I NotSwap OrI1)
qed

lemma ImpL_sim: "⟦ ❙¬ F▹ Γ ⊢ ⊥; G▹ Γ ⊢ ⊥⟧ ⟹ F ❙→ G▹ Γ ⊢ ⊥"
  by (meson CC ImpE ImpI ND.Ax Weaken insertI1 subset_insertI)

lemma ImpR_sim: "⟦ ❙¬ G▹ F▹ Γ ⊢ ⊥⟧ ⟹ ❙¬ (F ❙→ G)▹ Γ ⊢ ⊥"
  by (metis (full_types) ImpI NotSwap insert_commute)

lemma ND_lem: "{} ⊢ Not F ❙∨ F"
  apply(rule CC)
  apply(rule OrE[of _ "Not F" F])
    apply(rule OrI1)
    apply(rule NotI)
    apply(rule NotE[of _ "(❙¬ F ❙∨ F)"]; blast intro: OrI1 OrI2 Ax)+
done

lemma ND_caseDistinction: "⟦ F▹Γ ⊢ H; Not F▹Γ ⊢ H ⟧ ⟹ Γ ⊢ H"
  by (meson ND_lem OrE empty_subsetI Weaken)

lemma "⟦❙¬ F▹ Γ ⊢ H; G▹ Γ ⊢ H⟧ ⟹ F ❙→ G▹ Γ ⊢ H"
  apply(rule ND_caseDistinction[of F])
   apply (meson ImpE ImpI ND.intros(1) Weaken insertI1 subset_insertI)
  apply (metis Weaken insert_commute subset_insertI)
done

lemma ND_deMorganAnd: "{❙¬ (F ❙∧ G)} ⊢ ❙¬ F ❙∨ ❙¬ G"
  apply(rule CC)
  apply(rule NotE[of _ "F ❙∧ G"])
   apply(simp add: Ax; fail)
  apply(rule AndI)
   apply(rule CC)
   apply(rule NotE[of _ "❙¬ F ❙∨ ❙¬ G"])
    apply(simp add: Ax; fail)
   apply(rule OrI1)
   apply(simp add: Ax; fail)
  apply(rule CC)
   apply(rule NotE[of _ "❙¬ F ❙∨ ❙¬ G"])
   apply(simp add: Ax; fail)
  apply(rule OrI2)
  apply(simp add: Ax; fail)
done

lemma ND_deMorganOr: "{❙¬ (F ❙∨ G)} ⊢ ❙¬ F ❙∧ ❙¬ G" 
  apply(rule ND_caseDistinction[of F]; rule ND_caseDistinction[of G])
     apply(rule CC; rule NotE[of _ "F ❙∨ G"]; simp add: Ax OrI2 OrI1; fail)+
  apply(rule AndI; simp add: Ax; fail)
done

lemma sim_sim: "F▹ Γ ⊢ H ⟹ G▹Γ ⊢ F ⟹ G▹ Γ ⊢ H"
  by (meson ImpE ImpI Weaken subset_insertI)
thm sim_sim[where Γ="{}", rotated, no_vars] (* a bit easier to read? *)
  
lemma Top_provable[simp,intro!]: "Γ ⊢ ⊤" unfolding Top_def by (intro ND.ImpI ND.Ax) simp

lemma NotBot_provable[simp,intro!]: "Γ ⊢ ❙¬ ⊥" using NotI BotE Ax by blast

lemma Top_useless: "Γ ⊢ F ⟹ Γ - {⊤} ⊢ F"
  by (metis NDtrans Top_provable Weaken insert_Diff_single subset_insertI)  

lemma AssmBigAnd: "set G ⊢ F ⟷ {} ⊢ (❙⋀G ❙→ F)"
 proof(induction G arbitrary: F)
    case Nil thus ?case by(fastforce intro: ND.ImpI elim: Weaken ImpE[OF _ NotBot_provable])
  next
    case (Cons G GS) show ?case proof
      assume "set (G # GS) ⊢ F"
      hence "set GS ⊢ G ❙→ F" by(intro ND.ImpI) simp
      with Cons.IH have *: "{} ⊢ ❙⋀ GS ❙→ G ❙→ F" ..
      hence "{G,❙⋀GS} ⊢ F" proof -
        have *: "{❙⋀GS} ⊢ G ❙→ F" 
          using Weaken[OF * empty_subsetI] ImpE[where Γ="{❙⋀ GS}" and F="❙⋀ GS"] by (simp add: ND.Ax)
        show "{G,❙⋀GS} ⊢ F" using Weaken[OF *] ImpE[where Γ="{G,❙⋀ GS}" and F="G"] ND.Ax by (simp add: ND.Ax)
      qed
      thus "{} ⊢ ❙⋀ (G # GS) ❙→ F" by(intro ND.ImpI; simp add: AndL_sim)
    next
      assume "{} ⊢ ❙⋀ (G # GS) ❙→ F"
      hence "{G ❙∧ ❙⋀GS} ⊢ F" using ImpE[OF _ Ax[OF singletonI]] Weaken by fastforce      
      hence "{G,❙⋀GS} ⊢ F" by (meson AndI ImpE ImpI ND.intros(1) Weaken insertI1 subset_insertI)
      hence "{❙⋀GS} ⊢ G ❙→ F" using ImpI by blast
      hence "{} ⊢ ❙⋀ GS ❙→ G ❙→ F" using ImpI by blast
      with Cons.IH have "set GS ⊢ G ❙→ F" ..
      thus "set (G # GS) ⊢ F" using ImpE Weaken by (metis Ax list.set_intros(1) set_subset_Cons)
  qed
qed

end