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