|
1 (* Title: HOL/BNF/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 val ID_bnf: BNF_Def.bnf |
|
12 val DEADID_bnf: BNF_Def.bnf |
|
13 |
|
14 type unfold_set |
|
15 val empty_unfolds: unfold_set |
|
16 |
|
17 exception BAD_DEAD of typ * typ |
|
18 |
|
19 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
|
20 ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> typ -> |
|
21 unfold_set * Proof.context -> |
|
22 (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context) |
|
23 val default_comp_sort: (string * sort) list list -> (string * sort) list |
|
24 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
|
25 (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context -> |
|
26 (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context)) |
|
27 val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf -> |
|
28 Proof.context -> (BNF_Def.bnf * typ list) * local_theory |
|
29 end; |
|
30 |
|
31 structure BNF_Comp : BNF_COMP = |
|
32 struct |
|
33 |
|
34 open BNF_Def |
|
35 open BNF_Util |
|
36 open BNF_Tactics |
|
37 open BNF_Comp_Tactics |
|
38 |
|
39 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID"); |
|
40 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID"); |
|
41 |
|
42 (* TODO: Replace by "BNF_Defs.defs list" *) |
|
43 type unfold_set = { |
|
44 map_unfolds: thm list, |
|
45 set_unfoldss: thm list list, |
|
46 rel_unfolds: thm list |
|
47 }; |
|
48 |
|
49 val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []}; |
|
50 |
|
51 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; |
|
52 fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; |
|
53 |
|
54 fun add_to_unfolds map sets rel |
|
55 {map_unfolds, set_unfoldss, rel_unfolds} = |
|
56 {map_unfolds = add_to_thms map_unfolds map, |
|
57 set_unfoldss = adds_to_thms set_unfoldss sets, |
|
58 rel_unfolds = add_to_thms rel_unfolds rel}; |
|
59 |
|
60 fun add_bnf_to_unfolds bnf = |
|
61 add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf); |
|
62 |
|
63 val bdTN = "bdT"; |
|
64 |
|
65 fun mk_killN n = "_kill" ^ string_of_int n; |
|
66 fun mk_liftN n = "_lift" ^ string_of_int n; |
|
67 fun mk_permuteN src dest = |
|
68 "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest); |
|
69 |
|
70 (*copied from Envir.expand_term_free*) |
|
71 fun expand_term_const defs = |
|
72 let |
|
73 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; |
|
74 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; |
|
75 in Envir.expand_term get end; |
|
76 |
|
77 fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = |
|
78 let |
|
79 val olive = live_of_bnf outer; |
|
80 val onwits = nwits_of_bnf outer; |
|
81 val odead = dead_of_bnf outer; |
|
82 val inner = hd inners; |
|
83 val ilive = live_of_bnf inner; |
|
84 val ideads = map dead_of_bnf inners; |
|
85 val inwitss = map nwits_of_bnf inners; |
|
86 |
|
87 (* TODO: check olive = length inners > 0, |
|
88 forall inner from inners. ilive = live, |
|
89 forall inner from inners. idead = dead *) |
|
90 |
|
91 val (oDs, lthy1) = apfst (map TFree) |
|
92 (Variable.invent_types (replicate odead HOLogic.typeS) lthy); |
|
93 val (Dss, lthy2) = apfst (map (map TFree)) |
|
94 (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1); |
|
95 val (Ass, lthy3) = apfst (replicate ilive o map TFree) |
|
96 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2); |
|
97 val As = if ilive > 0 then hd Ass else []; |
|
98 val Ass_repl = replicate olive As; |
|
99 val (Bs, _(*lthy4*)) = apfst (map TFree) |
|
100 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3); |
|
101 val Bss_repl = replicate olive Bs; |
|
102 |
|
103 val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy |
|
104 |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs) |
|
105 ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs) |
|
106 ||>> mk_Frees "A" (map HOLogic.mk_setT As) |
|
107 ||>> mk_Frees "x" As; |
|
108 |
|
109 val CAs = map3 mk_T_of_bnf Dss Ass_repl inners; |
|
110 val CCA = mk_T_of_bnf oDs CAs outer; |
|
111 val CBs = map3 mk_T_of_bnf Dss Bss_repl inners; |
|
112 val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; |
|
113 val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; |
|
114 val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners; |
|
115 val outer_bd = mk_bd_of_bnf oDs CAs outer; |
|
116 |
|
117 (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) |
|
118 val mapx = fold_rev Term.abs fs' |
|
119 (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, |
|
120 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o |
|
121 mk_map_of_bnf Ds As Bs) Dss inners)); |
|
122 (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*) |
|
123 val rel = fold_rev Term.abs Qs' |
|
124 (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer, |
|
125 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o |
|
126 mk_rel_of_bnf Ds As Bs) Dss inners)); |
|
127 |
|
128 (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) |
|
129 (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) |
|
130 fun mk_set i = |
|
131 let |
|
132 val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i); |
|
133 val outer_set = mk_collect |
|
134 (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer) |
|
135 (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T); |
|
136 val inner_sets = map (fn sets => nth sets i) inner_setss; |
|
137 val outer_map = mk_map_of_bnf oDs CAs setTs outer; |
|
138 val map_inner_sets = Term.list_comb (outer_map, inner_sets); |
|
139 val collect_image = mk_collect |
|
140 (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets) |
|
141 (CCA --> HOLogic.mk_setT T); |
|
142 in |
|
143 (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets], |
|
144 HOLogic.mk_comp (mk_Union T, collect_image)) |
|
145 end; |
|
146 |
|
147 val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); |
|
148 |
|
149 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) |
|
150 val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; |
|
151 |
|
152 fun map_id0_tac _ = |
|
153 mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) |
|
154 (map map_id0_of_bnf inners); |
|
155 |
|
156 fun map_comp0_tac _ = |
|
157 mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) |
|
158 (map map_comp0_of_bnf inners); |
|
159 |
|
160 fun mk_single_set_map0_tac i _ = |
|
161 mk_comp_set_map0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) |
|
162 (collect_set_map_of_bnf outer) |
|
163 (map ((fn thms => nth thms i) o set_map0_of_bnf) inners); |
|
164 |
|
165 val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1); |
|
166 |
|
167 fun bd_card_order_tac _ = |
|
168 mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); |
|
169 |
|
170 fun bd_cinfinite_tac _ = |
|
171 mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer); |
|
172 |
|
173 val set_alt_thms = |
|
174 if Config.get lthy quick_and_dirty then |
|
175 [] |
|
176 else |
|
177 map (fn goal => |
|
178 Goal.prove_sorry lthy [] [] goal |
|
179 (fn {context = ctxt, prems = _} => |
|
180 mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |
|
181 |> Thm.close_derivation) |
|
182 (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt); |
|
183 |
|
184 fun map_cong0_tac _ = |
|
185 mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners); |
|
186 |
|
187 val set_bd_tacs = |
|
188 if Config.get lthy quick_and_dirty then |
|
189 replicate ilive (K all_tac) |
|
190 else |
|
191 let |
|
192 val outer_set_bds = set_bd_of_bnf outer; |
|
193 val inner_set_bdss = map set_bd_of_bnf inners; |
|
194 val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; |
|
195 fun single_set_bd_thm i j = |
|
196 @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i, |
|
197 nth outer_set_bds j] |
|
198 val single_set_bd_thmss = |
|
199 map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); |
|
200 in |
|
201 map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} => |
|
202 mk_comp_set_bd_tac ctxt set_alt single_set_bds) |
|
203 set_alt_thms single_set_bd_thmss |
|
204 end; |
|
205 |
|
206 val in_alt_thm = |
|
207 let |
|
208 val inx = mk_in Asets sets CCA; |
|
209 val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; |
|
210 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
|
211 in |
|
212 Goal.prove_sorry lthy [] [] goal |
|
213 (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms) |
|
214 |> Thm.close_derivation |
|
215 end; |
|
216 |
|
217 fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) |
|
218 (map le_rel_OO_of_bnf inners); |
|
219 |
|
220 fun rel_OO_Grp_tac _ = |
|
221 let |
|
222 val outer_rel_Grp = rel_Grp_of_bnf outer RS sym; |
|
223 val outer_rel_cong = rel_cong_of_bnf outer; |
|
224 val thm = |
|
225 (trans OF [in_alt_thm RS @{thm OO_Grp_cong}, |
|
226 trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF |
|
227 [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]}, |
|
228 rel_conversep_of_bnf outer RS sym], outer_rel_Grp], |
|
229 trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF |
|
230 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym) |
|
231 (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*); |
|
232 in |
|
233 rtac thm 1 |
|
234 end; |
|
235 |
|
236 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac |
|
237 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; |
|
238 |
|
239 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; |
|
240 |
|
241 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) |
|
242 (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) |
|
243 Dss inwitss inners); |
|
244 |
|
245 val inner_witsss = map (map (nth inner_witss) o fst) outer_wits; |
|
246 |
|
247 val wits = (inner_witsss, (map (single o snd) outer_wits)) |
|
248 |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit))) |
|
249 |> flat |
|
250 |> map (`(fn t => Term.add_frees t [])) |
|
251 |> minimize_wits |
|
252 |> map (fn (frees, t) => fold absfree frees t); |
|
253 |
|
254 fun wit_tac {context = ctxt, prems = _} = |
|
255 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) |
|
256 (maps wit_thms_of_bnf inners); |
|
257 |
|
258 val (bnf', lthy') = |
|
259 bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty |
|
260 Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy; |
|
261 in |
|
262 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
|
263 end; |
|
264 |
|
265 (* Killing live variables *) |
|
266 |
|
267 fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
|
268 let |
|
269 val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); |
|
270 val live = live_of_bnf bnf; |
|
271 val dead = dead_of_bnf bnf; |
|
272 val nwits = nwits_of_bnf bnf; |
|
273 |
|
274 (* TODO: check 0 < n <= live *) |
|
275 |
|
276 val (Ds, lthy1) = apfst (map TFree) |
|
277 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
278 val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree) |
|
279 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
280 val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree) |
|
281 (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2); |
|
282 |
|
283 val ((Asets, lives), _(*names_lthy*)) = lthy |
|
284 |> mk_Frees "A" (map HOLogic.mk_setT (drop n As)) |
|
285 ||>> mk_Frees "x" (drop n As); |
|
286 val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives; |
|
287 |
|
288 val T = mk_T_of_bnf Ds As bnf; |
|
289 |
|
290 (*bnf.map id ... id*) |
|
291 val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); |
|
292 (*bnf.rel (op =) ... (op =)*) |
|
293 val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); |
|
294 |
|
295 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
296 val sets = drop n bnf_sets; |
|
297 |
|
298 (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*) |
|
299 val bnf_bd = mk_bd_of_bnf Ds As bnf; |
|
300 val bd = mk_cprod |
|
301 (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd; |
|
302 |
|
303 fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; |
|
304 fun map_comp0_tac {context = ctxt, prems = _} = |
|
305 unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
|
306 rtac refl 1; |
|
307 fun map_cong0_tac {context = ctxt, prems = _} = |
|
308 mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); |
|
309 val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf)); |
|
310 fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
|
311 fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
|
312 val set_bd_tacs = |
|
313 map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
|
314 (drop n (set_bd_of_bnf bnf)); |
|
315 |
|
316 val in_alt_thm = |
|
317 let |
|
318 val inx = mk_in Asets sets T; |
|
319 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
|
320 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
|
321 in |
|
322 Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation |
|
323 end; |
|
324 |
|
325 fun le_rel_OO_tac {context = ctxt, prems = _} = |
|
326 EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN |
|
327 unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1; |
|
328 |
|
329 fun rel_OO_Grp_tac _ = |
|
330 let |
|
331 val rel_Grp = rel_Grp_of_bnf bnf RS sym |
|
332 val thm = |
|
333 (trans OF [in_alt_thm RS @{thm OO_Grp_cong}, |
|
334 trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF |
|
335 [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]}, |
|
336 rel_conversep_of_bnf bnf RS sym], rel_Grp], |
|
337 trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF |
|
338 (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @ |
|
339 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym); |
|
340 in |
|
341 rtac thm 1 |
|
342 end; |
|
343 |
|
344 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac |
|
345 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; |
|
346 |
|
347 val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; |
|
348 |
|
349 val wits = map (fn t => fold absfree (Term.add_frees t []) t) |
|
350 (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits); |
|
351 |
|
352 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
353 |
|
354 val (bnf', lthy') = |
|
355 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty |
|
356 Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
|
357 in |
|
358 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
|
359 end; |
|
360 |
|
361 (* Adding dummy live variables *) |
|
362 |
|
363 fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
|
364 let |
|
365 val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); |
|
366 val live = live_of_bnf bnf; |
|
367 val dead = dead_of_bnf bnf; |
|
368 val nwits = nwits_of_bnf bnf; |
|
369 |
|
370 (* TODO: check 0 < n *) |
|
371 |
|
372 val (Ds, lthy1) = apfst (map TFree) |
|
373 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
374 val ((newAs, As), lthy2) = apfst (chop n o map TFree) |
|
375 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1); |
|
376 val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree) |
|
377 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2); |
|
378 |
|
379 val (Asets, _(*names_lthy*)) = lthy |
|
380 |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As)); |
|
381 |
|
382 val T = mk_T_of_bnf Ds As bnf; |
|
383 |
|
384 (*%f1 ... fn. bnf.map*) |
|
385 val mapx = |
|
386 fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); |
|
387 (*%Q1 ... Qn. bnf.rel*) |
|
388 val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf); |
|
389 |
|
390 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
391 val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; |
|
392 |
|
393 val bd = mk_bd_of_bnf Ds As bnf; |
|
394 |
|
395 fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; |
|
396 fun map_comp0_tac {context = ctxt, prems = _} = |
|
397 unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
|
398 rtac refl 1; |
|
399 fun map_cong0_tac {context = ctxt, prems = _} = |
|
400 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
|
401 val set_map0_tacs = |
|
402 if Config.get lthy quick_and_dirty then |
|
403 replicate (n + live) (K all_tac) |
|
404 else |
|
405 replicate n (K empty_natural_tac) @ |
|
406 map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf); |
|
407 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
|
408 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
409 val set_bd_tacs = |
|
410 if Config.get lthy quick_and_dirty then |
|
411 replicate (n + live) (K all_tac) |
|
412 else |
|
413 replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @ |
|
414 (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
|
415 |
|
416 val in_alt_thm = |
|
417 let |
|
418 val inx = mk_in Asets sets T; |
|
419 val in_alt = mk_in (drop n Asets) bnf_sets T; |
|
420 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
|
421 in |
|
422 Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation |
|
423 end; |
|
424 |
|
425 fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1; |
|
426 |
|
427 fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; |
|
428 |
|
429 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac |
|
430 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; |
|
431 |
|
432 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
433 |
|
434 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
435 |
|
436 val (bnf', lthy') = |
|
437 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
|
438 [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
|
439 in |
|
440 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
|
441 end; |
|
442 |
|
443 (* Changing the order of live variables *) |
|
444 |
|
445 fun permute_bnf qualify src dest bnf (unfold_set, lthy) = |
|
446 if src = dest then (bnf, (unfold_set, lthy)) else |
|
447 let |
|
448 val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf); |
|
449 val live = live_of_bnf bnf; |
|
450 val dead = dead_of_bnf bnf; |
|
451 val nwits = nwits_of_bnf bnf; |
|
452 fun permute xs = permute_like (op =) src dest xs; |
|
453 fun unpermute xs = permute_like (op =) dest src xs; |
|
454 |
|
455 val (Ds, lthy1) = apfst (map TFree) |
|
456 (Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
|
457 val (As, lthy2) = apfst (map TFree) |
|
458 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
459 val (Bs, _(*lthy3*)) = apfst (map TFree) |
|
460 (Variable.invent_types (replicate live HOLogic.typeS) lthy2); |
|
461 |
|
462 val (Asets, _(*names_lthy*)) = lthy |
|
463 |> mk_Frees "A" (map HOLogic.mk_setT (permute As)); |
|
464 |
|
465 val T = mk_T_of_bnf Ds As bnf; |
|
466 |
|
467 (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*) |
|
468 val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) |
|
469 (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); |
|
470 (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*) |
|
471 val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) |
|
472 (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); |
|
473 |
|
474 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
|
475 val sets = permute bnf_sets; |
|
476 |
|
477 val bd = mk_bd_of_bnf Ds As bnf; |
|
478 |
|
479 fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; |
|
480 fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1; |
|
481 fun map_cong0_tac {context = ctxt, prems = _} = |
|
482 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
|
483 val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf)); |
|
484 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
|
485 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
486 val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
|
487 |
|
488 val in_alt_thm = |
|
489 let |
|
490 val inx = mk_in Asets sets T; |
|
491 val in_alt = mk_in (unpermute Asets) bnf_sets T; |
|
492 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
|
493 in |
|
494 Goal.prove_sorry lthy [] [] goal (K (mk_permute_in_alt_tac src dest)) |
|
495 |> Thm.close_derivation |
|
496 end; |
|
497 |
|
498 fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1; |
|
499 |
|
500 fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; |
|
501 |
|
502 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac |
|
503 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; |
|
504 |
|
505 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
506 |
|
507 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
|
508 |
|
509 val (bnf', lthy') = |
|
510 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
|
511 [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
|
512 in |
|
513 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
|
514 end; |
|
515 |
|
516 (* Composition pipeline *) |
|
517 |
|
518 fun permute_and_kill qualify n src dest bnf = |
|
519 bnf |
|
520 |> permute_bnf qualify src dest |
|
521 #> uncurry (kill_bnf qualify n); |
|
522 |
|
523 fun lift_and_permute qualify n src dest bnf = |
|
524 bnf |
|
525 |> lift_bnf qualify n |
|
526 #> uncurry (permute_bnf qualify src dest); |
|
527 |
|
528 fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy = |
|
529 let |
|
530 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
|
531 val kill_poss = map (find_indices op = Ds) Ass; |
|
532 val live_poss = map2 (subtract op =) kill_poss before_kill_src; |
|
533 val before_kill_dest = map2 append kill_poss live_poss; |
|
534 val kill_ns = map length kill_poss; |
|
535 val (inners', (unfold_set', lthy')) = |
|
536 fold_map5 (fn i => permute_and_kill (qualify i)) |
|
537 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
538 kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy); |
|
539 |
|
540 val Ass' = map2 (map o nth) Ass live_poss; |
|
541 val As = sort Ass'; |
|
542 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); |
|
543 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; |
|
544 val new_poss = map2 (subtract op =) old_poss after_lift_dest; |
|
545 val after_lift_src = map2 append new_poss old_poss; |
|
546 val lift_ns = map (fn xs => length As - length xs) Ass'; |
|
547 in |
|
548 ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) |
|
549 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
550 lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy')) |
|
551 end; |
|
552 |
|
553 fun default_comp_sort Ass = |
|
554 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); |
|
555 |
|
556 fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) = |
|
557 let |
|
558 val b = name_of_bnf outer; |
|
559 |
|
560 val Ass = map (map Term.dest_TFree) tfreess; |
|
561 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; |
|
562 |
|
563 val ((kill_poss, As), (inners', (unfold_set', lthy'))) = |
|
564 normalize_bnfs qualify Ass Ds sort inners unfold_set lthy; |
|
565 |
|
566 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); |
|
567 val As = map TFree As; |
|
568 in |
|
569 apfst (rpair (Ds, As)) |
|
570 (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')) |
|
571 end; |
|
572 |
|
573 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
|
574 |
|
575 fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy = |
|
576 let |
|
577 val live = live_of_bnf bnf; |
|
578 val nwits = nwits_of_bnf bnf; |
|
579 |
|
580 val (As, lthy1) = apfst (map TFree) |
|
581 (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy)); |
|
582 val (Bs, _) = apfst (map TFree) |
|
583 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
|
584 |
|
585 val map_unfolds = #map_unfolds unfold_set; |
|
586 val set_unfoldss = #set_unfoldss unfold_set; |
|
587 val rel_unfolds = #rel_unfolds unfold_set; |
|
588 |
|
589 val expand_maps = |
|
590 fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); |
|
591 val expand_sets = |
|
592 fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss); |
|
593 val expand_rels = |
|
594 fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds); |
|
595 fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds; |
|
596 fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss; |
|
597 fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds; |
|
598 fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt; |
|
599 val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf); |
|
600 val bnf_sets = map (expand_maps o expand_sets) |
|
601 (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); |
|
602 val bnf_bd = mk_bd_of_bnf Ds As bnf; |
|
603 val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf); |
|
604 val T = mk_T_of_bnf Ds As bnf; |
|
605 |
|
606 (*bd should only depend on dead type variables!*) |
|
607 val bd_repT = fst (dest_relT (fastype_of bnf_bd)); |
|
608 val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b); |
|
609 val params = fold Term.add_tfreesT Ds []; |
|
610 val deads = map TFree params; |
|
611 |
|
612 val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = |
|
613 typedef (bdT_bind, params, NoSyn) |
|
614 (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; |
|
615 |
|
616 val bnf_bd' = mk_dir_image bnf_bd |
|
617 (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads))) |
|
618 |
|
619 val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info); |
|
620 val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info); |
|
621 |
|
622 val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; |
|
623 val bd_card_order = |
|
624 @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; |
|
625 val bd_cinfinite = |
|
626 (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; |
|
627 |
|
628 val set_bds = |
|
629 map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf); |
|
630 |
|
631 fun mk_tac thm {context = ctxt, prems = _} = |
|
632 (rtac (unfold_all ctxt thm) THEN' |
|
633 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; |
|
634 |
|
635 val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf)) |
|
636 (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_of_bnf bnf)) |
|
637 (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) |
|
638 (mk_tac (le_rel_OO_of_bnf bnf)) |
|
639 (mk_tac (rel_OO_Grp_of_bnf bnf)); |
|
640 |
|
641 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
|
642 |
|
643 fun wit_tac {context = ctxt, prems = _} = |
|
644 mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf)); |
|
645 |
|
646 val (bnf', lthy') = |
|
647 bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads) |
|
648 Binding.empty Binding.empty [] |
|
649 ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy; |
|
650 in |
|
651 ((bnf', deads), lthy') |
|
652 end; |
|
653 |
|
654 exception BAD_DEAD of typ * typ; |
|
655 |
|
656 fun bnf_of_typ _ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum) |
|
657 | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable" |
|
658 | bnf_of_typ const_policy qualify' sort Xs (T as Type (C, Ts)) (unfold_set, lthy) = |
|
659 let |
|
660 fun check_bad_dead ((_, (deads, _)), _) = |
|
661 let val Ds = fold Term.add_tfreesT deads [] in |
|
662 (case Library.inter (op =) Ds Xs of [] => () |
|
663 | X :: _ => raise BAD_DEAD (TFree X, T)) |
|
664 end; |
|
665 |
|
666 val tfrees = Term.add_tfreesT T []; |
|
667 val bnf_opt = if null tfrees then NONE else bnf_of lthy C; |
|
668 in |
|
669 (case bnf_opt of |
|
670 NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy)) |
|
671 | SOME bnf => |
|
672 if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then |
|
673 let |
|
674 val T' = T_of_bnf bnf; |
|
675 val deads = deads_of_bnf bnf; |
|
676 val lives = lives_of_bnf bnf; |
|
677 val tvars' = Term.add_tvarsT T' []; |
|
678 val deads_lives = |
|
679 pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) |
|
680 (deads, lives); |
|
681 in ((bnf, deads_lives), (unfold_set, lthy)) end |
|
682 else |
|
683 let |
|
684 val name = Long_Name.base_name C; |
|
685 fun qualify i = |
|
686 let val namei = name ^ nonzero_string_of_int i; |
|
687 in qualify' o Binding.qualify true namei end; |
|
688 val odead = dead_of_bnf bnf; |
|
689 val olive = live_of_bnf bnf; |
|
690 val oDs_pos = find_indices op = [TFree ("dead", [])] (snd (Term.dest_Type |
|
691 (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf))); |
|
692 val oDs = map (nth Ts) oDs_pos; |
|
693 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); |
|
694 val ((inners, (Dss, Ass)), (unfold_set', lthy')) = |
|
695 apfst (apsnd split_list o split_list) |
|
696 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs) |
|
697 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy)); |
|
698 in |
|
699 compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy') |
|
700 end) |
|
701 |> tap check_bad_dead |
|
702 end; |
|
703 |
|
704 end; |