1structure Opening :> Opening = 2struct 3 4open HolKernel boolLib liteLib Trace; 5 6 7fun samerel t1 t2 = can (match_term t1) t2 8 9type congproc = {relation:term, 10 solver : term -> thm, 11 freevars: term list, 12 depther : thm list * term -> conv} -> conv 13 14 15fun WRAP_ERR x = STRUCT_WRAP "Opening" x; 16fun ERR x = STRUCT_ERR "Opening" x; 17 18(* --------------------------------------------------------------------- 19 * is_congruence 20 * Test if a term is a valid conclusion of a congruence rule, 21 * 22 * EXAMPLES 23 * is_congruence (--`(A ==> B) = (A' ==> B')`--); 24 * is_congruence (--`(A ==> B) ==> (A' ==> B')`--); 25 * is_congruence (--`(A ==> B) <== (A' ==> B')`--); 26 * is_congruence (--`(!x:'a. P x) <== (!x:'a. P' x)`--); 27 * is_congruence (--`(A <== A') ==> (A ==> B) ==> (A' ==> B')`--); (*false*) 28 * 29 * rel_of_congruence 30 * Discover the relation a congruence is expressed over. 31 * 32 * EXAMPLES 33 * rel_of_congrule imp_imp_rule; 34 * rel_of_congrule imp_pmi_rule; 35 * rel_of_congrule pmi_imp_rule; 36 * rel_of_congrule pmi_neg_rule; 37 * rel_of_congrule imp_forall_rule; 38 * 39 * nconds_of_congrule 40 * Discover how many side conditions a congruence rule has. Nb. Can't 41 * just call strip_imp as the congruence may be expressed over (--`$==>`--) 42 * 43 * nconds_of_congrule imp_imp_rule; (* 2 *) 44 * nconds_of_congrule imp_pmi_rule; (* 2 *) 45 * nconds_of_congrule pmi_imp_rule; (* 2 *) 46 * nconds_of_congrule pmi_neg_rule; (* 1 *) 47 * nconds_of_congrule pmi_forall_rule; (* 1 *) 48 * nconds_of_congrule imp_forall_rule; (* 1 *) 49 * ---------------------------------------------------------------------*) 50 51fun dest_binop t = let 52 val (fx,y) = dest_comb t 53 val (f,x) = dest_comb fx 54in 55 (f,x,y) 56end 57 58fun is_congruence tm = 59 is_eq tm orelse let 60 val (rel,left,right) = dest_binop tm 61 in 62 (can (ho_match_term [] empty_tmset left) right) andalso 63 (can (ho_match_term [] empty_tmset right) left) 64 end 65 handle HOL_ERR _ => false 66 67fun rel_of_congrule thm = let 68 fun aux tm = if is_congruence tm then #1 (dest_binop tm) 69 else aux (snd (dest_imp tm)) 70in 71 aux (snd(strip_forall (concl thm))) 72end handle e => WRAP_ERR("rel_of_congrule",e) 73 74fun nconds_of_congrule thm = let 75 fun aux tm = if is_congruence tm then 0 else aux (snd(dest_imp tm)) + 1 76in 77 aux (snd(strip_forall(concl thm))) 78end handle e => WRAP_ERR("nconds_of_congrule",e) 79 80(* --------------------------------------------------------------------- 81 * CONGPROC : REFL -> congrule -> congproc 82 * 83 * ---------------------------------------------------------------------*) 84 85fun strip_n_imp 0 tm = ([],tm) 86 | strip_n_imp n tm = 87 let val (x,y) = dest_imp tm 88 val (z,w) = strip_n_imp (n-1) y 89 in (x::z,w) 90 end; 91 92(* --------------------------------------------------------------------- 93 * strip_imp_until_rel 94 * 95 * this function strips implications off a sub-congruence until 96 * it is a relation (i.e. the rhs is one of the genvars we have chosen) 97 * or it is no longer an implication (in which case the sub-congruence 98 * is really a side condition. 99 * 100 * ---------------------------------------------------------------------*) 101 102 103fun strip_imp_until_rel genvars tm = 104 (if (is_var (rand tm) andalso mem (rand tm) genvars) 105 then ([],tm) 106 else let val (x,y) = dest_imp tm 107 val (z,w) = strip_imp_until_rel genvars y 108 in (x::z,w) 109 end) 110 handle HOL_ERR _ => ([],tm); 111 112(* --------------------------------------------------------------------- 113 * CONGPROC : REFL -> congrule -> congproc 114 * 115 * ---------------------------------------------------------------------*) 116 117val equality = boolSyntax.equality 118 119fun CONGPROC refl congrule = 120let 121 122 (* this discharges each antecedent of the congruence rule. Each 123 antecedent is either a side condition or a sub-congruence. 124 Side conditions must be passed to the solver, sub-congruences 125 must be passed to the depther. *) 126 127 val congrule' = GSPEC (GEN_ALL congrule) 128 val nconds = nconds_of_congrule congrule' 129 val rel = rel_of_congrule congrule' 130 131 val (conditions,conc) = strip_n_imp nconds (concl congrule') 132 val matcher = 133 HO_PART_MATCH (rator o snd o strip_n_imp nconds) congrule' 134 135 (* work out whether context assumptions need to be reprocessed *) 136 (* e.g "~g" in the "else" branch of COND_CONG needs to be. *) 137 138 val vars = free_vars (concl congrule') 139 fun reprocess_flag assum = if is_var assum then false else true; 140 val reprocess_flags = 141 map (map reprocess_flag o fst o strip_imp_until_rel vars o 142 #2 o strip_forall) 143 conditions 144 145in fn {relation,solver,depther,freevars} => 146 if not (samerel rel relation) andalso not (same_const rel relation) then 147 failwith "not applicable" 148 else fn tm => 149 let 150 val theta = match_type (#1 (dom_rng (type_of relation))) (type_of tm) 151 val relation' = Term.inst theta relation 152 val match_thm = matcher (mk_comb(relation',tm)) 153 val _ = trace(3,OPENING(tm,match_thm)) 154 val (_,conc) = strip_n_imp nconds (concl match_thm) 155 val genvars = filter is_genvar (free_vars (rand conc)) 156 157 (* this function does all the work of solving the side conditions 158 one by one. The integer is the number of side conditions 159 remaining to be discharged. Most of the side conditions 160 will be sub-congruences of the form (--`A = ?A`--) *) 161 162 fun process_subgoals (0,match_thm,_) = match_thm 163 | process_subgoals (_,_,[]) = raise Fail "process_subgoals BIND" 164 | process_subgoals (n,match_thm,flags::more_flags) = 165 let val condition = #1 (dest_imp (concl match_thm)) 166 167 (* work out whether the condition is a congruence condition 168 or a side condition. If it is two place and the 169 head combinator of the rhs is one of the subterms 170 in the congruence (see subterms above) then it 171 is a congruence condition *) 172 val (ho_vars,bdy1) = strip_forall condition 173 val (assums,bdy2) = strip_imp_until_rel genvars bdy1 174 val (oper,args) = let 175 val (f,x,y) = dest_binop bdy2 176 in 177 (f,[x,y]) 178 end handle HOL_ERR _ => strip_comb bdy2 179 in 180 if length args = 2 andalso mem (#1 (strip_comb (el 2 args))) genvars 181 then let 182 val (orig,res) = case args of [x,y] => (x,y) | _ => raise Bind 183 val genv = #1 (strip_comb res) 184 val assum_thms = map ASSUME assums 185 fun reprocess thm flag = 186 if flag then CONV_RULE (depther ([],equality)) thm 187 handle HOL_ERR _ => 188 (trace(5,PRODUCE(concl thm,"UNCHANGED",thm));thm) 189 else thm 190 val reprocessed_assum_thms = map2 reprocess assum_thms flags 191 val rewr_thm = 192 (depther (reprocessed_assum_thms,oper) orig) 193 handle HOL_ERR _ => 194 let val thm = refl {Rinst = oper, arg = orig} 195 in (trace(5,PRODUCE(orig,"UNCHANGED",thm));thm) 196 end 197 val abs_rewr_thm = 198 CONV_RULE (RAND_CONV (MK_ABSL_CONV ho_vars)) rewr_thm 199 val disch_abs_rewr_thm = itlist DISCH assums abs_rewr_thm 200 val gen_abs_rewr_thm = GENL ho_vars disch_abs_rewr_thm 201 val gen_abs_res = 202 funpow (length ho_vars) rator (rand (concl abs_rewr_thm)) 203 val spec_match_thm = SPEC gen_abs_res (GEN genv match_thm) 204 val new_match_thm = MP spec_match_thm gen_abs_rewr_thm 205 in process_subgoals (n-1,new_match_thm,more_flags) 206 end 207 else let 208 fun output() = 209 "Instantiated congruence condition is a side condition: "^ 210 term_to_string condition 211 val _ = trace (6, LZ_TEXT output) 212 val side_condition_thm = solver condition 213 val new_match_thm = MP match_thm side_condition_thm 214 in process_subgoals (n-1,new_match_thm,more_flags) 215 end 216 end 217 218 val final_thm = process_subgoals (nconds,match_thm,reprocess_flags) 219 220 in 221 if (rand (rator (concl final_thm)) = rand (concl final_thm)) 222 then raise HOL_ERR { origin_structure = "Opening", 223 origin_function = "CONGPROC", 224 message = "Congruence gives no change" } 225 else (trace(3,PRODUCE(tm,"congruence rule",final_thm)); final_thm) 226 end 227end; 228 229 230(* --------------------------------------------------------------------- 231 * EQ_CONGPROC 232 * 233 * Opening through HOL terms under HOL equality. 234 * ---------------------------------------------------------------------*) 235 236fun EQ_CONGPROC {relation,depther,solver,freevars} tm = 237 if not (same_const relation boolSyntax.equality) then failwith "not applicable" 238 else 239 case dest_term tm 240 of COMB(Rator,Rand) => 241 (let val th = depther ([],equality) Rator 242 in MK_COMB (th, depther ([],equality) Rand) 243 handle HOL_ERR _ => AP_THM th Rand 244 end 245 handle HOL_ERR _ => AP_TERM Rator (depther ([],equality) Rand)) 246 | LAMB(Bvar,Body) => 247 if mem Bvar freevars then 248 let val v = variant (freevars@free_vars Body) Bvar 249 val th1 = ALPHA_CONV v tm handle e as HOL_ERR _ 250 => (trace(0,REDUCE("SIMPLIFIER ERROR: bug when alpha converting",tm)); 251 trace(0,REDUCE("trying to alpha convert to",v)); 252 Raise e) 253 val rhs' = rhs(concl th1) 254 val Body' = body rhs' (* v = Bvar *) 255 val body_thm = depther ([],equality) Body' 256 val eq_thm' = ABS v body_thm 257 in 258 TRANS th1 eq_thm' 259 end 260 else let val _ = trace(4,TEXT "no alpha conversion") 261 val Bth = depther ([],equality) Body 262 in ABS Bvar Bth 263 end 264 | _ => failwith "unchanged"; 265 266 267end (* struct *) 268