# Theory MultiSequents

(* Author : Peter Chapman *)
(*<*)
section "Multisuccedent Sequents"

theory MultiSequents
imports "HOL-Library.Multiset"
begin
(*>*)

text‹
\section{Introduction}
In this paper, we give an overview of some results about invertibility in sequent calculi.  The framework is outlined in \S\ref{isadefs}.  The results are mainly concerned with multisuccedent calculi that have a single principal formula.  We will use, as our running example throughout, the calculus \textbf{G3cp}.  In \S\ref{isasingle}, we look at the formalisation of single-succedent calculi; in \S\ref{isafirstorder}, the formalisation in \textit{Nominal Isabelle} for first-order calculi is shown; in \S\ref{isamodal} the results for modal logic are examined.  We return to multisuccedent calculi in \S\ref{isaSRC} to look at manipulating rule sets.

\subsection{Formulae and Sequents \label{isaformulae}}
A \textit{formula} is either a propositional variable, the constant $\bot$, or a connective applied to a list of formulae.  We thus have a type variable indexing formulae, where the type variable will be a set of connectives.  In the usual way, we index propositional variables by use of natural numbers.  So, formulae are given by the datatype:
›

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

text‹
\noindent For \textbf{G3cp}, we define the datatype $Gp$, and give the following abbreviations:
›

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE
--------------------------------------------
-------------------------------------------- *)
(* Try a small example with conjunction and disjunction *)
datatype Gp = con | dis | imp
type_synonym Gp_form = "Gp form"

abbreviation con_form (infixl "∧*" 80) where
"p ∧* q ≡ Compound con [p,q]"

abbreviation dis_form (infixl "∨*" 80) where
"p ∨* q ≡ Compound dis [p,q]"

abbreviation imp_form (infixl "⊃" 80) where
"p ⊃ q  ≡ Compound imp [p,q]"
(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE ENDS
--------------------------------------------
-------------------------------------------- *)
(*<*)
abbreviation multiset_abbrev ("\<LM> _  \<RM>" [75]75) where
"\<LM> A \<RM> ≡ {# A #}"

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

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

(* 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"

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

text‹
\noindent A \textit{sequent} is a pair of multisets of formulae.  Sequents are indexed by the connectives used to index the formulae.  To add a single formula to a multiset of formulae, we use the symbol $\oplus$, whereas to join two multisets, we use the symbol $+$.

\subsection{Rules and Rule Sets \label{isarules}}
A \textit{rule} is a list of sequents (called the premisses) paired with a sequent (called the conclusion).  The two \textit{rule sets} used for multisuccedent calculi are the axioms, and the \SC rules (i.e. rules having one principal formula).  Both are defined as inductive sets.  There are two clauses for axioms, corresponding to $L\bot$ and normal axioms:

›
inductive_set "Ax" where
id(*<*)[intro](*>*): "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ Ax"
|  Lbot(*<*)[intro](*>*): "([], \<LM> ff \<RM> ⇒* \<Empt>) ∈ Ax"

text‹
\noindent The set of \SC rules, on the other hand, must not have empty premisses, and must have a single, compound formula in its conclusion.  The function \texttt{mset} takes a sequent, and returns the multiset obtained by adding the antecedent and the succedent together:
›

(* 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"

text‹
\noindent For \textbf{G3cp}, we have the following six rules, which we then show are a subset of the set of \SC rules:
›

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE
--------------------------------------------
-------------------------------------------- *)

inductive_set "g3cp"
where
conL(*<*)[intro](*>*): "([\<LM> A \<RM> + \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ∧* B \<RM> ⇒* \<Empt>) ∈ g3cp"
|   conR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM>, \<Empt> ⇒* \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ∧* B \<RM>) ∈ g3cp"
|   disL(*<*)[intro](*>*): "([\<LM> A \<RM> ⇒* \<Empt>, \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ∨* B\<RM> ⇒* \<Empt>) ∈ g3cp"
|   disR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM> + \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ∨* B \<RM>) ∈ g3cp"
|   impL(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM>, \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ⊃ B \<RM> ⇒* \<Empt>) ∈ g3cp"
|   impR(*<*)[intro](*>*): "([\<LM> A \<RM> ⇒* \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ⊃ B \<RM>) ∈ g3cp"

