|
1 (* Title: HOL/Codatatype/Tools/bnf_comp.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Composition of bounded natural functors. |
|
7 *) |
|
8 |
|
9 signature BNF_COMP = |
|
10 sig |
|
11 type unfold_thms |
|
12 val empty_unfold: unfold_thms |
|
13 val map_unfolds_of: unfold_thms -> thm list |
|
14 val set_unfoldss_of: unfold_thms -> thm list list |
|
15 val rel_unfolds_of: unfold_thms -> thm list |
|
16 val pred_unfolds_of: unfold_thms -> thm list |
|
17 |
|
18 val default_comp_sort: (string * sort) list list -> (string * sort) list |
|
19 val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) -> |
|
20 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context -> |
|
21 (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context) |
|
22 val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context |
|
23 val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> |
|
24 BNF_Def.BNF * local_theory |
|
25 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
|
26 (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context -> |
|
27 (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context)) |
|
28 end; |
|
29 |
|
30 structure BNF_Comp : BNF_COMP = |
|
31 struct |
|
32 |
|
33 open BNF_Def |
|
34 open BNF_Util |
|
35 open BNF_Tactics |
|
36 open BNF_Comp_Tactics |
|
37 |
|
38 type unfold_thms = { |
|
39 map_unfolds: thm list, |
|
40 set_unfoldss: thm list list, |
|
41 rel_unfolds: thm list, |
|
42 pred_unfolds: thm list |
|
43 }; |
|
44 |
|
45 fun add_to_thms thms NONE = thms |
|
46 | add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms; |
|
47 fun adds_to_thms thms NONE = thms |
|
48 | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_refl news) thms; |
|
49 |
|
50 fun mk_unfold_thms maps setss rels preds = |
|
51 {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds}; |
|
52 |
|
53 val empty_unfold = mk_unfold_thms [] [] [] []; |
|
54 |
|
55 fun add_to_unfold_opt map_opt sets_opt rel_opt pred_opt |
|
56 {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds} = { |
|
57 map_unfolds = add_to_thms maps map_opt, |
|
58 set_unfoldss = adds_to_thms setss sets_opt, |
|
59 rel_unfolds = add_to_thms rels rel_opt, |
|
60 pred_unfolds = add_to_thms preds pred_opt}; |
|
61 |
|
62 fun add_to_unfold map sets rel pred = |
|
63 add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred); |
|
64 |
|
65 val map_unfolds_of = #map_unfolds; |
|
66 val set_unfoldss_of = #set_unfoldss; |
|
67 val rel_unfolds_of = #rel_unfolds; |
|
68 val pred_unfolds_of = #pred_unfolds; |
|
69 |
|
70 val bdTN = "bdT"; |
|
71 |
|
72 val compN = "comp_" |
|
73 fun mk_killN n = "kill" ^ string_of_int n ^ "_"; |
|
74 fun mk_liftN n = "lift" ^ string_of_int n ^ "_"; |
|
75 fun mk_permuteN src dest = |
|
76 "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_"; |
|
77 |
|
78 val no_thm = refl; |
|
79 val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong}; |
|
80 val abs_pred_sym = sym RS @{thm abs_pred_def}; |
|
81 val abs_pred_sym_pred_abs = abs_pred_sym RS @{thm pred_def_abs}; |
|
82 |
|
83 (*copied from Envir.expand_term_free*) |
|
84 fun expand_term_const defs = |
|
85 let |
|
86 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; |
|
87 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; |
|
88 in Envir.expand_term get end; |
|
89 |
|
90 fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) = |
|
91 let |
|
92 val olive = live_of_bnf outer; |
|
93 val onwits = nwits_of_bnf outer; |
|
94 val odead = dead_of_bnf outer; |
|
95 val inner = hd inners; |
|
96 val ilive = live_of_bnf inner; |
|
97 val ideads = map dead_of_bnf inners; |
|
98 val inwitss = map nwits_of_bnf inners; |
|
99 |
|
100 (* TODO: check olive = length inners > 0, |
|
101 forall inner from inners. ilive = live, |
|
102 forall inner from inners. idead = dead *) |
|
103 |
|
104 val (oDs, lthy1) = apfst (map TFree) |
|
105 (Variable.invent_types (replicate odead HOLogic.typeS) lthy); |
|
106 val (Dss, lthy2) = apfst (map (map TFree)) |
|
107 (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1); |
|
108 val (Ass, lthy3) = apfst (replicate ilive o map TFree) |
|
109 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2); |
|
110 val As = if ilive > 0 then hd Ass else []; |
|
111 val Ass_repl = replicate olive As; |
|
112 val (Bs, _(*lthy4*)) = apfst (map TFree) |
|
113 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3); |
|
114 val Bss_repl = replicate olive Bs; |
|
115 |
|
116 val (((fs', Asets), xs), _(*names_lthy*)) = lthy |
|
117 |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs) |
|
118 ||>> mk_Frees "A" (map (HOLogic.mk_setT) As) |
|
119 ||>> mk_Frees "x" As; |
|
120 |
|
121 val CAs = map3 mk_T_of_bnf Dss Ass_repl inners; |
|
122 val CCA = mk_T_of_bnf oDs CAs outer; |
|
123 val CBs = map3 mk_T_of_bnf Dss Bss_repl inners; |
|
124 val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; |
|
125 val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; |
|
126 val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners; |
|
127 val outer_bd = mk_bd_of_bnf oDs CAs outer; |
|
128 |
|
129 (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) |
|
130 val comp_map = fold_rev Term.abs fs' |
|
131 (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, |
|
132 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o |
|
133 mk_map_of_bnf Ds As Bs) Dss inners)); |
|
134 |
|
135 (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) |
|
136 (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) |
|
137 fun mk_comp_set i = |
|
138 let |
|
139 val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i); |
|
140 val outer_set = mk_collect |
|
141 (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer) |
|
142 (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T); |
|
143 val inner_sets = map (fn sets => nth sets i) inner_setss; |
|
144 val outer_map = mk_map_of_bnf oDs CAs setTs outer; |
|
145 val map_inner_sets = Term.list_comb (outer_map, inner_sets); |
|
146 val collect_image = mk_collect |
|
147 (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets) |
|
148 (CCA --> HOLogic.mk_setT T); |
|
149 in |
|
150 (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets], |
|
151 HOLogic.mk_comp (mk_Union T, collect_image)) |
|
152 end; |
|
153 |
|
154 val (comp_sets, comp_sets_alt) = map_split mk_comp_set (0 upto ilive - 1); |
|
155 |
|
156 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) |
|
157 val comp_bd = Term.absdummy CCA (mk_cprod |
|
158 (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd); |
|
159 |
|
160 fun comp_map_id_tac {context = ctxt, ...} = |
|
161 let |
|
162 (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite |
|
163 rules*) |
|
164 val thms = (map map_id_of_bnf inners |
|
165 |> map (`(Term.size_of_term o Thm.prop_of)) |
|
166 |> sort (rev_order o int_ord o pairself fst) |
|
167 |> map snd) @ [map_id_of_bnf outer]; |
|
168 in |
|
169 (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1 |
|
170 end; |
|
171 |
|
172 fun comp_map_comp_tac _ = |
|
173 mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer) |
|
174 (map map_comp_of_bnf inners); |
|
175 |
|
176 fun mk_single_comp_set_natural_tac i _ = |
|
177 mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer) |
|
178 (collect_set_natural_of_bnf outer) |
|
179 (map ((fn thms => nth thms i) o set_natural_of_bnf) inners); |
|
180 |
|
181 val comp_set_natural_tacs = map mk_single_comp_set_natural_tac (0 upto ilive - 1); |
|
182 |
|
183 fun comp_bd_card_order_tac _ = |
|
184 mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); |
|
185 |
|
186 fun comp_bd_cinfinite_tac _ = |
|
187 mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer); |
|
188 |
|
189 val comp_set_alt_thms = |
|
190 if ! quick_and_dirty then |
|
191 replicate ilive no_thm |
|
192 else |
|
193 map (fn goal => Skip_Proof.prove lthy [] [] goal |
|
194 (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))) |
|
195 (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) comp_sets comp_sets_alt); |
|
196 |
|
197 fun comp_map_cong_tac _ = |
|
198 mk_comp_map_cong_tac comp_set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners); |
|
199 |
|
200 val comp_set_bd_tacs = |
|
201 if ! quick_and_dirty then |
|
202 replicate (length comp_set_alt_thms) (K all_tac) |
|
203 else |
|
204 let |
|
205 val outer_set_bds = set_bd_of_bnf outer; |
|
206 val inner_set_bdss = map set_bd_of_bnf inners; |
|
207 val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; |
|
208 fun comp_single_set_bd_thm i j = |
|
209 @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i, |
|
210 nth outer_set_bds j] |
|
211 val single_set_bd_thmss = |
|
212 map ((fn f => map f (0 upto olive - 1)) o comp_single_set_bd_thm) (0 upto ilive - 1); |
|
213 in |
|
214 map2 (fn comp_set_alt => fn single_set_bds => fn {context, ...} => |
|
215 mk_comp_set_bd_tac context comp_set_alt single_set_bds) |
|
216 comp_set_alt_thms single_set_bd_thmss |
|
217 end; |
|
218 |
|
219 val comp_in_alt_thm = |
|
220 if ! quick_and_dirty then |
|
221 no_thm |
|
222 else |
|
223 let |
|
224 val comp_in = mk_in Asets comp_sets CCA; |
|
225 val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; |
|
226 val goal = |
|
227 fold_rev Logic.all Asets |
|
228 (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt))); |
|
229 in |
|
230 Skip_Proof.prove lthy [] [] goal |
|
231 (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms) |
|
232 end; |
|
233 |
|
234 fun comp_in_bd_tac _ = |
|
235 mk_comp_in_bd_tac comp_in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer) |
|
236 (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer); |
|
237 |
|
238 fun comp_map_wpull_tac _ = |
|
239 mk_map_wpull_tac comp_in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer); |
|
240 |
|
241 val tacs = [comp_map_id_tac, comp_map_comp_tac, comp_map_cong_tac] @ comp_set_natural_tacs @ |
|
242 [comp_bd_card_order_tac, comp_bd_cinfinite_tac] @ comp_set_bd_tacs @ |
|
243 [comp_in_bd_tac, comp_map_wpull_tac]; |
|
244 |
|
245 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; |
|
246 |
|
247 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) |
|
248 (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) |
|
249 Dss inwitss inners); |
|
250 |
|
251 val inner_witsss = map (map (nth inner_witss) o fst) outer_wits; |
|
252 |
|
253 val comp_wits = (inner_witsss, (map (single o snd) outer_wits)) |
|
254 |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit))) |
|
255 |> flat |
|
256 |> map (`(fn t => Term.add_frees t [])) |
|
257 |> minimize_wits |
|
258 |> map (fn (frees, t) => fold absfree frees t); |
|
259 |
|
260 fun wit_tac {context = ctxt, ...} = |
|
261 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer) |
|
262 (maps wit_thms_of_bnf inners); |
|
263 |
|
264 val (bnf', lthy') = |
|
265 add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) |
|
266 ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy; |
|
267 |
|
268 val outer_rel_Gr = rel_Gr_of_bnf outer RS sym; |
|
269 val outer_rel_cong = rel_cong_of_bnf outer; |
|
270 |
|
271 val comp_rel_unfold_thm = |
|
272 trans OF [rel_def_of_bnf bnf', |
|
273 trans OF [comp_in_alt_thm RS @{thm subst_rel_def}, |
|
274 trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF |
|
275 [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]}, |
|
276 rel_converse_of_bnf outer RS sym], outer_rel_Gr], |
|
277 trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF |
|
278 (map (fn bnf => rel_def_of_bnf bnf RS sym) inners)]]]]; |
|
279 |
|
280 val comp_pred_unfold_thm = Collect_split_box_equals OF [comp_rel_unfold_thm, |
|
281 pred_def_of_bnf bnf' RS abs_pred_sym, |
|
282 trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners), |
|
283 pred_def_of_bnf outer RS abs_pred_sym]]; |
|
284 |
|
285 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
|
286 comp_rel_unfold_thm comp_pred_unfold_thm unfold; |
|
287 in |
|
288 (bnf', (unfold', lthy')) |
|
289 end; |
|
290 |
|
291 fun clean_compose_bnf_cmd (outer, inners) lthy = |
|
292 let |
|
293 val outer = the (bnf_of lthy outer) |
|
294 val inners = map (the o bnf_of lthy) inners |
|
295 val b = name_of_bnf outer |
|
296 |> Binding.prefix_name compN |
|
297 |> Binding.suffix_name ("_" ^ implode (map (Binding.name_of o name_of_bnf) inners)); |
|
298 in |
|
299 (snd o snd) (clean_compose_bnf Dont_Inline I b outer inners |
|
300 (empty_unfold, lthy)) |
|
301 end; |
|
302 |
|
303 (* Killing live variables *) |
|
304 |
|
305 fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
|
306 let |
|
307 val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf); |
|
308 val live = live_of_bnf bnf; |
|
309 val dead = dead_of_bnf bnf; |
|
310 val nwits = nwits_of_bnf bnf; |
|
311 |
|
312 (* TODO: check 0 < n <= live *) |
|
313 |
|
314 val (Ds, lthy1) = apfst (map TFree) |
|
315 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
316 val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree) |
|
317 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
318 val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree) |
|
319 (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2); |
|
320 |
|
321 val ((Asets, lives), _(*names_lthy*)) = lthy |
|
322 |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As)) |
|
323 ||>> mk_Frees "x" (drop n As); |
|
324 val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives; |
|
325 |
|
326 val T = mk_T_of_bnf Ds As bnf; |
|
327 |
|
328 (*bnf.map id ... id*) |
|
329 val killN_map = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); |
|
330 |
|
331 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
332 val killN_sets = drop n bnf_sets; |
|
333 |
|
334 (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*) |
|
335 val bnf_bd = mk_bd_of_bnf Ds As bnf; |
|
336 val killN_bd = mk_cprod |
|
337 (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd; |
|
338 |
|
339 fun killN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
|
340 fun killN_map_comp_tac {context, ...} = |
|
341 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
|
342 rtac refl 1; |
|
343 fun killN_map_cong_tac {context, ...} = |
|
344 mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf); |
|
345 val killN_set_natural_tacs = |
|
346 map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); |
|
347 fun killN_bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
|
348 fun killN_bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
|
349 val killN_set_bd_tacs = |
|
350 map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
|
351 (drop n (set_bd_of_bnf bnf)); |
|
352 |
|
353 val killN_in_alt_thm = |
|
354 if ! quick_and_dirty then |
|
355 no_thm |
|
356 else |
|
357 let |
|
358 val killN_in = mk_in Asets killN_sets T; |
|
359 val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
|
360 val goal = |
|
361 fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt))); |
|
362 in |
|
363 Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |
|
364 end; |
|
365 |
|
366 fun killN_in_bd_tac _ = |
|
367 mk_killN_in_bd_tac n (live > n) killN_in_alt_thm (in_bd_of_bnf bnf) |
|
368 (bd_Card_order_of_bnf bnf) (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf); |
|
369 fun killN_map_wpull_tac _ = |
|
370 mk_map_wpull_tac killN_in_alt_thm [] (map_wpull_of_bnf bnf); |
|
371 |
|
372 val tacs = [killN_map_id_tac, killN_map_comp_tac, killN_map_cong_tac] @ killN_set_natural_tacs @ |
|
373 [killN_bd_card_order_tac, killN_bd_cinfinite_tac] @ killN_set_bd_tacs @ |
|
374 [killN_in_bd_tac, killN_map_wpull_tac]; |
|
375 |
|
376 val wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; |
|
377 |
|
378 val killN_wits = map (fn t => fold absfree (Term.add_frees t []) t) |
|
379 (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) wits); |
|
380 |
|
381 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
382 |
|
383 val (bnf', lthy') = |
|
384 add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) |
|
385 ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy; |
|
386 |
|
387 val rel_Gr = rel_Gr_of_bnf bnf RS sym; |
|
388 |
|
389 val killN_rel_unfold_thm = |
|
390 trans OF [rel_def_of_bnf bnf', |
|
391 trans OF [killN_in_alt_thm RS @{thm subst_rel_def}, |
|
392 trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF |
|
393 [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym], |
|
394 rel_Gr], |
|
395 trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF |
|
396 (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @ |
|
397 replicate (live - n) @{thm Gr_fst_snd})]]]]; |
|
398 |
|
399 val killN_pred_unfold_thm = Collect_split_box_equals OF |
|
400 [Local_Defs.unfold lthy' @{thms Id_def'} killN_rel_unfold_thm, |
|
401 pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym]; |
|
402 |
|
403 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
|
404 killN_rel_unfold_thm killN_pred_unfold_thm unfold; |
|
405 in |
|
406 (bnf', (unfold', lthy')) |
|
407 end; |
|
408 |
|
409 fun killN_bnf_cmd (n, raw_bnf) lthy = |
|
410 (snd o snd) (killN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); |
|
411 |
|
412 (* Adding dummy live variables *) |
|
413 |
|
414 fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
|
415 let |
|
416 val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf); |
|
417 val live = live_of_bnf bnf; |
|
418 val dead = dead_of_bnf bnf; |
|
419 val nwits = nwits_of_bnf bnf; |
|
420 |
|
421 (* TODO: check 0 < n *) |
|
422 |
|
423 val (Ds, lthy1) = apfst (map TFree) |
|
424 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
425 val ((newAs, As), lthy2) = apfst (chop n o map TFree) |
|
426 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1); |
|
427 val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree) |
|
428 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2); |
|
429 |
|
430 val (Asets, _(*names_lthy*)) = lthy |
|
431 |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As)); |
|
432 |
|
433 val T = mk_T_of_bnf Ds As bnf; |
|
434 |
|
435 (*%f1 ... fn. bnf.map*) |
|
436 val liftN_map = |
|
437 fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); |
|
438 |
|
439 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
440 val liftN_sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; |
|
441 |
|
442 val liftN_bd = mk_bd_of_bnf Ds As bnf; |
|
443 |
|
444 fun liftN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
|
445 fun liftN_map_comp_tac {context, ...} = |
|
446 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
|
447 rtac refl 1; |
|
448 fun liftN_map_cong_tac {context, ...} = |
|
449 rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1); |
|
450 val liftN_set_natural_tacs = |
|
451 if ! quick_and_dirty then |
|
452 replicate (n + live) (K all_tac) |
|
453 else |
|
454 replicate n (K empty_natural_tac) @ |
|
455 map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf); |
|
456 fun liftN_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
|
457 fun liftN_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
458 val liftN_set_bd_tacs = |
|
459 if ! quick_and_dirty then |
|
460 replicate (n + live) (K all_tac) |
|
461 else |
|
462 replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @ |
|
463 (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
|
464 |
|
465 val liftN_in_alt_thm = |
|
466 if ! quick_and_dirty then |
|
467 no_thm |
|
468 else |
|
469 let |
|
470 val liftN_in = mk_in Asets liftN_sets T; |
|
471 val liftN_in_alt = mk_in (drop n Asets) bnf_sets T; |
|
472 val goal = |
|
473 fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt))) |
|
474 in |
|
475 Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |
|
476 end; |
|
477 |
|
478 fun liftN_in_bd_tac _ = |
|
479 mk_liftN_in_bd_tac n liftN_in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf); |
|
480 fun liftN_map_wpull_tac _ = |
|
481 mk_map_wpull_tac liftN_in_alt_thm [] (map_wpull_of_bnf bnf); |
|
482 |
|
483 val tacs = [liftN_map_id_tac, liftN_map_comp_tac, liftN_map_cong_tac] @ liftN_set_natural_tacs @ |
|
484 [liftN_bd_card_order_tac, liftN_bd_cinfinite_tac] @ liftN_set_bd_tacs @ |
|
485 [liftN_in_bd_tac, liftN_map_wpull_tac]; |
|
486 |
|
487 val liftN_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
488 |
|
489 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
490 |
|
491 val (bnf', lthy') = |
|
492 add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) |
|
493 ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy; |
|
494 |
|
495 val liftN_rel_unfold_thm = |
|
496 trans OF [rel_def_of_bnf bnf', |
|
497 trans OF [liftN_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]]; |
|
498 |
|
499 val liftN_pred_unfold_thm = Collect_split_box_equals OF [liftN_rel_unfold_thm, |
|
500 pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym]; |
|
501 |
|
502 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
|
503 liftN_rel_unfold_thm liftN_pred_unfold_thm unfold; |
|
504 in |
|
505 (bnf', (unfold', lthy')) |
|
506 end; |
|
507 |
|
508 fun liftN_bnf_cmd (n, raw_bnf) lthy = |
|
509 (snd o snd) (liftN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); |
|
510 |
|
511 (* Changing the order of live variables *) |
|
512 |
|
513 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else |
|
514 let |
|
515 val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf); |
|
516 val live = live_of_bnf bnf; |
|
517 val dead = dead_of_bnf bnf; |
|
518 val nwits = nwits_of_bnf bnf; |
|
519 fun permute xs = mk_permute src dest xs; |
|
520 fun permute_rev xs = mk_permute dest src xs; |
|
521 |
|
522 val (Ds, lthy1) = apfst (map TFree) |
|
523 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
524 val (As, lthy2) = apfst (map TFree) |
|
525 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
526 val (Bs, _(*lthy3*)) = apfst (map TFree) |
|
527 (Variable.invent_types (replicate live HOLogic.typeS) lthy2); |
|
528 |
|
529 val (Asets, _(*names_lthy*)) = lthy |
|
530 |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As)); |
|
531 |
|
532 val T = mk_T_of_bnf Ds As bnf; |
|
533 |
|
534 (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*) |
|
535 val permute_map = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) |
|
536 (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, |
|
537 permute_rev (map Bound ((live - 1) downto 0)))); |
|
538 |
|
539 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
540 val permute_sets = permute bnf_sets; |
|
541 |
|
542 val permute_bd = mk_bd_of_bnf Ds As bnf; |
|
543 |
|
544 fun permute_map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
|
545 fun permute_map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; |
|
546 fun permute_map_cong_tac {context, ...} = |
|
547 rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1); |
|
548 val permute_set_natural_tacs = |
|
549 permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf)); |
|
550 fun permute_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
|
551 fun permute_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
552 val permute_set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
|
553 |
|
554 val permute_in_alt_thm = |
|
555 if ! quick_and_dirty then |
|
556 no_thm |
|
557 else |
|
558 let |
|
559 val permute_in = mk_in Asets permute_sets T; |
|
560 val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T; |
|
561 val goal = |
|
562 fold_rev Logic.all Asets |
|
563 (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt))); |
|
564 in |
|
565 Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest)) |
|
566 end; |
|
567 |
|
568 fun permute_in_bd_tac _ = |
|
569 mk_permute_in_bd_tac src dest permute_in_alt_thm (in_bd_of_bnf bnf) |
|
570 (bd_Card_order_of_bnf bnf); |
|
571 fun permute_map_wpull_tac _ = |
|
572 mk_map_wpull_tac permute_in_alt_thm [] (map_wpull_of_bnf bnf); |
|
573 |
|
574 val tacs = [permute_map_id_tac, permute_map_comp_tac, permute_map_cong_tac] @ |
|
575 permute_set_natural_tacs @ [permute_bd_card_order_tac, permute_bd_cinfinite_tac] @ |
|
576 permute_set_bd_tacs @ [permute_in_bd_tac, permute_map_wpull_tac]; |
|
577 |
|
578 val permute_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
579 |
|
580 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
581 |
|
582 val (bnf', lthy') = |
|
583 add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) |
|
584 ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy; |
|
585 |
|
586 val permute_rel_unfold_thm = |
|
587 trans OF [rel_def_of_bnf bnf', |
|
588 trans OF [permute_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]]; |
|
589 |
|
590 val permute_pred_unfold_thm = Collect_split_box_equals OF [permute_rel_unfold_thm, |
|
591 pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym]; |
|
592 |
|
593 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
|
594 permute_rel_unfold_thm permute_pred_unfold_thm unfold; |
|
595 in |
|
596 (bnf', (unfold', lthy')) |
|
597 end; |
|
598 |
|
599 fun permute_bnf_cmd ((src, dest), raw_bnf) lthy = |
|
600 (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf)) |
|
601 (empty_unfold, lthy)); |
|
602 |
|
603 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
|
604 |
|
605 fun seal_bnf unfold b Ds bnf lthy = |
|
606 let |
|
607 val live = live_of_bnf bnf; |
|
608 val nwits = nwits_of_bnf bnf; |
|
609 |
|
610 val (As, lthy1) = apfst (map TFree) |
|
611 (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy)); |
|
612 val (Bs, _) = apfst (map TFree) |
|
613 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
614 |
|
615 val map_unfolds = filter_refl (map_unfolds_of unfold); |
|
616 val set_unfoldss = map filter_refl (set_unfoldss_of unfold); |
|
617 |
|
618 val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) |
|
619 map_unfolds); |
|
620 val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) |
|
621 set_unfoldss); |
|
622 val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds; |
|
623 val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss; |
|
624 val unfold_defs = unfold_sets o unfold_maps; |
|
625 val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf); |
|
626 val bnf_sets = map (expand_maps o expand_sets) |
|
627 (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); |
|
628 val bnf_bd = mk_bd_of_bnf Ds As bnf; |
|
629 val T = mk_T_of_bnf Ds As bnf; |
|
630 |
|
631 (*bd should only depend on dead type variables!*) |
|
632 val bd_repT = fst (dest_relT (fastype_of bnf_bd)); |
|
633 val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b; |
|
634 val params = fold Term.add_tfreesT Ds []; |
|
635 |
|
636 val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) = |
|
637 lthy |
|
638 |> Typedef.add_typedef true NONE (bdT_bind, params, NoSyn) |
|
639 (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) |
|
640 ||> `Local_Theory.restore; |
|
641 |
|
642 val phi = Proof_Context.export_morphism lthy lthy'; |
|
643 |
|
644 val bnf_bd' = mk_dir_image bnf_bd |
|
645 (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params))) |
|
646 |
|
647 val set_def = Morphism.thm phi (the (#set_def bdT_loc_info)); |
|
648 val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info); |
|
649 val Abs_cases = Morphism.thm phi (#Abs_cases bdT_loc_info); |
|
650 |
|
651 val Abs_bdT_inj = mk_Abs_inj_thm set_def Abs_inject; |
|
652 val Abs_bdT_bij = mk_Abs_bij_thm lthy' set_def Abs_inject Abs_cases; |
|
653 |
|
654 val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; |
|
655 val bd_card_order = |
|
656 @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; |
|
657 val bd_cinfinite = |
|
658 (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; |
|
659 |
|
660 val set_bds = |
|
661 map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf); |
|
662 val in_bd = |
|
663 @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf, |
|
664 @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then |
|
665 @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2}, |
|
666 bd_Card_order_of_bnf bnf]]; |
|
667 |
|
668 fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN' |
|
669 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; |
|
670 val tacs = |
|
671 map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @ |
|
672 set_natural_of_bnf bnf) @ |
|
673 map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @ |
|
674 map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]); |
|
675 |
|
676 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
677 |
|
678 fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf)); |
|
679 |
|
680 val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE |
|
681 ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy; |
|
682 |
|
683 val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf'); |
|
684 val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs'; |
|
685 |
|
686 val rel_def = unfold_defs' (rel_def_of_bnf bnf'); |
|
687 val rel_unfold = Local_Defs.unfold lthy' |
|
688 (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def; |
|
689 |
|
690 val unfold_defs'' = |
|
691 unfold_defs' o (Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf'])); |
|
692 |
|
693 val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs); |
|
694 val pred_unfold = Local_Defs.unfold lthy' |
|
695 (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def; |
|
696 |
|
697 fun note thmN thms = |
|
698 snd o Local_Theory.note |
|
699 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms); |
|
700 in |
|
701 (bnf', lthy' |
|
702 |> note rel_unfoldN [rel_unfold] |
|
703 |> note pred_unfoldN [pred_unfold]) |
|
704 end; |
|
705 |
|
706 (* Composition pipeline *) |
|
707 |
|
708 fun permute_and_kill qualify n src dest bnf = |
|
709 bnf |
|
710 |> permute_bnf qualify src dest |
|
711 #> uncurry (killN_bnf qualify n); |
|
712 |
|
713 fun lift_and_permute qualify n src dest bnf = |
|
714 bnf |
|
715 |> liftN_bnf qualify n |
|
716 #> uncurry (permute_bnf qualify src dest); |
|
717 |
|
718 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = |
|
719 let |
|
720 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
|
721 val kill_poss = map (find_indices Ds) Ass; |
|
722 val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; |
|
723 val before_kill_dest = map2 append kill_poss live_poss; |
|
724 val kill_ns = map length kill_poss; |
|
725 val (inners', (unfold', lthy')) = |
|
726 fold_map5 (fn i => permute_and_kill (qualify i)) |
|
727 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
728 kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); |
|
729 |
|
730 val Ass' = map2 (map o nth) Ass live_poss; |
|
731 val As = sort Ass'; |
|
732 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); |
|
733 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; |
|
734 val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; |
|
735 val after_lift_src = map2 append new_poss old_poss; |
|
736 val lift_ns = map (fn xs => length As - length xs) Ass'; |
|
737 in |
|
738 ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) |
|
739 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
740 lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) |
|
741 end; |
|
742 |
|
743 fun default_comp_sort Ass = |
|
744 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); |
|
745 |
|
746 fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) = |
|
747 let |
|
748 val name = Binding.name_of b; |
|
749 fun qualify i bind = |
|
750 let val namei = if i > 0 then name ^ string_of_int i else name; |
|
751 in |
|
752 if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind |
|
753 else qualify' (Binding.prefix_name namei bind) |
|
754 end; |
|
755 |
|
756 val Ass = map (map dest_TFree) tfreess; |
|
757 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; |
|
758 |
|
759 val ((kill_poss, As), (inners', (unfold', lthy'))) = |
|
760 normalize_bnfs qualify Ass Ds sort inners unfold lthy; |
|
761 |
|
762 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); |
|
763 val As = map TFree As; |
|
764 in |
|
765 apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) |
|
766 end; |
|
767 |
|
768 fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd) |
|
769 (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer)) |
|
770 (map (the o bnf_of lthy) inners) |
|
771 (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss) |
|
772 (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy)); |
|
773 |
|
774 fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) = |
|
775 ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE |
|
776 (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy)) |
|
777 | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable" |
|
778 | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) = |
|
779 let val tfrees = Term.add_tfreesT T []; |
|
780 in |
|
781 if null tfrees then |
|
782 ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy)) |
|
783 else if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then let |
|
784 val bnf = the (bnf_of lthy (Long_Name.base_name C)); |
|
785 val T' = T_of_bnf bnf; |
|
786 val deads = deads_of_bnf bnf; |
|
787 val lives = lives_of_bnf bnf; |
|
788 val tvars' = Term.add_tvarsT T' []; |
|
789 val deads_lives = |
|
790 pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) |
|
791 (deads, lives); |
|
792 val rel_def = rel_def_of_bnf bnf; |
|
793 val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_def RS sym)) |
|
794 (SOME (Local_Defs.unfold lthy [rel_def] (pred_def_of_bnf bnf) RS sym)) unfold; |
|
795 in ((bnf, deads_lives), (unfold', lthy)) end |
|
796 else |
|
797 let |
|
798 (* FIXME: we should allow several BNFs with the same base name *) |
|
799 val Tname = Long_Name.base_name C; |
|
800 val name = Binding.name_of b ^ "_" ^ Tname; |
|
801 fun qualify i bind = |
|
802 let val namei = if i > 0 then name ^ string_of_int i else name; |
|
803 in |
|
804 if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind |
|
805 else qualify' (Binding.prefix_name namei bind) |
|
806 end; |
|
807 val outer = the (bnf_of lthy Tname); |
|
808 val odead = dead_of_bnf outer; |
|
809 val olive = live_of_bnf outer; |
|
810 val oDs_pos = find_indices [TFree ("dead", [])] |
|
811 (snd (dest_Type |
|
812 (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) outer))); |
|
813 val oDs = map (nth Ts) oDs_pos; |
|
814 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); |
|
815 val ((inners, (Dss, Ass)), (unfold', lthy')) = |
|
816 apfst (apsnd split_list o split_list) |
|
817 (fold_map2 (fn i => |
|
818 bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort) |
|
819 (if length Ts' = 1 then [0] else (1 upto length Ts')) |
|
820 Ts' (unfold, lthy)); |
|
821 in |
|
822 compose_bnf const_policy (qualify 0) b sort outer inners oDs Dss Ass (unfold', lthy') |
|
823 end |
|
824 end; |
|
825 |
|
826 fun bnf_of_typ_cmd (b, rawT) lthy = (snd o snd) |
|
827 (bnf_of_typ Dont_Inline b I default_comp_sort (Syntax.read_typ lthy rawT) |
|
828 (empty_unfold, lthy)); |
|
829 |
|
830 val _ = |
|
831 Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs" |
|
832 (((Parse.binding --| Parse.$$$ "=") -- Parse.typ) >> bnf_of_typ_cmd); |
|
833 |
|
834 end; |