Theory Rely_Quotient

section ‹Rely Quotient Operator \label{S:rely-quotient}›

text ‹
  The rely quotient operator is used to generalise a Jones-style rely condition
  to a process \<^cite>‹"jon83a"›.
  It is defined in terms of the parallel operator and a process $i$
  representing interference from the environment.
›

theory Rely_Quotient
imports
  CRA
  Conjunctive_Iteration
begin

subsection ‹Basic rely quotient›

text ‹
  The rely quotient of a process $c$ and an interference process $i$
  is the most general process $d$ such that $c$ is refined by $d \parallel i$.
  The following locale introduces the definition of the 
  rely quotient $c \quotient i$ as a non-deterministic choice over 
  all processes $d$ such that $c$ is refined by $d \parallel i$. 
›

locale rely_quotient = par_distrib + conjunction_parallel
begin

definition
  rely_quotient :: "'a ⇒ 'a ⇒ 'a" (infixl "'/'/" 85)
where
  "c // i ≡ ⨅{ d. (c ⊑ d ∥ i)}"

text ‹
  Any process $c$ is implemented by itself if the interference is skip.
›
lemma quotient_identity: "c // skip = c"
proof -
  have "c // skip = ⨅{ d. (c ⊑ d ∥ skip) }" by (metis rely_quotient_def)
  then have "c // skip = ⨅{ d. (c ⊑ d)  }" by (metis (mono_tags, lifting) Collect_cong par_skip) 
  thus ?thesis by (metis Inf_greatest Inf_lower2 dual_order.antisym dual_order.refl mem_Collect_eq) 
qed

text ‹
  Provided the interference process $i$ is non-aborting (i.e. it refines chaos), 
  any process $c$ is refined by its rely quotient with $i$ in parallel with $i$.
  If interference $i$ was allowed to be aborting then, 
  because $(c \quotient \bot) \parallel \bot$ equals $\bot$,
  it does not refine $c$ in general. 
›
theorem rely_quotient: 
  assumes nonabort_i: "chaos ⊑ i"
  shows "c ⊑ (c // i) ∥ i"
proof -
  define D where "D = { d ∥ i | d. (c ⊑ d ∥ i)}"
  define C where "C = {c}"
  have "(∀d ∈ D. (∃ c ∈ C. c ⊑ d))" using D_def C_def CollectD singletonI by auto
  then have "⨅ C ⊑ (⨅ D)" by (simp add: Inf_mono) 
  then have "c ⊑ ⨅{ d ∥ i | d. (c ⊑ d ∥ i)}" by (simp add: C_def D_def) 
  also have "... = ⨅{ d ∥ i | d. d ∈ {d. (c ⊑ d ∥ i)}}" by simp
  also have "... = (⨅d ∈ {d. (c ⊑ d ∥ i)}. d ∥ i)" by (simp add: INF_Inf)
  also have "... = ⨅{ d | d. (c ⊑ d ∥ i)} ∥ i"
  proof (cases "{ d | d. (c ⊑ d ∥ i)} = {}")
    assume "{ d | d. (c ⊑ d ∥ i)} = {}"
    then show "(⨅d ∈ {d. (c ⊑ d ∥ i)}. d ∥ i) = ⨅{ d | d. (c ⊑ d ∥ i)} ∥ i"
      using nonabort_i Collect_empty_eq top_greatest
            nonabort_par_top par_commute by fastforce 
  next 
    assume a: "{ d | d. (c ⊑ d ∥ i)} ≠ {}"
    have b: "{d. (c ⊑ d ∥ i)}  ≠ {}" using a by blast 
    then have "(⨅d ∈ {d. (c ⊑ d ∥ i)}. d ∥ i) = ⨅{ d. (c ⊑ d ∥ i)} ∥ i"
      using Inf_par_distrib by simp
    then show ?thesis by auto 
  qed
  also have "... = (c // i) ∥ i" by (metis rely_quotient_def)
  finally show ?thesis .
qed

text ‹
  The following theorem represents the Galois connection between 
  the parallel operator (upper adjoint) and the rely quotient operator
  (lower adjoint). This basic relationship is used to prove the majority
  of the theorems about rely quotient.
›

theorem rely_refinement: 
  assumes nonabort_i: "chaos ⊑ i"
  shows "c // i ⊑ d ⟷ c ⊑ d ∥ i"
proof
  assume a: "c // i ⊑ d"
  have "c ⊑ (c // i) ∥ i" using rely_quotient nonabort_i by simp
  thus "c ⊑ d ∥ i" using par_mono a
    by (metis inf.absorb_iff2 inf_commute le_infI2 order_refl) 
