Theory ModalSequents

(*<*)
(* AUTHOR : Peter Chapman  *)
(* License: LGPL *)

section "Modal Sequents"

theory ModalSequents
imports "HOL-Library.Multiset"

begin

(* -------------------------------
   -------------------------------
            Multiset2.thy
   -------------------------------
   ------------------------------- *)

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

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

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


abbreviation
multiset_map (infixl ‹⋅⋅› 100) where
   "(f :: 'a ⇒ 'a)⋅⋅(Γ :: 'a multiset) ≡ image_mset f Γ" 


lemma nonEmpty_contain:
assumes "Γ ≠ \<Empt>"
shows "∃ a. a ∈# Γ"
using assms
by (induct Γ) auto

lemma nonEmpty_neq:
assumes "Γ ≠ \<Empt>"
shows "Γ + C ≠ C"
proof-
from assms and nonEmpty_contain obtain a where "a ∈# Γ" by auto
then have "count Γ a ≥ 1" by (simp add: Suc_le_eq)
then have "count (Γ + C) a ≠ count C a" by auto
then show "Γ + C ≠ C" by (auto simp add:multiset_eq_iff)
qed 

lemma nonEmpty_image:
assumes "Γ ≠ \<Empt>"
shows "f ⋅⋅ Γ ≠ \<Empt>"
using image_mset_is_empty_iff assms by auto

lemma single_plus_obtain:
assumes "A ∈# Γ"
shows "∃ Δ. Γ = Δ ⊕ A"
proof-
from assms have "Γ = Γ ⊖ A ⊕ A" by (auto simp add:multiset_eq_iff)
then show ?thesis by (rule_tac x="Γ⊖A" in exI) simp
qed

lemma singleton_add_means_equal:
assumes "\<LM>A\<RM> = Γ ⊕ B"
shows "A = B"
proof-
from assms have "size (\<LM>A\<RM>) = size (Γ ⊕ B)" by auto
then have "size (\<LM>A\<RM>) = size Γ + size (\<LM>B\<RM>)" by auto
then have "Γ = \<Empt>" by auto
with assms have "\<LM>A\<RM> = \<LM>B\<RM>" by auto
then show ?thesis by auto
qed

lemma singleton_add_means_empty:
assumes "\<LM>A\<RM> = Γ ⊕ B"
shows "Γ = \<Empt>"
proof-
from assms have "size (\<LM>A\<RM>) = size (Γ ⊕ B)" by auto
then have "size (\<LM>A\<RM>) = size Γ + size (\<LM>B\<RM>)" by auto
then show "Γ = \<Empt>" by auto
qed

lemma single_multiset_eq_non_empty:
assumes "\<LM>A\<RM> = Δ + Δ'"
and     "Δ ≠ \<Empt>"
shows "Δ' = \<Empt> ∧ Δ = \<LM>A\<RM>"
proof-
 from assms have "size (\<LM>A\<RM>) = size Δ + size Δ'" by auto
 then have "1 = size Δ + size Δ'" by auto
 moreover from ‹Δ ≠ \<Empt>› have "0 ≠ size Δ" by auto
 ultimately have "size Δ = 1 ∧ size Δ' = 0" by arith
 then have a: "Δ' = \<Empt>" by auto
 with ‹\<LM>A\<RM> = Δ + Δ'› have b: "Δ = \<LM>A\<RM>" by auto
 from a b show ?thesis by auto
qed

lemma two_neq_one_aux:
assumes "(\<LM>A\<RM>) ⊕ B = \<LM>C\<RM>"
shows "False"
proof-
 from assms have "size ((\<LM>A\<RM>) ⊕ B) = size (\<LM>C\<RM>)" by auto
 then have "size (\<LM>A\<RM>) + size (\<LM>B\<RM>) = size (\<LM>C\<RM>)" by auto
 then show ?thesis by auto
qed

lemma two_neq_one:
assumes "((\<LM>A\<RM>) ⊕ B) + Γ = \<LM>C\<RM>"
shows "False"
proof-
 from assms have "size (((\<LM>A\<RM>)⊕ B) + Γ) = size (\<LM>C\<RM>)" by auto
 then have "size (\<LM>A\<RM>) + size (\<LM>B\<RM>) + size Γ = 1" by auto
 then show ?thesis by auto
qed


lemma add_equal_means_equal:
assumes "Γ ⊕ A = Δ ⊕ A"
shows "Γ = Δ"
proof-
 from assms and add_eq_conv_diff[where M=Γ and N=Δ and a=A and b=A] show "Γ = Δ" by auto
qed





(* -------------------------------
   -------------------------------
        SequentRulesModal2.thy
   -------------------------------
   ------------------------------- *)

(*>*)
text‹
\section{Modal Calculi \label{isamodal}}
Some new techniques are needed when formalising results about modal calculi.  A set of modal operators must index formulae (and sequents and rules), there must be a method for modalising a multiset of formulae and we need to be able to handle implicit weakening rules.

The first of these is easy; instead of indexing formulae by a single type variable, we index on a pair of type variables, one which contains the propositional connectives, and one which contains the modal operators:
›
datatype ('a, 'b) form = At "nat"
                                 | Compound "'a" "('a, 'b) form list"
                                 | Modal "'b" "('a, 'b) form list"
                                 | ff

datatype_compat form

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

type_synonym ('a,'b) rule = "('a,'b) sequent list * ('a,'b) sequent"

type_synonym ('a,'b) deriv = "('a,'b) sequent * nat"

consts
  (* extend a sequent by adding another one.  A form of weakening.  *)
  extend :: "('a,'b) sequent ⇒ ('a,'b) sequent ⇒ ('a,'b) sequent"
  extendRule :: "('a,'b) sequent ⇒ ('a,'b) rule ⇒ ('a,'b) rule"
  extendRule2 :: "('a,'b) sequent ⇒ ('a,'b) sequent ⇒ ('a,'b) rule ⇒ ('a,'b) rule"
  extendConc :: "('a,'b) sequent ⇒ ('a,'b) rule ⇒ ('a,'b) rule"

  (* Unique conclusion Property *)
  uniqueConclusion :: "('a,'b) rule set ⇒ bool"

  (* Transform a multiset using a modal operator.  "Boxing" a context, effectively *)
  modaliseMultiset :: "'b ⇒ ('a,'b) form multiset ⇒ ('a,'b) form multiset" (infixl ‹⋅› 200)

  (* functions to get at components of sequents *)

primrec antec :: "('a,'b) sequent ⇒ ('a,'b) form multiset" where
  "antec (Sequent ant suc) = ant"

primrec succ :: "('a,'b) sequent ⇒ ('a,'b) form multiset" where
  "succ (Sequent ant suc) = suc"

primrec mset :: "('a,'b) sequent ⇒ ('a,'b) form multiset" where
  "mset (Sequent ant suc) = ant + suc"

primrec seq_size :: "('a,'b) 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 *)
overloading
  extend ≡ extend
  extendRule ≡ extendRule
  extendRule2 ≡ extendRule2
begin

definition extend
  where "extend forms seq ≡ (antec forms + antec seq) ⇒* (succ forms + succ seq)"

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

definition extendRule2 :: "('a,'b) sequent ⇒ ('a,'b) sequent ⇒ ('a,'b) rule ⇒ ('a,'b) rule"
  where "extendRule2 S1 S2 r ≡ (map (extend S1) (fst r), extend S2 (snd r))"

end

(*>*)

(* The unique conclusion property.  A set of rules has unique conclusion property if for any pair of rules,
   the conclusions being the same means the rules are the same*)
overloading
  uniqueConclusion ≡ uniqueConclusion
  modaliseMultiset ≡ modaliseMultiset
begin

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

text‹
\noindent Modalising multisets is relatively straightforward.  We use the notation $!\cdot \Gamma$, where $!$ is a modal operator and $\Gamma$ is a multiset of formulae:
›
definition modaliseMultiset :: "'b ⇒ ('a,'b) form multiset ⇒ ('a,'b) form multiset"
  where "modaliseMultiset a Γ ≡ {# Modal a [p]. p ∈# Γ #}"

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> ⇒* \<LM> At i \<RM>) ∈ Ax"
|  Lbot[intro]: "([], \<LM> ff \<RM> ⇒* \<Empt>) ∈ Ax"

(* upRules is the set of all rules which have a single conclusion.  This is akin to each rule having a 
   single principal formula.  We don't want rules to have no premisses, hence the restriction
   that ps ≠ [] *)
inductive_set "upRules" where
   I[intro]: "⟦ mset c = \<LM> Compound R Fs \<RM> ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"


(*>*)
text‹
\noindent Similarly to \S\ref{isafirstorder}, two new rule sets are created.  The first are the normal modal rules:
›
inductive_set "modRules2" where
   (*<*)I[intro]:(*>*) "⟦ ps ≠ [] ; mset c = \<LM> Modal M Ms \<RM> ⟧ ⟹ (ps,c) ∈ modRules2"

text‹
\noindent The second are the \textit{modalised context rules}.  Taking a subset of the normal modal rules, we extend using a pair of modalised multisets for context.  We create a new inductive rule set called \texttt{p-e}, for ``prime extend'', which takes a set of modal active parts and a pair of modal operators (say $!$ and $\bullet$), and returns the set of active parts extended with $!\cdot \Gamma \Rightarrow \bullet\cdot\Delta$:
›
inductive_set p_e :: "('a,'b) rule set ⇒ 'b ⇒ 'b ⇒ ('a,'b) rule set" 
  for R :: "('a,'b) rule set" and M N :: "'b" 
  where
  (*<*)I[intro]:(*>*) "⟦ (Ps, c) ∈ R ; R ⊆ modRules2 ⟧ ⟹ extendRule (M⋅Γ ⇒* N⋅Δ) (Ps, c) ∈ p_e R M N"

text‹
\noindent We need a method for extending the conclusion of a rule without extending the premisses.  Again, this is simple:›

overloading extendConc ≡ extendConc
begin

definition extendConc :: "('a,'b) sequent ⇒ ('a,'b) rule ⇒ ('a,'b) rule"
  where "extendConc S r ≡ (fst r, extend S (snd r))"

end

text‹\noindent  The extension of a rule set is now more complicated; the inductive definition has four clauses, depending on the type of rule:
›
inductive_set ext :: "('a,'b) rule set ⇒ ('a,'b) rule set ⇒ 'b ⇒ 'b ⇒ ('a,'b) rule set" 
  for R R' :: "('a,'b) rule set" and M N :: "'b"
  where
   ax(*<*)[intro](*>*):    "⟦ r ∈ R ; r ∈ Ax ⟧ ⟹ extendRule seq r ∈ ext R R' M N"
|  up(*<*)[intro](*>*):    "⟦ r ∈ R ; r ∈ upRules⟧ ⟹ extendRule seq r ∈ ext R R' M N"
| mod1(*<*)[intro](*>*): "⟦ r ∈ p_e R' M N ; r ∈ R ⟧ ⟹ extendConc seq r ∈ ext R R' M N"
| mod2(*<*)[intro](*>*): "⟦ r ∈ R ; r ∈ modRules2 ⟧ ⟹ extendRule seq r ∈ ext R R' M N"

text‹
\noindent Note the new rule set carries information about which set contains the modalised context rules and which modal operators which extend those prime parts.
›

(*<*)
(* A formulation of what it means to be a principal formula for a rule.   *)

inductive leftPrincipal :: "('a,'b) rule ⇒ ('a,'b) form ⇒ ('a,'b) rule set ⇒ bool"
  where
  up[intro]: "⟦ C = (\<LM> A \<RM> ⇒* \<Empt>) ; A ≠ ff ; (Ps,C) ∈ R ⟧  ⟹ 
                   leftPrincipal (Ps,C) A R"



inductive rightPrincipal :: "('a,'b) rule ⇒ ('a,'b) form ⇒ ('a,'b) rule set ⇒ bool"
  where
  up[intro]: "⟦ C = (\<Empt> ⇒* \<LM>A\<RM>) ; (Ps,C) ∈ R ⟧⟹ rightPrincipal (Ps,C) A R"



(* 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,'b) rule set ⇒ ('a,'b) deriv set"
  for R :: "('a,'b) rule set"
  where
   base[intro]: "⟦([],C) ∈ R⟧ ⟹ (C,0) ∈ derivable R"
|  step[intro]: "⟦ r ∈ R ; (fst r)≠[] ; ∀ p ∈ set (fst r). ∃ n ≤ m. (p,n) ∈ derivable R ⟧ 
                       ⟹ (snd r,m + 1) ∈ derivable R"


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

(* Obvious connection *)
lemma extend1_to_2:
shows "extendRule2 S S r = extendRule S r"
by (auto simp add:extendRule_def extendRule2_def)

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


(* Lemma which says that if we have extended an identity rule, then the propositional variable is
   contained in the extended multisets *)
lemma extendID:
assumes "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)"
shows "At i ∈# Γ ∧ At i ∈# Δ"
using assms
proof-
  from assms have "∃ Γ' Δ'. Γ = Γ' ⊕ At i ∧ Δ = Δ' ⊕ At i" 
     using extend_def[where forms=S and seq="\<LM> At i \<RM> ⇒* \<LM> At i \<RM>"]
     by (rule_tac x="antec S" in exI,rule_tac x="succ S" in exI) auto
  then show ?thesis by auto
qed

lemma extendFalsum:
assumes "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
shows "ff ∈# Γ"
proof-
  from assms have "∃ Γ'. Γ = Γ' ⊕ ff" 
     using extend_def[where forms=S and seq="\<LM>ff \<RM> ⇒* \<Empt>"]
     by (rule_tac x="antec S" in exI) auto
  then show ?thesis by auto
qed


(* Lemma that says if a propositional variable is in both the antecedent and succedent of a sequent,
   then it is derivable from idupRules *)
lemma containID:
assumes a:"At i ∈# Γ ∧ At i ∈# Δ"
    and b:"Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable (ext R R' M N)"
proof-
from a have "Γ = Γ ⊖ At i ⊕ At i ∧ Δ = Δ ⊖ At i ⊕ At i" by auto
then have "extend ((Γ ⊖ At i) ⇒* (Δ ⊖ At i)) (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)" 
     using extend_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and seq="\<LM>At i\<RM> ⇒* \<LM>At i\<RM>"] by auto
moreover
have "([],\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ R" using b by auto
ultimately
have "([],Γ ⇒* Δ) ∈ ext R R' M N" 
     using ext.ax[where R=R and r="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<RM>)" and seq="Γ ⊖ At i ⇒* Δ ⊖ At i"] 
       and extendRule_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and R="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"] by auto
then show ?thesis using derivable.base[where R="ext R R' M N" and C="Γ ⇒* Δ"] by auto
qed

lemma containFalsum:
assumes a: "ff ∈# Γ"
   and  b: "Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable (ext R R' M N)"
proof-
from a have "Γ = Γ ⊖ ff ⊕ ff" by auto
then have "extend (Γ ⊖ ff ⇒* Δ) (\<LM>ff\<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
     using extend_def[where forms="Γ ⊖ ff ⇒* Δ" and seq="\<LM>ff\<RM> ⇒* \<Empt>"] by auto 
moreover
have "([],\<LM>ff\<RM> ⇒* \<Empt>) ∈ R" using b by auto
ultimately have "([],Γ ⇒* Δ) ∈ ext R R' M N"
     using ext.ax[where R=R and r="([],  \<LM>ff\<RM> ⇒* \<Empt>)" and seq="Γ ⊖ ff ⇒* Δ"] 
       and extendRule_def[where forms="Γ ⊖ ff ⇒* Δ" and R="([],  \<LM>ff\<RM> ⇒* \<Empt>)"] by auto
then show ?thesis using derivable.base[where R="ext R R' M N" and C="Γ ⇒* Δ"] by auto
qed 

(* Lemma which says that if r is an identity rule, then r is of the form
   ([], P ⇒* P) *)
lemma characteriseAx:
shows "r ∈ Ax ⟹ r = ([],\<LM> ff \<RM> ⇒* \<Empt>) ∨ (∃ i. r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>))"
apply (cases r) by (rule Ax.cases) auto

(* A lemma about the last rule used in a derivation, i.e. that one exists *)
lemma characteriseLast:
assumes "(C,m+1) ∈ derivable R"
shows "∃ Ps. Ps ≠ [] ∧
             (Ps,C) ∈ R ∧ 
             (∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)"
using assms
by (cases) auto


(* Lemma which says that if rule is an upRule, then the succedent is either empty, or a single formula *)
lemma succ_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)" using mset.simps [where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

(* Equivalent, but the antecedent *)
lemma antec_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)" using mset.simps[where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

lemma upRule_Size:
assumes "r ∈ upRules"
shows "seq_size (snd r) = 1"
using assms
proof-
    obtain Ps C where "r = (Ps,C)" by (cases r)
    then have "(Ps,C) ∈ upRules" using assms by simp
    then show ?thesis
       proof (cases)
          case (I R Rs)
          obtain G H where "C = (G ⇒* H)" by (cases C) (auto)
          then have "G + H = \<LM>Compound R Rs\<RM>" using mset.simps and ‹mset C = \<LM>Compound R Rs\<RM>› by auto
          then have "size (G+H) = 1" by auto 
          then have "size G + size H = 1" by auto
          then have "seq_size C = 1" using seq_size.simps[where ant=G and suc=H] and ‹C = (G ⇒* H)› by auto
          moreover have "snd r = C" using ‹r = (Ps,C)› by simp
          ultimately show "seq_size (snd r) = 1" by simp
       qed
qed

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

