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.  nm. (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 MN 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.  mn'. (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).  mn'. (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 "mn'" 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 " mn'. (p,m)  derivable (ext R R2 M N)" using mn' by auto
           }
           then show ?thesis by auto
           qed
     then have " p'  set (fst (extendRule (extend S (Γ' ⇒* Δ')) r)).
                 mn'. (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.  nn'. (p,n)  derivable (ext R R2 M1 M2)"
    and nonempty: "Ps  []"  
shows " mn. (Γ + Γ' ⇒* Δ + Δ',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