Theory Parallel

section ‹Parallel Operator \label{S:parallel}›

theory Parallel
imports Refinement_Lattice
begin

subsection ‹Basic parallel operator›

text ‹
  The parallel operator is associative, commutative and has unit skip
  and has as an annihilator the lattice bottom. 
›

locale skip = 
  fixes skip :: "'a::refinement_lattice"  (‹skip›) 

locale par =
  fixes par :: "'a::refinement_lattice ⇒ 'a ⇒ 'a" (infixl ‹∥› 75)
  assumes abort_par:   "⊥ ∥ c = ⊥"    (* ++ *)

locale parallel = par + skip + par: comm_monoid par skip
begin

lemmas [algebra_simps, field_simps] =
  par.assoc
  par.commute
  par.left_commute

lemmas par_assoc = par.assoc            (* 36 *)
lemmas par_commute = par.commute        (* 37 *)
lemmas par_skip = par.right_neutral     (* 38 *)
lemmas par_skip_left = par.left_neutral (* 38 + 37 *)

end


subsection ‹Distributed parallel›

text ‹
  The parallel operator distributes across arbitrary non-empty infima.
›
locale par_distrib = parallel + 
  assumes par_Inf_distrib: "D ≠ {} ⟹ c ∥ (⨅ D) = (⨅d∈D. c ∥ d)"    (* 39+ *)

begin

lemma Inf_par_distrib: "D ≠ {} ⟹ (⨅ D) ∥ c = (⨅d∈D. d ∥ c)"
  using par_Inf_distrib par_commute by simp

lemma par_INF_distrib: "X ≠ {} ⟹ c ∥ (⨅x∈X. d x) = (⨅x∈X. c ∥ d x)"
  using par_Inf_distrib by (auto simp add: image_comp)

lemma INF_par_distrib: "X ≠ {} ⟹ (⨅x∈X. d x) ∥ c = (⨅x∈X. d x ∥ c)"
  using par_INF_distrib par_commute by (metis (mono_tags, lifting) INF_cong) 

lemma INF_INF_par_distrib: 
    "X ≠ {} ⟹ Y ≠ {} ⟹ (⨅x∈X. c x) ∥ (⨅y∈Y. d y) = (⨅x∈X. ⨅y∈Y. c x ∥ d y)"
proof -
  assume nonempty_X: "X ≠ {}"
  assume nonempty_Y: "Y ≠ {}"
  have "(⨅x∈X. c x) ∥ (⨅y∈Y. d y) = (⨅x∈X. c x ∥ (⨅y∈Y. d y))"
    using INF_par_distrib by (metis nonempty_X)
  also have "… = (⨅x∈X. ⨅y∈Y. c x ∥ d y)" using par_INF_distrib by (metis nonempty_Y)
  thus ?thesis by (simp add: calculation) 
qed 

lemma inf_par_distrib: "(c⇩0 ⊓ c⇩1) ∥ d = (c⇩0 ∥ d) ⊓ (c⇩1 ∥ d)"
proof -
  have "(c⇩0 ⊓ c⇩1) ∥ d = (⨅ {c⇩0, c⇩1}) ∥ d" by simp
  also have "... = (⨅c ∈ {c⇩0, c⇩1}. c ∥ d)" using Inf_par_distrib by (meson insert_not_empty) 
  also have "... = c⇩0 ∥ d ⊓ c⇩1 ∥ d" by simp
  finally show ?thesis .
qed

lemma inf_par_distrib2: "d ∥ (c⇩0 ⊓ c⇩1) = (d ∥ c⇩0) ⊓ (d ∥ c⇩1)"
  using inf_par_distrib par_commute by auto

lemma inf_par_product: "(a ⊓ b) ∥ (c ⊓ d) = (a ∥ c) ⊓ (a ∥ d) ⊓ (b ∥ c) ⊓ (b ∥ d)"
  by (simp add: inf_commute inf_par_distrib inf_par_distrib2 inf_sup_aci(3))

lemma par_mono: "c⇩1 ⊑ d⇩1 ⟹ c⇩2 ⊑ d⇩2 ⟹ c⇩1 ∥ c⇩2 ⊑ d⇩1 ∥ d⇩2"
  by (metis inf.orderE le_inf_iff order_refl inf_par_distrib par_commute)

end
end