lemma modRule2Characterise:
assumes "(Ps,C) ∈ modRules2"
shows "Ps ≠ [] ∧ (∃ F Fs. C = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ C = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>))"
using assms
proof (cases)
  case (I F Fs)
  then have "Ps ≠ []" by simp
  obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
  then have "(Ps,Γ ⇒* Δ) ∈ modRules2" using assms by simp
  then have "∃ F Fs. C = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ C = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)" 
    using ‹mset C = \<LM>Modal F Fs\<RM>› and ‹C = (Γ ⇒* Δ)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="Modal F Fs"]
    by auto
  thus ?thesis using ‹Ps ≠ []› by auto
qed

lemma modRule1Characterise:
assumes "(Ps,C) ∈ p_e R M N" and "R ⊆ modRules2"
shows "∃ F Fs Γ Δ ps r. (Ps,C) = extendRule (M⋅Γ⇒*N⋅Δ) r ∧ r ∈ R ∧ 
                    (r = (ps,\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ 
                     r = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>))"
using assms
proof (cases)
  case (I ps c Γ Δ)
  then have "(ps, c) ∈ modRules2" by auto
  with ‹(ps, c) ∈ modRules2› obtain F Fs where "c = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ c = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
    using modRule2Characterise[where C=c and Ps=ps] by auto
  with I show ?thesis
    apply -
    apply (rule_tac x=F in exI) apply (rule_tac x=Fs in exI) apply (rule_tac x=Γ in exI)
    apply (rule_tac x=Δ in exI) apply auto done
qed

lemma extendEmpty:
shows "extend (\<Empt> ⇒* \<Empt>) C = C"
apply (auto simp add:extend_def) by (cases C) auto

lemma mapExtendEmpty:
shows "map (extend (\<Empt> ⇒* \<Empt>)) ps = ps"
using extendEmpty
by (induct ps) auto

lemma extendRuleEmpty:
shows "extendRule (\<Empt> ⇒* \<Empt>) r = r"
by (auto simp add:extendRule_def extendEmpty mapExtendEmpty)

lemma extendNonEmpty:
assumes "¬ (Γ = \<Empt> ∧ Δ = \<Empt>)"
shows "extend (Γ ⇒* Δ) C ≠ C"
using assms
by (cases C) (auto simp add:extend_def nonEmpty_neq)

lemma extendRuleNonEmpty:
assumes "¬ (Γ = \<Empt> ∧ Δ = \<Empt>)"
shows "extendRule (Γ ⇒* Δ) r ≠ r"
using assms
by (cases r) (auto simp add:extendRule_def extendNonEmpty)

lemma extendRuleEmptyRev:
assumes "extendRule S r = r"
shows "S = (\<Empt> ⇒* \<Empt>)"
using assms extendRuleNonEmpty apply (cases r) by (cases S) (auto)

lemma modaliseEmpty:
shows "a ⋅ (\<Empt>) = \<Empt>"
using modaliseMultiset_def[where a=a and Γ="\<Empt>"] by auto

lemma modaliseNonEmpty:
assumes "Γ ≠ \<Empt>"
shows "a ⋅ Γ ≠ \<Empt>"
using assms nonEmpty_image[where Γ=Γ] modaliseMultiset_def[where Γ=Γ and a=a] by auto

lemma mset_extend:
shows "mset (extend S c) = mset S + mset c"
using mset.simps extend_def apply (cases S) apply (cases c)
by (auto simp add: union_ac extend_def)

lemma mset_extend_size:
assumes "¬ (Γ = \<Empt> ∧ Δ = \<Empt>)"
shows "size (mset ((extend (Γ ⇒* Δ) c))) > size (mset c)"
using assms
proof-
from assms have "mset (Γ ⇒* Δ) ≠ \<Empt>" by auto
then have "size (mset (Γ ⇒* Δ)) > 0" apply auto by (induct Γ) auto
moreover have "mset (extend (Γ ⇒* Δ) c) = mset (Γ⇒*Δ) + mset c"
     using mset_extend[where S="Γ ⇒* Δ" and c=c] by auto
then have "size (mset (extend (Γ ⇒* Δ) c)) = size (mset (Γ ⇒* Δ)) + size (mset c)" by simp
ultimately show ?thesis by arith
qed



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 extendCommute:
shows "(extend S) (extend R c) = (extend R) (extend S c)"
by (auto simp add:extend_def union_ac)

lemma mapCommute:
shows "map (extend S) (map (extend R) c) = map (extend R) (map (extend S) c)"
by (induct_tac c) (auto simp add:extendCommute)

lemma extendAssoc:
shows "(extend S) (extend R c) = extend (extend S R) c" 
by (auto simp add:extend_def union_ac)

lemma mapAssoc:
shows "map (extend S) (map (extend R) c) = map (extend (extend S R)) c"
by (induct_tac c) (auto simp add:extendAssoc)


(* Disjointness of the various rule sets *)
lemma disjoint_Aux:
assumes "mset c = \<LM>A\<RM>"
shows "A ∈# mset (extend S c)"
proof-
from assms have "c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)" by (cases c) (auto simp add:mset.simps union_is_single)
then show ?thesis by (auto simp add:extend_def mset.simps)
qed

lemma disjoint_Aux2:
assumes "mset c = \<LM>A\<RM>"
    and "A ≠ B"
    and "mset (extend S c) = \<LM>B\<RM>"
shows "False"
proof-
from assms have "A ∈# \<LM>B\<RM>" using disjoint_Aux[where c=c and A=A and S=S] by auto
with ‹A ≠ B› show ?thesis by auto
qed

lemma disjoint_Ax_up:
shows "Ax ∩ upRules = {}"
apply auto apply (rule Ax.cases) apply auto by (rotate_tac 1,rule upRules.cases,auto)+

lemma disjoint_Ax_mod2:
shows "Ax ∩ modRules2 = {}"
apply auto apply (rule Ax.cases) apply auto by (rotate_tac 1,rule modRules2.cases,auto)+

lemma disjoint_Ax_mod1:
shows "Ax ∩ p_e modRules2 M N = {}"
apply auto apply (rule Ax.cases) apply auto apply (rule p_e.cases) apply auto apply (rule modRules2.cases) 
apply (auto simp add:extendRule_def extend_def) apply (rule p_e.cases) apply auto apply (rule modRules2.cases)
by (auto simp add:extendRule_def extend_def)

lemma disjoint_up_mod2:
shows "upRules ∩ modRules2 = {}"
apply auto apply (rule upRules.cases) apply auto by (rotate_tac 1,rule modRules2.cases,auto)

lemma disjoint_up_mod1:
shows "upRules ∩ p_e modRules2 M N = {}"
using disjoint_Aux2
apply auto apply (rule upRules.cases) apply auto
apply (rule p_e.cases)  apply auto apply (rule modRules2.cases) 
apply (auto simp add:extendRule_def extend_def union_ac)
apply (drule_tac x=cb in meta_spec) apply (drule_tac x="Modal Ma Ms" in meta_spec)
apply (drule_tac x="Compound R Fs" in meta_spec) apply (drule_tac x="M⋅Γ ⇒* N⋅Δ" in meta_spec) by (auto simp:union_ac)

lemmas disjoint = disjoint_Ax_up disjoint_Ax_mod1 disjoint_Ax_mod2 
                  disjoint_up_mod2 disjoint_up_mod1


lemma Ax_subset_false_aux:
assumes "A ⊆ B" and "A ∩ B = {}" and "A ≠ {}"
shows "False"
proof-
 from ‹A ≠ {}› have "∃ a. a ∈ A" by auto
 then obtain a where a: "a ∈ A" by auto
 with ‹A ⊆ B› have "a ∈ B" by auto
 with a have "a ∈ A ∩ B" by simp
 with ‹A ∩ B = {}› show ?thesis by auto
qed

lemma Ax_subset_false:
assumes "Ax ⊆ modRules2"
shows "False"
proof-
 have a: "([],\<LM>ff\<RM> ⇒* \<Empt>) ∈ Ax" by auto
 then have "Ax ≠ {}" by auto
 with disjoint_Ax_mod2 and assms show ?thesis using Ax_subset_false_aux[where A=Ax and B="modRules2"] by auto
qed



lemma modal_not_contain:
assumes "M ≠ N"
shows "¬ (Modal M A ∈# N⋅Γ)"
using assms by (induct Γ) (auto simp add:modaliseMultiset_def)

lemma nonPrincipalID:
fixes A :: "('a,'b) form"
assumes "r ∈ Ax"
shows "¬ rightPrincipal r A R ∧ ¬ leftPrincipal r A R"
proof-
from assms obtain i where r1:"r = ([], \<LM> ff \<RM> ⇒* \<Empt>) ∨ r = ([], \<LM> At i \<RM> ⇒* \<LM> At i\<RM>)" 
     using characteriseAx[where r=r] by auto
{ assume "rightPrincipal r A R" then obtain Ps where r2:"r = (Ps, \<Empt> ⇒* \<LM> A \<RM>)" by (cases r) auto
  with r1 and disjoint and ‹r ∈ Ax› have "False" by auto
}
then have "¬ rightPrincipal r A R" by auto
moreover
{ assume "leftPrincipal r A R" then obtain Ps' 
          where r3:"r = (Ps', \<LM>A\<RM> ⇒* \<Empt>) ∧ A ≠ ff" by (cases r) auto
  with r1 and disjoint and ‹r ∈ Ax› have "False" by auto
}
then have "¬ leftPrincipal r A R" by auto
ultimately show ?thesis by simp
qed

lemma compound_not_in_modal_multi:
shows "¬ (Compound M Ms ∈# N⋅Γ)"
by (induct Γ) (auto simp add:modaliseMultiset_def)

lemma not_principal_aux:
assumes "mset c = \<LM>Modal T Ts\<RM>"
    and "M⋅Γ + succ c = N⋅Δ ⊕ Compound F Fs"
shows "False"
proof-
from assms and single_is_union have "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∨ c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)" apply (cases c)
     apply (rename_tac multiset1 multiset2)
     apply auto
     by (drule_tac x="Modal T Ts" in meta_spec,drule_tac x="multiset1" in meta_spec,
         drule_tac x="multiset2" in meta_spec,simp)+
moreover
   {assume "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)"
    with assms have "M⋅Γ ⊕ Modal T Ts = N⋅Δ ⊕ Compound F Fs" by auto
    then have "Compound F Fs ∈# M⋅Γ ⊕ Modal T Ts" by auto
    then have "Compound F Fs ∈# M⋅Γ" by auto
    then have "False" using compound_not_in_modal_multi[where M=F and Ms=Fs and N=M and Γ=Γ] by auto
   }
moreover
   {assume "c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
    with assms have "Compound F Fs ∈# M⋅Γ" by auto
    then have "False" using compound_not_in_modal_multi[where M=F and Ms=Fs and N=M and Γ=Γ] by auto
   }
ultimately show ?thesis by blast
qed

lemma not_principal_aux2:
assumes "mset c = \<LM>Modal T Ts\<RM>"
    and "M⋅Γ + antec c = N⋅Δ ⊕ Compound F Fs"
shows "False"
proof-
from assms and single_is_union have "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∨ c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)" apply (cases c)
     apply (rename_tac multiset1 multiset2)
     apply (auto simp add:mset.simps)
     by (drule_tac x="Modal T Ts" in meta_spec,drule_tac x="multiset1" in meta_spec,
         drule_tac x="multiset2" in meta_spec,simp)+
moreover
   {assume "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)"
    with assms have "Compound F Fs ∈# M⋅Γ" by auto
    then have "False" using compound_not_in_modal_multi[where M=F and Ms=Fs and N=M and Γ=Γ] by auto
   }
moreover
   {assume "c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
    with assms have "M⋅Γ ⊕ Modal T Ts = N⋅Δ ⊕ Compound F Fs" by auto
    then have "Compound F Fs ∈# M⋅Γ ⊕ Modal T Ts" by auto
    then have "Compound F Fs ∈# M⋅Γ" by auto
    then have "False" using compound_not_in_modal_multi[where M=F and Ms=Fs and N=M and Γ=Γ] by auto
   }
ultimately show ?thesis by blast
qed

lemma modRules_not_right_principal_for_compound:
assumes "r ∈ p_e modRules2 S T"
shows "¬ rightPrincipal r (Compound M Ms) R"
using assms
proof-
from assms have "fst r ≠ []" apply (rule p_e.cases) apply (insert modRule2Characterise)
     apply (drule_tac x=Ps in meta_spec) apply (drule_tac x=c in meta_spec)
     by (auto simp add:extendRule_def)
{assume "rightPrincipal r (Compound M Ms) R"
 with assms obtain ps c where "r = (ps,c)" and "c = (\<Empt> ⇒* \<LM>Compound M Ms\<RM>)" using not_principal_aux
      apply (cases r) by (rule rightPrincipal.cases) auto 
 then have "r ∈ upRules" using ‹fst r ≠ []› by auto
 with assms have "False" using disjoint_up_mod1[where M=S and N=T] by auto
}
thus ?thesis by auto
qed

lemma modRules_not_left_principal_for_compound:
assumes "r ∈ p_e modRules2 T S"
shows "¬ leftPrincipal r (Compound M Ms) R"
using assms
proof-
from assms have "fst r ≠ []" apply (rule p_e.cases) apply (insert modRule2Characterise)
     apply (drule_tac x=Ps in meta_spec) apply (drule_tac x=c in meta_spec)
     by (auto simp add:extendRule_def)
{assume "leftPrincipal r (Compound M Ms) R"
 with assms obtain ps c where "r = (ps,c)" and "c = (\<LM>Compound M Ms\<RM> ⇒* \<Empt>)" using not_principal_aux2
      apply (cases r) by (rule leftPrincipal.cases) auto 
 then have "r ∈ upRules" using ‹fst r ≠ []› by auto
 with assms have "False" using disjoint_up_mod1[where M=T and N=S] by auto
}
thus ?thesis by auto
qed

lemma modRules2_not_left_principal_for_compound:
assumes "r ∈ modRules2"
shows "¬ leftPrincipal r (Compound M Ms) R"
using assms
proof-
from assms obtain ps T Ts where "r = (ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∨ r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
     using modRule2Characterise apply (cases r) apply auto apply (rotate_tac 2) apply (drule_tac x=a in meta_spec)
     apply (rotate_tac 2) by (drule_tac x=b in meta_spec) auto
moreover
   {assume "r = (ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>)"
    then have "¬ leftPrincipal r (Compound M Ms) R" apply auto apply (rule leftPrincipal.cases) 
         by (auto simp add:extendRule_def extend_def)
   }
moreover
  {assume "r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
   then have "¬ leftPrincipal r (Compound M Ms) R" apply auto apply (rule leftPrincipal.cases)
        by (auto simp add:extendRule_def extend_def)
  }
ultimately show "¬ leftPrincipal r (Compound M Ms) R" by blast
qed

lemma modRules2_not_right_principal_for_compound:
assumes "r ∈ modRules2"
shows "¬ rightPrincipal r (Compound M Ms) R"
using assms
proof-
from assms obtain ps T Ts where "r = (ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∨ r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
     using modRule2Characterise apply (cases r) apply auto apply (rotate_tac 2) apply (drule_tac x=a in meta_spec)
     apply (rotate_tac 2) by (drule_tac x=b in meta_spec) auto
moreover
   {assume "r = (ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>)"
    then have "¬ rightPrincipal r (Compound M Ms) R" apply auto apply (rule rightPrincipal.cases) 
         by (auto simp add:extendRule_def extend_def)  
   }
moreover
  {assume "r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
   then have "¬ rightPrincipal r (Compound M Ms) R" apply auto apply (rule rightPrincipal.cases)
        by (auto simp add:extendRule_def extend_def)        
  }
ultimately show "¬ rightPrincipal r (Compound M Ms) R" by blast
qed

lemma upRules_not_right_principal_for_modal:
assumes "r ∈ upRules"
  shows "¬ rightPrincipal r (Modal M Ms) R"
proof-
from assms obtain ps T Ts where "r = (ps,\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
     using upRuleCharacterise apply (cases r) apply auto apply (rotate_tac 2) apply (drule_tac x=a in meta_spec)
     apply (rotate_tac 2) by (drule_tac x=b in meta_spec) auto
moreover
   {assume "r = (ps,\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
    then have "¬ rightPrincipal r (Modal M Ms) R" apply auto apply (rule rightPrincipal.cases)
         by (auto simp add:extendRule_def extend_def) 
   }
moreover
   {assume "r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
    then have "¬ rightPrincipal r (Modal M Ms) R" apply auto apply (rule rightPrincipal.cases)
         by (auto simp add:extendRule_def extend_def)
   }
ultimately show "¬ rightPrincipal r (Modal M Ms) R" by blast
qed

lemma upRules_not_left_principal_for_modal:
assumes "r ∈ upRules"
shows "¬ leftPrincipal r (Modal M Ms) R"
using assms
proof-
from assms obtain ps T Ts where "r = (ps,\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
     using upRuleCharacterise apply (cases r) apply auto apply (rotate_tac 2) apply (drule_tac x=a in meta_spec)
     apply (rotate_tac 2) by (drule_tac x=b in meta_spec) auto
moreover
   {assume "r = (ps,\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
    then have "¬ leftPrincipal r (Modal M Ms) R" apply auto apply (rule leftPrincipal.cases) 
         by (auto simp add:extendRule_def extend_def)
   }
moreover
  {assume "r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
   then have "¬ leftPrincipal r (Modal M Ms) R" apply auto apply (rule leftPrincipal.cases)
        by (auto simp add:extendRule_def extend_def)
  }
ultimately show "¬ leftPrincipal r (Modal M Ms) R" by blast
qed

lemmas nonPrincipalRight = upRules_not_right_principal_for_modal
                           modRules_not_right_principal_for_compound
                           modRules2_not_right_principal_for_compound

