9 sig |
9 sig |
10 val get_all_binders: bclause list -> (term option * int) list |
10 val get_all_binders: bclause list -> (term option * int) list |
11 val is_recursive_binder: bclause -> bool |
11 val is_recursive_binder: bclause -> bool |
12 |
12 |
13 val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> |
13 val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> |
14 (Attrib.binding * term) list -> local_theory -> |
14 Specification.multi_specs -> local_theory -> |
15 (term list * thm list * bn_info list * thm list * local_theory) |
15 (term list * thm list * bn_info list * thm list * local_theory) |
16 |
16 |
17 val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> |
17 val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> |
18 Proof.context -> term list * term list * thm list * thm list * local_theory |
18 Proof.context -> term list * term list * thm list * thm list * local_theory |
19 |
19 |
116 {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info |
116 {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info |
117 |
117 |
118 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
118 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
119 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
119 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
120 |
120 |
121 val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1) |
121 val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.reset lthy1) (* FIXME disrupts context *) |
122 val {fs, simps, inducts, ...} = info |
122 val {fs, simps, inducts, ...} = info |
123 |
123 |
124 val raw_bn_induct = (the inducts) |
124 val raw_bn_induct = (the inducts) |
125 val raw_bn_eqs = the simps |
125 val raw_bn_eqs = the simps |
126 |
126 |
250 |
250 |
251 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss |
251 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss |
252 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info |
252 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info |
253 |
253 |
254 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
254 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
255 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
255 val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat fv_eqs @ flat fv_bn_eqs) |
256 |
256 |
257 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
257 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
258 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
258 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
259 |
259 |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy') (* FIXME disrupts context *) |
261 |
261 |
262 val {fs, simps, inducts, ...} = info; |
262 val {fs, simps, inducts, ...} = info; |
263 |
263 |
264 val morphism = |
264 val morphism = |
265 Proof_Context.export_morphism lthy'' |
265 Proof_Context.export_morphism lthy'' |
322 val perm_bn_map = bns ~~ perm_bn_frees |
322 val perm_bn_map = bns ~~ perm_bn_frees |
323 |
323 |
324 val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info |
324 val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info |
325 |
325 |
326 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names |
326 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names |
327 val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) |
327 val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat perm_bn_eqs) |
328 |
328 |
329 val prod_simps = @{thms prod.inject HOL.simp_thms} |
329 val prod_simps = @{thms prod.inject HOL.simp_thms} |
330 |
330 |
331 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
331 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
332 Function_Common.default_config |
332 Function_Common.default_config |
333 (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy |
333 (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy |
334 |
334 |
335 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
335 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy') (* FIXME disrupts context *) |
336 |
336 |
337 val {fs, simps, ...} = info; |
337 val {fs, simps, ...} = info; |
338 |
338 |
339 val morphism = |
339 val morphism = |
340 Proof_Context.export_morphism lthy'' |
340 Proof_Context.export_morphism lthy'' |
410 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
410 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
411 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
411 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
412 |
412 |
413 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
413 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
414 in |
414 in |
415 (Attrib.empty_binding, eq) |
415 ((Binding.empty_atts, eq), [], []) |
416 end |
416 end |
417 |
417 |
418 |
418 |
419 fun define_raw_perms raw_dt_info lthy = |
419 fun define_raw_perms raw_dt_info lthy = |
420 let |
420 let |