Quelle  CRA.thy

section ‹Concurrent Refinement Algebra \label{S:CRA}›

text ‹
 This theory brings together the three main operators:
 sequential composition,
 parallel composition and
 conjunction,
 as well as the iteration operators.
 ›

theory CRA
imports 
  Sequential
  Conjunction
  Parallel
begin

text ‹
 Locale sequential-parallel brings together the sequential and parallel
 operators and relates their identities.
 ›
locale sequential_parallel = seq_distrib + par_distrib +
  assumes nil_par_nil: "nil ∥ nil ⊑ nil" 
  and skip_nil: "skip ⊑ nil"           (* 41 *)
  and skip_skip: "skip ⊑ skip;skip"    (* 40 *)
begin

lemma nil_absorb: "nil ∥ nil = nil" using nil_par_nil skip_nil par_skip
by (metis inf.absorb_iff2 inf.orderE inf_par_distrib2)

lemma skip_absorb [simp]: "skip;skip = skip"
by (metis antisym seq_mono_right seq_nil_right skip_skip skip_nil)

end

text ‹
 Locale conjunction-parallel brings together the weak conjunction and
 parallel operators and relates their identities.
 It also introduces the interchange axiom for conjunction and parallel.
 ›

locale conjunction_parallel = conj_distrib + par_distrib + 
  assumes chaos_par_top: "⊤ ⊑ chaos ∥ ⊤"
  assumes chaos_par_chaos: "chaos ⊑ chaos ∥ chaos"     (* 47 *)
  assumes parallel_interchange: "(c₀ ∥ c₁) 🚫 (d₀ ∥ d₁) ⊑ (c₀ 🚫 d₀) ∥ (c₁ 🚫 d₁)" (* 50 *)
begin

lemma chaos_skip: "chaos ⊑ skip"  (* 46 *)
proof -
  have "chaos = (chaos ∥ skip) 🚫 (skip ∥ chaos)" by simp
  then have "… ⊑ (chaos 🚫 skip) ∥ (skip 🚫 chaos)" using parallel_interchange by blast 
  thus ?thesis by auto
qed

lemma chaos_par_chaos_eq: "chaos = chaos ∥ chaos"
  by (metis antisym chaos_par_chaos chaos_skip order_refl par_mono par_skip)

lemma nonabort_par_top: "chaos ⊑ c ==> c ∥ ⊤ = ⊤"
  by (metis chaos_par_top par_mono top.extremum_uniqueI)

lemma skip_conj_top: "skip 🚫 ⊤ = ⊤"
by (simp add: chaos_skip conjoin_top)

lemma conj_distrib2: "c ⊑ c ∥ c ==> c 🚫 (d₀ ∥ d₁) ⊑ (c 🚫 d₀) ∥ (c 🚫 d₁)"
proof -
  assume "c ⊑ c ∥ c"
  then have "c 🚫 (d₀ ∥ d₁) ⊑ (c ∥ c) 🚫 (d₀ ∥ d₁)" by (metis conj_mono order.refl) 
  thus ?thesis by (metis parallel_interchange refine_trans) 
qed

end

text ‹
 Locale conjunction-sequential brings together the weak conjunction and
 sequential operators.
 It also introduces the interchange axiom for conjunction and sequential.
 ›

locale conjunction_sequential = conj_distrib + seq_distrib + (* iteration + *)
  assumes chaos_seq_chaos: "chaos ⊑ chaos;chaos"
  assumes sequential_interchange: "(c₀;c₁) 🚫 (d₀;d₁) ⊑ (c₀ 🚫 d₀);(c₁ 🚫 d₁)"  (* 51 *)
begin

lemma chaos_nil: "chaos ⊑ nil"
  by (metis conj_chaos local.conj_commute seq_nil_left seq_nil_right
       sequential_interchange)

lemma chaos_seq_absorb: "chaos = chaos;chaos" 
proof (rule antisym)
  show "chaos ⊑ chaos;chaos" by (simp add: chaos_seq_chaos) 
next
  show "chaos;chaos ⊑ chaos" using chaos_nil
    using seq_mono_left seq_nil_left by fastforce 
qed
  
lemma seq_bot_conj: "c;⊥ 🚫 d ⊑ (c 🚫 d);⊥"
   by (metis (no_types) conj_bot_left seq_nil_right sequential_interchange) 

