equal
deleted
inserted
replaced
19 val is_atom_fset: Proof.context -> typ -> bool |
19 val is_atom_fset: Proof.context -> typ -> bool |
20 val is_atom_list: Proof.context -> typ -> bool |
20 val is_atom_list: Proof.context -> typ -> bool |
21 val mk_atom_set: term -> term |
21 val mk_atom_set: term -> term |
22 val mk_atom_fset: term -> term |
22 val mk_atom_fset: term -> term |
23 |
23 |
24 |
|
25 val setify: Proof.context -> term -> term |
24 val setify: Proof.context -> term -> term |
26 val listify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
27 |
26 |
28 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
27 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
29 bclause list list list -> Proof.context -> term list * term list * thm list * local_theory |
28 bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory |
30 end |
29 end |
31 |
30 |
32 |
31 |
33 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
32 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
34 struct |
33 struct |
198 val nth_bclausess = nth bclausesss bn_n |
197 val nth_bclausess = nth bclausesss bn_n |
199 in |
198 in |
200 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
199 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
201 end |
200 end |
202 |
201 |
203 fun define_raw_fvs descr sorts bn_info bclausesss lthy = |
202 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = |
204 let |
203 let |
205 val fv_names = prefix_dt_names descr sorts "fv_" |
204 val fv_names = prefix_dt_names descr sorts "fv_" |
206 val fv_arg_tys = all_dtyps descr sorts |
205 val fv_arg_tys = all_dtyps descr sorts |
207 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
206 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
208 val fv_frees = map Free (fv_names ~~ fv_tys); |
207 val fv_frees = map Free (fv_names ~~ fv_tys); |
222 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info |
221 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info |
223 |
222 |
224 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
223 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
225 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
224 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
226 |
225 |
227 fun pat_completeness_auto lthy = |
|
228 Pat_Completeness.pat_completeness_tac lthy 1 |
|
229 THEN auto_tac (clasimpset_of lthy) |
|
230 |
|
231 fun prove_termination lthy = |
|
232 Function.prove_termination NONE |
|
233 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
|
234 |
|
235 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
226 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
236 Function_Common.default_config pat_completeness_auto lthy |
227 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
237 |
228 |
238 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
229 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
239 |
230 |
240 val {fs, simps, ...} = info; |
231 val {fs, simps, ...} = info; |
241 |
232 |