lemma g3cp_upRules:
shows "g3cp ⊆ upRules"
proof-
{
fix ps c
assume "(ps,c) ∈ g3cp"
then have "(ps,c) ∈ upRules" by (induct) auto
}
thus "g3cp ⊆ upRules" by auto
qed

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE ENDS
--------------------------------------------
-------------------------------------------- *)

text‹
\noindent We have thus given the \textit{active} parts of the \textbf{G3cp} calculus.  We now need to extend these active parts with \textit{passive} parts.

Given a sequent $C$, we extend it with another sequent $S$ by adding the two antecedents and the two succedents.  To extend an active part $(Ps,C)$ with a sequent $S$, we extend every $P \in Ps$ and $C$ with $S$:
›

(* Extend a sequent, and then a rule by adding seq to all premisses and the conclusion *)
extend ≡ extend
extendRule ≡ extendRule
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))"

end

text‹
\noindent Given a rule set $\mathcal{R}$, the \textit{extension} of $\mathcal{R}$, called $\mathcal{R}^{\star}$, is then defined as another inductive set:
›

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

text‹
\noindent The rules of \textbf{G3cp} all have unique conclusions.  This is easily formalised:
›

(* 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*)
begin

definition uniqueConclusion :: "'a rule set ⇒ bool"
where "uniqueConclusion R ≡ ∀ r1 ∈ R. ∀ r2 ∈ R. (snd r1 = snd r2) ⟶ (r1 = r2)"

end

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE
--------------------------------------------
-------------------------------------------- *)
lemma g3cp_uc:
shows "uniqueConclusion g3cp"
apply (rule g3cp.cases) apply auto by (rotate_tac 1,rule g3cp.cases,auto)+
(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE ENDS
--------------------------------------------
-------------------------------------------- *)
(*<*)
(* 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)"

(*>*)

text‹
A formula $A$ is \textit{left principal} for an active part $R$ iff the conclusion of $R$ is of the form $A \Rightarrow \emptyset$.  The definition of \textit{right principal} is then obvious.  We have an inductive predicate to check these things:
›

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

text‹
\noindent As an example, we show that if $A\wedge B$ is principal for an active part in \textbf{G3cp}, then $\emptyset \Rightarrow A$ is a premiss of that active part:
›

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE
--------------------------------------------
-------------------------------------------- *)

lemma principal_means_premiss:
assumes a: "rightPrincipal r (A ∧* B)"
and     b: "r ∈ g3cp"
shows      "(\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)"
proof-
from a and b obtain Ps where req: "r = (Ps, \<Empt> ⇒* \<LM> A∧*B \<RM>)"
by (cases r) auto
with b have "Ps = [\<Empt> ⇒* \<LM> A \<RM>, \<Empt> ⇒* \<LM> B \<RM>]"
apply (cases r) by (rule g3cp.cases) auto
with req show "(\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)" by auto
qed

(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE ENDS
--------------------------------------------
-------------------------------------------- *)

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

text‹
\noindent A sequent is \textit{derivable} at height $0$ if it is the conclusion of a rule with no premisses.  If a rule has $m$ premisses, and the maximum height of the derivation of any of the premisses is $n$, then the conclusion will be derivable at height $n+1$.  We encode this as pairs of sequents and natural numbers.  A sequent $S$ is derivable at a height $n$ in a rule system $\mathcal{R}$ iff $(S,n)$ belongs to the inductive set \texttt{derivable} $\mathcal{R}$:
›

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"

