1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6structure StrongLawsConv :> StrongLawsConv = 7struct 8 9open HolKernel Parse boolLib bossLib; 10open prim_recTheory arithmeticTheory numTheory numLib; 11open PFset_conv IndDefRules listSyntax stringLib; 12open CCSLib CCSTheory CCSSyntax CCSConv; 13open StrongEQTheory StrongEQLib StrongLawsTheory; 14 15infixr 0 S_THENC S_ORELSEC; 16 17(******************************************************************************) 18(* *) 19(* Conversions for the summation operator and strong equivalence *) 20(* *) 21(******************************************************************************) 22 23fun STRONG_SUM_ASSOC_CONV tm = let 24 val (a,b) = args_sum tm 25in 26 if is_sum b then 27 let val (b1, b2) = args_sum b; 28 val thm = ISPECL [a, b1, b2] STRONG_SUM_ASSOC_L; 29 val thm' = STRONG_SUM_ASSOC_CONV (rhs_tm thm) 30 in 31 S_TRANS thm thm' 32 end 33 else if is_sum a then 34 let val thm'' = STRONG_SUM_ASSOC_CONV a 35 in 36 ISPEC b (MATCH_MP STRONG_EQUIV_SUBST_SUM_R thm'') 37 end 38 else 39 ISPEC tm STRONG_EQUIV_REFL 40end; 41 42(* Conversion for the application of STRONG_SUM_IDENT(_L/R). *) 43fun STRONG_SUM_NIL_CONV tm = 44 if is_sum tm then 45 let 46 val (t1, t2) = args_sum tm 47 in 48 if is_nil t1 then 49 ISPEC t2 STRONG_SUM_IDENT_L 50 else if is_nil t2 then 51 ISPEC t1 STRONG_SUM_IDENT_R 52 else 53 failwith "STRONG_SUM_NIL_CONV" 54 end 55 else 56 failwith "STRONG_SUM_NIL_CONV"; 57 58(* Find repeated occurrences of a summand to be then deleted by applying 59 STRONG_SUM_IDEMP. *) 60fun STRONG_FIND_IDEMP tm l = let 61 val h::t = l 62in 63 if (null t) then 64 failwith "term not a CCS summation" 65 else 66 let val tm' = fst (args_sum tm) 67 in 68 if (mem h t) then 69 let val (l1, l2) = FIND_SMD [] h [] tm' 70 in 71 if (null l2) then 72 if (null l1) then 73 ISPEC h STRONG_SUM_IDEMP 74 else 75 let val y = hd l1 76 in 77 S_TRANS (ISPECL [y, h, h] STRONG_SUM_ASSOC_R) 78 (ISPEC y (MP (ISPECL [mk_sum (h, h), h] STRONG_EQUIV_SUBST_SUM_R) 79 (ISPEC h STRONG_SUM_IDEMP))) 80 end 81 else 82 let val thm1 = 83 if (null l1) then 84 S_TRANS (S_SYM (STRONG_SUM_ASSOC_CONV 85 (mk_sum (mk_sum (h, hd l2), h)))) 86 (ISPECL [h, hd l2] STRONG_SUM_MID_IDEMP) 87 else 88 S_TRANS (S_SYM (STRONG_SUM_ASSOC_CONV 89 (mk_sum (mk_sum (mk_sum (hd l1, h), hd l2), h)))) 90 (ISPECL [hd l1, h, hd l2] STRONG_LEFT_SUM_MID_IDEMP) 91 in 92 S_TRANS thm1 (STRONG_SUM_ASSOC_CONV (snd (args_thm thm1))) 93 end 94 end 95 else 96 let val thm' = STRONG_FIND_IDEMP tm' t 97 in 98 ISPEC h (MATCH_MP STRONG_EQUIV_SUBST_SUM_R thm') 99 end 100 end 101end; 102 103(* Conversion for the application of STRONG_SUM_IDEMP. *) 104fun STRONG_SUM_IDEMP_CONV tm = 105 if is_sum tm then 106 let val thm = STRONG_SUM_ASSOC_CONV tm; 107 val t1 = rhs_tm thm; 108 val thm' = STRONG_FIND_IDEMP t1 (rev (flat_sum t1)) 109 in 110 S_TRANS thm thm' 111 end 112 else 113 failwith "STRONG_SUM_IDEMP_CONV"; 114 115(******************************************************************************) 116(* *) 117(* Conversions for the restriction operator and strong equivalence *) 118(* *) 119(******************************************************************************) 120 121(* Conversion for the application of the laws for the restriction operator. *) 122fun STRONG_RESTR_ELIM_CONV tm = 123 if is_restr tm then 124 let val (P, L) = args_restr tm 125 in 126 if (is_nil P) then 127 ISPEC L STRONG_RESTR_NIL 128 else if (is_sum P) then 129 let val (P1, P2) = args_sum P in 130 ISPECL [P1, P2, L] STRONG_RESTR_SUM 131 end 132 else if (is_prefix P) then 133 let val (u, P') = args_prefix P in 134 if (is_tau u) then 135 ISPECL [P', L] STRONG_RESTR_PREFIX_TAU 136 else 137 let val l = arg_action u; 138 val thm = Label_IN_CONV l L 139 in 140 if (rconcl thm = ``T``) then 141 ISPEC P' (MP (ISPECL [l, L] STRONG_RESTR_PR_LAB_NIL) 142 (DISJ1 (EQT_ELIM thm) ``COMPL_LAB ^l IN ^L``)) 143 else 144 let val thmc = REWRITE_RHS_RULE [COMPL_LAB_def] (REFL ``COMPL_LAB ^l``); 145 val thm' = Label_IN_CONV (rconcl thmc) L 146 in 147 if (rconcl thm' = ``T``) then 148 ISPEC P' (MP (ONCE_REWRITE_RULE [COMPL_LAB_def] 149 (ISPECL [l, L] STRONG_RESTR_PR_LAB_NIL)) 150 (DISJ2 ``^l IN ^L`` (EQT_ELIM thm'))) 151 else 152 ISPEC P' (MP (ONCE_REWRITE_RULE [COMPL_LAB_def] 153 (ISPECL [l, L] STRONG_RESTR_PREFIX_LABEL)) 154 (CONJ (EQF_ELIM thm) (EQF_ELIM thm'))) 155 end 156 end 157 end 158 else 159 failwith "STRONG_RESTR_ELIM_CONV" 160 end 161 else 162 failwith "STRONG_RESTR_ELIM_CONV"; 163 164(******************************************************************************) 165(* *) 166(* Conversions for the relabelling operator and strong equivalence *) 167(* *) 168(******************************************************************************) 169 170(* Conversion for the application of the laws for the relabelling operator. *) 171fun STRONG_RELAB_ELIM_CONV tm = 172 if is_relab tm then 173 let val (P, rf) = args_relab tm 174 in 175 if (is_nil P) then 176 ISPEC rf STRONG_RELAB_NIL 177 else if (is_sum P) then 178 let val (P1, P2) = args_sum P in 179 ISPECL [P1, P2, rf] STRONG_RELAB_SUM 180 end 181 else if (is_prefix P) then 182 let val (u, P') = args_prefix P 183 and labl = arg_relabelling rf; 184 val thm_act = REWRITE_RHS_RULE 185 [relabel_def, Apply_Relab_def, 186 Label_distinct, Label_distinct', Label_11, 187 COMPL_LAB_def, COMPL_COMPL_LAB] 188 (REFL ``relabel (Apply_Relab ^labl) ^u``); 189 val thm_act' = RELAB_EVAL_CONV (rconcl thm_act) 190 in 191 ONCE_REWRITE_RULE [TRANS thm_act thm_act'] 192 (ISPECL [u, P', labl] STRONG_RELAB_PREFIX) 193 end 194 else 195 failwith "STRONG_RELAB_ELIM_CONV" 196 end 197 else 198 failwith "STRONG_RELAB_ELIM_CONV"; 199 200(******************************************************************************) 201(* *) 202(* Conversions for the parallel operator and strong equivalence *) 203(* *) 204(******************************************************************************) 205 206(* Conversion to evaluate conditionals involving numbers. *) 207fun COND_EVAL_CONV (c :term) :thm = 208 if is_cond c then 209 let val (b, l, r) = dest_cond c; 210 val thm1 = num_CONV b 211 and thm2 = ISPECL [l, r] CCS_COND_CLAUSES 212 in 213 if (rconcl thm1) = ``T`` then 214 SUBS [SYM thm1] (CONJUNCT1 thm2) 215 else 216 TRANS (SUBS [SYM thm1] (CONJUNCT2 thm2)) (COND_EVAL_CONV r) 217 end 218 else 219 REFL c; 220 221val BETA_COND_CONV = BETA_CONV THENC COND_EVAL_CONV; 222 223(* Conversion that checks that, for all k <= n, the agents given by the 224 function f are prefixed agents. *) 225fun IS_PREFIX_CHECK k n f = prove ( 226 ``!^k. ^k <= ^n ==> Is_Prefix (^f ^k)``, 227 GEN_TAC 228 >> REWRITE_TAC [LESS_OR_EQ, LESS_THM, NOT_LESS_0] 229 >> BETA_TAC 230 >> STRIP_TAC 231 >> ASM_REWRITE_TAC [INV_SUC_EQ, NOT_SUC, SUC_NOT, PREF_IS_PREFIX]); 232 233(* Conversion for deleting nil subterms by means of the identity laws for the 234 parallel operator. *) 235fun STRONG_PAR_NIL_CONV tm = 236 if is_par tm then 237 let val (P, Q) = args_par tm 238 in 239 if is_nil P then ISPEC Q STRONG_PAR_IDENT_L 240 else if is_nil Q then ISPEC P STRONG_PAR_IDENT_R 241 else 242 failwith "STRONG_PAR_NIL_CONV" 243 end 244 else 245 failwith "STRONG_PAR_NIL_CONV"; 246 247(* Conversion for deleting nil subterms by means of the identity laws for the 248 parallel and summation operators. *) 249fun STRONG_NIL_SUM_PAR_CONV tm = 250 if is_par tm then 251 let val (P, Q) = args_par tm 252 in 253 if is_nil P then 254 ISPEC Q STRONG_PAR_IDENT_L 255 else if is_nil Q then 256 ISPEC P STRONG_PAR_IDENT_R 257 else 258 failwith "STRONG_NIL_SUM_PAR_CONV" 259 end 260 else if is_sum tm then 261 let val (P, Q) = args_sum tm 262 in 263 if is_nil P then 264 ISPEC Q STRONG_SUM_IDENT_L 265 else if is_nil Q then 266 ISPEC P STRONG_SUM_IDENT_R 267 else 268 failwith "STRONG_NIL_SUM_PAR_CONV" 269 end 270 else 271 failwith "STRONG_NIL_SUM_PAR_CONV"; 272 273(* Conversion for extracting the prefixed action and the prefixed process by 274 applying PREF_ACT and PREF_PROC, respectively. *) 275fun PREFIX_EXTRACT tm = let 276 val (opr, opd) = dest_comb tm; 277 val (act, proc) = args_prefix opd 278in 279 if opr = mk_const ("PREF_ACT", type_of opr) then 280 ISPECL [act, proc] PREF_ACT_def 281 else if opr = mk_const ("PREF_PROC", type_of opr) then 282 ISPECL [act, proc] PREF_PROC_def 283 else 284 failwith "PREFIX_EXTRACT" 285end; 286 287(* Conversion for simplifying a summation term. *) 288val SIMPLIFY_CONV = 289 (DEPTH_CONV BETA_COND_CONV) THENC (DEPTH_CONV PREFIX_EXTRACT); 290 291(* Conversion to compute the synchronizing summands. *) 292fun ALL_SYNC_CONV f n1 f' n2 = 293 let val c1 = REWRITE_CONV [ALL_SYNC_def] ``ALL_SYNC ^f ^n1 ^f' ^n2``; 294 val c2 = TRANS c1 (SIMPLIFY_CONV (rconcl c1)); 295 val c3 = TRANS c2 (REWRITE_CONV [SYNC_def] (rconcl c2)); 296 val c4 = TRANS c3 (SIMPLIFY_CONV (rconcl c3)); 297 val c5 = TRANS c4 (REWRITE_CONV [LABEL_def, COMPL_LAB_def, Action_distinct_label, 298 Label_distinct, Label_distinct', Label_11] 299 (rconcl c4)) 300 in 301 TRANS c5 (REWRITE_RHS_RULE [] (DEPTH_CONV string_EQ_CONV (rconcl c5))) 302 end; 303 304(* Conversion for the application of the law for the parallel operator in the 305 general case of at least one summation agent in parallel. *) 306fun STRONG_PAR_SUM_CONV tm = let 307 fun comp_fun tm = 308 let val thm = REWRITE_RHS_RULE [CCS_SIGMA_def] ((DEPTH_CONV BETA_CONV) tm); 309 val thm' = REWRITE_RHS_RULE [INV_SUC_EQ, NOT_SUC, SUC_NOT, 310 PREF_ACT_def, PREF_PROC_def] 311 ((DEPTH_CONV BETA_CONV) (rconcl thm)) 312 in TRANS thm thm' end; 313 val (ls1, ls2) = (fn (x, y) => (flat_sum x, flat_sum y)) (args_par tm) 314 and (P1, P2) = args_par tm; 315 val ARBtm = inst [``:'a`` |-> ``:CCS``] ``ARB: 'a``; 316 val f = ``\x: num. ^(sum_to_fun ls1 ARBtm ``0: num``)`` 317 and f' = ``\x: num. ^(sum_to_fun ls2 ARBtm ``0: num``)`` 318 and [n1, n2] = map (term_of_int o length) [ls1, ls2]; 319 val [thm1, thm2] = 320 map (fn t => REWRITE_RULE [INV_SUC_EQ, NOT_SUC, SUC_ID] 321 (BETA_RULE (REWRITE_CONV [CCS_SIGMA_def] t))) 322 [``SIGMA ^f ^n1``, ``SIGMA ^f' ^n2``] 323 and thmp1 = IS_PREFIX_CHECK ``i: num`` n1 f 324 and thmp2 = IS_PREFIX_CHECK ``j: num`` n2 f' 325 and [thmc1, thmc2] = 326 map comp_fun 327 [``SIGMA (\i. prefix (PREF_ACT (^f i)) 328 (par (PREF_PROC (^f i)) (SIGMA ^f' ^n2))) ^n1``, 329 ``SIGMA (\j. prefix (PREF_ACT (^f' j)) 330 (par (SIGMA ^f ^n1) (PREF_PROC (^f' j)))) ^n2``] 331 and thm_sync = ALL_SYNC_CONV f n1 f' n2; 332 val thmt = 333 REWRITE_RULE [thmc1, thmc2, thm_sync] 334 (MATCH_MP (ISPECL [f, n1, f', n2] STRONG_EXPANSION_LAW) 335 (CONJ thmp1 thmp2)) 336in 337 if is_prefix P1 then 338 let val thma' = S_SUBST (STRONG_SUM_ASSOC_CONV P2) ``par ^P1 ^P2`` 339 in 340 S_TRANS thma' (REWRITE_LHS_RULE [thm1, thm2] thmt) 341 end 342 else if is_prefix P2 then 343 let val thma' = S_SUBST (STRONG_SUM_ASSOC_CONV P1) ``par ^P1 ^P2`` 344 in 345 S_TRANS thma' (REWRITE_LHS_RULE [thm1, thm2] thmt) 346 end 347 else 348 let val thma = S_SUBST (STRONG_SUM_ASSOC_CONV P1) ``par ^P1 ^P2``; 349 val thma' = S_TRANS thma 350 (S_SUBST (STRONG_SUM_ASSOC_CONV P2) (rhs_tm thma)) 351 in 352 S_TRANS thma' (REWRITE_LHS_RULE [thm1, thm2] thmt) 353 end 354end; 355 356(* Conversion for the application of the laws for the parallel operator in the 357 particular case of two prefixed agents in parallel. *) 358fun STRONG_PAR_PREFIX_CONV (u, P) (v, Q) = 359 if is_tau u andalso is_tau v then 360 ISPECL [P, Q] STRONG_PAR_TAU_TAU 361 else 362 if is_tau u then 363 ISPECL [P, v, Q] STRONG_PAR_TAU_PREF 364 else if is_tau v then 365 ISPECL [u, P, Q] STRONG_PAR_PREF_TAU 366 else 367 let val [l1, l2] = map arg_action [u, v]; 368 val thmc = REWRITE_RHS_RULE [COMPL_LAB_def] (REFL ``^l1 = COMPL ^l2``) 369 in 370 if (rconcl thmc = ``T``) then (* synchronization between l1 and l2 *) 371 ISPECL [P, Q] (MP (ISPECL [l1, l2] STRONG_PAR_PREF_SYNCR) 372 (EQT_ELIM thmc)) 373 else (* no synchronization between l1 and l2 *) 374 let val thm_lab = TRANS thmc (Label_EQ_CONV (rconcl thmc)) in 375 ISPECL [P, Q] (MP (ISPECL [l1, l2] STRONG_PAR_PREF_NO_SYNCR) 376 (EQF_ELIM thm_lab)) 377 end 378 end; 379 380(* Conversion for the application of the laws for the parallel operator. *) 381fun STRONG_PAR_ELIM_CONV tm = 382 if is_par tm then 383 let val (P1, P2) = args_par tm 384 in 385 if (is_prefix P1 andalso is_prefix P2) then 386 let val thm = STRONG_PAR_PREFIX_CONV (args_prefix P1) (args_prefix P2) in 387 S_TRANS thm (S_DEPTH_CONV STRONG_NIL_SUM_PAR_CONV (rhs_tm thm)) 388 end 389 else if (is_sum P1 andalso is_prefix P2) orelse 390 (is_prefix P1 andalso is_sum P2) orelse 391 (is_sum P1 andalso is_sum P2) then 392 let val thm = STRONG_PAR_SUM_CONV tm in 393 S_TRANS thm (S_DEPTH_CONV STRONG_NIL_SUM_PAR_CONV (rhs_tm thm)) 394 end 395 else 396 failwith "STRONG_PAR_ELIM_CONV" 397 end 398 else 399 failwith "STRONG_PAR_ELIM_CONV"; 400 401(* Conversion for applying the expansion theorem (parallel and restriction 402 operators). *) 403val STRONG_EXP_THM_CONV = 404 (S_DEPTH_CONV STRONG_PAR_ELIM_CONV) S_THENC 405 (S_TOP_DEPTH_CONV STRONG_RESTR_ELIM_CONV) S_THENC 406 (S_DEPTH_CONV STRONG_SUM_NIL_CONV); 407 408(******************************************************************************) 409(* *) 410(* Conversions for the recursion operator and strong equivalence *) 411(* *) 412(******************************************************************************) 413 414(* Conversion for applying the unfolding law for the recursion operator. *) 415fun STRONG_REC_UNF_CONV rtm = 416 if is_rec rtm then 417 let val (X, E) = args_rec rtm in 418 REWRITE_RULE [CCS_Subst_def] (ISPECL [X, E] STRONG_UNFOLDING) 419 end 420 else 421 failwith "STRONG_REC_UNF_CONV: no recursive terms"; 422 423(* Conversion for folding a recursive term. *) 424fun STRONG_REC_FOLD_CONV rtm = 425 if is_rec rtm then 426 let val (X, E) = args_rec rtm in 427 S_SYM (REWRITE_RULE [CCS_Subst_def] (ISPECL [X, E] STRONG_UNFOLDING)) 428 end 429 else 430 failwith "STRONG_REC_FOLD_CONV: no recursive terms"; 431 432(******************************************************************************) 433(* *) 434(* Tactics for applying the laws for strong equivalence *) 435(* *) 436(******************************************************************************) 437 438(* Tactics for the application of the laws for STRONG_EQUIV on the left-hand 439 side of a strong equivalence. *) 440val [STRONG_SUM_IDEMP_TAC, 441 STRONG_SUM_NIL_TAC, 442 STRONG_RELAB_ELIM_TAC, 443 STRONG_RESTR_ELIM_TAC, 444 STRONG_PAR_ELIM_TAC, 445 STRONG_REC_UNF_TAC] = map (S_LHS_CONV_TAC o S_DEPTH_CONV) 446 [STRONG_SUM_IDEMP_CONV, 447 STRONG_SUM_NIL_CONV, 448 STRONG_RELAB_ELIM_CONV, 449 STRONG_RESTR_ELIM_CONV, 450 STRONG_PAR_ELIM_CONV, 451 STRONG_REC_UNF_CONV]; 452 453(* Tactic for applying the expansion theorem. *) 454val STRONG_EXP_THM_TAC = S_LHS_CONV_TAC STRONG_EXP_THM_CONV; 455 456end (* struct *) 457 458(* last updated: Jun 18, 2017 *) 459