Theory SRCTransforms

(*<*)
(* Author : Peter Chapman *)
(* License: LGPL *)
section "Rule Set Transformations"
 
theory SRCTransforms
imports "HOL-Library.Multiset"
begin

datatype 'a form = At "nat"
                 | Compound "'a" "'a form list"
                 | ff

datatype 'a sequent = Sequent "('a form) multiset" "('a form) multiset" (‹ (_) ⇒* (_)› [6,6] 5)

abbreviation multiset_abbrev (‹\<LM> _  \<RM>› [75]75) where
   "\<LM> A \<RM> ≡ {# A #}"

abbreviation multiset_empty (‹\<Empt>› 75) where
  "\<Empt> ≡ {#}"

(* We have that any step in a rule, be it a primitive rule or an instance of a rule in a derivation
   can be represented as a list of premisses and a conclusion.  We need a list since a list is finite
   by definition *)
type_synonym 'a rule = "'a sequent list * 'a sequent"

type_synonym 'a deriv = "'a sequent * nat"

abbreviation
multiset_plus (infixl ‹⊕› 80) where
   "(Γ :: 'a multiset) ⊕ (A :: 'a) ≡ Γ + \<LM>A\<RM>"
abbreviation
multiset_minus (infixl ‹⊖› 80) where
   "(Γ :: 'a multiset) ⊖  (A :: 'a) ≡ Γ - \<LM>A\<RM>" 

consts
  (* extend a sequent by adding another one.  A form of weakening.  Is this overkill by adding a sequent? *)
  extend :: "'a sequent ⇒ 'a sequent ⇒ 'a sequent"
  extendRule :: "'a sequent ⇒ 'a rule ⇒ 'a rule"

  (* Unique conclusion Property *)
  uniqueConclusion :: "'a rule set ⇒ bool"

  (* Invertible definitions *)
  invertible :: "'a rule ⇒ 'a rule set ⇒ bool"
  invertible_set :: "'a rule set ⇒ bool"

  (* functions to get at components of sequents *)
primrec antec :: "'a sequent ⇒ 'a form multiset" where "antec (Sequent ant suc) = ant"
primrec succ :: "'a sequent ⇒ 'a form multiset" where "succ (Sequent ant suc) = suc"
primrec mset :: "'a sequent ⇒ 'a form multiset" where "mset (Sequent ant suc) = ant + suc"
primrec seq_size :: "'a sequent ⇒ nat" where "seq_size (Sequent ant suc) = size ant + size suc"

(* Extend a sequent, and then a rule by adding seq to all premisses and the conclusion *)
overloading
  extend ≡ extend
  extendRule ≡ extendRule
  uniqueConclusion ≡ uniqueConclusion
begin

definition extend
  where "extend forms seq ≡ (antec forms + antec seq) ⇒* (succ forms + succ seq)"

definition extendRule
  where "extendRule forms R ≡ (map (extend forms) (fst R), extend forms (snd R))"

(* The unique conclusion property.  A set of rules has unique conclusion property if for any pair of rules,
   the conclusions being the same means the rules are the same*)
definition uniqueConclusion :: "'a rule set ⇒ bool"
  where "uniqueConclusion R ≡ ∀ r1 ∈ R. ∀ r2 ∈ R. (snd r1 = snd r2) ⟶ (r1 =r2)"

end

primrec max_list :: "nat list ⇒ nat" where
  "max_list [] = 0"
| "max_list (n # ns) = max n (max_list ns)"

(* The depth of a formula.  Will be useful in later files. *)
fun depth :: "'a form ⇒ nat"
where
   "depth (At i) = 0"
|  "depth (Compound f fs) = (max_list (map depth fs)) + 1"
|  "depth (ff) = 0"

(* The formulation of various rule sets *)

(* Ax is the set containing all identity RULES and LBot *)
inductive_set "Ax" where
   id[intro]: "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ Ax"
|  Lbot[intro]: "([], \<LM> ff \<RM> ⇒* \<Empt>) ∈ Ax"

(* upRules is the set of all rules which have a single conclusion.  This is akin to each rule having a 
   single principal formula.  We don't want rules to have no premisses, hence the restriction
   that ps ≠ [] *)
inductive_set "upRules" where
   I[intro]: "⟦ mset c ≡ \<LM> Compound R Fs \<RM> ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"

inductive_set extRules :: "'a rule set ⇒ 'a rule set"  (‹_*›)
  for R :: "'a rule set" 
  where
   I[intro]: "r ∈ R ⟹ extendRule seq r ∈ R*"

(* A formulation of what it means to be a principal formula for a rule.  Note that we have to build up from
   single conclusion rules.   *)

inductive leftPrincipal :: "'a rule ⇒ 'a form ⇒ bool"
  where
  up[intro]: "C = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)  ⟹ 
                   leftPrincipal (Ps,C) (Compound F Fs)"


inductive rightPrincipal :: "'a rule ⇒ 'a form ⇒ bool"
  where
  up[intro]: "C = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ⟹ rightPrincipal (Ps,C) (Compound F Fs)"


(* What it means to be a derivable sequent.  Can have this as a predicate or as a set.
   The two formation rules say that the supplied premisses are derivable, and the second says
   that if all the premisses of some rule are derivable, then so is the conclusion.  *)

inductive_set derivable :: "'a rule set ⇒ 'a deriv set"
  for R :: "'a rule set"
  where
   base[intro]: "⟦([],C) ∈ R⟧ ⟹ (C,0) ∈ derivable R"
|  step[intro]: "⟦ r ∈ R ; (fst r)≠[] ; ∀ p ∈ set (fst r). ∃ n ≤ m. (p,n) ∈ derivable R ⟧ 
                       ⟹ (snd r,m + 1) ∈ derivable R"


(* When we don't care about height! *)
inductive_set derivable' :: "'a rule set ⇒ 'a sequent set"
   for R :: "'a rule set"
   where
    base[intro]: "⟦ ([],C) ∈ R ⟧ ⟹ C ∈ derivable' R"
|   step[intro]: "⟦ r ∈ R ; (fst r) ≠ [] ; ∀ p ∈ set (fst r). p ∈ derivable' R ⟧
                       ⟹ (snd r) ∈ derivable' R"

lemma deriv_to_deriv[simp]:
assumes "(C,n) ∈ derivable R"
shows "C ∈ derivable' R"
using assms by (induct) auto

lemma deriv_to_deriv2:
assumes "C ∈ derivable' R"
shows "∃ n. (C,n) ∈ derivable R"
using assms
proof (induct)
  case (base C)
  then have "(C,0) ∈ derivable R" by auto
  then show ?case by blast
next
  case (step r)
  then obtain ps c where "r = (ps,c)" and "ps ≠ []" by (cases r) auto
  then have aa: "∀ p ∈ set ps. ∃ n. (p,n) ∈ derivable R" using step(3) by auto
  then have "∃ m. ∀ p ∈ set ps. ∃ n≤m. (p,n) ∈ derivable R"
  proof (induct ps)
    case Nil
    then show ?case  by auto
  next
    case (Cons a as)
    then have "∃ m. ∀ p ∈ set as. ∃ n≤m. (p,n) ∈ derivable R" by auto
    then obtain m where "∀ p ∈ set as. ∃ n≤m. (p,n) ∈ derivable R" by auto
    moreover from ‹∀ p ∈ set (a # as). ∃ n. (p,n) ∈ derivable R› have
      "∃ n. (a,n) ∈ derivable R" by auto
    then obtain m' where "(a,m') ∈ derivable R" by blast
    ultimately have "∀ p ∈ set (a # as). ∃ n≤(max m m'). (p,n) ∈ derivable R"
      apply (auto simp add:Ball_def)
      apply (rule_tac x=m' in exI) apply simp
      apply (drule_tac x=x in spec) apply auto
      apply (rule_tac x=n in exI) apply auto done
    then show ?case by blast
  qed
  then obtain m where "∀ p ∈ set ps. ∃ n≤m. (p,n) ∈ derivable R" by blast
  with ‹r = (ps,c)› and ‹r ∈ R› have "(c,m+1) ∈ derivable R" using ‹ps ≠ []› and
    derivable.step[where r="(ps,c)" and R=R and m=m] by auto
  then show ?case using ‹r = (ps,c)› by auto
qed

(* definition of invertible rule and invertible set of rules.  It's a bit nasty, but all it really says is
   If a rule is in the given set, and if any extension of that rule is derivable at n, then the
   premisses of the extended rule are derivable at height at most n.  *)
overloading
  invertible ≡ invertible
  invertible_set ≡ invertible_set
begin

definition invertible
  where "invertible r R ≡
    ∀ n S. (r ∈ R ∧ (snd (extendRule S r),n) ∈ derivable R*) ⟶
    (∀ p ∈ set (fst (extendRule S r)). ∃ m ≤ n. (p,m) ∈ derivable R*)"

definition invertible_set
  where "invertible_set R ≡ ∀ (ps,c) ∈ R. invertible (ps,c) R"

end


(* Characterisation of a sequent *)
lemma characteriseSeq:
shows "∃ A B. (C :: 'a sequent) = (A ⇒* B)"
apply (rule_tac x="antec C" in exI, rule_tac x="succ C" in exI) by (cases C) (auto)


(* Helper function for later *)
lemma nonEmptySet:
shows "A ≠ [] ⟶ (∃ a. a ∈ set A)"
by (auto simp add:neq_Nil_conv)

(* Lemma which comes in helpful ALL THE TIME *)
lemma midMultiset:
  assumes "Γ ⊕ A = Γ' ⊕ B" and "A ≠ B"
  shows "∃ Γ''. Γ = Γ'' ⊕ B ∧ Γ' = Γ'' ⊕ A"
proof-
  from assms have "A ∈# Γ'"
      proof-
      from assms have "set_mset (Γ ⊕ A) = set_mset (Γ' ⊕ B)" by auto
      then have "set_mset Γ ∪ {A} = set_mset Γ' ∪ {B}" by auto
      then have "set_mset Γ ∪ {A} ⊆ set_mset Γ' ∪ {B}" by simp
      then have "A ∈ set_mset Γ'" using assms by auto
      thus "A ∈# Γ'" by simp
      qed
  then have "Γ' ⊖ A ⊕ A = Γ'" by (auto simp add:multiset_eq_iff)
  then have "∃ Γ''. Γ' = Γ'' ⊕ A" apply (rule_tac x="Γ' ⊖ A" in exI) by auto
  then obtain Γ'' where eq1:"Γ' = Γ'' ⊕ A" by blast
  from ‹Γ ⊕ A = Γ' ⊕ B› eq1 have "Γ ⊕ A = Γ'' ⊕ A ⊕ B" by auto
  then have "Γ = Γ'' ⊕ B" by auto
  thus ?thesis using eq1 by blast
qed

(* Lemma which says that if we have extended an identity rule, then the propositional variable is
   contained in the extended multisets *)
lemma extendID:
assumes "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)"
shows "At i ∈# Γ ∧ At i ∈# Δ"
using assms
proof-
  from assms have "∃ Γ' Δ'. Γ = Γ' ⊕ At i ∧ Δ = Δ' ⊕ At i" 
    using extend_def[where forms=S and seq="\<LM> At i \<RM> ⇒* \<LM> At i \<RM>"]
    by (rule_tac x="antec S" in exI,rule_tac x="succ S" in exI) auto
  then show ?thesis by auto
qed

lemma extendFalsum:
assumes "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
shows "ff ∈# Γ"
proof-
  from assms have "∃ Γ'. Γ = Γ' ⊕ ff" 
    using extend_def[where forms=S and seq="\<LM>ff \<RM> ⇒* \<Empt>"]
    by (rule_tac x="antec S" in exI) auto
  then show ?thesis by auto
qed


(* Lemma that says if a propositional variable is in both the antecedent and succedent of a sequent,
   then it is derivable from idupRules *)
lemma containID:
assumes a:"At i ∈# Γ ∧ At i ∈# Δ"
    and b:"Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
  from a have "Γ = Γ ⊖ At i ⊕ At i ∧ Δ = Δ ⊖ At i ⊕ At i" by auto
  then have "extend ((Γ ⊖ At i) ⇒* (Δ ⊖ At i)) (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)" 
    using extend_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and seq="\<LM>At i\<RM> ⇒* \<LM>At i\<RM>"]
    by auto
  moreover
  have "([],\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ R" using b by auto
  ultimately
  have "([],Γ ⇒* Δ) ∈ R*" 
    using extRules.I[where R=R and r="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<RM>)" and seq="Γ ⊖ At i ⇒* Δ ⊖ At i"] 
      and extendRule_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and R="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"] by auto
  then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* Δ"] by auto
qed

lemma containFalsum:
assumes a: "ff ∈# Γ"
   and  b: "Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
  from a have "Γ = Γ ⊖ ff ⊕ ff" by auto
  then have "extend (Γ ⊖ ff ⇒* Δ) (\<LM>ff\<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
    using extend_def[where forms="Γ ⊖ ff ⇒* Δ" and seq="\<LM>ff\<RM> ⇒* \<Empt>"] by auto 
  moreover
  have "([],\<LM>ff\<RM> ⇒* \<Empt>) ∈ R" using b by auto
  ultimately have "([],Γ ⇒* Δ) ∈ R*"
    using extRules.I[where R=R and r="([],  \<LM>ff\<RM> ⇒* \<Empt>)" and seq="Γ ⊖ ff ⇒* Δ"] 
      and extendRule_def[where forms="Γ ⊖ ff ⇒* Δ" and R="([],  \<LM>ff\<RM> ⇒* \<Empt>)"] by auto
  then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* Δ"] by auto
qed 

(* Lemma which says that if r is an identity rule, then r is of the form
   ([], P ⇒* P) *)
lemma characteriseAx:
shows "r ∈ Ax ⟹ r = ([],\<LM> ff \<RM> ⇒* \<Empt>) ∨ (∃ i. r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>))"
  apply (cases r) by (rule Ax.cases) auto

(* A lemma about the last rule used in a derivation, i.e. that one exists *)
lemma characteriseLast:
assumes "(C,m+1) ∈ derivable R"
shows "∃ Ps. Ps ≠ [] ∧
             (Ps,C) ∈ R ∧ 
             (∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)"
using assms
by (cases) auto


(* Lemma which says that if rule is an upRule, then the succedent is either empty, or a single formula *)
lemma succ_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)" using mset.simps[where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