next
  assume b: "c ⊑ d ∥ i"
  then have "⨅{ d. (c ⊑ d ∥ i)} ⊑ d" by (simp add: Inf_lower)
  thus "c // i ⊑ d" by (metis rely_quotient_def) 
qed

text ‹
  Refining the ``numerator'' in a quotient, refines the quotient.
›

lemma rely_mono:
  assumes c_refsto_d: "c ⊑ d"
  shows "(c // i) ⊑ (d // i)"
proof -
  have "⋀ f. ((d ⊑ f ∥ i) ⟹ ∃ e. (c ⊑ e ∥ i) ∧ (e ⊑ f))"
    using c_refsto_d order.trans by blast 
  then have b: "⨅{ e. (c ⊑ e ∥ i)} ⊑  ⨅{ f. (d ⊑ f ∥ i)}"
    by (metis Inf_mono mem_Collect_eq) 
  show ?thesis using rely_quotient_def b by simp
qed

text ‹
  Refining the ``denominator'' in a quotient, gives a reverse refinement 
  for the quotients. This corresponds to weaken rely condition law of
  Jones \<^cite>‹"jon83a"›, 
  i.e. assuming less about the environment.
›

lemma weaken_rely: 
  assumes i_refsto_j: "i ⊑ j"
  shows "(c // j) ⊑ (c // i)"
proof -
  have "⋀ f. ((c ⊑ f ∥ i) ⟹ ∃ e. (c ⊑ e ∥ j) ∧ (e ⊑ f))"
    using i_refsto_j order.trans
    by (metis inf.absorb_iff2 inf_le1 inf_par_distrib inf_sup_ord(2) par_commute) 
  then have b: "⨅{ e. (c ⊑ e ∥ j)} ⊑  ⨅{ f. (c ⊑ f ∥ i)}"
    by (metis Inf_mono mem_Collect_eq) 
  show ?thesis using rely_quotient_def b by simp
qed

lemma par_nonabort: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes nonabort_j: "chaos ⊑ j"
  shows "chaos ⊑ i ∥ j"
  by (meson chaos_par_chaos nonabort_i nonabort_j order_trans par_mono) 

text ‹
  Nesting rely quotients of $j$ and $i$ means the same as a single quotient
  which is the parallel composition of $i$ and $j$.
›

lemma nested_rely: 
  assumes j_nonabort: "chaos ⊑ j"
  shows "((c // j) // i) = c // (i ∥ j)"
proof (rule antisym)
  show "((c // j) // i) ⊑ c // (i ∥ j)" 
  proof -
    have "⋀ f. ((c ⊑ f ∥ i ∥ j) ⟹ ∃ e. (c ⊑ e ∥ j) ∧ (e ⊑ f ∥ i))" by blast
    then have "⨅{ d. (⨅{ e. (c ⊑ e ∥ j)} ⊑ d ∥ i)} ⊑  ⨅{ f. (c ⊑ f ∥ i ∥ j)}"
      by (simp add: Collect_mono Inf_lower Inf_superset_mono)
    thus ?thesis using local.rely_quotient_def par_assoc by auto 
  qed
next
  show "c // (i ∥ j) ⊑ ((c // j) // i) "
  proof -
    have "c ⊑ ⨅{ e. (c ⊑ e ∥ j)} ∥ j"
      using j_nonabort local.rely_quotient_def rely_quotient by auto 
    then have "⋀ d. ⨅{ e. (c ⊑ e ∥ j)} ⊑ d ∥ i  ⟹ (c ⊑ d ∥ i ∥ j)"
      by (meson j_nonabort order_trans rely_refinement)
    thus ?thesis
      by (simp add: Collect_mono Inf_superset_mono local.rely_quotient_def par_assoc) 
  qed
qed

end


subsection ‹Distributed rely quotient›

locale rely_distrib = rely_quotient + conjunction_sequential
begin

text ‹
  The following is a fundamental law for introducing a parallel composition
  of process to refine a conjunction of specifications. 
  It represents an abstract view of the parallel introduction law of Jones \<^cite>‹"jon83a"›.
›

lemma introduce_parallel: 
  assumes nonabort_i: "chaos ⊑  i"
  assumes nonabort_j: "chaos ⊑  j"
  shows "c \<iinter> d ⊑  (j \<iinter> (c // i)) ∥ (i \<iinter> (d // j))"
