22 val mk_atom_fset: term -> term |
22 val mk_atom_fset: term -> term |
23 |
23 |
24 val setify: Proof.context -> term -> term |
24 val setify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
26 |
26 |
27 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
27 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
28 bclause list list list -> thm list -> Proof.context -> |
28 thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
29 term list * term list * thm list * thm list * local_theory |
|
30 |
29 |
31 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
30 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
32 end |
31 end |
33 |
32 |
34 |
33 |
209 val nth_bclausess = nth bclausesss bn_n |
208 val nth_bclausess = nth bclausesss bn_n |
210 in |
209 in |
211 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
210 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
212 end |
211 end |
213 |
212 |
214 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = |
213 fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy = |
215 let |
214 let |
216 val fv_names = prefix_dt_names descr sorts "fv_" |
215 val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names |
217 val fv_arg_tys = all_dtyps descr sorts |
216 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys |
218 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
|
219 val fv_frees = map Free (fv_names ~~ fv_tys); |
217 val fv_frees = map Free (fv_names ~~ fv_tys); |
220 val fv_map = fv_arg_tys ~~ fv_frees |
218 val fv_map = raw_tys ~~ fv_frees |
221 |
219 |
222 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
220 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
223 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
221 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
224 val fv_bn_names = map (prefix "fv_") bn_names |
222 val fv_bn_names = map (prefix "fv_") bn_names |
225 val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys |
223 val fv_bn_arg_tys = map (nth raw_tys) bn_tys |
226 val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys |
224 val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys |
227 val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) |
225 val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) |
228 val fv_bn_map = bns ~~ fv_bn_frees |
226 val fv_bn_map = bns ~~ fv_bn_frees |
229 |
227 |
230 val constrs_info = all_dtyp_constrs_types descr sorts |
228 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss |
231 |
229 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info |
232 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss |
|
233 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info |
|
234 |
230 |
235 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
231 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
236 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
232 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
237 |
233 |
238 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
234 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |