# Theory SingleSuccedent

(*<*)
(*  Author : Peter Chapman *)
section "Single Succedent"

theory SingleSuccedent
imports "HOL-Library.Multiset"
begin

(* Has the empty formula O, which will mean we can have empty right-hand sides *)
(*>*)

text‹
\section{Single Succedent Calculi \label{isasingle}}
We must be careful when restricting sequents to single succedents.  If we have sequents as a pair of multisets, where the second is restricted to having size at most 1, then how does one extend the active part of $\implies{L}{}$ from \textbf{G3ip}?  The left premiss will be $\implies{A}{B} \Rightarrow A$, and the extension will be $\Gamma \Rightarrow C$.  The \texttt{extend} function must be able to correctly choose to discard the $C$.

Rather than taking this route, we instead restrict to single formulae in the succedents of sequents.  This raises its own problems, since now how does one represent the empty succedent?  We introduce a dummy formula \texttt{Em}, which will stand for the empty formula:
›

datatype 'a form = At "nat"
| Compound "'a" "'a form list"
| ff
| Em
(*<*)
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)" (" (_) ⇒* (_)" [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" 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 *)

(*>*)
text‹
\noindent When we come to extend a sequent, say $\Gamma \Rightarrow C$, with another sequent, say $\Gamma' \Rightarrow C'$, we only overwrite'' the succedent if $C$ is the empty formula:
›
extend ≡ extend
extendRule ≡ extendRule
begin

definition extend
where "extend forms seq ≡
if (succ seq = Em)
then (antec forms + antec seq) ⇒* (succ forms)
else (antec forms + antec seq ⇒* succ seq)"

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

end

(*<*)
(* 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> ⇒* At i) ∈ Ax"
|  Lbot[intro]: "([], \<LM> ff \<RM> ⇒* Em) ∈ 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
L[intro]: "⟦ c ≡ (\<LM> Compound R Fs \<RM> ⇒* Em) ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"
|  R[intro]: "⟦ c ≡ (\<Empt> ⇒* Compound F Fs) ; 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> ⇒* Em)  ⟹
leftPrincipal (Ps,C) (Compound F Fs)"

inductive rightPrincipal :: "'a rule ⇒ 'a form ⇒ bool"
where
up[intro]: "C = (\<Empt> ⇒* Compound F Fs) ⟹ 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 by (rule_tac x=n in exI) auto
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)"

(* 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> ⇒* At i) = (Γ ⇒* Δ)"
shows "At i ∈# Γ"
using assms
proof-
from assms have "∃ Γ'. Γ = Γ' ⊕ At i"
using extend_def[where forms=S and seq="\<LM> At i \<RM> ⇒* At i"]
by (rule_tac x="antec S" in exI) auto
then show ?thesis by auto
qed

lemma extendFalsum:
assumes "extend S (\<LM> ff \<RM> ⇒* Em) = (Γ ⇒* Δ)"
shows "ff ∈# Γ"
proof-
from assms have "∃ Γ'. Γ = Γ' ⊕ ff"
using extend_def[where forms=S and seq="\<LM>ff \<RM> ⇒* Em"]
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 ∈# Γ"
and b:"Ax ⊆ R"
shows "(Γ ⇒* At i,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ At i ⊕ At i" by auto
then have "extend ((Γ ⊖ At i) ⇒* Em) (\<LM> At i \<RM> ⇒* At i) = (Γ ⇒* At i)"
using extend_def[where forms="Γ ⊖ At i ⇒* Em" and seq="\<LM>At i\<RM> ⇒* At i"] by auto
moreover
have "([],\<LM> At i \<RM> ⇒* At i) ∈ R" using b by auto
ultimately
have "([],Γ ⇒* At i) ∈ R*"
using extRules.I[where R=R and r="([],  \<LM>At i\<RM> ⇒* At i)" and seq="Γ ⊖ At i ⇒* Em"]
and extendRule_def[where forms="Γ ⊖ At i ⇒* Em" and R="([],  \<LM>At i\<RM> ⇒* At i)"] by auto
then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* At i"] by auto
qed

lemma containFalsum:
assumes a: "ff ∈# Γ"
and  b: "Ax ⊆ R"
shows "(Γ ⇒* C,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ ff ⊕ ff" by auto
then have "extend (Γ ⊖ ff ⇒* C) (\<LM>ff\<RM> ⇒* Em) = (Γ ⇒* C)"
using extend_def[where forms="Γ ⊖ ff ⇒* C" and seq="\<LM>ff\<RM> ⇒* Em"] by auto
moreover
have "([],\<LM>ff\<RM> ⇒* Em) ∈ R" using b by auto
ultimately have "([],Γ ⇒* C) ∈ R*"
using extRules.I[where R=R and r="([],  \<LM>ff\<RM> ⇒* Em)" and seq="Γ ⊖ ff ⇒* C"]
and extendRule_def[where forms="Γ ⊖ ff ⇒* C" and R="([],  \<LM>ff\<RM> ⇒* Em)"] by auto
then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* 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> ⇒* Em) ∨ (∃ i. r = ([], \<LM> At i \<RM> ⇒* At i))"
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 upRuleCharacterise:
assumes "(Ps,C) ∈ upRules"
shows "∃ F Fs. C = (\<Empt> ⇒* Compound F Fs) ∨ C = (\<LM>Compound F Fs\<RM> ⇒* Em)"
using assms by (cases) auto

lemma extendEmpty:
shows "extend (\<Empt> ⇒* Em) C = C"
apply (auto simp add:extend_def) apply (cases C) apply auto 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> ⇒* Em) ∨ r = ([], \<LM> At i \<RM> ⇒* At i)"
using characteriseAx[where r=r] by auto
{ assume "rightPrincipal r A" then obtain Ps where r2:"r = (Ps, \<Empt> ⇒* A)" 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> ⇒* Em)" by (cases r) auto
with r1 have "False" by auto
}
then have "¬ leftPrincipal r A" by auto
ultimately show ?thesis by simp
qed

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)

