1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6open HolKernel Parse boolLib bossLib; 7 8open pred_setTheory relationTheory optionTheory listTheory finite_mapTheory; 9open CCSLib; 10 11val _ = new_theory "CCS"; 12val _ = temp_loose_equality (); 13 14(******************************************************************************) 15(* *) 16(* Labels and Actions *) 17(* *) 18(******************************************************************************) 19 20(* Define the set of labels as the union of names (`in`) (strings) and 21 co-names (`out`) (complement of names) *) 22val _ = Datatype `Label = name 'b | coname 'b`; 23 24(* Define structural induction on labels 25 |- ���P. (���s. P (name s)) ��� (���s. P (coname s)) ��� ���L. P L 26 *) 27val Label_induction = TypeBase.induction_of ``:'b Label``; 28 29(* The structural cases theorem for the type Label 30 |- ���LL. (���s. LL = name s) ��� ���s. LL = coname s 31 *) 32val Label_nchotomy = TypeBase.nchotomy_of ``:'b Label``; 33 34(* The distinction and injectivity theorems for the type Label 35 |- ���a' a. name a ��� coname a' 36 |- (���a a'. (name a = name a') ��� (a = a')) ��� 37 ���a a'. (coname a = coname a') ��� (a = a') 38 *) 39val Label_distinct = TypeBase.distinct_of ``:'b Label``; 40val Label_distinct' = save_thm ("Label_distinct'", GSYM Label_distinct); 41 42val Label_not_eq = save_thm ( 43 "Label_not_eq", STRIP_FORALL_RULE EQF_INTRO Label_distinct); 44 45val Label_not_eq' = save_thm ( 46 "Label_not_eq'", STRIP_FORALL_RULE 47 (PURE_REWRITE_RULE [SYM_CONV ``name s = coname s'``]) 48 Label_not_eq); 49 50val Label_11 = TypeBase.one_one_of ``:'b Label``; 51 52(* NEW: define the set of actions as the OPTION of Label *) 53val _ = type_abbrev ("Action", ``:'b Label option``); 54 55val _ = overload_on ("tau", ``NONE :'b Action``); 56val _ = overload_on ("label", ``SOME :'b Label -> 'b Action``); 57 58val _ = Unicode.unicode_version { u = UnicodeChars.tau, tmnm = "tau"}; 59val _ = TeX_notation { hol = "tau", TeX = ("\\ensuremath{\\tau}", 1) }; 60 61(* The compact representation for (visible) input and output actions, suggested by Michael Norrish *) 62val _ = overload_on ("In", ``\a. label (name a)``); 63val _ = overload_on ("Out", ``\a. label (coname a)``); 64 65(* Define structural induction on actions 66 |- ���P. P tau ��� (���L. P (label L)) ��� ���A. P A 67 *) 68val Action_induction = save_thm ( 69 "Action_induction", INST_TYPE [``:'a`` |-> ``:'b Label``] option_induction); 70 71(* The structural cases theorem for the type Action 72 |- ���AA. (AA = tau) ��� ���L. AA = label L 73 *) 74val Action_nchotomy = save_thm ( 75 "Action_nchotomy", INST_TYPE [``:'a`` |-> ``:'b Label``] option_nchotomy); 76 77(* The distinction and injectivity theorems for the type Action 78 |- ���a. tau ��� label a 79 |- ���a a'. (label a = label a') ��� (a = a') 80 *) 81val Action_distinct = save_thm ( 82 "Action_distinct", INST_TYPE [``:'a`` |-> ``:'b Label``] NOT_NONE_SOME); 83 84val Action_distinct_label = save_thm ( 85 "Action_distinct_label", INST_TYPE [``:'a`` |-> ``:'b Label``] NOT_SOME_NONE); 86 87val Action_11 = save_thm ( 88 "Action_11", INST_TYPE [``:'a`` |-> ``:'b Label``] SOME_11); 89 90(* |- ���A. A ��� tau ��� ���L. A = label L *) 91val Action_no_tau_is_Label = save_thm ( 92 "Action_no_tau_is_Label", 93 Q.GEN `A` (DISJ_IMP (Q.SPEC `A` Action_nchotomy))); 94 95(* Extract the label from a visible action, LABEL: Action -> Label. *) 96val _ = overload_on ("LABEL", ``THE :'b Label option -> 'b Label``); 97val LABEL_def = save_thm ( 98 "LABEL_def", INST_TYPE [``:'a`` |-> ``:'b Label``] THE_DEF); 99 100val IS_LABEL_def = save_thm ( 101 "IS_LABEL_def", INST_TYPE [``:'a`` |-> ``:'b Label``] IS_SOME_DEF); 102val _ = export_rewrites ["LABEL_def", "IS_LABEL_def"]; 103 104(* Define the complement of a label, COMPL: Label -> Label. *) 105val COMPL_LAB_def = Define `(COMPL_LAB (name (s :'b)) = (coname s)) /\ 106 (COMPL_LAB (coname s) = (name s))`; 107 108val _ = overload_on ("COMPL", ``COMPL_LAB``); 109val _ = export_rewrites ["COMPL_LAB_def"]; 110 111val coname_COMPL = store_thm ("coname_COMPL", 112 ``!(s :'b). coname s = COMPL (name s)``, 113 REWRITE_TAC [COMPL_LAB_def]); 114 115val COMPL_COMPL_LAB = store_thm ( 116 "COMPL_COMPL_LAB", ``!(l :'b Label). COMPL_LAB (COMPL_LAB l) = l``, 117 Induct >> REWRITE_TAC [COMPL_LAB_def]); 118 119(* Extend the complement to actions, COMPL_ACT: Action -> Action. *) 120val COMPL_ACT_def = Define ` 121 (COMPL_ACT (label (l: 'b Label)) = label (COMPL l)) /\ 122 (COMPL_ACT tau = tau)`; 123 124val _ = overload_on ("COMPL", ``COMPL_ACT``); 125val _ = export_rewrites ["COMPL_ACT_def"]; 126 127val COMPL_COMPL_ACT = store_thm ( 128 "COMPL_COMPL_ACT", ``!(a :'b Action). COMPL_ACT (COMPL_ACT a) = a``, 129 Induct 130 >| [ REWRITE_TAC [COMPL_ACT_def], 131 REWRITE_TAC [COMPL_ACT_def, COMPL_COMPL_LAB] ]); 132 133(* Auxiliary theorem about complementary labels. *) 134val COMPL_THM = store_thm ("COMPL_THM", 135 ``!(l :'b Label) s. (~(l = name s) ==> ~(COMPL l = coname s)) /\ 136 (~(l = coname s) ==> ~(COMPL l = name s))``, 137 Induct_on `l` 138 >| [ (* case 1 *) 139 rpt GEN_TAC >> CONJ_TAC >| 140 [ REWRITE_TAC [Label_11, COMPL_LAB_def], 141 REWRITE_TAC [Label_distinct, COMPL_LAB_def, Label_distinct'] ] , 142 (* case 2 *) 143 rpt GEN_TAC >> CONJ_TAC >| 144 [ REWRITE_TAC [Label_distinct, COMPL_LAB_def, Label_distinct'], 145 REWRITE_TAC [Label_11, COMPL_LAB_def] ] ]); 146 147val Is_Relabeling_def = Define ` 148 Is_Relabeling (f: 'b Label -> 'b Label) = (!s. f (coname s) = COMPL (f (name s)))`; 149 150val EXISTS_Relabeling = store_thm ("EXISTS_Relabeling", 151 ``?(f: 'b Label -> 'b Label). Is_Relabeling f``, 152 Q.EXISTS_TAC `\a. a` 153 >> PURE_ONCE_REWRITE_TAC [Is_Relabeling_def] 154 >> BETA_TAC 155 >> REWRITE_TAC [COMPL_LAB_def]); 156 157(* Relabeling_TY_DEF = 158 |- ���rep. TYPE_DEFINITION Is_Relabeling rep 159 *) 160val Relabeling_TY_DEF = new_type_definition ("Relabeling", EXISTS_Relabeling); 161 162(* Relabeling_ISO_DEF = 163 |- (���a. ABS_Relabeling (REP_Relabeling a) = a) ��� 164 ���r. Is_Relabeling r ��� (REP_Relabeling (ABS_Relabeling r) = r) 165 *) 166val Relabeling_ISO_DEF = define_new_type_bijections 167 { ABS = "ABS_Relabeling", 168 REP = "REP_Relabeling", 169 name = "Relabeling_ISO_DEF", 170 tyax = Relabeling_TY_DEF }; 171 172(* ABS_Relabeling_one_one = 173 |- ���r r'. 174 Is_Relabeling r ��� Is_Relabeling r' ��� 175 ((ABS_Relabeling r = ABS_Relabeling r') ��� (r = r')) 176 177 ABS_Relabeling_onto = 178 |- ���a. ���r. (a = ABS_Relabeling r) ��� Is_Relabeling r 179 180 REP_Relabeling_one_one = 181 |- ���a a'. (REP_Relabeling a = REP_Relabeling a') ��� (a = a') 182 183 REP_Relabeling_onto = 184 |- ���r. Is_Relabeling r ��� ���a. r = REP_Relabeling a 185 *) 186val [ABS_Relabeling_one_one, 187 ABS_Relabeling_onto, 188 REP_Relabeling_one_one, 189 REP_Relabeling_onto] = 190 map (fn f => f Relabeling_ISO_DEF) 191 [prove_abs_fn_one_one, 192 prove_abs_fn_onto, 193 prove_rep_fn_one_one, 194 prove_rep_fn_onto]; 195 196val REP_Relabeling_THM = store_thm ("REP_Relabeling_THM", 197 ``!rf :'b Relabeling. Is_Relabeling (REP_Relabeling rf)``, 198 GEN_TAC 199 >> REWRITE_TAC [REP_Relabeling_onto] 200 >> EXISTS_TAC ``rf :'b Relabeling`` 201 >> REWRITE_TAC []); 202 203(* Relabeling labels is extended to actions by renaming tau as tau. *) 204val relabel_def = Define `(relabel (rf :'b Relabeling) tau = tau) /\ 205 (relabel rf (label l) = label (REP_Relabeling rf l))`; 206 207(* If the renaming of an action is a label, that action is a label. *) 208val Relab_label = store_thm ("Relab_label", 209 ``!(rf :'b Relabeling) u l. (relabel rf u = label l) ==> ?l'. u = label l'``, 210 Induct_on `u` 211 >- REWRITE_TAC [relabel_def, Action_distinct] 212 >> REWRITE_TAC [relabel_def] 213 >> rpt STRIP_TAC 214 >> EXISTS_TAC ``a :'b Label`` 215 >> REWRITE_TAC []); 216 217(* If the renaming of an action is tau, that action is tau. *) 218val Relab_tau = store_thm ("Relab_tau", 219 ``!(rf :'b Relabeling) u. (relabel rf u = tau) ==> (u = tau)``, 220 Induct_on `u` 221 >> REWRITE_TAC [relabel_def, Action_distinct_label]); 222 223(* Apply_Relab: ((Label # Label) list) -> Label -> Label 224 (SND of any pair is a name, FST can be either name or coname) 225 *) 226val Apply_Relab_def = Define ` 227 (Apply_Relab ([]: ('b Label # 'b Label) list) l = l) /\ 228 (Apply_Relab (CONS (newold: 'b Label # 'b Label) ls) l = 229 if (SND newold = l) then (FST newold) 230 else if (COMPL (SND newold) = l) then (COMPL (FST newold)) 231 else (Apply_Relab ls l))`; 232 233val Apply_Relab_COMPL_THM = store_thm ("Apply_Relab_COMPL_THM", 234 ``!labl (s: 'b). Apply_Relab labl (coname s) = COMPL (Apply_Relab labl (name s))``, 235 Induct 236 >- REWRITE_TAC [Apply_Relab_def, COMPL_LAB_def] 237 >> rpt GEN_TAC 238 >> REWRITE_TAC [Apply_Relab_def] 239 >> COND_CASES_TAC 240 >- art [Label_distinct', COMPL_LAB_def, COMPL_COMPL_LAB] 241 >> ASM_CASES_TAC ``SND (h :'b Label # 'b Label) = name s`` 242 >- art [COMPL_LAB_def] 243 >> IMP_RES_TAC COMPL_THM 244 >> art []); 245 246val IS_RELABELING = store_thm ( 247 "IS_RELABELING", 248 ``!labl :('b Label # 'b Label) list. Is_Relabeling (Apply_Relab labl)``, 249 Induct 250 >- REWRITE_TAC [Is_Relabeling_def, Apply_Relab_def, COMPL_LAB_def] 251 >> GEN_TAC 252 >> REWRITE_TAC [Is_Relabeling_def, Apply_Relab_def] 253 >> GEN_TAC 254 >> COND_CASES_TAC 255 >- art [Label_distinct', COMPL_LAB_def, COMPL_COMPL_LAB] 256 >> ASM_CASES_TAC ``SND (h :'b Label # 'b Label) = name s`` 257 >- art [COMPL_LAB_def] 258 >> IMP_RES_TAC COMPL_THM 259 >> art [Apply_Relab_COMPL_THM]); 260 261(* Defining a relabelling function through substitution-like notation. 262 RELAB: (Label # Label) list -> Relabeling 263 *) 264val RELAB_def = Define ` 265 RELAB (labl :('b Label # 'b Label) list) = ABS_Relabeling (Apply_Relab labl)`; 266 267(* |- ���labl' labl. 268 (RELAB labl' = RELAB labl) ��� (Apply_Relab labl' = Apply_Relab labl) 269 *) 270val APPLY_RELAB_THM = save_thm ("APPLY_RELAB_THM", 271 Q_GENL [`labl'`, `labl`] 272 (REWRITE_RULE [GSYM RELAB_def] 273 (MATCH_MP (MATCH_MP ABS_Relabeling_one_one 274 (Q.SPEC `labl` IS_RELABELING)) 275 (Q.SPEC `labl` IS_RELABELING)))); 276 277(******************************************************************************) 278(* *) 279(* Syntax of pure CCS ('a, 'b) (general formalization) *) 280(* *) 281(******************************************************************************) 282 283(* Define the type of (pure) CCS agent expressions. *) 284val _ = Datatype `CCS = nil 285 | var 'a 286 | prefix ('b Action) CCS 287 | sum CCS CCS 288 | par CCS CCS 289 | restr (('b Label) set) CCS 290 | relab CCS ('b Relabeling) 291 | rec 'a CCS `; 292 293(* compact representation for single-action restriction *) 294val _ = overload_on ("nu", ``\(n :'b) P. restr {name n} P``); 295val _ = overload_on ("nu", ``restr``); 296val _ = Unicode.unicode_version { u = UnicodeChars.nu, tmnm = "nu" }; 297val _ = TeX_notation { hol = "nu", 298 TeX = ("\\ensuremath{\\nu}", 1) }; 299 300val _ = overload_on ("+", ``sum``); (* priority: 500 *) 301val _ = TeX_notation { hol = "+", 302 TeX = ("\\ensuremath{+}", 1) }; 303 304val _ = set_mapped_fixity { fixity = Infix(LEFT, 600), tok = "||", term_name = "par" }; 305val _ = TeX_notation { hol = "||", 306 TeX = ("\\ensuremath{\\parallel}", 1) }; 307val _ = 308 add_rule { term_name = "prefix", fixity = Infix(RIGHT, 700), 309 pp_elements = [ BreakSpace(0,0), TOK "..", BreakSpace(0,0) ], 310 paren_style = OnlyIfNecessary, 311 block_style = (AroundSamePrec, (PP.CONSISTENT, 0)) }; 312 313(* Define structural induction on CCS agent expressions. *) 314val CCS_induct = TypeBase.induction_of ``:('a, 'b) CCS``; 315 316(* The structural cases theorem for the type CCS. *) 317val CCS_cases = TypeBase.nchotomy_of ``:('a, 'b) CCS``; 318 319(* Prove that the constructors of the type CCS are distinct. *) 320val CCS_distinct = TypeBase.distinct_of ``:('a, 'b) CCS``; 321 322(* size definition *) 323val (CCS_size_tm, CCS_size_def) = TypeBase.size_of ``:('a, 'b) CCS``; 324 325local 326 val thm = CONJUNCTS CCS_distinct; 327 val CCS_distinct_LIST = thm @ (map GSYM thm); 328in 329 val CCS_distinct' = save_thm ("CCS_distinct'", LIST_CONJ CCS_distinct_LIST); 330end 331 332(* Prove that the constructors of the type CCS are one-to-one. *) 333val CCS_11 = TypeBase.one_one_of ``:('a, 'b) CCS``; 334 335(* Given any agent expression, define the substitution of an agent expression 336 E' for an agent variable X. 337 338 This works under the hypothesis that the Barendregt convention holds. *) 339val CCS_Subst_def = Define ` 340 (CCS_Subst nil E' X = nil) /\ 341 (CCS_Subst (prefix u E) E' X = prefix u (CCS_Subst E E' X)) /\ 342 (CCS_Subst (sum E1 E2) E' X = sum (CCS_Subst E1 E' X) 343 (CCS_Subst E2 E' X)) /\ 344 (CCS_Subst (par E1 E2) E' X = par (CCS_Subst E1 E' X) 345 (CCS_Subst E2 E' X)) /\ 346 (CCS_Subst (restr L E) E' X = restr L (CCS_Subst E E' X)) /\ 347 (CCS_Subst (relab E f) E' X = relab (CCS_Subst E E' X) f) /\ 348 (CCS_Subst (var Y) E' X = if (Y = X) then E' else (var Y)) /\ 349 (CCS_Subst (rec Y E) E' X = if (Y = X) then (rec Y E) 350 else (rec Y (CCS_Subst E E' X)))`; 351 352(* Note that in the rec clause, if Y = X then all occurrences of Y in E are X 353 and bound, so there exist no free variables X in E to be replaced with E'. 354 Hence, the term rec Y E is returned. 355 356 Below are two typical cases by CCS_Subst: *) 357 358(* |- ���X E E'. CCS_Subst (rec X E) E' X = rec X E (1st fixed point of CCS_Subst) *) 359val CCS_Subst_rec = save_thm ( 360 "CCS_Subst_rec", Q_GENL [`X`, `E`, `E'`] 361 (REWRITE_CONV [CCS_Subst_def] ``CCS_Subst (rec X E) E' X``)); 362 363(* |- ���X E. CCS_Subst (var X) E X = E (2nd fixed point of CCS_Subst) *) 364val CCS_Subst_var = save_thm ( 365 "CCS_Subst_var", Q_GENL [`X`, `E`] 366 (REWRITE_CONV [CCS_Subst_def] ``CCS_Subst (var X) E X``)); 367 368(* |- !t1 t2. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2) *) 369val CCS_COND_CLAUSES = save_thm ( 370 "CCS_COND_CLAUSES", INST_TYPE [``:'a`` |-> ``:('a, 'b) CCS``] COND_CLAUSES); 371 372(******************************************************************************) 373(* *) 374(* Definition of the transition relation for pure CCS *) 375(* *) 376(******************************************************************************) 377 378val _ = type_abbrev ("transition", 379 ``:('a, 'b) CCS -> 'b Action -> ('a, 'b) CCS -> bool``); 380 381(* Inductive definition of the transition relation TRANS for CCS. 382 TRANS: CCS -> Action -> CCS -> bool 383 384 NOTE: noticed that, the theorem TRANS_ind is never needed, thus even we define 385 TRANS co-inductively (i.e. by Hol_coreln), the whole formalization still works. 386 *) 387val (TRANS_rules, TRANS_ind, TRANS_cases) = Hol_reln ` 388 (!E u. TRANS (prefix u E) u E) /\ (* PREFIX *) 389 (!E u E1 E'. TRANS E u E1 ==> TRANS (sum E E') u E1) /\ (* SUM1 *) 390 (!E u E1 E'. TRANS E u E1 ==> TRANS (sum E' E) u E1) /\ (* SUM2 *) 391 (!E u E1 E'. TRANS E u E1 ==> TRANS (par E E') u (par E1 E')) /\ (* PAR1 *) 392 (!E u E1 E'. TRANS E u E1 ==> TRANS (par E' E) u (par E' E1)) /\ (* PAR2 *) 393 (!E l E1 E' E2. TRANS E (label l) E1 /\ TRANS E' (label (COMPL l)) E2 394 ==> TRANS (par E E') tau (par E1 E2)) /\ (* PAR3 *) 395 (!E u E' l L. TRANS E u E' /\ ((u = tau) \/ 396 ((u = label l) /\ l NOTIN L /\ (COMPL l) NOTIN L)) 397 ==> TRANS (restr L E) u (restr L E')) /\ (* RESTR *) 398 (!E u E' rf. TRANS E u E' 399 ==> TRANS (relab E rf) (relabel rf u) (relab E' rf)) /\ (* RELABELING *) 400 (!E u X E1. TRANS (CCS_Subst E (rec X E) X) u E1 401 ==> TRANS (rec X E) u E1) `; (* REC *) 402 403val _ = 404 add_rule { term_name = "TRANS", fixity = Infix (NONASSOC, 450), 405 pp_elements = [ BreakSpace(1,0), TOK "--", HardSpace 0, TM, HardSpace 0, TOK "->", 406 BreakSpace(1,0) ], 407 paren_style = OnlyIfNecessary, 408 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) }; 409 410val _ = TeX_notation { hol = "--", TeX = ("\\HOLTokenTransBegin", 1) }; 411val _ = TeX_notation { hol = "->", TeX = ("\\HOLTokenTransEnd", 1) }; 412 413(* The rules for the transition relation TRANS as individual theorems. *) 414val [PREFIX, SUM1, SUM2, PAR1, PAR2, PAR3, RESTR, RELABELING, REC] = 415 map save_thm 416 (combine (["PREFIX", "SUM1", "SUM2", "PAR1", "PAR2", "PAR3", "RESTR", 417 "RELABELING", "REC"], 418 CONJUNCTS TRANS_rules)); 419 420(* The process nil has no transitions. 421 |- ���u E. ��TRANS nil u E 422 *) 423val NIL_NO_TRANS = save_thm ("NIL_NO_TRANS", 424 Q_GENL [`u`, `E`] 425 (REWRITE_RULE [CCS_distinct] 426 (SPECL [``nil``, ``u :'b Action``, ``E :('a, 'b) CCS``] TRANS_cases))); 427 428(* |- ���u E. nil --u-> E ��� F *) 429val NIL_NO_TRANS_EQF = save_thm ( 430 "NIL_NO_TRANS_EQF", 431 Q_GENL [`u`, `E`] (EQF_INTRO (SPEC_ALL NIL_NO_TRANS))); 432 433(* Prove that if a process can do an action, then the process is not nil. 434 |- ���E u E'. TRANS E u E' ��� E ��� nil: 435 *) 436val TRANS_IMP_NO_NIL = store_thm ("TRANS_IMP_NO_NIL", 437 ``!E u E'. TRANS E u E' ==> ~(E = nil)``, 438 rpt GEN_TAC 439 >> ONCE_REWRITE_TAC [TRANS_cases] 440 >> rpt STRIP_TAC 441 >> PROVE_TAC [CCS_distinct']); 442 443(* Above proof could be easier using TRANS_ind for the only time in this project 444val TRANS_IMP_NO_NIL' = store_thm ("TRANS_IMP_NO_NIL'", 445 ``!E u E'. TRANS E u E' ==> ~(E = nil)``, 446 HO_MATCH_MP_TAC TRANS_ind 447 >> REWRITE_TAC [CCS_distinct']); 448 *) 449 450(* An agent variable has no transitions. 451 |- !X u E'. ~TRANS (var X) u E' 452 *) 453val VAR_NO_TRANS = save_thm ("VAR_NO_TRANS", 454 Q_GENL [`X`, `u`, `E`] 455 (REWRITE_RULE [CCS_distinct', CCS_11] 456 (Q.SPECL [`var X`, `u`, `E`] TRANS_cases))); 457 458(* |- !u E u' E'. TRANS (prefix u E) u' E' = (u' = u) /\ (E' = E) *) 459val TRANS_PREFIX_EQ = save_thm ( 460 "TRANS_PREFIX_EQ", 461 ((Q_GENL [`u`, `E`, `u'`, `E'`]) o 462 (ONCE_REWRITE_RHS_RULE [EQ_SYM_EQ]) o 463 SPEC_ALL o 464 (REWRITE_RULE [CCS_distinct', CCS_11])) 465 (SPECL [``prefix (u :'b Action) E``, ``u' :'b Action``, ``E' :('a, 'b) CCS``] 466 TRANS_cases)); 467 468(* |- ���u E u' E'. u..E --u'-> E' ��� (u' = u) ��� (E' = E) *) 469val TRANS_PREFIX = save_thm ( 470 "TRANS_PREFIX", EQ_IMP_LR TRANS_PREFIX_EQ); 471 472(******************************************************************************) 473(* *) 474(* The transitions of a binary summation *) 475(* *) 476(******************************************************************************) 477 478val SUM_cases_EQ = save_thm ( 479 "SUM_cases_EQ", 480 Q_GENL [`D`, `D'`, `u`, `D''`] 481 (REWRITE_RULE [CCS_distinct', CCS_11] 482 (SPECL [``sum D D'``, ``u :'b Action``, ``D'' :('a, 'b) CCS``] 483 TRANS_cases))); 484 485val SUM_cases = save_thm ( 486 "SUM_cases", EQ_IMP_LR SUM_cases_EQ); 487 488val TRANS_SUM_EQ = store_thm ("TRANS_SUM_EQ", 489 ``!E E' u E''. TRANS (sum E E') u E'' = TRANS E u E'' \/ TRANS E' u E''``, 490 rpt GEN_TAC 491 >> EQ_TAC (* 2 sub-goals here *) 492 >| [ (* goal 1 (of 2) *) 493 DISCH_TAC \\ 494 IMP_RES_TAC SUM_cases >> art [], 495 (* goal 2 (of 2) *) 496 STRIP_TAC >| (* 2 sub-goals here *) 497 [ MATCH_MP_TAC SUM1 >> art [], 498 MATCH_MP_TAC SUM2 >> art [] ] ]); 499 500(* for CCS_TRANS_CONV *) 501val TRANS_SUM_EQ' = store_thm ( 502 "TRANS_SUM_EQ'", 503 ``!E1 E2 u E. TRANS (sum E1 E2) u E = TRANS E1 u E \/ TRANS E2 u E``, 504 REWRITE_TAC [TRANS_SUM_EQ]); 505 506val TRANS_SUM = save_thm ( 507 "TRANS_SUM", EQ_IMP_LR TRANS_SUM_EQ); 508 509val TRANS_COMM_EQ = store_thm ("TRANS_COMM_EQ", 510 ``!E E' E'' u. TRANS (sum E E') u E'' = TRANS (sum E' E) u E''``, 511 rpt GEN_TAC 512 >> EQ_TAC (* 2 sub-goals here *) 513 >| [ (* goal 1 (of 2) *) 514 DISCH_TAC \\ 515 IMP_RES_TAC TRANS_SUM >| 516 [ MATCH_MP_TAC SUM2, MATCH_MP_TAC SUM1 ] \\ 517 art [], 518 (* goal 2 (of 2) *) 519 DISCH_TAC \\ 520 IMP_RES_TAC TRANS_SUM >| 521 [ MATCH_MP_TAC SUM2, MATCH_MP_TAC SUM1 ] \\ 522 art [] ]); 523 524val TRANS_ASSOC_EQ = store_thm ("TRANS_ASSOC_EQ", 525 ``!E E' E'' E1 u. TRANS (sum (sum E E') E'') u E1 = TRANS (sum E (sum E' E'')) u E1``, 526 rpt GEN_TAC 527 >> EQ_TAC 528 >| [ (* goal 1 (of 2) *) 529 DISCH_TAC \\ 530 IMP_RES_TAC TRANS_SUM >| 531 [ (* goal 1.1 (of 2) *) 532 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *) 533 [ MATCH_MP_TAC SUM1, 534 MATCH_MP_TAC SUM1, 535 MATCH_MP_TAC SUM2 >> MATCH_MP_TAC SUM1, 536 MATCH_MP_TAC SUM2 >> MATCH_MP_TAC SUM1 ] \\ 537 art [], 538 (* goal 1.2 (of 2) *) 539 MATCH_MP_TAC SUM2 >> MATCH_MP_TAC SUM2 \\ 540 art [] ], 541 (* goal 2 (of 2) *) 542 DISCH_TAC \\ 543 IMP_RES_TAC TRANS_SUM >| 544 [ MATCH_MP_TAC SUM1 >> MATCH_MP_TAC SUM1 \\ 545 art [], 546 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *) 547 [ MATCH_MP_TAC SUM1 >> MATCH_MP_TAC SUM1, 548 MATCH_MP_TAC SUM1 >> MATCH_MP_TAC SUM2, 549 MATCH_MP_TAC SUM2, 550 MATCH_MP_TAC SUM2 ] >> art [] ] ]); 551 552val TRANS_ASSOC_RL = save_thm ( 553 "TRANS_ASSOC_RL", EQ_IMP_RL TRANS_ASSOC_EQ); 554 555val TRANS_SUM_NIL_EQ = store_thm ( 556 "TRANS_SUM_NIL_EQ", 557 ``!E u E'. TRANS (sum E nil) u E' = TRANS E u E'``, 558 rpt GEN_TAC 559 >> EQ_TAC (* 2 sub-goals here *) 560 >| [ (* goal 1 (of 2) *) 561 DISCH_TAC \\ 562 IMP_RES_TAC TRANS_SUM \\ 563 IMP_RES_TAC NIL_NO_TRANS, 564 (* goal 2 (of 2) *) 565 DISCH_TAC \\ 566 MATCH_MP_TAC SUM1 >> art [] ]); 567 568(* |- ���E u E'. E + nil --u-> E' ��� E --u-> E' *) 569val TRANS_SUM_NIL = save_thm ("TRANS_SUM_NIL", EQ_IMP_LR TRANS_SUM_NIL_EQ); 570 571val TRANS_P_SUM_P_EQ = store_thm ("TRANS_P_SUM_P_EQ", 572 ``!E u E'. TRANS (sum E E) u E' = TRANS E u E'``, 573 rpt GEN_TAC 574 >> EQ_TAC 575 >| [ DISCH_TAC \\ 576 IMP_RES_TAC TRANS_SUM, 577 DISCH_TAC \\ 578 MATCH_MP_TAC SUM1 >> art [] ]); 579 580val TRANS_P_SUM_P = save_thm ("TRANS_P_SUM_P", EQ_IMP_LR TRANS_P_SUM_P_EQ); 581 582val PAR_cases_EQ = save_thm ("PAR_cases_EQ", 583 Q_GENL [`D`, `D'`, `u`, `D''`] 584 (REWRITE_RULE [CCS_distinct', CCS_11] 585 (Q.SPECL [`par D D'`, `u`, `D''`] TRANS_cases))); 586 587val PAR_cases = save_thm ("PAR_cases", EQ_IMP_LR PAR_cases_EQ); 588 589(* NOTE: the shape of this theorem can be easily got from above definition by replacing 590 REWRITE_RULE to SIMP_RULE, however the inner existential variable (E1) has a 591 different name. *) 592val TRANS_PAR_EQ = store_thm ("TRANS_PAR_EQ", 593 ``!E E' u E''. TRANS (par E E') u E'' = 594 (?E1. (E'' = par E1 E') /\ TRANS E u E1) \/ 595 (?E1. (E'' = par E E1) /\ TRANS E' u E1) \/ 596 (?E1 E2 l. (u = tau) /\ (E'' = par E1 E2) /\ 597 TRANS E (label l) E1 /\ TRANS E' (label (COMPL l)) E2)``, 598 rpt GEN_TAC 599 >> EQ_TAC (* 2 sub-goals here *) 600 >| [ (* case 1 (LR) *) 601 STRIP_TAC \\ 602 IMP_RES_TAC PAR_cases >| (* 3 sub-goals here *) 603 [ (* goal 1.1 *) 604 DISJ1_TAC \\ 605 Q.EXISTS_TAC `E1` >> art [], 606 (* goal 1.2 *) 607 DISJ2_TAC \\ 608 DISJ1_TAC \\ 609 Q.EXISTS_TAC `E1` >> art [], 610 (* goal 1.3 *) 611 DISJ2_TAC \\ 612 DISJ2_TAC \\ 613 take [`E1`, `E2`, `l`] >> art [] ], 614 (* case 2 (RL) *) 615 STRIP_TAC (* 3 sub-goals here, but they share the first and last steps *) 616 >> art [] 617 >| [ MATCH_MP_TAC PAR1 >> art [], 618 MATCH_MP_TAC PAR2 >> art [], 619 MATCH_MP_TAC PAR3 \\ 620 Q.EXISTS_TAC `l` >> art [] ] ]); 621 622val TRANS_PAR = save_thm ("TRANS_PAR", EQ_IMP_LR TRANS_PAR_EQ); 623 624val TRANS_PAR_P_NIL = store_thm ("TRANS_PAR_P_NIL", 625 ``!E u E'. TRANS (par E nil) u E' ==> (?E''. TRANS E u E'' /\ (E' = par E'' nil))``, 626 rpt STRIP_TAC 627 >> IMP_RES_TAC TRANS_PAR 628 >| [ Q.EXISTS_TAC `E1` >> art [], 629 IMP_RES_TAC NIL_NO_TRANS, 630 IMP_RES_TAC NIL_NO_TRANS ]); 631 632val TRANS_PAR_NO_SYNCR = store_thm ("TRANS_PAR_NO_SYNCR", 633 ``!(l :'b Label) l'. ~(l = COMPL l') ==> 634 (!E E' E''. ~(TRANS (par (prefix (label l) E) (prefix (label l') E')) tau E''))``, 635 rpt STRIP_TAC 636 >> IMP_RES_TAC TRANS_PAR (* 3 sub-goals here *) 637 >| [ IMP_RES_TAC TRANS_PREFIX >> IMP_RES_TAC Action_distinct, 638 IMP_RES_TAC TRANS_PREFIX >> IMP_RES_TAC Action_distinct, 639 IMP_RES_TAC TRANS_PREFIX >> IMP_RES_TAC Action_11 \\ 640 CHECK_ASSUME_TAC 641 (REWRITE_RULE [SYM (ASSUME ``(l'' :'b Label) = l``), 642 SYM (ASSUME ``COMPL (l'' :'b Label) = l'``), COMPL_COMPL_LAB] 643 (ASSUME ``~(l = COMPL (l' :'b Label))``)) \\ 644 RW_TAC bool_ss [] ]); 645 646val RESTR_cases_EQ = save_thm ( 647 "RESTR_cases_EQ", 648 Q_GENL [`D'`, `u`, `L`, `D`] 649 (REWRITE_RULE [CCS_distinct', CCS_11, Action_distinct, Action_11] 650 (Q.SPECL [`restr L D`, `u`, `D'`] TRANS_cases))); 651 652val RESTR_cases = save_thm ( 653 "RESTR_cases", EQ_IMP_LR RESTR_cases_EQ); 654 655val TRANS_RESTR_EQ = store_thm ("TRANS_RESTR_EQ", 656 ``!E L u E'. 657 TRANS (restr L E) u E' = 658 (?E'' l. (E' = restr L E'') /\ TRANS E u E'' /\ 659 ((u = tau) \/ ((u = label l) /\ ~(l IN L) /\ ~((COMPL l) IN L))))``, 660 let val a1 = ASSUME ``(u :'b Action) = tau`` 661 and a2 = ASSUME ``u = label (l :'b Label)`` 662 and a3 = ASSUME ``TRANS E'' u E'''`` 663 and a4 = ASSUME ``TRANS E u E''`` 664 in 665 rpt GEN_TAC 666 >> EQ_TAC >| (* two goals here *) 667 [ (* case 1 (LR) *) 668 STRIP_TAC \\ 669 IMP_RES_TAC RESTR_cases \\ (* two sub-goals here, first two steps are shared *) 670 Q.EXISTS_TAC `E'''` \\ 671 Q.EXISTS_TAC `l` >| 672 [ (* goal 1.1 *) 673 art [REWRITE_RULE [a1] a3], 674 (* goal 1.2 *) 675 art [REWRITE_RULE [a2] a3] ], 676 (* case 2 (RL) *) 677 STRIP_TAC >| (* two sub-goals here *) 678 [ (* sub-goal 2.1 *) 679 art [] \\ 680 MATCH_MP_TAC RESTR \\ 681 art [REWRITE_RULE [a1] a4], 682 (* sub-goal 2.2 *) 683 art [] \\ 684 MATCH_MP_TAC RESTR \\ 685 Q.EXISTS_TAC `l` \\ 686 art [REWRITE_RULE [a2] a4] ] ] 687 end); 688 689val TRANS_RESTR = save_thm ( 690 "TRANS_RESTR", EQ_IMP_LR TRANS_RESTR_EQ); 691 692val TRANS_P_RESTR = store_thm ( 693 "TRANS_P_RESTR", 694 ``!E u E' L. TRANS (restr L E) u (restr L E') ==> TRANS E u E'``, 695 let 696 val thm = REWRITE_RULE [CCS_11] (ASSUME ``restr (L :'b Label set) E' = restr L E''``) 697 in 698 rpt STRIP_TAC \\ 699 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 700 [ FILTER_ASM_REWRITE_TAC (fn t => not (t = ``(u :'b Action) = tau``)) [thm], 701 FILTER_ASM_REWRITE_TAC (fn t => not (t = ``(u :'b Action) = label l``)) [thm] ] 702 end); 703 704val RESTR_NIL_NO_TRANS = store_thm ("RESTR_NIL_NO_TRANS", 705 ``!(L :'b Label set) u E. ~(TRANS (restr L nil) u E)``, 706 rpt STRIP_TAC 707 >> IMP_RES_TAC TRANS_RESTR (* two sub-goals here, but same proofs *) 708 >> IMP_RES_TAC NIL_NO_TRANS); 709 710val TRANS_IMP_NO_RESTR_NIL = store_thm ("TRANS_IMP_NO_RESTR_NIL", 711 ``!E u E'. TRANS E u E' ==> !L. ~(E = restr L nil)``, 712 rpt STRIP_TAC 713 >> ASSUME_TAC (REWRITE_RULE [ASSUME ``E = restr L nil``] 714 (ASSUME ``TRANS E u E'``)) 715 >> IMP_RES_TAC RESTR_NIL_NO_TRANS); 716 717val TRANS_RESTR_NO_NIL = store_thm ("TRANS_RESTR_NO_NIL", 718 ``!E L u E'. TRANS (restr L E) u (restr L E') ==> ~(E = nil)``, 719 rpt STRIP_TAC 720 >> IMP_RES_TAC TRANS_RESTR 721 >> ASSUME_TAC (REWRITE_RULE [ASSUME ``E = nil``] 722 (ASSUME ``TRANS E u E''``)) 723 >> IMP_RES_TAC NIL_NO_TRANS); 724 725val RESTR_LABEL_NO_TRANS = store_thm ("RESTR_LABEL_NO_TRANS", 726 ``!(l :'b Label) L. (l IN L) \/ ((COMPL l) IN L) ==> 727 (!E u E'. ~(TRANS (restr L (prefix (label l) E)) u E'))``, 728 rpt STRIP_TAC (* 2 goals here *) 729 >| [ (* goal 1 *) 730 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 731 [ (* goal 1.1 *) 732 IMP_RES_TAC TRANS_PREFIX \\ 733 CHECK_ASSUME_TAC 734 (REWRITE_RULE [ASSUME ``(u :'b Action) = tau``, Action_distinct] 735 (ASSUME ``(u :'b Action) = label l``)), 736 (* goal 1.2 *) 737 IMP_RES_TAC TRANS_PREFIX \\ 738 CHECK_ASSUME_TAC 739 (MP (REWRITE_RULE 740 [REWRITE_RULE [ASSUME ``(u :'b Action) = label l'``, Action_11] 741 (ASSUME ``(u :'b Action) = label l``)] 742 (ASSUME ``~((l' :'b Label) IN L)``)) 743 (ASSUME ``(l :'b Label) IN L``)) ], 744 (* goal 2 *) 745 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 746 [ (* goal 2.1 *) 747 IMP_RES_TAC TRANS_PREFIX \\ 748 CHECK_ASSUME_TAC 749 (REWRITE_RULE [ASSUME ``(u :'b Action) = tau``, Action_distinct] 750 (ASSUME ``(u :'b Action) = label l``)), 751 (* goal 2.2 *) 752 IMP_RES_TAC TRANS_PREFIX \\ 753 CHECK_ASSUME_TAC 754 (MP (REWRITE_RULE 755 [REWRITE_RULE [ASSUME ``(u :'b Action) = label l'``, Action_11] 756 (ASSUME ``(u :'b Action) = label l``)] 757 (ASSUME ``~((COMPL (l' :'b Label)) IN L)``)) 758 (ASSUME ``(COMPL (l :'b Label)) IN L``)) ] ]); 759 760val RELAB_cases_EQ = save_thm ("RELAB_cases_EQ", 761 Q_GENL [`E`, `rf`] 762 (REWRITE_RULE [CCS_distinct', CCS_11] (SPEC ``relab E rf`` TRANS_cases))); 763 764val RELAB_cases = save_thm ("RELAB_cases", EQ_IMP_LR RELAB_cases_EQ); 765 766val TRANS_RELAB_EQ = store_thm ("TRANS_RELAB_EQ", 767 ``!E rf u E'. TRANS (relab E rf) u E' = 768 (?u' E''. (u = relabel rf u') /\ 769 (E' = relab E'' rf) /\ TRANS E u' E'')``, 770 rpt GEN_TAC 771 >> EQ_TAC (* 2 sub-goals here *) 772 >| [ (* goal 1 (of 2) *) 773 DISCH_TAC \\ 774 IMP_RES_TAC RELAB_cases \\ 775 take [`u'`, `E'''`] >> art [], 776 (* goal 2 (of 2) *) 777 STRIP_TAC \\ 778 PURE_ONCE_ASM_REWRITE_TAC [] \\ 779 MATCH_MP_TAC RELABELING \\ 780 PURE_ONCE_ASM_REWRITE_TAC [] ]); 781 782val TRANS_RELAB = save_thm ("TRANS_RELAB", EQ_IMP_LR TRANS_RELAB_EQ); 783 784val TRANS_RELAB_labl = save_thm ("TRANS_RELAB_labl", 785 Q_GENL [`E`, `labl`] (Q.SPECL [`E`, `RELAB labl`] TRANS_RELAB)); 786 787val RELAB_NIL_NO_TRANS = store_thm ("RELAB_NIL_NO_TRANS", 788 ``!(rf :'b Relabeling) u E. ~(TRANS (relab nil rf) u E)``, 789 rpt STRIP_TAC 790 >> IMP_RES_TAC TRANS_RELAB 791 >> IMP_RES_TAC NIL_NO_TRANS); 792 793val REC_cases_EQ = save_thm ("REC_cases_EQ", 794 Q_GENL [`X`, `E`, `u`, `E''`] 795 (Q.SPECL [`u`, `E''`] 796 (REWRITE_RULE [CCS_distinct', CCS_11] 797 (SPEC ``rec X E`` TRANS_cases)))); 798 799val REC_cases = save_thm ("REC_cases", EQ_IMP_LR REC_cases_EQ); 800 801val TRANS_REC_EQ = store_thm ("TRANS_REC_EQ", 802 ``!X E u E'. TRANS (rec X E) u E' = TRANS (CCS_Subst E (rec X E) X) u E'``, 803 rpt GEN_TAC 804 >> EQ_TAC 805 >| [ (* goal 1 (of 2) *) 806 PURE_ONCE_REWRITE_TAC [REC_cases_EQ] \\ 807 rpt STRIP_TAC \\ 808 PURE_ASM_REWRITE_TAC [], 809 (* goal 2 (of 2) *) 810 PURE_ONCE_REWRITE_TAC [REC] ]); 811 812val TRANS_REC = save_thm ("TRANS_REC", EQ_IMP_LR TRANS_REC_EQ); 813 814(******************************************************************************) 815(* *) 816(* Variables and Names (Labels) in CCS *) 817(* *) 818(******************************************************************************) 819 820(* ('a, 'b) CCS -> 'a set (set of free variables) *) 821val FV_def = Define ` 822 (FV (nil :('a, 'b) CCS) = (EMPTY :'a set)) /\ 823 (FV (prefix u p) = FV p) /\ 824 (FV (sum p q) = (FV p) UNION (FV q)) /\ 825 (FV (par p q) = (FV p) UNION (FV q)) /\ 826 (FV (restr L p) = FV p) /\ 827 (FV (relab p rf) = FV p) /\ 828 (FV (var X) = {X}) /\ 829 (FV (rec X p) = (FV p) DIFF {X}) `; 830 831(* ('a, 'b) CCS -> 'a set (set of bound variables) *) 832val BV_def = Define ` 833 (BV (nil :('a, 'b) CCS) = (EMPTY :'a set)) /\ 834 (BV (prefix u p) = BV p) /\ 835 (BV (sum p q) = (BV p) UNION (BV q)) /\ 836 (BV (par p q) = (BV p) UNION (BV q)) /\ 837 (BV (restr L p) = BV p) /\ 838 (BV (relab p rf) = BV p) /\ 839 (BV (var X) = EMPTY) /\ 840 (BV (rec X p) = X INSERT (BV p)) `; 841 842val IS_PROC_def = Define ` 843 IS_PROC E = (FV E = EMPTY)`; 844 845val ALL_PROC_def = Define ` 846 ALL_PROC ES = EVERY IS_PROC ES`; 847 848(* The use of finite_mapTheory (to get rid of substitution orders) is 849 suggested by Konrad Slind. *) 850val CCS_Subst1_def = Define ` 851 (CCS_Subst1 nil (fm :'a |-> ('a, 'b) CCS) = nil) /\ 852 (CCS_Subst1 (prefix u E) fm = prefix u (CCS_Subst1 E fm)) /\ 853 (CCS_Subst1 (sum E1 E2) fm = sum (CCS_Subst1 E1 fm) 854 (CCS_Subst1 E2 fm)) /\ 855 (CCS_Subst1 (par E1 E2) fm = par (CCS_Subst1 E1 fm) 856 (CCS_Subst1 E2 fm)) /\ 857 (CCS_Subst1 (restr L E) fm = restr L (CCS_Subst1 E fm)) /\ 858 (CCS_Subst1 (relab E rf) fm = relab (CCS_Subst1 E fm) rf) /\ 859 (CCS_Subst1 (var Y) fm = if (Y IN FDOM fm) then (FAPPLY fm Y) 860 else (var Y)) /\ 861 (CCS_Subst1 (rec Y E) fm = if (Y IN FDOM fm) then (rec Y E) 862 else (rec Y (CCS_Subst1 E fm)))`; 863 864(* :('a, 'b) CCS list -> ('a |-> ('a, 'b) CCS) -> ('a, 'b) CCS list *) 865val CCS_Subst2_def = Define ` 866 CCS_Subst2 ES fm = MAP (\e. CCS_Subst1 e fm) ES`; 867 868val DELETE_ELEMENT_def = Define ` 869 (DELETE_ELEMENT e [] = []) /\ 870 (DELETE_ELEMENT e (x :: l) = 871 if (e = x) then DELETE_ELEMENT e l else x :: DELETE_ELEMENT e l)`; 872 873val NOT_IN_DELETE_ELEMENT = store_thm ( 874 "NOT_IN_DELETE_ELEMENT", 875 ``!e L. ~MEM e (DELETE_ELEMENT e L)``, 876 GEN_TAC >> Induct_on `L` 877 >- REWRITE_TAC [DELETE_ELEMENT_def, MEM] 878 >> GEN_TAC >> REWRITE_TAC [DELETE_ELEMENT_def] 879 >> Cases_on `e = h` >> fs []); 880 881val DELETE_ELEMENT_FILTER = store_thm ( 882 "DELETE_ELEMENT_FILTER", 883 ``!e L. DELETE_ELEMENT e L = FILTER ((<>) e) L``, 884 GEN_TAC >> Induct_on `L` 885 >- REWRITE_TAC [DELETE_ELEMENT_def, FILTER] 886 >> GEN_TAC >> REWRITE_TAC [DELETE_ELEMENT_def, FILTER] 887 >> Cases_on `e = h` >> fs []); 888 889val LENGTH_DELETE_ELEMENT_LEQ = store_thm ( 890 "LENGTH_DELETE_ELEMENT_LEQ", 891 ``!e L. LENGTH (DELETE_ELEMENT e L) <= LENGTH L``, 892 rpt GEN_TAC 893 >> REWRITE_TAC [DELETE_ELEMENT_FILTER] 894 >> MP_TAC (Q.SPECL [`\y. e <> y`, `\y. T`] LENGTH_FILTER_LEQ_MONO) 895 >> BETA_TAC >> simp [] 896 >> STRIP_TAC 897 >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `L`)) 898 >> Know `FILTER (\y. T) L = L` 899 >- ( KILL_TAC \\ 900 Induct_on `L` >- REWRITE_TAC [FILTER] \\ 901 GEN_TAC >> REWRITE_TAC [FILTER] >> simp [] ) 902 >> DISCH_TAC >> fs []); 903 904val LENGTH_DELETE_ELEMENT_LE = store_thm ( 905 "LENGTH_DELETE_ELEMENT_LE", 906 ``!e L. MEM e L ==> LENGTH (DELETE_ELEMENT e L) < LENGTH L``, 907 rpt GEN_TAC >> Induct_on `L` 908 >- REWRITE_TAC [MEM] 909 >> GEN_TAC >> REWRITE_TAC [MEM, DELETE_ELEMENT_def] 910 >> Cases_on `e = h` >> fs [] 911 >> MP_TAC (Q.SPECL [`h`, `L`] LENGTH_DELETE_ELEMENT_LEQ) 912 >> KILL_TAC >> RW_TAC arith_ss []); 913 914val EVERY_DELETE_ELEMENT = store_thm ( 915 "EVERY_DELETE_ELEMENT", 916 ``!e L P. P e /\ EVERY P (DELETE_ELEMENT e L) ==> EVERY P L``, 917 GEN_TAC >> Induct_on `L` 918 >- RW_TAC std_ss [DELETE_ELEMENT_def] 919 >> rpt GEN_TAC >> REWRITE_TAC [DELETE_ELEMENT_def] 920 >> Cases_on `e = h` >> fs []); 921 922val DELETE_ELEMENT_APPEND = store_thm ( 923 "DELETE_ELEMENT_APPEND", 924 ``!a L L'. DELETE_ELEMENT a (L ++ L') = DELETE_ELEMENT a L ++ DELETE_ELEMENT a L'``, 925 REWRITE_TAC [DELETE_ELEMENT_FILTER] 926 >> REWRITE_TAC [GSYM FILTER_APPEND_DISTRIB]); 927 928(* not used so far, learnt from Robert Beers *) 929val ALL_IDENTICAL_def = Define ` 930 ALL_IDENTICAL t = ?x. !y. MEM y t ==> (y = x)`; 931 932(* 933You might define the sublist relation: (from Michael Norrish) 934Sublist [] l = T 935 Sublist _ [] = F 936 Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist (h1::t1) t2 937 938And show that 939 940 Sublist (DELETE_ELEMENT e l) l 941*) 942 943(* (size :(��, ��) CCS -> num) *) 944val size_def = Define ` 945 size (p :('a, 'b) CCS) = ^CCS_size_tm (\x. 0) (\x. 0) p`; 946 947(* (FN :('a, 'b) CCS -> 'a list -> 'b Label set) *) 948val FN_definition = ` 949 (FN (nil :('a, 'b) CCS) J = (EMPTY :'b Label set)) /\ 950 (FN (prefix (label l) p) J = l INSERT (FN p J)) /\ (* here! *) 951 (FN (prefix tau p) J = FN p J) /\ 952 (FN (sum p q) J = (FN p J) UNION (FN q J)) /\ 953 (FN (par p q) J = (FN p J) UNION (FN q J)) /\ 954 (FN (restr L p) J = (FN p J) DIFF (L UNION (IMAGE COMPL_LAB L))) /\ 955 (FN (relab p rf) J = IMAGE (REP_Relabeling rf) (FN p J)) /\ 956 (FN (var X) J = EMPTY) /\ 957 (FN (rec X p) J = if (MEM X J) then 958 FN (CCS_Subst p (rec X p) X) (DELETE_ELEMENT X J) 959 else EMPTY)`; 960 961(* (BN :('a, 'b) CCS -> 'a list -> 'b Label set) *) 962val BN_definition = ` 963 (BN (nil :('a, 'b) CCS) J = (EMPTY :'b Label set)) /\ 964 (BN (prefix u p) J = BN p J) /\ 965 (BN (sum p q) J = (BN p J) UNION (BN q J)) /\ 966 (BN (par p q) J = (BN p J) UNION (BN q J)) /\ 967 (BN (restr L p) J = (BN p J) UNION L) /\ (* here! *) 968 (BN (relab p rf) J = BN p J) /\ 969 (BN (var X) J = EMPTY) /\ 970 (BN (rec X p) J = if (MEM X J) then 971 FN (CCS_Subst p (rec X p) X) (DELETE_ELEMENT X J) 972 else EMPTY)`; 973 974(* This is how we get the correct tactics (FN_tac): 975 - val FN_defn = Hol_defn "FN" FN_definition; 976 - Defn.tgoal FN_defn; 977 *) 978local 979 val tactic = (* the use of `($< LEX $<)` is learnt from Ramana Kumar *) 980 WF_REL_TAC `inv_image ($< LEX $<) (\x. (LENGTH (SND x), size (FST x)))` 981 >> rpt STRIP_TAC >- ( IMP_RES_TAC LENGTH_DELETE_ELEMENT_LE >> art [] ) 982 >> REWRITE_TAC [size_def, CCS_size_def] 983 >> simp []; 984in 985 val FN_def = TotalDefn.tDefine "FN" FN_definition tactic; 986 val BN_def = TotalDefn.tDefine "BN" BN_definition tactic; 987end; 988 989(* (free_names :('a, 'b) CCS -> 'b Label set) collects all visible labels in the prefix *) 990val free_names_def = Define ` (* also called "sorts" by Robin Milner *) 991 free_names p = FN p (SET_TO_LIST (BV p))`; 992 993(* (bound_names :('a, 'b) CCS -> 'b Label set) collects all visible labels in the restr *) 994val bound_names_def = Define ` 995 bound_names p = BN p (SET_TO_LIST (BV p))`; 996 997val FN_UNIV1 = store_thm ("FN_UNIV1", 998 ``!p. free_names p <> (UNIV :'b Label set) ==> ?a. a NOTIN free_names p``, 999 PROVE_TAC [EQ_UNIV]); 1000 1001val FN_UNIV2 = store_thm ("FN_UNIV2", 1002 ``!p q. free_names p UNION free_names q <> (UNIV :'b Label set) ==> 1003 ?a. a NOTIN free_names p /\ a NOTIN free_names q``, 1004 PROVE_TAC [EQ_UNIV, IN_UNION]); 1005 1006val _ = export_theory (); 1007val _ = html_theory "CCS"; 1008 1009(* last updated: Oct 24, 2017 *) 1010