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