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