lemmas nonPrincipalLeft = upRules_not_left_principal_for_modal
                          modRules_not_left_principal_for_compound
                          modRules2_not_left_principal_for_compound




(* Bunch of results about modalising multisets *)
lemma modalise_characterise:
fixes A :: "('a,'b) form"
and   M :: "'b"
and  Δ  :: "('a,'b) form multiset"
assumes "A ∈# M⋅Δ"
shows "∃ B. A = Modal M [B]"
proof-
 from assms have "Δ ≠ \<Empt>" by (auto simp add:modaliseEmpty)
 with ‹A ∈# M⋅Δ› show "∃ B. A = Modal M [B]" 
      proof (induct Δ)
      case empty
      then show ?case by simp
  next
      case (add x Δ')
      then have IH: "⟦ A ∈# M⋅Δ' ; Δ' ≠ \<Empt> ⟧ ⟹ ∃ B. A = Modal M [B]"
            and b: "A ∈# M ⋅ (Δ' ⊕ x)" by auto
      from b have "A ∈# M⋅Δ' ∨ A ∈# M⋅(\<LM>x\<RM>)" by (auto simp add:modaliseMultiset_def)
      moreover
         {assume "A ∈# M⋅Δ'"
          then have "Δ' ≠ \<Empt>" by (auto simp add:modaliseEmpty)
          with ‹A ∈# M⋅Δ'› have "∃ B. A = Modal M [B]" using IH by simp
         }
      moreover
         {assume "A ∈# M⋅(\<LM>x\<RM>)"
          then have "A ∈# \<LM> Modal M [x] \<RM>" by (auto simp add:modaliseMultiset_def)
          then have "A ∈ set_mset (\<LM>Modal M [x]\<RM>)" by (auto simp only:set_mset_def)
          then have "A ∈ {Modal M [x]}" by auto
          then have "A = Modal M [x]" by auto
          then have "∃ B. A = Modal M [B]" by blast
         }
      ultimately show ?case by blast
  qed
qed


lemma non_contain:
fixes Δ Δ' :: "('a,'b) form multiset"
assumes "Δ ≠ \<Empt>" and "Δ' ≠ \<Empt>" and "M ≠ N"
shows "set_mset (M⋅Δ) ∩ set_mset (N⋅Δ') = {}"
proof-
{
assume "set_mset (M⋅Δ) ∩ set_mset (N⋅Δ') ≠ {}"
then have "∃ A. A ∈ set_mset (M⋅Δ) ∩ set_mset (N⋅Δ')" by auto
then obtain A where a: "A ∈ set_mset (M⋅Δ) ∩ set_mset (N⋅Δ')" by blast
then have "False"
 proof- 
   from a have box: "A ∈ set_mset (M⋅Δ)" and dia: "A ∈ set_mset (N⋅Δ')" by auto
   from box have "A ∈# M⋅Δ" by auto
   with ‹Δ ≠ \<Empt>› have "∃ B. A = Modal M [B]" using modalise_characterise[where M=M] by (auto)
   then obtain B where "A = Modal M [B]" by blast
   moreover 
   from dia have "A ∈# N⋅Δ'" by auto
   with ‹Δ' ≠ \<Empt>› have "∃ C. A = Modal N [C]" using modalise_characterise[where M=N] by auto
   then obtain C where "A = Modal N [C]" by blast
   ultimately show "False" using ‹M≠N› by auto
 qed
}
then show ?thesis by auto
qed


lemma modal_neq:
fixes A :: "('a,'b) form" and ps :: "('a,'b) form list"
shows "A ≠ Modal M [A]" and "ps ≠ [Modal M ps]"
by (induct A and ps rule: compat_form.induct compat_form_list.induct) auto

lemma p_e_non_empty: 
 "r ∈ p_e R M N ⟹ fst r ≠ []"
apply (rule p_e.cases) apply auto
apply (subgoal_tac "(Ps, c) ∈ modRules2")
apply (rule modRules2.cases) by (auto simp add:extendRule_def)


(* -------------------------------
   -------------------------------
        ModalWeakening2.thy
   -------------------------------
   ------------------------------- *)


lemma dpWeak:
assumes a:"(Γ ⇒* Δ,n) ∈ derivable (ext R R2 M N)"
   and  b: "R1 ⊆ upRules"
   and  c: "R2 ⊆ modRules2"
   and  d: "R3 ⊆ modRules2"
   and  e: "R = Ax ∪ R1 ∪ (p_e R2 M N) ∪ R3" 
shows "(Γ + Γ' ⇒* Δ + Δ',n) ∈ derivable (ext R R2 M N)"
using a
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
case (1 n Γ Δ)
then have IH: "∀m<n. ∀ Γ Δ. ( Γ ⇒* Δ, m) ∈ derivable (ext R R2 M N) ⟶ ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M N)" 
      and a': "( Γ ⇒* Δ, n) ∈ derivable (ext R R2 M N)" by auto
show ?case
proof (cases n)
case 0
 then have "(Γ ⇒* Δ,0) ∈ derivable (ext R R2 M N)" using a' by simp
 then have "([], Γ ⇒* Δ) ∈ (ext R R2 M N)" by (cases) auto      
 then obtain  r S where "r ∈ R" and split:"(extendRule S r = ([],Γ ⇒* Δ) ∨ extendConc S r = ([],Γ ⇒* Δ))" 
      apply (rule ext.cases) by (auto simp add:extendRule_def extend_def extendConc_def)
 then obtain c where "r = ([],c)" by (cases r) (auto simp add:extendRule_def extendConc_def)
 with ‹r ∈ R› have "r ∈ Ax ∨ (r ∈ upRules ∪ (p_e R2 M N) ∪ modRules2)" using b c d e by auto
 with ‹r = ([],c)› have "r ∈ Ax" apply auto apply (rule upRules.cases,auto)
                                 defer
                                 apply (rule modRules2.cases, auto)
                                 apply (rule p_e.cases,auto simp add:extendRule_def)
                                 apply hypsubst_thin
                                 apply (insert p_e_non_empty[where R=R2 and M=M and N=N])
                                 apply (drule_tac x="([], extend ( M ⋅ Γ ⇒* N ⋅ Δ) c)" in meta_spec) by auto
 with ‹r = ([],c)› obtain i where "c = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>) ∨ c = (\<LM>ff\<RM> ⇒* \<Empt>)"
      using characteriseAx[where r=r] by auto
 moreover
    {assume "c = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"
     then have "extend S (\<LM>At i\<RM> ⇒*\<LM>At i\<RM>) = (Γ ⇒* Δ)" using split and ‹r = ([],c)›
          by (auto simp add:extendRule_def extendConc_def)
     then have "At i ∈# Γ ∧ At i ∈# Δ" using extendID by auto
     then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
     then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M N)" 
          using e and containID[where Γ="Γ+Γ'" and Δ="Δ+Δ'" and R=R and i=i] by auto
    }
 moreover
    {assume "c = (\<LM>ff\<RM> ⇒* \<Empt>)"
     then have "extend S (\<LM>ff\<RM> ⇒*\<Empt>) = (Γ ⇒* Δ)" using split and ‹r = ([],c)›
          by (auto simp add:extendRule_def extendConc_def)
     then have "ff ∈# Γ" using extendFalsum by auto
     then have "ff ∈# Γ + Γ'" by auto
     then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M N)" 
          using e and containFalsum[where Γ="Γ+Γ'" and Δ="Δ+Δ'" and R=R] by auto
    }
 ultimately show "(Γ + Γ' ⇒* Δ + Δ',n) ∈ derivable (ext R R2 M N)" using ‹n=0› by auto
