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