# Theory NominalSequents

(*<*)
(* Author : Peter Chapman *)
section "First Order Sequents"
theory NominalSequents
imports "HOL-Library.Multiset" "HOL-Nominal.Nominal"
begin

atom_decl var

(*>*)
text‹
\section{First-Order Calculi \label{isafirstorder}}
To formalise first-order results we use the package \textit{Nominal Isabelle}.  The details, for the most part, are the same as in \S\ref{isadefs}.  However, we lose one important feature: that of polymorphism.

Recall we defined formulae as being indexed by a type of connectives.  We could then give abbreviations for these indexed formulae.  Unfortunately this feature (indexing by types) is not yet supported in \textit{Nominal Isabelle}.  Nested datatypes are also not supported.  Thus, strings are used for the connectives (both propositional and first-order) and lists of formulae are simulated to nest via a mutually recursive definition:

›

nominal_datatype form = At "nat" "var list"
| Cpd0 "string" "form_list"
| Cpd1 "string" "«var»form" ("_ (∇ [_]._)" (*<*)[100,100,100]100(*>*))
| ff
and form_list = FNil
| FCons "form" "form_list"

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

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

datatype sequent = Sequent "form multiset" "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 rule = "sequent list * sequent"

type_synonym deriv = "sequent * nat"

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

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

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

(* functions to get at components of sequents *)
primrec antec :: "sequent ⇒ form multiset" where "antec (Sequent ant suc) = ant"
primrec succ :: "sequent ⇒ form multiset" where "succ (Sequent ant suc) = suc"
primrec mset :: "sequent ⇒ form multiset" where "mset (Sequent ant suc) = ant + suc"
primrec seq_size :: "sequent ⇒ nat" where "seq_size (Sequent ant suc) = size ant + size suc"
primrec set_of_seq :: "sequent ⇒ form set" where "set_of_seq (Sequent ant suc) = set_mset (mset (Sequent ant suc))"
primrec set_of_prem :: "sequent list ⇒ form set" where
"set_of_prem Nil = {}"
| "set_of_prem (p # ps) = set_of_seq p ∪ set_of_prem ps"

