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 phi fs ⟷ (? f : set fs . evalF M phi f = True)"

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

lemma evalS_cons[simp]: "evalS M phi (A # Gamma) = (evalF M phi A | evalS M phi Gamma)"
  by(simp add: evalS_def)

lemma evalS_append: "evalS M phi (Gamma @ Delta) = (evalS M phi Gamma | evalS M phi Delta)"
  by(force simp add: evalS_def)

lemma evalS_equiv[rule_format]: "(equalOn (freeVarsFL Gamma) f g) --> (evalS M f Gamma = evalS M g Gamma)"
  apply (induct Gamma, simp, rule)
  apply(simp add: freeVarsFL_cons)
  apply(drule_tac equalOn_UnD)
  apply(blast dest: evalF_equiv)
  done


definition
  modelAssigns :: "[model] => (vbl => object) set" where
  "modelAssigns M = { phi . range phi <= objects M }"

lemma modelAssignsI: "range f <= objects M ⟹ f : modelAssigns M" 
  by(simp add: modelAssigns_def)

lemma modelAssignsD: "f : modelAssigns M ⟹ range f <= objects M" 
  by(simp add: modelAssigns_def)
  
definition
  validS :: "formula list => bool" where
  "validS fs ⟷ (! M . ! phi : modelAssigns M . evalS M phi 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)"
(*
    perms   "[| permutation conc' conc;
                conc' : 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
*)

(******
 * (f : formula -> formula) extended structurally over rules, deductions etc...
 * (((If f maps rules into themselves then can consider mapping derivation trees.)))
 * (((Is the asm necessary - think not?)))
 * The mapped deductions from the rules are same as
 * the deductions from the mapped rules.
 *
 * WHY:
 *
 * map f `` deductions rules <= deductions (mapRule f `` rules)     (this thm)
 *                           <= deductions rules                    (closed)
 *
 * If rules are closed under f then so are deductions.
 * Can take f = (subst u v) and have application to exercise #1.
 *
 * Q: maybe also make f dual mapping, (what about quantifier side conditions...?).
 ******)

(*
lemma map_deductions: "map f ` deductions rules <= deductions (mapRule f ` rules)"
  apply(rule subsetI)
  apply (erule_tac imageE, simp)
  apply(erule deductions.induct)
  apply(blast intro: deductions.inferI mapRuleI)
  done

lemma deductionsCloseRules: "! (conc,prems) : S . prems <= deductions R --> conc : deductions R ==> deductions (R Un S) = deductions R"
  apply(rule equalityI)
  prefer 2
  apply(rule mono_deductions) apply blast
  apply(rule subsetI)
  apply (erule_tac deductions.induct, simp) apply(erule conjE) apply(thin_tac "prems ⊆ deductions (R ∪ S)")
  apply(erule disjE)
  apply(rule inferI) apply assumption apply force
  apply blast
  done
*)


subsection "Basic Rule sets"

definition
  "Axioms  = { z. ? p vs.              z = ([FAtom Pos p vs,FAtom Neg p vs],{}) }"
definition
  "Conjs   = { z. ? A0 A1 Delta Gamma. z = (FConj Pos A0 A1#Gamma @ Delta,{A0#Gamma,A1#Delta}) }"
definition
  "Disjs   = { z. ? A0 A1       Gamma. z = (FConj Neg A0 A1#Gamma,{A0#A1#Gamma}) }"
definition
  "Alls    = { z. ? A x         Gamma. z = (FAll Pos A#Gamma,{instanceF x A#Gamma}) & x ~: freeVarsFL (FAll Pos A#Gamma) }"
definition
  "Exs     = { z. ? A x         Gamma. z = (FAll Neg A#Gamma,{instanceF x A#Gamma})}"
definition
  "Weaks   = { z. ? A           Gamma. z = (A#Gamma,{Gamma})}"
definition
  "Contrs  = { z. ? A           Gamma. z = (A#Gamma,{A#A#Gamma})}"
definition
  "Cuts    = { z. ? C Delta     Gamma. z = (Gamma @ Delta,{C#Gamma,FNot C#Delta})}"
definition
  "Perms   = { z. ? Gamma Gamma'     . z = (Gamma,{Gamma'}) & mset Gamma = mset Gamma'}"
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)"
  apply(rule deductions.inferI)
  apply(auto simp add: Axioms_def) done

lemma DAxiomsI: "[| DAxioms <= A |] ==> [FAtom Neg p vs,FAtom Pos p vs] : deductions(A)"
  apply(rule deductions.inferI)
  apply(auto simp add: DAxioms_def) done

lemma DisjI: "[| A0#A1#Gamma : deductions(A); Disjs <= A |] ==> (FConj Neg A0 A1#Gamma) : deductions(A)"
  apply(rule deductions.inferI)
  apply(auto simp add: Disjs_def) done

lemma ConjI: "[| (A0#Gamma) : deductions(A); (A1#Delta) : deductions(A); Conjs <= A |] ==> FConj Pos A0 A1#Gamma @ Delta : deductions(A)"
  apply(rule_tac prems="{A0#Gamma,A1#Delta}" in deductions.inferI)
  apply(auto simp add: Conjs_def) apply force done

