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;(d⇩0 ⊓ d⇩1) = c;d⇩0 ⊓ c;d⇩1"
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 = (⨅d∈D. c ; d)"
begin

sublocale seq_distrib
proof unfold_locales
  fix c::'a and d⇩0::'a and d⇩1::'a
  have "{d⇩0, d⇩1} ≠ {}" by simp
  then have "c ; ⨅{d⇩0, d⇩1} = ⨅{c ; d |d. d ∈ {d⇩0, d⇩1}}" using seq_Inf_distrib
  proof -
    have "⨅ ((;) c ` {d⇩0, d⇩1}) = ⨅{c ; a |a. a ∈ {d⇩0, d⇩1}}"
      using INF_Inf by blast
    then show ?thesis
      using ‹⋀(c::'a::refinement_lattice) D::'a::refinement_lattice set. D ≠ {} ⟹ c ; ⨅D = (⨅d::'a::refinement_lattice∈D. c ; d)› ‹{d⇩0::'a::refinement_lattice, d⇩1::'a::refinement_lattice} ≠ {}› by presburger
  qed
  also have "... = c ; d⇩0 ⊓ c ; d⇩1" by (simp only: Inf2_inf)
  finally show "c ; (d⇩0 ⊓ d⇩1) ⊑ c ; d⇩0 ⊓ c ; d⇩1" by simp
qed


lemma seq_INF_distrib: "X ≠ {} ⟹ c ; (⨅x∈X. d x) = (⨅x∈X. c ; d x)"
proof -
  assume xne: "X ≠ {}"
  have a: "c ; (⨅x∈X. 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: "... = (⨅x∈X. 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 ≠ {} ⟹ (⨅x∈X. c x) ; (⨅y∈Y. d y) = (⨅x∈X. ⨅y∈Y. 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