Theory ModalSequents
section "Modal Sequents"
theory ModalSequents
imports "HOL-Library.Multiset"
begin
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
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:
›