Theory Implicational_Logic_Sequent_Calculus

theory Implicational_Logic_Sequent_Calculus 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)›

abbreviation sc (‹⟦_⟧›) where ‹⟦I⟧ X Y ≡ (∀p ∈ set X. I ⊨ p) ⟶ (∃q ∈ set Y. I ⊨ q)›

inductive SC (infix ‹⪢› 50) where
  Imp_L: ‹p → q # X ⪢ Y› if ‹X ⪢ p # Y› and ‹q # X ⪢ Y› |
  Imp_R: ‹X ⪢ p → q # Y› if ‹p # X ⪢ q # Y› |
  Set_L: ‹X' ⪢ Y› if ‹X ⪢ Y› and ‹set X' = set X› |
  Set_R: ‹X ⪢ Y'› if ‹X ⪢ Y› and ‹set Y' = set Y› |
  Basic: ‹p # _ ⪢ p # _›

function mp where
  ‹mp A B (p → q # C) [] = (mp A B C [p] ∧ mp A B (q # C) [])› |
  ‹mp A B C (p → q # D) = mp A B (p # C) (q # D)› |
  ‹mp A B [] [] = (set A ∩ set B ≠ {})› |
  ‹mp A B (⋅n # C) [] = mp (n # A) B C []› |
  ‹mp A B C (⋅n # D) = mp A (n # B) C D›
  by pat_completeness simp_all

termination
  by (relation ‹measure (λ(_, _, C, D). 2 * (∑p ← C @ D. size p) + size (C @ D))›) simp_all

lemma main: ‹(∀I. ⟦I⟧ (map ⋅ A @ C) (map ⋅ B @ D)) ⟷ mp A B C D›
  by (induct rule: mp.induct) (auto 5 2)

definition prover (‹⊢›) where ‹⊢ p ≡ mp [] [] [] [p]›

theorem prover_correct: ‹⊢ p ⟷ (∀I. I ⊨ p)›
  unfolding prover_def by (simp flip: main)

export_code ⊢ in SML

lemma MP: ‹mp A B C D ⟹ set X ⊇ set (map ⋅ A @ C) ⟹ set Y ⊇ set (map ⋅ B @ D) ⟹ X ⪢ Y›
proof (induct A B C D arbitrary: X Y rule: mp.induct[case_names Imp_L Imp_R Basic])
  case (Imp_L A B p q C)
  have
    ‹set (map ⋅ A @ C) ⊆ set X›
    ‹set (map ⋅ B) ⊆ set Y›
    using Imp_L(4,5) by auto
  moreover from this have
    ‹set (map ⋅ A @ C) ⊆ set (q # X)›
    ‹set (map ⋅ B) ⊆ set (p # Y)›
    by auto
  ultimately have ‹p → q # X ⪢ Y›
    using Imp_L(1-3) SC.Imp_L by simp
  then show ?case
    using Imp_L(4) Set_L by fastforce
next
  case (Imp_R A B C p q D)
  have
    ‹set (map ⋅ A @ C) ⊆ set (p # X)›
    ‹set (map ⋅ B @ D) ⊆ set (q # Y)›
    using Imp_R(3,4) by auto
  then have ‹X ⪢ p → q # Y›
    using Imp_R(1,2) SC.Imp_R by simp
  then show ?case
    using Imp_R(4) Set_R by fastforce
next
  case (Basic A B)
  obtain n where
    ‹n ∈ set A›
    ‹n ∈ set B›
    using Basic(1) by auto
  then have
    ‹set (⋅n # X) = set X›
    ‹set (⋅n # Y) = set Y›
    using Basic(2,3) by auto
  then show ?case
    using Set_L Set_R SC.Basic by metis
qed simp_all

theorem OK: ‹(∀I. ⟦I⟧ X Y) ⟷ X ⪢ Y›
  by (rule, use MP main[of ‹[]› _ ‹[]› _] in simp, induct rule: SC.induct) auto

corollary ‹[] ⪢ [p] ⟷ (∀I. I ⊨ p)›
  using OK by force

proposition ‹[] ⪢ [p → p]›
proof -
  from Imp_R have ?thesis if ‹[p] ⪢ [p]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [p → (p → q) → q]›
proof -
  from Imp_R have ?thesis if ‹[p] ⪢ [(p → q) → q]›
    using that by force
  with Imp_R have ?thesis if ‹[p → q, p] ⪢ [q]›
    using that by force
  with Imp_L have ?thesis if ‹[p] ⪢ [p, q]› and ‹[q, p] ⪢ [q]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [p → q → q → p]›
proof -
  from Imp_R have ?thesis if ‹[p] ⪢ [q → q → p]›
    using that by force
  with Imp_R have ?thesis if ‹[q, p] ⪢ [q → p]›
    using that by force
  with Imp_R have ?thesis if ‹[q, q, p] ⪢ [p]›
    using that by force
  with Set_L have ?thesis if ‹[p, q] ⪢ [p]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [(p → q) → p → q]›
proof -
  from Imp_R have ?thesis if ‹[p → q] ⪢ [p → q]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [p → p → q → q]›
proof -
  from Imp_R have ?thesis if ‹[p] ⪢ [p → q → q]›
    using that by force
  with Imp_R have ?thesis if ‹[p, p] ⪢ [q → q]›
    using that by force
  with Imp_R have ?thesis if ‹[q, p, p] ⪢ [q]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [(p → p → q) → p → q]›
proof -
  from Imp_R have ?thesis if ‹[p → p → q] ⪢ [p → q]›
    using that by force
  with Imp_R have ?thesis if ‹[p, p → p → q] ⪢ [q]›
    using that by force
  with Set_L have ?thesis if ‹[p → p → q, p] ⪢ [q]›
    using that by force
  with Imp_L have ?thesis if ‹[p] ⪢ [p, q]› and ‹[p → q, p] ⪢ [q]›
    using that by force
  with Imp_L have ?thesis if ‹[p] ⪢ [p, q]› and ‹[q, p] ⪢ [q]› and ‹[p] ⪢ [p, q]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [p → q → p]›
proof -
  from Imp_R have ?thesis if ‹[p] ⪢ [q → p]›
    using that by force
  with Imp_R have ?thesis if ‹[q, p] ⪢ [p]›
    using that by force
  with Set_L have ?thesis if ‹[p, q] ⪢ [p]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [(p → r) → (r → q) → p → q]›
proof -
  from Imp_R have ?thesis if ‹[p → r] ⪢ [(r → q) → p → q]›
    using that by force
  with Imp_R have ?thesis if ‹[r → q, p → r] ⪢ [p → q]›
    using that by force
  with Imp_R have ?thesis if ‹[p, r → q, p → r] ⪢ [q]›
    using that by force
  with Set_L have ?thesis if ‹[r → q, p → r, p] ⪢ [q]›
    using that by force
  with Imp_L have ?thesis if ‹[p → r, p] ⪢ [r, q]› and ‹[q, p → r, p] ⪢ [q]›
    using that by force
  with Basic have ?thesis if ‹[p → r, p] ⪢ [r, q]›
    using that by force
  with Imp_L have ?thesis if ‹[p] ⪢ [p, r, q]› and ‹[r, p] ⪢ [r, q]›
    using that by force
  with Basic show ?thesis
    by force
qed

proposition ‹[] ⪢ [((p → q) → p) → p]›
proof -
  from Imp_R have ?thesis if ‹[(p → q) → p] ⪢ [p]›
    using that by force
  with Imp_L have ?thesis if ‹[] ⪢ [p → q, p]› and ‹[p] ⪢ [p]›
    using that by force
  with Basic have ?thesis if ‹[] ⪢ [p → q, p]›
    using that by force
  with Imp_R have ?thesis if ‹[p] ⪢ [q, p]›
    using that by force
  with Set_R have ?thesis if ‹[p] ⪢ [p, q]›
    using that by force
  with Basic show ?thesis
    by force
qed

end