Theory Sequents

section "Sequents"

theory Sequents
imports Formula
begin 

type_synonym sequent = "formula list"

definition
  evalS :: "[model,vbl ⇒ object,formula list] ⇒ bool" where
  "evalS M φ fs ≡ (∃f ∈ set fs . evalF M φ f = True)"

lemma evalS_nil[simp]: "evalS M φ [] = False"
  by(simp add: evalS_def)

lemma evalS_cons[simp]: "evalS M φ (A # Γ) = (evalF M φ A ∨ evalS M φ Γ)"
  by(simp add: evalS_def)

lemma evalS_append: "evalS M φ (Γ @ Δ) = (evalS M φ Γ ∨ evalS M φ Δ)"
  by(force simp add: evalS_def)

lemma evalS_equiv: "(equalOn (freeVarsFL Γ) f g) ⟹ (evalS M f Γ = evalS M g Γ)"
  by (induction Γ) (auto simp: equalOn_Un evalF_equiv freeVarsFL_cons)


definition
  modelAssigns :: "[model] ⇒ (vbl ⇒ object) set" where
  "modelAssigns M = { φ . range φ ⊆ objects M }"

lemma modelAssigns_iff [simp]: "f ∈ modelAssigns M ⟷ range f ⊆ objects M" 
  by(simp add: modelAssigns_def)
  
definition
  validS :: "formula list ⇒ bool" where
  "validS fs ≡ (∀M. ∀φ ∈ modelAssigns M . evalS M φ fs = True)"


subsection "Rules"

type_synonym rule = "sequent * (sequent set)"

definition
  concR :: "rule ⇒ sequent" where
  "concR = (λ(conc,prems). conc)"

definition
  premsR :: "rule ⇒ sequent set" where
  "premsR = (λ(conc,prems). prems)"

definition
  mapRule :: "(formula ⇒ formula) ⇒ rule ⇒ rule" where
  "mapRule = (λf (conc,prems) . (map f conc,(map f) ` prems))"

lemma mapRuleI: "⟦A = map f a; B = map f ` b⟧ ⟹ (A, B) = mapRule f (a, b)"
  by(simp add: mapRule_def)
    ― ‹FIXME tjr would like symmetric›


subsection "Deductions"

(*FIXME. I don't see why plain Pow_mono is rejected.*)
lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]

inductive_set
  deductions  :: "rule set ⇒ formula list set"
  for rules :: "rule set"
  (******
   * Given a set of rules,
   *   1. Given a rule conc/prem(i) in rules,
   *       and the prem(i) are deductions from rules,
   *       then conc is a deduction from rules.
   *   2. can derive permutation of any deducible formula list.
   *      (supposed to be multisets not lists).
   ******)
  where
    inferI: "⟦(conc,prems) ∈ rules; prems ∈ Pow(deductions(rules))
           ⟧ ⟹ conc ∈ deductions(rules)"
 
lemma mono_deductions: "⟦A ⊆ B⟧ ⟹ deductions(A) ⊆ deductions(B)"
  apply(best intro: deductions.inferI elim: deductions.induct) done
  
(*lemmas deductionsMono = mono_deductions*)

(*
-- "tjr following should be subsetD?"
lemmas deductionSubsetI = mono_deductions[THEN subsetD]
thm deductionSubsetI
*)





subsection "Basic Rule sets"

definition
  "Axioms  = {z. ∃p vs.              z = ([FAtom Pos p vs,FAtom Neg p vs],{}) }"

definition
  "Conjs   = {z. ∃A0 A1 Δ Γ. z = (FConj Pos A0 A1#Γ @ Δ,{A0#Γ,A1#Δ}) }"

definition
  "Disjs   = {z. ∃A0 A1       Γ. z = (FConj Neg A0 A1#Γ,{A0#A1#Γ}) }"

definition
  "Alls    = {z. ∃A x         Γ. z = (FAll Pos A#Γ,{instanceF x A#Γ}) ∧ x ∉ freeVarsFL (FAll Pos A#Γ) }"

definition
  "Exs     = {z. ∃A x         Γ. z = (FAll Neg A#Γ,{instanceF x A#Γ})}"

