Theory CRA

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⇩0 ∥ c⇩1) \<iinter> (d⇩0 ∥ d⇩1) ⊑ (c⇩0 \<iinter> d⇩0) ∥ (c⇩1 \<iinter> d⇩1)" (* 50 *)
begin

lemma chaos_skip: "chaos ⊑ skip"  (* 46 *)
proof -
  have "chaos = (chaos ∥ skip) \<iinter> (skip ∥ chaos)" by simp
  then have "… ⊑ (chaos \<iinter> skip) ∥ (skip \<iinter> 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 \<iinter> ⊤ = ⊤"
by (simp add: chaos_skip conjoin_top)

lemma conj_distrib2: "c ⊑ c ∥ c ⟹ c \<iinter> (d⇩0 ∥ d⇩1) ⊑ (c \<iinter> d⇩0) ∥ (c \<iinter> d⇩1)"
proof -
  assume "c ⊑ c ∥ c"
  then have "c \<iinter> (d⇩0 ∥ d⇩1) ⊑ (c ∥ c) \<iinter> (d⇩0 ∥ d⇩1)" 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⇩0;c⇩1) \<iinter> (d⇩0;d⇩1) ⊑ (c⇩0 \<iinter> d⇩0);(c⇩1 \<iinter> d⇩1)"  (* 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;⊥ \<iinter> d ⊑ (c \<iinter> d);⊥"
   by (metis (no_types) conj_bot_left seq_nil_right sequential_interchange) 

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

lemma conj_distrib3: "c ⊑ c;c ⟹ c \<iinter> (d⇩0 ; d⇩1) ⊑ (c \<iinter> d⇩0);(c \<iinter> d⇩1)"
proof -
  assume "c ⊑ c;c"
  then have "c \<iinter> (d⇩0;d⇩1) ⊑ (c;c) \<iinter> (d⇩0;d⇩1)" by (metis conj_mono order.refl) 
  thus ?thesis by (metis sequential_interchange refine_trans) 
qed

(*
lemma iter_conj_distrib:
  assumes nil: "c ⊑ nil"
    and repeat: "c ⊑ c ; c"
  shows "c \<iinter> d⇧ω ⊑ (c \<iinter> d)⇧ω"
proof (unfold iter_def)
  def F ≡ "(λ x. c \<iinter> x)"
  def G ≡ "(λ x. nil ⊓ d;x)"
  def H ≡ "(λ x. nil ⊓ ((c \<iinter> d);x))"

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

  have "F (lfp G) ⊑ 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 ⊓ d;x) = (c \<iinter> nil) ⊓ (c \<iinter> d;x)" by (metis inf_conj_distrib conj_commute)
    also have "... ⊑ nil ⊓ (c \<iinter> d;x)" by (metis conjunction_sup inf_mono_left le_iff_sup nil)
    also have "... ⊑ nil ⊓ (c;c \<iinter> d;x)" by (metis inf_conj_distrib inf.absorb_iff2 inf_mono_right repeat)
    also have "... ⊑ nil ⊓ (c \<iinter> d);(c \<iinter> x)" by (meson inf_mono_right sequential_interchange)
    finally show "(F ∘ G) x ⊑ (H ∘ F) x" by (simp add: FG HF)
  qed

  then show "c \<iinter> lfp(λx. nil ⊓ d ; x) ⊑ lfp (λx. nil ⊓ (c \<iinter> d) ; x)" using F_def G_def H_def by simp
qed

lemma iter_conj_distrib1: "c⇧ω \<iinter> d⇧ω ⊑ (c⇧ω \<iinter> d)⇧ω"
  by (simp add: iter0 iter_conj_distrib)

lemma iter_conj_distrib2: "c⇧ω \<iinter> d⇧ω ⊑ (c \<iinter> d)⇧ω"
proof -
  have a: "c⇧ω ⊑ c" by (metis iter1)
  have b: "c⇧ω \<iinter> d⇧ω ⊑ (c⇧ω \<iinter> d)⇧ω" by (metis iter_conj_distrib1)
  have "c⇧ω \<iinter> d ⊑ 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