Theory Implicational_Logic_Natural_Deduction

theory Implicational_Logic_Natural_Deduction imports Main begin

datatype form =
  Pro nat (‹⋅›) |
  Imp form form (infixr ‹→› 100)

primrec semantics (infix ‹⊨› 50) where
  ‹I ⊨ ⋅n = I n› |
  ‹I ⊨ p → q = (I ⊨ p ⟶ I ⊨ q)›

inductive Calculus (infix ‹↝› 50) where
  Assm: ‹p ∈ set A ⟹ A ↝ p› |
  ImpI: ‹p # A ↝ q ⟹ A ↝ p → q› |
  ImpE: ‹A ↝ p → q ⟹ A ↝ p ⟹ A ↝ q› |
  ImpC: ‹p → _ # A ↝ p ⟹ A ↝ p›

abbreviation natural_deduction (‹⊢ _› [100] 100) where ‹⊢ p ≡ [] ↝ p›

theorem soundness: ‹A ↝ p ⟹ ∀p ∈ set A. I ⊨ p ⟹ I ⊨ p›
  by (induct rule: Calculus.induct) auto

lemma weaken': ‹A ↝ p ⟹ set A = set B ⟹ B ↝ p›
proof (induct arbitrary: B rule: Calculus.induct)
  case ImpC
  with Calculus.ImpC show ?case
    using list.set(2) by metis
qed (auto intro: Calculus.intros)

lemma weak: ‹A ↝ p ⟹ q # A ↝ p›
proof (induct rule: Calculus.induct)
  case ImpI
  with Calculus.ImpI show ?case
    using insert_commute list.set(2) weaken' by (metis (full_types))
next
  case ImpC
  with Calculus.ImpC show ?case
    using insert_commute list.set(2) weaken' by (metis (full_types))
qed (auto intro: Calculus.intros)

lemma add_assumptions: ‹⊢ p ⟹ A ↝ p›
  by (induct A) (simp_all add: weak)

lemma weaken: ‹A ↝ p ⟹ set A ⊆ set B ⟹ B ↝ p›
proof (induct A arbitrary: p)
  case (Cons q A)
  moreover from this have ‹A ↝ q → p› and ‹set A ⊆ set B› and ‹B ↝ q›
    by (simp_all add: Assm ImpI)
  ultimately show ?case
    using ImpE by blast
qed (simp add: add_assumptions)

lemma deduct: ‹A ↝ p → q ⟹ p # A ↝ q›
  using Assm ImpE list.set_intros(1) weak by meson

lemma Peirce: ‹⊢ ((p → q) → p) → p›
  using Assm ImpC ImpI deduct list.set_intros(1) by meson

lemma Simp: ‹⊢ p → q → p›
  by (simp add: Assm ImpI)

lemma Tran: ‹⊢ (p → q) → (q → r) → p → r›
proof -
  have ‹[p, q → r, p → q] ↝ r›
    using Assm ImpE list.set_intros(1) weak by meson
  then show ?thesis
    using ImpI by blast
qed

lemma Swap: ‹⊢ (p → q → r) → q → p → r›
proof -
  have ‹[p, q, p → q → r] ↝ r›
    using Assm ImpE list.set_intros(1) weak by meson
  then show ?thesis
    using ImpI by blast
qed

lemma Tran': ‹⊢ (q → r) → (p → q) → p → r›
  using ImpE Swap Tran .

lemma Imp1: ‹⊢ (q → s) → ((q → r) → s) → s›
  using ImpE Peirce Tran Tran' by meson

lemma Imp2: ‹⊢ ((r → s) → s) → ((q → r) → s) → s›
  using ImpE Tran ImpE Tran Simp .

lemma Imp3: ‹⊢ ((q → s) → s) → (r → s) → (q → r) → s›
  using ImpE Tran Tran' by meson

fun pros where
  ‹pros (p → q) = remdups (pros p @ pros q)› |
  ‹pros p = (case p of ⋅n ⇒ [n] | _ ⇒ [])›

lemma distinct_pros: ‹distinct (pros p)›
  by induct simp_all

abbreviation ‹lift t s p ≡ if t then (p → s) → s else p → s›

abbreviation ‹lifts I s ≡ map (λn. lift (I n) s (⋅n))›