definition
  "Weaks   = {z. ∃A           Γ. z = (A#Γ,{Γ})}"

definition
  "Contrs  = {z. ∃A           Γ. z = (A#Γ,{A#A#Γ})}"

definition
  "Cuts    = {z. ∃C Δ     Γ. z = (Γ @ Δ,{C#Γ,FNot C#Δ})}"

definition
  "Perms   = {z. ∃Γ Δ     . z = (Γ,{Δ}) ∧ mset Γ = mset Δ}"

definition
  "DAxioms = {z. ∃p vs.              z = ([FAtom Neg p vs,FAtom Pos p vs],{}) }"


lemma AxiomI: "⟦Axioms ⊆ A⟧ ⟹ [FAtom Pos p vs,FAtom Neg p vs] ∈ deductions(A)"
  by (auto simp: Axioms_def deductions.simps)

lemma DAxiomsI: "⟦DAxioms ⊆ A⟧ ⟹ [FAtom Neg p vs,FAtom Pos p vs] ∈ deductions(A)"
  by (auto simp: DAxioms_def deductions.simps)

lemma DisjI: "⟦A0#A1#Γ ∈ deductions(A); Disjs ⊆ A⟧ ⟹ (FConj Neg A0 A1#Γ) ∈ deductions(A)"
  by (force simp: Disjs_def deductions.simps)

lemma ConjI: "⟦(A0#Γ) ∈ deductions(A); (A1#Δ) ∈ deductions(A); Conjs ⊆ A⟧ ⟹ FConj Pos A0 A1#Γ @ Δ ∈ deductions(A)"
  by (force simp: Conjs_def deductions.simps)

lemma AllI: "⟦instanceF w A#Γ ∈ deductions(R); w ∉ freeVarsFL (FAll Pos A#Γ); Alls ⊆ R⟧ ⟹ (FAll Pos A#Γ) ∈ deductions(R)"
  by (force simp: Alls_def deductions.simps)

lemma ExI: "⟦instanceF w A#Γ ∈ deductions(R); Exs ⊆ R⟧ ⟹ (FAll Neg A#Γ) ∈ deductions(R)"
  by (force simp: Exs_def deductions.simps)

lemma WeakI: "⟦Γ ∈ deductions R; Weaks ⊆ R⟧ ⟹ A#Γ ∈ deductions(R)"
  by (force simp: Weaks_def deductions.simps)

lemma ContrI: "⟦A#A#Γ ∈ deductions R; Contrs ⊆ R⟧ ⟹ A#Γ ∈ deductions(R)"
  by (force simp: Contrs_def deductions.simps)

lemma PermI: "⟦Gamma' ∈ deductions R; mset Γ = mset Gamma'; Perms ⊆ R⟧ ⟹ Γ ∈ deductions(R)"
  using deductions.inferI [where prems="{Gamma'}"] Perms_def by blast


subsection "Derived Rules"

lemma WeakI1: "⟦Γ ∈ deductions(A); Weaks ⊆ A⟧ ⟹ (Δ @ Γ) ∈ deductions(A)"
  by (induct Δ) (use WeakI in force)+

lemma WeakI2: "⟦Γ ∈ deductions(A); Perms ⊆ A; Weaks ⊆ A⟧ ⟹ (Γ @ Δ) ∈ deductions(A)"
  by (metis PermI WeakI1 mset_append union_commute)

lemma SATAxiomI: "⟦Axioms ⊆ A; Weaks ⊆ A; Perms ⊆ A; forms = [FAtom Pos n vs,FAtom Neg n vs] @ Γ⟧ ⟹ forms ∈ deductions(A)"
  using AxiomI WeakI2 by presburger
    
lemma DisjI1: "⟦(A1#Γ) ∈ deductions(A); Disjs ⊆ A; Weaks ⊆ A⟧ ⟹ FConj Neg A0 A1#Γ ∈ deductions(A)"
  using DisjI WeakI by presburger