lemma conj_seq_bot_right [simp]: "c;⊥ 🚫 c = c;⊥"
proof (rule antisym)
  show lr: "c;⊥ 🚫 c ⊑ c;⊥" by (metis seq_bot_conj conj_idem) 
next
  show rl: "c;⊥ ⊑ c;⊥ 🚫 c" 
    by (metis conj_idem conj_mono_right seq_bot_right)
qed

lemma conj_distrib3: "c ⊑ c;c ==> c 🚫 (d₀ ; d₁) ⊑ (c 🚫 d₀);(c 🚫 d₁)"
proof -
  assume "c ⊑ c;c"
  then have "c 🚫 (d₀;d₁) ⊑ (c;c) 🚫 (d₀;d₁)" by (metis conj_mono order.refl) 
  thus ?thesis by (metis sequential_interchange refine_trans) 
qed

(*
lemma iter_conj_distrib:
  assumes nil: "c \<sqsubseteq> nil"
    and repeat: "c \<sqsubseteq> c ; c"
  shows "c \<iinter> d\<^sup>\<omega> \<sqsubseteq> (c \<iinter> d)\<^sup>\<omega>"
proof (unfold iter_def)
  def F \<equiv> "(\<lambda> x. c \<iinter> x)"
  def G \<equiv> "(\<lambda> x. nil \<sqinter> d;x)"
  def H \<equiv> "(\<lambda> x. nil \<sqinter> ((c \<iinter> d);x))"

  have FG: "F \<circ> G = (\<lambda> x. c \<iinter> (nil \<sqinter> d;x))"  by (metis comp_def F_def G_def) 
  have HF: "H \<circ> F = (\<lambda> x. (nil \<sqinter> (c \<iinter> d);(c \<iinter> x)))" by (metis comp_def H_def F_def) 

  have "F (lfp G) \<sqsubseteq> lfp H"
  proof (rule fusion_lfp_leq)
    show "mono H" by (simp add: H_def iter_step_mono)
  next
    show "dist_over_sup F" by (simp add: F_def conj_Sup_distrib)
  next
    fix x
    have "c \<iinter> (nil \<sqinter> d;x) = (c \<iinter> nil) \<sqinter> (c \<iinter> d;x)" by (metis inf_conj_distrib conj_commute)
    also have "... \<sqsubseteq> nil \<sqinter> (c \<iinter> d;x)" by (metis conjunction_sup inf_mono_left le_iff_sup nil)
    also have "... \<sqsubseteq> nil \<sqinter> (c;c \<iinter> d;x)" by (metis inf_conj_distrib inf.absorb_iff2 inf_mono_right repeat)
    also have "... \<sqsubseteq> nil \<sqinter> (c \<iinter> d);(c \<iinter> x)" by (meson inf_mono_right sequential_interchange)
    finally show "(F \<circ> G) x \<sqsubseteq> (H \<circ> F) x" by (simp add: FG HF)
  qed

  then show "c \<iinter> lfp(\<lambda>x. nil \<sqinter> d ; x) \<sqsubseteq> lfp (\<lambda>x. nil \<sqinter> (c \<iinter> d) ; x)" using F_def G_def H_def by simp
qed

lemma iter_conj_distrib1: "c\<^sup>\<omega> \<iinter> d\<^sup>\<omega> \<sqsubseteq> (c\<^sup>\<omega> \<iinter> d)\<^sup>\<omega>"
  by (simp add: iter0 iter_conj_distrib)

lemma iter_conj_distrib2: "c\<^sup>\<omega> \<iinter> d\<^sup>\<omega> \<sqsubseteq> (c \<iinter> d)\<^sup>\<omega>"
proof -
  have a: "c\<^sup>\<omega> \<sqsubseteq> c" by (metis iter1)
  have b: "c\<^sup>\<omega> \<iinter> d\<^sup>\<omega> \<sqsubseteq> (c\<^sup>\<omega> \<iinter> d)\<^sup>\<omega>" by (metis iter_conj_distrib1)
  have "c\<^sup>\<omega> \<iinter> d \<sqsubseteq> c \<iinter> d" by (metis a conj_mono order.refl) 
  thus ?thesis using a b by (metis refine_trans iter_mono) 
qed
*)

end

text ‹
 Locale cra brings together sequential, parallel and weak conjunction.
 ›

locale cra = sequential_parallel + conjunction_parallel + conjunction_sequential

end