next
case (Suc n')
 then have "(Γ ⇒* Δ, n'+1) ∈ derivable (ext R R2 M N)" using a' by simp
 then obtain Ps where f:"Ps ≠ []"
                  and g:"(Ps, Γ ⇒* Δ) ∈ (ext R R2 M N)" 
                  and h:"∀ p ∈ set Ps. ∃ m≤n'. (p,m) ∈ derivable (ext R R2 M N)" 
      using characteriseLast[where C="Γ ⇒* Δ" and m=n' and R="ext R R2 M N"] by auto
 from g c obtain S r where "r ∈ R" and "((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ)) ∨
                                  (r ∈ p_e R2 M N ∧ extendConc S r = (Ps, Γ ⇒* Δ))"
      by (cases) auto
 moreover
    {assume as:"(r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ)"
     then have eq:"map (extend (Γ' ⇒* Δ')) Ps = fst (extendRule (extend S (Γ' ⇒* Δ')) r)"
           using mapCommute[where S="Γ'⇒*Δ'" and R=S and c="fst r"]
           by (auto simp add:extendRule_def extend_def mapAssoc simp del: map_map)
     from as have eq2: "(Γ + Γ' ⇒* Δ + Δ') = snd (extendRule (extend S (Γ' ⇒* Δ')) r)"
           by (auto simp add:extendRule_def extend_def union_ac)
     from as f have "fst r ≠ []" by (auto simp add:extendRule_def map_is_Nil_conv)
     with as have "r ∈ upRules ∨ r ∈ modRules2" apply (cases r,auto) by (rule Ax.cases) auto
     have "∀ p' ∈ set (map (extend (Γ' ⇒* Δ')) Ps). ∃ m≤n'. (p',m) ∈ derivable (ext R R2 M N)"
          proof-
          {fix p
           assume "p ∈ set (map (extend (Γ' ⇒* Δ')) Ps)"
           then obtain p' where t:"p' ∈ set Ps ∧ p = extend (Γ' ⇒* Δ') p'" by auto
           with h obtain m where "m≤n'" and "(p',m) ∈ derivable (ext R R2 M N)" by auto
           moreover obtain Φ Ψ where eq:"p' = (Φ ⇒* Ψ)" by (cases p') auto 
           then have "p = (Φ + Γ' ⇒* Ψ + Δ')" using t by (auto simp add:extend_def union_ac)
           ultimately have "(p,m) ∈ derivable (ext R R2 M N)" using IH and ‹n = Suc n'› and eq
                apply- by (drule_tac x=m in spec) simp
           then have "∃ m≤n'. (p,m) ∈ derivable (ext R R2 M N)" using ‹m≤n'› by auto
           }
           then show ?thesis by auto
           qed
     then have "∀ p' ∈ set (fst (extendRule (extend S (Γ' ⇒* Δ')) r)).
                ∃ m≤n'. (p',m) ∈ derivable (ext R R2 M N)" using eq by auto
     moreover have "extendRule (extend S (Γ' ⇒* Δ')) r ∈ (ext R R2 M N)" 
              using ‹r ∈ upRules ∨ r ∈ modRules2› and ‹r ∈ R› by auto
     ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M N)"
              using derivable.step[where r="extendRule (extend S (Γ' ⇒* Δ')) r" and R="ext R R2 M N" and m="n'"]
              and ‹fst r ≠ []› and eq2 by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
     }
 moreover
     {assume as:"r ∈ p_e R2 M N ∧ extendConc S r = (Ps, Γ ⇒* Δ)"
      then have "(Γ + Γ' ⇒* Δ + Δ') = snd (extendConc (extend S (Γ' ⇒* Δ')) r)"
           by (auto simp add:extendConc_def extend_def union_ac)
      moreover from as have "Ps = fst (extendConc (extend S (Γ' ⇒* Δ')) r)"
           by (auto simp add:extendConc_def)
      moreover have "extendConc S r ∈ ext R R2 M N" using as and g by auto
      moreover have "extendConc (extend S (Γ' ⇒* Δ')) r ∈ ext R R2 M N" using as and ‹r ∈ R› and c
            and ext.mod1[where r=r and R'=R2 and M=M and N=N and R=R and seq="extend S (Γ' ⇒* Δ')"]
            by auto
      ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M N)"
           using h f and 
           derivable.step[where r="extendConc (extend S (Γ' ⇒* Δ')) r" and R="ext R R2 M N" and m="n'"]
           by auto
     }
 ultimately show "( Γ + Γ' ⇒* Δ + Δ', n) ∈ derivable (ext R R2 M N)" using ‹n = Suc n'› by auto
 qed
qed



(* -------------------------------
   -------------------------------
        ModalInvertibility.thy
   -------------------------------
   ------------------------------- *)

lemma nonPrincipalInvertRight:
assumes "R1 ⊆ upRules" and "R2 ⊆ modRules2" and "R3 ⊆ modRules2"
    and "R = Ax ∪ R1 ∪ p_e R2 M1 M2 ∪ R3" and "r ∈ R" and "r = (ps,c)"
    and "R' = Ax ∪ R1 ∪ R2 ∪ R3"
    and IH: "∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ Modal M Ms, m) ∈ derivable (ext R R2 M1 M2) ⟶
              (∀r' ∈ R'. rightPrincipal r' (Modal M Ms) R' ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶              
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable (ext R R2 M1 M2))"
    and a': "(Γ ⇒* Δ ⊕ Modal M Ms,n) ∈ derivable (ext R R2 M1 M2)" 
    and b': "∀ r' ∈ R'. rightPrincipal r' (Modal M Ms) R' ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and np: "¬ rightPrincipal r (Modal M Ms) R'"
    and ext: "(r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Modal M Ms)"
    and num: "n = n' + 1"
    and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)"
    and nonempty: "Ps ≠ []"  
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
proof-
 from ext nonempty have "r ∈ upRules ∨ r ∈ modRules2" apply (auto simp add:extendRule_def) apply (cases r) 
       apply (rotate_tac 3) by (rule Ax.cases) auto
 obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
 from ‹r = (ps,c)› obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
 then have "\<LM> Modal M Ms \<RM> ≠ H" 
      proof-
      {assume "r ∈ upRules"
       with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
             using upRuleCharacterise[where Ps=ps and C=c] by auto
       moreover
         {assume "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
          with ‹c = (G ⇒* H)› have "\<LM> Modal M Ms \<RM> ≠ H" by auto
         }
       moreover
         {assume "c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
          then have "\<LM>Modal M Ms \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
         }
       ultimately have "\<LM> Modal M Ms \<RM> ≠ H" by blast
      }
      moreover
      {assume "r ∈ modRules2" 
       with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>) ∨ c = (\<LM> Modal T Ts\<RM> ⇒* \<Empt>)"
             using modRule2Characterise[where Ps=ps and C=c] by auto
       moreover
         {assume "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>)"
          then have "rightPrincipal r (Modal T Ts) R'" using ‹r = (ps,c)› and ‹r ∈ R›
               proof-
               from ‹c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)› and ‹r = (ps,c)› and ‹r ∈ R› and ‹r ∈ modRules2›
                    have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R" by auto
               with ‹R = Ax ∪ R1 ∪ p_e R2 M1 M2 ∪ R3›
                    have "(ps,  \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ p_e R2 M1 M2 ∨
                          (ps,  \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R3" apply auto apply (rule Ax.cases) apply auto
                    apply (subgoal_tac "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ upRules") apply (insert ‹R1 ⊆ upRules›)
                    apply auto apply (rule upRules.cases) by auto
               moreover
                  {assume "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R3"
                   then have "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" using ‹R' = Ax ∪ R1 ∪ R2 ∪ R3› by auto
                  }
               moreover
                  {assume "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ p_e R2 M1 M2"
                   then obtain Γ' Δ' r' where aa: "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) = extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∧ r' ∈ R2"
                        apply (rule p_e.cases) by auto
                   then have "r' ∈ modRules2" using ‹R2 ⊆ modRules2› by auto
                   then obtain F Fs where 
                        "snd r' = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ snd r' = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                        using modRule2Characterise[where Ps="fst r'" and C="snd r'"] by auto
                   with aa have "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs) ∨
                                 (\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                        by (auto simp add:extendRule_def extend_def)
                   moreover
                      {assume "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs)"
                       then have "M1⋅Γ' = \<Empt>" and "\<LM>Modal T Ts\<RM> = M2⋅Δ' ⊕ Modal F Fs" by auto
                       then have "M1⋅Γ' = \<Empt>" and "Modal T Ts = Modal F Fs" and "M2⋅Δ' = \<Empt>"
                            using 
                            singleton_add_means_equal[where A="Modal T Ts" and Γ="M2⋅Δ'" and B="Modal F Fs"]
                            and singleton_add_means_empty[where A="Modal T Ts" and Γ="M2⋅Δ'" and B="Modal F Fs"] 
                            by (auto simp add:modaliseMultiset_def)
                       then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' = r'" using extendRuleEmpty[where r=r'] by auto
                       then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∈ R2" using aa by auto
                       then have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R2" using aa by auto
                       then have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" using ‹R' = Ax∪R1 ∪R2 ∪ R3 › by simp
                      }
                   moreover
                      {assume "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                       then have "\<Empt> = M1⋅Γ' ⊕ Modal F Fs" by auto
                       then have "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by auto
                      }
                   ultimately have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by blast
                  }
              ultimately have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by auto
              then show ?thesis using ‹r = (ps,c)› and ‹c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)› by auto
              qed
          with ‹¬ rightPrincipal r (Modal M Ms) R'› have "Modal T Ts ≠ Modal M Ms" by auto
          with ‹c = (G ⇒* H)› have "\<LM> Modal M Ms \<RM> ≠ H" using ‹c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>)› by auto
         }
       moreover
         {assume "c = (\<LM>Modal T Ts \<RM> ⇒* \<Empt>)"
          then have "\<LM>Modal M Ms \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
         }
       ultimately have "\<LM> Modal M Ms \<RM> ≠ H" by blast
      }
      ultimately show ?thesis using ‹r ∈ upRules ∨ r ∈ modRules2› by blast
      qed
 moreover have "succ S + succ (snd r) = (Δ ⊕ Modal M Ms)" 
          using ext and extendRule_def[where forms=S and R=r]
                    and extend_def[where forms=S and seq="snd r"] by auto
 then have "Ψ + H = Δ ⊕ Modal M Ms" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
 moreover from ‹r = (ps,c)› and ‹r ∈ upRules ∨ r ∈ modRules2› have "(ps,c) ∈ upRules ∨ (ps,c) ∈ modRules2" by auto
 then have "∃ A. c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)"
      using upRuleCharacterise[where Ps=ps and C=c]
        and modRule2Characterise[where Ps=ps and C=c] by auto
 then have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" using ‹c = (G ⇒* H)› by auto
 ultimately have "Modal M Ms ∈# Ψ"
     proof-
     have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
     moreover
     {assume "H = \<Empt>"
      then have "Ψ = Δ ⊕ Modal M Ms" using ‹Ψ + H = Δ ⊕ Modal M Ms› by auto
      then have "Modal M Ms ∈# Ψ" by auto
     }
     moreover
     {assume "∃ A. H = \<LM>A\<RM>"
      then obtain T where "H = \<LM>T\<RM>" by auto
      then have "Ψ ⊕ T = Δ ⊕ Modal M Ms" using ‹Ψ + H = Δ ⊕ Modal M Ms› by auto
      then have "set_mset (Ψ ⊕ T) = set_mset (Δ ⊕ Modal M Ms)" by auto
      then have "set_mset Ψ ∪ {T} = set_mset Δ ∪ {Modal M Ms}" by auto
      moreover from ‹H = \<LM>T\<RM>› and ‹\<LM>Modal M Ms\<RM> ≠ H› have "Modal M Ms ≠ T" by auto
      ultimately have "Modal M Ms ∈ set_mset Ψ" by auto
      then have "Modal M Ms ∈# Ψ" by auto
     }
     ultimately show "Modal M Ms ∈# Ψ" by blast
     qed
 then have "∃ Ψ1. Ψ = Ψ1 ⊕ Modal M Ms" 
      by (rule_tac x="Ψ ⊖ Modal M Ms" in exI) (auto simp add:multiset_eq_iff)
 then obtain Ψ1 where "S = (Φ ⇒* Ψ1 ⊕ Modal M Ms)" using ‹S = (Φ ⇒* Ψ)› by auto
 have "Ps = map (extend S) ps" using ext and extendRule_def[where forms=S and R=r] and ‹r = (ps,c)› by auto
 then have "∀ p ∈ set Ps. (∃ p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
 then have "∀ p ∈ set Ps. (Modal M Ms ∈# succ p)" 
      using ‹Modal M Ms ∈# Ψ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) 
      by (drule_tac x=x in spec) (auto simp add:extend_def)
 then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⇒* Ψ' ⊕ Modal M Ms)" using characteriseSeq
      apply (auto simp add:Ball_def) apply (drule_tac x=x in spec,simp) 
      apply (rule_tac x="antec x" in exI,rule_tac x="succ x ⊖ Modal M Ms" in exI) 
      by (drule_tac x=x in meta_spec) (auto simp add:multiset_eq_iff)
 with all have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ 
                             (Φ' ⇒* Ψ' ⊕ Modal M Ms,n) ∈ derivable (ext R R2 M1 M2) ∧ 
                              p = (Φ' ⇒* Ψ' ⊕Modal M Ms)"
                  by (auto simp add:Ball_def)
 then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ 
                              (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable (ext R R2 M1 M2) ∧ 
                              p = (Φ' ⇒* Ψ' ⊕ Modal M Ms)"
                  using num and b' and IH
                  apply (auto simp add:Ball_def) apply (drule_tac x=x in spec) apply simp
                  apply hypsubst_thin
                  apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                  apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
                  apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) arith
 obtain Ps' where eq: "Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps" by auto
 have "length Ps = length Ps'" using ‹Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps›
                               and ‹Ps = map (extend S) ps› by auto
 then have "Ps' ≠ []" using nonempty by auto
 from ‹r ∈ upRules ∨ r ∈ modRules2› and ‹r ∈ R› have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r ∈ (ext R R2 M1 M2)" by auto
 moreover have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
          using ‹S = (Φ ⇒* Ψ1 ⊕ Modal M Ms)› and ext and ‹r = (ps,c)› and eq
          by (auto simp add:extendRule_def extend_def)
 ultimately have "(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ (ext R R2 M1 M2)" by simp
 have c1:"∀ p ∈ set ps. extend S p ∈ set Ps" using ‹Ps = map (extend S) ps› by (simp add:Ball_def)           
 have c2:"∀ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p ∈ set Ps'" using eq by (simp add:Ball_def)
 then have eq2:"∀ p ∈ set Ps'. ∃ Φ' Ψ'. p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq
           by (auto simp add: extend_def) 
 have d1:"∀ p ∈ set Ps. ∃ p' ∈ set ps. p = extend S p'" using ‹Ps = map (extend S) ps› by (auto simp add:Ball_def Bex_def)
 then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
 moreover have d2: "∀ p ∈ set Ps'. ∃ p' ∈ set ps. p = extend (Φ + Γ' ⇒* Ψ1 + Δ') p'" using eq
             by (auto simp add:Ball_def Bex_def)
 then have "∀ p ∈ set Ps'. ∃ p'. p' ∈ set Ps" using c1 by (auto simp add:Ball_def Bex_def)
 have "∀ Φ' Ψ'. (Φ' ⇒* Ψ' ⊕ Modal M Ms) ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
                proof-
                 {fix Φ' Ψ'
                  assume "(Φ' ⇒* Ψ' ⊕ Modal M Ms) ∈ set Ps"  
                  then have "∃ p ∈ set ps. extend (Φ ⇒* Ψ1 ⊕ Modal M Ms) p = (Φ' ⇒* Ψ' ⊕ Modal M Ms)"
                       using ‹Ps = map (extend S) ps› and ‹S = (Φ ⇒* Ψ1 ⊕ Modal M Ms)› and a1 and d1
                            apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⇒* Ψ' ⊕ Modal M Ms" in spec)
                            by (drule_tac x="Φ' ⇒* Ψ' ⊕ Modal M Ms" in spec) (auto)
                  then obtain p where t:"p ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Modal M Ms) = extend (Φ ⇒* Ψ1 ⊕ Modal M Ms) p"
                       apply auto by (drule_tac x=p in meta_spec) (simp)
                  then obtain D B where "p = (D ⇒* B)" by (cases p) 
                  then have "(D ⇒* B) ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Modal M Ms) = extend (Φ ⇒* Ψ1 ⊕ Modal M Ms) (D ⇒* B)"
                       using t by auto
                  then have ant: "Φ' = Φ + D" and suc: "Ψ' ⊕ Modal M Ms = Ψ1 ⊕ Modal M Ms + B" 
                       using extend_def[where forms="Φ ⇒* Ψ1 ⊕ Modal M Ms" and seq="D ⇒* B"] by auto
                  from ant have "Φ' + Γ' = (Φ + Γ') + D" by (auto simp add:union_ac)
                  moreover
                  from suc have "Ψ' = Ψ1 + B" by auto
                  then have "Ψ' + Δ' = (Ψ1 + Δ') + B" by (auto simp add:union_ac)
                  ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B)" 
                       using extend_def[where forms="Φ+Γ'⇒*Ψ1+Δ'" and seq="D⇒*B"] by auto
                  moreover have "extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B) ∈ set Ps'" using ‹p = (D ⇒* B)› and t and c2 by auto
                  ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                  }
                  thus ?thesis by blast
                qed
             moreover
             have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⇒* Ψ' ⊕ Modal M Ms) ∈ set Ps"
                proof-
                  {fix Φ' Ψ'
                  assume "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"  
                  then have "∃ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p = (Φ' + Γ' ⇒* Ψ' + Δ')"
                       using eq and eq2 and d2
                            apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec)
                           by (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec) (auto)
                  then obtain p where t:"p ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') p"
                       apply auto by (drule_tac x=p in meta_spec) (simp)
                  then obtain D B where "p = (D ⇒* B)" by (cases p) 
                  then have "(D ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B)"
                       using t by auto
                  then have ant: "Φ' + Γ' = Φ + Γ' + D" and suc: "Ψ' + Δ' = Ψ1 + Δ' + B" 
                       using extend_def[where forms="Φ+Γ'⇒*Ψ1+Δ'" and seq="D⇒*B"] by auto
                  from ant have "Φ' + Γ' = (Φ + D) + Γ'" by (auto simp add:union_ac)
                  then have "Φ' = Φ + D" by simp
                  moreover
                  from suc have "Ψ' + Δ' = (Ψ1 + B) + Δ'" by (auto simp add:union_ac)
                  then have "Ψ' = Ψ1 + B" by simp
                  then have "Ψ' ⊕ Modal M Ms = (Ψ1 ⊕ Modal M Ms) + B" by (auto simp add:union_ac)
                  ultimately have "(Φ' ⇒* Ψ' ⊕ Modal M Ms) = extend (Φ ⇒* Ψ1 ⊕ Modal M Ms) (D ⇒* B)" 
                       using extend_def[where forms="Φ⇒*Ψ1⊕Modal M Ms" and seq="D⇒*B"] by auto
                  moreover have "extend (Φ  ⇒* Ψ1 ⊕ Modal M Ms) (D ⇒* B) ∈ set Ps" using ‹p = (D ⇒* B)› and t and c1
                       and ‹S = (Φ ⇒* Ψ1 ⊕ Modal M Ms)› by auto
                  ultimately have "(Φ' ⇒* Ψ' ⊕ Modal M Ms) ∈ set Ps" by simp
                  }
                  thus ?thesis by blast
                qed
 ultimately
 have "∀ Φ' Ψ'. ((Φ' ⇒* Ψ' ⊕ Modal M Ms) ∈ set Ps) = ((Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps')" by auto
 then have "∀ p ∈ set Ps'. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',n) ∈ derivable (ext R R2 M1 M2)
                 ∧ p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq2 and a2
      apply (simp add:Ball_def) apply (intro allI impI) apply (drule_tac x=x in spec) apply simp
      apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
      by (drule_tac x="Φ' ⇒* Ψ' ⊕ Modal M Ms" in spec) (simp)
 then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)" by auto
 then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using num
      and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ (ext R R2 M1 M2)› and ‹Ps' ≠ []›
      and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="ext R R2 M1 M2"]
      by (auto simp add:Ball_def Bex_def)
qed



(* Check this later. *)

