author | blanchet |
Wed, 23 Apr 2014 10:23:26 +0200 | |
changeset 56640 | 0a35354137a5 |
parent 56638 | 092a306bcc3d |
child 56650 | 1f9ab71d43a5 |
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 -> |
11 |
BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list -> |
|
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 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
fun force_typ ctxt T = |
56638 | 28 |
Term.map_types Type_Infer.paramify_vars |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
#> Type.constraint T |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
#> Syntax.check_term ctxt |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
#> singleton (Variable.polymorphic ctxt); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
fun mk_prod_map f g = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
val ((fAT, fBT), fT) = `dest_funT (fastype_of f); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
val ((gAT, gBT), gT) = `dest_funT (fastype_of g); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
37 |
in |
55932 | 38 |
Const (@{const_name map_prod}, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g |
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 |
|
55931 | 42 |
fun mk_map_sum f g = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
val ((fAT, fBT), fT) = `dest_funT (fastype_of f); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
45 |
val ((gAT, gBT), gT) = `dest_funT (fastype_of g); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
in |
55931 | 47 |
Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
48 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
|
56484 | 50 |
fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs |
55819 | 51 |
(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
|
52 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
53 |
fun of_fp_res get = |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
54 |
map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
55 |
|
55966 | 56 |
fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); |
57 |
fun co_swap pair = case_fp fp I swap pair; |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
58 |
val mk_co_comp = HOLogic.mk_comp o co_swap; |
55966 | 59 |
val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum}; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
60 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
61 |
val dest_co_algT = co_swap o dest_funT; |
55966 | 62 |
val co_alg_argT = case_fp fp range_type domain_type; |
63 |
val co_alg_funT = case_fp fp domain_type range_type; |
|
64 |
val mk_co_product = curry (case_fp fp mk_convol mk_case_sum); |
|
65 |
val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum; |
|
66 |
val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd); |
|
67 |
val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT); |
|
68 |
val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT; |
|
69 |
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
|
70 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
71 |
val fp_absT_infos = map #absT_info fp_sugars; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
72 |
val fp_bnfs = of_fp_res #bnfs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
73 |
val pre_bnfs = map #pre_bnf fp_sugars; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
74 |
val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
75 |
val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
76 |
val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
77 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
84 |
val absTs = map #absT absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
85 |
val repTs = map #repT absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
val abss = map #abs absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
89 |
val reps = map #rep absT_infos; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
93 |
val n = length bnfs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
94 |
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
|
95 |
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
|
96 |
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
|
97 |
val m = length As; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
98 |
val live = m + n; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
99 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
100 |
val ((Xs, Bs), names_lthy) = names_lthy |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
101 |
|> mk_TFrees n |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
102 |
||>> mk_TFrees m; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
103 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
104 |
val allAs = As @ Xs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
105 |
val allBs = Bs @ Xs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
106 |
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
|
107 |
val thetaBs = As ~~ Bs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
108 |
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
|
109 |
val fold_thetaAs = Xs ~~ fpTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
110 |
val fold_thetaBs = Xs ~~ fpTs'; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
111 |
val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
112 |
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
|
113 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
114 |
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
|
115 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
in |
55966 | 119 |
((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
|
120 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
121 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
|
55819 | 127 |
val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; |
128 |
val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; |
|
129 |
val fp_repAs = map2 mk_rep absATs fp_reps; |
|
130 |
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
|
131 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
132 |
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
|
133 |
|> mk_Frees' "R" phiTs |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
134 |
||>> 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
|
135 |
||>> mk_Frees "x" xTs |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
136 |
||>> mk_Frees "y" yTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
137 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
138 |
val rels = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
139 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
140 |
fun find_rel T As Bs = fp_nesty_bnfss |
55394
d5ebe055b599
more liberal merging of BNFs and constructor sugar
blanchet
parents:
55067
diff
changeset
|
141 |
|> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf)) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
142 |
|> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
143 |
|> Option.map (fn bnf => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
|> 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
|
147 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
148 |
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
|
149 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
154 |
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
|
155 |
end |
54244 | 156 |
| mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As) |
157 |
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
|
158 |
| 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
|
159 |
in |
54298
347c3b0cab44
handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)
traytel
parents:
54244
diff
changeset
|
160 |
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
|
161 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
162 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
163 |
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
|
164 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
165 |
val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
166 |
val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm) |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
167 |
|> map (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
|
168 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
169 |
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
|
170 |
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
|
171 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
172 |
fun cast castA castB pre_rel = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
173 |
let |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
174 |
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
|
175 |
(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
|
176 |
in |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
177 |
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
|
178 |
(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
|
179 |
end; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
180 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
181 |
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
|
182 |
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
|
183 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
184 |
val rel_xtor_co_induct_thm = |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
185 |
mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
186 |
xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
187 |
lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
188 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
189 |
val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
190 |
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
|
191 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
192 |
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
|
193 |
(case fp of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
194 |
Least_FP => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
195 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
196 |
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
|
197 |
|> 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
|
198 |
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
|
199 |
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
|
200 |
in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
201 |
val cts = map (SOME o certify 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
|
202 |
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
|
203 |
@{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
|
204 |
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
|
205 |
@{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
|
206 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
207 |
cterm_instantiate_pos cts rel_xtor_co_induct_thm |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
208 |
|> singleton (Proof_Context.export names_lthy lthy) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
209 |
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
210 |
|> 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
|
211 |
|> 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
|
212 |
|> 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
|
213 |
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
|
214 |
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
|
215 |
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
|
216 |
|> 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
|
217 |
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
|
218 |
end |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
219 |
| Greatest_FP => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
220 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
221 |
val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
222 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
223 |
cterm_instantiate_pos cts rel_xtor_co_induct_thm |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
224 |
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
225 |
|> 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
|
226 |
|> 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
|
227 |
|> 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
|
228 |
end); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
229 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
230 |
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
|
231 |
val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
232 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
233 |
val rec_strTs = map2 mk_co_algT rec_preTs Xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
234 |
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
|
235 |
|
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
|
236 |
val ((rec_strs, rec_strs'), names_lthy) = names_lthy |
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
|
237 |
|> mk_Frees' "s" rec_strTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
238 |
|
55868 | 239 |
val co_recs = of_fp_res #xtor_co_recs; |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
240 |
val ns = map (length o #Ts o #fp_res) fp_sugars; |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
241 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56638
diff
changeset
|
242 |
fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
243 |
| substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
244 |
| substT _ T = T; |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
245 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
246 |
val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
247 |
|
55899
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
248 |
fun foldT_of_recT recT = |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
249 |
let |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
250 |
val ((FTXs, Xs), TX) = strip_fun_type recT |>> map_split dest_co_algT; |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
251 |
fun subst (Type (C, Ts as [_, X])) = |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
252 |
if C = co_productC andalso member op = Xs X then X else Type (C, map subst Ts) |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
253 |
| subst (Type (C, Ts)) = Type (C, map subst Ts) |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
254 |
| subst T = T; |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
255 |
in |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
256 |
map2 (mk_co_algT o subst) FTXs Xs ---> TX |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
257 |
end; |
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
258 |
|
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
259 |
fun force_rec i TU TU_rec raw_rec = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
260 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
261 |
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
|
262 |
|
55899
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
263 |
val approx_rec = raw_rec |
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
|
264 |
|> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
265 |
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
|
266 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
267 |
fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
268 |
val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
269 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
270 |
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
|
271 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
272 |
val fold_pre_deads_only_Ts = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
273 |
map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs'; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
274 |
|
56487
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
275 |
val (clique, TUs) = |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
276 |
map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) |
55478
3a6efda01da4
made N2M more robust w.r.t. identical nested types
traytel
parents:
55414
diff
changeset
|
277 |
|>> map subst |
56487
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
278 |
|> `(fn (_, Ys) => |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
279 |
nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs)) |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
280 |
||> uncurry (map2 mk_co_algT); |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
281 |
val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs; |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
282 |
val js = find_indices (fn ((cl, cand), TU) => |
961b34963fa4
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
traytel
parents:
56486
diff
changeset
|
283 |
cl = 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
|
284 |
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
|
285 |
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
|
286 |
force_typ names_lthy (Tpats ---> TU) raw_rec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
287 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
288 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
289 |
fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t = |
55966 | 290 |
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
|
291 |
(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
|
292 |
|
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
|
293 |
fun mk_rec b_opt recs lthy TU = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
294 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
295 |
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
|
296 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
297 |
val x = co_alg_argT TU; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
298 |
val i = find_index (fn T => x = T) Xs; |
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
|
299 |
val TUrec = |
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
|
300 |
(case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of |
55868 | 301 |
NONE => |
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
|
302 |
force_rec i TU |
55899
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55894
diff
changeset
|
303 |
(TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
304 |
| SOME f => f); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
305 |
|
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
|
306 |
val TUs = binder_fun_types (fastype_of TUrec); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
307 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
308 |
fun mk_s TU' = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
309 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
310 |
fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
311 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
312 |
val i = find_index (fn T => co_alg_argT TU' = T) Xs; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
313 |
val fp_abs = nth fp_abss i; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
314 |
val fp_rep = nth fp_reps i; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
315 |
val abs = nth abss i; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
316 |
val rep = nth reps i; |
54233 | 317 |
val sF = co_alg_funT TU'; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
318 |
val sF' = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
319 |
mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
320 |
handle Term.TYPE _ => sF; |
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
|
321 |
val F = nth rec_preTs i; |
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
|
322 |
val s = nth rec_strs i; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
323 |
in |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
324 |
if sF = F then s |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
325 |
else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
326 |
else |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
327 |
let |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
328 |
val smapT = replicate live dummyT ---> mk_co_algT sF' F; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
329 |
fun hidden_to_unit t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
330 |
Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
331 |
val smap = map_of_bnf (nth bnfs i) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
332 |
|> force_typ names_lthy smapT |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
333 |
|> hidden_to_unit; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
334 |
val smap_argTs = strip_typeN live (fastype_of smap) |> fst; |
54233 | 335 |
fun mk_smap_arg TU = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
336 |
(if domain_type TU = range_type TU then |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
337 |
HOLogic.id_const (domain_type TU) |
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
|
338 |
else |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
339 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
340 |
val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
341 |
val T = mk_co_algT TY U; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
342 |
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
|
343 |
(case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
344 |
SOME f => mk_co_product f |
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
|
345 |
(fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X)))) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
346 |
| NONE => mk_map_co_product |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
347 |
(build_map lthy co_proj1_const |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
348 |
(dest_funT (mk_co_algT (dest_co_productT TY |> fst) U))) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
349 |
(HOLogic.id_const X)) |
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
|
350 |
end) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
351 |
val smap_args = map mk_smap_arg smap_argTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
352 |
in |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
353 |
mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
354 |
(mk_co_comp (s, Term.list_comb (smap, smap_args))) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
355 |
end |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
356 |
end; |
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
|
357 |
val t = Term.list_comb (TUrec, map mk_s TUs); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
358 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
359 |
(case b_opt of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
360 |
NONE => ((t, Drule.dummy_thm), lthy) |
54233 | 361 |
| SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []), |
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
|
362 |
fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
363 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
364 |
|
55966 | 365 |
val recN = case_fp fp ctor_recN dtor_corecN; |
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
|
366 |
fun mk_recs lthy = |
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
|
367 |
fold2 (fn TU => fn b => fn ((recs, defs), lthy) => |
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
|
368 |
mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs))) |
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
|
369 |
resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
370 |
|>> apfst rev o apsnd rev; |
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
|
371 |
val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy |
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
|
372 |
|> mk_recs |
53331
20440c789759
prove theorem in the right context (that knows about local variables)
traytel
parents:
53309
diff
changeset
|
373 |
||> `Local_Theory.restore; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
374 |
|
53331
20440c789759
prove theorem in the right context (that knows about local variables)
traytel
parents:
53309
diff
changeset
|
375 |
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
|
376 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
377 |
val co_recs = map (Morphism.term phi) raw_co_recs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
378 |
|
56486 | 379 |
val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms |
380 |
|> maps (fn thm => [thm, thm RS rewrite_comp_comp]); |
|
55868 | 381 |
|
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
|
382 |
val xtor_co_rec_thms = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
383 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
384 |
val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
385 |
val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
386 |
val pre_rec_maps = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
387 |
map2 (fn Ds => fn bnf => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
388 |
Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
389 |
map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs)) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
390 |
Dss bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
391 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
392 |
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
|
393 |
let |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
394 |
val lhs = mk_co_comp (f, xtor); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
395 |
val rhs = mk_co_comp (s, smap); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
396 |
in |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
397 |
HOLogic.mk_eq (lhs, |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
398 |
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
|
399 |
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
|
400 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
401 |
|
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
|
402 |
val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
403 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
404 |
val pre_map_defs = no_refl (map map_def_of_bnf bnfs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
405 |
val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
406 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
407 |
val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs)); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
408 |
|
55868 | 409 |
val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
410 |
|
55966 | 411 |
val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: |
55932 | 412 |
map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @ |
413 |
@{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id}; |
|
55966 | 414 |
val rec_thms = fold_thms @ case_fp fp |
55932 | 415 |
@{thms fst_convol map_prod_o_convol convol_o} |
55931 | 416 |
@{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum}; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
417 |
|
55810 | 418 |
val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
419 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
420 |
val map_thms = no_refl (maps (fn bnf => |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
421 |
let val map_comp0 = map_comp0_of_bnf bnf RS sym |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
422 |
in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @ |
55966 | 423 |
remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc}) |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
424 |
(map2 (fn thm => fn bnf => |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
425 |
@{thm type_copy_map_comp0_undo} OF |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
426 |
(replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
427 |
rewrite_comp_comp) |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
428 |
type_definitions bnfs); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
429 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
430 |
fun mk_Rep_o_Abs thm = thm RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
431 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
432 |
val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
433 |
val Rep_o_Abss = map mk_Rep_o_Abs type_definitions; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
434 |
|
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
|
435 |
fun tac {context = ctxt, prems = _} = |
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
|
436 |
unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs, |
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
|
437 |
fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
438 |
CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
439 |
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
|
440 |
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
|
441 |
|> HOLogic.mk_Trueprop |
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
|
442 |
|> fold_rev Logic.all rec_strs |
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
|
443 |
|> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac) |
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
|
444 |
|> 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
|
445 |
|> 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
|
446 |
|> 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
|
447 |
|> 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
|
448 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
449 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
450 |
(* 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
|
451 |
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
|
452 |
val fp_res = |
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
|
453 |
({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, |
55868 | 454 |
xtor_co_recs = co_recs, 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
|
455 |
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
|
456 |
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
|
457 |
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
|
458 |
dtor_injects = of_fp_res #dtor_injects (*too general types*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
459 |
xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
460 |
xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*), |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
461 |
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*), |
55868 | 462 |
xtor_co_rec_thms = xtor_co_rec_thms, |
463 |
xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*), |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
464 |
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm} |
54740 | 465 |
|> 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
|
466 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
467 |
(fp_res, lthy) |
54242 | 468 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
469 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
470 |
end; |