(* Equivalent, but the antecedent *)
lemma antec_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)" using mset.simps[where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

lemma upRule_Size:
assumes "r ∈ upRules"
shows "seq_size (snd r) = 1"
using assms
proof-
    obtain Ps C where "r = (Ps,C)" by (cases r)
    then have "(Ps,C) ∈ upRules" using assms by simp
    then show ?thesis
       proof (cases)
          case (I R Rs)
          obtain G H where "C = (G ⇒* H)" by (cases C) (auto)
          then have "G + H = \<LM>Compound R Rs\<RM>" using mset.simps and ‹mset C ≡ \<LM>Compound R Rs\<RM>› by auto
          then have "size (G+H) = 1" by auto 
          then have "size G + size H = 1" by auto
          then have "seq_size C = 1" using seq_size.simps[where ant=G and suc=H] and ‹C = (G ⇒* H)› by auto
          moreover have "snd r = C" using ‹r = (Ps,C)› by simp
          ultimately show "seq_size (snd r) = 1" by simp
       qed
qed

lemma upRuleCharacterise:
assumes "(Ps,C) ∈ upRules"
shows "∃ F Fs. C = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ∨ C = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)"
using assms
proof (cases)
  case (I F Fs)
  then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
  then have "(Ps,Γ ⇒* Δ) ∈ upRules" using assms by simp
  then show "∃ F Fs. C = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ∨ C = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)" 
    using ‹mset C ≡ \<LM>Compound F Fs\<RM>› and ‹C = (Γ ⇒* Δ)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="Compound F Fs"]
    by auto
