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