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: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
27 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
28 thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
28 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
29 |
29 |
30 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 |
31 end |
31 end |
32 |
32 |
33 |
33 |
208 val nth_bclausess = nth bclausesss bn_n |
208 val nth_bclausess = nth bclausesss bn_n |
209 in |
209 in |
210 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 |
211 end |
211 end |
212 |
212 |
213 fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy = |
213 fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy = |
214 let |
214 let |
215 val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names |
215 val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names |
216 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys |
216 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys |
217 val fv_frees = map Free (fv_names ~~ fv_tys); |
217 val fv_frees = map Free (fv_names ~~ fv_tys); |
218 val fv_map = raw_tys ~~ fv_frees |
218 val fv_map = raw_tys ~~ fv_frees |
231 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) |
232 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) |
233 |
233 |
234 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
234 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
235 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
235 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
236 |
236 |
237 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
237 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
238 |
238 |
239 val {fs, simps, inducts, ...} = info; |
239 val {fs, simps, inducts, ...} = info; |
240 |
240 |
241 val morphism = ProofContext.export_morphism lthy'' lthy |
241 val morphism = ProofContext.export_morphism lthy'' lthy |
242 val fs_exp = map (Morphism.term morphism) fs |
242 val fs_exp = map (Morphism.term morphism) fs |
243 val simps_exp = map (Morphism.thm morphism) (the simps) |
243 val simps_exp = map (Morphism.thm morphism) (the simps) |
244 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
244 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
245 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
245 val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
246 |
246 in |
247 in |
247 (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'') |
248 (fv_frees_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'') |
|
249 end |
248 end |
250 |
249 |
251 |
250 |
252 (** equivarance proofs **) |
251 (** equivarance proofs **) |
253 |
252 |