Theory Denotational_Semantics
section ‹Denotational semantics of Circus actions›
theory Denotational_Semantics
imports Circus_Actions Var_list
begin
text ‹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.›
subsection ‹Skip›
definition Skip :: "('θ::ev_eq,'σ) action" where
"Skip ≡ action_of
(R (true ⊢ λ(A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A = more A'))"
lemma Skip_is_action:
"(R (true ⊢ λ(A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A = more A')) ∈ {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
by auto
lemmas Skip_is_CSP = Skip_is_action[simplified]
lemma relation_of_Skip:
"relation_of Skip =
(R (true ⊢ λ(A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A = more A'))"
by (simp add: Skip_def action_of_inverse Skip_is_CSP)
definition CSP3::"(('θ::ev_eq,'σ) alphabet_rp) Healthiness_condition"
where "CSP3 (P) ≡ relation_of Skip ;; P"
definition CSP4::"(('θ::ev_eq,'σ) alphabet_rp) Healthiness_condition"
where "CSP4 (P) ≡ 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 ‹Stop›
definition Stop :: "('θ::ev_eq,'σ) action"
where "Stop ≡ action_of (R (true ⊢ λ(A, A'). tr A' = tr A ∧ wait A'))"
lemma Stop_is_action:
"(R (true ⊢ λ(A, A'). tr A' = tr A ∧ wait A')) ∈ {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 ⊢ λ(A, A'). tr A' = tr A ∧ 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 ≤ tr ba", simp_all)
apply (case_tac "ok ba", simp_all)
apply (case_tac "tr ba ≤ 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 ≤ tr ba", simp_all)
apply (case_tac "ok ba", simp_all)
apply (case_tac "tr ba ≤ 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 ‹Chaos›
definition Chaos :: "('θ::ev_eq,'σ) action"
where "Chaos ≡ action_of (R(false ⊢ true))"
lemma Chaos_is_action: "(R(false ⊢ true)) ∈ {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 ⊢ true))"
by (simp add: Chaos_def action_of_inverse Chaos_is_CSP)
subsection ‹State update actions›
definition Pre ::"'σ relation ⇒ 'σ predicate"
where "Pre sc ≡ λA. ∃ A'. sc (A, A')"
definition state_update_before :: "'σ relation ⇒ ('θ::ev_eq,'σ) action ⇒ ('θ,'σ) action"
where "state_update_before sc Ac = action_of(R ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A'). sc (more A, more A') & ¬wait A' & tr A = tr A')) ;; relation_of Ac)"
lemma state_update_before_is_action:
"(R ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A').sc (more A, more A') & ¬wait A' & tr A = tr A')) ;; relation_of Ac) ∈ {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 ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A'). sc (more A, more A') & ¬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 mono_state_update_before: "mono (state_update_before sc)"
by (auto simp: mono_def less_eq_action ref_def relation_of_state_update_before 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_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 ≤ tr ab", simp_all)
apply (case_tac "ok ab", simp_all)
apply (case_tac "tr ab ≤ 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 :: "'σ relation ⇒ ('θ::ev_eq,'σ) action ⇒ ('θ,'σ) action"
where "state_update_after sc Ac = action_of(relation_of Ac ;; R (true ⊢ (λ(A, A'). sc (more A, more A') & ¬wait A' & tr A = tr A')))"
lemma state_update_after_is_action:
"(relation_of Ac ;; R (true ⊢ (λ(A, A'). sc (more A, more A') & ¬wait A' & tr A = tr A'))) ∈ {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 ⊢ (λ(A, A'). sc (more A, more A') & ¬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 ≤ tr c", simp_all)
apply (case_tac "ok ca", simp_all)
apply (case_tac "tr ca ≤ tr c", simp_all)
apply (auto simp add: prefix_def comp_def true_def split: cond_splits)
done
subsection ‹Sequential composition›
definition
Seq::"('θ::ev_eq,'σ) action ⇒ ('θ,'σ) action ⇒ ('θ,'σ) action" (infixl ‹`;`› 24)
where "P `;` Q ≡ action_of (relation_of P ;; relation_of Q)"
lemma Seq_is_action: "(relation_of P ;; relation_of Q) ∈ {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 ‹Internal choice›
definition
Ndet::"('θ::ev_eq,'σ) action ⇒ ('θ,'σ) action ⇒ ('θ,'σ) action" (infixl ‹⊓› 18)
where "P ⊓ Q ≡ action_of ((relation_of P) ∨ (relation_of Q))"
lemma Ndet_is_action: "((relation_of P) ∨ (relation_of Q)) ∈ {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 ⊓ Q) = ((relation_of P) ∨ (relation_of Q))"
by (simp add: Ndet_def action_of_inverse Ndet_is_CSP)
lemma mono_Ndet: "mono ((⊓) P)"
by (auto simp: mono_def less_eq_action ref_def relation_of_Ndet)
subsection ‹External choice›
definition
Det::"('θ::ev_eq,'σ) action ⇒ ('θ,'σ) action ⇒ ('θ,'σ) action" (infixl ‹□› 18)
where "P □ Q ≡ action_of(R((¬((relation_of P)⇧f⇩f) ∧ ¬((relation_of Q)⇧f⇩f)) ⊢
(((relation_of P)⇧t⇩f ∧ ((relation_of Q)⇧t⇩f))
◃ λ(A, A'). tr A = tr A' ∧ wait A' ▹
((relation_of P)⇧t⇩f ∨ ((relation_of Q)⇧t⇩f)))))"
lemma Det_is_action:
"(R((¬((relation_of P)⇧f⇩f) ∧ ¬((relation_of Q)⇧f⇩f)) ⊢
(((relation_of P)⇧t⇩f ∧ ((relation_of Q)⇧t⇩f))
◃ λ(A, A'). tr A = tr A' ∧ wait A' ▹
((relation_of P)⇧t⇩f ∨ ((relation_of Q)⇧t⇩f))))) ∈ {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 □ Q) = (R((¬((relation_of P)⇧f⇩f) ∧ ¬((relation_of Q)⇧f⇩f)) ⊢
(((relation_of P)⇧t⇩f ∧ ((relation_of Q)⇧t⇩f))
◃ λ(A, A'). tr A = tr A' ∧ wait A' ▹
((relation_of P)⇧t⇩f ∨ ((relation_of Q)⇧t⇩f)))))"
apply (unfold Det_def)
apply (rule action_of_inverse)
apply (rule Det_is_action)
done
lemma mono_Det: "mono ((□) 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 ‹Reactive design assignment›
definition
"rd_assign s = action_of (R (true ⊢ λ(A, A'). ref A' = ref A ∧ tr A' = tr A ∧ ¬wait A' ∧ more A' = s))"
lemma rd_assign_is_action:
"(R (true ⊢ λ(A, A'). ref A' = ref A ∧ tr A' = tr A ∧ ¬wait A' ∧ more A' = s)) ∈ {p. is_CSP_process p}"
apply (auto simp:)
apply (rule rd_is_CSP)
by auto
lemmas rd_assign_is_CSP = rd_assign_is_action[simplified]
lemma relation_of_rd_assign:
"relation_of (rd_assign s) =
(R (true ⊢ λ(A, A'). ref A' = ref A ∧ tr A' = tr A ∧ ¬wait A' ∧ more A' = s))"
by (simp add: rd_assign_def action_of_inverse rd_assign_is_CSP)
subsection ‹Local state external choice›
definition
Loc::"'σ ⇒ ('θ::ev_eq,'σ) action ⇒ 'σ ⇒ ('θ,'σ) action ⇒ ('θ,'σ) action"
(‹'(()loc _ ∙ _ ') \<boxplus> '(()loc _ ∙ _ ')›)
where "(loc s1 ∙ P) \<boxplus> (loc s2 ∙ Q) ≡
((rd_assign s1)`;`P) □ ((rd_assign s2)`;` Q)"
subsection ‹Schema expression›
definition Schema :: "'σ relation ⇒ ('θ::ev_eq,'σ) action" where
"Schema sc ≡ action_of(R ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A'). sc (more A, more A') ∧ ¬wait A' ∧ tr A = tr A')))"
lemma Schema_is_action:
"(R ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A'). sc (more A, more A') & ¬wait A' & tr A = tr A'))) ∈ {p. is_CSP_process p}"
apply (simp)
apply (rule rd_is_CSP)
apply (auto)
done
lemmas Schema_is_CSP = Schema_is_action[simplified]
lemma relation_of_Schema:
"relation_of (Schema sc) = (R ((λ(A, A'). (Pre sc) (more A)) ⊢
(λ(A, A'). sc (more A, more A') ∧ ¬wait A' ∧ 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 ‹Parallel composition›
type_synonym 'σ local_state = "('σ × ('σ ⇒ 'σ ⇒ 'σ))"
fun MergeSt :: "'σ local_state ⇒ 'σ local_state ⇒ ('θ,'σ) relation_rp" where
"MergeSt (s1,s1') (s2,s2') = ((λ(S, S'). (s1' s1) (more S) = more S');;
(λ(S::('θ,'σ) alphabet_rp, S'). (s2' s2) (more S) = more S'))"
definition listCons ::"'θ ⇒ 'θ list list ⇒ 'θ list list" (‹_ ## _›) where
"a ## l = ((map (Cons a)) l)"
fun ParMergel :: "'θ::ev_eq list ⇒ 'θ list ⇒ 'θ set ⇒ 'θ 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::"'θ::ev_eq list ⇒ 'θ list ⇒ 'θ set ⇒ 'θ list set" where
"ParMerge tr1 tr2 cs = set (ParMergel tr1 tr2 cs)"
lemma set_Cons1: "tr1 ∈ set l ⟹ a # tr1 ∈ (#) a ` set l"
by (auto)
lemma tr_in_set_eq: "(tr1 ∈ (#) b ` set l) = (tr1 ≠ [] ∧ hd tr1 = b ∧ tl tr1 ∈ set l)"
by (induct l) auto
definition M_par::"(('θ::ev_eq), 'σ) alpha_rp_scheme ⇒ ('σ ⇒ 'σ ⇒ 'σ)
⇒ ('θ, 'σ) alpha_rp_scheme ⇒ ('σ ⇒ 'σ ⇒ 'σ)
⇒ ('θ set) ⇒ ('θ, 'σ) relation_rp" where
"M_par s1 x1 s2 x2 cs =
((λ(S, S'). ((diff_tr S' S) ∈ ParMerge (diff_tr s1 S) (diff_tr s2 S) cs &
ev_eq (tr_filter (tr s1) cs) (tr_filter (tr s2) cs))) ∧
((λ(S, S'). (wait s1 ∨ wait s2) ∧
ref S' ⊆ ((((ref s1)∪(ref s2))∩cs)∪(((ref s1)∩(ref s2))-cs)))
◃ wait o snd ▹
((λ(S, S'). (¬wait s1 ∨ ¬wait s2)) ∧ MergeSt ((more s1), x1) ((more s2), x2))))"
definition Par::"('θ::ev_eq,'σ) action ⇒
('σ ⇒ 'σ ⇒ 'σ) ⇒ 'θ set ⇒ ('σ ⇒ 'σ ⇒ 'σ) ⇒
('θ,'σ) action ⇒ ('θ,'σ) action" (‹_ ⟦ _ | _ | _ ⟧ _›) where
"A1 ⟦ ns1 | cs | ns2 ⟧ A2 ≡ (action_of (R ((λ (S, S').
¬ (∃ tr1 tr2. ((relation_of A1)⇧f⇩f ;; (λ (S, S'). tr1 = (tr S))) (S, S')
∧ (spec False (wait S) (relation_of A2) ;; (λ (S, _). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs))) ∧
¬ (∃ tr1 tr2. (spec False (wait S) (relation_of A1);;(λ(S, _). tr1 = tr S)) (S, S')
∧ ((relation_of A2)⇧f⇩f ;; (λ(S, S'). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) ⊢
(λ (S, S'). (∃ s1 s2. ((λ (A, A'). (relation_of A1)⇧t⇩f (A, s1)
∧ ((relation_of A2)⇧t⇩f (A, s2)));; M_par s1 ns1 s2 ns2 cs) (S, S'))))))"
lemma Par_is_action: "(R ((λ (S, S').
¬ (∃ tr1 tr2. ((relation_of A1)⇧f⇩f ;; (λ (S, S'). tr1 = (tr S))) (S, S')
∧ (spec False (wait S) (relation_of A2) ;; (λ (S, S'). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs))) ∧
¬ (∃ tr1 tr2. (spec False (wait S) (relation_of A1);;(λ(S, _). tr1 = tr S)) (S, S')
∧ ((relation_of A2)⇧f⇩f ;; (λ (S, S'). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) ⊢
(λ (S, S'). (∃ s1 s2. ((λ (A, A'). (relation_of A1)⇧t⇩f (A, s1)
∧ ((relation_of A2)⇧t⇩f (A, s2)));; M_par s1 ns1 s2 ns2 cs) (S, S'))))) ∈ {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 ⟦ ns1 | cs | ns2 ⟧ A2) = (R ((λ (S, S').
¬ (∃ tr1 tr2. ((relation_of A1)⇧f⇩f ;; (λ (S, S'). tr1 = (tr S))) (S, S')
∧ (spec False (wait S) (relation_of A2) ;; (λ (S, S'). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs))) ∧
¬ (∃ tr1 tr2. (spec False (wait S) (relation_of A1);;(λ(S, _). tr1 = tr S)) (S, S')
∧ ((relation_of A2)⇧f⇩f ;; (λ (S, S'). tr2 = (tr S))) (S, S')
∧ ((tr_filter tr1 cs) = (tr_filter tr2 cs)))) ⊢
(λ (S, S'). (∃ s1 s2. ((λ (A, A'). (relation_of A1)⇧t⇩f (A, s1)
∧ ((relation_of A2)⇧t⇩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 (λQ. P ⟦ ns1 | cs | ns2 ⟧ 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 ‹Local parallel block›
definition
ParLoc::"'σ ⇒ ('σ ⇒ 'σ ⇒ 'σ) ⇒ ('θ::ev_eq, 'σ) action ⇒ 'θ set ⇒ 'σ ⇒ ('σ ⇒ 'σ ⇒ 'σ) ⇒ ('θ,'σ) action ⇒ ('θ,'σ) action"
(‹'(()par _ | _ ∙ _ ') ⟦ _ ⟧ '(()par _ | _ ∙ _ ')›)
where
"(par s1 | ns1 ∙ P) ⟦ cs ⟧ (par s2 | ns2 ∙ Q) ≡ ((rd_assign s1)`;`P) ⟦ ns1 | cs | ns2 ⟧ ((rd_assign s2)`;` Q)"
subsection ‹Assignment›
definition ASSIGN::"('v, 'σ) var_list ⇒ ('σ ⇒ 'v) ⇒ ('θ::ev_eq, 'σ) action" where
"ASSIGN x e ≡ action_of (R (true ⊢ (λ (S, S'). tr S' = tr S ∧ ¬wait S' ∧
(more S' = (update x (λ_. (e (more S)))) (more S)))))"
syntax "_assign"::"id ⇒ ('σ ⇒ 'v) ⇒ ('θ, 'σ) action" (‹_ `:=` _›)
translations "y `:=` vv" => "CONST ASSIGN (VAR y) vv"
lemma Assign_is_action:
"(R (true ⊢ (λ (S, S'). tr S' = tr S ∧ ¬wait S' ∧
(more S' = (update x (λ_. (e (more S)))) (more S))))) ∈ {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 ⊢ (λ (S, S'). tr S' = tr S ∧ ¬wait S' ∧
(more S' = (update x (λ_. (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 (λ (s, s') . s' = (update x (λ_. (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 ‹Variable scope›
definition Var::"('v, 'σ) var_list ⇒('θ, 'σ) action ⇒ ('θ::ev_eq,'σ) action" where
"Var v A ≡ action_of(
(R(true ⊢ (λ (A, A'). ∃ a. tr A' = tr A ∧ ¬wait A' ∧ more A' = (increase v a (more A)))));;
(relation_of A;;
(R(true ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A' = (decrease v (more A)))))))"
syntax "_var"::"idt ⇒ ('θ, 'σ) action ⇒ ('θ, 'σ) action" (‹var _ ∙ _› [1000] 999)
translations "var y ∙ Act" => "CONST Var (VAR_LIST y) Act"
lemma Var_is_action:
"((R(true ⊢ (λ (A, A'). ∃ a. tr A' = tr A ∧ ¬wait A' ∧ more A' = (increase v a (more A)))));;
(relation_of A;;
(R(true ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A' = (decrease v (more A))))))) ∈ {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 ⊢ (λ (A, A'). ∃ a. tr A' = tr A ∧ ¬wait A' ∧ more A' = (increase v a (more A)))));;
(relation_of A;;
(R(true ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ 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, 'σ) var_list ⇒('θ, 'σ) action ⇒ ('θ::ev_eq,'σ) action" where
"Let v A ≡ action_of((relation_of A;;
(R(true ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A' = (decrease v (more A)))))))"
syntax "_let"::"idt ⇒ ('θ, 'σ) action ⇒ ('θ, 'σ) action" (‹let _ ∙ _› [1000] 999)
translations "let y ∙ Act" => "CONST Let (VAR_LIST y) Act"
lemma Let_is_action:
"(relation_of A;;
(R(true ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ more A' = (decrease v (more A)))))) ∈ {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 ⊢ (λ (A, A'). tr A' = tr A ∧ ¬wait A' ∧ 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 (λ (s, s'). ∃ 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 "∃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 "∃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 (λ (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 ‹Guarded action›
definition Guard::"'σ predicate ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action" (‹_ `&` _›)
where "g `&` P ≡ action_of(R (((g o more o fst) ⟶ ¬ ((relation_of P)⇧f⇩f)) ⊢
(((g o more o fst) ∧ ((relation_of P)⇧t⇩f)) ∨
((¬(g o more o fst)) ∧ (λ (A, A'). tr A' = tr A ∧ wait A')))))"
lemma Guard_is_action:
"(R ( ((g o more o fst) ⟶ ¬ ((relation_of P)⇧f⇩f)) ⊢
(((g o more o fst) ∧ ((relation_of P)⇧t⇩f)) ∨
((¬(g o more o fst)) ∧ (λ (A, A'). tr A' = tr A ∧ wait A'))))) ∈ {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) ⟶ ¬ ((relation_of P)⇧f⇩f)) ⊢
(((g o more o fst) ∧ ((relation_of P)⇧t⇩f)) ∨
((¬(g o more o fst)) ∧ (λ (A, A'). tr A' = tr A ∧ 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: "⋀ a b. g (alpha_rp.more a) = False ⟹
(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: "⋀ a b. g (alpha_rp.more a) = True ⟹
(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 (λ (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 ‹Prefixed action›
definition do where
"do e ≡ (λ(A, A'). tr A = tr A' ∧ (e (more A)) ∉ (ref A')) ◃ wait o snd ▹
(λ(A, A'). tr A' = (tr A @[(e (more A))]))"
definition do_I::"('σ ⇒'θ) ⇒ 'θ set ⇒ ('θ, 'σ) relation_rp"
where "do_I c S ≡ ((λ(A, A'). tr A = tr A' & S ∩ (ref A') = {})
◃ wait o snd ▹
(λ(A, A'). hd (tr A' - tr A) ∈ S & (c (more A) = (last (tr A')))))"
definition
iPrefix::"('σ ⇒'θ::ev_eq) ⇒ ('σ relation) ⇒ (('θ, 'σ) action ⇒ ('θ, 'σ) action) ⇒ ('σ ⇒ 'θ set) ⇒ ('θ, 'σ) action ⇒ ('θ, 'σ) action" where
"iPrefix c i j S P ≡ action_of(R(true ⊢ (λ (A, A'). (do_I c (S (more A))) (A, A') & more A' = more A)))`;` P"
definition
oPrefix::"('σ ⇒'θ) ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action" where
"oPrefix c P ≡ action_of(R(true ⊢ (do c) ∧ (λ (A, A'). more A' = more A)))`;` P"
definition Prefix0::"'θ ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action" where
"Prefix0 c P ≡ action_of(R(true ⊢ (do (λ _. c)) ∧ (λ (A, A'). more A' = more A)))`;` P"
definition
read::"('v ⇒ 'θ) ⇒ ('v, 'σ) var_list ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action"
where "read c x P ≡ iPrefix (λ A. c (select x A)) (λ (s, s'). ∃ a. s' = increase x a s) (Let x) (λ_. range c) P"
definition
read1::"('v ⇒ 'θ) ⇒ ('v, 'σ) var_list ⇒ ('σ ⇒ 'v set) ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action"
where "read1 c x S P ≡ iPrefix (λ A. c (select x A)) (λ (s, s'). ∃ a. a∈(S s) & s' = increase x a s) (Let x) (λs. c`(S s)) P"
definition
write1::"('v ⇒ 'θ) ⇒ ('σ ⇒ 'v) ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action"
where "write1 c a P ≡ oPrefix (λ A. c (a A)) P"
definition
write0::"'θ ⇒ ('θ::ev_eq, 'σ) action ⇒ ('θ, 'σ) action"
where "write0 c P ≡ Prefix0 c P"
syntax
"_read" ::"[id, pttrn, ('θ, 'σ) action] => ('θ, 'σ) action" (‹(_`?`_ /→ _)›)
"_readS" ::"[id, pttrn, 'θ set,('θ, 'σ) action] => ('θ, 'σ) action" (‹(_`?`_`:`_ /→ _)›)
"_readSS" ::"[id, pttrn, 'σ => 'θ set,('θ, 'σ) action] => ('θ, 'σ) action" (‹(_`?`_`∈`_ /→ _)›)
"_write" ::"[id, 'σ, ('θ, 'σ) action] => ('θ, 'σ) action" (‹(_`!`_ /→ _)›)
"_writeS"::"['θ, ('θ, 'σ) action] => ('θ, 'σ) action" (‹(_ /→ _)›)
translations
"_read c p P" == "CONST read c (VAR_LIST p) P"
"_readS c p b P" == "CONST read1 c (VAR_LIST p) (λ_. 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 ⊢ (do c) ∧ (λ (A, A'). more A' = more A))) ∈ {p. is_CSP_process p}"
by (auto intro: rd_is_CSP)
lemma Prefix1_is_action:
"(R(true ⊢ λ(A, A'). do_I c (S (alpha_rp.more A)) (A, A') ∧ alpha_rp.more A' = alpha_rp.more A)) ∈ {p. is_CSP_process p}"
by (auto intro: rd_is_CSP)
lemma Prefix0_is_action:
"(R(true ⊢ (do c) ∧ (λ (A, A'). more A' = more A))) ∈ {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 ⊢ (λ (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 ⊢ (do c) ∧ (λ (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 ⊢ (do (λ _. c)) ∧ (λ (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 ‹Hiding›
definition Hide::"('θ::ev_eq, 'σ) action ⇒ 'θ set ⇒ ('θ, 'σ) action" (infixl ‹\› 18) where
"P \\ cs ≡ action_of(R(λ(S, S'). ∃ s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) &
(relation_of P)(S, S'⦇tr := s, ref := (ref S') ∪ cs ⦈));; (relation_of Skip))"
definition
"hid P cs == (R(λ(S, S'). ∃ s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) & (relation_of P)(S, S'⦇tr := s, ref := (ref S') ∪ cs ⦈)) ;; (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(λ(S, S'). ∃ s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs) &
(relation_of P)(S, S'⦇tr := s, ref := (ref S') ∪ cs ⦈));; (relation_of Skip)) ∈ {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(λ(S, S'). ∃ s. (diff_tr S' S) = (tr_filter (s - (tr S)) cs)
& (relation_of P)(S, S'⦇tr :=s, ref := (ref S') ∪ cs ⦈));; (relation_of Skip))"
by (simp add: Hide_def action_of_inverse Hide_is_CSP)
lemma mono_Hide : "mono(λ P. P \\ cs)"
by (auto simp: mono_def less_eq_action ref_def prefix_def utp_defs relation_of_Hide rp_defs)
subsection ‹Recursion›
text ‹To represent the recursion operator "‹μ›" 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.›
text ‹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.
›
syntax "_MU"::"[idt, idt ⇒ ('θ, 'σ) action] ⇒ ('θ, 'σ) action" (‹μ _ ∙ _›)
translations "_MU X P" == "CONST lfp (λ X. P)"
text‹Instead fo the following:›
lemma is_action_REP_Mu:
shows "is_CSP_process (relation_of (lfp P))"
oops
text‹... 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.›
text‹Monotonicity: STATUS: probably critical. Does not seem to be necessary for
parameterless Circus.›
lemma mono_Mu:
assumes A : "mono P"
and B : "⋀ X. mono (P X)"
shows "mono (lfp P)"
apply (subst lfp_unfold)
apply (auto simp: A B)
done
term Nat.Suc
end