qed

lemma extendEmpty:
shows "extend (\<Empt> ⇒* \<Empt>) C = C"
apply (auto simp add:extend_def) by (cases C) auto

lemma extendContain:
assumes "r = (ps,c)"
    and "(Ps,C) = extendRule S r"
    and "p ∈ set ps"
shows "extend S p ∈ set Ps"
proof-
from ‹p ∈ set ps› have "extend S p ∈ set (map (extend S) ps)" by auto
moreover from ‹(Ps,C) = extendRule S r› and ‹r = (ps,c)› have "map (extend S) ps = Ps" by (simp add:extendRule_def) 
ultimately show ?thesis by auto
qed

lemma nonPrincipalID:
fixes A :: "'a form"
assumes "r ∈ Ax"
shows "¬ rightPrincipal r A ∧ ¬ leftPrincipal r A"
proof-
from assms obtain i where r1:"r = ([], \<LM> ff \<RM> ⇒* \<Empt>) ∨ r = ([], \<LM> At i \<RM> ⇒* \<LM> At i\<RM>)" 
     using characteriseAx[where r=r] by auto
{ assume "rightPrincipal r A" then obtain Ps where r2:"r = (Ps, \<Empt> ⇒* \<LM> A \<RM>)" by (cases r) auto
  with r1 have "False" by simp
}
then have "¬ rightPrincipal r A" by auto
moreover
{ assume "leftPrincipal r A" then obtain Ps' F Fs where r3:"r = (Ps', \<LM>Compound F Fs\<RM> ⇒* \<Empt>)" by (cases r) auto
  with r1 have "False" by auto
}
then have "¬ leftPrincipal r A" by auto
ultimately show ?thesis by simp
qed

lemma extendCommute:
shows "(extend S) (extend R c) = (extend R) (extend S c)"
by (auto simp add:extend_def union_ac)

lemma mapCommute:
shows "map (extend S) (map (extend R) c) = map (extend R) (map (extend S) c)"
by (induct_tac c) (auto simp add:extendCommute)

lemma extendAssoc:
shows "(extend S) (extend R c) = extend (extend S R) c" 
by (auto simp add:extend_def union_ac)

lemma mapAssoc:
shows "map (extend S) (map (extend R) c) = map (extend (extend S R)) c"
by (induct_tac c) (auto simp add:extendAssoc)

