text:
section \<open>Denotational semantics of Circus actions\<close>

theory Denotational_Semantics
imports Circus_Actions Var_list
begin

text \<open>In this section, we introduce the definitions of Circus actions denotational semantics.
We provide the proof of well-formedness of every action. We also provide proofs concerning
the monotonicity of operators over actions.\<close>

subsection \<open>Skip\<close>

definition Skip :: "('\<theta>::ev_eq,'\<sigma>) action" where
"Skip \<equiv> action_of
                  (R (true \<turnstile> \<lambda>(A, A'). tr A' = tr A \<and> \<not>wait A' \<and> more A = more A'))"

lemmas Skip_is_CSP = Skip_is_action[simplified]

lemma relation_of_Skip:
"relation_of Skip =
                  (R (true \<turnstile> \<lambda>(A, A'). tr A' = tr A \<and> \<not>wait A' \<and> more A = more A'))"
by (simp add: Skip_def action_of_inverse Skip_is_CSP)

definition CSP3::"(('\<theta>::ev_eq,'\<sigma>) alphabet_rp) Healthiness_condition"
where "CSP3 (P)  \<equiv>  relation_of Skip ;; P"

definition CSP4::"(('\<theta>::ev_eq,'\<sigma>) alphabet_rp) Healthiness_condition"
where "CSP4 (P)  \<equiv>  P ;; relation_of Skip"

lemma Skip_is_CSP3: "(relation_of Skip) is CSP3 healthy"
apply (auto simp: relation_of_Skip rp_defs design_defs fun_eq_iff CSP3_def)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
prefer 3
apply (split cond_splits, simp_all)+
apply (auto simp add: prefix_def)
done

lemma Skip_is_CSP4: "(relation_of Skip) is CSP4 healthy"
apply (auto simp: relation_of_Skip rp_defs design_defs fun_eq_iff CSP4_def)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
prefer 3
apply (split cond_splits, simp_all)+
apply (auto simp add: prefix_def)
done

lemma Skip_comp_absorb: "(relation_of Skip ;; relation_of Skip) = relation_of Skip"
apply (auto simp: relation_of_Skip fun_eq_iff rp_defs true_def design_defs)
apply (clarsimp split: cond_splits)+
apply (case_tac "ok aa", simp_all)
apply (erule disjE)+
apply (clarsimp simp: prefix_def)
apply (clarsimp simp: prefix_def)
apply (erule disjE)+
apply (clarsimp simp: prefix_def)
apply (clarsimp simp: prefix_def)
apply (erule disjE)+
apply (clarsimp simp: prefix_def)
apply (clarsimp simp: prefix_def)
apply (case_tac "ok aa", simp_all)
apply (clarsimp simp: prefix_def)
apply (clarsimp split: cond_splits)+
apply (rule_tac b=a in comp_intro)
apply (clarsimp split: cond_splits)+
apply (rule_tac b=a in comp_intro)
apply (clarsimp split: cond_splits)+
done

subsection \<open>Stop\<close>

definition Stop :: "('\<theta>::ev_eq,'\<sigma>) action"
where "Stop \<equiv> action_of (R (true \<turnstile> \<lambda>(A, A'). tr A' = tr A \<and> wait A'))"

lemma Stop_is_action:
"(R (true \<turnstile> \<lambda>(A, A'). tr A' = tr A \<and> wait A')) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
by auto

lemmas Stop_is_CSP = Stop_is_action[simplified]

lemma relation_of_Stop:
"relation_of Stop = (R (true \<turnstile> \<lambda>(A, A'). tr A' = tr A \<and> wait A'))"
by (simp add: Stop_def action_of_inverse Stop_is_CSP)

lemma Stop_is_CSP3: "(relation_of Stop) is CSP3 healthy"
apply (auto simp: relation_of_Stop relation_of_Skip rp_defs design_defs fun_eq_iff CSP3_def)
apply (rule_tac b=a in comp_intro)
apply (split cond_splits, auto)
apply (split cond_splits)+
apply (simp_all)
apply (case_tac "ok aa", simp_all)
apply (case_tac "tr aa \<le> tr ba", simp_all)
apply (case_tac "ok ba", simp_all)
apply (case_tac "tr ba \<le> tr c", simp_all)
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (split cond_splits)+
apply (simp_all add: true_def)
apply (erule disjE)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (auto simp add: prefix_def)
done

lemma Stop_is_CSP4: "(relation_of Stop) is CSP4 healthy"
apply (auto simp: relation_of_Stop relation_of_Skip rp_defs design_defs fun_eq_iff CSP4_def)
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
apply (case_tac "ok aa", simp_all)
apply (case_tac "tr aa \<le> tr ba", simp_all)
apply (case_tac "ok ba", simp_all)
apply (case_tac "tr ba \<le> tr c", simp_all)
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (split cond_splits)+
apply (simp_all add: true_def)
apply (erule disjE)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (auto simp add: prefix_def)
done

subsection \<open>Chaos\<close>

definition Chaos :: "('\<theta>::ev_eq,'\<sigma>) action"
where "Chaos \<equiv> action_of (R(false \<turnstile> true))"

lemma Chaos_is_action: "(R(false \<turnstile> true)) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
by auto

lemmas Chaos_is_CSP = Chaos_is_action[simplified]

lemma relation_of_Chaos: "relation_of Chaos = (R(false \<turnstile> true))"
by (simp add: Chaos_def action_of_inverse Chaos_is_CSP)

subsection \<open>State update actions\<close>

definition Pre ::"'\<sigma> relation  \<Rightarrow> '\<sigma> predicate"
where "Pre sc \<equiv> \<lambda>A. \<exists> A'. sc (A, A')"

definition state_update_before :: "'\<sigma> relation \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action"
where "state_update_before sc Ac = action_of(R ((\<lambda>(A, A'). (Pre sc) (more A)) \<turnstile>
                      (\<lambda>(A, A'). sc (more A, more A') & \<not>wait A' & tr A = tr A')) ;; relation_of Ac)"

lemma state_update_before_is_action:
"(R ((\<lambda>(A, A'). (Pre sc) (more A)) \<turnstile>
                               (\<lambda>(A, A').sc (more A, more A') & \<not>wait A' & tr A = tr A')) ;; relation_of Ac) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule seq_CSP)
apply (rule rd_is_CSP1)
apply (auto simp: R_idem2 Healthy_def relation_of_CSP)
done

lemmas state_update_before_is_CSP = state_update_before_is_action[simplified]

lemma relation_of_state_update_before:
"relation_of (state_update_before sc Ac) = (R ((\<lambda>(A, A'). (Pre sc) (more A)) \<turnstile>
                               (\<lambda>(A, A'). sc (more A, more A') & \<not>wait A' & tr A = tr A')) ;; relation_of Ac)"
by (simp add: state_update_before_def action_of_inverse state_update_before_is_CSP)

lemma state_update_before_is_CSP3: "relation_of (state_update_before sc Ac) is CSP3 healthy"
apply (auto simp: relation_of_state_update_before relation_of_Skip rp_defs design_defs fun_eq_iff CSP3_def)
apply (rule_tac b=aa in comp_intro)
apply (split cond_splits, auto)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro)
apply (split cond_splits, simp_all)+
apply (case_tac "ok aa", simp_all)
apply (case_tac "tr aa \<le> tr ab", simp_all)
apply (case_tac "ok ab", simp_all)
apply (case_tac "tr ab \<le> tr bb", simp_all)
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (rule_tac b=bb in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule disjI1)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (rule_tac b=bb in comp_intro)
apply (split cond_splits, simp_all)+
apply (simp_all add: true_def)
apply (erule disjE)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zs@zsa" in exI, simp)
apply (auto simp add: prefix_def)
done

lemma state_update_before_is_CSP4:
  assumes A : "relation_of Ac is CSP4 healthy"
  shows "relation_of (state_update_before sc Ac) is CSP4 healthy"
apply (auto simp: relation_of_state_update_before relation_of_Skip rp_defs design_defs fun_eq_iff CSP4_def)
apply (rule_tac b=c in comp_intro)
apply (rule_tac b=ba in comp_intro, simp_all)
apply (split cond_splits, simp_all)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (subst A[simplified design_defs rp_defs CSP4_def relation_of_Skip])
apply (auto simp: rp_defs)
done

definition state_update_after :: "'\<sigma> relation \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action"
where "state_update_after sc Ac = action_of(relation_of Ac ;; R (true \<turnstile> (\<lambda>(A, A'). sc (more A, more A') & \<not>wait A' & tr A = tr A')))"

