Theory Sequential

section ‹Sequential Operator \label{S:sequential}›


theory Sequential
imports Refinement_Lattice
begin

subsection ‹Basic sequential›

text ‹
  The sequential composition operator ``$;$'' is associative and 
  has identity nil but it is not commutative. 
  It has $\bot$ as a left annihilator.
›

locale seq =
  fixes seq :: "'a::refinement_lattice ⇒ 'a ⇒ 'a" (infixl ‹;› 90)
  assumes seq_bot [simp]: "⊥ ; c = ⊥"   (* 35 *)

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

text ‹
  The monoid axioms imply ``;'' is associative and has identity nil.
  Abort is a left annihilator of sequential composition.
›
locale sequential = seq + nil + seq: monoid seq nil
begin

declare seq.assoc [algebra_simps, field_simps]

lemmas seq_assoc = seq.assoc             (* 30 *)
lemmas seq_nil_right = seq.right_neutral (* 31 *)
lemmas seq_nil_left = seq.left_neutral   (* 32 *)

end

subsection ‹Distributed sequential›

text ‹
  Sequential composition distributes across arbitrary infima 
  from the right but only across the binary (finite) infima from the left
  and hence it is monotonic in both arguments. 
  We consider left distribution first.
  Note that Section \ref{S:conjunctive-sequential} considers the
  case in which the weak-seq-inf-distrib axiom is strengthened to
  an equality.
›

locale seq_distrib_left = sequential +
  assumes weak_seq_inf_distrib: 
    "(c::'a::refinement_lattice);(d0 ⊓ d1) ⊑ (c;d0 ⊓ c;d1)"  (* 33 *)
begin

text ‹Left distribution implies sequential composition is monotonic is its right argument›
lemma seq_mono_right: "c0 ⊑ c1 ⟹ d ; c0 ⊑ d ; c1"
  by (metis inf.absorb_iff2 le_inf_iff weak_seq_inf_distrib)

(* Nec? *)
lemma seq_bot_right [simp]: "c;⊥ ⊑ c"
   by (metis bot.extremum seq.right_neutral seq_mono_right)

end

locale seq_distrib_right = sequential +
  assumes Inf_seq_distrib: 
    "(⨅ C) ; d = (⨅(c::'a::refinement_lattice)∈C. c ; d)" (* 34 *)
begin

lemma INF_seq_distrib: "(⨅c∈C. f c) ; d = (⨅c∈C. f c ; d)"
  using Inf_seq_distrib by (auto simp add: image_comp)

lemma inf_seq_distrib: "(c0 ⊓ c1) ; d = (c0 ; d ⊓ c1 ; d)"
proof -
  have "(c0 ⊓ c1) ; d = (⨅ {c0, c1}) ; d" by simp
  also have "... = (⨅c∈{c0, c1}. c ; d)" by (fact Inf_seq_distrib)
  also have "... = (c0 ; d) ⊓ (c1 ; d)" by simp
  finally show ?thesis .
qed

lemma seq_mono_left: "c0 ⊑ c1 ⟹ c0 ; d ⊑ c1 ; d"
  by (metis inf.absorb_iff2 inf_seq_distrib)

lemma seq_top [simp]: "⊤ ; c = ⊤"
proof -
  have "⊤ ; c = (⨅a∈{}. a ; c)"
    by (metis Inf_empty Inf_seq_distrib)
  thus ?thesis
    by simp
qed

primrec seq_power :: "'a ⇒ nat ⇒ 'a" (infixr ‹;^› 80) where
    seq_power_0: "a ;^ 0 = nil"
  | seq_power_Suc: "a ;^ Suc n = a ; (a ;^ n)"

notation (latex output)
  seq_power (‹(_⇗_⇖)› [1000] 1000)

notation (HTML output)
  seq_power (‹(_⇗_⇖)› [1000] 1000)


lemma seq_power_front: "(a ;^ n) ; a = a ; (a ;^ n)"
  by (induct n, simp_all add: seq_assoc)

lemma seq_power_split_less: "i < j ⟹ (b ;^ j) = (b ;^ i) ; (b ;^ (j - i))"
proof (induct j arbitrary: i type: nat)
  case 0
  thus ?case by simp
next
  case (Suc j)
  have "b ;^ Suc j = b ; (b ;^ i) ; (b ;^ (j - i))"
    using Suc.hyps Suc.prems less_Suc_eq seq_assoc by auto
  also have "... = (b ;^ i) ; b ; (b ;^ (j - i))" by (simp add: seq_power_front)
  also have "... = (b ;^ i) ; (b ;^ (Suc j - i))"
    using Suc.prems Suc_diff_le seq_assoc by force
  finally show ?case .
qed

end

locale seq_distrib = seq_distrib_right + seq_distrib_left
begin

lemma seq_mono: "c1 ⊑ d1 ⟹ c2 ⊑ d2 ⟹ c1;c2 ⊑ d1;d2"
  using seq_mono_left seq_mono_right by (metis inf.orderE le_infI2) 

end

end