144 *} |
144 *} |
145 |
145 |
146 ML {* |
146 ML {* |
147 (** definition of the raw binding functions **) |
147 (** definition of the raw binding functions **) |
148 |
148 |
149 (* TODO: needs cleaning *) |
149 fun prep_bn_info lthy dt_names dts bn_funs eqs = |
150 fun find [] _ = error ("cannot find element") |
150 let |
151 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
151 fun process_eq eq = |
152 |
|
153 fun prep_bn_info lthy dt_names dts eqs = |
|
154 let |
|
155 fun aux eq = |
|
156 let |
152 let |
157 val (lhs, rhs) = eq |
153 val (lhs, rhs) = eq |
158 |> HOLogic.dest_Trueprop |
154 |> HOLogic.dest_Trueprop |
159 |> HOLogic.dest_eq |
155 |> HOLogic.dest_eq |
160 val (bn_fun, [cnstr]) = strip_comb lhs |
156 val (bn_fun, [cnstr]) = strip_comb lhs |
161 val (_, ty) = dest_Const bn_fun |
157 val (_, ty) = dest_Const bn_fun |
162 val (ty_name, _) = dest_Type (domain_type ty) |
158 val (ty_name, _) = dest_Type (domain_type ty) |
163 val dt_index = find_index (fn x => x = ty_name) dt_names |
159 val dt_index = find_index (fn x => x = ty_name) dt_names |
164 val (cnstr_head, cnstr_args) = strip_comb cnstr |
160 val (cnstr_head, cnstr_args) = strip_comb cnstr |
|
161 val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) |
165 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
162 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
166 in |
163 in |
167 (dt_index, (bn_fun, (cnstr_head, rhs_elements))) |
164 ((bn_fun, dt_index), (cnstr_name, rhs_elements)) |
168 end |
165 end |
169 |
166 |
170 fun order dts i ts = |
167 (* order according to constructor names *) |
|
168 fun cntrs_order ((bn, dt_index), data) = |
171 let |
169 let |
172 val dt = nth dts i |
170 val dt = nth dts dt_index |
173 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
171 val cts = (fn (_, _, _, x) => x) dt |
174 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
172 val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts |
175 in |
173 in |
176 map (find ts') cts |
174 (bn, (bn, dt_index, order (op=) ct_names data)) |
177 end |
175 end |
178 |
176 |
179 val unordered = AList.group (op=) (map aux eqs) |
177 in |
180 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
178 eqs |
181 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
179 |> map process_eq |
182 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
180 |> AList.group (op=) (* eqs grouped according to bn_functions *) |
183 |
181 |> map cntrs_order (* inner data ordered according to constructors *) |
184 (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) |
182 |> order (op=) bn_funs (* ordered according to bn_functions *) |
185 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) |
183 end |
186 (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) |
184 *} |
187 in |
185 |
188 ordered' |
186 ML {* |
189 end |
|
190 |
|
191 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
187 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
192 if null raw_bn_funs |
188 if null raw_bn_funs |
193 then ([], [], [], [], lthy) |
189 then ([], [], [], [], lthy) |
194 else |
190 else |
195 let |
191 let |
267 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
263 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
268 if get_STEPS lthy > 0 |
264 if get_STEPS lthy > 0 |
269 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
265 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
270 else raise TEST lthy |
266 else raise TEST lthy |
271 |
267 |
|
268 val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs)) |
|
269 |
272 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
270 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
273 val {descr, sorts, ...} = dtinfo |
271 val {descr, sorts, ...} = dtinfo |
274 |
272 |
275 val raw_tys = all_dtyps descr sorts |
273 val raw_tys = all_dtyps descr sorts |
276 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
274 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
309 if get_STEPS lthy3 > 1 |
307 if get_STEPS lthy3 > 1 |
310 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
308 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
311 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
309 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
312 else raise TEST lthy3 |
310 else raise TEST lthy3 |
313 |
311 |
|
312 (* |
|
313 val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns)) |
|
314 val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info)) |
|
315 val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info)) |
|
316 *) |
|
317 |
314 (* defining the permute_bn functions *) |
318 (* defining the permute_bn functions *) |
315 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
319 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
316 if get_STEPS lthy3a > 2 |
320 if get_STEPS lthy3a > 2 |
317 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
321 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
318 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
322 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
487 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
491 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
488 |
492 |
489 val qalpha_bns_descr = |
493 val qalpha_bns_descr = |
490 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
494 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
491 |
495 |
|
496 (* |
|
497 val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info)) |
|
498 val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs)) |
|
499 val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns)) |
|
500 val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns)) |
|
501 val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms)) |
|
502 *) |
|
503 |
492 val qperm_descr = |
504 val qperm_descr = |
493 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
505 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
494 |
506 |
495 val qsize_descr = |
507 val qsize_descr = |
496 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
508 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
497 |
509 |
498 val qperm_bn_descr = |
510 val qperm_bn_descr = |
499 map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns |
511 map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns |
500 |
512 |
501 |
513 |
502 val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = |
514 val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= |
503 if get_STEPS lthy > 24 |
515 if get_STEPS lthy > 24 |
504 then |
516 then |
505 lthy7 |
517 lthy7 |
506 |> define_qconsts qtys qconstrs_descr |
518 |> define_qconsts qtys qconstrs_descr |
507 ||>> define_qconsts qtys qbns_descr |
519 ||>> define_qconsts qtys qbns_descr |
525 val qtrms = map #qconst qconstrs_info |
537 val qtrms = map #qconst qconstrs_info |
526 val qbns = map #qconst qbns_info |
538 val qbns = map #qconst qbns_info |
527 val qfvs = map #qconst qfvs_info |
539 val qfvs = map #qconst qfvs_info |
528 val qfv_bns = map #qconst qfv_bns_info |
540 val qfv_bns = map #qconst qfv_bns_info |
529 val qalpha_bns = map #qconst qalpha_bns_info |
541 val qalpha_bns = map #qconst qalpha_bns_info |
|
542 val qperm_bns = map #qconst qperm_bns_info |
530 |
543 |
531 (* lifting of the theorems *) |
544 (* lifting of the theorems *) |
532 val _ = warning "Lifting of Theorems" |
545 val _ = warning "Lifting of Theorems" |
533 |
546 |
534 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
547 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
584 if get_STEPS lthy > 32 |
597 if get_STEPS lthy > 32 |
585 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
598 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
586 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
599 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
587 else [] |
600 else [] |
588 |
601 |
589 (* proving that the qbn result is finite *) |
|
590 val qbn_finite_thms = |
|
591 if get_STEPS lthy > 33 |
|
592 then prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
|
593 else [] |
|
594 |
|
595 (* postprocessing of eq and fv theorems *) |
602 (* postprocessing of eq and fv theorems *) |
596 |
603 |
597 val qeq_iffs' = qeq_iffs |
604 val qeq_iffs' = qeq_iffs |
598 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
605 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
599 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
606 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
609 @{thm fresh_def[symmetric]}] |
616 @{thm fresh_def[symmetric]}] |
610 |
617 |
611 val qfresh_constrs = qsupp_constrs |
618 val qfresh_constrs = qsupp_constrs |
612 |> map (fn thm => thm RS transform_thm) |
619 |> map (fn thm => thm RS transform_thm) |
613 |> map (simplify (HOL_basic_ss addsimps transform_thms)) |
620 |> map (simplify (HOL_basic_ss addsimps transform_thms)) |
|
621 |
|
622 (* proving that the qbn result is finite *) |
|
623 val qbn_finite_thms = |
|
624 if get_STEPS lthy > 33 |
|
625 then prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
|
626 else [] |
|
627 |
|
628 (* proving that perm_bns preserve alpha *) |
|
629 val qperm_bn_alpha_thms = @{thms TrueI} |
|
630 (* if get_STEPS lthy > 33 |
|
631 then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC |
|
632 else []*) |
614 |
633 |
615 |
634 |
616 (* noting the theorems *) |
635 (* noting the theorems *) |
617 |
636 |
618 (* generating the prefix for the theorem names *) |
637 (* generating the prefix for the theorem names *) |
637 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
656 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
638 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
657 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
639 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
658 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
640 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
659 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
641 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
660 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
|
661 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
642 in |
662 in |
643 (0, lthy9') |
663 (0, lthy9') |
644 end handle TEST ctxt => (0, ctxt) |
664 end handle TEST ctxt => (0, ctxt) |
645 *} |
665 *} |
646 |
666 |