lemma state_update_after_is_action:
"(relation_of Ac ;; R (true \<turnstile> (\<lambda>(A, A'). sc (more A, more A') & \<not>wait A' & tr A = tr A'))) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule seq_CSP)
apply (auto simp: relation_of_CSP[simplified is_CSP_process_def])
apply (rule rd_is_CSP, auto)
done

lemmas state_update_after_is_CSP = state_update_after_is_action[simplified]

lemma relation_of_state_update_after:
"relation_of (state_update_after sc Ac) = (relation_of Ac ;; R (true \<turnstile> (\<lambda>(A, A'). sc (more A, more A') & \<not>wait A' & tr A = tr A')))"
by (simp add: state_update_after_def action_of_inverse state_update_after_is_CSP)

lemma mono_state_update_after: "mono (state_update_after sc)"
by (auto simp: mono_def less_eq_action ref_def relation_of_state_update_after design_defs rp_defs fun_eq_iff
            split: cond_splits dest: relation_of_spec_f_f[simplified]
                                     relation_of_spec_t_f[simplified])

lemma state_update_after_is_CSP3:
  assumes A : "relation_of Ac is CSP3 healthy"
  shows "relation_of (state_update_after sc Ac) is CSP3 healthy"
apply (auto simp: relation_of_state_update_after relation_of_Skip rp_defs design_defs fun_eq_iff CSP3_def)
apply (rule_tac b=aa in comp_intro)
apply (split cond_splits, auto)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (subst A[simplified design_defs rp_defs CSP3_def relation_of_Skip])
apply (auto simp: rp_defs)
done

lemma state_update_after_is_CSP4: "relation_of (state_update_after sc Ac) is CSP4 healthy"
apply (auto simp: relation_of_state_update_after relation_of_Skip rp_defs design_defs fun_eq_iff CSP4_def)
apply (rule_tac b=c in comp_intro)
apply (rule_tac b=ba in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (case_tac "ok bb", simp_all)
apply (case_tac "tr bb \<le> tr c", simp_all)
apply (case_tac "ok ca", simp_all)
apply (case_tac "tr ca \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE)+
apply (erule_tac x="zs@zsa" in allE, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all add: true_def)+
apply (case_tac "ok ca", simp_all)
apply (case_tac "tr ca \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zsa@zs" in exI, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (case_tac "tr bb \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (erule_tac x="zsa@zs" in allE, simp)
apply (auto simp add: prefix_def)
done

subsection \<open>Sequential composition\<close>

definition
Seq::"('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action" (infixl "`;`" 24)
where "P `;` Q \<equiv> action_of (relation_of P ;; relation_of Q)"

lemma Seq_is_action: "(relation_of P ;; relation_of Q) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule seq_CSP[OF relation_of_CSP[THEN CSP_is_CSP1] relation_of_CSP[THEN CSP_is_R] relation_of_CSP])
done

lemmas Seq_is_CSP = Seq_is_action[simplified]

lemma relation_of_Seq: "relation_of (P `;` Q) = (relation_of P ;; relation_of Q)"
by (simp add: Seq_def action_of_inverse Seq_is_CSP)

lemma mono_Seq: "mono ((`;`) P)"
  by (auto simp: mono_def less_eq_action ref_def relation_of_Seq)

lemma CSP3_imp_left_Skip:
  assumes A: "relation_of P is CSP3 healthy"
  shows "(Skip `;` P) = P"
apply (subst relation_of_inject[symmetric])
apply (simp add: relation_of_Seq A[simplified design_defs CSP3_def, symmetric])
done

lemma CSP4_imp_right_Skip:
  assumes A: "relation_of P is CSP4 healthy"
  shows "(P `;` Skip) = P"
apply (subst relation_of_inject[symmetric])
apply (simp add: relation_of_Seq A[simplified design_defs CSP4_def, symmetric])
done

lemma Seq_assoc: "(A `;` (B `;` C)) = ((A `;` B) `;` C)"
by (auto simp: relation_of_inject[symmetric] fun_eq_iff relation_of_Seq rp_defs design_defs)

lemma Skip_absorb: "(Skip `;` Skip) = Skip"
by (auto simp: Skip_comp_absorb relation_of_inject[symmetric] relation_of_Seq)

subsection \<open>Internal choice\<close>

definition
Ndet::"('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action" (infixl "\<sqinter>" 18)
where "P \<sqinter> Q \<equiv> action_of ((relation_of P) \<or> (relation_of Q))"

lemma Ndet_is_action: "((relation_of P) \<or> (relation_of Q)) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule disj_CSP)
apply (simp_all add: relation_of_CSP)
done

lemmas Ndet_is_CSP = Ndet_is_action[simplified]

lemma relation_of_Ndet: "relation_of (P \<sqinter> Q) = ((relation_of P) \<or> (relation_of Q))"
by (simp add: Ndet_def action_of_inverse Ndet_is_CSP)

lemma mono_Ndet: "mono ((\<sqinter>) P)"
by (auto simp: mono_def less_eq_action ref_def relation_of_Ndet)

subsection \<open>External choice\<close>

definition
Det::"('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action" (infixl "\<box>" 18)
where "P \<box> Q \<equiv> action_of(R((\<not>((relation_of P)\<^sup>f\<^sub>f) \<and> \<not>((relation_of Q)\<^sup>f\<^sub>f)) \<turnstile>
                                             (((relation_of P)\<^sup>t\<^sub>f \<and> ((relation_of Q)\<^sup>t\<^sub>f))
                                                \<triangleleft> \<lambda>(A, A'). tr A = tr A' \<and> wait A' \<triangleright>
                                              ((relation_of P)\<^sup>t\<^sub>f \<or> ((relation_of Q)\<^sup>t\<^sub>f)))))"

lemma Det_is_action:
"(R((\<not>((relation_of P)\<^sup>f\<^sub>f) \<and> \<not>((relation_of Q)\<^sup>f\<^sub>f)) \<turnstile>
           (((relation_of P)\<^sup>t\<^sub>f \<and> ((relation_of Q)\<^sup>t\<^sub>f))
              \<triangleleft> \<lambda>(A, A'). tr A = tr A' \<and> wait A' \<triangleright>
            ((relation_of P)\<^sup>t\<^sub>f \<or> ((relation_of Q)\<^sup>t\<^sub>f))))) \<in> {p. is_CSP_process p}"
apply (simp add: spec_def)
apply (rule rd_is_CSP)
apply (auto)
done

lemmas Det_is_CSP = Det_is_action[simplified]

lemma relation_of_Det:
"relation_of (P \<box> Q) = (R((\<not>((relation_of P)\<^sup>f\<^sub>f) \<and> \<not>((relation_of Q)\<^sup>f\<^sub>f)) \<turnstile>
                                          (((relation_of P)\<^sup>t\<^sub>f \<and> ((relation_of Q)\<^sup>t\<^sub>f))
                                             \<triangleleft> \<lambda>(A, A'). tr A = tr A' \<and> wait A' \<triangleright>
                                           ((relation_of P)\<^sup>t\<^sub>f \<or> ((relation_of Q)\<^sup>t\<^sub>f)))))"
apply (unfold Det_def)
apply (rule action_of_inverse)
apply (rule Det_is_action)
done

lemma mono_Det: "mono ((\<box>) P)"
by (auto simp: mono_def less_eq_action ref_def relation_of_Det design_defs rp_defs fun_eq_iff
            split: cond_splits dest: relation_of_spec_f_f[simplified]
                                     relation_of_spec_t_f[simplified])

subsection \<open>Reactive design assignment\<close>

definition
"rd_assign s = action_of (R (true \<turnstile> \<lambda>(A, A'). ref A' = ref A \<and> tr A' = tr A \<and> \<not>wait A' \<and> more A' = s))"

lemmas rd_assign_is_CSP = rd_assign_is_action[simplified]

lemma relation_of_rd_assign:
"relation_of (rd_assign s) =
                  (R (true \<turnstile> \<lambda>(A, A'). ref A' = ref A \<and> tr A' = tr A \<and> \<not>wait A' \<and> more A' = s))"
by (simp add: rd_assign_def  action_of_inverse rd_assign_is_CSP)

subsection \<open>Local state external choice\<close>

definition
Loc::"'\<sigma> \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow> '\<sigma> \<Rightarrow> ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action"
                                        ("'(()loc _ \<bullet> _ ') \<boxplus> '(()loc _ \<bullet> _ ')")
where "(loc s1 \<bullet> P) \<boxplus> (loc s2 \<bullet> Q) \<equiv>
                   ((rd_assign s1)`;`P) \<box> ((rd_assign s2)`;` Q)"

subsection \<open>Schema expression\<close>

definition Schema :: "'\<sigma> relation \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action" where
"Schema sc \<equiv> action_of(R ((\<lambda>(A, A'). (Pre sc) (more A)) \<turnstile>
                           (\<lambda>(A, A'). sc (more A, more A') \<and> \<not>wait A' \<and> tr A = tr A')))"

lemmas Schema_is_CSP = Schema_is_action[simplified]

lemma relation_of_Schema:
"relation_of (Schema sc) = (R ((\<lambda>(A, A'). (Pre sc) (more A)) \<turnstile>
                          (\<lambda>(A, A'). sc (more A, more A') \<and> \<not>wait A' \<and> tr A = tr A')))"
