Theory Conjunction

section ‹Weak Conjunction Operator \label{S:conjunction}›

theory Conjunction
imports Refinement_Lattice
begin

text ‹
  The weak conjunction operator $\doublecap$ is similar to
  least upper bound ($\sqcup$) 
  but is abort strict,
  i.e.\ the lattice bottom is an annihilator: $c \doublecap \bot = \bot$. 
  It has identity the command chaos that allows any non-aborting behaviour.
›

locale chaos =
  fixes chaos :: "'a::refinement_lattice"    (‹chaos›) 
(*
The weak conjunction operator uses a special symbol: double intersection.
To see this symbol in your Isabelle PIDE, install DejaVu Sans fonts
(available freely online at http://dejavu-fonts.org/wiki/Download)
and add the following line to ~/.isabelle/Isabelle2015/etc/symbols
(create the file if it does not exist):

\<iinter>               code: 0x0022d2  group: operator  font: DejaVuSans

Note: if the symbol is rendering correctly, you do not need to do anything.
*)
locale conj =
  fixes conj :: "'a::refinement_lattice ⇒ 'a ⇒ 'a"   (infixl ‹\<iinter>› 80)
  assumes conj_bot_right: "c \<iinter> ⊥ = ⊥"

text ‹
  Conjunction forms an idempotent, commutative monoid
  (i.e. a semi-lattice), with identity chaos.
›

locale conjunction = conj + chaos + conj: semilattice_neutr conj chaos

begin
lemmas [algebra_simps, field_simps] =
  conj.assoc
  conj.commute
  conj.left_commute

lemmas conj_assoc = conj.assoc             (* 42 *)
lemmas conj_commute = conj.commute         (* 43 *)
lemmas conj_idem = conj.idem               (* 44 *)
lemmas conj_chaos = conj.right_neutral     (* 45 *)            
lemmas conj_chaos_left = conj.left_neutral (* 45 + 43 *)

lemma conj_bot_left [simp]: "⊥ \<iinter> c = ⊥"
using conj_bot_right local.conj_commute by fastforce

lemma conj_not_bot: "a \<iinter> b ≠ ⊥ ⟹ a ≠ ⊥ ∧ b ≠ ⊥"
  using conj_bot_right by auto

lemma conj_distrib1: "c \<iinter> (d0 \<iinter> d1) = (c \<iinter> d0) \<iinter> (c \<iinter> d1)"
  by (metis conj_assoc conj_commute conj_idem)

end



subsection ‹Distributed weak conjunction›

text ‹
  The weak conjunction operator distributes across arbitrary non-empty infima.
›

locale conj_distrib = conjunction +
  assumes Inf_conj_distrib: "D ≠ {} ⟹ (⨅ D) \<iinter> c = (⨅d∈D. d \<iinter> c)"   (* 48 *)
  (* and sup_conj_distrib: "(c0 ⊔ c1) \<iinter> d = (c0 \<iinter> d) ⊔ (c1 \<iinter> d)"  *)       (* 49+ *)
begin

lemma conj_Inf_distrib: "D ≠ {} ⟹ c \<iinter> (⨅ D) = (⨅d∈D. c \<iinter> d)"
  using Inf_conj_distrib conj_commute by auto

lemma inf_conj_distrib: "(c0 ⊓ c1) \<iinter> d = (c0 \<iinter> d) ⊓ (c1 \<iinter> d)"
proof -
  have "(c0 ⊓ c1) \<iinter> d = (⨅ {c0, c1}) \<iinter> d" by simp
  also have "... = (⨅c ∈ {c0, c1}. c \<iinter> d)" by (rule Inf_conj_distrib, simp)
  also have "... = (c0 \<iinter> d) ⊓ (c1 \<iinter> d)" by simp
  finally show ?thesis .
qed

lemma inf_conj_product: "(a ⊓ b) \<iinter> (c ⊓ d) = (a \<iinter> c) ⊓ (a \<iinter> d) ⊓ (b \<iinter> c) ⊓ (b \<iinter> d)"
  by (metis inf_conj_distrib conj_commute inf_assoc)

lemma conj_mono: "c0 ⊑ d0 ⟹ c1 ⊑ d1 ⟹ c0 \<iinter> c1 ⊑ d0 \<iinter> d1"
  by (metis inf.absorb_iff1 inf_conj_product inf_right_idem)

lemma conj_mono_left: "c0 ⊑ c1 ⟹ c0 \<iinter> d ⊑ c1 \<iinter> d"
  by (simp add: conj_mono)

lemma conj_mono_right: "c0 ⊑ c1 ⟹ d \<iinter> c0 ⊑ d \<iinter> c1"
  by (simp add: conj_mono)

lemma conj_refine: "c0 ⊑ d ⟹ c1 ⊑ d ⟹ c0 \<iinter> c1 ⊑ d" (* law 'refine-conjunction' *)
  by (metis conj_idem conj_mono)

lemma refine_to_conj: "c ⊑ d0 ⟹ c ⊑ d1 ⟹ c ⊑ d0 \<iinter> d1"
  by (metis conj_idem conj_mono)

lemma conjoin_non_aborting: "chaos ⊑ c ⟹ d ⊑ d \<iinter> c"
  by (metis conj_mono order.refl conj_chaos)

lemma conjunction_sup: "c \<iinter> d ⊑ c ⊔ d"
  by (simp add: conj_refine)

lemma conjunction_sup_nonaborting: 
  assumes "chaos ⊑ c" and "chaos ⊑ d"
  shows "c \<iinter> d = c ⊔ d"
proof (rule antisym)
  show "c ⊔ d ⊑ c \<iinter> d" using assms(1) assms(2) conjoin_non_aborting local.conj_commute by fastforce 
next
  show "c \<iinter> d ⊑ c ⊔ d" by (metis conjunction_sup)
qed

lemma conjoin_top: "chaos ⊑ c ⟹ c \<iinter> ⊤ = ⊤"
by (simp add: conjunction_sup_nonaborting)

end

end