Theory SC

section‹Proof Systems›
subsection‹Sequent Calculus›

theory SC
imports Formulas "HOL-Library.Multiset"
begin

abbreviation msins ("_, _" [56,56] 56) where "x,M == add_mset x M"  

text‹We do not formalize the concept of sequents, only that of sequent calculus derivations.›
inductive SCp :: "'a formula multiset ⇒ 'a formula multiset ⇒ bool" ("(_ ⇒/ _)" [53] 53) where
BotL: "⊥ ∈# Γ ⟹ Γ⇒Δ" |
Ax: "Atom k ∈# Γ ⟹ Atom k ∈# Δ ⟹ Γ⇒Δ" |
NotL: "Γ ⇒ F,Δ ⟹ Not F, Γ ⇒ Δ" |
NotR: "F,Γ ⇒ Δ ⟹ Γ ⇒ Not F, Δ" |
AndL: "F,G,Γ ⇒ Δ ⟹ And F G, Γ ⇒ Δ" |
AndR: "⟦ Γ ⇒ F,Δ; Γ ⇒ G,Δ ⟧ ⟹ Γ ⇒ And F G, Δ" |
OrL: "⟦ F,Γ ⇒ Δ; G,Γ ⇒ Δ ⟧ ⟹ Or F G, Γ ⇒ Δ" |
OrR: "Γ ⇒ F,G,Δ ⟹ Γ ⇒ Or F G, Δ" |
ImpL: "⟦ Γ ⇒ F,Δ; G,Γ ⇒ Δ ⟧ ⟹ Imp F G, Γ ⇒ Δ" |
ImpR: "F,Γ ⇒ G,Δ ⟹ Γ ⇒ Imp F G, Δ"

text‹Many of the proofs here are inspired Troelstra and Schwichtenberg~\<^cite>‹"troelstra2000basic"›.›

lemma
  shows BotL_canonical[intro!]: "⊥,Γ⇒Δ"
    and Ax_canonical[intro!]: "Atom k,Γ ⇒ Atom k,Δ"
  by (meson SCp.intros union_single_eq_member)+
    

lemma lem1: "x ≠ y ⟹ x, M = y,N ⟷ x ∈# N ∧ M = y,(N - {#x#})"
  by (metis (no_types, lifting) add_eq_conv_ex add_mset_remove_trivial add_mset_remove_trivial_eq)

lemma lem2: "x ≠ y ⟹ x, M = y, N ⟷ y ∈# M ∧ N = x, (M - {#y#})"
  using lem1 by fastforce

text‹This is here to deal with a technical problem: the way the simplifier uses @{thm add_mset_commute} is really suboptimal for the unification of SC rules.›
  
lemma sc_insertion_ordering[simp]:
  "NO_MATCH (I❙→J) H ⟹ H,F❙→G,S = F❙→G,H,S"
  "NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ H,F❙∨G,S = F❙∨G,H,S"
  "NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ H,F❙∧G,S = F❙∧G,H,S"
  "NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ NO_MATCH (❙¬J) H ⟹ H,❙¬G,S = ❙¬G,H,S"
  "NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ NO_MATCH (❙¬J) H ⟹ NO_MATCH (⊥) H ⟹ H,⊥,S = ⊥,H,S"
  "NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ NO_MATCH (❙¬J) H ⟹ NO_MATCH (⊥) H ⟹ NO_MATCH (Atom k) H ⟹ H,Atom l,S = Atom l,H,S"
  (* I have decided that ⊥ and atoms should be pulled outwards with the lowest priorities. this may not always be smart. *)
  by simp_all
    
lemma shows
     inR1: "Γ ⇒ G, H, Δ ⟹ Γ ⇒ H, G, Δ"
 and inL1: "G, H, Γ ⇒ Δ ⟹ H, G, Γ ⇒ Δ"
 and inR2: "Γ ⇒ F, G, H, Δ ⟹ Γ ⇒ G, H, F, Δ"
 and inL2: "F, G, H, Γ ⇒ Δ ⟹ G, H, F, Γ ⇒ Δ" by(simp_all add: add_mset_commute)
lemmas SCp_swap_applies[elim!,intro] = inL1 inL2 inR1 inR2