proof -
  have a: "c ⊑ (c // i) ∥ i" using nonabort_i nonabort_j rely_quotient by auto
  have b: "d ⊑ j ∥ (d // j)" using rely_quotient par_commute 
    by (simp add: nonabort_j) 
  have "c \<iinter> d ⊑  ((c // i) ∥ i) \<iinter> ( j ∥ (d // j))" using a b by (metis conj_mono) 
  also have interchange: "c \<iinter> d ⊑  ((c // i) \<iinter> j) ∥ ( i \<iinter> (d // j))" 
   using parallel_interchange refine_trans calculation by blast 
  show ?thesis using interchange by (simp add: local.conj_commute) 
qed

text ‹
  Rely quotients satisfy a range of distribution properties with respect
  to the other operators.
›

lemma distribute_rely_conjunction: 
  assumes nonabort_i: "chaos ⊑  i"
  shows "(c \<iinter> d) // i  ⊑  (c // i) \<iinter> (d // i)"
proof -
  have "c \<iinter> d ⊑ ((c // i) ∥ i) \<iinter> ((d // i) ∥ i)" using conj_mono rely_quotient
    by (simp add: nonabort_i) 
  then have "c \<iinter> d ⊑ ((c // i) \<iinter> (d // i)) ∥ (i \<iinter> i)"
    by (metis parallel_interchange refine_trans) 
  then have "c \<iinter> d ⊑ ((c // i) \<iinter> (d // i)) ∥ i" by (metis conj_idem) 
  thus ?thesis using rely_refinement by (simp add: nonabort_i)
qed

lemma distribute_rely_choice: 
  assumes nonabort_i: "chaos ⊑  i"
  shows "(c ⊓ d) // i  ⊑  (c // i) ⊓ (d // i)"
proof -
  have "c ⊓ d ⊑ ((c // i) ∥ i) ⊓ ((d // i) ∥ i)" 
    by (metis nonabort_i inf_mono rely_quotient) 
  then have "c ⊓ d ⊑ ((c // i) ⊓ (d // i)) ∥ i" by (metis inf_par_distrib) 
  thus ?thesis by (metis nonabort_i rely_refinement) 
qed

lemma distribute_rely_parallel1: 
  assumes nonabort_i: "chaos ⊑  i"
  assumes nonabort_j: "chaos ⊑  j"
  shows "(c ∥ d) // (i ∥ j)  ⊑  (c // i) ∥ (d // j)"
proof -
  have "(c ∥ d) ⊑ ((c // i) ∥ i) ∥ ((d // j) ∥ j)" 
    using par_mono rely_quotient nonabort_i nonabort_j by simp
  then have "(c ∥ d) ⊑ (c // i) ∥ (d // j) ∥ j ∥ i" by (metis par_assoc par_commute) 
  thus ?thesis using par_assoc par_commute rely_refinement
    by (metis nonabort_i nonabort_j par_nonabort) 
qed

lemma distribute_rely_parallel2: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes i_par_i: "i ∥ i ⊑ i"
  shows "(c ∥ d) // i  ⊑  (c // i) ∥ (d // i)"
proof -
  have "(c ∥ d) // i ⊑ ((c ∥ d) // (i ∥ i))" using assms(1) using weaken_rely
    by (simp add: i_par_i par_nonabort)
  thus ?thesis by (metis distribute_rely_parallel1 refine_trans nonabort_i) 
qed

lemma distribute_rely_sequential: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes "(∀ c. (∀ d. ((c ∥ i);(d ∥ i) ⊑ (c;d) ∥ i)))"
  shows "(c;d) // i ⊑ (c // i);(d // i)"
proof -
  have "c;d ⊑ ((c // i) ∥ i);((d // i) ∥ i)" 
    by (metis rely_quotient nonabort_i seq_mono) 
  then have "c;d ⊑ (c // i) ; (d // i) ∥ i" using assms(2) by (metis refine_trans)
  thus ?thesis by (metis rely_refinement nonabort_i) 
qed

lemma distribute_rely_sequential_event: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes nonabort_j: "chaos ⊑ j"
  assumes nonabort_e: "chaos ⊑ e"
  assumes "(∀ c. (∀ d. ((c ∥ i);e;(d ∥ j) ⊑ (c;e;d) ∥ (i;e;j))))" 
  shows "(c;e;d) // (i;e;j) ⊑ (c // i);e;(d // j)"
proof -
  have "c;e;d ⊑ ((c // i) ∥ i);e;((d // j) ∥ j)" 
    by (metis order.refl rely_quotient nonabort_i nonabort_j seq_mono) 
  then have "c;e;d ⊑ ((c // i);e;(d // j)) ∥ (i;e;j)" using assms 
    by (metis refine_trans) 
  thus ?thesis using rely_refinement nonabort_i nonabort_j nonabort_e
    by (simp add: Inf_lower local.rely_quotient_def)
