1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6structure CCSConv :> CCSConv = 7struct 8 9open HolKernel Parse boolLib bossLib; 10open CCSLib CCSTheory CCSSyntax stringTheory; 11 12structure Parse = struct 13 open Parse 14 val (Type, Term) = parse_from_grammars CCSTheory.CCS_grammars 15end 16open Parse 17 18(******************************************************************************) 19(* *) 20(* Conversion for computing the transitions of a pure CCS agent *) 21(* *) 22(******************************************************************************) 23 24(* Source Level Debugging in Poly/ML 25 26 PolyML.Compiler.debug := true; 27 open PolyML.Debug; 28 breakIn "CCS_TRANS_CONV"; 29 30 clearIn "CCS_TRANS_CONV"; 31 32Tracing program execution 33 34 val trace = fn : bool -> unit 35 36Breakpoints 37 38 val breakAt = fn : string * int -> unit 39 val breakIn = fn : string -> unit 40 val breakEx = fn : exn -> unit 41 val clearAt = fn : string * int -> unit 42 val clearIn = fn : string -> unit 43 val clearEx = fn : exn -> unit 44 45Single Stepping and Continuing 46 47 val continue = fn : unit -> unit 48 val step = fn : unit -> unit 49 val stepOver = fn : unit -> unit 50 val stepOut = fn : unit -> unit 51 52Examining and Traversing the Stack 53 54 val up = fn : unit -> unit 55 val down = fn : unit -> unit 56 val dump = fn : unit -> unit 57 val variables = fn : unit -> unit 58 *) 59 60fun eqf_elim thm = let 61 val concl = (rconcl thm) handle HOL_ERR _ => ``F`` 62in 63 if concl = ``F`` then 64 STRIP_FORALL_RULE EQF_ELIM thm 65 else 66 thm 67end; 68 69(* Conversion for executing the operational semantics. *) 70local 71 val list2_pair = fn [x, y] => (x, y); 72 val f = (fn c => map (snd o dest_eq) (strip_conj c)); 73in 74 75fun strip_trans (thm) = let 76 val concl = (rconcl thm) handle HOL_ERR _ => ``F`` 77in 78 if concl = ``F`` then [] 79 else 80 map (list2_pair o f) (strip_disj concl) 81end; 82 83fun CCS_TRANS_CONV tm = 84 85(* case 1: nil *) 86 if is_nil tm then 87 NIL_NO_TRANS_EQF 88 89(* case 2: prefix *) 90 else if is_prefix tm then 91 let val (u, P) = args_prefix tm 92 in 93 ISPECL [u, P] TRANS_PREFIX_EQ 94 end 95 96(* case 3: sum *) 97 else if is_sum tm then 98 let val (P1, P2) = args_sum tm; 99 val thm1 = CCS_TRANS_CONV P1 100 and thm2 = CCS_TRANS_CONV P2 101 in 102 REWRITE_RULE [thm1, thm2] (ISPECL [P1, P2] TRANS_SUM_EQ') 103 end 104 105(* case 4: restr *) 106 else if is_restr tm then 107 let fun extr_acts [] _ = [] 108 | extr_acts actl L = let 109 val act = hd actl 110 in 111 if is_tau act then 112 act :: (extr_acts (tl actl) L) 113 else 114 let val l = arg_action act; 115 val thml = Label_IN_CONV l L 116 in 117 if (rconcl thml = ``T``) then 118 extr_acts (tl actl) L 119 else 120 let val thmlc = Label_IN_CONV 121 (rconcl 122 (REWRITE_CONV [COMPL_LAB_def] ``COMPL ^l``)) 123 L 124 in 125 if (rconcl thmlc = ``T``) then 126 extr_acts (tl actl) L 127 else 128 act :: (extr_acts (tl actl) L) 129 end (* val thmlc *) 130 end (* val l *) 131 end; (* val act *) 132 val (P, L) = args_restr tm; 133 val thm = CCS_TRANS_CONV P 134 in 135 if (rconcl thm = ``F``) then 136 prove (``!u E. TRANS ^tm u E = F``, 137(** PROOF BEGIN ***************************************************************) 138 REPEAT GEN_TAC 139 >> EQ_TAC 140 >| [ (* goal 1 *) 141 DISCH_TAC \\ 142 IMP_RES_TAC TRANS_RESTR \\ 143 IMP_RES_TAC thm, 144 (* goal 2 *) 145 REWRITE_TAC [] ]) 146(****************************************************************** Q. E. D. **) 147 else 148 let val dl = strip_disj (rconcl thm); 149 val actl = map (snd o dest_eq o hd o strip_conj o hd o strip_disj) dl; 150 val actl_not = extr_acts actl L; 151 val tau = mk_const ("NONE", type_of (hd actl)); 152 val U = mk_var ("u", type_of (hd actl)); 153 in 154 if (null actl_not) then 155 prove (``!u E. TRANS ^tm u E = F``, 156(** PROOF BEGIN ***************************************************************) 157 REPEAT GEN_TAC >> EQ_TAC 158 >| [ (* goal 1 *) 159 STRIP_TAC \\ 160 IMP_RES_TAC TRANS_RESTR >| 161 [ (* goal 1.1 *) 162 IMP_RES_TAC thm >| 163 (list_apply_tac 164 (fn a => CHECK_ASSUME_TAC 165 (REWRITE_RULE [ASSUME ``u = ^tau``, Action_distinct] 166 (ASSUME ``u = ^a``))) actl), 167 (* goal 1.2 *) 168 IMP_RES_TAC thm >| 169 (list_apply_tac 170 (fn a => ASSUME_TAC (REWRITE_RULE [ASSUME ``^U = label l``, Action_11] 171 (ASSUME ``u = ^a``)) \\ 172 CHECK_ASSUME_TAC 173 (REWRITE_RULE [ASSUME ``l = ^(arg_action a)``, 174 Label_IN_CONV (arg_action a) L] 175 (ASSUME ``~(l IN ^L)``)) \\ 176 CHECK_ASSUME_TAC 177 (REWRITE_RULE [ASSUME ``l = ^(arg_action a)``, COMPL_LAB_def, 178 Label_IN_CONV 179 (rconcl (REWRITE_CONV [COMPL_LAB_def] 180 ``COMPL ^(arg_action a)``)) L] 181 (ASSUME ``~((COMPL_LAB l) IN ^L)``))) actl) ], 182 (* goal 2 *) 183 REWRITE_TAC [] ]) 184(****************************************************************** Q. E. D. **) 185 else (* actl_not is not empty => the list of pairs lp is not empty as well *) 186 let fun build_disj lp L = 187 let val (u, p) = hd lp in 188 if (null (tl lp)) then 189 mk_conj (``u = ^u``, ``E = ^(mk_restr (p, L))``) 190 else 191 mk_disj (mk_conj (``u = ^u``, 192 ``E = ^(mk_restr (p, L))``), 193 build_disj (tl lp) L) 194 end; 195 val lp = map (list2_pair o f) 196 (filter (fn c => 197 mem ((snd o dest_eq o hd o strip_conj 198 o hd o strip_disj) c) 199 actl_not) dl); 200 val dsjt = build_disj lp L; 201 val (u, p) = hd lp; 202 val tau = mk_const ("NONE", type_of u); 203 in 204 prove (``!u E. TRANS ^tm u E = ^dsjt``, 205(** PROOF BEGIN ***************************************************************) 206 REPEAT GEN_TAC >> EQ_TAC 207 >| [ (* goal 1 *) 208 DISCH_TAC >> IMP_RES_TAC TRANS_RESTR >| 209 [ (* goal 1.1 *) 210 IMP_RES_TAC thm >| 211 (list_apply_tac 212 (fn a => CHECK_ASSUME_TAC (REWRITE_RULE [ASSUME ``u = ^tau``, Action_distinct] 213 (ASSUME ``u = ^a``)) \\ 214 ASM_REWRITE_TAC []) actl), 215 (* goal 1.2 *) 216 IMP_RES_TAC thm >| 217 (list_apply_tac 218 (fn a => if is_tau a then 219 ASSUME_TAC (REWRITE_RULE [ASSUME ``^U = label l``, Action_11] 220 (ASSUME ``u = ^a``)) \\ 221 ASM_REWRITE_TAC [] 222 else 223 ASSUME_TAC (REWRITE_RULE [ASSUME ``^U = label l``, Action_11] 224 (ASSUME ``u = ^a``)) \\ 225 CHECK_ASSUME_TAC 226 (REWRITE_RULE [ASSUME ``l = ^(arg_action a)``, 227 Label_IN_CONV (arg_action a) L] 228 (ASSUME ``~(l IN ^L)``)) \\ 229 CHECK_ASSUME_TAC 230 (REWRITE_RULE 231 [ASSUME ``l = ^(arg_action a)``, COMPL_LAB_def, 232 Label_IN_CONV 233 (rconcl (REWRITE_CONV [COMPL_LAB_def] ``COMPL ^(arg_action a)``)) L] 234 (ASSUME ``~((COMPL_LAB l) IN ^L)``)) \\ 235 ASM_REWRITE_TAC []) actl) ], 236 (* goal 2 *) 237 STRIP_TAC >| 238 (list_apply_tac 239 (fn (a, P) => 240 REWRITE_TAC [ASSUME ``u = ^a``, 241 ASSUME ``E = restr ^L ^P``] \\ 242 MATCH_MP_TAC RESTR \\ 243 (if is_tau a then 244 ASM_REWRITE_TAC [thm] 245 else 246 EXISTS_TAC (arg_action a) \\ 247 ASM_REWRITE_TAC 248 [thm, COMPL_LAB_def, 249 Label_IN_CONV (arg_action a) L, 250 Label_IN_CONV (rconcl (REWRITE_CONV [COMPL_LAB_def] 251 ``COMPL ^(arg_action a)``)) L])) 252 lp) ]) (* prove *) 253(****************************************************************** Q. E. D. **) 254 end (* let: build_disj *) 255 end (* let: dl *) 256 end (* let: extr_acts *) 257 258(* case 5: relab *) 259 else if is_relab tm then 260 let val (P, rf) = args_relab tm; 261 val thm = CCS_TRANS_CONV P 262 in 263 if (rconcl thm = ``F``) then 264 prove (``!u E. TRANS ^tm u E = F``, 265(** PROOF BEGIN ***************************************************************) 266 REPEAT GEN_TAC 267 >> EQ_TAC (* 2 sub-goals here *) 268 >| [ (* goal 1 (of 2) *) 269 DISCH_TAC \\ 270 IMP_RES_TAC TRANS_RELAB \\ 271 IMP_RES_TAC thm, 272 (* goal 2 (of 2) *) 273 REWRITE_TAC [] ]) 274(****************************************************************** Q. E. D. **) 275 else (* ~(rconcl thm = "F") implies dl is not empty *) 276 let fun relab_act [] _ = [] 277 | relab_act actl labl = let 278 val act = hd actl; 279 val thm_act = 280 REWRITE_RHS_RULE [relabel_def, Apply_Relab_def, 281 Label_distinct, Label_distinct', Label_11, 282 COMPL_LAB_def, COMPL_COMPL_LAB] 283 (REFL ``relabel (Apply_Relab ^labl) ^act``); 284 val thm_act' = RELAB_EVAL_CONV (rconcl thm_act) 285 in 286 (TRANS thm_act thm_act') :: (relab_act (tl actl) labl) 287 end; 288 fun build_disj_relab rlp rf = 289 let val (u, p) = hd rlp 290 in 291 if (null (tl rlp)) then 292 mk_conj (``u = ^u``, 293 ``E = ^(mk_relab (p, rf))``) 294 else 295 mk_disj (mk_conj (``u = ^u``, 296 ``E = ^(mk_relab (p, rf))``), 297 build_disj_relab (tl rlp) rf) 298 end; 299 val dl = strip_disj (rconcl thm); 300 val actl = map (snd o dest_eq o hd o strip_conj) dl 301 and labl = arg_relabelling rf; 302 val U = mk_var ("u", type_of (hd actl)); 303 val thml = relab_act actl labl; 304 val rlp = combine (map rconcl thml, map (snd o list2_pair o f) dl); 305 val disjt = build_disj_relab rlp rf 306 in 307 prove (``!u E. TRANS ^tm u E = ^disjt``, 308(** PROOF BEGIN ***************************************************************) 309 REPEAT GEN_TAC 310 >> EQ_TAC (* 2 sub-goals here *) 311 >| [ (* goal 1 (of 2) *) 312 DISCH_TAC \\ 313 IMP_RES_TAC TRANS_RELAB \\ 314 IMP_RES_TAC thm >| 315 (list_apply_tac 316 (fn (a, thm_act) => 317 REWRITE_TAC [REWRITE_RULE [ASSUME ``u' = ^a``, thm_act] 318 (REWRITE_RULE [SYM (ASSUME ``RELAB ^labl = RELAB labl``)] 319 (ASSUME ``^U = relabel (Apply_Relab labl) u'``))] \\ 320 ASM_REWRITE_TAC []) 321 (combine (actl, thml))), 322 (* goal 2 (of 2) *) 323 STRIP_TAC >| 324 (list_apply_tac 325 (fn ((a, P), thm_act) => 326 REWRITE_TAC [ONCE_REWRITE_RULE [SYM thm_act] 327 (ASSUME ``u = ^a``), 328 ASSUME ``E = relab ^P ^rf``] \\ 329 MATCH_MP_TAC RELABELING \\ 330 REWRITE_TAC [thm]) 331 (combine (rlp, thml))) ]) 332(****************************************************************** Q. E. D. **) 333 end (* fun relab_act *) 334 end (* val (P, rf) *) 335 336(* case 6: par *) 337 else if is_par tm then 338 let fun build_disj1 dl P = 339 let val (u, p) = hd dl 340 in 341 if (null (tl dl)) then 342 mk_conj (``u = ^u``, ``E = ^(mk_par (p, P))``) 343 else 344 mk_disj (mk_conj (``u = ^u``, ``E = ^(mk_par (p, P))``), 345 build_disj1 (tl dl) P) 346 end; 347 fun build_disj2 dl P = 348 let val (u, p) = hd dl 349 in 350 if (null (tl dl)) then 351 mk_conj (``u = ^u``, ``E = ^(mk_par (P, p))``) 352 else 353 mk_disj (mk_conj (``u = ^u``, ``E = ^(mk_par (P, p))``), 354 build_disj2 (tl dl) P) 355 end; 356 fun build_disj_tau _ [] = ``F`` 357 | build_disj_tau p syncl = let 358 val (u, p') = hd syncl; 359 val tau = mk_const ("NONE", type_of u); 360 in 361 mk_disj (mk_conj (``u = ^tau``, ``E = ^(mk_par (p, p'))``), 362 build_disj_tau p (tl syncl)) 363 end; 364 fun act_sync [] _ = [] 365 | act_sync dl1 dl2 = let 366 val (act, p) = hd dl1; 367 val syncl = filter (fn (a, p) => 368 a = (if is_tau act then 369 act 370 else 371 rconcl (REWRITE_CONV [COMPL_ACT_def, COMPL_LAB_def] 372 ``COMPL_ACT ^act``))) 373 dl2 374 in 375 if (null syncl) then 376 act_sync (tl dl1) dl2 377 else 378 act :: (act_sync (tl dl1) dl2) 379 end; 380 fun build_sync dl1 dl2 = 381 let val (act, p) = hd dl1; 382 val syncl = filter (fn (a, p) => 383 a = (if is_tau act then 384 act 385 else 386 rconcl (REWRITE_CONV [COMPL_ACT_def, COMPL_LAB_def] 387 ``COMPL_ACT ^act``))) 388 dl2 389 in 390 if (null (tl dl1)) then 391 build_disj_tau p syncl 392 else 393 mk_disj (build_disj_tau p syncl, build_sync (tl dl1) dl2) 394 end; 395 val (P1, P2) = args_par tm; 396 val thm1 = CCS_TRANS_CONV P1 397 and thm2 = CCS_TRANS_CONV P2 398 in 399 if (rconcl thm1 = ``F``) andalso (rconcl thm2 = ``F``) then 400 prove (``!u E. TRANS ^tm u E = F``, 401(** PROOF BEGIN ***************************************************************) 402 REPEAT GEN_TAC 403 >> EQ_TAC (* 2 sub-goals here *) 404 >| [ (* goal 1 *) 405 DISCH_TAC \\ 406 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 407 [ IMP_RES_TAC thm1, IMP_RES_TAC thm2, IMP_RES_TAC thm1 ], 408 (* goal 2 *) 409 REWRITE_TAC [] ]) 410(****************************************************************** Q. E. D. **) 411 else if (rconcl thm1 = ``F``) then 412 let val dl2 = map (list2_pair o f) (strip_disj (rconcl thm2)); 413 val actl2 = map fst dl2 414 and disj_nosync = build_disj2 dl2 P1 415 in 416 prove (``!u E. TRANS ^tm u E = ^disj_nosync``, 417(** PROOF BEGIN ***************************************************************) 418 REPEAT GEN_TAC 419 >> EQ_TAC 420 >| [ (* goal 1 (of 2) *) 421 DISCH_TAC \\ 422 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 423 [ IMP_RES_TAC thm1, 424 IMP_RES_TAC thm2 >> ASM_REWRITE_TAC [], 425 IMP_RES_TAC thm1 ], 426 (* goal 2 (of 2) *) 427 STRIP_TAC >| 428 (list_apply_tac 429 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR2 \\ 430 REWRITE_TAC [GEN_ALL thm2]) actl2) ]) 431(****************************************************************** Q. E. D. **) 432 end 433 else if (rconcl thm2 = ``F``) then 434 let val dl1 = map (list2_pair o f) (strip_disj (rconcl thm1)); 435 val actl1 = map fst dl1 436 and disj_nosync = build_disj1 dl1 P2 437 in 438 prove (``!u E. TRANS ^tm u E = ^disj_nosync``, 439(** PROOF BEGIN ***************************************************************) 440 REPEAT GEN_TAC 441 >> EQ_TAC 442 >| [ (* goal 1 (of 2) *) 443 DISCH_TAC \\ 444 IMP_RES_TAC TRANS_PAR >| 445 [ IMP_RES_TAC thm1 >> ASM_REWRITE_TAC [], 446 IMP_RES_TAC thm2, 447 IMP_RES_TAC thm2 ], 448 (* goal 2 (of 2) *) 449 STRIP_TAC >| 450 (list_apply_tac 451 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR1 \\ 452 REWRITE_TAC [GEN_ALL thm1]) actl1) ]) 453(****************************************************************** Q. E. D. **) 454 end 455 else (* ~(rconcl thm1 = "F") and ~(rconcl thm2 = "F") => dl1 and dl2 are not empty *) 456 let val [dl1, dl2] = map ((map (list2_pair o f)) o strip_disj o rconcl) 457 [thm1, thm2]; 458 val [actl1, actl2] = map (map fst) [dl1, dl2] 459 and disj_nosync = mk_disj (build_disj1 dl1 P2, build_disj2 dl2 P1) 460 and disj_sync = rconcl (QCONV (REWRITE_CONV []) (build_sync dl1 dl2)) 461 in 462 if (disj_sync = ``F``) then 463 prove (``!u E. TRANS ^tm u E = ^disj_nosync``, 464(** PROOF BEGIN ***************************************************************) 465 REPEAT GEN_TAC 466 >> EQ_TAC (* 2 sub-goals here *) 467 >| [ (* goal 1 (of 2) *) 468 DISCH_TAC \\ 469 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 470 [ IMP_RES_TAC thm1 >> ASM_REWRITE_TAC [], 471 IMP_RES_TAC thm2 >> ASM_REWRITE_TAC [], 472 IMP_RES_TAC thm1 \\ 473 IMP_RES_TAC thm2 >| 474 (list_apply_tac 475 (fn a => 476 if is_tau (hd actl1) then 477 IMP_RES_TAC Action_distinct_label 478 else 479 let val eq = REWRITE_RULE [REWRITE_RULE [Action_11] 480 (ASSUME ``label l = ^(hd actl1)``), 481 COMPL_LAB_def] 482 (ASSUME ``label (COMPL_LAB l) = ^a``) 483 in 484 CHECK_ASSUME_TAC 485 (REWRITE_RULE [eq] (Action_EQ_CONV (concl eq))) 486 end) actl2) ], 487 (* goal 2 (of 2) *) 488 STRIP_TAC >| (* as many as the number of the summands *) 489 (list_apply_tac 490 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR1 \\ 491 REWRITE_TAC [GEN_ALL thm1]) actl1) @ 492 (list_apply_tac 493 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR2 \\ 494 REWRITE_TAC [GEN_ALL thm2]) actl2) @ 495 (list_apply_tac 496 (fn a => ASM_REWRITE_TAC [] \\ 497 MATCH_MP_TAC PAR3 \\ 498 EXISTS_TAC (arg_action a) \\ 499 REWRITE_TAC [COMPL_LAB_def, GEN_ALL thm1, GEN_ALL thm2]) 500 (act_sync dl1 dl2)) ]) 501(****************************************************************** Q. E. D. **) 502 else 503 prove (``!u E. TRANS ^tm u E = ^(mk_disj (disj_nosync, disj_sync))``, 504(** PROOF BEGIN ***************************************************************) 505 REPEAT GEN_TAC 506 >> EQ_TAC (* 2 sub-goals here *) 507 >| [ (* goal 1 (of 2) *) 508 DISCH_TAC \\ 509 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 510 [ IMP_RES_TAC thm1 >> ASM_REWRITE_TAC [], 511 IMP_RES_TAC thm2 >> ASM_REWRITE_TAC [], 512 IMP_RES_TAC thm1 >> IMP_RES_TAC thm2 >> ASM_REWRITE_TAC [] ], 513 (* goal 2 (of 2) *) 514 STRIP_TAC >| (* as many as the number of the summands *) 515 (list_apply_tac (* goal 2.1 *) 516 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR1 \\ 517 REWRITE_TAC [GEN_ALL thm1]) actl1) @ 518 (list_apply_tac (* goal 2.2 *) 519 (fn a => ASM_REWRITE_TAC [] >> MATCH_MP_TAC PAR2 \\ 520 REWRITE_TAC [GEN_ALL thm2]) actl2) @ 521 (list_apply_tac (* goal 2.3 *) 522 (fn a => ASM_REWRITE_TAC [] \\ 523 MATCH_MP_TAC PAR3 \\ 524 EXISTS_TAC (arg_action a) \\ 525 REWRITE_TAC [COMPL_LAB_def, GEN_ALL thm1, GEN_ALL thm2]) 526 (act_sync dl1 dl2)) ]) 527(****************************************************************** Q. E. D. **) 528 end (* val [dl1, dl2] *) 529 end (* fun build_disj1 *) 530 531(* case 7: rec *) 532 else if is_rec tm then 533 let val (X, P) = args_rec tm; 534 val thmS = SIMP_CONV (srw_ss ()) [CCS_Subst_def] ``CCS_Subst ^P ^tm ^X``; 535 val thm = CCS_TRANS_CONV (rconcl thmS) 536 in 537 GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, thmS, thm] ``TRANS ^tm u E``) 538 end (* val (X, P) *) 539 else (* no need to distinguish on (rconcl thm) *) 540 failwith "CCS_TRANS_CONV"; 541 542(** CCS_TRANS returns both a theorem and a list of CCS transitions **) 543fun CCS_TRANS tm = 544 let val thm = CCS_TRANS_CONV tm; 545 val trans = strip_trans thm 546 in 547 (eqf_elim thm, trans) 548 end; 549 550end; (* local *) 551 552(******************************************************************************) 553(* *) 554(* Test cases for CCS_TRANS_CONV *) 555(* *) 556(******************************************************************************) 557 558(* moved to selftest.sml *) 559 560end (* struct *) 561 562(* last updated: May 15, 2017 *) 563