author | blanchet |
Wed, 26 Oct 2016 22:40:28 +0200 | |
changeset 64413 | c0d5e78eb647 |
parent 63813 | 076129f60a31 |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_fp_n2m.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
Flattening of nested to mutual (co)recursion. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
signature BNF_FP_N2M = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
56484 | 10 |
val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list -> |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
11 |
(int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list -> |
56484 | 12 |
typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> |
13 |
BNF_FP_Util.fp_result * local_theory |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
14 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
16 |
structure BNF_FP_N2M : BNF_FP_N2M = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
17 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
19 |
open BNF_Def |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
20 |
open BNF_Util |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
21 |
open BNF_Comp |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
open BNF_FP_Def_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
open BNF_Tactics |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
open BNF_FP_N2M_Tactics |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
|
63045 | 27 |
fun mk_arg_cong ctxt n t = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
let |
63045 | 29 |
val Us = fastype_of t |> strip_typeN n |> fst; |
30 |
val ((xs, ys), _) = ctxt |
|
31 |
|> mk_Frees "x" Us |
|
32 |
||>> mk_Frees "y" Us; |
|
33 |
val goal = Logic.list_implies (@{map 2} (curry mk_Trueprop_eq) xs ys, |
|
34 |
mk_Trueprop_eq (list_comb (t, xs), list_comb (t, ys))); |
|
35 |
val vars = Variable.add_free_names ctxt goal []; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
in |
63045 | 37 |
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => |
38 |
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl)) |
|
39 |
|> Thm.close_derivation |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
42 |
val cacheN = "cache" |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
43 |
fun mk_cacheN i = cacheN ^ string_of_int i ^ "_"; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
44 |
val cache_threshold = Attrib.setup_config_int @{binding bnf_n2m_cache_threshold} (K 200); |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
45 |
type cache = int * (term * thm) Typtab.table |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
46 |
val empty_cache = (0, Typtab.empty) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
47 |
fun update_cache b0 TU t (cache as (i, tab), lthy) = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
48 |
if size_of_term t < Config.get lthy cache_threshold then (t, (cache, lthy)) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
49 |
else |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
50 |
let |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
51 |
val b = Binding.prefix_name (mk_cacheN i) b0; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
52 |
val ((c, thm), lthy') = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
53 |
Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), t)) lthy |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
54 |
|>> apsnd snd; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
55 |
in |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
56 |
(c, ((i + 1, Typtab.update (TU, (c, thm)) tab), lthy')) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
57 |
end; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
58 |
|
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
59 |
fun lookup_cache (SOME _) _ _ = NONE |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
60 |
| lookup_cache NONE TU ((_, tab), _) = Typtab.lookup tab TU |> Option.map fst; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
61 |
|
63045 | 62 |
fun construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs |
62719 | 63 |
(absT_infos : absT_info list) lthy = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
let |
62689 | 65 |
val time = time lthy; |
66 |
val timer = time (Timer.startRealTimer ()); |
|
67 |
||
68 |
val b_names = map Binding.name_of bs; |
|
69 |
val b_name = mk_common_name b_names; |
|
70 |
val b = Binding.name b_name; |
|
71 |
||
62719 | 72 |
fun of_fp_res get = map (uncurry nth o swap o apsnd get) indexed_fp_ress; |
55966 | 73 |
fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); |
74 |
fun co_swap pair = case_fp fp I swap pair; |
|
63045 | 75 |
val mk_co_comp = curry (HOLogic.mk_comp o co_swap); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
76 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
77 |
val dest_co_algT = co_swap o dest_funT; |
55966 | 78 |
val co_alg_argT = case_fp fp range_type domain_type; |
79 |
val co_alg_funT = case_fp fp domain_type range_type; |
|
80 |
val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
81 |
|
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
82 |
val fp_absT_infos = of_fp_res #absT_infos; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
83 |
val fp_bnfs = of_fp_res #bnfs; |
63045 | 84 |
val fp_pre_bnfs = of_fp_res #pre_bnfs; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
85 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
86 |
val fp_absTs = map #absT fp_absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
87 |
val fp_repTs = map #repT fp_absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
88 |
val fp_abss = map #abs fp_absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
89 |
val fp_reps = map #rep fp_absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
90 |
val fp_type_definitions = map #type_definition fp_absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
91 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
92 |
val absTs = map #absT absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
93 |
val repTs = map #repT absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
94 |
val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
95 |
val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
96 |
val abss = map #abs absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
97 |
val reps = map #rep absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
98 |
val abs_inverses = map #abs_inverse absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
99 |
val type_definitions = map #type_definition absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
100 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
101 |
val n = length bnfs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
102 |
val deads = fold (union (op =)) Dss resDs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
103 |
val As = subtract (op =) deads (map TFree resBs); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
104 |
val names_lthy = fold Variable.declare_typ (As @ deads) lthy; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
105 |
val m = length As; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
106 |
val live = m + n; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
107 |
|
63045 | 108 |
val (((Xs, Ys), Bs), names_lthy) = names_lthy |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
109 |
|> mk_TFrees n |
63045 | 110 |
||>> mk_TFrees n |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
111 |
||>> mk_TFrees m; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
112 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
113 |
val allAs = As @ Xs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
114 |
val allBs = Bs @ Xs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
115 |
val phiTs = map2 mk_pred2T As Bs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
116 |
val thetaBs = As ~~ Bs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
117 |
val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
118 |
val fold_thetaAs = Xs ~~ fpTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
119 |
val fold_thetaBs = Xs ~~ fpTs'; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
120 |
val pre_phiTs = map2 mk_pred2T fpTs fpTs'; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
121 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
122 |
val ((ctors, dtors), (xtor's, xtors)) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
123 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
124 |
val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
125 |
val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
126 |
in |
55966 | 127 |
((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors)) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
128 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
129 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
130 |
val absATs = map (domain_type o fastype_of) ctors; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
131 |
val absBTs = map (Term.typ_subst_atomic thetaBs) absATs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
132 |
val xTs = map (domain_type o fastype_of) xtors; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
133 |
val yTs = map (domain_type o fastype_of) xtor's; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
134 |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
135 |
val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
136 |
val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; |
55819 | 137 |
val fp_repAs = map2 mk_rep absATs fp_reps; |
138 |
val fp_repBs = map2 mk_rep absBTs fp_reps; |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
139 |
|
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
140 |
val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single); |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
141 |
val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs) |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
142 |
val sorted_fpTs = map fst sorted_theta; |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
143 |
|
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
144 |
val nesting_bnfs = nesting_bnfs lthy |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
145 |
[[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]] |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
146 |
allAs; |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
147 |
val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs); |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
148 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
149 |
val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
150 |
|> mk_Frees' "R" phiTs |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
151 |
||>> mk_Frees "S" pre_phiTs |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
152 |
||>> mk_Frees "x" xTs |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
153 |
||>> mk_Frees "y" yTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
154 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
155 |
val rels = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
156 |
let |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
157 |
fun find_rel T As Bs = fp_or_nesting_bnfs |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
158 |
|> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf) |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
159 |
|> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
160 |
|> Option.map (fn bnf => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
161 |
let val live = live_of_bnf bnf; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
162 |
in (mk_rel live As Bs (rel_of_bnf bnf), live) end) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
163 |
|> the_default (HOLogic.eq_const T, 0); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
164 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
165 |
fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
166 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
167 |
val (rel, live) = find_rel T Ts Us; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
168 |
val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
169 |
val rels = map2 mk_rel Ts' Us'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
170 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
171 |
Term.list_comb (rel, rels) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
172 |
end |
54244 | 173 |
| mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As) |
174 |
handle General.Subscript => HOLogic.eq_const T) |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
175 |
| mk_rel _ _ = raise Fail "fpTs contains schematic type variables"; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
176 |
in |
54298
347c3b0cab44
handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)
traytel
parents:
54244
diff
changeset
|
177 |
map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs' |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
178 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
179 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
180 |
val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
181 |
|
63045 | 182 |
val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) fp_pre_bnfs; |
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
183 |
val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct) |
62649
d23be25c0835
normalize schematic names since they are used to instantiate the theorem later
traytel
parents:
61101
diff
changeset
|
184 |
|> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
185 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
186 |
val rel_defs = map rel_def_of_bnf bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
187 |
val rel_monos = map rel_mono_of_bnf bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
188 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
189 |
fun cast castA castB pre_rel = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
190 |
let |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
191 |
val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
192 |
(Term.subst_atomic_types fold_thetaBs castB); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
193 |
in |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
194 |
fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs] |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
195 |
(castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0))) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
196 |
end; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
197 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
198 |
val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
199 |
val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
200 |
|
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
201 |
val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs); |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
202 |
val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs; |
58203 | 203 |
|
63045 | 204 |
fun mutual_instantiate ctxt inst = |
205 |
let |
|
206 |
val thetas = AList.group (op =) (mutual_cliques ~~ inst); |
|
207 |
in |
|
208 |
map2 (infer_instantiate ctxt o the o AList.lookup (op =) thetas) mutual_cliques |
|
209 |
end; |
|
210 |
||
59049
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
211 |
val rel_xtor_co_inducts_inst = |
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
212 |
let |
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
213 |
val extract = |
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
214 |
case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); |
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
215 |
val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; |
63045 | 216 |
val inst = map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis); |
59049
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
217 |
in |
63045 | 218 |
mutual_instantiate lthy inst rel_xtor_co_inducts |
59049
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
219 |
end |
0d1bfc982501
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
traytel
parents:
58634
diff
changeset
|
220 |
|
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
221 |
val xtor_rel_co_induct = |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
222 |
mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys |
63045 | 223 |
xtors xtor's (mk_rel_xtor_co_induct_tac fp abs_inverses rel_xtor_co_inducts_inst rel_defs |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
224 |
rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos) |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
225 |
lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
226 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
227 |
val map_id0s = no_refl (map map_id0_of_bnf bnfs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
228 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
229 |
val xtor_co_induct_thm = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
230 |
(case fp of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
231 |
Least_FP => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
232 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
233 |
val (Ps, names_lthy) = names_lthy |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
234 |
|> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
235 |
fun mk_Grp_id P = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
236 |
let val T = domain_type (fastype_of P); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
237 |
in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end; |
60788 | 238 |
val cts = |
239 |
map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps); |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
240 |
fun mk_fp_type_copy_thms thm = map (curry op RS thm) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
241 |
@{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep}; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
242 |
fun mk_type_copy_thms thm = map (curry op RS thm) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
243 |
@{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs}; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
244 |
in |
60788 | 245 |
infer_instantiate' names_lthy cts xtor_rel_co_induct |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
246 |
|> singleton (Proof_Context.export names_lthy lthy) |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
247 |
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
248 |
fp_or_nesting_rel_eqs) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
249 |
|> funpow n (fn thm => thm RS spec) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
250 |
|> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s) |
55854
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55819
diff
changeset
|
251 |
|> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
252 |
Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @ |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
253 |
maps mk_fp_type_copy_thms fp_type_definitions @ |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
254 |
maps mk_type_copy_thms type_definitions) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
255 |
|> unfold_thms lthy @{thms subset_iff mem_Collect_eq |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
256 |
atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
257 |
end |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
258 |
| Greatest_FP => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
259 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59580
diff
changeset
|
260 |
val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
261 |
in |
60788 | 262 |
infer_instantiate' lthy cts xtor_rel_co_induct |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
263 |
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58352
diff
changeset
|
264 |
fp_or_nesting_rel_eqs) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
265 |
|> funpow (2 * n) (fn thm => thm RS spec) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset
|
266 |
|> Conv.fconv_rule (Object_Logic.atomize lthy) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
267 |
|> funpow n (fn thm => thm RS mp) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
268 |
end); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
269 |
|
62689 | 270 |
val timer = time (timer "Nested-to-mutual (co)induction"); |
271 |
||
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
272 |
val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
273 |
|
63045 | 274 |
val fold_strTs = map2 mk_co_algT fold_preTs Xs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
275 |
val resTs = map2 mk_co_algT fpTs Xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
276 |
|
63045 | 277 |
val fp_un_folds = of_fp_res #xtor_un_folds; |
62719 | 278 |
val ns = map (length o #Ts o snd) indexed_fp_ress; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
279 |
|
63045 | 280 |
fun force_fold i TU raw_un_fold = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
281 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
282 |
val thy = Proof_Context.theory_of lthy; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
283 |
|
63045 | 284 |
val approx_un_fold = raw_un_fold |
57802 | 285 |
|> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
286 |
val subst = Term.typ_subst_atomic fold_thetaAs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
287 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
288 |
fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT; |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
289 |
val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
290 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
291 |
val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
292 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
293 |
val fold_pre_deads_only_Ts = |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
294 |
map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs'; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
295 |
|
58340 | 296 |
val (mutual_clique, TUs) = |
63045 | 297 |
map_split dest_co_algT (binder_fun_types (fastype_of approx_un_fold)) |
55478
3a6efda01da4
made N2M more robust w.r.t. identical nested types
traytel
parents:
55414
diff
changeset
|
298 |
|>> map subst |
63045 | 299 |
|> `(fn (_, Ys) => nth mutual_cliques |
62719 | 300 |
(find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs)) |
56487
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
301 |
||> uncurry (map2 mk_co_algT); |
63045 | 302 |
val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs; |
56487
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
303 |
val js = find_indices (fn ((cl, cand), TU) => |
58340 | 304 |
cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
305 |
val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
306 |
in |
63045 | 307 |
force_typ names_lthy (Tpats ---> TU) raw_un_fold |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
308 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
309 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
310 |
fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t = |
55966 | 311 |
case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep)) |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
312 |
(HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t))); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
313 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
314 |
val thy = Proof_Context.theory_of lthy; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
315 |
fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
316 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
317 |
fun mk_un_fold b_opt ss un_folds cache_lthy TU = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
318 |
(case lookup_cache b_opt TU cache_lthy of |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
319 |
SOME t => ((t, Drule.dummy_thm), cache_lthy) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
320 |
| NONE => |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
321 |
let |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
322 |
val x = co_alg_argT TU; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
323 |
val i = find_index (fn T => x = T) Xs; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
324 |
val TUfold = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
325 |
(case find_first (fn f => body_fun_type (fastype_of f) = TU) un_folds of |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
326 |
NONE => force_fold i TU (nth fp_un_folds i) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
327 |
| SOME f => f); |
63813 | 328 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
329 |
val TUs = binder_fun_types (fastype_of TUfold); |
63813 | 330 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
331 |
fun mk_s TU' cache_lthy = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
332 |
let |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
333 |
val i = find_index (fn T => co_alg_argT TU' = T) Xs; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
334 |
val fp_abs = nth fp_abss i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
335 |
val fp_rep = nth fp_reps i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
336 |
val abs = nth abss i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
337 |
val rep = nth reps i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
338 |
val sF = co_alg_funT TU'; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
339 |
val sF' = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
340 |
mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
341 |
handle Term.TYPE _ => sF; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
342 |
val F = nth fold_preTs i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
343 |
val s = nth ss i; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
344 |
in |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
345 |
if sF = F then (s, cache_lthy) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
346 |
else if sF' = F then (mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s, cache_lthy) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
347 |
else |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
348 |
let |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
349 |
val smapT = replicate live dummyT ---> mk_co_algT sF' F; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
350 |
fun hidden_to_unit t = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
351 |
Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
352 |
val smap = map_of_bnf (nth bnfs i) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
353 |
|> force_typ names_lthy smapT |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
354 |
|> hidden_to_unit; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
355 |
val smap_argTs = strip_typeN live (fastype_of smap) |> fst; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
356 |
fun mk_smap_arg T_to_U cache_lthy = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
357 |
(if domain_type T_to_U = range_type T_to_U then |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
358 |
(HOLogic.id_const (domain_type T_to_U), cache_lthy) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
359 |
else |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
360 |
mk_un_fold NONE ss un_folds cache_lthy T_to_U |>> fst); |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
361 |
val (smap_args, cache_lthy') = fold_map mk_smap_arg smap_argTs cache_lthy; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
362 |
in |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
363 |
(mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
364 |
(mk_co_comp s (Term.list_comb (smap, smap_args))), cache_lthy') |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
365 |
end |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
366 |
end; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
367 |
val (args, cache_lthy) = fold_map mk_s TUs cache_lthy; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
368 |
val t = Term.list_comb (TUfold, args); |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
369 |
in |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
370 |
(case b_opt of |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
371 |
NONE => update_cache b TU t cache_lthy |>> rpair Drule.dummy_thm |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
372 |
| SOME b => cache_lthy |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
373 |
|-> (fn cache => |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
374 |
let |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
375 |
val S = HOLogic.mk_tupleT fold_strTs; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
376 |
val s = HOLogic.mk_tuple ss; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
377 |
val u = Const (@{const_name Let}, S --> (S --> TU) --> TU) $ s $ absdummy S t; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
378 |
in |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
379 |
Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), u)) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
380 |
#>> apsnd snd ##> pair cache |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
381 |
end)) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
382 |
end); |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
383 |
|
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
384 |
val un_foldN = case_fp fp ctor_foldN dtor_unfoldN; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
385 |
fun mk_un_folds (ss_names, lthy) = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
386 |
let val ss = map2 (curry Free) ss_names fold_strTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
387 |
in |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
388 |
fold2 (fn TU => fn b => fn ((un_folds, defs), cache_lthy) => |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
389 |
mk_un_fold (SOME b) (map2 (curry Free) ss_names fold_strTs) un_folds cache_lthy TU |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
390 |
|>> (fn (f, d) => (f :: un_folds, d :: defs))) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
391 |
resTs (map (Binding.suffix_name ("_" ^ un_foldN)) bs) (([], []), (empty_cache, lthy)) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
392 |
|>> map_prod rev rev |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
393 |
|>> pair ss |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
394 |
end; |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
395 |
val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
396 |
|> Local_Theory.open_target |> snd |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
397 |
|> Variable.add_fixes (mk_names n "s") |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
398 |
|> mk_un_folds |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
399 |
||> apsnd (`(Local_Theory.close_target)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
400 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
401 |
val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
402 |
|
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
403 |
val cache_defs = snd cache |> Typtab.dest |> map (snd o snd); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
404 |
|
53331
20440c789759
prove theorem in the right context (that knows about local variables)
traytel
parents:
53309
diff
changeset
|
405 |
val phi = Proof_Context.export_morphism raw_lthy lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
406 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
407 |
val xtor_un_folds = map (head_of o Morphism.term phi) un_folds; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
408 |
val xtor_un_fold_defs = map (Drule.abs_def o Morphism.thm phi) un_fold_defs; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
409 |
val xtor_cache_defs = map (Drule.abs_def o Morphism.thm phi) cache_defs; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
410 |
val xtor_un_folds' = map2 (fn raw => fn t => |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
411 |
Const (fst (dest_Const t), fold_strTs ---> fastype_of raw)) |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
412 |
un_folds xtor_un_folds; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
413 |
|
63045 | 414 |
val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps |
56486 | 415 |
|> maps (fn thm => [thm, thm RS rewrite_comp_comp]); |
55868 | 416 |
|
63045 | 417 |
val fold_mapTs = co_swap (As @ fpTs, As @ Xs); |
418 |
val pre_fold_maps = @{map 2} (fn Ds => uncurry (mk_map_of_bnf Ds) fold_mapTs) Dss bnfs |
|
419 |
fun mk_pre_fold_maps fs = |
|
420 |
map (fn mapx => Term.list_comb (mapx, map HOLogic.id_const As @ fs)) pre_fold_maps; |
|
421 |
||
422 |
val pre_map_defs = no_refl (map map_def_of_bnf bnfs); |
|
423 |
val fp_map_defs = no_refl (map map_def_of_bnf fp_pre_bnfs); |
|
424 |
val map_defs = pre_map_defs @ fp_map_defs; |
|
425 |
val pre_rel_defs = no_refl (map rel_def_of_bnf bnfs); |
|
426 |
val fp_rel_defs = no_refl (map rel_def_of_bnf fp_pre_bnfs); |
|
427 |
val rel_defs = pre_rel_defs @ fp_rel_defs; |
|
428 |
fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs}) |
|
429 |
|> (fn thm => [thm, thm RS rewrite_comp_comp]); |
|
430 |
val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions; |
|
431 |
val pre_Rep_o_Abss = maps mk_Rep_o_Abs type_definitions; |
|
432 |
val Rep_o_Abss = fp_Rep_o_Abss @ pre_Rep_o_Abss; |
|
433 |
||
434 |
val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs)); |
|
435 |
val simp_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: |
|
436 |
@{thms id_apply comp_id id_comp}; |
|
437 |
||
438 |
val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; |
|
439 |
||
440 |
val map_thms = no_refl (maps (fn bnf => |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
441 |
let val map_comp0 = map_comp0_of_bnf bnf RS sym |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
442 |
in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) |
63045 | 443 |
fp_or_nesting_bnfs) @ |
444 |
remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc}) |
|
445 |
(map2 (fn thm => fn bnf => |
|
446 |
@{thm type_copy_map_comp0_undo} OF |
|
447 |
(replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS |
|
448 |
rewrite_comp_comp) |
|
449 |
type_definitions bnfs); |
|
450 |
||
451 |
val xtor_un_fold_thms = |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
452 |
let |
63045 | 453 |
val pre_fold_maps = mk_pre_fold_maps un_folds; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
454 |
fun mk_goals f xtor s smap fp_abs fp_rep abs rep = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
455 |
let |
63045 | 456 |
val lhs = mk_co_comp f xtor; |
457 |
val rhs = mk_co_comp s smap; |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
458 |
in |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
459 |
HOLogic.mk_eq (lhs, |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
460 |
mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
461 |
fp_abs fp_rep abs rep rhs) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
462 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
463 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
464 |
val goals = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
465 |
@{map 8} mk_goals un_folds xtors ss pre_fold_maps fp_abss fp_reps abss reps; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
466 |
|
64413 | 467 |
val fp_un_folds = map (mk_pointfree2 lthy) (of_fp_res #xtor_un_fold_thms); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
468 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
469 |
val simps = flat [simp_thms, un_fold_defs, map_defs, fp_un_folds, |
63045 | 470 |
fp_un_fold_o_maps, map_thms, Rep_o_Abss]; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
471 |
in |
55894
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
472 |
Library.foldr1 HOLogic.mk_conj goals |
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
473 |
|> HOLogic.mk_Trueprop |
63045 | 474 |
|> (fn goal => Goal.prove_sorry raw_lthy [] [] goal |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
475 |
(fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps cache_defs)) |
55894
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
476 |
|> Thm.close_derivation |
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
477 |
|> Morphism.thm phi |
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
478 |
|> split_conj_thm |
8f3fe443948a
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
blanchet
parents:
55868
diff
changeset
|
479 |
|> map (fn thm => thm RS @{thm comp_eq_dest}) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
480 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
481 |
|
63045 | 482 |
val xtor_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps |
483 |
|> maps (fn thm => [thm, thm RS rewrite_comp_comp]); |
|
484 |
val xtor_un_fold_unique_thm = |
|
485 |
let |
|
486 |
val (fs, _) = names_lthy |> mk_Frees "f" resTs; |
|
487 |
val fold_maps = mk_pre_fold_maps fs; |
|
488 |
fun mk_prem f s mapx xtor fp_abs fp_rep abs rep = |
|
489 |
let |
|
490 |
val lhs = mk_co_comp f xtor; |
|
491 |
val rhs = mk_co_comp s mapx; |
|
492 |
in |
|
493 |
mk_Trueprop_eq (lhs, |
|
494 |
mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) |
|
495 |
fp_abs fp_rep abs rep rhs) |
|
496 |
end; |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
497 |
val prems = @{map 8} mk_prem fs ss fold_maps xtors fp_abss fp_reps abss reps; |
63045 | 498 |
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
499 |
(map2 (curry HOLogic.mk_eq) fs un_folds)); |
|
500 |
val vars = Variable.add_free_names raw_lthy concl []; |
|
501 |
val fp_un_fold_uniques0 = of_fp_res (split_conj_thm o #xtor_un_fold_unique) |
|
502 |
|> map (Drule.zero_var_indexes o unfold_thms lthy fp_map_defs); |
|
503 |
val names = fp_un_fold_uniques0 |
|
504 |
|> map (Thm.concl_of #> HOLogic.dest_Trueprop |
|
505 |
#> HOLogic.dest_eq #> fst #> dest_Var #> fst); |
|
506 |
val inst = names ~~ map (Thm.cterm_of lthy) fs; |
|
507 |
val fp_un_fold_uniques = mutual_instantiate lthy inst fp_un_fold_uniques0; |
|
508 |
val map_arg_congs = |
|
509 |
map (fn bnf => mk_arg_cong lthy (live_of_bnf bnf) (map_of_bnf bnf) |
|
510 |
|> unfold_thms lthy (pre_map_defs @ simp_thms)) nesting_bnfs; |
|
511 |
in |
|
512 |
Goal.prove_sorry raw_lthy vars prems concl |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
513 |
(mk_xtor_un_fold_unique_tac fp un_fold_defs map_arg_congs xtor_un_fold_o_maps |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
514 |
Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs) |
63045 | 515 |
|> Thm.close_derivation |
516 |
|> case_fp fp I (fn thm => thm OF replicate n sym) |
|
517 |
|> Morphism.thm phi |
|
518 |
end; |
|
519 |
||
520 |
val ABs = As ~~ Bs; |
|
521 |
val XYs = Xs ~~ Ys; |
|
522 |
val ABphiTs = @{map 2} mk_pred2T As Bs; |
|
523 |
val XYphiTs = @{map 2} mk_pred2T Xs Ys; |
|
524 |
||
525 |
val ((ABphis, XYphis), _) = names_lthy |
|
526 |
|> mk_Frees "R" ABphiTs |
|
527 |
||>> mk_Frees "S" XYphiTs; |
|
528 |
||
529 |
val pre_rels = @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ Xs) (Bs @ Ys)) Dss bnfs; |
|
530 |
||
531 |
val ns = map (fn i => length (filter (fn c => i = c) mutual_cliques)) mutual_cliques; |
|
532 |
||
533 |
val map_transfers = map (funpow live (fn thm => thm RS @{thm rel_funD}) |
|
534 |
#> unfold_thms lthy pre_rel_defs) |
|
535 |
(map map_transfer_of_bnf bnfs); |
|
536 |
val fp_un_fold_transfers = map2 (fn n => funpow n (fn thm => thm RS @{thm rel_funD}) |
|
537 |
#> unfold_thms lthy fp_rel_defs) |
|
538 |
ns (of_fp_res #xtor_un_fold_transfers); |
|
539 |
val pre_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions; |
|
540 |
val fp_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) fp_type_definitions; |
|
541 |
val Abs_transfers = pre_Abs_transfers @ fp_Abs_transfers; |
|
542 |
||
543 |
fun tac {context = ctxt, prems = _} = |
|
544 |
mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
545 |
map_transfers Abs_transfers fp_or_nesting_rel_eqs xtor_cache_defs; |
63045 | 546 |
|
547 |
val xtor_un_fold_transfer_thms = |
|
548 |
mk_xtor_co_iter_transfer_thms fp pre_rels XYphis XYphis rels ABphis |
|
549 |
xtor_un_folds' (map (subst_atomic_types (ABs @ XYs)) xtor_un_folds') tac lthy; |
|
550 |
||
551 |
val timer = time (timer "Nested-to-mutual (co)iteration"); |
|
552 |
||
553 |
val xtor_maps = of_fp_res #xtor_maps; |
|
554 |
val xtor_rels = of_fp_res #xtor_rels; |
|
555 |
fun mk_Ts Cs = map (typ_subst_atomic (As ~~ Cs)) fpTs; |
|
556 |
val phi = Local_Theory.target_morphism lthy; |
|
557 |
val export = map (Morphism.term phi); |
|
558 |
val ((xtor_co_recs, (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, |
|
559 |
xtor_co_rec_transfer_thms)), lthy) = lthy |
|
560 |
|> derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) bnfs |
|
561 |
(export xtors) (export xtor_un_folds) |
|
562 |
xtor_un_fold_unique_thm xtor_un_fold_thms xtor_un_fold_transfer_thms xtor_maps xtor_rels |
|
563 |
(@{map 2} (curry (SOME o @{apply 2} (morph_absT_info phi))) fp_absT_infos absT_infos); |
|
564 |
||
62689 | 565 |
val timer = time (timer "Nested-to-mutual (co)recursion"); |
566 |
||
567 |
val common_notes = |
|
568 |
(case fp of |
|
569 |
Least_FP => |
|
570 |
[(ctor_inductN, [xtor_co_induct_thm]), |
|
571 |
(ctor_rel_inductN, [xtor_rel_co_induct])] |
|
572 |
| Greatest_FP => |
|
573 |
[(dtor_coinductN, [xtor_co_induct_thm]), |
|
574 |
(dtor_rel_coinductN, [xtor_rel_co_induct])]) |
|
575 |
|> map (fn (thmN, thms) => |
|
576 |
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
|
577 |
||
578 |
val notes = |
|
579 |
(case fp of |
|
63045 | 580 |
Least_FP => [(ctor_foldN, xtor_un_fold_thms)] |
581 |
| Greatest_FP => [(dtor_unfoldN, xtor_un_fold_thms)]) |
|
62689 | 582 |
|> map (apsnd (map single)) |
583 |
|> maps (fn (thmN, thmss) => |
|
584 |
map2 (fn b => fn thms => |
|
585 |
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
|
586 |
bs thmss); |
|
587 |
||
588 |
val lthy = lthy |> Config.get lthy bnf_internals |
|
589 |
? snd o Local_Theory.notes (common_notes @ notes); |
|
590 |
||
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
591 |
(* These results are half broken. This is deliberate. We care only about those fields that are |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55530
diff
changeset
|
592 |
used by "primrec", "primcorecursive", and "datatype_compat". *) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
593 |
val fp_res = |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
594 |
({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos, |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62649
diff
changeset
|
595 |
dtors = dtors, ctors = ctors, |
63045 | 596 |
xtor_un_folds = xtor_un_folds, xtor_co_recs = xtor_co_recs, |
59819 | 597 |
xtor_co_induct = xtor_co_induct_thm, |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
598 |
dtor_ctors = of_fp_res #dtor_ctors (*too general types*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
599 |
ctor_dtors = of_fp_res #ctor_dtors (*too general types*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
600 |
ctor_injects = of_fp_res #ctor_injects (*too general types*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
601 |
dtor_injects = of_fp_res #dtor_injects (*too general types*), |
62863
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
602 |
xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), |
63045 | 603 |
xtor_map_unique = xtor_un_fold_unique_thm (*wrong*), |
58584 | 604 |
xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), |
58585 | 605 |
xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), |
63045 | 606 |
xtor_un_fold_thms = xtor_un_fold_thms, |
607 |
xtor_co_rec_thms = xtor_co_rec_thms, |
|
608 |
xtor_un_fold_unique = xtor_un_fold_unique_thm, |
|
609 |
xtor_co_rec_unique = xtor_co_rec_unique_thm, |
|
610 |
xtor_un_fold_o_maps = fp_un_fold_o_maps (*wrong*), |
|
611 |
xtor_co_rec_o_maps = xtor_co_rec_o_map_thms (*wrong*), |
|
612 |
xtor_un_fold_transfers = xtor_un_fold_transfer_thms, |
|
613 |
xtor_co_rec_transfers = xtor_co_rec_transfer_thms (*wrong*), |
|
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
614 |
xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} |
54740 | 615 |
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
616 |
in |
62689 | 617 |
timer; (fp_res, lthy) |
54242 | 618 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
619 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
620 |
end; |