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