Theory SingleSuccedent

(*<*)
(*  Author : Peter Chapman *)
(* License: LGPL *)
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:
›
overloading
  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.  *)
overloading
  invertible ≡ invertible
  invertible_set ≡ invertible_set
begin

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

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

end

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


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

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

(* Lemma which says that if we have extended an identity rule, then the propositional variable is
   contained in the extended multisets *)
lemma extendID:
assumes "extend S (\<LM> At i \<RM> ⇒* 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)›
          by (auto simp add:extendRule_def extend_def)
     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)›
          by (auto simp add:extendRule_def extend_def)
     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*"
      by(auto simp add:extendRule_def)
 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›
                by (auto simp add:extend_def union_ac)
          }
       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›
                by (auto simp add:extend_def union_ac)
          }
       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)›
          by (auto simp add:extendRule_def extend_def)
     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*"
          by(auto simp add:extendRule_def)
     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›
                    by (auto simp add:extend_def union_ac)
              }
           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)› 
            by (auto simp add:extendRule_def extend_def)
       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"
                  by (auto simp add:extendRule_def extend_def)
             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
                           by (auto simp add:extend_def)
                      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
                           by (auto simp add:extend_def)
                      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 ⇒* δ)› 
            by (auto simp add:extendRule_def extend_def)
       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
                           by (auto simp add:extend_def union_ac)
                      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
                           by (auto simp add:extend_def union_ac)
                      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'›
                      by (auto,rule_tac x=m in exI) (simp)
                }
             moreover
                {assume "Compound F Fs ≠ Compound T Ts"
                 obtain Γ'' δ' where "S = (Γ'' ⇒* δ')" by (cases S) auto
                 with ext and r and ‹r = (ps,c)› have "δ = δ'" by (auto simp add:extendRule_def extend_def)
                 then have "S = (Γ'' ⇒* δ)" using ‹S = (Γ'' ⇒* δ')› by simp
                 with r and ‹r = (ps,c)› and ext have "Γ ⊕ Compound F Fs = Γ'' ⊕ Compound T Ts"
                      by (auto simp add:extendRule_def extend_def)
                 with ‹Compound F Fs ≠ Compound T Ts› obtain Γ1 where
                      gam1: "Γ = Γ1 ⊕ Compound T Ts" and
                      gam2: "Γ'' = Γ1 ⊕ Compound F Fs"
                      using midMultiset[where Γ=Γ and Γ'=Γ'' and A="Compound F Fs" and B="Compound T Ts"] by auto
                 with ‹S = (Γ'' ⇒* δ)› have "S = (Γ1 ⊕ Compound F Fs ⇒* δ)" by simp
                 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 + Γ' ⇒* δ) 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
                               by (auto simp add:extend_def union_ac)
                          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 + Γ' ⇒* δ,m') ∈ derivable R*"
                               by auto
                          then have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* δ) 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 ⊕ Compound F Fs ⇒* δi)" using p
                               by (auto simp add:extend_def union_ac)
                          with pms obtain m where "m≤n'" and "(Γ1 + Γi ⊕ Compound F Fs ⇒* δi,m) ∈ derivable R*"
                               using ‹p ∈ set ps› by auto
                          with IH and ‹n = Suc n'› and b' have "∃ m'≤m. (Γ1 + Γi + Γ' ⇒* δi,m') ∈ derivable R*"
                               by auto
                          then have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* δ) p,m) ∈ derivable R*" using ‹m≤n'›
                               and p and ‹δi ≠ Em› and ‹n = Suc n'› apply (auto simp add:extend_def union_ac)
                               apply (rule_tac x=m' in exI) by auto
                         } 
                      ultimately have "∃ m≤n'. (extend (Γ1 + Γ' ⇒* δ) p, m) ∈ derivable R*" by blast
                     }
                     thus ?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 ∈ R'› and rules by auto
                 moreover from ‹S = (Γ1 ⊕ Compound F Fs ⇒* δ)› and ext and ‹c = (\<LM>Compound T Ts\<RM> ⇒* Em)›
                     and gam1 and ‹r = (ps,c)›
                     have "extend (Γ1 + Γ' ⇒* δ) (snd r) = (Γ + Γ' ⇒* δ)" 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 "(Γ + Γ' ⇒* δ,n'+1) ∈ derivable R*" using
                     derivable.step[where r="extendRule (Γ1 + Γ' ⇒* δ) 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'› by auto
                }
            ultimately have "∃ m≤n. (Γ + Γ' ⇒* δ, m) ∈ derivable R*" by blast
           }
       ultimately have "∃ m≤n. (Γ + Γ' ⇒* δ, m) ∈ derivable R*" by blast
      }
   ultimately show "∃ m≤n. (Γ + Γ' ⇒* δ, m) ∈ derivable R*" by blast
   qed