lemma extended_Ax_prems_empty:
assumes "r ∈ Ax"
shows "fst (extendRule S r) = []"
using assms apply (cases r) by (rule Ax.cases) (auto simp add:extendRule_def)

inductive lastRule :: "'a deriv ⇒ 'a rule ⇒ 'a rule set ⇒ bool"
  where
  base[intro]: "⟦ r ∈ Ax; Ax ⊆ R ; snd (extendRule S r) = (Γ ⇒* Δ)⟧
                 ⟹ lastRule (Γ ⇒* Δ,0) r R"
|    I[intro]:  "⟦ r∈R ; r ∉ Ax ; snd (extendRule S r) = (Γ ⇒* Δ) ; 
                ∀ p ∈ set (fst (extendRule S r)). ∃ m≤n. (p,m) ∈ derivable R* ⟧ 
                 ⟹ lastRule (Γ ⇒* Δ,n+1) r R" 

lemma obv:
fixes a :: "('a * 'b)"
shows "a = (fst a, snd a)" by auto

lemma getLast:
assumes "lastRule (Γ ⇒* Δ,n+1) r R"
shows "∃ S Ps. extendRule S r = (Ps, Γ ⇒* Δ) ∧ (∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*) ∧ r ∈ R ∧ r ∉ Ax"
proof-
  from assms show ?thesis apply (rule lastRule.cases) apply simp apply simp
  apply (rule_tac x=S in exI) apply (rule_tac x="fst (extendRule S r)" in exI) apply simp
  apply auto
  apply (subgoal_tac "extendRule S (a,b) = (fst (extendRule S (a,b)),snd (extendRule S (a,b)))")
  apply simp by (rule obv)
qed

lemma getAx:
assumes "lastRule (Γ ⇒* Δ,0) r R"
shows "r ∈ Ax ∧ (∃ S. extendRule S r = ([],Γ ⇒* Δ))"
proof-
  from assms have "r ∈ Ax ∧ (∃ S. snd (extendRule S r) = (Γ ⇒* Δ))"
       by (rule lastRule.cases) auto
  then obtain S where "r ∈ Ax" and "snd (extendRule S r) = (Γ ⇒* Δ)" by auto
  from ‹r ∈ Ax› have "fst r = []" apply (cases r) by (rule Ax.cases) auto
  then have "fst (extendRule S r) = []" by (auto simp add:extendRule_def)
  with ‹snd (extendRule S r) = (Γ ⇒* Δ)› and ‹r ∈ Ax› show ?thesis apply auto
       apply (rule_tac x=S in exI) 
       apply (subgoal_tac "extendRule S r = (fst (extendRule S r),snd (extendRule S r))") apply simp
       by (rule obv)
qed


(* Has the usual set-up: takes a subset of the upRules, combines with all the axioms, blah blah *)


(* Constructing the rule set we will use.  It contains all axioms, but only a subset
   of the possible logical rules. *)
lemma ruleSet:
assumes "R' ⊆ upRules"
    and "R = Ax ∪ R'"
    and "(Ps,C) ∈ R*"
shows "∃ S r. extendRule S r = (Ps,C) ∧ (r ∈ R' ∨ r ∈ Ax)"
proof-
from ‹(Ps,C) ∈ R*› have "∃ S r. extendRule S r = (Ps,C) ∧ r ∈ R" by (cases) auto
then obtain S r where "(Ps,C) = extendRule S r" and "r ∈ R" apply auto 
                by (drule_tac x=S in meta_spec,drule_tac x=a in meta_spec, drule_tac x=b in meta_spec) auto
moreover from ‹r ∈ R› and ‹R = Ax ∪ R'› have "r ∈ Ax ∨ r ∈ R'" by blast
ultimately show ?thesis by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
qed

lemma dpWeak:
assumes a:"(Γ ⇒* Δ,n) ∈ derivable R*"
   and  b: "R' ⊆ upRules"
   and  c: "R = Ax ∪ R'" 
shows "(Γ + Γ' ⇒* Δ + Δ',n) ∈ derivable R*"
using a
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
case (1 n Γ Δ)
then have IH: "∀m<n. ∀ Γ Δ. ( Γ ⇒* Δ, m) ∈ derivable R* ⟶ ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable R*" 
      and a': "( Γ ⇒* Δ, n) ∈ derivable R*" by auto
show ?case
proof (cases n)
case 0
 then have "(Γ ⇒* Δ,0) ∈ derivable R*" using a' by simp
 then have "([], Γ ⇒* Δ) ∈ R*" by (cases) auto
 then obtain  r S where "r ∈ R" and split:"extendRule S r = ([],Γ ⇒* Δ)" 
      by (rule extRules.cases) auto
 then obtain c where "r = ([],c)" by (cases r) (auto simp add:extendRule_def)
 with ‹r ∈ R› have "r ∈ Ax ∨ r ∈ upRules" using b c by auto
 with ‹r = ([],c)› have "r ∈ Ax" by (auto) (rule upRules.cases,auto)                                 
 with ‹r = ([],c)› obtain i where "c = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>) ∨ c = (\<LM>ff\<RM> ⇒* \<Empt>)"
      using characteriseAx[where r=r] by auto
 moreover
    {assume "c = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"
     then have "extend S (\<LM>At i\<RM> ⇒*\<LM>At i\<RM>) = (Γ ⇒* Δ)" using split and ‹r = ([],c)›
          by (auto simp add:extendRule_def)
     then have "At i ∈# Γ ∧ At i ∈# Δ" using extendID by auto
     then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
     then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" 
          using c and containID[where Γ="Γ+Γ'" and Δ="Δ+Δ'" and R=R and i=i] by auto
    }
 moreover
    {assume "c = (\<LM>ff\<RM> ⇒* \<Empt>)"
     then have "extend S (\<LM>ff\<RM> ⇒*\<Empt>) = (Γ ⇒* Δ)" using split and ‹r = ([],c)›
          by (auto simp add:extendRule_def)
     then have "ff ∈# Γ" using extendFalsum by auto
     then have "ff ∈# Γ + Γ'" by auto
     then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" 
          using c and containFalsum[where Γ="Γ+Γ'" and Δ="Δ+Δ'" and R=R] by auto
    }
 ultimately show "(Γ + Γ' ⇒* Δ + Δ',n) ∈ derivable R*" using ‹n=0› by auto