lemma nonPrincipalInvertLeft:
assumes "R1 ⊆ upRules" and "R2 ⊆ modRules2" and "R3 ⊆ modRules2"
    and "R = Ax ∪ R1 ∪ p_e R2 M1 M2 ∪ R3" and "r ∈ R" and "r = (ps,c)" and "R' = Ax ∪ R1 ∪ R2 ∪ R3"
    and IH: "∀m<n. ∀Γ Δ. ( Γ ⊕ Modal M Ms ⇒* Δ, m) ∈ derivable (ext R R2 M1 M2) ⟶
              (∀r' ∈ R'. leftPrincipal r' (Modal M Ms) R' ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable (ext R R2 M1 M2) )"
    and a': "(Γ ⊕ Modal M Ms ⇒* Δ,n) ∈ derivable (ext R R2 M1 M2)" 
    and b': "∀ r' ∈ R'. leftPrincipal r' (Modal M Ms) R' ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and np: "¬ leftPrincipal r (Modal M Ms) R'"
    and ext: "((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⊕ Modal M Ms ⇒* Δ))"
    and num: "n = n' + 1"
    and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)"
    and nonempty: "Ps ≠ []"  
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
proof-
 from ext nonempty have "r ∈ upRules ∨ r ∈ modRules2" apply (auto simp add:extendRule_def) apply (cases r) 
       apply (rotate_tac 3) by (rule Ax.cases) auto
 obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
 from ‹r = (ps,c)› obtain G H where "c = (H ⇒* G)" by (cases c) (auto)
 then have "\<LM> Modal M Ms \<RM> ≠ H" 
      proof-
      {assume "r ∈ upRules"
       with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
             using upRuleCharacterise[where Ps=ps and C=c] by auto
       moreover
         {assume "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
          with ‹c = (H ⇒* G)› have "\<LM> Modal M Ms \<RM> ≠ H" by auto
         }
       moreover
         {assume "c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
          then have "\<LM>Modal M Ms \<RM> ≠ H" using ‹c = (H ⇒* G)› by auto
         }
       ultimately have "\<LM> Modal M Ms \<RM> ≠ H" by blast
      }
      moreover
      {assume "r ∈ modRules2" 
       with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>) ∨ c = (\<LM> Modal T Ts\<RM> ⇒* \<Empt>)"
             using modRule2Characterise[where Ps=ps and C=c] by auto
       moreover
         {assume "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>)"
          then have "\<LM>Modal M Ms \<RM> ≠ H" using ‹c = (H ⇒* G)› by auto          
         }
       moreover
         {assume "c = (\<LM>Modal T Ts \<RM> ⇒* \<Empt>)"
          then have "leftPrincipal r (Modal T Ts) R'" using ‹r = (ps,c)› and ‹r ∈ R›
               proof-
               from ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› and ‹r = (ps,c)› and ‹r ∈ R› and ‹r ∈ modRules2›
                    have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R" by auto
               with ‹R = Ax ∪ R1 ∪ p_e R2 M1 M2 ∪ R3›
                    have "(ps,  \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ p_e R2 M1 M2 ∨
                          (ps,  \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R3" apply auto apply (rule Ax.cases) apply auto
                    apply (subgoal_tac "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ upRules") apply (insert ‹R1 ⊆ upRules›)
                    apply auto apply (rule upRules.cases) by auto
               moreover
                  {assume "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R3"
                   then have "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" using ‹R' = Ax ∪ R1 ∪ R2 ∪ R3› by auto
                  }
               moreover
                  {assume "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ p_e R2 M1 M2"
                   then obtain Γ' Δ' r' where aa: "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) = extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∧ r' ∈ R2"
                        apply (rule p_e.cases) by auto
                   then have "r' ∈ modRules2" using ‹R2 ⊆ modRules2› by auto
                   then obtain F Fs where 
                        "snd r' = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ snd r' = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                        using modRule2Characterise[where Ps="fst r'" and C="snd r'"] by auto
                   with aa have "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs) ∨
                                 (\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                        by (auto simp add:extendRule_def extend_def)
                   moreover
                      {assume "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs)"
                       then have "\<Empt> = M2⋅Δ' ⊕ Modal F Fs" by auto
                       then have "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by auto 
                      }
                   moreover
                      {assume "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                       then have "M1⋅Γ' ⊕ Modal F Fs = \<LM>Modal T Ts\<RM>" and "\<Empt> = M2⋅Δ'" by auto
                       then have "M1⋅Γ' = \<Empt>" and "Modal T Ts = Modal F Fs" and "M2⋅Δ' = \<Empt>"
                            using 
                            singleton_add_means_equal[where A="Modal T Ts" and Γ="M1⋅Γ'" and B="Modal F Fs"]
                            and singleton_add_means_empty[where A="Modal T Ts" and Γ="M1⋅Γ'" and B="Modal F Fs"] 
                            by (auto simp add:modaliseMultiset_def)
                       then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' = r'" using extendRuleEmpty[where r=r'] by auto
                       then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∈ R2" using aa by auto
                       then have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R2" using aa by auto
                       then have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" using ‹R' = Ax∪R1 ∪R2 ∪ R3 › by simp
                      }
                   ultimately have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by blast
                  }
              ultimately have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by auto
              then show ?thesis using ‹r = (ps,c)› and ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› by auto
              qed
          then have "leftPrincipal r (Modal T Ts) R'" using ‹r = (ps,c)› by auto
          with ‹¬ leftPrincipal r (Modal M Ms) R'› have "Modal T Ts ≠ Modal M Ms" by auto
          with ‹c = (H ⇒* G)› have "\<LM> Modal M Ms \<RM> ≠ H" using ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› by auto
         }
       ultimately have "\<LM> Modal M Ms \<RM> ≠ H" by blast
      }
      ultimately show ?thesis using ‹r ∈ upRules ∨ r ∈ modRules2› by blast
      qed
 moreover have "antec S + antec (snd r) = (Γ ⊕ Modal M Ms)" 
          using ext and extendRule_def[where forms=S and R=r]
                    and extend_def[where forms=S and seq="snd r"] by auto
 then have "Φ + H = Γ ⊕ Modal M Ms" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (H ⇒* G)› by auto
 moreover from ‹r = (ps,c)› and ‹r ∈ upRules ∨ r ∈ modRules2› have "(ps,c) ∈ upRules ∨ (ps,c) ∈ modRules2" by auto
 then have "∃ A. c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)"
      using upRuleCharacterise[where Ps=ps and C=c]
        and modRule2Characterise[where Ps=ps and C=c] by auto
 then have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" using ‹c = (H ⇒* G)› by auto
 ultimately have "Modal M Ms ∈# Φ"
     proof-
     have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
     moreover
     {assume "H = \<Empt>"
      then have "Φ = Γ ⊕ Modal M Ms" using ‹Φ + H = Γ ⊕ Modal M Ms› by auto
      then have "Modal M Ms ∈# Φ" by auto
     }
     moreover
     {assume "∃ A. H = \<LM>A\<RM>"
      then obtain T where "H = \<LM>T\<RM>" by auto
      then have "Φ ⊕ T = Γ ⊕ Modal M Ms" using ‹Φ + H = Γ ⊕ Modal M Ms› by auto
      then have "set_mset (Φ ⊕ T) = set_mset (Γ ⊕ Modal M Ms)" by auto
      then have "set_mset Φ ∪ {T} = set_mset Γ ∪ {Modal M Ms}" by auto
      moreover from ‹H = \<LM>T\<RM>› and ‹\<LM>Modal M Ms\<RM> ≠ H› have "Modal M Ms ≠ T" by auto
      ultimately have "Modal M Ms ∈ set_mset Φ" by auto
      then have "Modal M Ms ∈# Φ" by auto
     }
     ultimately show "Modal M Ms ∈# Φ" by blast
     qed
 then have "∃ Φ1. Φ = Φ1 ⊕ Modal M Ms" 
      by (rule_tac x="Φ ⊖ Modal M Ms" in exI) (auto simp add:multiset_eq_iff)
 then obtain Φ1 where "S = (Φ1 ⊕ Modal M Ms ⇒* Ψ)" using ‹S = (Φ ⇒* Ψ)› by auto
 have "Ps = map (extend S) ps" using ext and extendRule_def[where forms=S and R=r] and ‹r = (ps,c)› by auto
 then have "∀ p ∈ set Ps. (∃ p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
 then have "∀ p ∈ set Ps. (Modal M Ms ∈# antec p)" 
      using ‹Modal M Ms ∈# Φ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) 
      by (drule_tac x=x in spec) (auto simp add:extend_def)
 then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ'⊕ Modal M Ms ⇒* Ψ')" using characteriseSeq
      apply (auto simp add:Ball_def) apply (drule_tac x=x in spec,simp) 
      apply (rule_tac x="antec x ⊖ Modal M Ms" in exI,rule_tac x="succ x" in exI) 
      by (drule_tac x=x in meta_spec) (auto simp add:multiset_eq_iff)
 with all have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ'⊕ Modal M Ms ⇒* Ψ',n) ∈ derivable (ext R R2 M1 M2) ∧ 
                              p = (Φ'⊕Modal M Ms ⇒* Ψ')"
                  by (auto simp add:Ball_def)
 then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable (ext R R2 M1 M2) ∧ 
                  p = (Φ'⊕Modal M Ms ⇒* Ψ')"
                  using num and b' and IH 
                  apply (auto simp add:Ball_def) apply (drule_tac x=x in spec) apply simp
                  apply hypsubst_thin
                  apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                  apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
                  apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) (arith)
 obtain Ps' where eq: "Ps' = map (extend (Φ1 + Γ' ⇒* Ψ + Δ')) ps" by auto
 have "length Ps = length Ps'" using ‹Ps' = map (extend (Φ1 + Γ' ⇒* Ψ + Δ')) ps›
                               and ‹Ps = map (extend S) ps› by auto
 then have "Ps' ≠ []" using nonempty by auto
 from ‹r ∈ upRules ∨ r ∈ modRules2› and ‹r ∈ R› have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r ∈ (ext R R2 M1 M2)" by auto
 moreover have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
          using ‹S = (Φ1 ⊕ Modal M Ms ⇒* Ψ)› and ext and ‹r = (ps,c)› and eq
          by (auto simp add:extendRule_def extend_def)
 ultimately have "(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ (ext R R2 M1 M2)" by simp
 have c1:"∀ p ∈ set ps. extend S p ∈ set Ps" using ‹Ps = map (extend S) ps› by (simp add:Ball_def)           
 have c2:"∀ p ∈ set ps. extend (Φ1 + Γ' ⇒* Ψ + Δ') p ∈ set Ps'" using eq by (simp add:Ball_def)
 then have eq2:"∀ p ∈ set Ps'. ∃ Φ' Ψ'. p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq
           by (auto simp add: extend_def) 
 have d1:"∀ p ∈ set Ps. ∃ p' ∈ set ps. p = extend S p'" using ‹Ps = map (extend S) ps› by (auto simp add:Ball_def Bex_def)
 then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
 moreover have d2: "∀ p ∈ set Ps'. ∃ p' ∈ set ps. p = extend (Φ1 + Γ' ⇒* Ψ + Δ') p'" using eq
             by (auto simp add:Ball_def Bex_def)
 then have "∀ p ∈ set Ps'. ∃ p'. p' ∈ set Ps" using c1 by (auto simp add:Ball_def Bex_def)
 have "∀ Φ' Ψ'. (Φ'⊕ Modal M Ms ⇒* Ψ') ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
                proof-
                 {fix Φ' Ψ'
                  assume "(Φ' ⊕ Modal M Ms⇒* Ψ') ∈ set Ps"  
                  then have "∃ p ∈ set ps. extend (Φ1⊕ Modal M Ms ⇒* Ψ) p = (Φ'⊕ Modal M Ms ⇒* Ψ')"
                       using ‹Ps = map (extend S) ps› and ‹S = (Φ1⊕ Modal M Ms ⇒* Ψ)› and a1 and d1
                            apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ'⊕ Modal M Ms ⇒* Ψ'" in spec)
                            by (drule_tac x="Φ'⊕ Modal M Ms ⇒* Ψ'" in spec) (auto)
                  then obtain p where t:"p ∈ set ps ∧ (Φ'⊕ Modal M Ms ⇒* Ψ') = extend (Φ1⊕ Modal M Ms ⇒* Ψ) p"
                       apply auto by (drule_tac x=p in meta_spec) (simp)
                  then obtain D B where "p = (D ⇒* B)" by (cases p) 
                  then have "(D ⇒* B) ∈ set ps ∧ (Φ'⊕ Modal M Ms ⇒* Ψ') = extend (Φ1⊕ Modal M Ms ⇒* Ψ) (D ⇒* B)"
                       using t by auto
                  then have ant: "Φ'⊕ Modal M Ms = Φ1⊕ Modal M Ms + D" and suc: "Ψ' = Ψ + B" 
                       using extend_def[where forms="Φ1⊕ Modal M Ms ⇒* Ψ" and seq="D ⇒* B"] by auto
                  from suc have "Ψ' + Δ' = (Ψ + Δ') + B" by (auto simp add:union_ac)
                  moreover
                  from ant have "Φ' = Φ1 + D" by auto
                  then have "Φ' + Γ' = (Φ1 + Γ') + D" by (auto simp add:union_ac)
                  ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B)" 
                       using extend_def[where forms="Φ1+Γ'⇒*Ψ+Δ'" and seq="D⇒*B"] by auto
                  moreover have "extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B) ∈ set Ps'" using ‹p = (D ⇒* B)› and t and c2 by auto
                  ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                  }
                  thus ?thesis by blast
                qed
             moreover
             have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⊕ Modal M Ms ⇒* Ψ') ∈ set Ps"
                proof-
                  {fix Φ' Ψ'
                  assume "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"  
                  then have "∃ p ∈ set ps. extend (Φ1 + Γ' ⇒* Ψ + Δ') p = (Φ' + Γ' ⇒* Ψ' + Δ')"
                       using eq and eq2 and d2
                            apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec)
                           by (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec) (auto)
                  then obtain p where t:"p ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') p"
                       apply auto by (drule_tac x=p in meta_spec) (simp)
                  then obtain D B where "p = (D ⇒* B)" by (cases p) 
                  then have "(D ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B)"
                       using t by auto
                  then have ant: "Φ' + Γ' = Φ1 + Γ' + D" and suc: "Ψ' + Δ' = Ψ + Δ' + B" 
                       using extend_def[where forms="Φ1+Γ'⇒*Ψ+Δ'" and seq="D⇒*B"] by auto
                  from suc have "Ψ' + Δ' = (Ψ + B) + Δ'" by (auto simp add:union_ac)
                  then have "Ψ' = Ψ + B" by simp
                  moreover
                  from ant have "Φ' + Γ' = (Φ1 + D) + Γ'" by (auto simp add:union_ac)
                  then have "Φ' = Φ1 + D" by simp
                  then have "Φ' ⊕ Modal M Ms = (Φ1 ⊕ Modal M Ms) + D" by (auto simp add:union_ac)
                  ultimately have "(Φ' ⊕ Modal M Ms ⇒* Ψ' ) = extend (Φ1⊕ Modal M Ms ⇒* Ψ) (D ⇒* B)" 
                       using extend_def[where forms="Φ1 ⊕ Modal M Ms⇒*Ψ" and seq="D⇒*B"] by auto
                  moreover have "extend (Φ1⊕Modal M Ms  ⇒* Ψ) (D ⇒* B) ∈ set Ps" using ‹p = (D ⇒* B)› and t and c1
                       and ‹S = (Φ1 ⊕ Modal M Ms ⇒* Ψ)› by auto
                  ultimately have "(Φ' ⊕ Modal M Ms ⇒* Ψ' ) ∈ set Ps" by simp
                  }
                  thus ?thesis by blast
                qed
 ultimately
 have "∀ Φ' Ψ'. ((Φ'⊕ Modal M Ms ⇒* Ψ' ) ∈ set Ps) = ((Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps')" by auto
 then have "∀ p ∈ set Ps'. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',n) ∈ derivable (ext R R2 M1 M2)
                 ∧ p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq2 and a2
      apply (simp add:Ball_def) apply (intro allI impI) apply (drule_tac x=x in spec) apply simp
      apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
      by (drule_tac x="Φ'⊕ Modal M Ms ⇒* Ψ' " in spec) (simp)
 then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)" by auto
 then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using num
      and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ (ext R R2 M1 M2)› and ‹Ps' ≠ []›
      and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="(ext R R2 M1 M2)"]
      by (auto simp add:Ball_def Bex_def)
qed


(*>*)
text‹
We have two different inversion lemmata, depending on whether the rule was a modalised context rule, or some other kind of rule.  We only show the former, since the latter is much the same as earlier proofs.  The interesting cases are picked out:
›
lemma rightInvert:
fixes Γ Δ :: "('a,'b) form multiset"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ modRules2 ∧ R3 ⊆ modRules2 ∧ 
                R = Ax ∪ R1 ∪ (p_e R2 M1 M2) ∪ R3 ∧
                R' = Ax ∪ R1 ∪ R2 ∪ R3"
    and   a: "(Γ ⇒* Δ ⊕ Modal M Ms,n) ∈ derivable (ext R R2 M1 M2)"
    and   b: "∀ r' ∈ R'. rightPrincipal r' (Modal M Ms) R' ⟶ 
                         (Γ' ⇒* Δ') ∈ set (fst r')"
    and  neq: "M2 ≠ M"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"

(*<*)
using assms
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ Modal M Ms, m) ∈ derivable (ext R R2 M1 M2) ⟶
              (∀r' ∈ R'. rightPrincipal r' (Modal M Ms) R' ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable (ext R R2 M1 M2))" 
     and a': "(Γ ⇒* Δ ⊕ Modal M Ms,n) ∈ derivable (ext R R2 M1 M2)" 
     and b': "∀ r' ∈ R'. rightPrincipal r' (Modal M Ms) R' ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(Γ ⇒* Δ ⊕ Modal M Ms,0) ∈ derivable (ext R R2 M1 M2)" using a' by simp
     then have "([],Γ ⇒* Δ ⊕ Modal M Ms) ∈ ext R R2 M1 M2" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⇒* Δ ⊕ Modal M Ms) ∧ (r ∈ Ax)"
          using rules apply- apply (rule ext.cases [where 'a = 'a and 'b = 'b]) apply (auto simp add:extendRule_def extend_def)
          apply (rule_tac x=b in exI) apply (rule_tac x=seq in exI) apply auto apply (rule upRules.cases) apply auto
          apply (rule upRules.cases) apply auto apply (rule upRules.cases) apply auto
          apply (insert p_e_non_empty[where R=R2 and M=M1 and N=M2])
          apply (rule Ax.cases) apply auto apply (drule_tac x="[]" in meta_spec) 
          apply (drule_tac x="\<LM>At i\<RM> ⇒* \<LM>At i\<RM>" in meta_spec) apply auto
          apply (drule_tac x="[]" in meta_spec) apply (drule_tac x="\<LM>ff\<RM> ⇒* \<Empt>" in meta_spec) apply auto
          apply (drule_tac x=a in meta_spec) apply (drule_tac x=b in meta_spec) apply (auto simp add:extendConc_def)
          apply (drule_tac x="[]" in meta_spec) apply (drule_tac x=b in meta_spec) apply auto
          apply (subgoal_tac "([],b) ∈ modRules2") by (rule modRules2.cases,auto)+
     then obtain r S where "extendRule S r = ([],Γ ⇒* Δ ⊕ Modal M Ms)" and "r ∈ Ax" by auto
     then obtain i xs where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨ r = ([],\<LM>ff\<RM> ⇒* \<Empt>)" 
          using characteriseAx[where r=r] by auto
     moreover 
         {assume "r = ([],\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"
          with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ Modal M Ms)›
               have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ ⊕ Modal M Ms)"
               using extendRule_def[where R="([],\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)" and forms=S] by auto
          then have "At i ∈# Γ ∧ At i ∈# Δ" 
               using extendID[where S=S and i=i and Γ=Γ and Δ="Δ ⊕ Modal M Ms"] by auto
          then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
          then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" using rules
               and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R] by auto
         }
     moreover
         {assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
          with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ Modal M Ms)›
             have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ ⊕ Modal M Ms)"
             using extendRule_def[where R="([],\<LM>ff\<RM> ⇒* \<Empt>)" and forms=S] by auto
          then have "ff ∈# Γ" 
               using extendFalsum[where S=S and Γ=Γ and Δ="Δ ⊕ Modal M Ms"] by auto
          then have "ff ∈# Γ + Γ'" by auto
          then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" using rules
               and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R] by auto
         }
     ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" by blast
     then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n=0› by auto
 next
     case (Suc n')
     then have "(Γ ⇒* Δ ⊕ Modal M Ms,n'+1) ∈ derivable (ext R R2 M1 M2)" using a' by simp
     then obtain Ps where "(Ps, Γ ⇒* Δ ⊕ Modal M Ms) ∈ (ext R R2 M1 M2)" and 
                          "Ps ≠ []" and 
                       d':"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)"
          using characteriseLast[where C="Γ ⇒* Δ ⊕ Modal M Ms" and m=n' and R="ext R R2 M1 M2"] by auto
     then have "∃ r S. (((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Modal M Ms)) ∨
                       (r ∈ p_e R2 M1 M2 ∧ extendConc S r = (Ps,Γ ⇒* Δ ⊕ Modal M Ms))) ∧ r∈R" by (cases) auto
     then obtain r S where ext: "((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Modal M Ms))
                                ∨ (r ∈ p_e R2 M1 M2 ∧ extendConc S r = (Ps,Γ ⇒* Δ ⊕ Modal M Ms))" and "r ∈ R" by auto
     moreover
        {assume ext1: "(r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Modal M Ms)"
         with ‹Ps ≠ []› have "r ∈ upRules ∨ r ∈ modRules2" and "extendRule S r = (Ps,Γ ⇒* Δ ⊕ Modal M Ms)" 
               apply auto apply (cases r) 
               by (rule Ax.cases) (auto simp add:extendRule_def)
         moreover
            {assume "r ∈ upRules"
             with ‹r ∈ R› have "r ∈ R1" using rules [[hypsubst_thin=true]]
                  apply auto apply (insert disjoint) apply auto
                  apply (insert upRuleCharacterise) apply (rotate_tac 10) apply (drule_tac x="fst r" in meta_spec)
                  apply (rotate_tac 10) apply (drule_tac x="snd r" in meta_spec) apply simp
                  apply (elim exE) 
                  apply (insert modRule1Characterise[where Ps="fst r" and C="snd r" and R=R2 and M=M1 and N=M2])
                  by (auto simp add:extendRule_def extend_def)
             with rules have "r ∈ R'" by auto
             obtain ps c where "r = (ps,c)" by (cases r) auto
             with ‹r ∈ upRules› obtain T Ts where sw:"c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ 
                                                   c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                  using upRuleCharacterise[where Ps=ps and C=c] by auto
             have "(rightPrincipal r (Modal M Ms) R') ∨ ¬(rightPrincipal r (Modal M Ms) R')" by blast
             moreover
                {assume "rightPrincipal r (Modal M Ms) R'"
                 then have "c = (\<Empt> ⇒* \<LM>Modal M Ms\<RM>)" using ‹r = (ps,c)› by (cases) auto
                 with sw and ‹r ∈ R'› have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
                      by auto
                }
             moreover
                {assume "¬ rightPrincipal r (Modal M Ms) R'"
                 then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using IH and a' b' d' ‹Ps ≠ []›
                      and nonPrincipalInvertRight[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and n=n
                                                  and Γ=Γ and Δ=Δ and M=M and Ms=Ms and r=r and S=S
                                                  and Γ'=Γ' and Δ'=Δ' and n'=n' and Ps=Ps and ps=ps 
                                                  and c=c and R'=R' and ?M1.0=M1 and ?M2.0=M2]
                      and ‹n = Suc n'› and ext1 and rules and ‹r = (ps,c)› and ‹r ∈ R› by auto
                }
             ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by blast
            }
         moreover
(*>*)

txt‹\noindent This is the case where the last inference was a normal modal inference:›

  {assume "r ∈ modRules2"
   obtain ps c where "r = (ps,c)" by (cases r) auto
   with ‹r ∈ modRules2› obtain T Ts where "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>) ∨ 
            c = (\<LM> Modal T Ts\<RM> ⇒* \<Empt>)"
            using modRule2Characterise[where Ps=ps and C=c] by auto
   moreover
     {assume "c = (\<Empt> ⇒* \<LM> Modal T Ts \<RM>)"
      then have bb: "rightPrincipal r (Modal T Ts) R'" using ‹r = (ps,c)› and ‹r ∈ R›
      proof-  
txt‹\noindent We need to know $r \in R$ so that we can extend the active part›
    from ‹c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)› and 
           ‹r = (ps,c)› and 
           ‹r ∈ R› and 
           ‹r ∈ modRules2›
        have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R" by auto
    with rules have "(ps,  \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ p_e R2 M1 M2 ∨
         (ps,  \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R3" (*<*)apply auto apply (rule Ax.cases) apply auto
                 apply (subgoal_tac "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ upRules")
                                apply auto apply (rule upRules.cases)(*>*) by auto
   moreover
      {assume "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R3"
        then have "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" using rules by auto
       }
   moreover
      {assume "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ p_e R2 M1 M2"

txt‹\noindent In this case, we show that $\Delta'$ and $\Gamma'$ must be empty.  The details are generally suppressed:›
  then obtain Γ' Δ' r' 
  where aa: "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) = extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' 
            ∧ r' ∈ R2"(*<*)apply (rule p_e.cases)(*>*) by auto
  (*<*) then have "r' ∈ modRules2" using rules by auto
                              then obtain F Fs where 
                                   "snd r' = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ snd r' = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                                   using modRule2Characterise[where Ps="fst r'" and C="snd r'"] by auto
                              with aa have "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs) ∨
                                            (\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                                   by (auto simp add:extendRule_def extend_def)
                              moreover
                                 {assume "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs)"
                                  then have "M1⋅Γ' = \<Empt>" and "\<LM>Modal T Ts\<RM> = M2⋅Δ' ⊕ Modal F Fs" by auto(*>*) 
     then have "M1⋅Γ' = \<Empt>" (*<*)and "Modal T Ts = Modal F Fs"(*>*) and "M2⋅Δ' = \<Empt>"
     (*<*)    using 
                                       singleton_add_means_equal[where A="Modal T Ts" and Γ="M2⋅Δ'" and B="Modal F Fs"]
                                       and singleton_add_means_empty[where A="Modal T Ts" and Γ="M2⋅Δ'" and B="Modal F Fs"] (*>*) by (auto simp add:modaliseMultiset_def)
                      (*<*)            then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' = r'" using extendRuleEmpty[where r=r'] by auto
     
   then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∈ R2" using aa by auto
                                  then have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R2" using aa by auto
                                  then have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" using rules by simp
                                 }
                              moreover
                                 {assume "(\<Empt> ⇒* \<LM>Modal T Ts\<RM>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                                  then have "\<Empt> = M1⋅Γ' ⊕ Modal F Fs" by auto
                                  then have "(ps, \<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by auto
                                 }
                              ultimately have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by blast
                             }
                         ultimately have "(ps,\<Empt> ⇒* \<LM>Modal T Ts\<RM>) ∈ R'" by auto
                         then show ?thesis using ‹r = (ps,c)› and ‹c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)› by auto
                         qed
                    have "Modal T Ts = Modal M Ms ∨ Modal T Ts ≠ Modal M Ms" by blast
                    moreover
                       {assume "Modal T Ts = Modal M Ms"
                        with bb have "rightPrincipal r (Modal M Ms) R'" by auto
                        with b' have "(Γ' ⇒* Δ') ∈ set (fst r)" apply- by (rule rightPrincipal.cases) auto
                        moreover from ‹r = (ps,c)› and ‹c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)› and ‹Modal T Ts = Modal M Ms›
                                 and ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Modal M Ms)›
                                 have "S = (Γ ⇒* Δ)" apply (auto simp add:extendRule_def extend_def) by (cases S) auto
                        ultimately have "(Γ+Γ' ⇒* Δ+Δ') ∈ set Ps" 
                             using extendContain[where r=r and ps=ps and c=c and Ps=Ps 
                                               and C="Γ ⇒* Δ ⊕ Modal M Ms" and S="Γ ⇒* Δ" and p="Γ'⇒*Δ'"]
                             and ‹r = (ps,c)› and ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Modal M Ms)› by (auto simp add:extend_def)
                        with d' have "∃ n≤n'. (Γ+Γ' ⇒* Δ+Δ',n) ∈ derivable (ext R R2 M1 M2)" by auto
                        with ‹n = Suc n'› have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)"
                             apply auto apply (rule_tac x=n in exI) by arith
                       }
                    moreover
                       {assume "Modal T Ts ≠ Modal M Ms"
                        with bb have "¬ rightPrincipal r (Modal M Ms) R'" apply auto apply (rule rightPrincipal.cases)
                             apply auto apply (rotate_tac 1) apply (rule rightPrincipal.cases) apply auto
                             apply (rule rightPrincipal.cases) apply auto apply (rotate_tac 1)
                             by (rule rightPrincipal.cases) auto
                        then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using IH and a' b' d' ‹Ps ≠ []›
                             and nonPrincipalInvertRight[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and n=n
                                                  and Γ=Γ and Δ=Δ and M=M and Ms=Ms and r=r and S=S
                                                  and Γ'=Γ' and Δ'=Δ' and n'=n' and Ps=Ps and ps=ps 
                                                  and c=c and R'=R' and ?M1.0=M1 and ?M2.0=M2]
                             and ‹n = Suc n'› and ext1 and rules and ‹r = (ps,c)› and ‹r ∈ R› by auto
                       }
                    ultimately have " ∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
                   }
                moreover
                   {assume "c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
                    with ‹r = (ps,c)› have "¬ rightPrincipal r (Modal M Ms) R'"
                         apply auto by (rule rightPrincipal.cases) auto
                    then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using IH and a' b' d' ‹Ps ≠ []›
                         and nonPrincipalInvertRight[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and n=n
                                                  and Γ=Γ and Δ=Δ and M=M and Ms=Ms and r=r and S=S
                                                  and Γ'=Γ' and Δ'=Δ' and n'=n' and Ps=Ps and ps=ps 
                                                  and c=c and R'=R' and ?M1.0=M1 and ?M2.0=M2]
                         and ‹n = Suc n'› and ext1 and rules and ‹r = (ps,c)› and ‹r ∈ R› by auto
                   }
                ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
               }
            ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
           }
       moreover(*>*)
