# Theory ModalSequents

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

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

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

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

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 *)
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*)
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:›

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"

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

(* Lemma which says that if we have extended an identity rule, then the propositional variable is
contained in the extended multisets *)
lemma extendID:
assumes "extend S (\<LM> At i \<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)"

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"

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)

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)
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)
{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)
{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)
}
moreover
{assume "r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
then have "¬ leftPrincipal r (Compound M Ms) R" apply auto apply (rule leftPrincipal.cases)
}
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)
}
moreover
{assume "r = (ps,\<LM>Modal T Ts\<RM> ⇒* \<Empt>)"
then have "¬ rightPrincipal r (Compound M Ms) R" apply auto apply (rule rightPrincipal.cases)
}
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)
}
moreover
{assume "r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
then have "¬ rightPrincipal r (Modal M Ms) R" apply auto apply (rule rightPrincipal.cases)
}
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)
}
moreover
{assume "r = (ps,\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
then have "¬ leftPrincipal r (Modal M Ms) R" apply auto apply (rule leftPrincipal.cases)
}
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
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 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)›
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)›
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)"
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⋅Δ')"
then have "M1⋅Γ' = \<Empt>" and "Modal T Ts = Modal F