(* ---------------------------------------------------
---------------------------------------------------
---------------------------------------------------
---------------------------------------------------
THIS IS NOW
SingleWeakening.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

lemma dpWeak:
assumes a:"(Γ ⇒* E,n) ∈ derivable R*"
and  b: "R' ⊆ upRules"
and  c: "R = Ax ∪ R'"
shows "(Γ + Γ' ⇒* E,n) ∈ derivable R*"
using a
proof (induct n arbitrary: Γ E rule:nat_less_induct)
case (1 n Γ E)
then have IH: "∀m<n. ∀ Γ E. ( Γ ⇒* E, m) ∈ derivable R* ⟶ ( Γ + Γ' ⇒* E, m) ∈ derivable R*"
and a': "( Γ ⇒* E, n) ∈ derivable R*" by auto
show ?case
proof (cases n)
case 0
then have "(Γ ⇒* E,0) ∈ derivable R*" using a' by simp
then have "([], Γ ⇒* E) ∈ R*" by (cases) auto
then obtain  r S where "r ∈ R" and split:"extendRule S r = ([],Γ ⇒* E)"
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> ⇒* At i) ∨ c = (\<LM>ff\<RM> ⇒* Em)"
using characteriseAx[where r=r] by auto
moreover
{assume "c = (\<LM>At i\<RM> ⇒* At i)"
then have "extend S (\<LM>At i\<RM> ⇒* At i) = (Γ ⇒* At i)" and "At i = E" using split and ‹r = ([],c)›
then have "At i ∈# Γ" using extendID by auto
then have "At i ∈# Γ + Γ'" by auto
then have "(Γ + Γ' ⇒* E,0) ∈ derivable R*"
using c and containID[where Γ="Γ+Γ'" and R=R and i=i] and ‹At i = E› by auto
}
moreover
{assume "c = (\<LM>ff\<RM> ⇒* Em)"
then have "extend S (\<LM>ff\<RM> ⇒* Em) = (Γ ⇒* E)" using split and ‹r = ([],c)›
then have "ff ∈# Γ" using extendFalsum by auto
then have "ff ∈# Γ + Γ'" by auto
then have "(Γ + Γ' ⇒* E,0) ∈ derivable R*"
using c and containFalsum[where Γ="Γ+Γ'" and R=R] by auto
}
ultimately show "(Γ + Γ' ⇒* E,n) ∈ derivable R*" using ‹n=0› by auto
next
case (Suc n')
then have "(Γ ⇒* E, n'+1) ∈ derivable R*" using a' by simp
then obtain Ps where f:"Ps ≠ []"
and g:"(Ps, Γ ⇒* E) ∈ R*"
and h:"∀ p ∈ set Ps. ∃ m≤n'. (p,m) ∈ derivable R*"
using characteriseLast[where C="Γ ⇒* E" 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, Γ ⇒* E)" by (cases) auto
with b have as: "(r ∈ Ax ∨ r ∈ upRules) ∧ extendRule S r = (Ps, Γ ⇒* E)" by auto
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
moreover obtain ps c where "r = (ps,c)" by (cases r) auto
ultimately have "(ps,c) ∈ upRules" by simp
obtain Γ1 δ where "S = (Γ1 ⇒* δ)" by (cases S) auto
with h as ‹r = (ps,c)› have pms: "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1 ⇒* δ) p,m) ∈ derivable R*"
have "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*"
proof-
{fix p
assume "p ∈ set ps"
with pms obtain m where "m≤n'" and aa: "(extend (Γ1 ⇒* δ) p,m) ∈ derivable R*" by auto
moreover obtain Γ2 δ' where eq:"p = (Γ2 ⇒* δ')" by (cases p) auto
have "δ' = Em ∨ δ' ≠ Em" by blast
moreover
{assume "δ' = Em"
then have "extend (Γ1 ⇒* δ) p = (Γ1 + Γ2 ⇒* δ)" using eq by (auto simp add:extend_def)
then have "(Γ1 + Γ2 ⇒* δ,m) ∈ derivable R*" using aa by auto
then have "(Γ1 + Γ2 + Γ' ⇒* δ, m) ∈ derivable R*" using IH and ‹n = Suc n'› and ‹m≤n'›
apply- apply (drule_tac x=m in spec) by auto
then have "(extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*" using eq and ‹δ' = Em›
}
moreover
{assume "δ' ≠ Em"
then have "extend (Γ1 ⇒* δ) p = (Γ1 + Γ2 ⇒* δ')" using eq by (auto simp add:extend_def)
then have "(Γ1 + Γ2 ⇒* δ',m) ∈ derivable R*" using aa by auto
then have "(Γ1 + Γ2 + Γ' ⇒* δ', m) ∈ derivable R*" using IH and ‹n = Suc n'› and ‹m≤n'›
apply- apply (drule_tac x=m in spec) by auto
then have "(extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*" using eq and ‹δ' ≠ Em›
}
ultimately have "(extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*" by blast
then have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*" using ‹m≤n'› by auto
}
then show ?thesis by auto
qed
then have "∀ p ∈ set (fst (extendRule (Γ1 + Γ' ⇒* δ) r)).
∃ m≤n'. (p,m) ∈ derivable R*" using ‹r = (ps,c)› by (auto simp add:extendRule_def)
moreover have "extendRule (Γ1 + Γ' ⇒* δ) r ∈ R*"
using ‹r ∈ upRules› and ‹r ∈ R› by auto
moreover from ‹S = (Γ1 ⇒* δ)› and as have "extend (Γ1 + Γ' ⇒* δ) (snd r) = (Γ + Γ' ⇒* E)"
by (auto simp add:extendRule_def extend_def union_ac)
ultimately have "(Γ + Γ' ⇒* E,n'+1) ∈ derivable R*"
using derivable.step[where r="extendRule (Γ1 + Γ' ⇒* δ) r" and R="R*" and m="n'"]
and ‹fst r ≠ []› by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
then show "( Γ + Γ' ⇒* E, n) ∈ derivable R*" using ‹n = Suc n'› by auto
qed
qed

