1(* ========================================================================== *)
2(* FILE          : ExampleScript.sml                                           *)
3(* DESCRIPTION   : Example theorems and definitions used in the thesis         *)
4(*                                                                            *)
5(* THESIS        : A Formalization of Unique Solutions of Equations in        *)
6(*                 Process Algebra                                            *)
7(* AUTHOR        : (c) Chun Tian, University of Bologna                       *)
8(* DATE          : 2017                                                       *)
9(* ========================================================================== *)
10
11open HolKernel Parse boolLib bossLib;
12
13open pred_setTheory relationTheory pairTheory sumTheory listTheory;
14open prim_recTheory arithmeticTheory combinTheory stringTheory;
15
16open CCSLib CCSTheory CCSSyntax CCSConv;
17open StrongEQTheory StrongEQLib StrongLawsTheory;
18open WeakEQTheory WeakEQLib WeakLawsTheory;
19open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory;
20open CongruenceTheory CoarsestCongrTheory;
21open TraceTheory ExpansionTheory ContractionTheory;
22open BisimulationUptoTheory UniqueSolutionsTheory;
23
24val _ = new_theory "Example";
25val _ = temp_loose_equality ();
26
27(* For paper generating purposes, some type abbreviations are disabled *)
28val _ = disable_tyabbrev_printing "transition";
29val _ = disable_tyabbrev_printing "context";
30val _ = disable_tyabbrev_printing "simulation";
31val _ = disable_tyabbrev_printing "list_simulation";
32
33(******************************************************************************)
34(*                                                                            *)
35(*          The proof of PROPERTY_STAR (old way as in Milner's book)          *)
36(*                                                                            *)
37(******************************************************************************)
38
39(*
40 In StrongEQScript.ml, currently we define STRONG_EQUIV (strong bisimilarity) by
41 HOL's co-inductive package (Hol_coreln):
42
43val (STRONG_EQUIV_rules, STRONG_EQUIV_coind, STRONG_EQUIV_cases) = Hol_coreln `
44    (!(E :('a, 'b) CCS) (E' :('a, 'b) CCS).
45       (!u.
46         (!E1. TRANS E u E1 ==>
47               (?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2)) /\
48         (!E2. TRANS E' u E2 ==>
49               (?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2))) ==> STRONG_EQUIV E E')`;
50
51  then the 3rd returned value (STRONG_EQUIV_cases) is just the PROPERTY_STAR:
52
53(* Prop. 4, page 91: strong equivalence satisfies property [*] *)
54val PROPERTY_STAR = save_thm ((* NEW *)
55   "PROPERTY_STAR", STRONG_EQUIV_cases);
56
57 However, if we started with the original definition of STRONG_EQUIV, which now
58 becomes a theorem:
59
60val STRONG_EQUIV = new_definition (
61   "STRONG_EQUIV",
62  ``STRONG_EQUIV E E' = ?Bsm. Bsm E E' /\ STRONG_BISIM Bsm``);
63
64 It's not easy to prove PROPERTY_STAR, below is the proof of Robin Milner through
65 a temporarily definition STRONG_EQUIV', originally formalized by Monica Nesi.
66
67 *)
68
69(* Definition 3, page 91 in Milner's book. *)
70val STRONG_EQUIV' = new_definition (
71   "STRONG_EQUIV'",
72  ``STRONG_EQUIV' E E' =
73        (!u.
74         (!E1. TRANS E u E1 ==>
75               (?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2)) /\
76         (!E2. TRANS E' u E2 ==>
77               (?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2)))``);
78
79(* Strong equivalence implies the new relation. *)
80val STRONG_EQUIV_IMP_STRONG_EQUIV' = store_thm (
81   "STRONG_EQUIV_IMP_STRONG_EQUIV'",
82      ``!E E'. STRONG_EQUIV E E' ==> STRONG_EQUIV' E E'``,
83    rpt GEN_TAC
84 >> REWRITE_TAC [STRONG_EQUIV', STRONG_EQUIV]
85 >> rpt STRIP_TAC (* 2 sub-goals *)
86 >> IMP_RES_TAC
87      (MATCH_MP (EQ_MP STRONG_BISIM (ASSUME ``STRONG_BISIM Bsm``))
88                (ASSUME ``(Bsm: ('a, 'b) simulation) E E'``))
89 >| [ Q.EXISTS_TAC `E2`,
90      Q.EXISTS_TAC `E1` ]
91 >> ASM_REWRITE_TAC []
92 >> Q.EXISTS_TAC `Bsm`
93 >> ASM_REWRITE_TAC [] );
94
95val STRONG_EQUIV'_IS_STRONG_BISIM = store_thm (
96   "STRONG_EQUIV'_IS_STRONG_BISIM",
97  ``STRONG_BISIM STRONG_EQUIV'``,
98    PURE_ONCE_REWRITE_TAC [STRONG_BISIM]
99 >> rpt STRIP_TAC (* 2 sub-goals here *)
100 >> IMP_RES_TAC
101       (EQ_MP (Q.SPECL [`E`, `E'`] STRONG_EQUIV')
102              (ASSUME ``STRONG_EQUIV' E E'``))
103 >| [ Q.EXISTS_TAC `E2`,
104      Q.EXISTS_TAC `E1` ]
105 >> IMP_RES_TAC STRONG_EQUIV_IMP_STRONG_EQUIV'
106 >> ASM_REWRITE_TAC []);
107
108(* The new relation implies strong equivalence. *)
109val STRONG_EQUIV'_IMP_STRONG_EQUIV = store_thm (
110   "STRONG_EQUIV'_IMP_STRONG_EQUIV",
111      ``!E E'. STRONG_EQUIV' E E' ==> STRONG_EQUIV E E'``,
112    rpt STRIP_TAC
113 >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV]
114 >> EXISTS_TAC ``STRONG_EQUIV'``
115 >> ASM_REWRITE_TAC [STRONG_EQUIV'_IS_STRONG_BISIM]);
116
117(* Prop. 4, page 91: strong equivalence satisfies property [*] *)
118val PROPERTY_STAR' = store_thm (
119   "PROPERTY_STAR'",
120      ``!E E'. STRONG_EQUIV E E' =
121         (!u.
122           (!E1. TRANS E u E1 ==>
123                 (?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2)) /\
124           (!E2. TRANS E' u E2 ==>
125                 (?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2)))``,
126    rpt GEN_TAC
127 >> EQ_TAC (* 2 sub-goals here *)
128 >| [ PURE_ONCE_REWRITE_TAC
129        [ONCE_REWRITE_RULE [STRONG_EQUIV'] STRONG_EQUIV_IMP_STRONG_EQUIV'],
130      PURE_ONCE_REWRITE_TAC
131        [ONCE_REWRITE_RULE [STRONG_EQUIV'] STRONG_EQUIV'_IMP_STRONG_EQUIV] ]);
132
133(******************************************************************************)
134(*                                                                            *)
135(*                     The coffee machine model                               *)
136(*                                                                            *)
137(******************************************************************************)
138
139val VM = ``rec "VM" (In "coin"..(In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
140                                 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))``;
141
142(* ex1 =
143|- label (name "a")..label (name "b")..nil +
144   label (name "b")..label (name "a")..nil
145   -label (name "a")->
146   label (name "b")..nil
147 *)
148local
149    val t1 = ISPEC ``label (name "a")`` (ISPEC ``prefix (label (name "b")) nil`` PREFIX)
150    and t2 = ISPECL [``prefix (label (name "a")) (prefix (label (name "b")) nil)``,
151                    ``label (name "a")``,
152                    ``prefix (label (name "b")) nil``,
153                    ``prefix (label (name "b")) (prefix (label (name "a")) nil)``]
154                   SUM1;
155in
156    val ex1 = save_thm ("ex1", MP t2 t1)
157end;
158
159(******************************************************************************)
160(*                                                                            *)
161(*       Example showing no difference between ind and coind definitions      *)
162(*                                                                            *)
163(******************************************************************************)
164
165val (List_rules, List_ind, List_cases) = Hol_reln
166   `(!l. (l = []) ==> List l) /\
167    (!l h t. (l = h::t) /\ List t ==> List l)`;
168
169val (coList_rules, coList_coind, coList_cases) = Hol_coreln
170   `(!l. (l = []) ==> coList l) /\
171    (!l h t. (l = h::t) /\ coList t ==> coList l)`;
172
173val List_imp_coList = store_thm (
174   "List_imp_coList", ``!l. List l ==> coList l``,
175    HO_MATCH_MP_TAC List_ind
176 >> RW_TAC bool_ss [coList_rules]);
177
178val coList_imp_List = store_thm (
179   "coList_imp_List", ``!l. coList l ==> List l``,
180    Induct_on `l`
181 >| [ RW_TAC bool_ss [List_rules, coList_rules],
182      STRIP_TAC
183   >> ONCE_REWRITE_TAC [coList_cases]
184   >> ONCE_REWRITE_TAC [List_cases]
185   >> REPEAT STRIP_TAC
186   >| [ ASM_REWRITE_TAC [],
187        SIMP_TAC list_ss []
188     >> `t = l` by PROVE_TAC [CONS_11]
189     >> PROVE_TAC [] ] ]);
190
191val List_eq_coList = store_thm (
192   "List_eq_coList", ``!l. coList l = List l``,
193    PROVE_TAC [List_imp_coList, coList_imp_List]);
194
195(******************************************************************************)
196(*                                                                            *)
197(*                        Example used in presentation                        *)
198(*                                                                            *)
199(******************************************************************************)
200
201local
202    val (temp_A, trans) = CCS_TRANS ``label (name "a")..nil || label (coname "a")..nil``;
203    val nodes = map (fn (l, s) => CCS_TRANS s) trans;
204in
205  val ex_A = save_thm ("ex_A", temp_A);
206  val [ex_A1, ex_A2, ex_A3] = map (fn (n, (thm, _)) => save_thm (n, thm))
207                                (combine (["ex_A1", "ex_A2", "ex_A3"], nodes))
208end;
209
210val (WB_rules, WB_coind, WB_cases) = Hol_coreln `
211    (!(P :('a, 'b) CCS) (Q :('a, 'b) CCS).
212       (!l.
213         (!P'. TRANS P (label l) P' ==>
214               (?Q'. WEAK_TRANS Q (label l) Q' /\ WB P' Q')) /\
215         (!Q'. TRANS Q (label l) Q' ==>
216               (?P'. WEAK_TRANS P (label l) P' /\ WB P' Q'))) /\
217       (!P'. TRANS P tau P' ==> (?Q'. EPS Q Q' /\ WB P' Q')) /\
218       (!Q'. TRANS Q tau Q' ==> (?P'. EPS P P' /\ WB P' Q'))
219     ==> WB P Q)`;
220
221(* SOS rules with changed variable names *)
222val PREFIX' = store_thm (
223   "PREFIX'", ``!P u. TRANS (prefix u P) u P``,
224    PROVE_TAC [PREFIX]);
225
226val SUM1' = store_thm (
227   "SUM1'", ``!P u P' Q.    TRANS P u P' ==> TRANS (sum P Q) u P'``,
228    PROVE_TAC [SUM1]);
229
230val SUM2' = store_thm (
231   "SUM2'", ``!P u P' Q.    TRANS P u P' ==> TRANS (sum Q P) u P'``,
232    PROVE_TAC [SUM2]);
233
234val PAR1' = store_thm (
235   "PAR1'", ``!P u P' Q.    TRANS P u P' ==> TRANS (par P Q) u (par P' Q)``,
236    PROVE_TAC [PAR1]);
237
238val PAR2' = store_thm (
239   "PAR2'", ``!P u P' Q.    TRANS P u P' ==> TRANS (par Q P) u (par Q P')``,
240    PROVE_TAC [PAR2]);
241
242val PAR3' = store_thm (
243   "PAR3'", ``!P l P' Q P2. TRANS P (label l) P' /\ TRANS Q (label (COMPL l)) Q'
244                ==> TRANS (par P Q) tau (par P' Q')``,
245    PROVE_TAC [PAR3]);
246
247val RESTR' = store_thm (
248   "RESTR'", ``!P u Q l L.   TRANS P u Q /\ ((u = tau) \/
249                                     ((u = label l) /\ l NOTIN L /\ (COMPL l) NOTIN L))
250                ==> TRANS (restr L P) u (restr L Q)``,
251    PROVE_TAC [RESTR]);
252
253val RELABELING' = store_thm (
254   "RELABELING'", ``!P u Q rf.    TRANS P u Q
255                ==> TRANS (relab P rf) (relabel rf u) (relab Q rf)``,
256    PROVE_TAC [RELABELING]);
257
258val REC' = store_thm (
259   "REC'", ``!P u A P'.     TRANS (CCS_Subst P (rec A P) A) u P'
260                ==> TRANS (rec A P) u P'``,
261    PROVE_TAC [REC]);
262
263val _ = export_theory ();
264val _ = html_theory "Example";
265
266open EmitTeX;
267
268(* Emit theory books in TeX *)
269val _ =
270 if (OS.FileSys.isDir "../paper" handle e => false) then
271    let in
272        OS.FileSys.remove "../paper/references.tex" handle e => {};
273        OS.FileSys.remove "../paper/HOLCCS.tex" handle e => {};
274        OS.FileSys.remove "../paper/HOLStrongEQ.tex" handle e => {};
275        OS.FileSys.remove "../paper/HOLStrongLaws.tex" handle e => {};
276        OS.FileSys.remove "../paper/HOLWeakEQ.tex" handle e => {};
277        OS.FileSys.remove "../paper/HOLWeakLaws.tex" handle e => {};
278        OS.FileSys.remove "../paper/HOLObsCongr.tex" handle e => {};
279        OS.FileSys.remove "../paper/HOLObsCongrLaws.tex" handle e => {};
280        OS.FileSys.remove "../paper/HOLCongruence.tex" handle e => {};
281        OS.FileSys.remove "../paper/HOLTrace.tex" handle e => {};
282        OS.FileSys.remove "../paper/HOLCoarsestCongr.tex" handle e => {};
283        OS.FileSys.remove "../paper/HOLBisimulationUpto.tex" handle e => {};
284        OS.FileSys.remove "../paper/HOLExpansion.tex" handle e => {};
285        OS.FileSys.remove "../paper/HOLContraction.tex" handle e => {};
286        OS.FileSys.remove "../paper/HOLUniqueSolutions.tex" handle e => {};
287
288        EmitTeX.print_theories_as_tex_doc
289            ["CCS",
290             "StrongEQ",
291             "StrongLaws",
292             "WeakEQ",
293             "WeakLaws",
294             "ObsCongr",
295             "ObsCongrLaws",
296             "Congruence",
297             "CoarsestCongr",
298             "BisimulationUpto",
299             "Trace",
300             "Expansion",
301             "Contraction",
302             "UniqueSolutions"]
303            "../paper/references"
304    end
305 else
306    {};
307
308(* last updated: Oct 15, 2017 *)
309