txt‹\noindent  The other interesting case is where the last inference was a modalised context inference:›

 {assume ba: "r ∈ p_e R2 M1 M2 ∧ 
         extendConc S r = (Ps,  Γ ⇒* Δ ⊕ Modal M Ms)"
  with rules obtain F Fs Γ'' Δ'' ps r' where
       ca: "r = extendRule (M1⋅Γ'' ⇒* M2⋅Δ'') r'" and 
       cb: "r' ∈ R2" and
     cc:  "r' = (ps, \<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
  (*<*)using modRule1Characterise[where Ps="fst r" and C="snd r" and M=M1 and N=M2 and R=R2] by auto
  obtain Γ1 Δ1 where "S = (Γ1 ⇒* Δ1)" by (cases S) auto
  moreover
    {assume "r' = (ps, \<Empt> ⇒* \<LM>Modal F Fs\<RM>)"
     with ba ca ‹S = (Γ1 ⇒* Δ1)› have
   eq1: "(M1⋅Γ'' + Γ1 ⇒* M2⋅Δ'' + Δ1 ⊕ Modal F Fs) = (Γ ⇒* Δ ⊕ Modal M Ms)"
            by (auto simp add:extendRule_def extend_def extendConc_def union_ac)
     (*<*)         then have eq2: "M2⋅Δ'' + Δ1 ⊕ Modal F Fs = Δ ⊕ Modal M Ms" by auto
                then have "set_mset (M2 ⋅ Δ'' + Δ1 ⊕ Modal F Fs) = set_mset (Δ ⊕ Modal M Ms)" by auto
                then have "set_mset (\<LM>Modal M Ms\<RM>) ⊆ set_mset (M2 ⋅ Δ'') ∪ set_mset Δ1 ∪  {Modal F Fs}" by auto (*>*)
  then have "Modal M Ms ∈ set_mset (M2⋅Δ'') ∨ 
             Modal M Ms ∈ set_mset Δ1 ∨ 
             Modal M Ms = Modal F Fs"
       by auto
  moreover
     {assume "Modal M Ms ∈ set_mset (M2⋅Δ'')" ― ‹Contradiction›
     then have "Modal M Ms ∈# M2⋅Δ''" by auto
     with (*<*)modal_not_contain[where M=M and N=M2 and A=Ms and Γ=Δ''] and(*>*) neq
       have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" 
       by auto
    }
 moreover
   {assume "Modal M Ms = Modal F Fs" ― ‹The last inference is principal›
   then have "r' = (ps, \<Empt> ⇒* \<LM>Modal M Ms\<RM>)" 
        using ‹r' = (ps,\<Empt> ⇒* \<LM>Modal F Fs\<RM>)› by simp
   with cb and rules have "rightPrincipal r' (Modal M Ms) R'" 
        and "r' ∈ R'" by auto
   with b have "(Γ' ⇒* Δ') ∈ set ps" using ‹r' = (ps, \<Empt> ⇒* \<LM>Modal M Ms\<RM>)›
       by (auto simp add:Ball_def)
  (*<*)    then have "extend (M1⋅Γ'' ⇒* M2⋅Δ'') (Γ' ⇒* Δ') 
                               ∈ set (map (extend (M1⋅Γ'' ⇒* M2⋅Δ'')) ps)" by auto
                    moreover from ba and ‹r' = (ps, \<Empt> ⇒* \<LM>Modal M Ms\<RM>)› and ca
                         have "Ps = map (extend (M1⋅Γ'' ⇒* M2⋅Δ'')) ps"
                         by (auto simp add:extendRule_def extendConc_def)
                    moreover have "extend (M1⋅Γ'' ⇒* M2⋅Δ'') (Γ' ⇒* Δ') = (M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ')" 
                         by (auto simp add:extend_def) 
                    ultimately have "(M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ') ∈ set Ps" by auto
                    with d' have "∃ m≤n'. (M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ',m) ∈ derivable (ext R R2 M1 M2)" by auto
                    then have "∃ m≤n'. (M1⋅Γ'' + Γ' + Γ1 ⇒* M2⋅Δ'' + Δ' + Δ1,m) ∈ derivable (ext R R2 M1 M2)"
                         using dpWeak[where Γ="M1⋅Γ'' + Γ'" and Δ="M2⋅Δ'' + Δ'" and R=R and ?R2.0=R2
                                      and M=M1 and N=M2 and ?R1.0=R1 and ?R3.0=R3 and Γ'=Γ1 and Δ'=Δ1] 
                         and rules by auto
                    with ‹n = Suc n'› 
                         have ee: "∃ m≤n. (M1⋅Γ'' + Γ' + Γ1 ⇒* M2⋅Δ'' + Δ' + Δ1,m) ∈ derivable (ext R R2 M1 M2)"
                         apply auto apply (rule_tac x=m in exI) by arith
                    from eq1 have "M1⋅Γ'' + Γ1 = Γ" by auto
                    then have "M1⋅Γ'' + Γ' + Γ1 = Γ + Γ'" by (auto simp add:union_ac)
                    moreover from eq2 and ‹Modal M Ms = Modal F Fs› have "M2⋅Δ'' + Δ1 = Δ" 
                         using add_equal_means_equal[where Γ=" M2 ⋅ Δ'' + Δ1" and Δ=Δ and A="Modal F Fs"]
                         by (auto simp add:union_ac)
                    then have "M2⋅Δ'' + Δ' + Δ1 = Δ + Δ'" by (auto simp add:union_ac) (*>*)
  ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ+Δ',m) ∈ derivable (ext R R2 M1 M2)"
   (*<*) using ee(*>*) by metis
  }
moreover
  {assume "Modal M Ms ∈ set_mset Δ1" ― ‹Formula is in the implicit weakening›
 (*<*)  then have "Modal M Ms ∈# Δ1" by auto
  then have "∃ Δ2. Δ1 = Δ2 ⊕ Modal M Ms" using insert_DiffM[where x="Modal M Ms" and M="Δ1"]
                         apply auto apply (rule_tac x="Δ1⊖Modal M Ms" in exI) by (auto simp add:union_ac)(*>*)
  then obtain Δ2 where "Δ1 = Δ2 ⊕ Modal M Ms" by blast (*>*)
  from ba and rules 
       have "extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r ∈ (ext R R2 M1 M2)" by auto
  moreover from ba and ca have "fst (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r) = Ps"
           by (auto simp add:extendConc_def)
 (*<*)        ultimately have "(snd (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r),n'+1) ∈ derivable (ext R R2 M1 M2)"
                         using d' and derivable.step[where r="extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r"
                                                     and R="ext R R2 M1 M2" and m=n'] and ‹Ps ≠ []› by auto
                    moreover from ca and ‹r' = (ps,\<Empt> ⇒* \<LM>Modal F Fs \<RM>)› 
                         have "snd (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r) = (M1⋅Γ'' + (Γ1 + Γ') ⇒* (M2⋅Δ'' ⊕ Modal F Fs) + Δ2 + Δ')"
                         by (auto simp add:extendRule_def extendConc_def extend_def union_ac)
                    ultimately have gg: "(M1⋅Γ'' + Γ1 + Γ' ⇒* M2⋅Δ'' + Δ2 + Δ' ⊕ Modal F Fs,n'+1) ∈ derivable (ext R R2 M1 M2)"
                         by (auto simp add:union_ac)
                    from eq1 have "M1⋅Γ'' + Γ1 = Γ" by auto
                    then have "(M1⋅Γ'' + Γ1 + Γ') = Γ + Γ'" by auto
                    moreover from eq2 and ‹Δ1 = Δ2 ⊕ Modal M Ms›
                         have "M2⋅Δ'' + Δ2 ⊕ Modal F Fs ⊕ Modal M Ms = Δ ⊕ Modal M Ms" by (auto simp add:union_ac)
                    then have "M2⋅Δ'' + Δ2 ⊕ Modal F Fs = Δ" 
                         using add_equal_means_equal[where Γ=" M2 ⋅ Δ'' + Δ2 ⊕ Modal F Fs" and Δ=Δ and A="Modal M Ms"]
                         by (auto simp add:union_ac)
                    then have "M2⋅Δ'' + Δ2 + Δ' ⊕ Modal F Fs = Δ + Δ'" by (auto simp add:union_ac) (*>*) 
 ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)" (*<*)using gg(*>*)   
           
           by auto
  then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" 
           using ‹n = Suc n'› by auto
 }
ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" 
           by blast
(*<*)  }(*>*)
txt‹\noindent The other case, where the last inference was a left inference, is more straightforward, and so is omitted.›
 (*<*)
            moreover
               {assume "r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                with ba ca ‹S = (Γ1 ⇒* Δ1)› have
                     eq1: "(M1⋅Γ'' + Γ1 ⊕ Modal F Fs ⇒* M2⋅Δ'' + Δ1) = (Γ ⇒* Δ ⊕ Modal M Ms)"
                     by (auto simp add:extendRule_def extend_def extendConc_def union_ac)
                then have eq2: "M2⋅Δ'' + Δ1 = Δ ⊕ Modal M Ms" by auto
                then have "set_mset (M2 ⋅ Δ'' + Δ1) = set_mset (Δ ⊕ Modal M Ms)" by auto
                then have "set_mset (\<LM>Modal M Ms\<RM>) ⊆ set_mset (M2 ⋅ Δ'') ∪ set_mset Δ1" by auto
                then have "Modal M Ms ∈ set_mset (M2⋅Δ'') ∨ Modal M Ms ∈ set_mset Δ1"
                     by auto
                moreover
                   {assume "Modal M Ms ∈ set_mset (M2⋅Δ'')"
                    then have "Modal M Ms ∈# M2⋅Δ''" by auto
                    with modal_not_contain[where M=M and N=M2 and A=Ms and Γ=Δ''] and neq
                         have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by auto
                   }
                moreover
                   {assume "Modal M Ms ∈ set_mset Δ1"
                    then have "Modal M Ms ∈# Δ1" by auto
                    then have "∃ Δ2. Δ1 = Δ2 ⊕ Modal M Ms" using insert_DiffM[where x="Modal M Ms" and M="Δ1"]
                         apply auto apply (rule_tac x="Δ1⊖Modal M Ms" in exI) by (auto simp add:union_ac)
                    then obtain Δ2 where "Δ1 = Δ2 ⊕ Modal M Ms" by blast
                    from ba and rules have "extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r ∈ (ext R R2 M1 M2)" by auto
                    moreover from ba and ca have "fst (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r) = Ps"
                         by (auto simp add:extendConc_def)
                    ultimately have "(snd (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r),n'+1) ∈ derivable (ext R R2 M1 M2)"
                         using d' and derivable.step[where r="extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r"
                                                     and R="ext R R2 M1 M2" and m=n'] and ‹Ps ≠ []› by auto
                    moreover from ca and ‹r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)› 
                         have "snd (extendConc (Γ1 + Γ' ⇒* Δ2 + Δ') r) = ((M1⋅Γ'' ⊕ Modal F Fs)+ Γ1 + Γ' ⇒* M2⋅Δ'' + Δ2 + Δ')"
                         by (auto simp add:extendRule_def extendConc_def extend_def union_ac)
                    ultimately have gg: "(M1⋅Γ'' + Γ1 + Γ' ⊕ Modal F Fs ⇒* M2⋅Δ'' + Δ2 + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)"
                         by (auto simp add:union_ac)
                    from eq1 have "M1⋅Γ'' + Γ1 ⊕ Modal F Fs  = Γ" by auto
                    then have "(M1⋅Γ'' + Γ1 + Γ') ⊕ Modal F Fs = Γ + Γ'" by (auto simp add:union_ac)
                    moreover from eq2 and ‹Δ1 = Δ2 ⊕ Modal M Ms›
                         have "M2⋅Δ'' + Δ2 ⊕ Modal M Ms = Δ ⊕ Modal M Ms" by (auto simp add:union_ac)
                    then have "M2⋅Δ'' + Δ2 = Δ" 
                         using add_equal_means_equal[where Γ=" M2 ⋅ Δ'' + Δ2" and Δ=Δ and A="Modal M Ms"]
                         by (auto simp add:union_ac)
                    then have "M2⋅Δ'' + Δ2 + Δ'  = Δ + Δ'" by (auto simp add:union_ac)
                    ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)" using gg by (auto simp add:union_ac)
                    then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n = Suc n'›
                         by auto
                   }
                ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
               }
           ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" using cc by blast
          }   
      ultimately show "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by auto
   qed