qed

lemma introduce_parallel_with_rely: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes nonabort_j0: "chaos ⊑  j⇩0"
  assumes nonabort_j1: "chaos ⊑  j⇩1"
  shows "(c \<iinter> d) // i ⊑ (j⇩1 \<iinter> (c // (j⇩0 ∥ i))) ∥ (j⇩0 \<iinter> (d // (j⇩1 ∥ i)))"
proof -
  have "(c \<iinter> d) // i ⊑ (c // i) \<iinter> (d // i)" 
    by (metis distribute_rely_conjunction nonabort_i) 
  then have "(c \<iinter> d) // i ⊑ (j⇩1 \<iinter> ((c // i) // j⇩0)) ∥ (j⇩0 \<iinter> ((d // i) // j⇩1))" 
    by (metis introduce_parallel nonabort_j0 nonabort_j1 inf_assoc inf.absorb_iff1) 
  thus ?thesis by (simp add: nested_rely nonabort_i) 
qed

lemma introduce_parallel_with_rely_guarantee: 
  assumes nonabort_i: "chaos ⊑  i"
  assumes nonabort_j0: "chaos ⊑  j⇩0"
  assumes nonabort_j1: "chaos ⊑  j⇩1"
  shows "(j⇩1 ∥ j⇩0) \<iinter> (c \<iinter> d) // i ⊑ (j⇩1 \<iinter> (c // (j⇩0 ∥ i))) ∥ (j⇩0 \<iinter> (d // (j⇩1 ∥ i)))"
proof -
  have "(j⇩1 ∥ j⇩0) \<iinter> (c \<iinter> d) // i ⊑ (j⇩1 ∥ j⇩0) \<iinter> ((j⇩1 \<iinter> (c // (j⇩0 ∥ i))) ∥ (j⇩0 \<iinter> (d // (j⇩1 ∥ i))))" 
    by (metis introduce_parallel_with_rely nonabort_i nonabort_j0 nonabort_j1 
        conj_mono order.refl) 
  also have "... ⊑ (j⇩1 \<iinter> j⇩1 \<iinter> (c // (j⇩0 ∥ i))) ∥ (j⇩0 \<iinter> j⇩0 \<iinter> (d // (j⇩1 ∥ i)))" 
    by (metis conj_assoc parallel_interchange) 
  finally show ?thesis by (metis conj_idem)
qed

lemma wrap_rely_guar:
  assumes nonabort_rg: "chaos ⊑ rg" 
  and skippable: "rg ⊑ skip"
  shows "c ⊑ rg \<iinter> c // rg"
proof -
  have "c = c // skip" by (simp add: quotient_identity)
  also have "... ⊑ c // rg" by (simp add: skippable weaken_rely nonabort_rg)
  also have "... ⊑ rg \<iinter> c // rg" using conjoin_non_aborting conj_commute nonabort_rg 
    by auto
  finally show "c ⊑ rg \<iinter> c // rg" .
qed

end


locale rely_distrib_iteration = rely_distrib + iteration_finite_conjunctive

begin

lemma distribute_rely_iteration: 
  assumes nonabort_i: "chaos ⊑ i"
  assumes "(∀ c. (∀ d. ((c ∥ i);(d ∥ i) ⊑ (c;d) ∥ i)))"
  shows "(c⇧ω;d) // i ⊑ (c // i)⇧ω;(d // i)"
proof -
  have "d ⊓ c ; ((c // i)⇧ω;(d // i) ∥ i) ⊑ ((d // i) ∥ i) ⊓ ((c // i) ∥ i);((c // i)⇧ω;(d // i) ∥ i)"
    by (metis inf_mono order.refl rely_quotient nonabort_i seq_mono) 
  also have "... ⊑ ((d // i) ∥ i) ⊓ ((c // i);(c // i)⇧ω;(d // i) ∥ i )"
    using assms inf_mono_right seq_assoc by fastforce
  also have "... ⊑ ((d // i) ⊓ (c // i);(c // i)⇧ω;(d // i)) ∥ i"
    by (simp add: inf_par_distrib) 
  also have "... = ((c // i)⇧ω;(d // i)) ∥ i"
    by (metis iter_unfold inf_seq_distrib seq_nil_left)
  finally show ?thesis by (metis rely_refinement nonabort_i iter_induct) 
qed

end

end