lemma NotL_inv: "Not F, Γ ⇒ Δ ⟹ Γ ⇒ F,Δ"
proof(induction "Not F, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (NotL Γ' G Δ) thus ?case by(cases "Not F = Not G") (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2)
qed (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)

lemma AndL_inv: "And F G, Γ ⇒ Δ ⟹ F,G,Γ ⇒ Δ"
proof(induction "And F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (AndL F' G' Γ' Δ) thus ?case 
    by(cases "And F G = And F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2 inL2)

lemma OrL_inv: 
  assumes "Or F G, Γ ⇒ Δ"
  shows "F,Γ ⇒ Δ ∧ G,Γ ⇒ Δ"
proof(insert assms, induction "Or F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (OrL F' Γ' Δ G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma ImpL_inv: 
  assumes "Imp F G, Γ ⇒ Δ"
  shows "Γ ⇒ F,Δ ∧ G,Γ ⇒ Δ"
proof(insert assms, induction "Imp F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (ImpL Γ' F' Δ G') thus ?case 
    by(cases "Or F G = Or F' G'"; (* oops, I didn't pay attention and used the wrong constructor… doesn't matter! *)
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+
  
lemma ImpR_inv:
  assumes "Γ ⇒ Imp F G,Δ"
  shows "F,Γ ⇒ G,Δ"
proof(insert assms, induction Γ "Imp F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (ImpR  F' Γ G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma AndR_inv:
shows "Γ ⇒ And F G, Δ ⟹ Γ ⇒ F, Δ ∧ Γ ⇒ G, Δ"
proof(induction Γ "And F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (AndR  Γ F' Δ' G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma OrR_inv: "Γ ⇒ Or F G, Δ ⟹ Γ ⇒ F,G,Δ"
proof(induction Γ "Or F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (OrR  Γ F' G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma NotR_inv: "Γ ⇒ Not F, Δ ⟹ F,Γ ⇒ Δ"
proof(induction Γ "Not F, Δ" arbitrary: Δ rule: SCp.induct)
  case (NotR  G Γ Δ') thus ?case 
    by(cases "Not F = Not G"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma weakenL: "Γ ⇒ Δ ⟹ F,Γ ⇒ Δ"
  by(induction rule: SCp.induct) 
    (auto intro!: SCp.intros(3-) intro: SCp.intros(1,2))

lemma weakenR: "Γ ⇒ Δ ⟹ Γ ⇒ F,Δ "
  by(induction rule: SCp.induct)
    (auto intro!: SCp.intros(3-) intro: SCp.intros(1,2))

lemma weakenL_set: "Γ ⇒ Δ ⟹ F + Γ ⇒ Δ"
  by(induction F; simp add: weakenL) 
lemma weakenR_set: "Γ ⇒ Δ ⟹ Γ ⇒ F + Δ"
  by(induction F; simp add: weakenR)

lemma extended_Ax: "Γ ∩# Δ ≠ {#} ⟹ Γ ⇒ Δ"
proof -
  assume "Γ ∩# Δ ≠ {#}"
  then obtain W where "W ∈# Γ" "W ∈# Δ" by force
  then show ?thesis proof(induction W arbitrary: Γ Δ)
    case (Not W)
    from Not.prems obtain Γ' Δ' where [simp]: "Γ = Not W,Γ'" "Δ = Not W,Δ'" by (metis insert_DiffM)
    have "W ∈# W,Γ'" "W ∈# W,Δ'" by simp_all
    from Not.IH[OF this] obtain n where "W, Γ' ⇒ W, Δ'" by presburger
    hence "Not W, Γ' ⇒ Not W, Δ'" using SCp.intros(3,4) add_mset_commute by metis
    thus "Γ ⇒ Δ" by auto
  next
    case (And G H)
    from And.prems obtain Γ' Δ' where [simp]: "Γ = And G H,Γ'" "Δ = And G H,Δ'" by (metis insert_DiffM)
    have "G ∈# G, H, Γ'" "G ∈# G, Δ'" by simp_all
    with And.IH(1) have IH1: "G, H, Γ' ⇒ G, Δ'" .
    have "H ∈# G, H, Γ'" "H ∈# H, Δ'" by simp_all
    with And.IH(2) have IH2: "G, H, Γ' ⇒ H, Δ'" .
    from IH1 IH2 have "G, H, Γ' ⇒ G, Δ'" "G, H, Γ' ⇒ H, Δ'" by fast+
    thus "Γ ⇒ Δ" using SCp.intros(5,6) by fastforce
  next
    case (Or G H)
    case (Imp G H)
    text‹analogously› (*<*)
  next
    case (Or G H)
    from Or.prems obtain Γ' Δ' where [simp]: "Γ = Or G H,Γ'" "Δ = Or G H,Δ'" by (metis insert_DiffM)
    with Or.IH show ?case using SCp.intros(7,8)[where 'a='a] by fastforce
  next
    case (Imp G H)
    from Imp.prems obtain Γ' Δ' where [simp]: "Γ = Imp G H,Γ'" "Δ = Imp G H,Δ'" by (metis insert_DiffM)
    from Imp.IH have "G, Γ' ⇒ G, H, Δ'" "H, G, Γ' ⇒ H, Δ'" by simp_all
    thus ?case by(auto intro!: SCp.intros(3-))
  (*>*)
  qed (auto intro: SCp.intros)
qed

lemma Bot_delR: "Γ ⇒ Δ ⟹ Γ ⇒ Δ-{#⊥#}"
proof(induction rule: SCp.induct)
  case BotL
  thus ?case by (simp add: SCp.BotL)
next
  case Ax
  thus ?case
    by (metis SCp.Ax diff_union_swap formula.distinct(1) insert_DiffM union_single_eq_member)
next
  case NotL
  thus ?case
    by (metis SCp.NotL diff_single_trivial diff_union_swap2)
next
  case NotR
  thus ?case by(simp add: SCp.NotR)
next
  case AndL
  thus ?case by (simp add: SCp.AndL)
next
  case AndR
  thus ?case
    by (metis SCp.AndR diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(13))
next
  case OrL
  thus ?case by(simp add: SCp.OrL)
next
  case OrR
  thus ?case
    by (metis SCp.OrR diff_single_trivial diff_union_swap2 formula.distinct(15) insert_iff set_mset_add_mset_insert)
next
  case ImpL
  thus ?case by (metis SCp.ImpL diff_single_trivial diff_union_swap2)
next
  case ImpR
  thus ?case
    by (metis SCp.ImpR diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(17))
qed
corollary Bot_delR_simp: "Γ ⇒ ⊥,Δ = Γ ⇒ Δ"
  using Bot_delR weakenR by fastforce

end