(*>*)
text‹
\noindent Given this, it is possible to have right weakening, where we overwrite the empty formula if it appears as the succedent of the root of a derivation:
›
lemma dpWeakR:
assumes (*<*)a:(*>*)"(Γ ⇒* Em,n) ∈ derivable R*"
and  (*<*)b:(*>*) "R' ⊆ upRules"
and  (*<*)c:(*>*) "R = Ax ∪ R'"
shows "(Γ ⇒* C,n) ∈ derivable R*"   ― ‹Proof omitted›
(*<*)
using a
proof (induct n arbitrary: Γ rule:nat_less_induct)
case (1 n Γ)
then have IH: "∀m<n. ∀ Γ. ( Γ ⇒* Em, m) ∈ derivable R* ⟶ ( Γ ⇒* C, m) ∈ derivable R*"
and a': "( Γ ⇒* Em, n) ∈ derivable R*" by auto
show ?case
proof (cases n)
case 0
then have "(Γ ⇒* Em,0) ∈ derivable R*" using a' by simp
then have "([], Γ ⇒* Em) ∈ R*" by (cases) auto
then obtain  r S where "r ∈ R" and split:"extendRule S r = ([],Γ ⇒* Em)"
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> ⇒* At i) ∨ c = (\<LM>ff\<RM> ⇒* Em)"
using characteriseAx[where r=r] by auto
moreover
{assume "c = (\<LM>At i\<RM> ⇒* At i)"
with split and ‹r = ([],c)› have "(Γ ⇒* C,0) ∈ derivable R*" by (auto simp add:extendRule_def extend_def)
}
moreover
{assume "c = (\<LM>ff\<RM> ⇒* Em)"
then have "extend S (\<LM>ff\<RM> ⇒* Em) = (Γ ⇒* Em)" using split and ‹r = ([],c)›
then have "ff ∈# Γ" using extendFalsum by auto
then have "(Γ ⇒* C,0) ∈ derivable R*"
using c and containFalsum[where Γ=Γ and R=R] by auto
}
ultimately show "(Γ ⇒* C,n) ∈ derivable R*" using ‹n=0› by auto
next
case (Suc n')
then have "(Γ ⇒* Em, n'+1) ∈ derivable R*" using a' by simp
then obtain Ps where f:"Ps ≠ []"
and g:"(Ps, Γ ⇒* Em) ∈ R*"
and h:"∀ p ∈ set Ps. ∃ m≤n'. (p,m) ∈ derivable R*"
using characteriseLast[where C="Γ ⇒* Em" and m=n' and R="R*"] by auto
from g c obtain S r where "r ∈ R" and split: "(r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⇒* Em)" by (cases) auto
with b have as: "(r ∈ Ax ∨ r ∈ upRules) ∧ extendRule S r = (Ps, Γ ⇒* Em)" by auto
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
moreover obtain ps c where "r = (ps,c)" by (cases r) auto
ultimately have "(ps,c) ∈ upRules" by simp
then obtain F Fs where "c = (\<LM>Compound F Fs\<RM> ⇒* Em) ∨ c = (\<Empt> ⇒* Compound F Fs)" by (rule upRules.cases) auto
moreover
{assume "c = (\<Empt> ⇒* Compound F Fs)"
with ‹r = (ps,c)› and split have "(Γ ⇒* C,n'+1) ∈ derivable R*" by (auto simp add:extendRule_def extend_def)
}
moreover
{assume "c = (\<LM> Compound F Fs \<RM> ⇒* Em)"
moreover obtain Γ1 δ where "S = (Γ1 ⇒* δ)" by (cases S) auto
ultimately have "δ = Em" using split and ‹r= (ps,c)› by (auto simp add:extendRule_def extend_def)
then have "S = (Γ1 ⇒* Em)" using ‹S = (Γ1 ⇒* δ)› by simp
with h as ‹r = (ps,c)› have pms: "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1 ⇒* Em) p,m) ∈ derivable R*"
have "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1  ⇒* C) p,m) ∈ derivable R*"
proof-
{fix p
assume "p ∈ set ps"
with pms obtain m where "m≤n'" and aa: "(extend (Γ1 ⇒* Em) p,m) ∈ derivable R*" by auto
moreover obtain Γ2 δ' where eq:"p = (Γ2 ⇒* δ')" by (cases p) auto
have "δ' = Em ∨ δ' ≠ Em" by blast
moreover
{assume "δ' = Em"
then have "extend (Γ1 ⇒* Em) p = (Γ1 + Γ2 ⇒* Em)" using eq by (auto simp add:extend_def)
then have "(Γ1 + Γ2 ⇒* Em,m) ∈ derivable R*" using aa by auto
then have "(Γ1 + Γ2 ⇒* C, m) ∈ derivable R*" using IH and ‹n = Suc n'› and ‹m≤n'›
apply- apply (drule_tac x=m in spec) by auto
then have "(extend (Γ1  ⇒* C) p,m) ∈ derivable R*" using eq and ‹δ' = Em›
}
moreover
{assume "δ' ≠ Em"
then have "extend (Γ1 ⇒* Em) p = (Γ1 + Γ2 ⇒* δ')" using eq by (auto simp add:extend_def)
then have "(Γ1 + Γ2 ⇒* δ',m) ∈ derivable R*" using aa by auto
moreover have "extend (Γ1 ⇒* C) p = (Γ1 + Γ2 ⇒* δ')" using eq and ‹δ' ≠ Em› by (auto simp add:extend_def)
ultimately have "(extend (Γ1 ⇒* C) p,m) ∈ derivable R*" by simp
}
ultimately have "(extend (Γ1  ⇒* C) p,m) ∈ derivable R*" by blast
then have "∃ m≤n'. (extend (Γ1  ⇒* C) p,m) ∈ derivable R*" using ‹m≤n'› by auto
}
then show ?thesis by auto
qed
then have "∀ p ∈ set (fst (extendRule (Γ1  ⇒* C) r)).
∃ m≤n'. (p,m) ∈ derivable R*" using ‹r = (ps,c)› by (auto simp add:extendRule_def)
moreover have "extendRule (Γ1  ⇒* C) r ∈ R*"
using ‹r ∈ upRules› and ‹r ∈ R› by auto
moreover from ‹S = (Γ1 ⇒* Em)› and as have "extend (Γ1  ⇒* C) (snd r) = (Γ ⇒* C)"
by (auto simp add:extendRule_def extend_def union_ac)
ultimately have "(Γ ⇒* C,n'+1) ∈ derivable R*"
using derivable.step[where r="extendRule (Γ1 ⇒* C) r" and R="R*" and m="n'"]
and ‹fst r ≠ []› by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
}
ultimately show "( Γ ⇒* C, n) ∈ derivable R*" using ‹n = Suc n'› by auto
qed
qed

(* ---------------------------------------------------
---------------------------------------------------
---------------------------------------------------
---------------------------------------------------
THIS IS NOW
SingleInvertible.thy
---------------------------------------------------
---------------------------------------------------
---------------------------------------------------
--------------------------------------------------- *)
(*>*)
text‹
\noindent Of course, if $C = Em$, then the above lemma is trivial.  The burden is on the user not to use'' the empty formula as a normal formula.  An invertibility lemma can then be formalised:
›

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) ⟶ (Γ' ⇒* E) ∈ set (fst r')"
and (*<*)nonEm:(*>*) "E ≠ Em"
shows "∃ m≤n. (Γ +Γ' ⇒* E,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. rightPrincipal r' (Compound F Fs) ⟶ ( Γ' ⇒* E) ∈ set (fst r')) ⟶
(∃m'≤m. ( Γ + Γ' ⇒* E, m') ∈ derivable R*)"
and a': "(Γ ⇒* Compound F Fs,n) ∈ derivable R*"
and b': "∀ r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶ (Γ' ⇒* E) ∈ 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 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
moreover
{assume "r ∈ Ax"
then have "r = ([], \<LM> ff \<RM> ⇒* Em)"
using characteriseAx[where r=r] and ‹extendRule S r = ([],Γ ⇒* Compound F Fs)›
with ‹extendRule S r = ([],Γ ⇒* Compound F Fs)›
have "extend S (\<LM> ff \<RM> ⇒* Em) = (Γ ⇒* Compound F Fs)"
using extendRule_def[where R="([],\<LM>ff\<RM>⇒* Em)" 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 "(Γ + Γ' ⇒* E,0) ∈ derivable R*" using rules
and containFalsum[where Γ="Γ + Γ'" and R=R] by auto
then have "(Γ + Γ' ⇒* E,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 "(Γ + Γ' ⇒* E,0) ∈ derivable R*" using rules by simp
}
ultimately show "∃ m≤n. (Γ + Γ' ⇒* E,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
derv: "∀ 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 ext: "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 ext
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. (Γ + Γ' ⇒* E,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
then have "∃ T Ts. c = (\<LM>Compound T Ts\<RM> ⇒* Em) ∨ c = (\<Empt> ⇒* Compound T Ts)" using ‹r=(ps,c)›
and upRuleCharacterise[where Ps=ps and C=c] by auto
then obtain T Ts where "c = (\<LM>Compound T Ts\<RM> ⇒* Em) ∨ c = (\<Empt> ⇒* Compound T Ts)" by blast
moreover
{assume "c = (\<Empt> ⇒* Compound T Ts)"
with ext have "Compound T Ts = Compound F Fs"
using ‹r = (ps,c)› by (auto simp add:extendRule_def extend_def)
then have "rightPrincipal r (Compound F Fs)" using ‹c = (\<Empt> ⇒* Compound T Ts)› and ‹r = (ps,c)›
by auto
then have "(Γ' ⇒* E) ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R'› and rules
by auto
then have "extend S (Γ' ⇒* E) ∈ 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> ⇒* Compound F Fs)"
using ‹r = (ps,c)› by (cases) auto
with ext have "antec S = Γ"
using ‹r = (ps,c)› by (auto simp add:extendRule_def extend_def)
ultimately have "(Γ + Γ' ⇒* E) ∈ set Ps" using nonEm by (simp add:extend_def)
then have "∃ m≤n'. (Γ + Γ' ⇒* E,m) ∈ derivable R*"
using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
then have "∃ m≤n. (Γ + Γ' ⇒* E,m) ∈ derivable R*" using ‹n = Suc n'›
by (auto,rule_tac x=m in exI) (simp)
}
moreover
{assume "c = (\<LM>Compound T Ts\<RM> ⇒* Em)"
with ext and ‹r = (ps,c)›
have "Compound T Ts ∈# Γ" by (auto simp add:extendRule_def extend_def)
then have "∃ Γ1. Γ = Γ1 ⊕ Compound T Ts"
by (rule_tac x="Γ ⊖ Compound T Ts" in exI) (auto simp add:multiset_eq_iff)
then obtain Γ1 where "Γ = Γ1 ⊕ Compound T Ts" by auto
moreover from ‹c = (\<LM>Compound T Ts\<RM> ⇒* Em)› and ‹r = (ps,c)› and ext
have "succ S = Compound F Fs"
ultimately have "S = (Γ1 ⇒* Compound F Fs)" using ext
and ‹r = (ps,c)› and ‹c = (\<LM>Compound T Ts\<RM> ⇒* Em)› apply (auto simp add:extendRule_def extend_def)
by (cases S) auto
with derv have pms: "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1 ⇒* Compound F Fs) p,m) ∈ derivable R*" using ext
and ‹r= (ps,c)› by (auto simp add:extendRule_def)
have "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ1 + Γ' ⇒* E) p,m) ∈ derivable R*"
proof-
{fix p
assume "p ∈ set ps"
obtain Γi δi where p: "p = (Γi ⇒* δi)" by (cases p) auto
have "δi = Em ∨ δi ≠ Em" by blast
moreover
{assume "δi = Em"
then have "extend (Γ1 ⇒* Compound F Fs) p = (Γ1 + Γi ⇒* Compound F Fs)" using p
with pms obtain m where "m ≤n'" and "(Γ1 + Γi ⇒* Compound F Fs,m) ∈ derivable R*"
using ‹p ∈ set ps› by auto
with IH and ‹n = Suc n'› and b' have "∃ m'≤m. (Γ1 + Γi + Γ' ⇒* E,m') ∈ derivable R*"
by auto
then have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* E) p,m) ∈ derivable R*" using ‹m≤n'›
and p and ‹δi = Em› apply (auto simp add:extend_def union_ac)
by (rule_tac x="m'" in exI) auto
}
moreover
{assume "δi ≠ Em"
then have "extend (Γ1 ⇒* Compound F Fs) p = (Γ1 + Γi ⇒* δi)" using p
with pms obtain m where "m≤n'" and "(Γ1 + Γi ⇒* δi,m) ∈ derivable R*"
using ‹p ∈ set ps› by auto
then have "(Γ1 + Γi + Γ' ⇒* δi,m) ∈ derivable R*" using rules
and dpWeak[where Γ="Γ1 + Γi" and E="δi" and n=m and R=R and R'=R'] by auto
then have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* E) p,m) ∈ derivable R*" using ‹m≤n'›
and p and ‹δi ≠ Em› by (auto simp add:extend_def union_ac)
}
ultimately have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* E) p, m) ∈ derivable R*" by blast
}
thus ?thesis by auto
qed
then have "∀ p ∈ set (fst (extendRule (Γ1 + Γ' ⇒* E) r)).
∃ m≤n'. (p,m) ∈ derivable R*" using ‹r = (ps,c)› by (auto simp add:extendRule_def)
moreover have "extendRule (Γ1 + Γ' ⇒* E) r ∈ R*" using ‹r ∈ R'› and rules by auto
moreover from ‹S = (Γ1 ⇒* Compound F Fs)› and ext and ‹c = (\<LM>Compound T Ts\<RM> ⇒* Em)›
and ‹Γ = Γ1 ⊕ Compound T Ts› and ‹r = (ps,c)›
have "extend (Γ1 + Γ' ⇒* E) (snd r) = (Γ + Γ' ⇒* E)" by (auto simp add:extend_def union_ac)
moreover from ext and ‹r = (ps,c)› and ‹Ps ≠ []› have "fst r ≠ []" by (auto simp add:extendRule_def)
ultimately have "(Γ + Γ' ⇒* E,n'+1) ∈ derivable R*" using
derivable.step[where r="extendRule (Γ1 + Γ' ⇒* E) r" and m="n'" and R="R*"]
by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
then have "∃ m≤n. (Γ + Γ' ⇒* E,m) ∈ derivable R*" using ‹n = Suc n'› by auto
}
ultimately have "∃ m≤n. (Γ + Γ' ⇒* E,m) ∈ derivable R*" by blast
}
ultimately show "∃ m≤n. (Γ + Γ' ⇒* E,m) ∈ derivable R*" by blast
qed
qed
(*>*)

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) ⟶ (Γ' ⇒* Em) ∈ 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) ⟶ ( Γ' ⇒* Em) ∈ 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) ⟶ (Γ' ⇒* Em) ∈ 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 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
moreover
{assume "r ∈ Ax"
then obtain i where "r = ([], \<LM> ff \<RM> ⇒* Em) ∨ r = ([], \<LM>At i\<RM> ⇒* At i)"
using characteriseAx[where r=r] and ‹extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* δ)›
moreover
{assume "r = ([], \<LM>ff\<RM> ⇒* Em)"
with ‹extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* δ)›
have "extend S (\<LM> ff \<RM> ⇒* Em) = (Γ ⊕ Compound F Fs ⇒* δ)"
using extendRule_def[where R="([],\<LM>ff\<RM>⇒* Em)" and forms=S] by auto
then have "ff ∈# Γ ⊕ Compound F Fs"
using extendFalsum[where S=S and Γ="Γ⊕ Compound F Fs" and Δ=δ] by auto
then have "ff ∈# Γ" by auto
then have "ff ∈# Γ + Γ'" by auto
then have "(Γ + Γ' ⇒* δ,0) ∈ derivable R*" using rules
and containFalsum[where Γ="Γ + Γ'" and R=R] by auto
}
moreover
{assume "r = ([], \<LM>At i\<RM> ⇒* At i)"
with ‹extendRule S r = ([], Γ ⊕ Compound F Fs ⇒* δ)›
have "extend S (\<LM> At i\<RM> ⇒* At i) = (Γ ⊕ Compound F Fs ⇒* δ)"
using extendRule_def[where R="([], \<LM>At i \<RM> ⇒* At i)" and forms=S] by auto
then have "At i ∈# Γ ⊕ Compound F Fs" and eq: "δ = At i"
using extendID[where S=S and Γ="Γ ⊕ Compound F Fs" and Δ=δ and i=i] by (auto simp add:extend_def)
then have "At i ∈# Γ" by auto
then have "At i ∈# Γ + Γ'" by auto
with eq have "(Γ + Γ' ⇒* δ,0) ∈ derivable R*" using rules
and containID[where i=i 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*" using rules 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
derv: "∀ 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 ext: "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 ext
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
then have "∃ T Ts. c = (\<LM>Compound T Ts\<RM> ⇒* Em) ∨ c = (\<Empt> ⇒* Compound T Ts)" using ‹r=(ps,c)›
and upRuleCharacterise[where Ps=ps and C=c] by auto
then obtain T Ts where "c = (\<LM>Compound T Ts\<RM> ⇒* Em) ∨ c = (\<Empt> ⇒* Compound T Ts)" by blast
moreover
{assume "c = (\<Empt> ⇒* Compound T Ts)"
with ext have "antec S = Γ ⊕ Compound F Fs" and del: "Compound T Ts = δ"
using ‹r = (ps,c)› by (auto simp add:extendRule_def extend_def)
then obtain δ' where "S = (Γ ⊕ Compound F Fs ⇒* δ')" by (cases S) auto
with derv have pms: "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ ⊕ Compound F Fs ⇒* δ') p,m) ∈ derivable R*"
using ext and ‹r = (ps,c)› by (auto simp add:extendRule_def)
have "∀ p ∈ set ps. ∃ m≤n'. (extend (Γ + Γ' ⇒* δ') p,m) ∈ derivable R*"
proof-
{fix p
assume "p ∈ set ps"
obtain Γi δi where p: "p = (Γi ⇒* δi)" by (cases p) auto
have "δi = Em ∨ δi ≠ Em" by blast
moreover
{assume "δi = Em"
then have "extend (Γ ⊕ Compound F Fs ⇒* δ') p = (Γ + Γi ⊕ Compound F Fs ⇒* δ')" using p
with pms obtain m where "m ≤n'" and "(Γ + Γi ⊕ Compound F Fs ⇒* δ',m) ∈ derivable R*"
using ‹p ∈ set ps› by auto
with IH and ‹n = Suc n'› and b' have "∃ m'≤m. (Γ + Γi + Γ' ⇒* δ',m') ∈ derivable R*"
by auto
then have "∃ m≤n'. (extend (Γ + Γ' ⇒* δ') p,m) ∈ derivable R*" using ‹m≤n'›
and p and ‹δi = Em› apply (auto simp add:extend_def union_ac)
by (rule_tac x="m'" in exI) auto
}
moreover
{assume "δi ≠ Em"
then have "extend (Γ ⊕ Compound F Fs ⇒* δ') p = (Γ + Γi ⊕ Compound F Fs ⇒* δi)" using p
with pms obtain m where "m≤n'" and "(Γ + Γi ⊕ Compound F Fs ⇒* δi,m) ∈ derivable R*"
using ‹p ∈ set ps› by auto
then have "∃ m≤n'. (Γ + Γi + Γ' ⇒* δi,m) ∈ derivable R*" using ‹n = Suc n'› and b'
and IH
apply auto apply (drule_tac x=m in spec) apply auto
apply (drule_tac x="Γ + Γi" in spec) apply (drule_tac x=δi in spec)
apply (auto simp add:union_ac) apply (rule_tac x="m'" in exI) by auto
then have "∃ m≤n'. (extend (Γ + Γ' ⇒* δ') p,m) ∈ derivable R*" using ‹m≤n'›
and p and ‹δi ≠ Em› by (auto simp add:extend_def union_ac)
}
ultimately have "∃ m≤n'. (extend (Γ + Γ' ⇒* δ') p, m) ∈ derivable R*" by blast
}
thus ?thesis by auto
qed
then have "∀ p ∈ set (fst (extendRule (Γ + Γ' ⇒* δ') r)).
∃ m≤n'. (p,m) ∈ derivable R*" using ‹r = (ps,c)› by (auto simp add:extendRule_def)
moreover have "extendRule (Γ + Γ' ⇒* δ') r ∈ R*" using ‹r ∈ R'› and rules by auto
moreover from ‹S = (Γ ⊕ Compound F Fs ⇒* δ')› and ext and ‹c = (\<Empt> ⇒* Compound T Ts)›
and ‹r = (ps,c)›
have "extend (Γ + Γ' ⇒* δ') (snd r) = (Γ + Γ' ⇒* Compound T Ts)" by (auto simp add:extend_def union_ac)
moreover from ext and ‹r = (ps,c)› and ‹Ps ≠ []› have "fst r ≠ []" by (auto simp add:extendRule_def)
ultimately have "(Γ + Γ' ⇒* Compound T Ts ,n'+1) ∈ derivable R*" using
derivable.step[where r="extendRule (Γ + Γ' ⇒* δ') r" and m="n'" and R="R*"]
by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
then have "∃ m≤n. (Γ + Γ' ⇒* δ,m) ∈ derivable R*" using ‹n = Suc n'› and del by auto
}
moreover
{assume r: "c = (\<LM>Compound T Ts\<RM> ⇒* Em)"
have "Compound F Fs = Compound T Ts ∨ Compound F Fs ≠ Compound T Ts" by blast
moreover
{assume "Compound F Fs = Compound T Ts"
then have "leftPrincipal r (Compound F Fs)" using r and ‹r = (ps,c)› by auto
then have "(Γ' ⇒* Em) ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R'› and rules
by auto
then have "extend S (Γ' ⇒* Em) ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⊕ Compound F Fs ⇒* δ)›
and ‹r = (ps,c)› by (simp add:extendContain)
moreover from r and ‹Compound F Fs = Compound T Ts› have "c = (\<LM>Compound F Fs\<RM> ⇒* Em)" by auto
with ext 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'</