1structure abstraction :> abstraction = 2struct 3 4open HolKernel Parse boolLib; 5infix o |->; 6 7fun ABS_ERR function message = 8 HOL_ERR{origin_structure = "abs_tools", 9 origin_function = function, 10 message = message}; 11 12val curr_assums = ref ([]:term list); 13val fv_ass = ref ([]:term list); 14 15 16fun add_parameter v = 17 let val _ = dest_var v in 18 fv_ass := v :: !fv_ass 19 end; 20 21fun get_assums () = !curr_assums; 22 23fun set_assums asl = 24 (curr_assums := asl; 25 fv_ass := free_varsl asl) 26; 27 28fun add_assums asl = 29 (curr_assums := rev asl @ !curr_assums; 30 fv_ass := subtract (free_varsl asl) (!fv_ass) @ !fv_ass) 31; 32 33 34fun select_disch (h,th) = 35 if HOLset.member(hypset th, h) then DISCH h th 36 else th; 37 38(* Only the variables appearing in the discharged hypothese should 39 * be generalized. 40 *) 41fun gen_assums thm = 42 GENL (!fv_ass) (foldr select_disch thm (!curr_assums)); 43 44 45 46val impl_param_cstr = ref ([]:(string * term list) list); 47fun add_impl_param x p = 48 impl_param_cstr := (x,p)::(!impl_param_cstr); 49fun impl_of x = 50 map Absyn.mk_AQ (assoc x (!impl_param_cstr)) handle HOL_ERR _ => [] 51 52 53 54fun head tm = 55 let val a = fst(strip_comb(lhs 56 (snd(strip_forall(Lib.trye hd (strip_conj tm)))))) 57 in 58 fst(dest_var a handle HOL_ERR _ => dest_const a) 59 end; 60 61fun param_eq eqs0 = 62 let val nm = head eqs0 63 val eqs = map (snd o strip_forall) (strip_conj eqs0) 64 val fvrhs = subtract (free_varsl (map rhs eqs)) (free_varsl (map lhs eqs)) 65 val pv = filter (C mem fvrhs) (!fv_ass) 66 val ty = type_of(fst(strip_comb(lhs(hd eqs)))) 67 val old_var = mk_var(nm, ty) 68 val newvar = mk_var(nm, foldr (op -->) ty (map type_of pv)) 69 val _ = if null pv then () else add_impl_param nm pv 70 in subst [old_var |-> list_mk_comb(newvar,pv)] eqs0 71 end; 72 73fun new_param_definition (x,tm) = new_definition(x, param_eq tm); 74 75 76 77(* Instantiating variables such that general constants can be replaced by 78 * the local constants. 79 * Could be improved (both in efficiency and soundness!). 80 *) 81 82fun is_defd sub v = exists (fn {redex,residue} => v=redex) sub; 83 84fun except_assoc x [] = raise ABS_ERR "except_assoc" "" 85 | except_assoc x ((s as {redex,residue})::l) = 86 if x=redex then (residue,l) 87 else 88 let val (v,nsub) = except_assoc x l in 89 (v,s::nsub) 90 end 91; 92 93fun majo NONE o2 = o2 94 | majo o1 NONE = o1 95 | majo (SOME x1) (SOME x2) = 96 if x1=x2 then (SOME x1) 97 else raise ABS_ERR "under_conj" 98 "vars were instantiated differently in conjuncts" 99; 100 101fun under_conj f th = 102 case (f (CONJUNCT1 th), f (CONJUNCT2 th)) of 103 ((NONE, _),(NONE, _)) => (NONE, th) 104 | ((o1,th1),(o2,th2)) => (majo o1 o2, CONJ th1 th2) 105; 106 107 108fun under_forall f th = 109 let val qvars = fst(strip_forall(concl th)) 110 val thm = SPECL qvars th 111 val (ovars,rthm) = f thm in 112 case ovars of 113 SOME (ivars,ti) => 114 let val (rsub,thm) = 115 foldr (fn (x,(sub,th)) => 116 let val (v,nsub) = except_assoc (inst ti x) sub in 117 (nsub,SPEC v (GEN (inst ti x) th)) 118 end 119 handle HOL_ERR _ => (sub,GEN (inst ti x) th)) (ivars,rthm) qvars 120 in (SOME (rsub,ti), thm) 121 end 122 | NONE => (NONE,th) 123 end 124; 125 126fun under_all f th = 127 if is_forall (concl th) then under_forall (under_all f) th 128 else if is_conj (concl th) then under_conj (under_all f) th 129 else f th 130; 131 132 133fun first_match env mfun [] = raise ABS_ERR "first_match" "no match" 134 | first_match env mfun (x::l) = 135 (let val (vi,ti) = mfun x in 136 if exists (fn {redex,residue} => mem redex env) vi then 137 raise ABS_ERR "" "" 138 else (vi,ti) 139 end 140 handle HOL_ERR _ => first_match env mfun l) 141; 142 143 144fun inst_csts inst env tm = 145 case dest_term tm of 146 LAMB(Bvar,Body) => inst_csts inst (Bvar::env) Body 147 | COMB(Rator,Rand) => 148 (SOME (first_match env (match_term tm) inst) 149 handle HOL_ERR _ => 150 (case inst_csts inst env Rand of 151 SOME i => SOME i 152 | NONE => inst_csts inst env Rator)) 153 | _ => NONE 154; 155 156 157fun inst_thm inst thm = 158 case inst_csts inst [] (concl thm) of 159 NONE => (NONE,thm) 160 | SOME(vi,ti) => (SOME (vi,ti), INST_TYPE ti thm) 161; 162 163fun inst_all ctab thm = 164 let val (osub,thm) = under_all (inst_thm ctab) thm in 165 case osub of 166 SOME (sub,ti) => 167 foldl (fn ({redex,residue},th) => SPEC residue (GEN redex th)) 168 thm sub 169 | NONE => thm 170 end 171 handle HOL_ERR _ => thm; 172 173(* example: 174 inst_all [--`0+0`--,--`0-0`--] 175 (GEN_ALL(CONJ(GEN (--`y:num`--) (REFL(--` x+y = x-y `--))) 176 (REFL(--`z`--)))) 177 ; 178*) 179 180 181fun inst_hyp (h,thm) = 182 MATCH_MP thm h 183 handle HOL_ERR _ => thm 184; 185 186fun import_fun inst thm = 187 foldl inst_hyp thm inst 188; 189 190 191(*----------------*) 192 193type inst_infos = 194 { Vals : term list, 195 Inst : thm list, 196 Rule : thm -> thm, 197 Rename : string -> string option }; 198 199type cinst_infos = 200 { Inst : thm list, Rule : thm -> thm, Csts : term list, Defs : thm list }; 201 202 203fun compute_inst_infos ctab ({Rename,Inst,Rule,...}:inst_infos) = 204 let fun mk_def tm = 205 case Rename(#Name(dest_thy_const(fst(strip_comb tm)))) of 206 SOME name => SOME(name^"_def", mk_eq(mk_var(name,type_of tm),tm)) 207 | NONE => NONE 208 val defs = List.mapPartial mk_def ctab 209 val thms = map (GSYM o new_param_definition) defs 210 in { Csts=ctab, Defs=thms, Inst=Inst, Rule=Rule } 211 end; 212 213fun inst_thm_fun { Inst=inst, Rule=f, Csts=ctab, Defs=thms } = 214 f o REWRITE_RULE thms o inst_all ctab o import_fun inst 215; 216 217 218(* --> abs_tools ? *) 219 220val pr_list_sep = PP.pr_list 221 222val S = PP.add_string; 223val NL = PP.add_newline; 224val N = PP.add_string o int_to_string; 225val SPC = PP.add_break(1,0) 226val B = PP.block PP.CONSISTENT 0 227 228 229val functor_header = [S "fun IMPORT P =", NL] 230; 231 232fun compute_cst_arg_map (fv,impargs) = 233 let val thcsts = map (#Name o dest_thy_const) (constants(current_theory())) 234 fun is_param_cst (x,iargs) = 235 mem x thcsts andalso all (C mem fv) iargs 236 val ptab = filter is_param_cst impargs 237 val pr_var = S o fst o dest_var 238 val sep = [S ",", NL, S " "] 239 in 240 B [ 241 S " let open Parse abstraction", NL, 242 S " fun sing [x] = x | sing _ = raise Match", NL, 243 S " val ", 244 B (pr_list_sep pr_var [S","] (!fv_ass)), 245 S " = sing (#Vals P)", NL, 246 S " val ctab =", NL, 247 S " [ ", 248 B (pr_list_sep (fn (x,iargs) => 249 B [ 250 S ("Term`"^x^" "), 251 B (pr_list_sep (fn v => S ("^"^fst(dest_var v))) 252 [S " "] iargs), 253 S "`" 254 ]) 255 sep ptab), 256 S " ]", NL, 257 S " val inst_fun = inst_thm_fun (compute_inst_infos ctab P) in", 258 NL] 259 end 260; 261 262fun export_param_theory () = let 263 val _ = Theory.scrub() 264 val defs = rev (map fst (definitions"-")) 265 val thms = rev (map fst (theorems"-")) 266 fun struct_line thn = B [S thn, SPC, S "= inst_fun ", S thn] 267 fun sig_line thn = B [S thn, S " : thm"] 268 val sep = [S ",", NL, S " "] 269 val adj = { 270 sig_ps = 271 SOME (fn _ => B[ 272 S "val IMPORT : abstraction.inst_infos ->", NL, 273 S " { ", 274 B (pr_list_sep sig_line [S ",", SPC] (defs@thms)), 275 S " }", NL 276 ]), 277 struct_ps = 278 SOME (fn _ => B ( 279 functor_header @ 280 [compute_cst_arg_map (!fv_ass, !impl_param_cstr), 281 S " { ", 282 B (pr_list_sep struct_line sep (defs@thms)), 283 S " }", NL, 284 S " end", NL])) 285 } 286in 287 adjoin_to_theory adj; 288 export_theory() 289end; 290 291 292end; 293