next
case (Suc n')
 then have "(Γ ⇒* Δ, n'+1) ∈ derivable R*" using a' by simp
 then obtain Ps where f:"Ps ≠ []"
                  and g:"(Ps, Γ ⇒* Δ) ∈ R*" 
                  and h:"∀ p ∈ set Ps. ∃ m≤n'. (p,m) ∈ derivable R*" 
      using characteriseLast[where C="Γ ⇒* Δ" and m=n' and R="R*"] by auto
 from g c obtain S r where "r ∈ R" and "(r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⇒* Δ)" by (cases) auto
 with b have as: "(r ∈ Ax ∨ r ∈ upRules) ∧ extendRule S r = (Ps, Γ ⇒* Δ)" by auto
 then have eq:"map (extend (Γ' ⇒* Δ')) Ps = fst (extendRule (extend S (Γ' ⇒* Δ')) r)"
       using mapCommute[where S="Γ'⇒*Δ'" and R=S and c="fst r"]
       by (auto simp add:extendRule_def extend_def mapAssoc simp del: map_map)
 from as have eq2: "(Γ + Γ' ⇒* Δ + Δ') = snd (extendRule (extend S (Γ' ⇒* Δ')) r)"
       by (auto simp add:extendRule_def extend_def union_ac)
 from as f have "fst r ≠ []" by (auto simp add:extendRule_def map_is_Nil_conv)
 with as have "r ∈ upRules" apply (cases r,auto) by (rule Ax.cases) auto
 have "∀ p' ∈ set (map (extend (Γ' ⇒* Δ')) Ps). ∃ m≤n'. (p',m) ∈ derivable R*"
      proof-
      {fix p
       assume "p ∈ set (map (extend (Γ' ⇒* Δ')) Ps)"
       then obtain p' where t:"p' ∈ set Ps ∧ p = extend (Γ' ⇒* Δ') p'" by auto
       with h obtain m where "m≤n'" and "(p',m) ∈ derivable R*" by auto
       moreover obtain Φ Ψ where eq:"p' = (Φ ⇒* Ψ)" by (cases p') auto 
       then have "p = (Φ + Γ' ⇒* Ψ + Δ')" using t by (auto simp add:extend_def union_ac)
       ultimately have "(p,m) ∈ derivable R*" using IH and ‹n = Suc n'› and eq
            apply- by (drule_tac x=m in spec) simp
       then have "∃ m≤n'. (p,m) ∈ derivable R*" using ‹m≤n'› by auto
       }
       then show ?thesis by auto
       qed
 then have "∀ p' ∈ set (fst (extendRule (extend S (Γ' ⇒* Δ')) r)).
            ∃ m≤n'. (p',m) ∈ derivable R*" using eq by auto
 moreover have "extendRule (extend S (Γ' ⇒* Δ')) r ∈ R*" 
          using ‹r ∈ upRules› and ‹r ∈ R› by auto
 ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable R*"
          using derivable.step[where r="extendRule (extend S (Γ' ⇒* Δ')) r" and R="R*" and m="n'"]
          and ‹fst r ≠ []› and eq2 by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
 then show "( Γ + Γ' ⇒* Δ + Δ', n) ∈ derivable R*" using ‹n = Suc n'› by auto
 qed
qed
(*>*)
text‹
\section{Manipulating Rule Sets \label{isaSRC}}
The removal of superfluous and redundant rules \<^cite>‹"AL01"› will not be harmful to invertibility: removing rules means that the conditions of earlier sections are more likely to be fulfilled.  Here, we formalise the results that the removal of such rules from a calculus $\mathcal{L}$ will create a new calculus $\mathcal{L}'$ which is equivalent.  In other words, if a sequent is derivable in $\mathcal{L}$, then it is derivable in $\mathcal{L}'$.
The results formalised in this section are for \SC multisuccedent calculi.

When dealing with lists of premisses, a rule $R$ with premisses $P$ will be redundant given a rule $R'$ with premisses $P'$ if there exists some $p$ such that $P = p \# P'$.  There are other ways in which a rule could be redundant; say if $P = Q @ P'$, or if $P = P' @ Q$, and so on.  The order of the premisses is not really important, since the formalisation operates on the finite set based upon the list.  The more general ``append'' lemma could be proved from the lemma we give; we prove the inductive step case in the proof of such an append lemma.  This is a height preserving transformation.  Some of the proof is shown:
›

lemma removeRedundant:
assumes (*<*)a:(*>*) "r1 = (p#ps,c) ∧ r1 ∈ upRules"
and     (*<*)b:(*>*) "r2 = (ps,c) ∧ r2 ∈ upRules"
and     (*<*)c:(*>*) "R1 ⊆ upRules ∧ R = Ax ∪ R1"
and     (*<*)d:(*>*) "(T,n) ∈ derivable (R ∪ {r1} ∪ {r2})*"
shows   "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*"
 (*<*)
using assms (*>*)
proof (induct n (*<*)arbitrary: T (*>*)rule:nat_less_induct)
 (*<*)case (1 n T)
    then have IH: " ∀m<n. ∀ x. (r1 = (p # ps, c) ∧ r1 ∈ upRules ⟶
                         r2 = (ps, c) ∧ r2 ∈ upRules ⟶
                         R1 ⊆ upRules ∧ R = Ax ∪ R1 ⟶ 
                         (x, m) ∈ derivable (R ∪ {r1} ∪ {r2})* ⟶ 
                         (∃ m'≤m. (x, m') ∈ derivable (R ∪ {r2})*))" and
             prm: "(T,n) ∈ derivable (R ∪ {r1} ∪ {r2})*" by auto
    show ?case
 proof (cases n) (*>*)
 case 0
  (*<*) with prm (*>*) have "(T,0) ∈ derivable (R ∪ {r1} ∪ {r2})*" by simp
   then have "([],T) ∈ (R ∪ {r1} ∪ {r2})*" by (cases) auto
   then obtain S r where ext: "extendRule S r = ([],T)" and 
        "r ∈ (R ∪ {r1} ∪ {r2})" by (rule extRules.cases) auto
   then have "r ∈ R ∨ r = r1 ∨ r = r2" using c by auto