text‹
\noindent In some instances, we do not care about the height of a derivation, rather that the root is derivable.  For this, we have the additional definition of \texttt{derivable'}, which is a set of sequents:
›

(* 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"

text‹
\noindent It is desirable to switch between the two notions.  Shifting from derivable at a height to derivable is simple: we delete the information about height.  The converse is more complicated and involves an induction on the length of the premiss list:
›

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
with step(3) have aa: "∀ p ∈ set ps. ∃ n. (p,n) ∈ derivable R" by auto
then have "∃ m. ∀ p ∈ set ps. ∃ n≤m. (p,n) ∈ derivable R"
proof (induct ps) ― ‹induction on the list›
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 (rule_tac x=m' in exI) apply simp
apply (drule_tac x=x in spec) apply auto(*>*) by (*<*)(rule_tac x=n in exI)(*>*) auto ― ‹max returns the maximum of two integers›
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.  *)

(* 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)"

(* 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)"

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"

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

(* -------------------------------------------
-------------------------------------------
THIS IS NOW INVERTIBLERULESPOLY.THY
-------------------------------------------
------------------------------------------- *)

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

text‹
\section{Formalising the Results \label{isaproofs}}
A variety of helper'' lemmata are used in the proofs, but they are not shown.  The proof tactics themselves are hidden in the following proof, except where they are interesting.  Indeed, only the interesting parts of the proof are shown at all.  The main result of this section is that a rule is invertible if the premisses appear as premisses of \textit{every} rule with the same principal formula.  The proof is interspersed with comments.
›

lemma rightInvertible:
fixes Γ Δ :: "'a form multiset"
assumes rules: "R' ⊆ upRules ∧ R = Ax ∪ R'"
and   a: "(Γ ⇒* Δ ⊕ Compound F Fs,n) ∈ derivable R*"
and   b: "∀ r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶
(Γ' ⇒* Δ') ∈ set (fst r')"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
using assms
txt‹
\noindent The height of derivations is decided by the length of the longest branch.  Thus, we need to use
strong induction: i.e. $\forall m\leq n.\ \textrm{If } P(m) \textrm{ then } P(n+1)$.
›
proof (induct n arbitrary:Γ Δ rule:nat_less_induct)
case (1 n Γ Δ)
then have IH:"∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ Compound F Fs, m) ∈ derivable R* ⟶
(∀r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶
( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
(∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
and a': "(Γ ⇒* Δ ⊕ Compound F Fs,n) ∈ derivable R*"
and b': "∀ r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶
(Γ' ⇒* Δ') ∈ set (fst r')"
by auto
show ?case
proof (cases n)   ― ‹Case analysis on $n$›
case 0
(*<*)    then have "(Γ ⇒* Δ ⊕ Compound F Fs,0) ∈ derivable R*" using a' by simp
then have "([],Γ ⇒* Δ ⊕ Compound F Fs) ∈ R*" by (cases) (auto)
then have "∃ r S. extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs) ∧ (r ∈ Ax ∨ r ∈ R')"
using rules and ruleSet[where R'=R' and R=R and Ps="[]" and C="Γ ⇒* Δ ⊕ Compound F Fs"] by auto(*>*)
then obtain r S where "extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs)"
and "r ∈ Ax ∨ r ∈ R'" by auto  ― ‹At height 0, the premisses are empty›
moreover
{assume "r ∈ Ax"
then obtain i where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨
r = ([], \<LM> ff \<RM> ⇒* \<Empt>)"
using characteriseAx[where r=r] by auto
moreover ― ‹Case split on the kind of axiom used›
{assume "r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>)"
(*<*)         with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs)›
have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ ⊕ Compound F Fs)"
using extendRule_def[where R="([],\<LM>At i\<RM>⇒*\<LM>At i\<RM>)" and forms=S] by auto (*>*)
then have "At i ∈# Γ ∧ At i ∈# Δ" (*<*)using extendID[where S=S and i=i and Γ=Γ and Δ="Δ ⊕ Compound F Fs"](*>*) by auto
then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules (*<*)
and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R](*>*) by auto
}
moreover
{assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
(*<*)          with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs)›
have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ ⊕ Compound F Fs)"
using extendRule_def[where R="([],\<LM>ff\<RM>⇒*\<Empt>)" and forms=S] by auto (*>*)
then have "ff ∈# Γ" (*<*)using extendFalsum[where S=S and Γ=Γ and Δ="Δ ⊕ Compound F Fs"](*>*)  by auto
then have "ff ∈# Γ + Γ'" by auto
then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules (*<*)
and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R](*>*) by auto
}
ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" by blast
}
moreover
(*<*)      then have "r ∈ upRules" using rules by auto
then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
proof-
obtain x y where "r = (x,y)" by (cases r)
with ‹r ∈ upRules› have "(x,y) ∈ upRules" by simp
then obtain Ps where "(Ps :: 'a sequent list) ≠ []" and "x=Ps" by (cases) (auto)
with ‹r = (x,y)› have "r = (Ps, y)" by simp
then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹Ps ≠ []› by blast
qed (*>*)
then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
moreover (*<*) from ‹extendRule S r = ([], Γ ⇒* Δ ⊕ Compound F Fs)› have "∃ S. r = ([],S)"
using extendRule_def[where forms=S and R=r] by (cases r) (auto)
then(*>*) obtain S where "r = ([],S)" by blast   ― ‹Contradiction›
ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules by simp
}
ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" (*<*)using ‹n=0› (*>*) by blast
(*<*)next (*>*)
txt‹\noindent In the case where $n = n' + 1$ for some $n'$, we know the premisses are empty,
and every premiss is derivable at a height lower than $n'$:›
case (Suc n')
then have "(Γ ⇒* Δ ⊕ Compound F Fs,n'+1) ∈ derivable R*" using a' by simp
then obtain Ps where "(Ps, Γ ⇒* Δ ⊕ Compound F Fs) ∈ R*" and
"Ps ≠ []" and
"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*" (*<*)
using characteriseLast[where C="Γ ⇒* Δ ⊕ Compound F Fs" and m=n' and R="R*"](*>*) by auto
(*<*)    then have "∃ r S. (r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)"
using rules and ruleSet[where R'=R' and R=R and Ps=Ps and C="Γ ⇒* Δ ⊕ Compound F Fs"] by auto (*>*)
then obtain r S where "r ∈ Ax ∨ r ∈ R'"
and "extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)" by auto
moreover
{assume "r ∈ Ax"   ― ‹Gives a contradiction›
then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
moreover obtain x y where "r = (x,y)" by (cases r)
then have "x ≠ []" using ‹Ps ≠ []›
and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)› (*<*)
and extendRule_def[where forms=S and R=r]
and extend_def[where forms=S and seq="snd r"] (*>*)by auto
ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" (*<*)
using ‹r=(x,y)›(*>*)  by auto
}
moreover
{assume "r ∈ R'"
obtain ps c where "r = (ps,c)" by (cases r) auto
(*<*)       then have "r ∈ upRules" using rules and ‹r ∈ R'› by auto (*>*)
have "(rightPrincipal r (Compound F Fs)) ∨
¬(rightPrincipal r (Compound F Fs))"
by blast  ― ‹The formula is principal, or not›
(*<*)  moreover (*>*)
txt‹\noindent If the formula is principal, then $\Gamma' \Rightarrow \Delta'$ is amongst the premisses of $r$:›
{assume "rightPrincipal r (Compound F Fs)"
then have "(Γ' ⇒* Δ') ∈ set ps" using b' (*<*)and ‹r = (ps,c)› and ‹r ∈ R'› and rules(*>*)
by auto
then have "extend S (Γ' ⇒* Δ') ∈ set Ps"
using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›
(*<*)  and ‹r = (ps,c)›(*>*) by (simp(*<*) add:extendContain(*>*))
moreover (*<*)from ‹rightPrincipal r (Compound F Fs)› have "c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)"
using ‹r = (ps,c)› by (cases) auto
with ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›(*>*) have "S = (Γ ⇒* Δ)" (*<*)
using ‹r = (ps,c)› apply (auto simp add:extendRule_def extend_def)(*>*) by (cases S) auto
ultimately have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" (*<*)using ‹n = Suc n'›(*>*) by (auto(*<*),rule_tac x=m in exI) (simp(*>*))
}
(*<*) moreover (*>*)
txt‹\noindent If the formula is not principal, then it must appear in the premisses.  The first two lines give a characterisation of the extension and conclusion, respectively.  Then, we apply the induction hypothesis
at the lower height of the premisses:›
{assume "¬ rightPrincipal r (Compound F Fs)"
obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
then obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
then have "\<LM> Compound F Fs \<RM> ≠ H"   ― ‹Proof omitted›
(*<*)                 proof-
from ‹r = (ps,c)› and ‹r ∈ upRules›
obtain T Ts where  "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
using upRuleCharacterise[where Ps=ps and C=c] by auto
moreover
{assume "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
then have "rightPrincipal r (Compound T Ts)" using ‹r = (ps,c)› by auto
with ‹¬ rightPrincipal r (Compound F Fs)› have "Compound T Ts ≠ Compound F Fs" by auto
then have "\<LM>Compound F Fs\<RM> ≠ H" using ‹c = (G ⇒* H)› and ‹c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)› by auto
}
moreover
{assume "c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
then have "\<LM>Compound F Fs\<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
}
ultimately show "\<LM>Compound F Fs\<RM> ≠ H" by blast
qed
moreover have "succ S + succ (snd r) = (Δ ⊕ Compound F Fs)"
using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›
and extendRule_def[where forms=S and R=r]
and extend_def[where forms=S and seq="snd r"] by auto
then (*>*) have "Ψ + H = Δ ⊕ Compound F Fs"
using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
moreover from ‹r = (ps,c)› and ‹c = (G ⇒* H)› (*<*)and ‹r ∈ upRules› (*>*)

have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)"(*<*)
using succ_upRule[where Ps=ps and Φ=G and Ψ=H](*>*) by auto
ultimately have "Compound F Fs ∈# Ψ"   ― ‹Proof omitted›
(*<*)                proof-
have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
moreover
{assume "H = \<Empt>"
then have "Ψ = Δ ⊕ Compound F Fs" using ‹Ψ + H = Δ ⊕ Compound F Fs› by auto
then have "Compound F Fs ∈# Ψ" by auto
}
moreover
{assume "∃ A. H = \<LM>A\<RM>"
then obtain A where "H = \<LM>A\<RM>" by auto
then have "Ψ ⊕ A = Δ ⊕ Compound F Fs" using ‹Ψ + H = Δ ⊕ Compound F Fs› by auto
then have "set_mset (Ψ ⊕ A) = set_mset (Δ ⊕ Compound F Fs)" by auto
then have "set_mset Ψ ∪ {A} = set_mset Δ ∪ {Compound F Fs}" by auto
moreover from ‹H = \<LM>A\<RM>› and ‹\<LM>Compound F Fs\<RM> ≠ H› have "Compound F Fs ≠ A" by auto
ultimately have "Compound F Fs ∈ set_mset Ψ" by auto
then have "Compound F Fs ∈# Ψ" by auto
}
ultimately show "Compound F Fs ∈# Ψ" by blast
qed (*>*)
then have "∃ Ψ1. Ψ = Ψ1 ⊕ Compound F Fs" by (*<*)(rule_tac x="Ψ ⊖ Compound F Fs" in exI)(*>*) (auto(*<*) simp add:multiset_eq_iff(*>*))
then obtain Ψ1 where "S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)"(*<*) using ‹S = (Φ ⇒* Ψ)›(*>*) by auto
(*<*)           have "Ps = map (extend S) ps"
using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›
and extendRule_def[where forms=S and R=r] and ‹r = (ps,c)› by auto
then have "∀ p ∈ set Ps. (∃ p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
then (*>*) have "∀ p ∈ set Ps. (Compound F Fs ∈# succ p)"  ― ‹Appears in every premiss›
(*<*)     using ‹Compound F Fs ∈# Ψ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) (*>*)
by (*<*)(drule_tac x=x in spec)(*>*) (auto(*<*) simp add:extend_def(*>*))
(*<*)          then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)" using characteriseSeq
apply (auto simp add:Ball_def) apply (drule_tac x=x in spec,simp)
apply (rule_tac x="antec x" in exI,rule_tac x="succ x ⊖ Compound F Fs" in exI)
by (drule_tac x=x in meta_spec) (auto simp add:multiset_eq_iff)
moreover have "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*" by fact
ultimately have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs,n) ∈ derivable R*
∧ p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)"
then have (*<*)a2:(*>*) "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧
(Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R* ∧
p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)" using (*<*)‹n = Suc n'› and b' and (*>*)IH(*<*)
apply (auto simp add:Ball_def) apply (drule_tac x=x in spec) apply simp
apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
apply (simp) apply (elim exE)(*>*) by(*<*) (rule_tac x=m' in exI)(*>*) (arith)
txt‹\noindent  To this set of new premisses, we apply a new instance of $r$, with a different extension:›
obtain Ps' where eq: "Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps" by auto
(*<*)          have "length Ps = length Ps'" using ‹Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps›
and ‹Ps = map (extend S) ps› by auto
then have "Ps' ≠ []" using ‹Ps ≠ []› by auto
from ‹r ∈ R'› have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r ∈ R*" using rules by auto
moreover have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
using ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)›
and ‹r = (ps,c)› and eq
ultimately(*>*) have "(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*" by simp
(*<*)          have c1:"∀ p ∈ set ps. extend S p ∈ set Ps" using ‹Ps = map (extend S) ps› by (simp add:Ball_def)
have c2:"∀ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p ∈ set Ps'" using eq
then have eq2:"∀ p ∈ set Ps'. ∃ Φ' Ψ'. p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq
have d1:"∀ p ∈ set Ps. ∃ p' ∈ set ps. p = extend S p'" using ‹Ps = map (extend S) ps›
then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2
moreover have d2: "∀ p ∈ set Ps'. ∃ p' ∈ set ps. p = extend (Φ + Γ' ⇒* Ψ1 + Δ') p'" using eq
then have "∀ p ∈ set Ps'. ∃ p'. p' ∈ set Ps" using c1
have "∀ Φ' Ψ'. (Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps ⟶
(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
proof-
{fix Φ' Ψ'
assume "(Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps"
then have "∃ p ∈ set ps. extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)"
using ‹Ps = map (extend S) ps› and ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› and a1 and d1
apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec)
by (drule_tac x="Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec) (auto)
then obtain p where t:"p ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) p"
apply auto by (drule_tac x=p in meta_spec) (simp)
then obtain A B where "p = (A ⇒* B)" by (cases p)
then have "(A ⇒* B) ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B)"
using t by auto
then have ant: "Φ' = Φ + A" and suc: "Ψ' ⊕ Compound F Fs = Ψ1 ⊕ Compound F Fs + B"
using extend_def[where forms="Φ ⇒* Ψ1 ⊕ Compound F Fs" and seq="A ⇒* B"] by auto
from ant have "Φ' + Γ' = (Φ + Γ') + A" by (auto simp add:union_ac)
moreover
from suc have "Ψ' = Ψ1 + B" by auto
then have "Ψ' + Δ' = (Ψ1 + Δ') + B" by (auto simp add:union_ac)
ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (A ⇒* B)"
using extend_def[where forms="Φ + Γ' ⇒* Ψ1 + Δ'" and seq="A ⇒* B"] by auto
moreover have "extend (Φ + Γ' ⇒* Ψ1 + Δ') (A ⇒* B) ∈ set Ps'" using ‹p = (A ⇒* B)› and t and c2 by auto
ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
}
thus ?thesis by blast
qed
moreover
have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps"
proof-
{fix Φ' Ψ'
assume "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
then have "∃ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p = (Φ' + Γ' ⇒* Ψ' + Δ')"
using eq and eq2 and d2
apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec)
by (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec) (auto)
then obtain p where t:"p ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') p"
apply auto by (drule_tac x=p in meta_spec) (simp)
then obtain A B where "p = (A ⇒* B)" by (cases p)
then have "(A ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (A ⇒* B)"
using t by auto
then have ant: "Φ' + Γ' = Φ + Γ' + A" and suc: "Ψ' + Δ' = Ψ1 + Δ' + B"
using extend_def[where forms="Φ + Γ' ⇒* Ψ1 + Δ'" and seq="A ⇒* B"] by auto
from ant have "Φ' + Γ' = (Φ + A) + Γ'" by (auto simp add:union_ac)
then have "Φ' = Φ + A" by simp
moreover
from suc have "Ψ' + Δ' = (Ψ1 + B) + Δ'" by (auto simp add:union_ac)
then have "Ψ' = Ψ1 + B" by simp
then have "Ψ' ⊕ Compound F Fs = (Ψ1 ⊕ Compound F Fs) + B" by (auto simp add:union_ac)
ultimately have "(Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B)"
using extend_def[where forms="Φ ⇒* Ψ1 ⊕ Compound F Fs" and seq="A⇒*B"] by auto
moreover have "extend (Φ  ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B) ∈ set Ps" using ‹p = (A ⇒* B)› and t and c1
and ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› by auto
ultimately have "(Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps" by simp
}
thus ?thesis by blast
qed
ultimately
have "∀ Φ' Ψ'. ((Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps) = ((Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps')" by auto
then have "∀ p ∈ set Ps'. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',n) ∈ derivable R*
∧ p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq2 and a2
apply (simp add:Ball_def) apply (intro allI impI) apply (drule_tac x=x in spec) apply simp
apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
by (drule_tac x="Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec) (simp) (*>*)
then have "∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
using (*<*)‹n = Suc n'› and ‹Ps' ≠ []›
and(*>*) ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› (*<*)
and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"](*>*)
(*<*)          }
ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
}(*>*)
txt‹\noindent All of the cases are now complete.›
ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
(*<*)  qed (*>*)
qed
(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE
--------------------------------------------
-------------------------------------------- *)
text‹
As an example, we show the left premiss of $R\wedge$ in \textbf{G3cp} is derivable at a height not greater than that of the conclusion.  The two results used in the proof (\texttt{principal-means-premiss} and \texttt{rightInvertible}) are those we have previously shown:
›

