author | blanchet |
Wed, 23 Apr 2014 10:23:26 +0200 | |
changeset 56640 | 0a35354137a5 |
parent 56639 | c9d6b581bd3b |
child 56642 | 15cd15f9b40c |
permissions | -rw-r--r-- |
56638 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_size.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2014 |
|
4 |
||
5 |
Generation of size functions for new-style datatypes. |
|
6 |
*) |
|
7 |
||
8 |
structure BNF_LFP_Size : sig end = |
|
9 |
struct |
|
10 |
||
11 |
open BNF_Util |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
12 |
open BNF_Tactics |
56638 | 13 |
open BNF_Def |
14 |
open BNF_FP_Def_Sugar |
|
15 |
||
16 |
val size_N = "size_" |
|
17 |
||
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
18 |
val rec_o_mapN = "rec_o_map" |
56638 | 19 |
val sizeN = "size" |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
20 |
val size_o_mapN = "size_o_map" |
56638 | 21 |
|
22 |
structure Data = Theory_Data |
|
23 |
( |
|
24 |
type T = (string * (thm list * thm list)) Symtab.table; |
|
25 |
val empty = Symtab.empty; |
|
26 |
val extend = I |
|
27 |
fun merge data = Symtab.merge (K true) data; |
|
28 |
); |
|
29 |
||
30 |
val zero_nat = @{const zero_class.zero (nat)}; |
|
31 |
||
32 |
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus}, |
|
33 |
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; |
|
34 |
||
35 |
fun mk_to_natT T = T --> HOLogic.natT; |
|
36 |
||
37 |
fun mk_abs_zero_nat T = Term.absdummy T zero_nat; |
|
38 |
||
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
39 |
fun pointfill ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
40 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
41 |
fun mk_unabs_def_unused_0 n = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
42 |
funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
43 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
44 |
val rec_o_map_simp_thms = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
45 |
@{thms o_def id_apply case_prod_app case_sum_o_map_sum case_prod_o_map_prod |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
46 |
BNF_Comp.id_bnf_comp_def}; |
56638 | 47 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
48 |
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
49 |
unfold_thms_tac ctxt [rec_def] THEN |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
50 |
HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN' |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
51 |
K (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)) THEN' asm_simp_tac |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
52 |
(ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @ rec_o_map_simp_thms) ctxt)); |
56638 | 53 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
54 |
val size_o_map_simp_thms = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
55 |
@{thms o_apply prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
56 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
57 |
fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
58 |
unfold_thms_tac ctxt [size_def] THEN |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
59 |
HEADGOAL (rtac (rec_o_map RS trans) THEN' |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
60 |
asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)); |
56638 | 61 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
62 |
fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
63 |
fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs, ...} |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
64 |
: fp_sugar) :: _) thy = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
65 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
66 |
val data = Data.get thy; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
67 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
68 |
val Ts = map #T fp_sugars |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
69 |
val T_names = map (fst o dest_Type) Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
70 |
val nn = length Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
71 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
72 |
val B_ify = Term.typ_subst_atomic (As ~~ Bs); |
56638 | 73 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
74 |
val recs = map #co_rec fp_sugars; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
75 |
val rec_thmss = map #co_rec_thms fp_sugars; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
76 |
val rec_Ts as rec_T1 :: _ = map fastype_of recs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
77 |
val rec_arg_Ts = binder_fun_types rec_T1; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
78 |
val Cs = map body_type rec_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
79 |
val Cs_rho = map (rpair HOLogic.natT) Cs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
80 |
val substCnatT = Term.subst_atomic_types Cs_rho; |
56638 | 81 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
82 |
val f_Ts = map mk_to_natT As; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
83 |
val f_TsB = map mk_to_natT Bs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
84 |
val num_As = length As; |
56638 | 85 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
86 |
val f_names = map (prefix "f" o string_of_int) (1 upto num_As); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
87 |
val fs = map2 (curry Free) f_names f_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
88 |
val fsB = map2 (curry Free) f_names f_TsB; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
89 |
val As_fs = As ~~ fs; |
56638 | 90 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
91 |
val size_names = map (Long_Name.map_base_name (prefix size_N)) T_names; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
92 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
93 |
fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T' |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
94 |
| is_pair_C _ _ = false; |
56638 | 95 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
96 |
fun mk_size_of_typ (T as TFree _) = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
97 |
pair (case AList.lookup (op =) As_fs T of |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
98 |
SOME f => f |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
99 |
| NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
100 |
| mk_size_of_typ (T as Type (s, Ts)) = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
101 |
if is_pair_C s Ts then |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
102 |
pair (snd_const T) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
103 |
else if exists (exists_subtype_in As) Ts then |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
104 |
(case Symtab.lookup data s of |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
105 |
SOME (size_name, (_, size_o_maps)) => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
106 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
107 |
val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
108 |
val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
109 |
in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
110 |
fold (union Thm.eq_thm) (size_o_maps :: size_o_mapss') |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
111 |
#> pair (Term.list_comb (size_const, args)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
112 |
end |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
113 |
| NONE => pair (mk_abs_zero_nat T)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
114 |
else |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
115 |
pair (mk_abs_zero_nat T); |
56638 | 116 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
117 |
fun mk_size_of_arg t = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
118 |
mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t))); |
56638 | 119 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
120 |
fun mk_size_arg rec_arg_T size_o_maps = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
121 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
122 |
val x_Ts = binder_types rec_arg_T; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
123 |
val m = length x_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
124 |
val x_names = map (prefix "x" o string_of_int) (1 upto m); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
125 |
val xs = map2 (curry Free) x_names x_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
126 |
val (summands, size_o_maps') = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
127 |
fold_map mk_size_of_arg xs size_o_maps |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
128 |
|>> remove (op =) zero_nat; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
129 |
val sum = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
130 |
if null summands then HOLogic.zero |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
131 |
else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
132 |
in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
133 |
(fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps') |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
134 |
end; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
135 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
136 |
fun mk_size_rhs recx size_o_maps = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
137 |
let val (args, size_o_maps') = fold_map mk_size_arg rec_arg_Ts size_o_maps in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
138 |
(fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)), size_o_maps') |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
139 |
end; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
140 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
141 |
fun mk_def_binding f = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
142 |
Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name; |
56638 | 143 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
144 |
val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs []; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
145 |
val size_Ts = map fastype_of size_rhss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
146 |
val size_consts = map2 (curry Const) size_names size_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
147 |
val size_constsB = map (Term.map_types B_ify) size_consts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
148 |
val size_def_bs = map (mk_def_binding I) size_names; |
56638 | 149 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
150 |
val (size_defs, thy2) = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
151 |
thy |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
152 |
|> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), T, NoSyn)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
153 |
(size_names ~~ size_Ts)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
154 |
|> Global_Theory.add_defs false (map Thm.no_attributes (size_def_bs ~~ |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
155 |
map Logic.mk_equals (size_consts ~~ size_rhss))); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
156 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
157 |
val zeros = map mk_abs_zero_nat As; |
56638 | 158 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
159 |
val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
160 |
val overloaded_size_Ts = map fastype_of overloaded_size_rhss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
161 |
val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
162 |
val overloaded_size_def_bs = map (mk_def_binding (suffix "_overloaded")) size_names; |
56638 | 163 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
164 |
fun define_overloaded_size def_b lhs0 rhs lthy = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
165 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
166 |
val Free (c, _) = Syntax.check_term lthy lhs0; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
167 |
val (thm, lthy') = lthy |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
168 |
|> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
169 |
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
170 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
171 |
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
172 |
in (thm', lthy') end; |
56638 | 173 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
174 |
val (overloaded_size_defs, thy3) = thy2 |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
175 |
|> Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size]) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
176 |
|> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
177 |
overloaded_size_rhss |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
178 |
||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
179 |
||> Local_Theory.exit_global; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
180 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
181 |
val thy3_ctxt = Proof_Context.init_global thy3; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
182 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
183 |
val size_defs' = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
184 |
map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
185 |
val size_defs_unused_0 = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
186 |
map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
187 |
val overloaded_size_defs' = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
188 |
map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs; |
56638 | 189 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
190 |
val nested_size_maps = map (pointfill thy3_ctxt) nested_size_o_maps @ nested_size_o_maps; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
191 |
val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs); |
56638 | 192 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
193 |
fun derive_size_simp size_def' simp0 = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
194 |
(trans OF [size_def', simp0]) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
195 |
|> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @ |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
196 |
all_inj_maps @ nested_size_maps) thy3_ctxt) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
197 |
|> fold_thms thy3_ctxt size_defs_unused_0; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
198 |
fun derive_overloaded_size_simp size_def' simp0 = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
199 |
(trans OF [size_def', simp0]) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
200 |
|> unfold_thms thy3_ctxt @{thms add_0_left add_0_right} |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
201 |
|> fold_thms thy3_ctxt overloaded_size_defs'; |
56638 | 202 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
203 |
val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
204 |
val size_simps = flat size_simpss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
205 |
val overloaded_size_simpss = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
206 |
map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss; |
56638 | 207 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
208 |
val ABs = As ~~ Bs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
209 |
val g_names = map (prefix "g" o string_of_int) (1 upto num_As); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
210 |
val gs = map2 (curry Free) g_names (map (op -->) ABs); |
56638 | 211 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
212 |
val liveness = map (op <>) ABs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
213 |
val live_gs = AList.find (op =) (gs ~~ liveness) true; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
214 |
val live = length live_gs; |
56638 | 215 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
216 |
val maps0 = map map_of_bnf fp_bnfs; |
56638 | 217 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
218 |
val (rec_o_map_thmss, size_o_map_thmss) = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
219 |
if live = 0 then |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
220 |
`I (replicate nn []) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
221 |
else |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
222 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
223 |
val pre_bnfs = map #pre_bnf fp_sugars; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
224 |
val pre_map_defs = map map_def_of_bnf pre_bnfs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
225 |
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
226 |
val rec_defs = map #co_rec_def fp_sugars; |
56638 | 227 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
228 |
val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; |
56638 | 229 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
230 |
val num_rec_args = length rec_arg_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
231 |
val h_Ts = map B_ify rec_arg_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
232 |
val h_names = map (prefix "h" o string_of_int) (1 upto num_rec_args); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
233 |
val hs = map2 (curry Free) h_names h_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
234 |
val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs; |
56638 | 235 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
236 |
val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
237 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
238 |
val ABgs = ABs ~~ gs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
239 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
240 |
fun mk_rec_arg_arg (x as Free (_, T)) = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
241 |
let val U = B_ify T in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
242 |
if T = U then x else build_map thy3_ctxt (the o AList.lookup (op =) ABgs) (T, U) $ x |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
243 |
end; |
56638 | 244 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
245 |
fun mk_rec_o_map_arg rec_arg_T h = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
246 |
let |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
247 |
val x_Ts = binder_types rec_arg_T; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
248 |
val m = length x_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
249 |
val x_names = map (prefix "x" o string_of_int) (1 upto m); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
250 |
val xs = map2 (curry Free) x_names x_Ts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
251 |
val xs' = map mk_rec_arg_arg xs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
252 |
in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
253 |
fold_rev Term.lambda xs (Term.list_comb (h, xs')) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
254 |
end; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
255 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
256 |
fun mk_rec_o_map_rhs recx = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
257 |
let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
258 |
Term.list_comb (recx, args) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
259 |
end; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
260 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
261 |
val rec_o_map_rhss = map mk_rec_o_map_rhs recs; |
56638 | 262 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
263 |
val rec_o_map_goals = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
264 |
map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
265 |
val rec_o_map_thms = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
266 |
map3 (fn goal => fn rec_def => fn ctor_rec_o_map => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
267 |
Goal.prove_global thy3 [] [] goal (fn {context = ctxt, ...} => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
268 |
mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
269 |
|> Thm.close_derivation) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
270 |
rec_o_map_goals rec_defs ctor_rec_o_maps; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
271 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
272 |
val size_o_map_conds = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
273 |
if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
274 |
map (HOLogic.mk_Trueprop o mk_inj) live_gs |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
275 |
else |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
276 |
[]; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
277 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
278 |
val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
279 |
val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps; |
56638 | 280 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
281 |
val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
282 |
if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
283 |
val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
284 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
285 |
val size_o_map_goals = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
286 |
map2 (curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
287 |
curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
288 |
val size_o_map_thms = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
289 |
map3 (fn goal => fn size_def => fn rec_o_map => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
290 |
Goal.prove_global thy3 [] [] goal (fn {context = ctxt, ...} => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
291 |
mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
292 |
|> Thm.close_derivation) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
293 |
size_o_map_goals size_defs rec_o_map_thms; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
294 |
in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
295 |
pairself (map single) (rec_o_map_thms, size_o_map_thms) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
296 |
end; |
56638 | 297 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
298 |
val (_, thy4) = thy3 |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
299 |
|> fold_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
300 |
let val qualify = Binding.qualify true (Long_Name.base_name T_name) in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
301 |
Global_Theory.note_thmss "" |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
302 |
([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]), |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
303 |
((qualify (Binding.name sizeN), |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
304 |
[Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
305 |
(fn thm => Context.mapping (Code.add_default_eqn thm) I)]), |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
306 |
[(size_simps, [])]), |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
307 |
((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])] |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
308 |
|> filter_out (forall (null o fst) o snd)) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
309 |
end) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
310 |
T_names (map2 append size_simpss overloaded_size_simpss) rec_o_map_thmss size_o_map_thmss |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
311 |
||> Spec_Rules.add_global Spec_Rules.Equational (size_consts, size_simps); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
312 |
in |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
313 |
thy4 |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
314 |
|> Data.map (fold2 (fn T_name => fn size_name => |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
315 |
Symtab.update_new (T_name, (size_name, (size_simps, flat size_o_map_thmss)))) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
316 |
T_names size_names) |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
317 |
end |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
318 |
| generate_size _ thy = thy; |
56638 | 319 |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
320 |
val _ = Theory.setup (fp_sugar_interpretation generate_size); |
56638 | 321 |
|
322 |
end; |