# 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 *)
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.  *)
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(*>*)