Theory Conjunctive_Sequential

section ‹Sequential composition for conjunctive models \label{S:conjunctive-sequential}›

theory Conjunctive_Sequential
imports Sequential
begin

text ‹
  Sequential left-distributivity is only supported by conjunctive models
  but does not apply in general. The relational model is one such example.
›

locale seq_finite_conjunctive = seq_distrib_right + 
  assumes seq_inf_distrib: "c;(d0  d1) = c;d0  c;d1"
begin

sublocale seq_distrib_left
    by (simp add: seq_distrib_left.intro seq_distrib_left_axioms.intro 
        seq_inf_distrib sequential_axioms) 
end


locale seq_infinite_conjunctive = seq_distrib_right +
  assumes seq_Inf_distrib: "D  {}  c ; D = (dD. c ; d)"
begin

sublocale seq_distrib
proof unfold_locales
  fix c::'a and d0::'a and d1::'a
  have "{d0, d1}  {}" by simp
  then have "c ; {d0, d1} = {c ; d |d. d  {d0, d1}}" using seq_Inf_distrib
  proof -
    have " ((;) c ` {d0, d1}) = {c ; a |a. a  {d0, d1}}"
      using INF_Inf by blast
    then show ?thesis
      using (c::'a::refinement_lattice) D::'a::refinement_lattice set. D  {}  c ; D = (d::'a::refinement_latticeD. c ; d) {d0::'a::refinement_lattice, d1::'a::refinement_lattice}  {} by presburger
  qed
  also have "... = c ; d0  c ; d1" by (simp only: Inf2_inf)
  finally show "c ; (d0  d1)  c ; d0  c ; d1" by simp
qed


lemma seq_INF_distrib: "X  {}  c ; (xX. d x) = (xX. c ; d x)"
proof -
  assume xne: "X  {}"
  have a: "c ; (xX. d x) = c ; (d ` X)" by auto
  also have b: "... = (d(d ` X). c ; d)" by (meson image_is_empty seq_Inf_distrib xne)
  also have c: "... = (xX. c ; d x)" by (simp add: image_comp)
  finally show ?thesis by (simp add: b image_comp)
qed

lemma seq_INF_distrib_UNIV: "c ; (x. d x) = (x. c ; d x)"
  by (simp add: seq_INF_distrib)

lemma INF_INF_seq_distrib: "Y  {}  (xX. c x) ; (yY. d y) = (xX. yY. c x ; d y)"
  by (simp add: INF_seq_distrib seq_INF_distrib)

lemma INF_INF_seq_distrib_UNIV: "(x. c x) ; (y. d y) = (x. y. c x ; d y)"
  by (simp add: INF_INF_seq_distrib)

end

end