16 isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") |
16 isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") |
17 |
17 |
18 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *) |
18 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *) |
19 |
19 |
20 section {* Customization *} |
20 section {* Customization *} |
21 |
|
22 subsection{* Setup for map, set, pred *} |
|
23 |
|
24 lemma pre_process_pred[simp]: |
|
25 "pre_process_pred (op =) \<phi> (Inl (a,p)) (Inl (a',p')) \<longleftrightarrow> a = a' \<and> \<phi> p p'" |
|
26 "pre_process_pred (op =) \<phi> (Inr (p,q)) (Inr (p',q')) \<longleftrightarrow> \<phi> p p' \<and> \<phi> q q'" |
|
27 "\<not> pre_process_pred (op =) \<phi> (Inl ap) (Inr q1q2)" |
|
28 "\<not> pre_process_pred (op =) \<phi> (Inr q1q2) (Inl ap)" |
|
29 by (auto simp: diag_def pre_process.pred_unfold) |
|
30 |
|
31 |
21 |
32 subsection {* Basic properties *} |
22 subsection {* Basic properties *} |
33 |
23 |
34 declare |
24 declare |
35 process.inject[simp] |
25 process.inject[simp] |
36 process.distinct[simp] |
26 process.distinct[simp] |
37 process.discs[simp] |
27 process.discs[simp] |
38 process.sels[simp] |
28 process.sels[simp] |
39 process.collapse[simp] |
29 process.collapse[simp] |
|
30 pre_process.pred_unfold[simp] |
40 |
31 |
41 lemmas process_exhaust = |
32 lemmas process_exhaust = |
42 process.exhaust[elim, case_names Action Choice] |
33 process.exhaust[elim, case_names Action Choice] |
43 |
34 |
44 (* Constructors versus discriminators *) |
35 (* Constructors versus discriminators *) |