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