txt‹\noindent It cannot be the case that $r=r_{1}$ or $r=r_{2}$, since those are \SC rules, whereas anything with an empty set of premisses
must be an axiom.  Since $\mathcal{R}$ contains the set of axioms, so will $\mathcal{R} \cup r_{2}$:›
 (*<*)   moreover from ext obtain d where "r = ([],d)" by (cases r) (auto simp add:extendRule_def) 
   ultimately have "r ∈ R ∨ r = r2" using c a ext by (auto simp add:extendRule_def) (*>*)
   then have "r ∈ (R ∪ {r2})" using c by auto
 (*<*)  then have "([],T) ∈ (R ∪ {r2})*" using ‹extendRule S r = ([],T)› 
          and extRules.I[where r=r and R="R ∪ {r2}" and seq=S] by auto (*>*)
  then have "(T,0) ∈ derivable (R ∪ {r2})*" by auto
  then show "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*" using ‹n=0› by auto
next
 case (Suc n')
 (*<*) with prm (*>*)have "(T,n'+1) ∈ derivable (R ∪ {r1} ∪ {r2})*" by simp
  then obtain Ps where e: "Ps ≠ []"
         and   f: "(Ps,T) ∈ (R ∪ {r1} ∪ {r2})*"
         and   g: "∀ P ∈ set Ps. ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r1} ∪ {r2})*"
        (*<*) using characteriseLast[where C=T and m=n' and R="(R ∪ {r1} ∪ {r2})*"](*>*) by auto
  have g': "∀ P ∈ set Ps. ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r2})*"
  (*<*)       proof-
              {fix P
               assume "P ∈ set Ps"
               with g obtain m where "(P,m) ∈ derivable (R ∪ {r1} ∪ {r2})*" and "m≤n'" by auto
               with IH have "∃ m'≤m. (P,m') ∈ derivable (R ∪ {r2})*" using a b c and ‹n = Suc n'›
                    by auto
               then have "∃ m≤n'. (P,m) ∈ derivable (R ∪ {r2})*" using ‹m≤n'› apply auto 
                    by (rule_tac x=m' in exI) auto
              } 
              then show ?thesis by auto
         qed  (*>*)             
   from f obtain S r where ext: "extendRule S r = (Ps,T)"
        and "r ∈ (R ∪ {r1} ∪ {r2})" by (rule extRules.cases) auto
    then have "r ∈ (R ∪ {r2}) ∨ r = r1" by auto
txt‹\noindent Either $r$ is in the new rule set or $r$ is the redundant rule.  In the former case, there is nothing to do:›
 (*<*)moreover
    {(*>*) assume "r ∈ (R ∪ {r2})"
     then have "(Ps,T) ∈ (R ∪ {r2})*" (*<*)using ext and extRules.I[where r=r and R="R ∪ {r2}" and seq=S](*>*) by auto
     with g' have "(T,n) ∈ derivable (R ∪ {r2})*" using ‹n = Suc n'› (*<*)and e and
       derivable.step[where r="(Ps,T)" and R="(R ∪ {r2})*" and m=n'](*>*) by auto
   (*<*) }
 moreover 
    { (*>*)
txt‹\noindent In the latter case, the last inference was redundant.  Therefore the premisses, which are derivable at a lower height than the conclusion, 
contain the premisses of $r_{2}$ (these premisses are \texttt{extend S ps}).  This completes the proof:›
     assume "r = r1" 
     with ext have "map (extend S) (p # ps) = Ps" using a by (auto(*<*) simp add:extendRule_def(*>*))
     then have "∀ P ∈ set (map (extend S) (p#ps)). 
                   ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r2})*"
         using g' by simp
     then have h: "∀ P ∈ set (map (extend S) ps). 
                      ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r2})*" by auto

 (*<*)    have "extendRule S r2 = (map (extend S) ps, T)" using b and a and ext and ‹r = r1› 
           by (auto simp add:extendRule_def)
     then have i: "(map (extend S) ps,T) ∈ (R ∪ {r2})*" using extRules.I(*<*)[where r=r2 and R="(R ∪ {r2})" and seq=S](*>*)
               by auto
    have "ps = [] ∨ ps ≠ []" by blast
   moreover
       {assume "ps = []"
         with i have "([],T) ∈ (R ∪ {r2})*" by auto
         then have "(T,0) ∈ derivable (R ∪ {r2})*" by auto
         then have "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*" by auto
       }
       moreover
          {assume "ps ≠ []"
           then have "map (extend S) ps ≠ []" by auto
            with i and h have "(T,n'+1) ∈ derivable (R ∪ {r2})*" 
                  using derivable.step[where r="(map (extend S) ps,T)" and R="(R ∪ {r2})*" and m=n'] by auto
           with ‹n = Suc n'› have "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*" by auto
           }
       ultimately have "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*" by blast
     }
  ultimately show "∃ m≤n. (T,m) ∈ derivable (R ∪ {r2})*" by blast
  qed
qed(*>*)
text‹
\noindent Recall that to remove superfluous rules, we must know that Cut is admissible in the original calculus \<^cite>‹"AL01"›.  Again, we add the two distinguished premisses at the head of the premiss list; general results about permutation of lists will achieve a more general result.  Since one uses Cut in the proof, this will in general not be height-preserving:
›

lemma removeSuperfluous:
assumes (*<*)a:(*>*) "r1 = ((\<Empt> ⇒* \<LM>A\<RM>) # ((\<LM>A\<RM> ⇒* \<Empt>) # ps),c) ∧ r1 ∈ upRules"
and     (*<*)b:(*>*) "R1 ⊆ upRules ∧ R = Ax ∪ R1"
and     "(T,n) ∈ derivable (R ∪ {r1})*"
and     CA: "∀ Γ Δ A. ((Γ ⇒* Δ ⊕ A) ∈ derivable' R* ⟶ 
             (Γ ⊕ A ⇒* Δ) ∈ derivable' R*) ⟶
             (Γ ⇒* Δ) ∈ derivable' R*"
shows   "T ∈ derivable' R*"
(*<*)
using assms
proof (induct n arbitrary: T rule: nat_less_induct)
  case (1 n T)
  then have IH: "∀m<n. r1 = (( \<Empt> ⇒* \<LM>A\<RM>) # ( \<LM>A\<RM> ⇒* \<Empt>) # ps, c) ∧ r1 ∈ upRules ⟶
    R1 ⊆ upRules ∧ R = Ax ∪ R1 ⟶
    (∀ T. (T, m) ∈ derivable (R ∪ {r1})* ⟶
    (∀ Γ Δ B.
    ((Γ ⇒* Δ ⊕ B) ∈ derivable' R* ⟶ (Γ ⊕ B ⇒* Δ) ∈ derivable' R*) ⟶ 
    (Γ ⇒* Δ) ∈ derivable' R*) ⟶
    T ∈ derivable' R*)" by blast
  from 1 have prm: "(T,n) ∈ derivable (R ∪ {r1})*" by blast
  show ?case
  proof (cases n)
    case 0
    with prm have "(T,0) ∈ derivable (R ∪ {r1})*" by simp
    then have "([],T) ∈ (R ∪ {r1})*" by (rule derivable.cases) auto
    then obtain S r where ext: "extendRule S r = ([],T)" and "r ∈ (R ∪ {r1})" by (rule extRules.cases) auto
    then have "r ∈ R ∨ r = r1" by auto
    with a have "r ∈ R" using ext by (auto simp add:extendRule_def)
    then have "([],T) ∈ R*" using ext and extRules.I[where r=r and R=R and seq=S] by auto
    then show "T ∈ derivable' R*" by auto
  next
    case (Suc n')
    with prm have prm': "(T,n'+1) ∈ derivable (R ∪ {r1})*" by auto
    then obtain Ps where ne: "Ps ≠ []"
      and   ex: "(Ps,T) ∈ (R ∪ {r1})*"
      and   "∀ P ∈ set Ps. ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r1})*"
      using characteriseLast[where C=T and m=n' and R="(R ∪ {r1})*"] by auto
    with IH have e: "∀ P ∈ set Ps. P ∈ derivable' R*" using a b and prm' and ‹n = Suc n'›
      apply (auto simp only:Ball_def) apply (drule_tac x=x in spec) apply auto
      apply (drule_tac x=m in spec) apply auto apply (drule_tac x=x in spec) apply simp
      apply (insert CA[simplified]) apply (subgoal_tac "R = Ax ∪ R1") apply blast apply (insert b) by blast
    from ex obtain S r where ext: "extendRule S r = (Ps,T)" and "r ∈ (R ∪ {r1})" by (rule extRules.cases) auto
    then have "r ∈ R ∨ r = r1" by blast
    moreover
    {assume "r ∈ R"
      with ext have "(Ps,T) ∈ R*" using extRules.I[where r=r and R=R and seq=S] by auto
      with e have "T ∈ derivable' R*" using ne and
        derivable'.step[where r="(Ps,T)" and R="R*"] by auto
    }
    moreover
    {assume "r = r1"
      with e and a and ext have "(extend S (\<LM>A\<RM> ⇒* \<Empt>)) ∈ derivable' R*"
        and  "(extend S (\<Empt> ⇒* \<LM>A\<RM>)) ∈ derivable' R*"
        by (auto simp add:extendRule_def)
      then have "S ∈ derivable' R*" using CA apply-
        apply (drule_tac x="antec S" in spec) apply (drule_tac x="succ S" in spec) apply (drule_tac x=A in spec)
        apply (simp add:extend_def) by (cases S) auto
      then obtain s where "(S,s) ∈ derivable R*" using deriv_to_deriv2 by auto
      then have "(extend S c,s) ∈ derivable R*" 
        using dpWeak[where R=R and R'=R1 and Γ="antec S" and Δ="succ S"
          and Γ'="antec c" and Δ'="succ c" and n=s] and b
        apply (auto simp add:extend_def union_ac) by (cases S) auto
      with ext have "(T,s) ∈ derivable R*" using ‹r = r1› and a by (auto simp add:extendRule_def)
      then have "T ∈ derivable' R*" by auto
    }
    ultimately show "T ∈ derivable' R*" by blast
  qed
qed
(*>*)

text‹
\noindent \textit{Combinable rules} can also be removed.  We encapsulate the combinable criterion by saying that if $(p \# P,T)$ and $(q \# P, T)$ are rules in a calculus, then we get an equivalent calculus by replacing these two rules by $((\textrm{extend } p \ q) \# P, T)$.  Since the \texttt{extend} function is commutative, the order of $p$ and $q$ in the new rule is not important.  This transformation is height preserving:
›

lemma removeCombinable:
assumes a: "r1 = (p # ps,c) ∧ r1 ∈ upRules"
and     b: "r2 = (q # ps,c) ∧ r2 ∈ upRules"
and     c: "r3 = (extend p q # ps, c) ∧ r3 ∈ upRules"
and     d: "R1 ⊆ upRules ∧ R = Ax ∪ R1"
and     "(T,n) ∈ derivable (R ∪ {r1} ∪ {r2})*"
shows   "(T,n) ∈ derivable (R ∪ {r3})*"
(*<*)
using assms
proof (induct n arbitrary:T rule:nat_less_induct)
case (1 n T)
    then have IH: "∀m<n. ∀ T. (r1 = (p # ps, c) ∧ r1 ∈ upRules ⟶
                               r2 = (q # ps, c) ∧ r2 ∈ upRules ⟶
                               r3 = (extend p q # ps, c) ∧ r3 ∈ upRules ⟶
                               R1 ⊆ upRules ∧ R = Ax ∪ R1 ⟶ 
                              (T, m) ∈ derivable (R ∪ {r1} ∪ {r2})* ⟶ 
                              (T, m) ∈ derivable (R ∪ {r3})*)" and
             prm: "(T, n) ∈ derivable (R ∪ {r1} ∪ {r2})*" by auto
    show ?case
    proof (cases n)
    case 0
        with prm have "(T,0) ∈ derivable (R ∪ {r1} ∪ {r2})*" by simp
        then have "([],T) ∈ (R ∪ {r1} ∪ {r2})*" by (rule derivable.cases) auto
        then obtain S r where ext: "extendRule S r = ([],T)" and "r ∈ (R ∪ {r1} ∪ {r2})" by (rule extRules.cases) auto
        then have "r ∈ R ∨ r = r1 ∨ r = r2" by blast
        with ext and a and b have "r ∈ R" by (auto simp add:extendRule_def)
        then have "r ∈ (R ∪ {r3})" by simp
        with ext have "([],T) ∈ (R ∪ {r3})*" using extRules.I[where r=r and R="R ∪ {r3}" and seq=S] by auto
        then have "(T,0) ∈ derivable (R ∪ {r3})*" by auto
        then show "(T,n) ∈ derivable (R ∪ {r3})*" using ‹n=0› by auto
    next
    case (Suc n')
        with prm have prm': "(T,n'+1) ∈ derivable (R ∪ {r1} ∪ {r2})*" by simp
        then obtain Ps where ne: "Ps ≠ []"
                       and   ex: "(Ps,T) ∈ (R ∪ {r1} ∪ {r2})*"
                       and   "∀ P ∈ set Ps. ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r1} ∪ {r2})*"
             using characteriseLast[where C=T and m=n' and R="(R ∪ {r1} ∪ {r2})*"] by auto
        with IH have e: "∀ P ∈ set Ps. ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*" using a b c d and prm' and ‹n = Suc n'›
             apply (auto simp add:Ball_def) by (drule_tac x=x in spec) auto
        from ex obtain S r where ext: "extendRule S r = (Ps,T)" and "r ∈ (R ∪ {r1} ∪ {r2})" by (rule extRules.cases) auto
        then have "r ∈ R ∨ r = r1 ∨ r = r2" by blast
        moreover
           {assume "r ∈ R"
            then have "r ∈ (R ∪ {r3})" by simp
            with ext have "(Ps,T) ∈ (R ∪ {r3})*" using extRules.I[where r=r and R="R ∪ {r3}" and seq=S] by auto
            with e have "(T,n'+1) ∈ derivable (R ∪ {r3})*" using ne and
                 derivable.step[where r="(Ps,T)" and R="(R ∪ {r3})*" and m=n'] by auto
           }
        moreover
           {assume "r = r1"
            with e and a and ext have "∃ m≤n'. (extend S p,m) ∈ derivable (R ∪ {r3})*"
                 by (auto simp add:extendRule_def)
            then have "∃ m≤n'. (extend S (extend q p),m) ∈ derivable (R ∪ {r3})*" 
                 using dpWeak[where R="R ∪ {r3}" and R'="R1 ∪ {r3}" and Γ="antec S + antec p" and Δ="succ S + succ p"
                              and Γ'="antec q" and Δ'="succ q"] and d c by (auto simp add:extend_def union_ac)
            moreover from e and ext and ‹r = r1› and a
                 have "∀ P ∈ set (map (extend S) ps). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 by (auto simp add:extendRule_def)
            ultimately have "∀ P ∈ set (map (extend S) (extend q p # ps)). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 by auto
            moreover have "extend q p = extend p q" by (auto simp add:extend_def union_ac)
            ultimately have pm: "∀ P ∈ set (fst (extendRule S r3)). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 using c by (auto simp add:extendRule_def)
            from ext and a and c and ‹r = r1› have con: "snd (extendRule S r3) = T" by (auto simp add:extendRule_def)
            have "r3 ∈ (R ∪ {r3})" by simp
            then have "extendRule S r3 ∈ (R ∪ {r3})*" by auto
            with pm and con and c have "(T,n'+1) ∈ derivable (R ∪ {r3})*"
                 using derivable.step[where r="extendRule S r3" and R="(R ∪ {r3})*" and m=n']
                 by (auto simp add:extendRule_def)
           }
        moreover
           {assume "r = r2"
            with e and b and ext have "∃ m≤n'. (extend S q,m) ∈ derivable (R ∪ {r3})*"
                 by (auto simp add:extendRule_def)
            then have "∃ m≤n'. (extend S (extend p q),m) ∈ derivable (R ∪ {r3})*" 
                 using dpWeak[where R="R ∪ {r3}" and R'="R1 ∪ {r3}" and Γ="antec S + antec q" and Δ="succ S + succ q"
                              and Γ'="antec p" and Δ'="succ p"] and d c by (auto simp add:extend_def union_ac)
            moreover from e and ext and ‹r = r2› and b
                 have "∀ P ∈ set (map (extend S) ps). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 by (auto simp add:extendRule_def)
            ultimately have "∀ P ∈ set (map (extend S) (extend p q # ps)). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 by auto
            then have pm: "∀ P ∈ set (fst (extendRule S r3)). ∃ m≤n'. (P,m) ∈ derivable (R ∪ {r3})*"
                 using c by (auto simp add:extendRule_def)
            from ext and b and c and ‹r = r2› have con: "snd (extendRule S r3) = T" by (auto simp add:extendRule_def)
            have "r3 ∈ (R ∪ {r3})" by simp
            then have "extendRule S r3 ∈ (R ∪ {r3})*" by auto
            with pm and con and c have "(T,n'+1) ∈ derivable (R ∪ {r3})*"
                 using derivable.step[where r="extendRule S r3" and R="(R ∪ {r3})*" and m=n']
                 by (auto simp add:extendRule_def)
           }
        ultimately show "(T,n) ∈ derivable (R ∪ {r3})*" using ‹n = Suc n'› by auto
    qed
qed
(*>*)
text‹
\section{Conclusions}

Only a portion of the formalisation was shown; a variety of intermediate lemmata were not made explicit.  This was necessary, for the \textit{Isabelle} theory files run to almost 8000 lines.  However, these files do not have to be replicated for each new calculus.  It takes very little effort to define a new calculus.  Furthermore, proving invertibility is now a quick process; less than 25 lines of proof in most cases.  
›
(*<*)
end(*>*)