1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6structure WeakLawsConv :> WeakLawsConv = 7struct 8 9open HolKernel Parse boolLib bossLib; 10 11open IndDefRules; 12open CCSLib CCSTheory CCSSyntax CCSConv; 13open StrongEQTheory StrongEQLib StrongLawsTheory StrongLawsConv; 14open WeakEQTheory WeakEQLib WeakLawsTheory; 15 16infixr 0 OE_THENC OE_ORELSEC; 17 18(******************************************************************************) 19(* *) 20(* Conversions and tactics for applying the laws for *) 21(* observation equivalence through strong equivalence *) 22(* *) 23(******************************************************************************) 24 25(* Define the conversions and tactics for the application of the laws for 26 WEAK_EQUIV (through the conversions and tactics for strong equivalence). *) 27fun STRONG_TO_WEAK_EQUIV_CONV (c: conv) tm = 28 MATCH_MP STRONG_IMP_WEAK_EQUIV (c tm); 29 30val [OE_SUM_IDEMP_CONV, OE_SUM_NIL_CONV, OE_RELAB_ELIM_CONV, 31 OE_RESTR_ELIM_CONV, OE_PAR_ELIM_CONV, OE_EXP_THM_CONV, 32 OE_REC_UNF_CONV] = 33 map STRONG_TO_WEAK_EQUIV_CONV 34 [STRONG_SUM_IDEMP_CONV, STRONG_SUM_NIL_CONV, STRONG_RELAB_ELIM_CONV, 35 STRONG_RESTR_ELIM_CONV, STRONG_PAR_ELIM_CONV, STRONG_EXP_THM_CONV, 36 STRONG_REC_UNF_CONV]; 37 38val [OE_SUM_IDEMP_TAC, OE_SUM_NIL_TAC, OE_RELAB_ELIM_TAC, 39 OE_RESTR_ELIM_TAC, OE_PAR_ELIM_TAC, OE_REC_UNF_TAC] = 40 map OE_LHS_CONV_TAC 41 [STRONG_SUM_IDEMP_CONV, STRONG_SUM_NIL_CONV, STRONG_RELAB_ELIM_CONV, 42 STRONG_RESTR_ELIM_CONV, STRONG_PAR_ELIM_CONV, STRONG_REC_UNF_CONV]; 43 44val OE_RHS_RELAB_ELIM_TAC = OE_RHS_CONV_TAC STRONG_RELAB_ELIM_CONV; 45 46(* TODO: idem for the other operators *) 47 48(* Tactic for applying the expansion theorem (parallel and restriction operators). *) 49val OE_EXP_THM_TAC :tactic = 50 fn (asl, w) => let 51 val (opt, t1, t2) = args_equiv w 52 in 53 if opt ~~ mk_const ("WEAK_EQUIV", type_of opt) then 54 let val thm = MATCH_MP STRONG_IMP_WEAK_EQUIV (STRONG_EXP_THM_CONV t1); 55 val (t1', t') = args_thm thm (* t1' = t1 *) 56 in 57 if (t' ~~ t2) then 58 ([], fn [] => OE_TRANS thm (ISPEC t' WEAK_EQUIV_REFL)) 59 else 60 ([(asl, ``WEAK_EQUIV ^t' ^t2``)], fn [thm'] => OE_TRANS thm thm') 61 end 62 else 63 failwith "the goal is not an WEAK_EQUIV relation" 64 end; 65 66(******************************************************************************) 67(* *) 68(* Basic conversions and tactics for applying the laws for *) 69(* observation equivalence *) 70(* *) 71(******************************************************************************) 72 73(* Conversion that proves whether or not a CCS term is stable. *) 74fun STABLE_CONV tm = let 75 fun list2_pair [x, y] = (x, y); 76 val f = (fn c => map (snd o dest_eq) (strip_conj c)); 77 val thm = CCS_TRANS_CONV tm; 78 val lp = map (list2_pair o f) (strip_disj (rconcl thm)); 79 val taul = filter (fn (act, _) => is_tau act) lp; 80 val ccs_typ = type_of tm 81in 82 if (null taul) then 83 prove (``STABLE ^tm``, 84 REWRITE_TAC [STABLE, thm] 85 >> REPEAT STRIP_TAC 86 >| list_apply_tac 87 (fn act => CHECK_ASSUME_TAC (REWRITE_RULE [ASSUME ``u = tau``, Action_distinct] 88 (ASSUME ``u = ^act``))) 89 (fst (split lp))) 90 else 91 prove (``~STABLE ^tm``, 92 REWRITE_TAC [STABLE, thm] 93 >> CONV_TAC (TOP_DEPTH_CONV NOT_FORALL_CONV) 94 >> EXISTS_TAC (fst (hd taul)) 95 >> EXISTS_TAC (snd (hd taul)) 96 >> REWRITE_TAC []) 97end; 98 99(* Define the function OE_SUB_CONV. *) 100fun OE_SUB_CONV (c: conv) tm = 101 if is_prefix tm then 102 let val (u, P) = args_prefix tm; 103 val thm = c P 104 in 105 ISPEC u (MATCH_MP WEAK_EQUIV_SUBST_PREFIX thm) 106 end 107 else if is_sum tm then 108 let val (t1, t2) = args_sum tm; 109 val thm1 = c t1 110 and thm2 = c t2; 111 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *) 112 and (t2', t2'') = args_thm thm2 113 in 114 if t1' ~~ t1'' andalso t2' ~~ t2'' then 115 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL 116 else if t1' ~~ t1'' then 117 ISPEC t1' (MATCH_MP WEAK_EQUIV_SUBST_SUM_L 118 (LIST_CONJ [thm2, STABLE_CONV t2', STABLE_CONV t2''])) 119 else if t2' ~~ t2'' then 120 ISPEC t2' (MATCH_MP WEAK_EQUIV_SUBST_SUM_R 121 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1''])) 122 else 123 MATCH_MP WEAK_EQUIV_PRESD_BY_SUM 124 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'', 125 thm2, STABLE_CONV t2', STABLE_CONV t2'']) 126 handle HOL_ERR _ => failwith "stable conditions not satisfied" 127 end 128 else if is_par tm then 129 let val (t1, t2) = args_par tm; 130 val thm1 = c t1 131 and thm2 = c t2 132 in 133 MATCH_MP WEAK_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2) 134 end 135 else if is_restr tm then 136 let val (P, L) = args_restr tm; 137 val thm = c P 138 in 139 ISPEC L (MATCH_MP WEAK_EQUIV_SUBST_RESTR thm) 140 end 141 else if is_relab tm then 142 let val (P, rf) = args_relab tm; 143 val thm = c P 144 in 145 ISPEC rf (MATCH_MP WEAK_EQUIV_SUBST_RELAB thm) 146 end 147 else 148 OE_ALL_CONV tm; 149 150(* Define the function OE_DEPTH_CONV. *) 151fun OE_DEPTH_CONV (c: conv) t = 152 OE_SUB_CONV ((OE_DEPTH_CONV c) OE_THENC (OE_REPEATC c)) t; 153 154(* Define the function OE_TOP_DEPTH_CONV. *) 155fun OE_TOP_DEPTH_CONV (c: conv) t = 156 ((OE_REPEATC c) OE_THENC 157 (OE_SUB_CONV (OE_TOP_DEPTH_CONV c)) OE_THENC 158 ((c OE_THENC (OE_TOP_DEPTH_CONV c)) OE_ORELSEC OE_ALL_CONV)) 159 t; 160 161(* Define the function OE_SUBST for substitution in WEAK_EQUIV terms. *) 162fun OE_SUBST thm tm = let 163 val (ti, ti') = args_thm thm 164in 165 if tm ~~ ti then thm 166 else if is_prefix tm then 167 let val (u, t) = args_prefix tm; 168 val thm1 = OE_SUBST thm t 169 in 170 ISPEC u (MATCH_MP WEAK_EQUIV_SUBST_PREFIX thm1) 171 end 172 else if is_sum tm then 173 let val (t1, t2) = args_sum tm; 174 val thm1 = OE_SUBST thm t1 175 and thm2 = OE_SUBST thm t2; 176 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *) 177 and (t2', t2'') = args_thm thm2 178 in 179 if (t1' ~~ t1'') andalso (t2' ~~ t2'') then 180 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL 181 else if (t1' ~~ t1'') then 182 ISPEC t1' (MATCH_MP WEAK_EQUIV_SUBST_SUM_L 183 (LIST_CONJ [thm2, STABLE_CONV t2', STABLE_CONV t2''])) 184 else if (t2' ~~ t2'') then 185 ISPEC t2' (MATCH_MP WEAK_EQUIV_SUBST_SUM_R 186 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1''])) 187 else 188 MATCH_MP WEAK_EQUIV_PRESD_BY_SUM 189 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'', 190 thm2, STABLE_CONV t2', STABLE_CONV t2'']) 191 handle HOL_ERR _ => 192 failwith "stable conditions not satisfied" 193 end 194 else if is_par tm then 195 let val (t1, t2) = args_par tm; 196 val thm1 = OE_SUBST thm t1 197 and thm2 = OE_SUBST thm t2 198 in 199 MATCH_MP WEAK_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2) 200 end 201 else if is_restr tm then 202 let val (t, L) = args_restr tm; 203 val thm1 = OE_SUBST thm t 204 in 205 ISPEC L (MATCH_MP WEAK_EQUIV_SUBST_RESTR thm1) 206 end 207 else if is_relab tm then 208 let val (t, rf) = args_relab tm; 209 val thm1 = OE_SUBST thm t 210 in 211 ISPEC rf (MATCH_MP WEAK_EQUIV_SUBST_RELAB thm1) 212 end 213 else 214 OE_ALL_CONV tm 215end; 216 217(* Define the tactic OE_LHS_SUBST1_TAC: thm_tactic which substitutes a theorem 218 in the left-hand side of an observation equivalence. *) 219fun OE_LHS_SUBST1_TAC thm :tactic = 220 fn (asl, w) => let 221 val (opt, t1, t2) = args_equiv w 222 in 223 if opt ~~ mk_const ("WEAK_EQUIV", type_of opt) then 224 let val thm' = OE_SUBST thm t1; 225 val (t1', t') = args_thm thm' (* t1' = t1 *) 226 in 227 if (t' ~~ t2) then 228 ([], fn [] => OE_TRANS thm' (ISPEC t' WEAK_EQUIV_REFL)) 229 else 230 ([(asl, ``WEAK_EQUIV ^t' ^t2``)], fn [thm''] => OE_TRANS thm' thm'') 231 end 232 else 233 failwith "the goal is not an WEAK_EQUIV relation" 234 end; 235 236(* The tactic OE_LHS_SUBST_TAC substitutes a list of theorems in the left-hand 237 side of an observation equivalence. *) 238fun OE_LHS_SUBST_TAC thmlist = EVERY (map OE_LHS_SUBST1_TAC thmlist); 239 240(* The tactic OE_RHS_SUBST1_TAC substitutes a theorem in the right-hand side 241 of an observation equivalence. *) 242fun OE_RHS_SUBST1_TAC thm = 243 REPEAT GEN_TAC 244 >> RULE_TAC WEAK_EQUIV_SYM 245 >> OE_LHS_SUBST1_TAC thm 246 >> RULE_TAC WEAK_EQUIV_SYM; 247 248(* The tactic OE_RHS_SUBST_TAC substitutes a list of theorems in the right-hand 249 side of an observation equivalence. *) 250fun OE_RHS_SUBST_TAC thmlist = 251 REPEAT GEN_TAC 252 >> RULE_TAC WEAK_EQUIV_SYM 253 >> OE_LHS_SUBST_TAC thmlist 254 >> RULE_TAC WEAK_EQUIV_SYM; 255 256(* The tactic OE_SUBST1_TAC (OE_SUBST_TAC) substitutes a (list of) theorem(s) 257 in both sides of an observation equivalence. *) 258fun OE_SUBST1_TAC thm = 259 OE_LHS_SUBST1_TAC thm 260 >> OE_RHS_SUBST1_TAC thm; 261 262fun OE_SUBST_TAC thmlist = 263 OE_LHS_SUBST_TAC thmlist 264 >> OE_RHS_SUBST_TAC thmlist; 265 266end (* struct *) 267 268(* last updated: Jun 18, 2017 *) 269