by (simp add: Schema_def action_of_inverse Schema_is_CSP)

lemma Schema_is_state_update_before: "Schema u = state_update_before u Skip"
apply (subst relation_of_inject[symmetric])
apply (auto simp: relation_of_Schema relation_of_state_update_before relation_of_Skip rp_defs fun_eq_iff
                  design_defs)
apply (split cond_splits, simp_all)
apply (rule comp_intro)
apply (split cond_splits, simp_all)+
apply (rule comp_intro)
apply (split cond_splits, simp_all)+
prefer 3
apply (split cond_splits, simp_all)+
apply (auto simp: prefix_def)
done

subsection \<open>Parallel composition\<close>

type_synonym '\<sigma> local_state = "('\<sigma> \<times> ('\<sigma>  \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>))"

fun MergeSt :: "'\<sigma> local_state \<Rightarrow> '\<sigma> local_state \<Rightarrow> ('\<theta>,'\<sigma>) relation_rp" where
"MergeSt (s1,s1') (s2,s2') = ((\<lambda>(S, S'). (s1' s1) (more S) = more S');;
                            (\<lambda>(S::('\<theta>,'\<sigma>) alphabet_rp, S'). (s2' s2) (more S) = more S'))"

definition listCons ::"'\<theta> \<Rightarrow> '\<theta> list list \<Rightarrow> '\<theta> list list" ("_ ## _") where
"a ## l = ((map (Cons a)) l)"

fun ParMergel :: "'\<theta>::ev_eq list \<Rightarrow> '\<theta> list \<Rightarrow> '\<theta> set \<Rightarrow> '\<theta> list list" where
    "ParMergel [] [] cs = [[]]"
  | "ParMergel [] (b#tr2) cs = (if (filter_chan_set b cs) then [[]]
                                          else (b ## (ParMergel [] tr2 cs)))"
  | "ParMergel (a#tr1) [] cs = (if (filter_chan_set a cs) then [[]]
                                          else (a ## (ParMergel tr1 [] cs)))"
  | "ParMergel (a#tr1) (b#tr2) cs =
           (if (filter_chan_set a cs)
                   then (if (ev_eq a b)
                              then (a ## (ParMergel tr1 tr2 cs))
                               else (if (filter_chan_set b cs)
                                        then [[]]
                                         else (b ## (ParMergel (a#tr1) tr2 cs))))
                     else (if (filter_chan_set b cs)
                               then (a ## (ParMergel tr1 (b#tr2) cs))
                                 else (a ## (ParMergel tr1 (b#tr2) cs))
                                            @ (b ## (ParMergel (a#tr1) tr2 cs))))"

definition ParMerge::"'\<theta>::ev_eq list \<Rightarrow> '\<theta> list \<Rightarrow> '\<theta> set \<Rightarrow> '\<theta> list set" where
"ParMerge tr1 tr2 cs = set (ParMergel tr1 tr2 cs)"

lemma set_Cons1: "tr1 \<in> set l \<Longrightarrow> a # tr1 \<in> (#) a ` set l"
by (auto)

lemma tr_in_set_eq: "(tr1 \<in> (#) b ` set l) = (tr1 \<noteq> [] \<and> hd tr1 = b \<and> tl tr1 \<in> set l)"
by (induct l) auto

definition M_par::"(('\<theta>::ev_eq), '\<sigma>) alpha_rp_scheme \<Rightarrow> ('\<sigma>  \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>)
                            \<Rightarrow> ('\<theta>, '\<sigma>) alpha_rp_scheme \<Rightarrow> ('\<sigma> \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>)
                                \<Rightarrow> ('\<theta> set) \<Rightarrow> ('\<theta>, '\<sigma>) relation_rp" where
"M_par s1 x1 s2 x2 cs =
((\<lambda>(S, S'). ((diff_tr S' S) \<in> ParMerge (diff_tr s1 S) (diff_tr s2 S) cs &
     ev_eq (tr_filter (tr s1) cs) (tr_filter (tr s2) cs))) \<and>
   ((\<lambda>(S, S'). (wait s1 \<or> wait s2) \<and>
                             ref S' \<subseteq> ((((ref s1)\<union>(ref s2))\<inter>cs)\<union>(((ref s1)\<inter>(ref s2))-cs)))
   \<triangleleft> wait o snd \<triangleright>
   ((\<lambda>(S, S'). (\<not>wait s1 \<or> \<not>wait s2)) \<and> MergeSt ((more s1), x1) ((more s2), x2))))"

definition  Par::"('\<theta>::ev_eq,'\<sigma>) action \<Rightarrow>
                    ('\<sigma>  \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>) \<Rightarrow> '\<theta> set \<Rightarrow> ('\<sigma>  \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>) \<Rightarrow>
                    ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action" ("_ \<lbrakk> _ | _ | _ \<rbrakk> _") where
"A1 \<lbrakk> ns1 | cs | ns2 \<rbrakk> A2 \<equiv> (action_of (R ((\<lambda> (S, S').
 \<not> (\<exists> tr1 tr2. ((relation_of A1)\<^sup>f\<^sub>f ;; (\<lambda> (S, S'). tr1 = (tr S))) (S, S')
 \<and> (spec False (wait S) (relation_of A2) ;; (\<lambda> (S, _). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs))) \<and>
 \<not> (\<exists> tr1 tr2. (spec False (wait S) (relation_of A1);;(\<lambda>(S, _). tr1 = tr S)) (S, S')
 \<and> ((relation_of A2)\<^sup>f\<^sub>f ;; (\<lambda>(S, S'). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) \<turnstile>
   (\<lambda> (S, S'). (\<exists> s1 s2. ((\<lambda> (A, A'). (relation_of A1)\<^sup>t\<^sub>f (A, s1)
 \<and> ((relation_of A2)\<^sup>t\<^sub>f (A, s2)));; M_par s1 ns1 s2 ns2 cs) (S, S'))))))"

lemma Par_is_action: "(R ((\<lambda> (S, S').
 \<not> (\<exists> tr1 tr2. ((relation_of A1)\<^sup>f\<^sub>f ;; (\<lambda> (S, S'). tr1 = (tr S))) (S, S')
 \<and> (spec False (wait S) (relation_of A2) ;; (\<lambda> (S, S'). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs))) \<and>
 \<not> (\<exists> tr1 tr2. (spec False (wait S) (relation_of A1);;(\<lambda>(S, _). tr1 = tr S)) (S, S')
 \<and> ((relation_of A2)\<^sup>f\<^sub>f ;; (\<lambda> (S, S'). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) \<turnstile>
   (\<lambda> (S, S'). (\<exists> s1 s2. ((\<lambda> (A, A'). (relation_of A1)\<^sup>t\<^sub>f (A, s1)
 \<and> ((relation_of A2)\<^sup>t\<^sub>f (A, s2)));; M_par s1 ns1 s2 ns2 cs) (S, S'))))) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
apply (blast)
done

lemmas Par_is_CSP = Par_is_action[simplified]

lemma relation_of_Par:
"relation_of (A1 \<lbrakk> ns1 | cs | ns2 \<rbrakk> A2) = (R ((\<lambda> (S, S').
 \<not> (\<exists> tr1 tr2. ((relation_of A1)\<^sup>f\<^sub>f ;; (\<lambda> (S, S'). tr1 = (tr S))) (S, S')
 \<and> (spec False (wait S) (relation_of A2) ;; (\<lambda> (S, S'). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs))) \<and>
 \<not> (\<exists> tr1 tr2. (spec False (wait S) (relation_of A1);;(\<lambda>(S, _). tr1 = tr S)) (S, S')
 \<and> ((relation_of A2)\<^sup>f\<^sub>f ;; (\<lambda> (S, S'). tr2 = (tr S))) (S, S')
 \<and> ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) \<turnstile>
   (\<lambda> (S, S'). (\<exists> s1 s2. ((\<lambda> (A, A'). (relation_of A1)\<^sup>t\<^sub>f (A, s1)
 \<and> ((relation_of A2)\<^sup>t\<^sub>f (A, s2)));; M_par s1 ns1 s2 ns2 cs) (S, S')))))"
apply (unfold Par_def)
apply (rule action_of_inverse)
apply (rule Par_is_action)
done

lemma mono_Par: "mono (\<lambda>Q. P \<lbrakk> ns1 | cs | ns2 \<rbrakk> Q)"
  apply (auto simp: mono_def less_eq_action ref_def relation_of_Par design_defs fun_eq_iff rp_defs
              split: cond_splits)
  apply (auto simp: rp_defs dest: relation_of_spec_f_f[simplified] relation_of_spec_t_f[simplified])
  apply (erule_tac x="tr ba" in allE, auto)
  apply (erule notE)
  apply (auto dest: relation_of_spec_f_f relation_of_spec_t_f)
done

subsection \<open>Local parallel block\<close>

definition
ParLoc::"'\<sigma> \<Rightarrow> ('\<sigma> \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>) \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> '\<theta> set \<Rightarrow> '\<sigma> \<Rightarrow> ('\<sigma> \<Rightarrow> '\<sigma> \<Rightarrow> '\<sigma>) \<Rightarrow> ('\<theta>,'\<sigma>) action \<Rightarrow> ('\<theta>,'\<sigma>) action"
                                        ("'(()par _ | _ \<bullet> _ ') \<lbrakk> _ \<rbrakk> '(()par _ | _ \<bullet> _ ')")
where
"(par s1 | ns1 \<bullet> P) \<lbrakk> cs \<rbrakk> (par s2 | ns2 \<bullet> Q) \<equiv> ((rd_assign s1)`;`P) \<lbrakk> ns1 | cs | ns2 \<rbrakk> ((rd_assign s2)`;` Q)"

subsection \<open>Assignment\<close>

definition ASSIGN::"('v, '\<sigma>) var_list \<Rightarrow> ('\<sigma> \<Rightarrow> 'v) \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action" where
"ASSIGN x e \<equiv> action_of (R (true \<turnstile> (\<lambda> (S, S'). tr S' = tr S \<and> \<not>wait S' \<and>
                                 (more S' = (update x (\<lambda>_. (e (more S)))) (more S)))))"

syntax "_assign"::"id \<Rightarrow> ('\<sigma> \<Rightarrow> 'v) \<Rightarrow> ('\<theta>, '\<sigma>) action"  ("_ `:=` _")
translations "y `:=` vv" => "CONST ASSIGN (VAR y) vv"

lemma Assign_is_action:
"(R (true \<turnstile> (\<lambda> (S, S'). tr S' = tr S \<and> \<not>wait S' \<and>
                (more S' = (update x (\<lambda>_. (e (more S)))) (more S))))) \<in> {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
apply (blast)
done

lemmas Assign_is_CSP = Assign_is_action[simplified]

lemma relation_of_Assign:
"relation_of (ASSIGN x e) = (R (true \<turnstile> (\<lambda> (S, S'). tr S' = tr S \<and> \<not>wait S' \<and>
                                   (more S' = (update x (\<lambda>_. (e (more S)))) (more S)))))"
by (simp add: ASSIGN_def action_of_inverse Assign_is_CSP)

lemma Assign_is_state_update_before: "ASSIGN x e = state_update_before (\<lambda> (s, s') . s' = (update x (\<lambda>_. (e s))) s) Skip"
apply (subst relation_of_inject[symmetric])
apply (auto simp: relation_of_Assign relation_of_state_update_before relation_of_Skip rp_defs fun_eq_iff
                  Pre_def update_def design_defs)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=b in comp_intro)
apply (split cond_splits, simp_all)+
defer
apply (split cond_splits, simp_all)+
prefer 3
apply (split cond_splits, simp_all)+
apply (auto simp add: prefix_def)
done

subsection \<open>Variable scope\<close>

definition Var::"('v, '\<sigma>) var_list \<Rightarrow>('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action" where
"Var v A \<equiv> action_of(
     (R(true \<turnstile> (\<lambda> (A, A'). \<exists> a. tr A' = tr A \<and> \<not>wait A' \<and> more A' = (increase v a (more A)))));;
     (relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A)))))))"

syntax "_var"::"idt \<Rightarrow> ('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" ("var _ \<bullet> _" [1000] 999)
translations "var y \<bullet> Act" => "CONST Var (VAR_LIST y) Act"

lemma Var_is_action:
"((R(true \<turnstile> (\<lambda> (A, A'). \<exists> a. tr A' = tr A \<and> \<not>wait A' \<and> more A' = (increase v a (more A)))));;
     (relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A))))))) \<in> {p. is_CSP_process p}"
  apply (simp)
  apply (rule seq_CSP)
  prefer 3
  apply (rule seq_CSP)
  apply (auto simp: relation_of_CSP1 relation_of_R)
  apply (rule rd_is_CSP)
  apply (auto simp: csp_defs rp_defs design_defs fun_eq_iff prefix_def increase_def decrease_def
               split: cond_splits)
done

lemmas Var_is_CSP = Var_is_action[simplified]

lemma relation_of_Var:
"relation_of (Var v A) =
    ((R(true \<turnstile> (\<lambda> (A, A'). \<exists> a. tr A' = tr A \<and> \<not>wait A' \<and> more A' = (increase v a (more A)))));;
     (relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A)))))))"
apply (simp only: Var_def)
apply (rule action_of_inverse)
apply (rule Var_is_action)
done

lemma mono_Var : "mono (Var x)"
  by (auto simp: mono_def less_eq_action ref_def relation_of_Var)

definition Let::"('v, '\<sigma>) var_list \<Rightarrow>('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>::ev_eq,'\<sigma>) action" where
"Let v A \<equiv> action_of((relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A)))))))"

syntax "_let"::"idt \<Rightarrow> ('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" ("let _ \<bullet> _" [1000] 999)
translations "let y \<bullet> Act" => "CONST Let (VAR_LIST y) Act"

lemma Let_is_action:
"(relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A)))))) \<in> {p. is_CSP_process p}"
  apply (simp)
  apply (rule seq_CSP)
  apply (auto simp: relation_of_CSP1 relation_of_R)
  apply (rule rd_is_CSP)
  apply (auto)
done

lemmas Let_is_CSP = Let_is_action[simplified]

lemma relation_of_Let:
"relation_of (Let v A) =
    (relation_of A;;
     (R(true \<turnstile> (\<lambda> (A, A').  tr A' = tr A \<and> \<not>wait A' \<and> more A' = (decrease v (more A))))))"
by (simp add: Let_def action_of_inverse Let_is_CSP)

lemma mono_Let : "mono (Let x)"
  by (auto simp: mono_def less_eq_action ref_def relation_of_Let)

lemma Var_is_state_update_before: "Var v A = state_update_before (\<lambda> (s, s'). \<exists> a. s' = increase v a s) (Let v A)"
apply (subst relation_of_inject[symmetric])
apply (auto simp: relation_of_Var relation_of_Let relation_of_state_update_before relation_of_Skip fun_eq_iff)
apply (auto simp: rp_defs fun_eq_iff Pre_def design_defs)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+ defer
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+ defer
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (case_tac "\<exists>A' a. A' = increase v a (alpha_rp.more aa)", simp_all add: true_def)
apply (erule_tac x="increase v a (alpha_rp.more aa)" in allE)
apply (erule_tac x="a" in allE, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (rule_tac b=ab in comp_intro)
apply (split cond_splits, simp_all)+
apply (case_tac "\<exists>A' a. A' = increase v a (alpha_rp.more aa)", simp_all add: true_def)
apply (erule_tac x="increase v a (alpha_rp.more aa)" in allE)
apply (erule_tac x="a" in allE, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
done

lemma Let_is_state_update_after: "Let v A = state_update_after (\<lambda> (s, s'). s' = decrease v s) A"
apply (subst relation_of_inject[symmetric])
apply (auto simp: relation_of_Var relation_of_Let relation_of_state_update_after relation_of_Skip fun_eq_iff)
apply (auto simp: rp_defs fun_eq_iff Pre_def design_defs)
apply (auto split: cond_splits)
done

subsection \<open>Guarded action\<close>

definition Guard::"'\<sigma> predicate \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" ("_ `&` _")
where "g `&` P \<equiv> action_of(R (((g o more o fst) \<longrightarrow> \<not> ((relation_of P)\<^sup>f\<^sub>f)) \<turnstile>
                             (((g o more o fst) \<and> ((relation_of P)\<^sup>t\<^sub>f)) \<or>
                         ((\<not>(g o more o fst)) \<and> (\<lambda> (A, A'). tr A' = tr A \<and> wait A')))))"

lemma Guard_is_action:
"(R ( ((g o more o fst) \<longrightarrow> \<not> ((relation_of P)\<^sup>f\<^sub>f)) \<turnstile>
                (((g o more o fst) \<and> ((relation_of P)\<^sup>t\<^sub>f)) \<or>
                 ((\<not>(g o more o fst)) \<and> (\<lambda> (A, A'). tr A' = tr A \<and> wait A'))))) \<in> {p. is_CSP_process p}"
  by (auto simp add: spec_def intro: rd_is_CSP)

lemmas Guard_is_CSP = Guard_is_action[simplified]

lemma relation_of_Guard:
"relation_of (g `&` P) = (R (((g o more o fst) \<longrightarrow>  \<not> ((relation_of P)\<^sup>f\<^sub>f)) \<turnstile>
                             (((g o more o fst) \<and> ((relation_of P)\<^sup>t\<^sub>f)) \<or>
                          ((\<not>(g o more o fst)) \<and> (\<lambda> (A, A'). tr A' = tr A \<and> wait A')))))"
  apply (unfold Guard_def)
  apply (subst action_of_inverse)
  apply (simp_all only: Guard_is_action)
done

lemma mono_Guard : "mono (Guard g)"
  apply (auto simp: mono_def less_eq_action ref_def rp_defs design_defs relation_of_Guard
                split: cond_splits)
  apply (auto dest: relation_of_spec_f_f relation_of_spec_t_f)
done

lemma false_Guard: "false `&` P = Stop"
apply (subst relation_of_inject[symmetric])
apply (subst relation_of_Stop)
apply (subst relation_of_Guard)
apply (simp add: fun_eq_iff utp_defs csp_defs design_defs rp_defs)
done

lemma false_Guard1: "\<And> a b. g (alpha_rp.more a) = False \<Longrightarrow>
                                (relation_of (g `&` P)) (a, b) = (relation_of Stop) (a, b)"
apply (subst relation_of_Guard)
apply (subst relation_of_Stop)
apply (auto simp: fun_eq_iff csp_defs design_defs rp_defs split: cond_splits)
done

lemma true_Guard: "true `&` P = P"
apply (subst relation_of_inject[symmetric])
apply (subst relation_of_Guard)
apply (subst CSP_is_rd[OF relation_of_CSP]) back back
apply (simp add: fun_eq_iff utp_defs csp_defs design_defs rp_defs)
done

lemma true_Guard1: "\<And> a b. g (alpha_rp.more a) = True \<Longrightarrow>
                                     (relation_of (g `&` P)) (a, b) = (relation_of P) (a, b)"
apply (subst relation_of_Guard)
apply (subst CSP_is_rd[OF relation_of_CSP]) back back
apply (auto simp: fun_eq_iff csp_defs design_defs rp_defs split: cond_splits)
done

lemma Guard_is_state_update_before: "g `&` P = state_update_before (\<lambda> (s, s') . g s) P"
apply (subst relation_of_inject[symmetric])
apply (auto simp: relation_of_Guard relation_of_state_update_before relation_of_Skip rp_defs fun_eq_iff
                  Pre_def update_def design_defs)
apply (rule_tac b=a in comp_intro)
apply (split cond_splits, simp_all)+
apply (subst CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+
apply (auto)
apply (subst (asm) CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+
apply (subst (asm) CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+
apply (subst CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+
apply (subst CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+
apply (auto) defer
apply (split cond_splits, simp_all)+
apply (subst (asm) CSP_is_rd)
apply (simp_all add: relation_of_CSP rp_defs design_defs fun_eq_iff)
apply (split cond_splits, simp_all)+ defer
apply (rule disjI1) defer
apply (case_tac "g (alpha_rp.more aa)", simp_all)
apply (rule)+
apply (simp add: impl_def) defer
oops

subsection \<open>Prefixed action\<close>

definition do where
"do e \<equiv> (\<lambda>(A, A'). tr A = tr A' \<and> (e (more A)) \<notin> (ref A')) \<triangleleft> wait o snd \<triangleright>
         (\<lambda>(A, A'). tr A' = (tr A @[(e (more A))]))"

definition do_I::"('\<sigma> \<Rightarrow>'\<theta>) \<Rightarrow> '\<theta> set \<Rightarrow> ('\<theta>, '\<sigma>) relation_rp"
where "do_I c S \<equiv>  ((\<lambda>(A, A'). tr A = tr A' & S \<inter> (ref A') = {})
                                \<triangleleft> wait o snd \<triangleright>
  (\<lambda>(A, A'). hd (tr A' - tr A) \<in> S & (c (more A) = (last (tr A')))))"

(*
definition do_I::"('v \<Rightarrow> '\<theta>) \<Rightarrow> ('v, '\<sigma>) var_list \<Rightarrow> 'v set \<Rightarrow> ('\<theta>, '\<sigma>) relation_rp"
where "do_I c x P \<equiv>  ((\<lambda>(A, A'). tr A = tr A' \<and> (c`P) \<inter> (ref A') = {})
                                \<triangleleft> wait o fst \<triangleright>
  (\<lambda>(A, A'). hd (tr A' - tr A) \<in> (c`P) \<and> (c (select x (more A)) = (last (tr A')))))"
*)

definition
iPrefix::"('\<sigma> \<Rightarrow>'\<theta>::ev_eq) \<Rightarrow> ('\<sigma> relation) \<Rightarrow> (('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action) \<Rightarrow> ('\<sigma> \<Rightarrow> '\<theta> set) \<Rightarrow> ('\<theta>, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" where
"iPrefix c i j S P \<equiv> action_of(R(true \<turnstile> (\<lambda> (A, A'). (do_I c (S (more A))) (A, A') & more A' = more A)))`;` P"

definition
oPrefix::"('\<sigma> \<Rightarrow>'\<theta>) \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" where
"oPrefix c P \<equiv> action_of(R(true \<turnstile> (do c) \<and> (\<lambda> (A, A'). more A' = more A)))`;` P"

definition Prefix0::"'\<theta> \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action" where
"Prefix0 c P \<equiv> action_of(R(true \<turnstile> (do (\<lambda> _. c)) \<and> (\<lambda> (A, A'). more A' = more A)))`;` P"

definition
read::"('v \<Rightarrow> '\<theta>) \<Rightarrow> ('v, '\<sigma>) var_list \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action"
where  "read c x P  \<equiv> iPrefix (\<lambda> A. c (select x A)) (\<lambda> (s, s'). \<exists> a. s' = increase x a s) (Let x) (\<lambda>_. range c) P"

definition
read1::"('v \<Rightarrow> '\<theta>) \<Rightarrow> ('v, '\<sigma>) var_list \<Rightarrow> ('\<sigma> \<Rightarrow> 'v set) \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action"
where  "read1 c x S P  \<equiv> iPrefix (\<lambda> A. c (select x A)) (\<lambda> (s, s'). \<exists> a. a\<in>(S s) & s' = increase x a s) (Let x) (\<lambda>s. c`(S s)) P"

definition
write1::"('v \<Rightarrow> '\<theta>) \<Rightarrow> ('\<sigma> \<Rightarrow> 'v) \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action"
where "write1 c a P \<equiv> oPrefix (\<lambda> A. c (a A)) P"

definition
write0::"'\<theta> \<Rightarrow> ('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> ('\<theta>, '\<sigma>) action"
where "write0 c P \<equiv> Prefix0 c P"

syntax
"_read"  ::"[id, pttrn, ('\<theta>, '\<sigma>) action] => ('\<theta>, '\<sigma>) action" ("(_`?`_ /\<rightarrow> _)")
"_readS" ::"[id, pttrn, '\<theta> set,('\<theta>, '\<sigma>) action] => ('\<theta>, '\<sigma>) action" ("(_`?`_`:`_ /\<rightarrow> _)")
"_readSS" ::"[id, pttrn, '\<sigma> => '\<theta> set,('\<theta>, '\<sigma>) action] => ('\<theta>, '\<sigma>) action" ("(_`?`_`\<in>`_ /\<rightarrow> _)")
"_write" ::"[id, '\<sigma>, ('\<theta>, '\<sigma>) action] => ('\<theta>, '\<sigma>) action" ("(_`!`_ /\<rightarrow> _)")
"_writeS"::"['\<theta>, ('\<theta>, '\<sigma>) action] => ('\<theta>, '\<sigma>) action" ("(_ /\<rightarrow> _)")

translations
"_read c p P"    == "CONST read c (VAR_LIST p) P"
"_readS c p b P" == "CONST read1 c (VAR_LIST p) (\<lambda>_. b) P"
"_readSS c p b P" == "CONST read1 c (VAR_LIST p) b P"
"_write c p P"   == "CONST write1 c p P"
"_writeS a P"    == "CONST write0 a P"

lemma Prefix_is_action:
"(R(true \<turnstile> (do c) \<and> (\<lambda> (A, A'). more A' = more A))) \<in> {p. is_CSP_process p}"
by (auto intro: rd_is_CSP)

lemma Prefix1_is_action:
"(R(true \<turnstile> \<lambda>(A, A'). do_I c (S (alpha_rp.more A)) (A, A') \<and> alpha_rp.more A' = alpha_rp.more A)) \<in> {p. is_CSP_process p}"
by (auto intro: rd_is_CSP)

lemma Prefix0_is_action:
"(R(true \<turnstile> (do c) \<and> (\<lambda> (A, A'). more A' = more A))) \<in> {p. is_CSP_process p}"
by (auto intro: rd_is_CSP)

lemmas Prefix_is_CSP = Prefix_is_action[simplified]

lemmas Prefix1_is_CSP = Prefix1_is_action[simplified]

lemmas Prefix0_is_CSP = Prefix0_is_action[simplified]

lemma relation_of_iPrefix:
"relation_of (iPrefix c i j S P) =
((R(true \<turnstile> (\<lambda> (A, A'). (do_I c (S (more A))) (A, A') & more A' = more A)));; relation_of P)"
by (simp add: iPrefix_def relation_of_Seq action_of_inverse Prefix1_is_CSP)

lemma relation_of_oPrefix:
"relation_of (oPrefix c P) =
((R(true \<turnstile> (do c) \<and> (\<lambda> (A, A'). more A' = more A)));; relation_of P)"
by (simp add: oPrefix_def relation_of_Seq action_of_inverse Prefix_is_CSP)

lemma relation_of_Prefix0:
"relation_of (Prefix0 c P) =
((R(true \<turnstile> (do (\<lambda> _. c)) \<and> (\<lambda> (A, A'). more A' = more A)));; relation_of P)"
by (simp add: Prefix0_def relation_of_Seq action_of_inverse Prefix0_is_CSP)

lemma mono_iPrefix : "mono (iPrefix c i j s)"
by (auto simp: mono_def less_eq_action ref_def relation_of_iPrefix)

lemma mono_oPrefix : "mono (oPrefix c)"
by (auto simp: mono_def less_eq_action ref_def relation_of_oPrefix)

lemma mono_Prefix0 : "mono(Prefix0 c)"
by (auto simp: mono_def less_eq_action ref_def relation_of_Prefix0)

subsection \<open>Hiding\<close>

definition Hide::"('\<theta>::ev_eq, '\<sigma>) action \<Rightarrow> '\<theta> set \<Rightarrow> ('\<theta>, '\<sigma>) action" (infixl "\\" 18) where
"P \\ cs \<equiv> action_of(R(\<lambda>(S, S'). \<exists> s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) &
             (relation_of P)(S, S'\<lparr>tr := s, ref := (ref S') \<union> cs \<rparr>));; (relation_of Skip))"

definition
"hid P cs == (R(\<lambda>(S, S'). \<exists> s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) & (relation_of P)(S, S'\<lparr>tr := s, ref := (ref S') \<union> cs \<rparr>)) ;; (relation_of Skip))"

lemma hid_is_R: "hid P cs is R healthy"
apply (simp add: hid_def)
apply (rule seq_R)
apply (simp add: Healthy_def R_idem2)
apply (rule CSP_is_R)
apply (rule relation_of_CSP)
done

lemma hid_Skip: "hid P cs = (hid P cs ;; relation_of Skip)"
by (simp add: hid_def comp_assoc[symmetric] Skip_comp_absorb)

lemma hid_is_CSP1: "hid P cs is CSP1 healthy"
apply (auto simp: design_defs CSP1_def hid_def rp_defs fun_eq_iff)
apply (rule_tac b="a" in comp_intro)
apply (clarsimp split: cond_splits)
apply (subst CSP_is_rd, auto simp: rp_defs relation_of_CSP design_defs fun_eq_iff split: cond_splits)
apply (auto simp: diff_tr_def relation_of_Skip rp_defs design_defs true_def split: cond_splits)
apply (rule_tac x="[]" in exI, auto)
done

lemma hid_is_CSP2: "hid P cs is CSP2 healthy"
apply (simp add: hid_def)
apply (rule seq_CSP2)
apply (rule CSP_is_CSP2)
apply (rule relation_of_CSP)
done

lemma hid_is_CSP: "is_CSP_process (hid P cs)"
by (auto simp: csp_defs hid_is_CSP1 hid_is_R hid_is_CSP2)

lemma Hide_is_action:
"(R(\<lambda>(S, S'). \<exists> s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) &
   (relation_of P)(S, S'\<lparr>tr := s, ref := (ref S') \<union> cs \<rparr>));; (relation_of Skip)) \<in> {p. is_CSP_process p}"
by (simp add: hid_is_CSP[simplified hid_def])

lemmas Hide_is_CSP = Hide_is_action[simplified]

lemma relation_of_Hide:
"relation_of (P \\ cs) = (R(\<lambda>(S, S'). \<exists> s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs)
        & (relation_of P)(S, S'\<lparr>tr :=s, ref := (ref S') \<union> cs \<rparr>));; (relation_of Skip))"
  by (simp add: Hide_def action_of_inverse Hide_is_CSP)

lemma mono_Hide : "mono(\<lambda> P. P \\ cs)"
by (auto simp: mono_def less_eq_action ref_def prefix_def utp_defs relation_of_Hide rp_defs)

subsection \<open>Recursion\<close>

text \<open>To represent the recursion operator "\<open>\<mu>\<close>" over actions, we use the
universal least fix-point operator "@{const lfp}" defined in the HOL library for lattices.
The operator "@{const lfp}" is inherited from the "Complete Lattice class" under some conditions.
All theorems defined over this operator can be reused.\<close>

text \<open>In the @{theory Circus.Circus_Actions} theory, we presented the proof that Circus actions
form a complete lattice. The Knaster-Tarski Theorem (in its simplest formulation) states
that any monotone function on a complete lattice has a least fixed-point.
This is a consequence of the basic boundary properties of the complete lattice operations.
Instantiating the complete lattice class allows one to inherit these properties with the
definition of the least fixed-point for monotonic functions over Circus actions.
\<close>

syntax "_MU"::"[idt, idt \<Rightarrow> ('\<theta>, '\<sigma>) action] \<Rightarrow> ('\<theta>, '\<sigma>) action"  ("\<mu> _ \<bullet> _")
translations "_MU X P" == "CONST lfp (\<lambda> X. P)"

(*<*)
text\<open>Instead fo the following:\<close>
lemma is_action_REP_Mu:
  shows "is_CSP_process (relation_of (lfp P))"
oops

text\<open>... we refer to the proof of @{thm Sup_is_action} and its
analogue who capture the essence of this proof at the level of the
type instantiation.\<close>

text\<open>Monotonicity: STATUS: probably critical.  Does not seem to be necessary for
parameterless Circus.\<close>
lemma mono_Mu:
  assumes A : "mono P"
  and     B : "\<And> X. mono (P X)"
  shows  "mono (lfp P)"
apply (subst lfp_unfold)
apply (auto simp: A B)
done

term Nat.Suc
(*>*)
end


text:
(*  Title:      Jinja/J/Conform.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

section \<open>Conformance Relations for Type Soundness Proofs\<close>

theory Conform
imports Exceptions
begin

definition conf :: "'m prog \<Rightarrow> heap \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"   ("_,_ \<turnstile> _ :\<le> _"  [51,51,51,51] 50)
where
  "P,h \<turnstile> v :\<le> T  \<equiv>
  \<exists>T'. typeof\<^bsub>h\<^esub> v = Some T' \<and> P \<turnstile> T' \<le> T"

definition oconf :: "'m prog \<Rightarrow> heap \<Rightarrow> obj \<Rightarrow> bool"   ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
where
  "P,h \<turnstile> obj \<surd>  \<equiv>
  let (C,fs) = obj in \<forall>F D T. P \<turnstile> C has F:T in D \<longrightarrow>
  (\<exists>v. fs(F,D) = Some v \<and> P,h \<turnstile> v :\<le> T)"

definition hconf :: "'m prog \<Rightarrow> heap \<Rightarrow> bool"  ("_ \<turnstile> _ \<surd>" [51,51] 50)
where
  "P \<turnstile> h \<surd>  \<equiv>
  (\<forall>a obj. h a = Some obj \<longrightarrow> P,h \<turnstile> obj \<surd>) \<and> preallocated h"

definition lconf :: "'m prog \<Rightarrow> heap \<Rightarrow> (vname \<rightharpoonup> val) \<Rightarrow> (vname \<rightharpoonup> ty) \<Rightarrow> bool"   ("_,_ \<turnstile> _ '(:\<le>') _" [51,51,51,51] 50)
where
  "P,h \<turnstile> l (:\<le>) E  \<equiv>
  \<forall>V v. l V = Some v \<longrightarrow> (\<exists>T. E V = Some T \<and> P,h \<turnstile> v :\<le> T)"

abbreviation
  confs :: "'m prog \<Rightarrow> heap \<Rightarrow> val list \<Rightarrow> ty list \<Rightarrow> bool"
             ("_,_ \<turnstile> _ [:\<le>] _" [51,51,51,51] 50) where
  "P,h \<turnstile> vs [:\<le>] Ts \<equiv> list_all2 (conf P h) vs Ts"

subsection\<open>Value conformance \<open>:\<le>\<close>\<close>

lemma conf_Null [simp]: "P,h \<turnstile> Null :\<le> T  =  P \<turnstile> NT \<le> T"
(*<*)by (simp (no_asm) add: conf_def)(*>*)

lemma typeof_conf[simp]: "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
(*<*)by (induct v) (auto simp: conf_def)(*>*)

lemma typeof_lit_conf[simp]: "typeof v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
(*<*)by (rule typeof_conf[OF typeof_lit_typeof])(*>*)

lemma defval_conf[simp]: "P,h \<turnstile> default_val T :\<le> T"
(*<*)by (cases T) (auto simp: conf_def)(*>*)

lemma conf_upd_obj: "h a = Some(C,fs) \<Longrightarrow> (P,h(a\<mapsto>(C,fs')) \<turnstile> x :\<le> T) = (P,h \<turnstile> x :\<le> T)"
(*<*)by (rule val.induct) (auto simp:conf_def fun_upd_apply)(*>*)

lemma conf_widen: "P,h \<turnstile> v :\<le> T \<Longrightarrow> P \<turnstile> T \<le> T' \<Longrightarrow> P,h \<turnstile> v :\<le> T'"
(*<*)by (induct v) (auto intro: widen_trans simp: conf_def)(*>*)

lemma conf_hext: "h \<unlhd> h' \<Longrightarrow> P,h \<turnstile> v :\<le> T \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
(*<*)by (induct v) (auto dest: hext_objD simp: conf_def)(*>*)

lemma conf_ClassD: "P,h \<turnstile> v :\<le> Class C \<Longrightarrow>
  v = Null \<or> (\<exists>a obj T. v = Addr a \<and>  h a = Some obj \<and> obj_ty obj = T \<and>  P \<turnstile> T \<le> Class C)"
(*<*)by(induct v) (auto simp: conf_def)(*>*)

lemma conf_NT [iff]: "P,h \<turnstile> v :\<le> NT = (v = Null)"
(*<*)by (auto simp add: conf_def)(*>*)

lemma non_npD: "\<lbrakk> v \<noteq> Null; P,h \<turnstile> v :\<le> Class C \<rbrakk>
  \<Longrightarrow> \<exists>a C' fs. v = Addr a \<and> h a = Some(C',fs) \<and> P \<turnstile> C' \<preceq>\<^sup>* C"
(*<*)by (auto dest: conf_ClassD)(*>*)

subsection\<open>Value list conformance \<open>[:\<le>]\<close>\<close>

lemma confs_widens [trans]: "\<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> P,h \<turnstile> vs [:\<le>] Ts'"
(*<*)by(auto intro: list_all2_trans conf_widen)(*>*)

lemma confs_rev: "P,h \<turnstile> rev s [:\<le>] t = (P,h \<turnstile> s [:\<le>] rev t)"
(*<*)by (simp add: list_all2_rev1)(*>*)

lemma confs_conv_map:
  "\<And>Ts'. P,h \<turnstile> vs [:\<le>] Ts' = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')"
(*<*)
proof(induct vs)
  case (Cons a vs)
  then show ?case by(case_tac Ts') (auto simp add:conf_def)
qed simp
(*>*)

lemma confs_hext: "P,h \<turnstile> vs [:\<le>] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts"
(*<*)by (erule list_all2_mono, erule conf_hext, assumption)(*>*)

lemma confs_Cons2: "P,h \<turnstile> xs [:\<le>] y#ys = (\<exists>z zs. xs = z#zs \<and> P,h \<turnstile> z :\<le> y \<and> P,h \<turnstile> zs [:\<le>] ys)"
(*<*)by (rule list_all2_Cons2)(*>*)

subsection "Object conformance"

lemma oconf_hext: "P,h \<turnstile> obj \<surd> \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> obj \<surd>"
(*<*)by (fastforce elim:conf_hext simp: oconf_def)(*>*)

lemma oconf_init_fields:
 "P \<turnstile> C has_fields FDTs \<Longrightarrow> P,h \<turnstile> (C, init_fields FDTs) \<surd>"
by(fastforce simp add: has_field_def oconf_def init_fields_def map_of_map
            dest: has_fields_fun)

lemma oconf_fupd [intro?]:
  "\<lbrakk> P \<turnstile> C has F:T in D; P,h \<turnstile> v :\<le> T; P,h \<turnstile> (C,fs) \<surd> \<rbrakk>
  \<Longrightarrow> P,h \<turnstile> (C, fs((F,D)\<mapsto>v)) \<surd>"
(*<*)by (auto dest: has_fields_fun simp add: oconf_def has_field_def fun_upd_apply)(*>*)

(*<*)
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
(*>*)

subsection "Heap conformance"

lemma hconfD: "\<lbrakk> P \<turnstile> h \<surd>; h a = Some obj \<rbrakk> \<Longrightarrow> P,h \<turnstile> obj \<surd>"
(*<*)by (unfold hconf_def) fast(*>*)

lemma hconf_new: "\<lbrakk> P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>obj) \<surd>"
(*<*)by (unfold hconf_def) (auto intro: oconf_new preallocated_new)(*>*)

lemma hconf_upd_obj: "\<lbrakk> P \<turnstile> h\<surd>; h a = Some(C,fs); P,h \<turnstile> (C,fs')\<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>(C,fs'))\<surd>"
(*<*)by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)(*>*)

subsection "Local variable conformance"

lemma lconf_hext: "\<lbrakk> P,h \<turnstile> l (:\<le>) E; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>) E"
(*<*)by (unfold lconf_def) (fast elim: conf_hext)(*>*)

lemma lconf_upd:
  "\<lbrakk> P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T; E V = Some T \<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E"
(*<*)by (unfold lconf_def) auto(*>*)

lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>) E"
(*<*)by(simp add:lconf_def)(*>*)

lemma lconf_upd2: "\<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E(V\<mapsto>T)"
(*<*)by(simp add:lconf_def)(*>*)

end

author: isabelle-prover

repo: mirror-afp-devel


text:
theory javabip_1
  imports Main "/Volumes/Setup/Isabelle/Isabelle-Code/Jan21-Isab/trinhlibs"
begin
(*---- JavaBIP encoding ----*)
(*
(\<not>P(t,l) \<or> (Q(el1, el1) \<and> \<not>Q(el1,h))) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)
\<equiv> [\<not>P(t,l) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)] \<or> [Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)]
*)
value "(\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l \<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t) l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)"

value "((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)) \<or>
(((\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)))"
(*[\<not>P(t,l) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)]*)
value "((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))"

(*\<not>P(t,l) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)
\<equiv> \<not>P(t,l) \<and> \<not>Q(k,h1) *)
lemma rutgon_1:"
((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))
\<Longrightarrow> ((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))
"
  by simp

(*[Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)]*)
value "((\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))"

(*[Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1)]*)
value "((\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1))"

(*[Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1) \<and> \<not>Q(k,h1)]
\<equiv> [Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1)]
*)
lemma rutgon_2:"((\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)) \<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))
\<Longrightarrow>((\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)) \<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)) "
  by simp

(*check after 2 shortened*)
lemma sau2rg: "((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l \<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t) l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))
\<Longrightarrow> ((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)
\<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)) \<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1))"
  by blast

(*JavaBIP \<equiv> [\<not>P(t,l) \<and> \<not>Q(k,h1)] \<or> [Q(el1, el1) \<and> \<not>Q(el1,h) \<and> \<not>P(t,l1)]*)
value "((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)
\<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1))"

lemma trans_javaBIP: "((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l \<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1)) \<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h)))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t) l1)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1))
\<Longrightarrow> (((\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)
\<or> (\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)))"
  by blast

(*JavaBIP - ve 1*)
value "(\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j.\<forall>t \<in> set u. \<forall>l \<in> set (snd t). \<not>P (fst t) l)
\<and> (\<forall>i \<in> set t_TrigInstance_1. \<forall>v \<in> set i. \<forall>k \<in> set v. \<exists>h \<in> set (snd k).\<forall>h1 \<in> set (snd k) - {h}. \<not> Q (fst k) h1)"

(*JavaBIP - ve 2*)
value "(\<exists>bet \<in> set t_betaSet_1. (\<forall>elm \<in> set bet.\<exists>el1 \<in> set elm. Q (fst el1) (snd el1))
\<and> (\<forall>elm \<in> set bet.\<forall>el1 \<in> set elm.\<forall>h \<in> set (lookup_3 (fst el1) t_TrigInstance_1) - {snd el1}. \<not>Q (fst el1) h))
\<and> (\<forall>j \<in> set t_SyncInstance_1. \<forall>u \<in> set j. \<forall>t \<in> set u. \<exists>l \<in> set (snd t).\<forall>l1 \<in> set (snd t) - {l}. \<not> P (fst t)  l1)"
end

author: TrinhLK

repo: Isabelle-Code


(*
 * Copyright 2022, Proofcraft Pty Ltd
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory ArchAInvsPre
imports AInvsPre
begin

unbundle l4v_word_context

context Arch begin

global_naming AARCH64

lemma ucast_ucast_mask_low: "(ucast (x && mask asid_low_bits) :: asid_low_index) = ucast x"
  by (rule ucast_mask_drop, simp add: asid_low_bits_def)

lemma ptes_of_idx:
  "\<lbrakk> ptes_of s (level_type level) (pt_slot_offset level pt_ptr p) = Some pte;
     pts_of s pt_ptr = Some pt; pt_type pt = level_type level; pspace_aligned s \<rbrakk> \<Longrightarrow>
   \<exists>idx. pt_apply pt idx = pte"
  apply (drule_tac pt_ptr=pt_ptr in pspace_aligned_pts_ofD, simp)
  apply (fastforce simp: level_pte_of_def in_omonad)
  done

lemma pte_info_not_InvalidPTE:
  "pte_info level pte = Some (b, a, attr, r) \<Longrightarrow> pte \<noteq> InvalidPTE"
  by (simp add: pte_info_def split: pte.splits)

lemma get_vspace_of_thread_reachable:
  "\<lbrakk> get_vspace_of_thread (kheap s) (arch_state s) t \<noteq> global_pt s;
     valid_uses s \<rbrakk>
   \<Longrightarrow> (\<exists>\<rhd> (max_pt_level, get_vspace_of_thread (kheap s) (arch_state s) t)) s"
  by (auto simp: get_vspace_of_thread_def
          split: option.splits cap.splits kernel_object.splits arch_cap.splits if_split_asm pt_type.splits
          intro: vspace_for_asid_vs_lookup)

lemma data_at_aligned:
  "\<lbrakk> data_at sz p s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned p (pageBitsForSize sz)"
  unfolding data_at_def by (auto simp: obj_at_def dest: pspace_alignedD)

lemma some_get_page_info_umapsD:
  "\<lbrakk>get_page_info (aobjs_of s) pt_ref vptr = Some (b, a, attr, r);
    \<exists>\<rhd> (max_pt_level, pt_ref) s; vptr \<in> user_region; valid_vspace_objs s; pspace_aligned s;
    valid_asid_table s; valid_objs s\<rbrakk>
   \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s"
  apply (clarsimp simp: get_page_info_def vs_lookup_table_def)
  apply (clarsimp simp: pt_lookup_slot_def pt_lookup_slot_from_level_def)
  apply (frule pt_walk_max_level)
  apply (drule pt_walk_level)
  apply (rename_tac pte asid pool_ptr vref level pt_ptr')
  apply (prop_tac "vs_lookup_table level asid vptr s = Some (level, pt_ptr')")
   apply (clarsimp simp: vs_lookup_table_def in_omonad)
  apply (drule (2) valid_vspace_objs_strongD; assumption?)
  apply (clarsimp simp: pte_info_def split: pte.splits)
  apply (rename_tac pt ppn)
  apply (frule pspace_aligned_pts_ofD, fastforce)
  apply (drule_tac x="PagePTE b ppn attr r" in bspec)
   apply (erule (1) pt_slot_offset_pt_range, simp)
  apply (subst (asm) valid_pte.simps)
  apply clarsimp
  apply (rule_tac x="vmsize_of_level level" in exI)
  apply (clarsimp simp: obj_at_def)
  apply (drule (1) data_at_aligned)
  apply (simp add: is_aligned_ptrFromPAddr_n_eq)
  done

lemma user_mem_dom_cong:
  "kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')"
  by (simp add: user_mem_def in_user_frame_def dom_def obj_at_def)

lemma device_mem_dom_cong:
  "kheap s = kheap s' \<Longrightarrow> dom (device_mem s) = dom (device_mem s')"
  by (simp add: device_mem_def in_device_frame_def dom_def obj_at_def)

lemma device_frame_in_device_region:
  "\<lbrakk>in_device_frame p s; pspace_respects_device_region s\<rbrakk>
  \<Longrightarrow> device_state (machine_state s) p \<noteq> None"
  by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)

global_naming Arch
named_theorems AInvsPre_asms

lemma get_vspace_of_thread_asid_or_global_pt:
  "(\<exists>asid. vspace_for_asid asid s = Some (get_vspace_of_thread (kheap s) (arch_state s) t))
    \<or> get_vspace_of_thread (kheap s) (arch_state s) t = global_pt s"
  by (auto simp: get_vspace_of_thread_def
           split: option.split kernel_object.split cap.split arch_cap.split pt_type.splits)

lemma get_page_info_gpd_kmaps:
  "\<lbrakk>valid_global_objs s; valid_arch_state s; pspace_aligned s;
    get_page_info (aobjs_of s) (global_pt s) vptr = Some (b, a, attr, r)\<rbrakk>
   \<Longrightarrow> False"
  apply (clarsimp simp: get_page_info_def in_omonad pt_lookup_slot_def pt_lookup_slot_from_level_def)
  apply (clarsimp simp: valid_arch_state_def valid_global_tables_def)
  apply (subst (asm) pt_walk.simps)
  apply (drule (1) pspace_aligned_pts_ofD)
  apply (clarsimp simp: ptes_of_def in_omonad pte_info_def
                        table_base_pt_slot_offset[where level=max_pt_level, simplified])
  done

lemma ptable_rights_imp_frame[AInvsPre_asms]:
  assumes "valid_state s"
  shows "\<lbrakk> ptable_rights t s vptr \<noteq> {}; ptable_lift t s vptr = Some (addrFromPPtr p) \<rbrakk> \<Longrightarrow>
         in_user_frame p s \<or> in_device_frame p s"
  apply (rule ccontr, frule ptable_lift_Some_user_regionD)
  using assms get_vspace_of_thread_asid_or_global_pt[of s t]
  apply (clarsimp simp: ptable_lift_def ptable_rights_def in_user_frame_def in_device_frame_def
                 split: option.splits)
  apply (frule some_get_page_info_umapsD)
         apply (rule get_vspace_of_thread_reachable)
          apply clarsimp
          apply (frule get_page_info_gpd_kmaps[rotated 3])
            apply (simp_all add: valid_state_def valid_pspace_def valid_arch_state_def)
  apply clarsimp
  apply (drule_tac x=sz in spec)+
  apply (rename_tac p_addr attr rghts sz)
  apply (frule is_aligned_add_helper[OF _ and_mask_less', THEN conjunct2, of _ _ vptr])
   apply (simp only: pbfs_less_wb'[simplified word_bits_def])
  apply (clarsimp simp: data_at_def ptrFromPAddr_def addrFromPPtr_def field_simps)
  apply (subgoal_tac "p_addr + (pptrBaseOffset + (vptr && mask (pageBitsForSize sz)))
                        && ~~ mask (pageBitsForSize sz) = p_addr + pptrBaseOffset")
   apply simp
  apply (subst add.assoc[symmetric])
  apply (subst is_aligned_add_helper)
    apply (erule aligned_add_aligned)
     apply (case_tac sz; simp add: is_aligned_def pptrBaseOffset_def pptrBase_def paddrBase_def
                                   canonical_bit_def bit_simps)
    apply simp
   apply (rule and_mask_less')
   apply (case_tac sz; simp add: bit_simps)
  apply simp
  done

end

interpretation AInvsPre?: AInvsPre
proof goal_cases
  interpret Arch .
  case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?)
qed

requalify_facts
  AARCH64.user_mem_dom_cong
  AARCH64.device_mem_dom_cong
  AARCH64.device_frame_in_device_region

end