193 let |
193 let |
194 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
194 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
195 in |
195 in |
196 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
196 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
197 end; |
197 end; |
|
198 |
198 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); |
199 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); |
199 val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees |
200 val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees |
200 val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; |
201 val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; |
201 val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs); |
202 val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs); |
202 in |
203 in |
240 map2 fv_constr constrs bclausess |
241 map2 fv_constr constrs bclausess |
241 end |
242 end |
242 *} |
243 *} |
243 |
244 |
244 ML {* |
245 ML {* |
245 fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy = |
246 fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy = |
246 let |
247 let |
247 val thy = ProofContext.theory_of lthy; |
248 val thy = ProofContext.theory_of lthy; |
248 |
249 |
249 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
250 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
250 val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; |
251 val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; |
251 val fv_frees = map Free (fv_names ~~ fv_types); |
252 val fv_frees = map Free (fv_names ~~ fv_types); |
252 |
253 |
253 (* free variables for the bn-functions *) |
254 (* free variables for the bn-functions *) |
254 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
255 val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) = |
255 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
256 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
256 |
257 |
|
258 val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map)) |
257 |
259 |
258 val fv_bns = map snd bn_fvbn; |
260 val fv_bns = map snd bn_fvbn_map; |
259 val fv_nums = 0 upto (length fv_frees - 1) |
261 val fv_nums = 0 upto (length fv_frees - 1) |
260 |
262 |
261 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums); |
263 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums); |
262 |
264 |
263 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
265 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
264 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
266 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
265 |
267 |
266 fun pat_completeness_auto ctxt = |
268 fun pat_completeness_auto ctxt = |
282 val fs_exp = map (Morphism.term morphism) fs |
284 val fs_exp = map (Morphism.term morphism) fs |
283 |
285 |
284 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
286 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
285 val simps_exp = Morphism.fact morphism (the simps) |
287 val simps_exp = Morphism.fact morphism (the simps) |
286 in |
288 in |
287 ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'') |
289 (fv_frees_exp, fv_bns_exp, simps_exp, lthy'') |
288 end |
290 end |
289 *} |
291 *} |
290 |
292 |
291 end |
293 end |