qed
       
                     

lemma leftInvert:
fixes Γ Δ :: "('a,'b) form multiset"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ modRules2 ∧ R3 ⊆ modRules2 ∧ R = Ax ∪ R1 ∪ p_e R2 M1 M2 ∪ R3 ∧ R' = Ax ∪ R1 ∪ R2 ∪ R3"
    and   a: "(Γ ⊕ Modal M Ms ⇒* Δ,n) ∈ derivable (ext R R2 M1 M2)"
    and   b: "∀ r' ∈ R'. leftPrincipal r' (Modal M Ms) R' ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and neq: "M1 ≠ M"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
using assms
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⊕ Modal M Ms ⇒* Δ, m) ∈ derivable (ext R R2 M1 M2) ⟶
              (∀r' ∈ R'. leftPrincipal r' (Modal M Ms) R' ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable (ext R R2 M1 M2))" 
     and a': "(Γ ⊕ Modal M Ms ⇒* Δ,n) ∈ derivable (ext R R2 M1 M2)" 
     and b': "∀ r' ∈ R'. leftPrincipal r' (Modal M Ms) R' ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(Γ ⊕ Modal M Ms ⇒* Δ,0) ∈ derivable (ext R R2 M1 M2)" using a' by simp
     then have "([],Γ ⊕ Modal M Ms ⇒* Δ) ∈ (ext R R2 M1 M2)" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⊕ Modal M Ms ⇒* Δ) ∧ (r ∈ Ax)"
          using rules apply- apply (rule ext.cases [where 'a = 'a and 'b = 'b]) apply (auto simp add:extendRule_def extend_def)
          apply (rule_tac x=b in exI) apply (rule_tac x=seq in exI) apply auto apply (rule upRules.cases) apply auto
          apply (rule upRules.cases) apply auto apply (rule upRules.cases) apply auto
          apply (insert p_e_non_empty[where R=R2 and M=M1 and N=M2])
          apply (rule Ax.cases) apply auto apply (drule_tac x="[]" in meta_spec) 
          apply (drule_tac x="\<LM>At i\<RM> ⇒* \<LM>At i\<RM>" in meta_spec) apply auto
          apply (drule_tac x="[]" in meta_spec) apply (drule_tac x="\<LM>ff\<RM> ⇒* \<Empt>" in meta_spec) apply auto
          apply (drule_tac x=a in meta_spec) apply (drule_tac x=b in meta_spec) apply (auto simp add:extendConc_def)
          apply (drule_tac x="[]" in meta_spec) apply (drule_tac x=b in meta_spec) apply auto
          apply (subgoal_tac "([],b) ∈ modRules2") by (rule modRules2.cases,auto)+
     then obtain r S where "extendRule S r = ([],Γ ⊕ Modal M Ms ⇒* Δ)" and "r ∈ Ax" by auto
     then obtain i xs where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨ r = ([],\<LM>ff\<RM> ⇒* \<Empt>)" 
          using characteriseAx[where r=r] by auto
     moreover 
         {assume "r = ([],\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)"
          with ‹extendRule S r = ([],Γ ⊕ Modal M Ms ⇒* Δ)›
               have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⊕ Modal M Ms ⇒* Δ)"
               using extendRule_def[where R="([],\<LM>At i\<RM> ⇒* \<LM>At i\<RM>)" and forms=S] by auto
          then have "At i ∈# Γ ∧ At i ∈# Δ" 
               using extendID[where S=S and i=i and Γ="Γ⊕ Modal M Ms" and Δ=Δ] by auto
          then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" by auto
          then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" using rules
               and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R] by auto
         }
     moreover
         {assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
          with ‹extendRule S r = ([],Γ ⊕ Modal M Ms ⇒* Δ)›
             have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⊕ Modal M Ms ⇒* Δ)"
             using extendRule_def[where R="([],\<LM>ff\<RM> ⇒* \<Empt>)" and forms=S] by auto
          then have "ff ∈# Γ" 
               using extendFalsum[where S=S and Γ="Γ⊕Modal M Ms" and Δ=Δ] by auto
          then have "ff ∈# Γ + Γ'" by auto
          then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" using rules
               and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R] by auto
         }
     ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable (ext R R2 M1 M2)" by blast
     then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n=0› by auto
 next
     case (Suc n')
     then have "(Γ ⊕ Modal M Ms ⇒* Δ,n'+1) ∈ derivable (ext R R2 M1 M2)" using a' by simp
     then obtain Ps where "(Ps, Γ ⊕ Modal M Ms ⇒* Δ) ∈ (ext R R2 M1 M2)" and 
                          "Ps ≠ []" and 
                       d':"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)"
          using characteriseLast[where C="Γ ⊕ Modal M Ms ⇒* Δ" and m=n' and R="(ext R R2 M1 M2)"] by auto
     then have "∃ r S. (((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⊕ Modal M Ms ⇒* Δ)) ∨
                       (r ∈ p_e R2 M1 M2 ∧ extendConc S r = (Ps,Γ ⊕ Modal M Ms ⇒* Δ))) ∧ r∈R" by (cases) auto
     then obtain r S where ext: "((r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⊕ Modal M Ms ⇒* Δ))
                                ∨ (r ∈ p_e R2 M1 M2 ∧ extendConc S r = (Ps,Γ ⊕ Modal M Ms ⇒* Δ))" and "r ∈ R" by auto
     moreover
        {assume ext1: "(r ∈ Ax ∨ r ∈ upRules ∨ r ∈ modRules2) ∧ extendRule S r = (Ps, Γ ⊕ Modal M Ms ⇒* Δ)"
         with ‹Ps ≠ []› have "r ∈ upRules ∨ r ∈ modRules2" and "extendRule S r = (Ps,Γ ⊕ Modal M Ms ⇒* Δ)" 
               apply auto apply (cases r) 
               by (rule Ax.cases) (auto simp add:extendRule_def)
         moreover
            {assume "r ∈ upRules"
             then obtain ps c where "r = (ps,c)" by (cases r) auto
             with ‹r ∈ upRules› obtain T Ts where sw:"c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ 
                                                   c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                  using upRuleCharacterise[where Ps=ps and C=c] by auto
             have "(leftPrincipal r (Modal M Ms) R') ∨ ¬(leftPrincipal r (Modal M Ms) R')" by blast
             moreover
                {assume "leftPrincipal r (Modal M Ms) R'"
                 then have "c = (\<LM>Modal M Ms\<RM> ⇒* \<Empt>)" using ‹r = (ps,c)› by (cases) auto
                 with sw and ‹r ∈ upRules› and disjoint have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
                      by auto
                }
             moreover
                {assume "¬ leftPrincipal r (Modal M Ms) R'"
                 then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using IH and a' b' d' ‹Ps ≠ []›
                      and nonPrincipalInvertLeft[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and n=n
                                                  and Γ=Γ and Δ=Δ and M=M and Ms=Ms and r=r and S=S
                                                  and Γ'=Γ' and Δ'=Δ' and n'=n' and Ps=Ps and ps=ps 
                                                  and c=c and R'=R' and ?M1.0=M1 and ?M2.0=M2]
                      and ‹n = Suc n'› and ext1 and rules and ‹r = (ps,c)› and ‹r ∈ R› by auto
                }
             ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by blast
            }
         moreover
            {assume "r ∈ modRules2"
             then obtain ps c where "r = (ps,c)" by (cases r) auto
             with ‹r ∈ modRules2› obtain T Ts where sw: "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)
                                                         ∨ c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
                  using modRule2Characterise[where Ps=ps and C=c] by auto
             have "leftPrincipal r (Modal M Ms) R' ∨ ¬ leftPrincipal r (Modal M Ms) R'" by blast
             moreover
                {assume "leftPrincipal r (Modal M Ms) R'"
                 then have "(Γ' ⇒* Δ') ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R›
                      apply- apply (rule leftPrincipal.cases) by auto
                 then have ex:"extend S (Γ' ⇒* Δ') ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⊕ Modal M Ms ⇒* Δ)›
                      and ‹r = (ps,c)› by (simp add:extendContain)
                 moreover
                    {assume "c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
                     then have bb: "leftPrincipal r (Modal T Ts) R'" using ‹r = (ps,c)› and ‹r ∈ R›
                       proof-
                          from ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› and ‹r = (ps,c)› and ‹r ∈ R› and ‹r ∈ modRules2›
                          have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R" by auto
                          with rules
                          have "(ps,  \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ p_e R2 M1 M2 ∨
                                (ps,  \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R3" apply auto apply (rule Ax.cases) apply auto
                                apply (subgoal_tac "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ upRules")
                                apply auto apply (rule upRules.cases) by auto
                          moreover
                             {assume "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R3"
                              then have "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" using rules by auto
                             }
                          moreover
                             {assume "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ p_e R2 M1 M2"
                              then obtain Γ' Δ' r' 
                                   where aa: "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) = extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∧ r' ∈ R2"
                                   apply (rule p_e.cases) by auto
                              then have "r' ∈ modRules2" using rules by auto
                              then obtain F Fs where 
                                   "snd r' = (\<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ snd r' = (\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                                   using modRule2Characterise[where Ps="fst r'" and C="snd r'"] by auto
                              with aa have "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs) ∨
                                            (\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                                   by (auto simp add:extendRule_def extend_def)
                              moreover
                                 {assume "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⇒* M2⋅Δ' ⊕ Modal F Fs)"
                                  then have "\<Empt> = M2⋅Δ' ⊕ Modal F Fs" by auto
                                  then have "(ps, \<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by auto
                                 }
                              moreover
                                 {assume "(\<LM>Modal T Ts\<RM> ⇒* \<Empt>) = (M1⋅Γ' ⊕ Modal F Fs ⇒* M2⋅Δ')"
                                  then have "M2⋅Δ' = \<Empt>" and "\<LM>Modal T Ts\<RM> = M1⋅Γ' ⊕ Modal F Fs" by auto
                                  then have "M1⋅Γ' = \<Empt>" and "Modal T Ts = Modal F Fs" and "M2⋅Δ' = \<Empt>"
                                       using 
                                       singleton_add_means_equal[where A="Modal T Ts" and Γ="M1⋅Γ'" and B="Modal F Fs"]
                                       and singleton_add_means_empty[where A="Modal T Ts" and Γ="M1⋅Γ'" and B="Modal F Fs"] 
                                       by (auto simp add:modaliseMultiset_def)
                                  then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' = r'" using extendRuleEmpty[where r=r'] by auto
                                  then have "extendRule (M1⋅Γ' ⇒* M2⋅Δ') r' ∈ R2" using aa by auto
                                  then have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R2" using aa by auto
                                  then have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" using rules by simp
                                 }
                              ultimately have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by blast
                             }
                         ultimately have "(ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>) ∈ R'" by auto
                         then show ?thesis using ‹r = (ps,c)› and ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› by auto
                         qed
                     then have "Modal T Ts = Modal M Ms" using ‹leftPrincipal r (Modal M Ms) R'› apply auto
                          apply (rule leftPrincipal.cases) apply auto apply (rotate_tac 1) apply (rule leftPrincipal.cases)
                          apply auto apply (rule leftPrincipal.cases) apply auto apply (rotate_tac 1)
                          apply (rule leftPrincipal.cases) by auto
                     then have "c = (\<LM>Modal M Ms\<RM> ⇒* \<Empt>)" using ‹c = (\<LM>Modal T Ts\<RM> ⇒* \<Empt>)› by auto
                    }
                    moreover
                    {assume "c = (\<Empt> ⇒* \<LM>Modal T Ts\<RM>)"
                     then have "¬ leftPrincipal r (Modal M Ms) R'" using ‹r = (ps,c)› apply auto
                          by (rule leftPrincipal.cases) (auto simp add:extendRule_def extend_def)
                     with ‹leftPrincipal r (Modal M Ms) R'› have "c = (\<LM>Modal M Ms\<RM> ⇒* \<Empt>)" by simp
                    }
                 ultimately have "c = (\<LM>Modal M Ms\<RM> ⇒* \<Empt>)" using sw by blast
                 with ‹extendRule S r = (Ps,Γ ⊕ Modal M Ms ⇒* Δ)› have "S = (Γ ⇒* Δ)"
                      using ‹r = (ps,c)› apply (auto simp add:extendRule_def extend_def) by (cases S) auto
                 with ex have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
                 then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)"
                      using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable (ext R R2 M1 M2)› by auto
                 then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n = Suc n'›
                      by (auto,rule_tac x=m in exI) (simp)
                }
             moreover
                {assume "¬ leftPrincipal r (Modal M Ms) R'"
                 then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using IH and a' b' d' ‹Ps ≠ []›
                      and nonPrincipalInvertLeft[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and n=n
                                                  and Γ=Γ and Δ=Δ and M=M and Ms=Ms and r=r and S=S
                                                  and Γ'=Γ' and Δ'=Δ' and n'=n' and Ps=Ps and ps=ps 
                                                  and c=c and R'=R' and ?M1.0=M1 and ?M2.0=M2]
                      and ‹n = Suc n'› and ext1 and rules and ‹r = (ps,c)› and ‹r ∈ R› by auto
                }
             ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by blast
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by blast
        }
     moreover
        {assume ba: "r ∈ p_e R2 M1 M2 ∧ extendConc S r = (Ps,  Γ ⊕ Modal M Ms ⇒* Δ)"
           with rules obtain F Fs Γ'' Δ'' ps r' where
                ca: "r = extendRule (M1⋅Γ'' ⇒* M2⋅Δ'') r'" and 
                cb: "r' ∈ R2" and
                cc:  "r' = (ps, \<Empt> ⇒* \<LM>Modal F Fs\<RM>) ∨ r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                using modRule1Characterise[where Ps="fst r" and C="snd r" and M=M1 and N=M2 and R=R2] by auto
            obtain Γ1 Δ1 where "S = (Γ1 ⇒* Δ1)" by (cases S) auto
            moreover
               {assume "r' = (ps, \<Empt> ⇒* \<LM>Modal F Fs\<RM>)"
                with ba ca ‹S = (Γ1 ⇒* Δ1)› have
                     eq1: "(M1⋅Γ'' + Γ1  ⇒* M2⋅Δ'' + Δ1 ⊕ Modal F Fs) = (Γ ⊕ Modal M Ms ⇒* Δ)"
                     by (auto simp add:extendRule_def extend_def extendConc_def union_ac)
                then have eq2: "M1⋅Γ'' + Γ1 = Γ ⊕ Modal M Ms" by auto
                then have "set_mset (M1 ⋅ Γ'' + Γ1) = set_mset (Γ ⊕ Modal M Ms)" by auto
                then have "set_mset (\<LM>Modal M Ms\<RM>) ⊆ set_mset (M1 ⋅ Γ'') ∪ set_mset Γ1" by auto
                then have "Modal M Ms ∈ set_mset (M1⋅Γ'') ∨ Modal M Ms ∈ set_mset Γ1"
                     by auto
                moreover
                   {assume "Modal M Ms ∈ set_mset (M1⋅Γ'')"
                    then have "Modal M Ms ∈# M1⋅Γ''" by auto
                    with modal_not_contain[where M=M and N=M1 and A=Ms and Γ=Γ''] and neq
                         have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by auto
                   }
                moreover
                   {assume "Modal M Ms ∈ set_mset Γ1"
                    then have "Modal M Ms ∈# Γ1" by auto
                    then have "∃ Γ2. Γ1 = Γ2 ⊕ Modal M Ms" using insert_DiffM[where x="Modal M Ms" and M="Γ1"]
                         apply auto apply (rule_tac x="Γ1⊖Modal M Ms" in exI) by (auto simp add:union_ac)
                    then obtain Γ2 where "Γ1 = Γ2 ⊕ Modal M Ms" by blast
                    from ba and rules have "extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r ∈ (ext R R2 M1 M2)" by auto
                    moreover from ba and ca have "fst (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r) = Ps"
                         by (auto simp add:extendConc_def)
                    ultimately have "(snd (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r),n'+1) ∈ derivable (ext R R2 M1 M2)"
                         using d' and derivable.step[where r="extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r"
                                                     and R="ext R R2 M1 M2" and m=n'] and ‹Ps ≠ []› by auto
                    moreover from ca and ‹r' = (ps,\<Empt> ⇒* \<LM>Modal F Fs\<RM>)› 
                         have "snd (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r) = (M1⋅Γ''+ Γ2 + Γ' ⇒* (M2⋅Δ'' ⊕ Modal F Fs)+ Δ1 + Δ')"
                         by (auto simp add:extendRule_def extendConc_def extend_def union_ac)
                    ultimately have gg: "(M1⋅Γ'' + Γ2 + Γ' ⇒* M2⋅Δ'' + Δ1 + Δ' ⊕ Modal F Fs,n'+1) ∈ derivable (ext R R2 M1 M2)"
                         by (auto simp add:union_ac)
                    from eq1 have "M2⋅Δ'' + Δ1 ⊕ Modal F Fs  = Δ" by auto
                    then have "(M2⋅Δ'' + Δ1 + Δ') ⊕ Modal F Fs = Δ + Δ'" by (auto simp add:union_ac)
                    moreover from eq2 and ‹Γ1 = Γ2 ⊕ Modal M Ms›
                         have "M1⋅Γ'' + Γ2 ⊕ Modal M Ms = Γ ⊕ Modal M Ms" by (auto simp add:union_ac)
                    then have "M1⋅Γ'' + Γ2 = Γ" 
                         using add_equal_means_equal[where Γ=" M1 ⋅ Γ'' + Γ2" and Δ=Γ and A="Modal M Ms"]
                         by (auto simp add:union_ac)
                    then have "M1⋅Γ'' + Γ2 + Γ'  = Γ + Γ'" by (auto simp add:union_ac)
                    ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)" using gg by (auto simp add:union_ac)
                    then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n = Suc n'›
                         by auto
                   }
                ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
               }
            moreover
               {assume "r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)"
                with ba ca ‹S = (Γ1 ⇒* Δ1)› have
                     eq1: "(M1⋅Γ'' + Γ1 ⊕ Modal F Fs ⇒* M2⋅Δ'' + Δ1) = (Γ ⊕ Modal M Ms ⇒* Δ)"
                     by (auto simp add:extendRule_def extend_def extendConc_def union_ac)
                then have eq2: "M1⋅Γ'' + Γ1 ⊕ Modal F Fs = Γ ⊕ Modal M Ms" by auto
                then have "set_mset (M1 ⋅ Γ'' + Γ1 ⊕ Modal F Fs) = set_mset (Γ ⊕ Modal M Ms)" by auto
                then have "set_mset (\<LM>Modal M Ms\<RM>) ⊆ set_mset (M1⋅ Γ'') ∪ set_mset Γ1 ∪  {Modal F Fs}" by auto
                then have "Modal M Ms ∈ set_mset (M1⋅Γ'') ∨ Modal M Ms ∈ set_mset Γ1 ∨ Modal M Ms = Modal F Fs"
                     by auto
                moreover
                   {assume "Modal M Ms ∈ set_mset (M1⋅Γ'')"
                    then have "Modal M Ms ∈# M1⋅Γ''" by auto
                    with modal_not_contain[where M=M and N=M1 and A=Ms and Γ=Γ''] and neq
                         have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by auto
                   }
                moreover
                   {assume "Modal M Ms = Modal F Fs"
                    then have "r' = (ps, \<LM>Modal M Ms\<RM> ⇒* \<Empt>)" using ‹r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)› by simp
                    with cb and rules have "leftPrincipal r' (Modal M Ms) R'" and "r' ∈ R'" by auto
                    with b have "(Γ' ⇒* Δ') ∈ set ps" using ‹r' = (ps, \<LM>Modal M Ms\<RM> ⇒* \<Empt>)›
                         by (auto simp add:Ball_def)
                    then have "extend (M1⋅Γ'' ⇒* M2⋅Δ'') (Γ' ⇒* Δ') ∈ set (map (extend (M1⋅Γ'' ⇒* M2⋅Δ'')) ps)" by auto
                    moreover from ba and ‹r' = (ps, \<LM>Modal M Ms\<RM> ⇒* \<Empt>)› and ca
                         have "Ps = map (extend (M1⋅Γ'' ⇒* M2⋅Δ'')) ps"
                         by (auto simp add:extendRule_def extendConc_def)
                    moreover have "extend (M1⋅Γ'' ⇒* M2⋅Δ'') (Γ' ⇒* Δ') = (M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ')" 
                         by (auto simp add:extend_def) 
                    ultimately have "(M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ') ∈ set Ps" by auto
                    with d' have "∃ m≤n'. (M1⋅Γ'' + Γ' ⇒* M2⋅Δ'' + Δ',m) ∈ derivable (ext R R2 M1 M2)" by auto
                    then have "∃ m≤n'. (M1⋅Γ'' + Γ' + Γ1 ⇒* M2⋅Δ'' + Δ' + Δ1,m) ∈ derivable (ext R R2 M1 M2)"
                         using dpWeak[where Γ="M1⋅Γ'' + Γ'" and Δ="M2⋅Δ'' + Δ'" and R=R and ?R2.0=R2
                                      and M=M1 and N=M2 and ?R1.0=R1 and ?R3.0=R3 and Γ'=Γ1 and Δ'=Δ1] 
                         and rules by auto
                    with ‹n = Suc n'› 
                         have ee: "∃ m≤n. (M1⋅Γ'' + Γ' + Γ1 ⇒* M2⋅Δ'' + Δ' + Δ1,m) ∈ derivable (ext R R2 M1 M2)"
                         apply auto apply (rule_tac x=m in exI) by arith
                    from eq1 have "M2⋅Δ'' + Δ1 = Δ" by auto
                    then have "M2⋅Δ'' + Δ' + Δ1 = Δ + Δ'" by (auto simp add:union_ac)
                    moreover from eq2 and ‹Modal M Ms = Modal F Fs› have "M1⋅Γ'' + Γ1 = Γ" 
                         using add_equal_means_equal[where Γ=" M1 ⋅ Γ'' + Γ1" and Δ=Γ and A="Modal F Fs"]
                         by (auto simp add:union_ac)
                    then have "M1⋅Γ'' + Γ' + Γ1 = Γ + Γ'" by (auto simp add:union_ac)
                    ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ+Δ',m) ∈ derivable (ext R R2 M1 M2)"
                         using ee by metis
                   }
                moreover
                   {assume "Modal M Ms ∈ set_mset Γ1"
                    then have "Modal M Ms ∈# Γ1" by auto
                    then have "∃ Γ2. Γ1 = Γ2 ⊕ Modal M Ms" using insert_DiffM[where x="Modal M Ms" and M="Γ1"]
                         apply auto apply (rule_tac x="Γ1⊖Modal M Ms" in exI) by (auto simp add:union_ac)
                    then obtain Γ2 where "Γ1 = Γ2 ⊕ Modal M Ms" by blast
                    from ba and rules have "extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r ∈ (ext R R2 M1 M2)" by auto
                    moreover from ba and ca have "fst (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r) = Ps"
                         by (auto simp add:extendConc_def)
                    ultimately have "(snd (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r),n'+1) ∈ derivable (ext R R2 M1 M2)"
                         using d' and derivable.step[where r="extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r"
                                                     and R="ext R R2 M1 M2" and m=n'] and ‹Ps ≠ []› by auto
                    moreover from ca and ‹r' = (ps,\<LM>Modal F Fs\<RM> ⇒* \<Empt>)› 
                         have "snd (extendConc (Γ2 + Γ' ⇒* Δ1 + Δ') r) = ((M1⋅Γ'' ⊕ Modal F Fs )+ Γ2 + Γ' ⇒* M2⋅Δ'' + Δ1 + Δ')"
                         by (auto simp add:extendRule_def extendConc_def extend_def union_ac)
                    ultimately have gg: "(M1⋅Γ'' + Γ2 + Γ' ⊕ Modal F Fs⇒* M2⋅Δ'' + Δ1 + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)"
                         by (auto simp add:union_ac)
                    from eq1 have "M2⋅Δ'' + Δ1 = Δ" by auto
                    then have "(M2⋅Δ'' + Δ1 + Δ') = Δ + Δ'" by auto
                    moreover from eq2 and ‹Γ1 = Γ2 ⊕ Modal M Ms›
                         have "M1⋅Γ'' + Γ2 ⊕ Modal F Fs ⊕ Modal M Ms = Γ ⊕ Modal M Ms" by (auto simp add:union_ac)
                    then have "M1⋅Γ'' + Γ2 ⊕ Modal F Fs = Γ" 
                         using add_equal_means_equal[where Γ=" M1⋅Γ'' + Γ2 ⊕ Modal F Fs" and Δ=Γ and A="Modal M Ms"]
                         by (auto simp add:union_ac)
                    then have "M1⋅Γ'' + Γ2 + Γ' ⊕ Modal F Fs = Γ + Γ'" by (auto simp add:union_ac)
                    ultimately have "(Γ + Γ' ⇒* Δ + Δ',n'+1) ∈ derivable (ext R R2 M1 M2)" using gg by auto
                    then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" using ‹n = Suc n'›
                         by auto
                   }
                ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" by blast
               }
           ultimately have "∃m≤n. ( Γ + Γ' ⇒* Δ + Δ', m) ∈ derivable (ext R R2 M1 M2)" using cc by blast
           }
      ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable (ext R R2 M1 M2)" by blast
   qed
qed



datatype C = con
datatype BD = BOX (‹□›)| DIAMOND (‹◇›)

type_synonym CDBD_form = "(C,BD) form"

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

abbreviation BOX_form ( ‹□ _› [80]80) where
   "□ (p:: CDBD_form)  ≡ Modal □ [p]"

abbreviation DIAMOND_form (‹◇ _› [80]80) where
   "◇ (p :: CDBD_form) ≡ Modal ◇ [p]"

inductive_set "g3up"
where
    conL[intro]: "([\<LM> A \<RM> + \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ∧* B \<RM> ⇒* \<Empt>) ∈ g3up"
|   conR[intro]: "([\<Empt> ⇒* \<LM> A \<RM>, \<Empt> ⇒* \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ∧* B \<RM>) ∈ g3up"

(*>*)
text‹

We guarantee no other rule has the same modal operator in the succedent of a modalised context rule using the condition $M \neq M_{2}$.  Note this lemma only allows one kind of modalised context rule.  In other words, it could not be applied to a calculus with the rules:

\[
\begin{array}{ccc}
\infer[R_{1}]{\Gamma',!\cdot\Gamma \Rightarrow \bullet A,\bullet\cdot\Delta,\Delta'}{!\cdot\Gamma \Rightarrow A,\bullet\cdot\Delta} & \ \ \ &
\infer[R_{2}]{\Gamma',\bullet\cdot\Gamma \Rightarrow \bullet A,!\cdot\Delta,\Delta'}{\bullet\cdot\Gamma \Rightarrow A,!\cdot\Delta}
\end{array}
\]
since, if $([\emptyset \Rightarrow A],\emptyset \Rightarrow \bullet A) \in \mathcal{R}$, then $R_{1} \in \textrm{p-e } \mathcal{R}\ !\ \bullet$, whereas $R_{2} \in \textrm{p-e } \mathcal{R}\ \bullet\ !$.  Similarly, we cannot have modalised context rules which have more than one modalised multiset in the antecedent or succedent of the active part.  For instance:

\[
\infer{\Gamma',!\cdot\Gamma_{1},\bullet\cdot\Gamma_{2} \Rightarrow \bullet A,!\cdot\Delta_{1},\bullet\cdot\Delta_{2},\Delta'}{!\cdot\Gamma_{1},\bullet\cdot\Gamma_{2} \Rightarrow A,!\cdot\Delta_{1},\bullet\cdot\Delta_{2}}
\]
cannot belong to any \texttt{p-e} set.  It would be a simple matter to extend the definition of \texttt{p-e} to take a \textit{set} of modal operators, however this has not been done. 

As an example, classical modal logic can be formalised.
The (modal) rules for this calculus are then given in two sets, the latter of which will be extended with $\Box\cdot\Gamma \Rightarrow \Diamond\cdot\Delta$:
›
inductive_set "g3mod2" 
where
    diaR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM>], \<Empt> ⇒* \<LM> ◇ A \<RM>) ∈ g3mod2"