(* 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 :: "rule set ⇒ bool"
where "uniqueConclusion R ≡ ∀ r1 ∈ R. ∀ r2 ∈ R. (snd r1 = snd r2) ⟶ (r1 =r2)"

end

primrec sequentMinus :: "sequent ⇒ form ⇒ sequent" ("_ - _" [100,100]100) where
"(Γ ⇒* Δ) - A = (Γ ⊖ A ⇒* Δ ⊖ A)"

primrec listMinus :: "sequent list ⇒ form ⇒ sequent list" (" _ - _ " [100,100]100) where
"[] - A = []"
| "(P # Ps) - A = (P - A) # (Ps - A)"

(* The formulation of various rule sets *)

(* idRules is the set containing all identity RULES *)
inductive_set "Ax" where
id[intro]: "([], \<LM> At i xs \<RM> ⇒* \<LM> At i xs \<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> Cpd0 R Fs \<RM> ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"
(*>*)

text‹
\noindent Formulae are quantified over a single variable at a time.  This is a restriction imposed by \textit{Nominal Isabelle}.

There are two new \SC rule sets in addition to the propositional rule set: first-order rules without a freshness proviso and first-order rules with a freshness proviso.  Freshness provisos are particularly easy to encode in \textit{Nominal Isabelle}.  We also show that the rules with a freshness proviso form a subset of the first-order rules.  The function \texttt{set-of-prem} takes a list of premisses, and returns all the formulae in that list:
›

(* provRules is the set of rules where we have a freshness proviso *)
inductive_set "provRules" where
(*<*) I[intro]:(*>*) "⟦ mset c = \<LM> F ∇ [x].A \<RM> ; ps ≠ [] ; x ♯ set_of_prem (ps - A)⟧
⟹ (ps,c) ∈ provRules"

(* nprovRules is the set of rules where we do not have a freshness proviso, but we have
a first order formula *)
inductive_set "nprovRules" where
(*<*)I[intro]:(*>*) "⟦ mset c = \<LM> F ∇ [x].A \<RM> ; ps ≠ [] ⟧
⟹ (ps,c) ∈ nprovRules"

(* provRules are a subset of nprovRules *)
lemma nprovContain:
shows "provRules ⊆ nprovRules"
proof-
{fix ps c
assume "(ps,c) ∈ provRules"
then have "(ps,c) ∈ nprovRules" by (cases) auto
}
then show ?thesis by auto
qed
(*<*)
primrec subst :: "var ⇒ var ⇒ var list ⇒ var list" ("[_;_]_" [100,100,100] 100) where
Empt:"[z;y][] = []"
| NEmpt:"[z;y](x#ys) = (if x=y then (z#([z;y]ys)) else (x#([z;y]ys)))"

lemma subst_var_list_eqvt[eqvt]:
fixes pi::"var prm"
and   y::"var list"
shows "pi∙([z;x]y) = [(pi∙z);(pi∙x)](pi∙y)"
by (induct y) (auto simp add: eqvts)
(*>*)

text‹
\noindent Substitution is defined in the usual way:›

nominal_primrec
subst_form  :: "var ⇒ var ⇒ form ⇒ form" ("[_,_]_"(*<*) [100,100,100] 100(*>*))
and subst_forms :: "var ⇒ var ⇒ form_list ⇒ form_list" ("[_,_]_"(*<*) [100,100,100] 100(*>*))
where
"[z,y](At P xs) = At P ([z;y]xs)"
|  "x♯(z,y) ⟹ [z,y](F ∇ [x].A) = F ∇ [x].([z,y]A)"
|  "[z,y](Cpd0 F Fs) = Cpd0 F ([z,y]Fs)"
|  "[z,y]ff = ff"
|  "[z,y]FNil = FNil"
|  "[z,y](FCons f Fs) = FCons ([z,y]f) ([z,y]Fs)"
(*<*)
apply(finite_guess)+
apply(rule TrueI)+
done
(*>*)

text‹\noindent Substitution is extended to multisets in the obvious way.

To formalise the condition no specific substitutions'', an inductive predicate is introduced.  If some formula in the multiset $\Gamma$ is a non-trivial substitution, then \texttt{multSubst} $\Gamma$:
›

definition multSubst :: "form multiset ⇒ bool" where
multSubst_def: "multSubst Γ ≡ (∃ A ∈ (set_mset Γ). ∃ x y B. [y,x]B = A ∧ y≠x)"

text‹
\noindent The notation $[z;y]xs$ stands for substitution of a variable in a variable list.  The details are simple, and so are not shown.

Extending the rule sets with passive parts depends upon which kind of active part is being extended.  The active parts with freshness contexts have additional constraints upon the multisets which are added:
›

(* We need to be careful now about how to extend a rule, since we have binding *)
inductive_set extRules :: "rule set ⇒ rule set"   (" _*" )
for R :: "rule set"
where
id(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ Ax ⟧ ⟹ extendRule S r ∈ R*"
| sc(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ upRules ⟧ ⟹ extendRule S r ∈ R*"
| np(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ nprovRules ⟧ ⟹ extendRule S r ∈ R*"
| p(*<*)[intro](*>*):     "⟦ (ps,c) ∈ R ; (ps,c) ∈ provRules ; mset c = \<LM> F ∇ [x].A \<RM> ; x ♯ set_of_seq S ⟧
⟹ extendRule S (ps,c) ∈ 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 :: "rule ⇒ form ⇒ bool"
where
sc[intro]: "⟦ C = (\<LM>A\<RM> ⇒* \<Empt>) ; A ≠ ff ⟧  ⟹
leftPrincipal (Ps,C) A"

inductive rightPrincipal :: "rule ⇒ form ⇒ bool"
where
sc[intro]: "C = (\<Empt> ⇒* \<LM>A\<RM>) ⟹ rightPrincipal (Ps,C) A"

(* 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 :: "rule set ⇒ deriv set"
for R :: "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"

(* Characterisation of a sequent *)
lemma characteriseSeq:
shows "∃ A B. (C :: 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 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 xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⇒* Δ)"
shows "At i xs ∈# Γ ∧ At i xs ∈# Δ"
using assms
proof-
from assms have "∃ Γ' Δ'. Γ = Γ' ⊕ At i xs ∧ Δ = Δ' ⊕ At i xs"
using extend_def[where forms=S and seq="\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<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 idscRules *)
lemma containID:
assumes a:"At i xs ∈# Γ ∧ At i xs ∈# Δ"
and b:"Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ At i xs ⊕ At i xs ∧ Δ = Δ ⊖ At i xs ⊕ At i xs" by auto
then have "extend ((Γ ⊖ At i xs) ⇒* (Δ ⊖ At i xs)) (\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⇒* Δ)"
using extend_def[where forms="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs" and seq="\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>"] by auto
moreover
have "([],\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) ∈ R" using b by auto
ultimately
have "([],Γ ⇒* Δ) ∈ extRules R"
using extRules.id[where R=R and r="([],  \<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)" and S="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs"]
and extendRule_def[where forms="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs" and R="([],  \<LM>At i xs\<RM> ⇒* \<LM>At i xs\<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.id[where R=R and r="([],  \<LM>ff\<RM> ⇒* \<Empt>)" and S="Γ ⊖ 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 xs. r = ([], \<LM> At i xs\<RM> ⇒* \<LM> At i xs\<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
proof (cases)
case base
then show "∃ Ps. Ps ≠ [] ∧
(Ps,C) ∈ R ∧
(∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)" using assms by simp
next
case (step r n)
then obtain Ps where "r = (Ps,C)" and "m=n" by (cases r) (auto)
then have "fst r = Ps" and "snd r = C" by auto
then show "∃ Ps. Ps ≠ [] ∧
(Ps,C) ∈ R ∧
(∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)"
using ‹r ∈ R› and ‹m=n› and step(4,5)
by (rule_tac x=Ps in exI) (auto)
qed

lemma propRuleCharacterise:
assumes "(Ps,C) ∈ upRules"
shows "∃ F Fs. C = (\<Empt> ⇒* \<LM>Cpd0 F Fs\<RM>) ∨ C = (\<LM>Cpd0 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>Cpd0 F Fs\<RM>) ∨ C = (\<LM>Cpd0 F Fs\<RM> ⇒* \<Empt>)"
using ‹mset C ≡ \<LM>Cpd0 F Fs\<RM>› and ‹C = (Γ ⇒* Δ)›
and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="Cpd0 F Fs"]
by auto
qed

lemma provRuleCharacterise:
assumes "(Ps,C) ∈ provRules"
shows "∃ F x A. (C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem (Ps - A)"
using assms
proof (cases)
case (I F x A)
then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
then have "(Ps,Γ ⇒* Δ) ∈ provRules" using assms by simp
then show "∃ F x A. (C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem (Ps - A)"
using ‹mset C = \<LM> F ∇ [x].A \<RM>› and ‹C = (Γ ⇒* Δ)› and ‹x ♯ set_of_prem (Ps - A)›
and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="F ∇ [x].A"]
by auto
qed

lemma nprovRuleCharacterise:
assumes "(Ps,C) ∈ nprovRules"
shows "∃ F x A. C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)"
using assms
proof (cases)
case (I F x A)
then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
then have "(Ps,Γ ⇒* Δ) ∈ nprovRules" using assms by simp
then show "∃ F x A. C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)"
using ‹mset C = \<LM> F ∇ [x].A \<RM>› and ‹C = (Γ ⇒* Δ)›
and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="F ∇ [x].A"]
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 finSeqSet:
fixes S :: "sequent"
shows "finite (set_of_seq S)"
proof-
obtain Γ Δ where "S = (Γ ⇒* Δ)" by (cases S) auto
then show ?thesis by (auto simp add:finite_set_mset)
qed

lemma finPremSet:
fixes Ps :: "sequent list"
shows "finite (set_of_prem Ps)"
by (induct Ps) (auto simp add:finSeqSet)

lemma finSupp:
fixes A :: "form" and As :: "form_list"
shows "finite ((supp A) :: var set)" and "finite ((supp As) :: var set)"
proof (nominal_induct A and As rule:form_form_list.strong_inducts)
print_cases
case (At n xs)
have "finite (set xs :: var set)" by (induct xs) auto
moreover have "set xs = (supp xs :: var set)" by (induct xs) (auto simp add:supp_list_nil supp_set_empty supp_list_cons supp_atm)
ultimately have "finite (supp xs :: var set)" by auto
moreover have "supp (At n xs) = supp n ∪ (supp xs :: var set)" using form.supp(1)[where ?x2.0=n and ?x1.0=xs] by auto
then have "supp (At n xs) = (supp xs :: var set)" using supp_nat[where n=n] by force
ultimately show ?case by auto
next
case FNil
have "supp FNil = ({} :: var set)" using form_list.supp by auto
then show ?case by auto
next
case (FCons F Fs)
then show ?case using form_list.supp by auto
next
case (Cpd0 Str Fs)
then show ?case using form.supp(2)[where ?x2.0="Str" and ?x1.0=Fs] and supp_string[where s=Str] by auto
next
case (Cpd1 F x B)
from ‹finite (supp B)› have "supp ([x].B) = supp B - {x}" using abs_fun_supp[OF pt_var_inst, OF at_var_inst] by auto
then show ?case using form.supp(3)[where ?x3.0=F and ?x1.0=x and ?x2.0=B] and supp_string[where s=F]
and ‹finite (supp B)› by force
next
case ff
then show ?case using form.supp by auto
qed

lemma getFresh:
fixes x :: "var" and A :: "form" and S :: "sequent" and Ps :: "sequent list"
shows "∃ (y :: var). y ♯ x ∧ y ♯ A ∧ y ♯ set_of_seq S ∧ y ♯ set_of_prem Ps"
proof-
have "finite ({A} ∪ set_of_seq S ∪ set_of_prem Ps)" using finSeqSet and finPremSet by auto
then have "finite (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) :: var set)"
using finSupp(1) and supp_of_fin_sets[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,
where X="({A} ∪ set_of_seq S ∪ set_of_prem Ps)"]
by auto
then have "finite (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x :: var set)" using supp_atm by auto
then obtain y where "y ∉ (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x :: var set)"
using ex_in_inf[OF at_var_inst,where A="supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x"] by auto
then have "y ∉ supp x ∧ y ∉ supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps)" by auto
then have "y ♯ ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∧ y ♯ x" using fresh_def[where a=y and x=x]
and fresh_def[where a=y and x="{A} ∪ set_of_seq S ∪ set_of_prem Ps"] by auto
then have "y ♯ A ∧ y ♯ (set_of_seq S ∪ set_of_prem Ps) ∧ y ♯ x"
using fresh_fin_insert[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,where X="set_of_seq S ∪ set_of_prem Ps" and x=A]
and finSeqSet and finPremSet by auto
then have "y ♯ A ∧ y ♯ set_of_seq S ∧ y ♯ set_of_prem Ps ∧ y ♯ x"
using fresh_fin_union[OF pt_var_inst,OF at_var_inst, OF fs_var_inst, where X="set_of_seq S" and Y="set_of_prem Ps"]
and finSeqSet and finPremSet by auto
then show ?thesis by auto
qed

lemma switchAux:
fixes Xs :: "var list"
assumes "y ♯ Xs"
shows "[y;x]Xs = [(y,x)]∙Xs"
using assms
proof (induct Xs)
print_cases
case Nil
then show ?case using nil_eqvt by auto
next
case (Cons a As)
then have "y ♯ a ∧ y ♯ As" and "[y;x]As = [(y,x)]∙As"
using fresh_list_cons[where a=y and x=a and xs=As] by auto
then show ?case using NEmpt[where z=y and y=x and x=a and ys= As]
and cons_eqvt[where pi="[(y,x)]" and x=a and xs=As] by (perm_simp add:fresh_atm)
qed

lemma switch:
fixes A :: "form" and As :: "form_list"
shows "y ♯ A ⟹ [y,x]A = [(y,x)]∙A" and "y ♯ As ⟹ [y,x]As = [(y,x)]∙As"
proof (nominal_induct A and As avoiding: x y rule:form_form_list.strong_inducts)
case (At n xs s t)
then have "t ♯ xs" using form.fresh by auto
then show ?case using perm_nat_def[where pi="[(t,s)]" and i=n] and switchAux[where y=t and Xs=xs]
by auto
next
case FNil
then show ?case by auto
next
case (FCons B Bs s t)
then show ?case by auto
next
case (Cpd0 Str Bs s t)
then show ?case using Cpd0.hyps[where ba=t and b=s] and form.fresh
and perm_string[where s="Str" and pi="[(t,s)]"] by auto
next
case (Cpd1 F a B s t)
then have "t ♯ B" using form.fresh(3)[where ?x3.0=F and ?x1.0=a and ?x2.0=B and a=t]
and fresh_atm[where a=a and b=t] and fresh_string[where a=t and s=F]
and fresh_abs_funE[OF pt_var_inst, OF at_var_inst,where x=B and b=t and a=a]
and finSupp(1)[where A=B] by auto
then show ?case using Cpd1(4)[where ba=t and b=s] and form.fresh and Cpd1(1,2)
and perm_string[where pi="[(t,s)]" and s=F] and fresh_atm by perm_simp
next
case ff
then show ?case by auto
qed
(*>*)

text‹
\noindent The final clause says we can only use an $S$ which is suitable fresh.

The only lemma which is unique to first-order calculi is the Substitution Lemma.  We show the crucial step in the proof; namely that one can substitute a fresh variable into a formula and the resultant formula is unchanged.  The proof is not particularly edifying and is omitted:
›

lemma formSubst:
shows "y ♯ x ∧ y ♯ A ⟹ F ∇ [x].A = F ∇ [y].([y,x]A)"
(*<*)
proof-
assume "y ♯ x ∧ y ♯ A" then have "[x].A = [y].([y,x]A)"
using abs_fun_eq3[OF pt_var_inst, OF at_var_inst,where x="[y,x]A" and y=A and a=y and b=x]
and switch(1)[where y=y and A=A and x=x] and fresh_atm[where a=y and b=x] by (perm_simp)
then show ?thesis using form.inject(3) by auto
qed
(*>*)

text‹
\noindent  Using the above lemma, we can change any sequent to an equivalent new sequent which does not contain certain variables.  Therefore, we can extend with any sequent:
›

lemma extend_for_any_seq:
fixes S :: "sequent"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ nprovRules ∧ R3 ⊆ provRules"
and rules2: "R = Ax ∪ R1 ∪ R2 ∪ R3"
and rin: "r ∈ R"
shows "extendRule S r ∈ R*"
(*<*)
proof-
from rin and rules2 have "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" by auto
moreover
{assume "r ∈ Ax"
then have "extendRule S r ∈ R*" using extRules.id[where r=r and R=R and S=S] and rin by auto
}
moreover
{assume "r ∈ R1"
then have "r ∈ upRules" using rules by auto
then have "extendRule S r ∈ R*" using extRules.sc[where r=r and R=R and S=S] and rin by auto
}
moreover
{assume "r ∈ R2"
then have "r ∈ nprovRules" using rules by auto
then have "extendRule S r ∈ R*" using extRules.np[where r=r and R=R and S=S] and rin by auto
}
moreover

{(*>*)
txt‹\noindent  We only show the interesting case: where the last inference had a freshness proviso:›

assume "r ∈ R3"
then have "r ∈ provRules" using rules by auto
obtain ps c where "r = (ps,c)" by (cases r) auto
then have r1: "(ps,c) ∈ R"
and r2: "(ps,c) ∈ provRules" using ‹r ∈ provRules› and rin by auto
with ‹r = (ps,c)› obtain F x A
where "(c = ( \<Empt> ⇒* \<LM>F ∇ [x].A\<RM>) ∨
c = ( \<LM>F ∇ [x].A\<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem ( ps - A )"
using provRuleCharacterise(*<*)[where Ps=ps and C=c](*>*) and ‹r ∈ provRules› by auto
then have "mset c = \<LM> F ∇ [x].A \<RM> ∧ x ♯ set_of_prem (ps - A)" (*<*)using mset.simps(*>*) by auto
moreover obtain y where fr:  "y ♯ x ∧
y ♯ A ∧
y ♯ set_of_seq S ∧
(y :: var) ♯ set_of_prem (ps-A)"
using getFresh(*<*)[where x=x and A=A and S=S and Ps="ps-A"](*>*) by auto
then have fr2: "y ♯ set_of_seq S" by auto
ultimately have "mset c = \<LM> F ∇ [y].([y,x]A) \<RM> ∧ y ♯ set_of_prem (ps - A)"
using formSubst and fr by auto
then have "mset c = \<LM> F ∇ [y].([y,x]A) \<RM>" by auto
then have "extendRule S (ps,c) ∈ R*" using r1 and r2 and fr2
and extRules.p(*<*)[where ps=ps and c=c and R=R and F=F and x=y and A="[y,x]A" and S=S](*>*) by auto
then have "extendRule S r ∈ R*" using ‹r = (ps,c)› by simp
(*<*) }

ultimately show ?thesis by blast
qed

(* Constructing the rule set we will use.  It contains all axioms, but only a subset
of the possible logical rules. *)
lemma ruleSet:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
and "R = Ax ∪ R1 ∪ R2 ∪ R3"
and "(Ps,C) ∈ R*"
shows "∃ S r. extendRule S r = (Ps,C) ∧ (r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3 ∨ 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 ∪ R1 ∪ R2 ∪ R3› have "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3 ∨ r ∈ Ax" by blast
ultimately show ?thesis by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
qed

(* Non-principal rule lemma *)
lemma nonPrincipalInvertRight:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
and "R = Ax ∪ R1 ∪ R2 ∪ R3" and "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" and "r = (ps,c)"
and IH: "∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ F ∇ [x].A, m) ∈ derivable R* ⟶
(∀r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
(¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
(∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
and a': "(Γ ⇒* Δ ⊕ F ∇ [x].A,n) ∈ derivable R*"
and b': "∀ r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
and np: "¬ rightPrincipal r (F ∇ [x].A)"
and ext: "extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)"
and num: "n = n' + 1"
and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
and nonempty: "Ps ≠ []"
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
proof-
from ext obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
from ‹r = (ps,c)› obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
then have "\<LM> F ∇ [x].A  \<RM> ≠ H" using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3›
proof-
{assume "r ∈ R1" then have "r ∈ upRules" using ‹R1 ⊆ upRules› by auto
with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>) ∨ c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
using propRuleCharacterise[where Ps=ps and C=c] by auto
moreover
{assume "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>)"
with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ H" by auto
}
moreover
{assume "c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
then have "\<LM>F ∇ [x].A \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
}
ultimately have "\<LM> F ∇ [x].A \<RM> ≠ H" by blast
}
moreover
{assume "r ∈ R2 ∨ r ∈ R3"
then have "r ∈ provRules ∨ r ∈ nprovRules" using ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
with ‹r = (ps,c)› obtain T y B where "c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>) ∨ c = (\<LM> T ∇ [y].B\<RM> ⇒* \<Empt>)"
using provRuleCharacterise[where Ps=ps and C=c]
and nprovRuleCharacterise[where Ps=ps and C=c] by auto
moreover
{assume "c = (\<Empt> ⇒* \<LM> T ∇ [y].B\<RM>)"
then have "rightPrincipal r (T ∇ [y].B)" using ‹r = (ps,c)› by auto
with ‹¬ rightPrincipal r (F ∇ [x].A)› have "T ∇ [y].B ≠ F ∇ [x].A" by auto
with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ H" using ‹c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>)› by auto
}
moreover
{assume "c = (\<LM>T ∇ [y].B \<RM> ⇒* \<Empt>)"
then have "\<LM>F ∇ [x].A \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
}
ultimately have "\<LM> F ∇ [x].A \<RM> ≠ H" by blast
}
ultimately show ?thesis using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› by blast
qed
moreover have "succ S + succ (snd r) = (Δ ⊕ F ∇ [x].A)"
using ext and extendRule_def[where forms=S and R=r]
and extend_def[where forms=S and seq="snd r"] by auto
then have "Ψ + H = Δ ⊕ F ∇ [x].A" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
moreover from ‹r = (ps,c)› and ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules›
and ‹R3 ⊆ provRules› have "(ps,c) ∈ upRules ∨ (ps,c) ∈ nprovRules ∨ (ps,c) ∈ provRules" by auto
then have "∃ A. c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)"
using propRuleCharacterise[where Ps=ps and C=c]
and nprovRuleCharacterise[where Ps=ps and C=c]
and provRuleCharacterise[where Ps=ps and C=c] by auto
then have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" using ‹c = (G ⇒* H)› by auto
ultimately have "F ∇ [x].A ∈# Ψ"
proof-
have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
moreover
{assume "H = \<Empt>"
then have "Ψ = Δ ⊕ F ∇ [x].A" using ‹Ψ + H = Δ ⊕ F ∇ [x].A› by auto
then have "F ∇ [x].A ∈# Ψ" by auto
}
moreover
{assume "∃ A. H = \<LM>A\<RM>"
then obtain T where "H = \<LM>T\<RM>" by auto
then have "Ψ ⊕ T = Δ ⊕ F ∇ [x].A" using ‹Ψ + H = Δ ⊕ F ∇ [x].A› by auto
then have "set_mset (Ψ ⊕ T) = set_mset (Δ ⊕ F ∇ [x].A)" by auto
then have "set_mset Ψ ∪ {T} = set_mset Δ ∪ {F ∇ [x].A}" by auto
moreover from ‹H = \<LM>T\<RM>› and ‹\<LM>F ∇ [x].A\<RM> ≠ H› have "F ∇ [x].A ≠ T" by auto
ultimately have "F ∇ [x].A ∈ set_mset Ψ" by auto
then have "F ∇ [x].A ∈# Ψ" by auto
}
ultimately show "F ∇ [x].A ∈# Ψ" by blast
qed
then have "∃ Ψ1. Ψ = Ψ1 ⊕ F ∇ [x].A"
by (rule_tac x="Ψ ⊖ F ∇ [x].A" in exI) (auto simp add:multiset_eq_iff)
then obtain Ψ1 where "S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)" using ‹S = (Φ ⇒* Ψ)› by auto
have "Ps = map (extend S) ps"
using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)› and extendRule_def 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. (F ∇ [x].A ∈# succ p)"
using ‹F ∇ [x].A ∈# Ψ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def)
by (drule_tac x=xa in spec) (auto simp add:extend_def)
then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)" using characteriseSeq
apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec,simp)
apply (rule_tac x="antec xa" in exI,rule_tac x="succ xa ⊖ F ∇ [x].A" in exI)
by (drule_tac x=xa in meta_spec) (auto simp add:multiset_eq_iff)
with all have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A,n) ∈ derivable R* ∧ p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R* ∧ p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
using num and b' and IH and c'
apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec) apply simp
apply hypsubst_thin
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 conjE) by (rule_tac x=m' in exI) (arith)
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 nonempty by auto
from ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› have "r ∈ R" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3› by auto
then have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r ∈ R*" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3›
and extend_for_any_seq[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and r=r and S="Φ + Γ' ⇒* Ψ1 + Δ'"]
and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
moreover have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
using ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ F ∇ [x].A)›
and ‹r = (ps,c)› and eq
by (auto simp add:extendRule_def extend_def union_ac)
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 by (simp add:Ball_def)
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› by (auto simp add:Ball_def Bex_def)
then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
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 by (auto simp add:Ball_def Bex_def)
have "∀ Φ' Ψ'. (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
proof-
{fix Φ' Ψ'
assume "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps"
then have "∃ p ∈ set ps. extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
using ‹Ps = map (extend S) ps› and ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› and a1 and d1
apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec)
by (drule_tac x="Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec) (auto)
then obtain p where t:"p ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) p"
apply auto by (drule_tac x=p in meta_spec) (simp)
then obtain D B where "p = (D ⇒* B)" by (cases p)
then have "(D ⇒* B) ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B)"
using t by auto
then have ant: "Φ' = Φ + D" and suc: "Ψ' ⊕ F ∇ [x].A = Ψ1 ⊕ F ∇ [x].A + B" using extend_def by auto
from ant have "Φ' + Γ' = (Φ + Γ') + D" 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 + Δ') (D ⇒* B)" using extend_def by auto
moreover have "extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B) ∈ set Ps'" using ‹p = (D ⇒* B)› and t and c2 by auto
ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
}
thus ?thesis by blast
qed
moreover
have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ 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 D B where "p = (D ⇒* B)" by (cases p)
then have "(D ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B)"
using t by auto
then have ant: "Φ' + Γ' = Φ + Γ' + D" and suc: "Ψ' + Δ' = Ψ1 + Δ' + B" using extend_def by auto
from ant have "Φ' + Γ' = (Φ + D) + Γ'" by (auto simp add:union_ac)
then have "Φ' = Φ + D" by simp
moreover
from suc have "Ψ' + Δ' = (Ψ1 + B) + Δ'" by (auto simp add:union_ac)
then have "Ψ' = Ψ1 + B" by simp
then have "Ψ' ⊕ F ∇ [x].A = (Ψ1 ⊕ F ∇ [x].A) + B" by (auto simp add:union_ac)
ultimately have "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B)"
using extend_def by auto
moreover have "extend (Φ  ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B) ∈ set Ps" using ‹p = (D ⇒* B)› and t and c1
and ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› by auto
ultimately have "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps" by simp
}
thus ?thesis by blast
qed
ultimately
have "∀ Φ' Ψ'. ((Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ 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=xa in spec) apply simp
apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
by (drule_tac x="Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec) (simp)
then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using num
and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› and ‹Ps' ≠ []›
and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"]
qed

(* Non-principal Left *)
lemma nonPrincipalInvertLeft:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
and "R = Ax ∪ R1 ∪ R2 ∪ R3" and "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" and "r = (ps,c)"
and IH: "∀m<n. ∀Γ Δ. ( Γ ⊕ F ∇ [x].A ⇒* Δ, m) ∈ derivable R* ⟶
(∀r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
(¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
(∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
and a': "(Γ ⊕ F ∇ [x].A ⇒* Δ,n) ∈ derivable R*"
and b': "∀ r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
and np: "¬ leftPrincipal r (F ∇ [x].A)"
and ext: "extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)"
and num: "n = n' + 1"
and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
and nonempty: "Ps ≠ []"
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
proof-
from ext obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
from ‹r = (ps,c)› obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
then have "\<LM> F ∇ [x].A  \<RM> ≠ G" using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3›
proof-
{assume "r ∈ R1" then have "r ∈ upRules" using ‹R1 ⊆ upRules› by auto
with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>) ∨ c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
using propRuleCharacterise[where Ps=ps and C=c] by auto
moreover
{assume "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>)"
with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ G" by auto
}
moreover
{assume "c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
then have "\<LM>F ∇ [x].A \<RM> ≠ G" using ‹c = (G ⇒* H)› by auto
}
ultimately have "\<LM> F ∇ [x].A \<RM> ≠ G" by blast
}
moreover
{assume "r ∈ R2 ∨ r ∈ R3"
then have "r ∈ provRules ∨ r ∈ nprovRules" using ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
with ‹r = (ps,c)› obtain T y B where "c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>) ∨ c = (\<LM> T ∇ [y].B\<RM> ⇒* \<Empt>)"
using provRuleCharacterise[where Ps=ps and C=c]
and nprovRuleCharacterise[where Ps=ps and C=c] by auto
moreover
{assume "c = (\<Empt> ⇒* \<LM> T ∇ [y].B\<RM>)"
then have "\<LM>F ∇ [x].A \<RM> ≠ G" using ‹c = (G ⇒* H)› by auto
}
moreover
{assume "c = (\<LM>T ∇ [y].B \<RM> ⇒* \<Empt>)"
then have "leftPrincipal r (T ∇ [y].B)" using ‹r = (ps,c)› by auto
with ‹¬ leftPrincipal r (F ∇ [x].A)› have "T ∇ [y].B ≠ F ∇ [x].A" by auto
with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ G" using ‹c = (\<LM> T ∇ [y].B \<RM> ⇒* \<Empt>)› by auto
}
ultimately have "\<LM> F ∇ [x].A \<RM> ≠ G"