1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6structure StrongEQLib :> StrongEQLib = 7struct 8 9open HolKernel Parse boolLib bossLib; 10 11open IndDefRules; 12open CCSLib CCSTheory CCSSyntax StrongEQTheory; 13 14infixr 0 S_THENC S_ORELSEC; 15 16(******************************************************************************) 17(* *) 18(* Basic functions and conversions for rewriting with *) 19(* the CCS laws for strong equivalence (basic_fun.ml) *) 20(* *) 21(******************************************************************************) 22 23(* Define S_SYM such that, when given a theorem A |- STRONG_EQUIV t1 t2, 24 returns the theorem A |- STRONG_EQUIV t2 t1. *) 25fun S_SYM thm = MATCH_MP STRONG_EQUIV_SYM thm; 26 27(* Define S_TRANS such that, when given the theorems thm1 and thm2, applies 28 STRONG_EQUIV_TRANS on them, if possible. *) 29fun S_TRANS thm1 thm2 = 30 if rhs_tm thm1 ~~ lhs_tm thm2 then 31 MATCH_MP STRONG_EQUIV_TRANS (CONJ thm1 thm2) 32 else 33 failwith "transitivity of strong equivalence not applicable"; 34 35(* When applied to a term "t: CCS", the conversion S_ALL_CONV returns the 36 theorem: |- STRONG_EQUIV t t *) 37fun S_ALL_CONV t = ISPEC t STRONG_EQUIV_REFL; 38 39fun op S_THENC ((c1, c2) :conv * conv) :conv = 40 fn t => let 41 val thm1 = c1 t; 42 val thm2 = c2 (rhs_tm thm1) 43 in 44 S_TRANS thm1 thm2 45 end; 46 47fun op S_ORELSEC ((c1, c2) :conv * conv) :conv = 48 fn t => c1 t handle HOL_ERR _ => c2 t; 49 50fun S_REPEATC (c :conv) (t :term) :thm = 51 ((c S_THENC (S_REPEATC c)) S_ORELSEC S_ALL_CONV) t; 52 53(* Convert a conversion for the application of the laws for STRONG_EQUIV to a tactic. *) 54fun S_LHS_CONV_TAC (c :conv) :tactic = 55 fn (asl, w) => let 56 val (opt, t1, t2) = args_equiv w 57 in 58 if opt ~~ ``STRONG_EQUIV`` then 59 let 60 val thm = c t1 61 val (t1', t') = args_thm thm (* t1' = t1 *) 62 in 63 if t' ~~ t2 then ([], fn _ => S_TRANS thm (ISPEC t' STRONG_EQUIV_REFL)) 64 else 65 ([(asl, ``STRONG_EQUIV ^t' ^t2``)], 66 fn ths => 67 case ths of [thm'] => S_TRANS thm thm' 68 | _ => failwith "S_LHS_CONV_TAC: weird!") 69 end 70 else 71 failwith "the goal is not a STRONG_EQUIV relation" 72 end; 73 74fun S_RHS_CONV_TAC (c :conv) :tactic = 75 fn (asl, w) => let 76 val (opt, t1, t2) = args_equiv w 77 in 78 if (opt ~~ ``STRONG_EQUIV``) then 79 let val thm = c t2; 80 val (t2', t'') = args_thm thm (* t2' = t2 *) 81 in 82 if t'' ~~ t1 then ([], fn _ => S_SYM thm) 83 else 84 ([(asl, ``STRONG_EQUIV ^t1 ^t''``)], 85 fn [thm'] => S_TRANS thm' (S_SYM thm)) 86 end 87 else 88 failwith "the goal is not a STRONG_EQUIV relation" 89 end; 90 91(******************************************************************************) 92(* *) 93(* Basic conversions and tactics for applying the laws for *) 94(* strong equivalence *) 95(* *) 96(******************************************************************************) 97 98fun S_SUB_CONV (c :conv) tm = 99 if is_prefix tm then 100 let val (u, P) = args_prefix tm; 101 val thm = c P 102 in 103 ISPEC u (MATCH_MP STRONG_EQUIV_SUBST_PREFIX thm) 104 end 105 else if is_sum tm then 106 let val (t1, t2) = args_sum tm; 107 val thm1 = c t1 108 and thm2 = c t2 109 in 110 MATCH_MP STRONG_EQUIV_PRESD_BY_SUM (CONJ thm1 thm2) 111 end 112 else if is_par tm then 113 let val (t1, t2) = args_par tm; 114 val thm1 = c t1 115 and thm2 = c t2 116 in 117 MATCH_MP STRONG_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2) 118 end 119 else if is_restr tm then 120 let val (P, L) = args_restr tm; 121 val thm = c P 122 in 123 ISPEC L (MATCH_MP STRONG_EQUIV_SUBST_RESTR thm) 124 end 125 else if is_relab tm then 126 let val (P, rf) = args_relab tm; 127 val thm = c P 128 in 129 ISPEC rf (MATCH_MP STRONG_EQUIV_SUBST_RELAB thm) 130 end 131 else 132 S_ALL_CONV tm; 133 134fun S_DEPTH_CONV (c :conv) t = 135 S_SUB_CONV ((S_DEPTH_CONV c) S_THENC (S_REPEATC c)) t; 136 137fun S_TOP_DEPTH_CONV (c :conv) t = 138 ((S_REPEATC c) S_THENC 139 (S_SUB_CONV (S_TOP_DEPTH_CONV c)) S_THENC 140 ((c S_THENC (S_TOP_DEPTH_CONV c)) S_ORELSEC S_ALL_CONV)) 141 t; 142 143(* Define the function S_SUBST for substitution in STRONG_EQUIV terms. *) 144fun S_SUBST thm tm :thm = let 145 val (ti, ti') = args_thm thm 146in 147 if tm ~~ ti then thm 148 else if is_prefix tm then 149 let val (u, t) = args_prefix tm; 150 val thm1 = S_SUBST thm t 151 in 152 ISPEC u (MATCH_MP STRONG_EQUIV_SUBST_PREFIX thm1) 153 end 154 else if is_sum tm then 155 let val (t1, t2) = args_sum tm; 156 val thm1 = S_SUBST thm t1 157 and thm2 = S_SUBST thm t2 158 in 159 MATCH_MP STRONG_EQUIV_PRESD_BY_SUM (CONJ thm1 thm2) 160 end 161 else if is_par tm then 162 let val (t1, t2) = args_par tm; 163 val thm1 = S_SUBST thm t1 164 and thm2 = S_SUBST thm t2 165 in 166 MATCH_MP STRONG_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2) 167 end 168 else if is_restr tm then 169 let val (t, L) = args_restr tm; 170 val thm1 = S_SUBST thm t 171 in 172 ISPEC L (MATCH_MP STRONG_EQUIV_SUBST_RESTR thm1) 173 end 174 else if is_relab tm then 175 let val (t, rf) = args_relab tm; 176 val thm1 = S_SUBST thm t 177 in 178 ISPEC rf (MATCH_MP STRONG_EQUIV_SUBST_RELAB thm1) 179 end 180 else 181 S_ALL_CONV tm 182end; 183 184(* Define the tactic S_LHS_SUBST1_TAC: thm_tactic which substitutes a theorem 185 in the left-hand side of a strong equivalence. *) 186fun S_LHS_SUBST1_TAC thm :tactic = 187 fn (asl, w) => let 188 val (opt, t1, t2) = args_equiv w 189 in 190 if (opt ~~ ``STRONG_EQUIV``) then 191 let val thm' = S_SUBST thm t1; 192 val (t1', t') = args_thm thm' (* t1' = t1 *) 193 in 194 if t' ~~ t2 then 195 ([], fn [] => S_TRANS thm' (ISPEC t' STRONG_EQUIV_REFL)) 196 else 197 ([(asl, ``STRONG_EQUIV ^t' ^t2``)], 198 fn [thm''] => S_TRANS thm' thm'') 199 end 200 else 201 failwith "the goal is not a STRONG_EQUIV relation" 202 end; 203 204(* The tactic S_LHS_SUBST_TAC substitutes a list of theorems in the left-hand 205 side of a strong equivalence. *) 206fun S_LHS_SUBST_TAC thmlist = EVERY (map S_LHS_SUBST1_TAC thmlist); 207 208(* The tactic S_RHS_SUBST1_TAC substitutes a theorem in the right-hand side of 209 a strong equivalence. *) 210fun S_RHS_SUBST1_TAC thm = 211 REPEAT GEN_TAC 212 >> RULE_TAC STRONG_EQUIV_SYM 213 >> S_LHS_SUBST1_TAC thm 214 >> RULE_TAC STRONG_EQUIV_SYM; 215 216(* The tactic S_RHS_SUBST_TAC substitutes a list of theorems in the right-hand 217 side of a strong equivalence. *) 218fun S_RHS_SUBST_TAC thmlist = 219 REPEAT GEN_TAC 220 >> RULE_TAC STRONG_EQUIV_SYM 221 >> S_LHS_SUBST_TAC thmlist 222 >> RULE_TAC STRONG_EQUIV_SYM; 223 224(* The tactic S_SUBST1_TAC (S_SUBST_TAC) substitutes a (list of) theorem(s) in 225 both sides of a strong equivalence. *) 226fun S_SUBST1_TAC thm = 227 S_LHS_SUBST1_TAC thm 228 >> S_RHS_SUBST1_TAC thm; 229 230fun S_SUBST_TAC thmlist = 231 S_LHS_SUBST_TAC thmlist 232 >> S_RHS_SUBST_TAC thmlist; 233 234end (* struct *) 235 236(* last updated: May 14, 2017 *) 237