lemma DisjI2: "⟦(A0#Γ) ∈ deductions(A); Disjs ⊆ A; Weaks ⊆ A; Perms ⊆ A⟧ ⟹ FConj Neg A0 A1#Γ ∈ deductions(A)"
  using PermI [of ‹A1 # A0 # Γ›]
  by (metis DisjI WeakI append_Cons mset_append mset_rev rev.simps(2))

    ― ‹FIXME the following 4 lemmas could all be proved for the standard rule sets using monotonicity as below›
    ― ‹we keep proofs as in original, but they are slightly ugly, and do not state what is intuitively happening›
lemma perm_tmp4: "Perms ⊆ R ⟹ A @ (a # list) @ (a # list) ∈ deductions R ⟹ (a # a # A) @ list @ list ∈ deductions R"
  by (rule PermI, auto)

lemma weaken_append:
  "Contrs ⊆ R ⟹ Perms ⊆ R ⟹ A @ Γ @ Γ ∈ deductions(R) ⟹ A @ Γ ∈ deductions(R)"
proof (induction Γ arbitrary: A)
  case Nil
  then show ?case
    by auto
next
  case (Cons a Γ)
  then have "(a # a # A) @ Γ ∈ deductions R"
    using perm_tmp4 by blast
  then have "a # A @ Γ ∈ deductions R"
    by (metis Cons.prems(1) ContrI append_Cons)
  then show ?case
    using Cons.prems(2) PermI by force
qed

lemma ListWeakI: "Perms ⊆ R ⟹ Contrs ⊆ R ⟹ x # Γ @ Γ ∈ deductions(R) ⟹ x # Γ ∈ deductions(R)"
  by (metis append.left_neutral append_Cons weaken_append)
    
lemma ConjI': "⟦(A0#Γ) ∈ deductions(A);  (A1#Γ) ∈ deductions(A); Contrs ⊆ A; Conjs ⊆ A; Perms ⊆ A⟧ ⟹ FConj Pos A0 A1#Γ ∈ deductions(A)"
  by (metis ConjI ListWeakI)


subsection "Standard Rule Sets For Predicate Calculus"

definition
  PC :: "rule set" where
  "PC = Union {Perms,Axioms,Conjs,Disjs,Alls,Exs,Weaks,Contrs,Cuts}"

definition
  CutFreePC :: "rule set" where
  "CutFreePC = Union {Perms,Axioms,Conjs,Disjs,Alls,Exs,Weaks,Contrs}"

lemma rulesInPCs: "Axioms ⊆ PC" "Axioms ⊆ CutFreePC"
  "Conjs  ⊆ PC" "Conjs  ⊆ CutFreePC"
  "Disjs  ⊆ PC" "Disjs  ⊆ CutFreePC"
  "Alls   ⊆ PC" "Alls   ⊆ CutFreePC"
  "Exs    ⊆ PC" "Exs    ⊆ CutFreePC"
  "Weaks  ⊆ PC" "Weaks  ⊆ CutFreePC"
  "Contrs ⊆ PC" "Contrs ⊆ CutFreePC"
  "Perms  ⊆ PC" "Perms  ⊆ CutFreePC"
  "Cuts   ⊆ PC"
  "CutFreePC ⊆ PC"
  by(auto simp: PC_def CutFreePC_def)


subsection "Monotonicity for CutFreePC deductions"

  ― ‹these lemmas can be used to replace complicated permutation reasoning above›
  ― ‹essentially if x is a deduction, and set x subset set y, then y is a deduction›

definition
  inDed :: "formula list ⇒ bool" where
  "inDed xs ≡ xs ∈ deductions CutFreePC"

lemma perm: "mset xs = mset ys ⟹ (inDed xs = inDed ys)"
  by (metis PermI inDed_def rulesInPCs(16))

lemma contr: "inDed (x#x#xs) ⟹ inDed (x#xs)"
  using ContrI inDed_def rulesInPCs(14) by blast

lemma weak: "inDed xs ⟹ inDed (x#xs)"
  by (simp add: WeakI inDed_def rulesInPCs(12))

lemma inDed_mono'[simplified inDed_def]: "set x ⊆ set y ⟹ inDed x ⟹ inDed y"
  using contr perm perm_weak_contr_mono weak by blast

lemma inDed_mono[simplified inDed_def]: "inDed x ⟹ set x ⊆ set y ⟹ inDed y"
  using inDed_def inDed_mono' by auto

end