lemma AllI: "[| instanceF w A#Gamma : deductions(R); w ~: freeVarsFL (FAll Pos A#Gamma); Alls <= R |] ==> (FAll Pos A#Gamma) : deductions(R)"
  apply(rule_tac prems="{instanceF w A#Gamma}" in deductions.inferI)
  apply(auto simp add: Alls_def) done

lemma ExI: "[| instanceF w A#Gamma : deductions(R); Exs <= R |] ==> (FAll Neg A#Gamma) : deductions(R)"
  apply(rule_tac prems = "{instanceF w A#Gamma}" in deductions.inferI)
  apply(auto simp add: Exs_def) done

lemma WeakI: "[| Gamma : deductions R; Weaks <= R |] ==> A#Gamma : deductions(R)"
  apply(rule_tac prems="{Gamma}" in deductions.inferI)
  apply(auto simp add: Weaks_def) done

lemma ContrI: "[| A#A#Gamma : deductions R; Contrs <= R |] ==> A#Gamma : deductions(R)"
  apply(rule_tac prems="{A#A#Gamma}" in deductions.inferI)
  apply(auto simp add: Contrs_def) done

lemma PermI: "[| Gamma' : deductions R; mset Gamma = mset Gamma'; Perms <= R |] ==> Gamma : deductions(R)"
  apply(rule_tac prems="{Gamma'}" in deductions.inferI)
  apply(auto simp add: Perms_def) done


subsection "Derived Rules"

lemma WeakI1: "[| Gamma : deductions(A); Weaks <= A |] ==> (Delta @ Gamma) : deductions(A)"
  apply (induct Delta, simp)
  apply(auto intro: WeakI) done

lemma WeakI2: "[| Gamma : deductions(A); Perms <= A; Weaks <= A |] ==> (Gamma @ Delta) : deductions(A)"
  apply (auto intro: PermI [of ‹Delta @ Gamma›] WeakI1)
  done

lemma SATAxiomI: "[| Axioms <= A; Weaks <= A; Perms <= A; forms = [FAtom Pos n vs,FAtom Neg n vs] @ Gamma |] ==> forms : deductions(A)"
  apply(simp only:)
  apply(blast intro: WeakI2 AxiomI)
  done
    
lemma DisjI1: "[| (A1#Gamma) : deductions(A); Disjs <= A; Weaks <= A |] ==> FConj Neg A0 A1#Gamma : deductions(A)"
  apply(blast intro: DisjI WeakI)
  done

lemma DisjI2: "!!A. [| (A0#Gamma) : deductions(A); Disjs <= A; Weaks <= A; Perms <= A |] ==> FConj Neg A0 A1#Gamma : deductions(A)"
  apply(rule DisjI)
   apply(rule PermI [of ‹A1 # A0 # Gamma›])
  apply simp_all
  apply(rule WeakI)
  .

    ― ‹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"
  apply (rule PermI, auto)
  done

lemma weaken_append[rule_format]: "Contrs <= R ==> Perms <= R ==> !A. A @ Gamma @ Gamma : deductions(R) -->  A @ Gamma : deductions(R)"
  apply (induct_tac Gamma, simp, rule) apply rule
  apply(drule_tac x="a#a#A" in spec)
  apply(erule_tac impE)
  apply(rule perm_tmp4) apply(assumption, assumption)
  apply(thin_tac "A @ (a # list) @ a # list ∈ deductions R")
  apply simp
  apply(frule_tac ContrI) apply assumption
  apply(thin_tac "a # a # A @ list ∈ deductions R")
  apply(rule PermI) apply assumption 
  apply(simp add: perm_count_conv) 
  by assumption
  ― ‹FIXME horrible›

lemma ListWeakI: "Perms <= R ==> Contrs <= R ==> x # Gamma @ Gamma : deductions(R) ==> x # Gamma : deductions(R)"
  by(rule weaken_append[of R "[x]" Gamma, simplified])
    
lemma ConjI': "[| (A0#Gamma) : deductions(A);  (A1#Gamma) : deductions(A); Contrs <= A; Conjs <= A; Perms <= A |] ==> FConj Pos A0 A1#Gamma : deductions(A)"
  apply(rule ListWeakI, assumption, assumption)
  apply(rule ConjI) .



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: "! xs ys. mset xs = mset ys --> (inDed xs = inDed ys)"
  by (metis PermI inDed_def rulesInPCs(16))

lemma contr: "! x xs. inDed (x#x#xs) --> inDed (x#xs)"
  apply(simp add: inDed_def)
  apply(blast intro!: ContrI rulesInPCs)
  done

lemma weak: "! x xs. inDed xs --> inDed (x#xs)"
  apply(simp add: inDed_def)
  apply(blast intro!: WeakI rulesInPCs)
  done

lemma inDed_mono'[simplified inDed_def]: "set x <= set y ==> inDed x ==> inDed y"
  using perm_weak_contr_mono[OF perm contr weak] .

lemma inDed_mono[simplified inDed_def]: "inDed x ==> set x <= set y ==> inDed y"
  using perm_weak_contr_mono[OF perm contr weak] .


end