lemma lifts_weaken: ‹lifts I s l ↝ p ⟹ set l ⊆ set l' ⟹ lifts I s l' ↝ p›
proof -
  assume ‹lifts I s l ↝ p›
  moreover assume ‹set l ⊆ set l'›
  then have ‹set ((lifts I s) l) ⊆ set ((lifts I s) l')›
    by auto
  ultimately show ?thesis
    using weaken by blast
qed

lemma lifts_pros_lift: ‹lifts I s (pros p) ↝ lift (I ⊨ p) s p›
proof (induct p)
  case (Imp q r)
  consider ‹¬ I ⊨ q› | ‹I ⊨ r› | ‹I ⊨ q› and ‹¬ I ⊨ r›
    by blast
  then show ?case
  proof cases
    case 1
    then have ‹lifts I s (pros (q → r)) ↝ q → s›
      using Imp(1) lifts_weaken[where l' = ‹pros (q → r)›] by simp
    then have ‹lifts I s (pros (q → r)) ↝ ((q → r) → s) → s›
      using Imp1 ImpE add_assumptions by blast
    with 1 show ?thesis
      by simp
  next
    case 2
    then have ‹lifts I s (pros (q → r)) ↝ (r → s) → s›
      using Imp(2) lifts_weaken[where l' = ‹pros (q → r)›] by simp
    then have ‹lifts I s (pros (q → r)) ↝ ((q → r) → s) → s›
      using Imp2 ImpE add_assumptions by blast
    with 2 show ?thesis
      by simp
  next
    case 3
    then have
      ‹lifts I s (pros (q → r)) ↝ (q → s) → s›
      ‹lifts I s (pros (q → r)) ↝ r → s›
      using Imp lifts_weaken[where l' = ‹pros (q → r)›] by simp_all
    then have ‹lifts I s (pros (q → r)) ↝ (q → r) → s›
      using Imp3 ImpE add_assumptions by blast
    with 3 show ?thesis
      by simp
  qed
qed (simp add: Assm)

lemma lifts_pros: ‹I ⊨ p ⟹ lifts I p (pros p) ↝ p›
proof -
  assume ‹I ⊨ p›
  then have ‹lifts I p (pros p) ↝ (p → p) → p›
    using lifts_pros_lift[of I p p] by simp
  then show ?thesis
    using ImpC deduct by blast
qed

theorem completeness: ‹∀I. I ⊨ p ⟹ ⊢ p›
proof -
  let ?A = ‹λl I. lifts I p l ↝ p›
  let ?B = ‹λl. ∀I. ?A l I ∧ distinct l›
  assume ‹∀I. I ⊨ p›
  moreover have ‹?B l ⟹ (⋀n l. ?B (n # l) ⟹ ?B l) ⟹ ?B []› for l
    by (induct l) blast+
  moreover have ‹?B (n # l) ⟹ ?B l› for n l
  proof -
    assume *: ‹?B (n # l)›
    show ‹?B l›
    proof
      fix I
      from * have
        ‹?A (n # l) (I(n := True))›
        ‹?A (n # l) (I(n := False))›
        by blast+
      moreover from * have ‹∀m ∈ set l. ∀t. (I(n := t)) m = I m›
        by simp
      ultimately have
        ‹((⋅n → p) → p) # lifts I p l ↝ p›
        ‹(⋅n → p) # lifts I p l ↝ p›
        by (simp_all cong: map_cong)
      then have ‹?A l I›
        using ImpE ImpI by blast
      moreover from * have ‹distinct (n # l)›
        by blast
      ultimately show ‹?A l I ∧ distinct l›
        by simp
    qed
  qed
  ultimately have ‹?B []›
    using lifts_pros distinct_pros by blast
  then show ?thesis
    by simp
qed

primrec chain where
  ‹chain p [] = p› |
  ‹chain p (q # A) = q → chain p A›

lemma chain_rev: ‹B ↝ chain p A ⟹ rev A @ B ↝ p›
  by (induct A arbitrary: B) (simp_all add: deduct)

lemma chain_deduct: ‹⊢ chain p A ⟹ A ↝ p›
proof (induct A)
  case (Cons q A)
  then have ‹rev (q # A) @ [] ↝ p›
    using chain_rev by blast
  moreover have ‹set (rev (q # A) @ []) = set (q # A)›
    by simp
  ultimately show ?case
    using weaken by blast
qed simp

lemma chain_semantics: ‹I ⊨ chain p A = ((∀p ∈ set A. I ⊨ p) ⟶ I ⊨ p)›
  by (induct A) auto

theorem main: ‹A ↝ p = (∀I. (∀p ∈ set A. I ⊨ p) ⟶ I ⊨ p)›
  using chain_deduct chain_semantics completeness soundness by meson

end