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: "(c0  c1) \<iinter> (d0  d1)  (c0 \<iinter> d0)  (c1 \<iinter> d1)" (* 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> (d0  d1)  (c \<iinter> d0)  (c \<iinter> d1)"
proof -
  assume "c  c  c"
  then have "c \<iinter> (d0  d1)  (c  c) \<iinter> (d0  d1)" 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: "(c0;c1) \<iinter> (d0;d1)  (c0 \<iinter> d0);(c1 \<iinter> d1)"  (* 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> (d0 ; d1)  (c \<iinter> d0);(c \<iinter> d1)"
proof -
  assume "c  c;c"
  then have "c \<iinter> (d0;d1)  (c;c) \<iinter> (d0;d1)" 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