|   boxL(*<*)[intro](*>*): "([\<LM> A \<RM> ⇒* \<Empt>], \<LM> □ A \<RM> ⇒* \<Empt>) ∈ g3mod2"

inductive_set "g3mod1"
where
    boxR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM>A\<RM>],\<Empt> ⇒* \<LM> □ A \<RM>) ∈ g3mod1"
|   diaL(*<*)[intro](*>*): "([\<LM>A\<RM> ⇒* \<Empt>],\<LM> ◇ A \<RM> ⇒* \<Empt>) ∈ g3mod1"

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

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

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



lemmas g3 = g3up_upRules g3mod1_modRules2 g3mod2_modRules2




lemma principal_Ax:
shows "⟦ r ∈ Ax ; rightPrincipal r (□ A) R ⟧ ⟹ (\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)"
by (auto simp add:nonPrincipalID)

lemma principal_g3up:
shows "⟦ r ∈ g3up ; rightPrincipal r (□ A) R ⟧ ⟹ (\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)"
apply (subgoal_tac "r ∈ upRules") apply (auto simp add:upRules_not_right_principal_for_modal)
apply (insert g3up_upRules) by auto


lemma principal_g3mod2:
assumes "r ∈ g3mod2"
and "R = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2"
and "rightPrincipal r (□ A) R"
shows "(\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)"
proof-
 from ‹r ∈ g3mod2› have "∃ A. r = ([\<LM>A\<RM> ⇒* \<Empt>], \<LM>□ A\<RM> ⇒* \<Empt>) ∨
                              r = ([\<Empt> ⇒* \<LM>A\<RM>], \<Empt> ⇒* \<LM>◇ A\<RM>)" 
      apply (cases r) by (rule g3mod2.cases) auto
 then obtain B where  "r = ([\<LM>B\<RM> ⇒* \<Empt>], \<LM>□ B\<RM> ⇒* \<Empt>) ∨
                       r = ([\<Empt> ⇒* \<LM>B\<RM>], \<Empt> ⇒* \<LM>◇ B\<RM>)" by blast
 then have "¬ rightPrincipal r (□ A) R" using ‹R = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2›
      apply auto apply (rule rightPrincipal.cases) apply (auto simp add:extendRule_def extend_def)
      apply (rule rightPrincipal.cases) by (auto simp add:extendRule_def extend_def)
 with ‹rightPrincipal r (□ A) R› show ?thesis by auto
qed

lemma principal_g3mod1:
assumes "r ∈ g3mod1"
and "R = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2"
and "rightPrincipal r (□ A) R"
shows "(\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)"
proof-
 from ‹r ∈ g3mod1› have "∃ A. r = ([\<LM>A\<RM> ⇒* \<Empt>], \<LM>◇ A\<RM> ⇒* \<Empt>) ∨
                              r = ([\<Empt> ⇒* \<LM>A\<RM>], \<Empt> ⇒* \<LM>□ A\<RM>)" 
      apply (cases r) by (rule g3mod1.cases) auto
 then obtain B where  "r = ([\<LM>B\<RM> ⇒* \<Empt>], \<LM>◇ B\<RM> ⇒* \<Empt>) ∨
                       r = ([\<Empt> ⇒* \<LM>B\<RM>], \<Empt> ⇒* \<LM>□ B\<RM>)" by blast
 moreover
    {assume "r = ([\<LM>B\<RM> ⇒* \<Empt>], \<LM>◇ B\<RM> ⇒* \<Empt>)"
     then have "¬ rightPrincipal r (□ A) R" using ‹R = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2›
          apply auto apply (rule rightPrincipal.cases) by (auto simp add:extendRule_def extend_def)
     with ‹rightPrincipal r (□ A) R› have "(\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)" by auto
    }
 moreover
    {assume "r = ([\<Empt> ⇒* \<LM>B\<RM>], \<Empt> ⇒* \<LM>□ B\<RM>)"
     then have "rightPrincipal r (□ B) R" using ‹r ∈ g3mod1› and ‹R = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2› by auto
     with ‹rightPrincipal r (□ A) R› have "A = B" apply-
          apply (rule rightPrincipal.cases) apply auto apply (rotate_tac 1) 
          by (rule rightPrincipal.cases) auto
     with ‹r = ([\<Empt> ⇒* \<LM>B\<RM>], \<Empt> ⇒* \<LM>□ B\<RM>)› have "(\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)" by auto
    }
 ultimately show ?thesis by auto
qed  

lemma principal:
assumes "R' = Ax ∪ g3up ∪ g3mod1 ∪ g3mod2"
shows "∀ r ∈ R'. rightPrincipal r (□ A) R' ⟶ (\<Empt> ⇒* \<LM>A\<RM>) ∈ set (fst r)"
using assms apply auto
apply (insert principal_Ax)[1] apply (drule_tac x="(a,b)" in meta_spec) apply auto
apply (insert principal_g3up)[1] apply (drule_tac x="(a,b)" in meta_spec) apply auto
apply (insert principal_g3mod1)[1] apply (drule_tac x="(a,b)" in meta_spec) apply auto
apply (insert principal_g3mod2) apply (drule_tac x="(a,b)" in meta_spec) by auto
(*>*)
text‹
\noindent We then show the strong admissibility of the rule:

\[
\infer{\Gamma \Rightarrow A,\Delta}{\Gamma \Rightarrow \Box A,\Delta}
\]

›
lemma invertBoxR:
assumes "R = Ax ∪ g3up ∪ (p_e g3mod1 □ ◇) ∪ g3mod2"
and     "(Γ ⇒* Δ ⊕ (□ A),n) ∈ derivable (ext R g3mod1 □ ◇)"
shows   "∃ m≤n. (Γ ⇒* Δ ⊕ A,m) ∈ derivable (ext R g3mod1 □ ◇)"
proof-
 from assms show ?thesis
 using principal(*<*)[where R'="Ax ∪ g3up ∪ g3mod1 ∪ g3mod2" and A=A] (*>*)
 and rightInvert(*<*)[where ?R1.0="g3up" and ?R2.0="g3mod1" and ?R3.0="g3mod2" and R=R and ?M1.0=□ and ?M2.0=◇
                       and M=□ and Ms="[A]" and n=n and Γ=Γ and Δ=Δ and Γ'="\<Empt>" and Δ'="\<LM>A\<RM>"
                       and R'="Ax ∪ g3up ∪ g3mod1 ∪ g3mod2"](*>*)
 and g3 by auto
qed

text‹\noindent where \textit{principal} is the result which fulfils the principal formula conditions given in the inversion lemma, and \textit{g3} is a result about rule sets.›
(*<*) 
end
(*>*)