qed
    


(* ---------------------------------------------------
   ---------------------------------------------------
   ---------------------------------------------------
   ---------------------------------------------------
                THIS IS NOW
                G3ip.thy
   ---------------------------------------------------
   ---------------------------------------------------
   ---------------------------------------------------
   --------------------------------------------------- *)



datatype cdi = con | dis | imp

type_synonym cdi_form = "cdi 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]"
(*>*)
text‹
\noindent \textbf{G3ip} can be expressed in this formalism: 
›
inductive_set "g3ip"
where
   conL(*<*)[intro](*>*):  "([\<LM> A \<RM> + \<LM> B \<RM> ⇒* Em], \<LM> A ∧* B \<RM> ⇒* Em) ∈ g3ip"
|  conR(*<*)[intro](*>*):  "([\<Empt> ⇒* A, \<Empt> ⇒* B], \<Empt> ⇒* (A ∧* B)) ∈ g3ip"
|  disL(*<*)[intro](*>*):  "([\<LM> A \<RM> ⇒* Em, \<LM> B \<RM> ⇒* Em], \<LM> A ∨* B\<RM> ⇒* Em) ∈ g3ip"
|  disR1(*<*)[intro](*>*): "([\<Empt> ⇒* A], \<Empt> ⇒* (A ∨* B)) ∈ g3ip"
|  disR2(*<*)[intro](*>*): "([\<Empt> ⇒* B], \<Empt> ⇒* (A ∨* B)) ∈ g3ip"
|  impL(*<*)[intro](*>*):  "([\<LM> A ⊃ B \<RM> ⇒* A, \<LM> B \<RM> ⇒* Em], \<LM> (A ⊃ B) \<RM> ⇒* Em) ∈ g3ip"
|  impR(*<*)[intro](*>*):  "([\<LM> A \<RM> ⇒* B], \<Empt> ⇒* (A ⊃ B)) ∈ g3ip"

(*<*)
lemma g3ip_upRules:
shows "g3ip ⊆ upRules"
proof-
  {fix r
   assume "r ∈ g3ip"
   then have "r ∈ upRules" apply (cases r) by (rule g3ip.cases) auto
  }
  then show "g3ip ⊆ upRules" by auto
qed
(*>*)

text‹\noindent As expected, $\implies{R}{}$ can be shown invertible:›

lemma impRInvert:
assumes "(Γ ⇒* (A ⊃ B), n) ∈ derivable (Ax ∪ g3ip)*" and "B ≠ Em"
shows "∃ m≤n. (Γ ⊕ A ⇒* B, m) ∈ derivable (Ax ∪ g3ip)*"
proof-
  have "∀ r ∈ (Ax ∪ g3ip). rightPrincipal r (A ⊃ B) ⟶ 
                           (\<LM>A\<RM> ⇒* B) ∈ set (fst r)"
  proof-  ― ‹Showing that $A \Rightarrow B$ is a premiss of every rule with $\implies{A}{B}$ principal› 
   {fix r
    assume "r ∈ (Ax ∪ g3ip)"
    moreover assume "rightPrincipal r (A ⊃ B)"
    ultimately have "r ∈ g3ip" (*<*)apply auto apply (rule rightPrincipal.cases) apply auto (*>*)by(*<*) (rule Ax.cases) (*>*) auto  ― ‹If $\implies{A}{B}$ was principal, then $r \notin Ax$›
    from ‹rightPrincipal r (A ⊃ B)› have "snd r = (\<Empt> ⇒* (A ⊃ B))" by(*<*) (rule rightPrincipal.cases)(*>*) auto
    with ‹r ∈ g3ip› and ‹rightPrincipal r (A ⊃ B)› 
        have "r = ([\<LM>A\<RM> ⇒* B], \<Empt> ⇒* (A⊃B))" (*<*) apply (cases r)(*>*) by (rule g3ip.cases) auto
    then have "(\<LM>A\<RM> ⇒* B) ∈ set (fst r)" by auto
   }
   thus ?thesis by auto
   qed
  with assms (*<*)and g3ip_upRules(*>*) show ?thesis using rightInvertible(*<*)[where R'="g3ip" and R="Ax ∪ g3ip" and Γ=Γ and n=n
                            and Γ'="\<LM>A\<RM>" and E=B and F="imp" and Fs="[A,B]"](*>*) by auto
qed

(*<*)
end
(*>*)