lemma conRInvert:
assumes "(Γ ⇒* Δ ⊕ (A ∧* B),n) ∈ derivable (g3cp ∪ Ax)*"
shows "∃ m≤n. (Γ ⇒* Δ ⊕ A,m) ∈ derivable (g3cp ∪ Ax)*"
proof-
have "∀ r ∈ g3cp. rightPrincipal r (A ∧* B) ⟶ (\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)"
using principal_means_premiss by auto
with assms show ?thesis using rightInvertible(*<*)[where R'="g3cp" and Γ'="\<Empt>" and Δ'="\<LM> A \<RM>"
and R="g3cp ∪ Ax"](*>*) by (auto(*<*) simp add:Un_commute Ball_def nonPrincipalID g3cp_upRules(*>*))
qed
(* --------------------------------------------
--------------------------------------------
G3cp EXAMPLE ENDS
--------------------------------------------
-------------------------------------------- *)

text‹
\noindent  We can obviously show the equivalent proof for left rules, too:
›

lemma leftInvertible:
fixes Γ Δ :: "'a form multiset"
assumes rules: "R' ⊆ upRules ∧ R = Ax ∪ R'"
and   a: "(Γ ⊕ Compound F Fs ⇒* Δ,n) ∈ derivable R*"
and   b: "∀ r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
(*<*)
using assms
proof (induct n arbitrary:Γ Δ rule:nat_less_induct)
case (1 n Γ Δ)
then have IH:"∀m<n. ∀Γ Δ. ( Γ ⊕ Compound F Fs ⇒* Δ, m) ∈ derivable R* ⟶
(∀r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
(∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
and a': "(Γ ⊕ Compound F Fs ⇒* Δ,n) ∈ derivable R*"
and b': "∀ r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
by auto
show ?case
proof (cases n)
case 0
then have "(Γ ⊕ Compound F Fs ⇒* Δ,0) ∈ derivable R*" using a' by simp
then have "([],Γ ⊕ Compound F Fs ⇒* Δ) ∈ R*" by (cases) (auto)
then have "∃ r S. extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ) ∧ (r ∈ Ax ∨ r ∈ R')"
using rules and ruleSet[where Ps="[]" and C="Γ ⊕ Compound F Fs ⇒* Δ" and R'=R' and R=R] by (auto)
then obtain r S where "extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ)" and "r ∈ Ax ∨ r ∈ R'" by auto
moreover
{assume "r ∈ Ax"
then obtain i where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨ r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
using characteriseAx[where r=r] by auto
moreover
{assume "r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>)"
with ‹extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ)›
have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⊕ Compound F Fs ⇒* Δ)"
using extendRule_def[where R="([],\<LM>At i\<RM>⇒*\<LM>At i\<RM>)" and forms=S] by auto
then have "At i ∈# Γ ∧ At i ∈# Δ" using extendID[where S=S and i=i and Γ="Γ ⊕ Compound F Fs" and Δ=Δ] by auto
then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R] by auto
}
moreover
{assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
with ‹extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ)›
have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⊕ Compound F Fs ⇒* Δ)"
using extendRule_def[where R="([],\<LM>ff\<RM>⇒*\<Empt>)" and forms=S] by auto
then have "ff ∈# Γ" using extendFalsum[where S=S and Γ="Γ⊕Compound F Fs" and Δ=Δ] by auto
then have "ff ∈# Γ + Γ'" by auto
then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R] by auto
}
ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" by blast
}
moreover
{assume "r ∈ R'"
then have "r ∈ upRules" using rules by auto
then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
proof-
obtain x y where "r = (x,y)" by (cases r)
with ‹r ∈ upRules› have "(x,y) ∈ upRules" by simp
then obtain Ps where "(Ps :: 'a sequent list) ≠ []" and "x=Ps" by (cases) (auto)
with ‹r = (x,y)› have "r = (Ps, y)" by simp
then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹Ps ≠ []› by blast
qed
then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
moreover from ‹extendRule S r = ([], Γ ⊕ Compound F Fs ⇒* Δ)› have "∃ S. r = ([],S)"
using extendRule_def[where forms=S and R=r] by (cases r) (auto)
then obtain S where "r = ([],S)" by blast
ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" by simp
}
ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n=0› by blast
next
case (Suc n')
then have "(Γ ⊕ Compound F Fs ⇒* Δ,n'+1) ∈ derivable R*" using a' by simp
then obtain Ps where "(Ps, Γ ⊕ Compound F Fs ⇒* Δ) ∈ R*" and
"Ps ≠ []" and
"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
using characteriseLast[where C="Γ ⊕ Compound F Fs ⇒* Δ" and m=n' and R="R*"] by auto
then have "∃ r S. (r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)"
using rules ruleSet[where R'=R' and R=R and Ps=Ps and C="Γ⊕ Compound F Fs ⇒* Δ"] by auto
then obtain r S where "r ∈ Ax ∨ r ∈ R'" and "extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)" by auto
moreover
{assume "r ∈ Ax"
then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
moreover obtain x y where "r = (x,y)" by (cases r)
then have "x ≠ []" using ‹Ps ≠ []› and ‹extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)›
and extendRule_def[where forms=S and R=r]
and