1 (* Title: HOL/BNF/Tools/bnf_def.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Definition of bounded natural functors. |
|
7 *) |
|
8 |
|
9 signature BNF_DEF = |
|
10 sig |
|
11 type bnf |
|
12 type nonemptiness_witness = {I: int list, wit: term, prop: thm list} |
|
13 |
|
14 val morph_bnf: morphism -> bnf -> bnf |
|
15 val eq_bnf: bnf * bnf -> bool |
|
16 val bnf_of: Proof.context -> string -> bnf option |
|
17 val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory) |
|
18 |
|
19 val name_of_bnf: bnf -> binding |
|
20 val T_of_bnf: bnf -> typ |
|
21 val live_of_bnf: bnf -> int |
|
22 val lives_of_bnf: bnf -> typ list |
|
23 val dead_of_bnf: bnf -> int |
|
24 val deads_of_bnf: bnf -> typ list |
|
25 val nwits_of_bnf: bnf -> int |
|
26 |
|
27 val mapN: string |
|
28 val relN: string |
|
29 val setN: string |
|
30 val mk_setN: int -> string |
|
31 val mk_witN: int -> string |
|
32 |
|
33 val map_of_bnf: bnf -> term |
|
34 val sets_of_bnf: bnf -> term list |
|
35 val rel_of_bnf: bnf -> term |
|
36 |
|
37 val mk_T_of_bnf: typ list -> typ list -> bnf -> typ |
|
38 val mk_bd_of_bnf: typ list -> typ list -> bnf -> term |
|
39 val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term |
|
40 val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term |
|
41 val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list |
|
42 val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list |
|
43 |
|
44 val bd_Card_order_of_bnf: bnf -> thm |
|
45 val bd_Cinfinite_of_bnf: bnf -> thm |
|
46 val bd_Cnotzero_of_bnf: bnf -> thm |
|
47 val bd_card_order_of_bnf: bnf -> thm |
|
48 val bd_cinfinite_of_bnf: bnf -> thm |
|
49 val collect_set_map_of_bnf: bnf -> thm |
|
50 val in_bd_of_bnf: bnf -> thm |
|
51 val in_cong_of_bnf: bnf -> thm |
|
52 val in_mono_of_bnf: bnf -> thm |
|
53 val in_rel_of_bnf: bnf -> thm |
|
54 val map_comp0_of_bnf: bnf -> thm |
|
55 val map_comp_of_bnf: bnf -> thm |
|
56 val map_cong0_of_bnf: bnf -> thm |
|
57 val map_cong_of_bnf: bnf -> thm |
|
58 val map_def_of_bnf: bnf -> thm |
|
59 val map_id0_of_bnf: bnf -> thm |
|
60 val map_id_of_bnf: bnf -> thm |
|
61 val map_transfer_of_bnf: bnf -> thm |
|
62 val le_rel_OO_of_bnf: bnf -> thm |
|
63 val rel_def_of_bnf: bnf -> thm |
|
64 val rel_Grp_of_bnf: bnf -> thm |
|
65 val rel_OO_of_bnf: bnf -> thm |
|
66 val rel_OO_Grp_of_bnf: bnf -> thm |
|
67 val rel_cong_of_bnf: bnf -> thm |
|
68 val rel_conversep_of_bnf: bnf -> thm |
|
69 val rel_mono_of_bnf: bnf -> thm |
|
70 val rel_mono_strong_of_bnf: bnf -> thm |
|
71 val rel_eq_of_bnf: bnf -> thm |
|
72 val rel_flip_of_bnf: bnf -> thm |
|
73 val set_bd_of_bnf: bnf -> thm list |
|
74 val set_defs_of_bnf: bnf -> thm list |
|
75 val set_map0_of_bnf: bnf -> thm list |
|
76 val set_map_of_bnf: bnf -> thm list |
|
77 val wit_thms_of_bnf: bnf -> thm list |
|
78 val wit_thmss_of_bnf: bnf -> thm list list |
|
79 |
|
80 val mk_map: int -> typ list -> typ list -> term -> term |
|
81 val mk_rel: int -> typ list -> typ list -> term -> term |
|
82 val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term |
|
83 val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term |
|
84 val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list |
|
85 val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list -> |
|
86 'a list |
|
87 |
|
88 val mk_witness: int list * term -> thm list -> nonemptiness_witness |
|
89 val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list |
|
90 val wits_of_bnf: bnf -> nonemptiness_witness list |
|
91 |
|
92 val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list |
|
93 |
|
94 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline |
|
95 datatype fact_policy = Dont_Note | Note_Some | Note_All |
|
96 |
|
97 val bnf_note_all: bool Config.T |
|
98 val bnf_timing: bool Config.T |
|
99 val user_policy: fact_policy -> Proof.context -> fact_policy |
|
100 val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context -> |
|
101 Proof.context |
|
102 |
|
103 val print_bnfs: Proof.context -> unit |
|
104 val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> |
|
105 (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option -> |
|
106 binding -> binding -> binding list -> |
|
107 (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context -> |
|
108 string * term list * |
|
109 ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) * |
|
110 ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) * |
|
111 local_theory * thm list |
|
112 |
|
113 val define_bnf_consts: const_policy -> fact_policy -> typ list option -> |
|
114 binding -> binding -> binding list -> |
|
115 (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> |
|
116 ((typ list * typ list * typ list * typ) * |
|
117 (term * term list * term * (int list * term) list * term) * |
|
118 (thm * thm list * thm * thm list * thm) * |
|
119 ((typ list -> typ list -> typ list -> term) * |
|
120 (typ list -> typ list -> term -> term) * |
|
121 (typ list -> typ list -> typ -> typ) * |
|
122 (typ list -> typ list -> typ list -> term) * |
|
123 (typ list -> typ list -> typ list -> term))) * local_theory |
|
124 |
|
125 val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> |
|
126 ({prems: thm list, context: Proof.context} -> tactic) list -> |
|
127 ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> |
|
128 binding -> binding list -> |
|
129 (((((binding * typ) * term) * term list) * term) * term list) * term option -> |
|
130 local_theory -> bnf * local_theory |
|
131 end; |
|
132 |
|
133 structure BNF_Def : BNF_DEF = |
|
134 struct |
|
135 |
|
136 open BNF_Util |
|
137 open BNF_Tactics |
|
138 open BNF_Def_Tactics |
|
139 |
|
140 val fundefcong_attrs = @{attributes [fundef_cong]}; |
|
141 |
|
142 type axioms = { |
|
143 map_id0: thm, |
|
144 map_comp0: thm, |
|
145 map_cong0: thm, |
|
146 set_map0: thm list, |
|
147 bd_card_order: thm, |
|
148 bd_cinfinite: thm, |
|
149 set_bd: thm list, |
|
150 le_rel_OO: thm, |
|
151 rel_OO_Grp: thm |
|
152 }; |
|
153 |
|
154 fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) = |
|
155 {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o, |
|
156 bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel}; |
|
157 |
|
158 fun dest_cons [] = raise List.Empty |
|
159 | dest_cons (x :: xs) = (x, xs); |
|
160 |
|
161 fun mk_axioms n thms = thms |
|
162 |> map the_single |
|
163 |> dest_cons |
|
164 ||>> dest_cons |
|
165 ||>> dest_cons |
|
166 ||>> chop n |
|
167 ||>> dest_cons |
|
168 ||>> dest_cons |
|
169 ||>> chop n |
|
170 ||>> dest_cons |
|
171 ||> the_single |
|
172 |> mk_axioms'; |
|
173 |
|
174 fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel = |
|
175 [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel]; |
|
176 |
|
177 fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, |
|
178 le_rel_OO, rel_OO_Grp} = |
|
179 zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO |
|
180 rel_OO_Grp; |
|
181 |
|
182 fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, |
|
183 le_rel_OO, rel_OO_Grp} = |
|
184 {map_id0 = f map_id0, |
|
185 map_comp0 = f map_comp0, |
|
186 map_cong0 = f map_cong0, |
|
187 set_map0 = map f set_map0, |
|
188 bd_card_order = f bd_card_order, |
|
189 bd_cinfinite = f bd_cinfinite, |
|
190 set_bd = map f set_bd, |
|
191 le_rel_OO = f le_rel_OO, |
|
192 rel_OO_Grp = f rel_OO_Grp}; |
|
193 |
|
194 val morph_axioms = map_axioms o Morphism.thm; |
|
195 |
|
196 type defs = { |
|
197 map_def: thm, |
|
198 set_defs: thm list, |
|
199 rel_def: thm |
|
200 } |
|
201 |
|
202 fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel}; |
|
203 |
|
204 fun map_defs f {map_def, set_defs, rel_def} = |
|
205 {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def}; |
|
206 |
|
207 val morph_defs = map_defs o Morphism.thm; |
|
208 |
|
209 type facts = { |
|
210 bd_Card_order: thm, |
|
211 bd_Cinfinite: thm, |
|
212 bd_Cnotzero: thm, |
|
213 collect_set_map: thm lazy, |
|
214 in_bd: thm lazy, |
|
215 in_cong: thm lazy, |
|
216 in_mono: thm lazy, |
|
217 in_rel: thm lazy, |
|
218 map_comp: thm lazy, |
|
219 map_cong: thm lazy, |
|
220 map_id: thm lazy, |
|
221 map_transfer: thm lazy, |
|
222 rel_eq: thm lazy, |
|
223 rel_flip: thm lazy, |
|
224 set_map: thm lazy list, |
|
225 rel_cong: thm lazy, |
|
226 rel_mono: thm lazy, |
|
227 rel_mono_strong: thm lazy, |
|
228 rel_Grp: thm lazy, |
|
229 rel_conversep: thm lazy, |
|
230 rel_OO: thm lazy |
|
231 }; |
|
232 |
|
233 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel |
|
234 map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono |
|
235 rel_mono_strong rel_Grp rel_conversep rel_OO = { |
|
236 bd_Card_order = bd_Card_order, |
|
237 bd_Cinfinite = bd_Cinfinite, |
|
238 bd_Cnotzero = bd_Cnotzero, |
|
239 collect_set_map = collect_set_map, |
|
240 in_bd = in_bd, |
|
241 in_cong = in_cong, |
|
242 in_mono = in_mono, |
|
243 in_rel = in_rel, |
|
244 map_comp = map_comp, |
|
245 map_cong = map_cong, |
|
246 map_id = map_id, |
|
247 map_transfer = map_transfer, |
|
248 rel_eq = rel_eq, |
|
249 rel_flip = rel_flip, |
|
250 set_map = set_map, |
|
251 rel_cong = rel_cong, |
|
252 rel_mono = rel_mono, |
|
253 rel_mono_strong = rel_mono_strong, |
|
254 rel_Grp = rel_Grp, |
|
255 rel_conversep = rel_conversep, |
|
256 rel_OO = rel_OO}; |
|
257 |
|
258 fun map_facts f { |
|
259 bd_Card_order, |
|
260 bd_Cinfinite, |
|
261 bd_Cnotzero, |
|
262 collect_set_map, |
|
263 in_bd, |
|
264 in_cong, |
|
265 in_mono, |
|
266 in_rel, |
|
267 map_comp, |
|
268 map_cong, |
|
269 map_id, |
|
270 map_transfer, |
|
271 rel_eq, |
|
272 rel_flip, |
|
273 set_map, |
|
274 rel_cong, |
|
275 rel_mono, |
|
276 rel_mono_strong, |
|
277 rel_Grp, |
|
278 rel_conversep, |
|
279 rel_OO} = |
|
280 {bd_Card_order = f bd_Card_order, |
|
281 bd_Cinfinite = f bd_Cinfinite, |
|
282 bd_Cnotzero = f bd_Cnotzero, |
|
283 collect_set_map = Lazy.map f collect_set_map, |
|
284 in_bd = Lazy.map f in_bd, |
|
285 in_cong = Lazy.map f in_cong, |
|
286 in_mono = Lazy.map f in_mono, |
|
287 in_rel = Lazy.map f in_rel, |
|
288 map_comp = Lazy.map f map_comp, |
|
289 map_cong = Lazy.map f map_cong, |
|
290 map_id = Lazy.map f map_id, |
|
291 map_transfer = Lazy.map f map_transfer, |
|
292 rel_eq = Lazy.map f rel_eq, |
|
293 rel_flip = Lazy.map f rel_flip, |
|
294 set_map = map (Lazy.map f) set_map, |
|
295 rel_cong = Lazy.map f rel_cong, |
|
296 rel_mono = Lazy.map f rel_mono, |
|
297 rel_mono_strong = Lazy.map f rel_mono_strong, |
|
298 rel_Grp = Lazy.map f rel_Grp, |
|
299 rel_conversep = Lazy.map f rel_conversep, |
|
300 rel_OO = Lazy.map f rel_OO}; |
|
301 |
|
302 val morph_facts = map_facts o Morphism.thm; |
|
303 |
|
304 type nonemptiness_witness = { |
|
305 I: int list, |
|
306 wit: term, |
|
307 prop: thm list |
|
308 }; |
|
309 |
|
310 fun mk_witness (I, wit) prop = {I = I, wit = wit, prop = prop}; |
|
311 fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop}; |
|
312 fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi); |
|
313 |
|
314 datatype bnf = BNF of { |
|
315 name: binding, |
|
316 T: typ, |
|
317 live: int, |
|
318 lives: typ list, (*source type variables of map*) |
|
319 lives': typ list, (*target type variables of map*) |
|
320 dead: int, |
|
321 deads: typ list, |
|
322 map: term, |
|
323 sets: term list, |
|
324 bd: term, |
|
325 axioms: axioms, |
|
326 defs: defs, |
|
327 facts: facts, |
|
328 nwits: int, |
|
329 wits: nonemptiness_witness list, |
|
330 rel: term |
|
331 }; |
|
332 |
|
333 (* getters *) |
|
334 |
|
335 fun rep_bnf (BNF bnf) = bnf; |
|
336 val name_of_bnf = #name o rep_bnf; |
|
337 val T_of_bnf = #T o rep_bnf; |
|
338 fun mk_T_of_bnf Ds Ts bnf = |
|
339 let val bnf_rep = rep_bnf bnf |
|
340 in Term.typ_subst_atomic ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#T bnf_rep) end; |
|
341 val live_of_bnf = #live o rep_bnf; |
|
342 val lives_of_bnf = #lives o rep_bnf; |
|
343 val dead_of_bnf = #dead o rep_bnf; |
|
344 val deads_of_bnf = #deads o rep_bnf; |
|
345 val axioms_of_bnf = #axioms o rep_bnf; |
|
346 val facts_of_bnf = #facts o rep_bnf; |
|
347 val nwits_of_bnf = #nwits o rep_bnf; |
|
348 val wits_of_bnf = #wits o rep_bnf; |
|
349 |
|
350 fun flatten_type_args_of_bnf bnf dead_x xs = |
|
351 let |
|
352 val Type (_, Ts) = T_of_bnf bnf; |
|
353 val lives = lives_of_bnf bnf; |
|
354 val deads = deads_of_bnf bnf; |
|
355 in |
|
356 permute_like (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs) |
|
357 end; |
|
358 |
|
359 (*terms*) |
|
360 val map_of_bnf = #map o rep_bnf; |
|
361 val sets_of_bnf = #sets o rep_bnf; |
|
362 fun mk_map_of_bnf Ds Ts Us bnf = |
|
363 let val bnf_rep = rep_bnf bnf; |
|
364 in |
|
365 Term.subst_atomic_types |
|
366 ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#map bnf_rep) |
|
367 end; |
|
368 fun mk_sets_of_bnf Dss Tss bnf = |
|
369 let val bnf_rep = rep_bnf bnf; |
|
370 in |
|
371 map2 (fn (Ds, Ts) => Term.subst_atomic_types |
|
372 ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts))) (Dss ~~ Tss) (#sets bnf_rep) |
|
373 end; |
|
374 val bd_of_bnf = #bd o rep_bnf; |
|
375 fun mk_bd_of_bnf Ds Ts bnf = |
|
376 let val bnf_rep = rep_bnf bnf; |
|
377 in Term.subst_atomic_types ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#bd bnf_rep) end; |
|
378 fun mk_wits_of_bnf Dss Tss bnf = |
|
379 let |
|
380 val bnf_rep = rep_bnf bnf; |
|
381 val wits = map (fn x => (#I x, #wit x)) (#wits bnf_rep); |
|
382 in |
|
383 map2 (fn (Ds, Ts) => apsnd (Term.subst_atomic_types |
|
384 ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)))) (Dss ~~ Tss) wits |
|
385 end; |
|
386 val rel_of_bnf = #rel o rep_bnf; |
|
387 fun mk_rel_of_bnf Ds Ts Us bnf = |
|
388 let val bnf_rep = rep_bnf bnf; |
|
389 in |
|
390 Term.subst_atomic_types |
|
391 ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep) |
|
392 end; |
|
393 |
|
394 (*thms*) |
|
395 val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf; |
|
396 val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf; |
|
397 val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf; |
|
398 val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf; |
|
399 val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf; |
|
400 val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf; |
|
401 val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf; |
|
402 val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf; |
|
403 val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf; |
|
404 val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf; |
|
405 val map_def_of_bnf = #map_def o #defs o rep_bnf; |
|
406 val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf; |
|
407 val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf; |
|
408 val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf; |
|
409 val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf; |
|
410 val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf; |
|
411 val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf; |
|
412 val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf; |
|
413 val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf; |
|
414 val rel_def_of_bnf = #rel_def o #defs o rep_bnf; |
|
415 val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf; |
|
416 val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf; |
|
417 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; |
|
418 val set_defs_of_bnf = #set_defs o #defs o rep_bnf; |
|
419 val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf; |
|
420 val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf; |
|
421 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; |
|
422 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf; |
|
423 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf; |
|
424 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf; |
|
425 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf; |
|
426 val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf; |
|
427 val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf; |
|
428 val wit_thms_of_bnf = maps #prop o wits_of_bnf; |
|
429 val wit_thmss_of_bnf = map #prop o wits_of_bnf; |
|
430 |
|
431 fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel = |
|
432 BNF {name = name, T = T, |
|
433 live = live, lives = lives, lives' = lives', dead = dead, deads = deads, |
|
434 map = map, sets = sets, bd = bd, |
|
435 axioms = axioms, defs = defs, facts = facts, |
|
436 nwits = length wits, wits = wits, rel = rel}; |
|
437 |
|
438 fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives', |
|
439 dead = dead, deads = deads, map = map, sets = sets, bd = bd, |
|
440 axioms = axioms, defs = defs, facts = facts, |
|
441 nwits = nwits, wits = wits, rel = rel}) = |
|
442 BNF {name = Morphism.binding phi name, T = Morphism.typ phi T, |
|
443 live = live, lives = List.map (Morphism.typ phi) lives, |
|
444 lives' = List.map (Morphism.typ phi) lives', |
|
445 dead = dead, deads = List.map (Morphism.typ phi) deads, |
|
446 map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets, |
|
447 bd = Morphism.term phi bd, |
|
448 axioms = morph_axioms phi axioms, |
|
449 defs = morph_defs phi defs, |
|
450 facts = morph_facts phi facts, |
|
451 nwits = nwits, |
|
452 wits = List.map (morph_witness phi) wits, |
|
453 rel = Morphism.term phi rel}; |
|
454 |
|
455 fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...}, |
|
456 BNF {T = T2, live = live2, dead = dead2, ...}) = |
|
457 Type.could_unify (T1, T2) andalso live1 = live2 andalso dead1 = dead2; |
|
458 |
|
459 structure Data = Generic_Data |
|
460 ( |
|
461 type T = bnf Symtab.table; |
|
462 val empty = Symtab.empty; |
|
463 val extend = I; |
|
464 val merge = Symtab.merge eq_bnf; |
|
465 ); |
|
466 |
|
467 fun bnf_of ctxt = |
|
468 Symtab.lookup (Data.get (Context.Proof ctxt)) |
|
469 #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt))); |
|
470 |
|
471 |
|
472 (* Utilities *) |
|
473 |
|
474 fun normalize_set insts instA set = |
|
475 let |
|
476 val (T, T') = dest_funT (fastype_of set); |
|
477 val A = fst (Term.dest_TVar (HOLogic.dest_setT T')); |
|
478 val params = Term.add_tvar_namesT T []; |
|
479 in Term.subst_TVars ((A :: params) ~~ (instA :: insts)) set end; |
|
480 |
|
481 fun normalize_rel ctxt instTs instA instB rel = |
|
482 let |
|
483 val thy = Proof_Context.theory_of ctxt; |
|
484 val tyenv = |
|
485 Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB)) |
|
486 Vartab.empty; |
|
487 in Envir.subst_term (tyenv, Vartab.empty) rel end |
|
488 handle Type.TYPE_MATCH => error "Bad relator"; |
|
489 |
|
490 fun normalize_wit insts CA As wit = |
|
491 let |
|
492 fun strip_param (Ts, T as Type (@{type_name fun}, [T1, T2])) = |
|
493 if Type.raw_instance (CA, T) then (Ts, T) else strip_param (T1 :: Ts, T2) |
|
494 | strip_param x = x; |
|
495 val (Ts, T) = strip_param ([], fastype_of wit); |
|
496 val subst = Term.add_tvar_namesT T [] ~~ insts; |
|
497 fun find y = find_index (fn x => x = y) As; |
|
498 in |
|
499 (map (find o Term.typ_subst_TVars subst) (rev Ts), Term.subst_TVars subst wit) |
|
500 end; |
|
501 |
|
502 fun minimize_wits wits = |
|
503 let |
|
504 fun minimize done [] = done |
|
505 | minimize done ((I, wit) :: todo) = |
|
506 if exists (fn (J, _) => subset (op =) (J, I)) (done @ todo) |
|
507 then minimize done todo |
|
508 else minimize ((I, wit) :: done) todo; |
|
509 in minimize [] wits end; |
|
510 |
|
511 fun mk_map live Ts Us t = |
|
512 let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in |
|
513 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
|
514 end; |
|
515 |
|
516 fun mk_rel live Ts Us t = |
|
517 let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in |
|
518 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
|
519 end; |
|
520 |
|
521 fun build_map_or_rel mk const of_bnf dest ctxt build_simple = |
|
522 let |
|
523 fun build (TU as (T, U)) = |
|
524 if T = U then |
|
525 const T |
|
526 else |
|
527 (case TU of |
|
528 (Type (s, Ts), Type (s', Us)) => |
|
529 if s = s' then |
|
530 let |
|
531 val bnf = the (bnf_of ctxt s); |
|
532 val live = live_of_bnf bnf; |
|
533 val mapx = mk live Ts Us (of_bnf bnf); |
|
534 val TUs' = map dest (fst (strip_typeN live (fastype_of mapx))); |
|
535 in Term.list_comb (mapx, map build TUs') end |
|
536 else |
|
537 build_simple TU |
|
538 | _ => build_simple TU); |
|
539 in build end; |
|
540 |
|
541 val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT; |
|
542 val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T; |
|
543 |
|
544 fun map_flattened_map_args ctxt s map_args fs = |
|
545 let |
|
546 val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs; |
|
547 val flat_fs' = map_args flat_fs; |
|
548 in |
|
549 permute_like (op aconv) flat_fs fs flat_fs' |
|
550 end; |
|
551 |
|
552 |
|
553 (* Names *) |
|
554 |
|
555 val mapN = "map"; |
|
556 val setN = "set"; |
|
557 fun mk_setN i = setN ^ nonzero_string_of_int i; |
|
558 val bdN = "bd"; |
|
559 val witN = "wit"; |
|
560 fun mk_witN i = witN ^ nonzero_string_of_int i; |
|
561 val relN = "rel"; |
|
562 |
|
563 val bd_card_orderN = "bd_card_order"; |
|
564 val bd_cinfiniteN = "bd_cinfinite"; |
|
565 val bd_Card_orderN = "bd_Card_order"; |
|
566 val bd_CinfiniteN = "bd_Cinfinite"; |
|
567 val bd_CnotzeroN = "bd_Cnotzero"; |
|
568 val collect_set_mapN = "collect_set_map"; |
|
569 val in_bdN = "in_bd"; |
|
570 val in_monoN = "in_mono"; |
|
571 val in_relN = "in_rel"; |
|
572 val map_id0N = "map_id0"; |
|
573 val map_idN = "map_id"; |
|
574 val map_comp0N = "map_comp0"; |
|
575 val map_compN = "map_comp"; |
|
576 val map_cong0N = "map_cong0"; |
|
577 val map_congN = "map_cong"; |
|
578 val map_transferN = "map_transfer"; |
|
579 val rel_eqN = "rel_eq"; |
|
580 val rel_flipN = "rel_flip"; |
|
581 val set_map0N = "set_map0"; |
|
582 val set_mapN = "set_map"; |
|
583 val set_bdN = "set_bd"; |
|
584 val rel_GrpN = "rel_Grp"; |
|
585 val rel_conversepN = "rel_conversep"; |
|
586 val rel_monoN = "rel_mono" |
|
587 val rel_mono_strongN = "rel_mono_strong" |
|
588 val rel_comppN = "rel_compp"; |
|
589 val rel_compp_GrpN = "rel_compp_Grp"; |
|
590 |
|
591 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline; |
|
592 |
|
593 datatype fact_policy = Dont_Note | Note_Some | Note_All; |
|
594 |
|
595 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false); |
|
596 val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false); |
|
597 |
|
598 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; |
|
599 |
|
600 val smart_max_inline_size = 25; (*FUDGE*) |
|
601 |
|
602 fun note_bnf_thms fact_policy qualify' bnf_b bnf = |
|
603 let |
|
604 val axioms = axioms_of_bnf bnf; |
|
605 val facts = facts_of_bnf bnf; |
|
606 val wits = wits_of_bnf bnf; |
|
607 val qualify = |
|
608 let val (_, qs, _) = Binding.dest bnf_b; |
|
609 in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify' end; |
|
610 in |
|
611 (if fact_policy = Note_All then |
|
612 let |
|
613 val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); |
|
614 val notes = |
|
615 [(bd_card_orderN, [#bd_card_order axioms]), |
|
616 (bd_cinfiniteN, [#bd_cinfinite axioms]), |
|
617 (bd_Card_orderN, [#bd_Card_order facts]), |
|
618 (bd_CinfiniteN, [#bd_Cinfinite facts]), |
|
619 (bd_CnotzeroN, [#bd_Cnotzero facts]), |
|
620 (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), |
|
621 (in_bdN, [Lazy.force (#in_bd facts)]), |
|
622 (in_monoN, [Lazy.force (#in_mono facts)]), |
|
623 (in_relN, [Lazy.force (#in_rel facts)]), |
|
624 (map_comp0N, [#map_comp0 axioms]), |
|
625 (map_id0N, [#map_id0 axioms]), |
|
626 (map_transferN, [Lazy.force (#map_transfer facts)]), |
|
627 (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), |
|
628 (set_map0N, #set_map0 axioms), |
|
629 (set_bdN, #set_bd axioms)] @ |
|
630 (witNs ~~ wit_thmss_of_bnf bnf) |
|
631 |> map (fn (thmN, thms) => |
|
632 ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []), |
|
633 [(thms, [])])); |
|
634 in |
|
635 Local_Theory.notes notes #> snd |
|
636 end |
|
637 else |
|
638 I) |
|
639 #> (if fact_policy <> Dont_Note then |
|
640 let |
|
641 val notes = |
|
642 [(map_compN, [Lazy.force (#map_comp facts)], []), |
|
643 (map_cong0N, [#map_cong0 axioms], []), |
|
644 (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs), |
|
645 (map_idN, [Lazy.force (#map_id facts)], []), |
|
646 (rel_comppN, [Lazy.force (#rel_OO facts)], []), |
|
647 (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []), |
|
648 (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), |
|
649 (rel_eqN, [Lazy.force (#rel_eq facts)], []), |
|
650 (rel_flipN, [Lazy.force (#rel_flip facts)], []), |
|
651 (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), |
|
652 (rel_monoN, [Lazy.force (#rel_mono facts)], []), |
|
653 (set_mapN, map Lazy.force (#set_map facts), [])] |
|
654 |> filter_out (null o #2) |
|
655 |> map (fn (thmN, thms, attrs) => |
|
656 ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), |
|
657 attrs), [(thms, [])])); |
|
658 in |
|
659 Local_Theory.notes notes #> snd |
|
660 end |
|
661 else |
|
662 I) |
|
663 end; |
|
664 |
|
665 |
|
666 (* Define new BNFs *) |
|
667 |
|
668 fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs |
|
669 ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy = |
|
670 let |
|
671 val live = length set_rhss; |
|
672 |
|
673 val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b); |
|
674 |
|
675 fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b; |
|
676 |
|
677 fun maybe_define user_specified (b, rhs) lthy = |
|
678 let |
|
679 val inline = |
|
680 (user_specified orelse fact_policy = Dont_Note) andalso |
|
681 (case const_policy of |
|
682 Dont_Inline => false |
|
683 | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs |
|
684 | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size |
|
685 | Do_Inline => true) |
|
686 in |
|
687 if inline then |
|
688 ((rhs, Drule.reflexive_thm), lthy) |
|
689 else |
|
690 let val b = b () in |
|
691 apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) |
|
692 lthy) |
|
693 end |
|
694 end; |
|
695 |
|
696 fun maybe_restore lthy_old lthy = |
|
697 lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore; |
|
698 |
|
699 val map_bind_def = |
|
700 (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b), |
|
701 map_rhs); |
|
702 val set_binds_defs = |
|
703 let |
|
704 fun set_name i get_b = |
|
705 (case try (nth set_bs) (i - 1) of |
|
706 SOME b => if Binding.is_empty b then get_b else K b |
|
707 | NONE => get_b) #> def_qualify; |
|
708 val bs = if live = 1 then [set_name 1 (fn () => mk_prefix_binding setN)] |
|
709 else map (fn i => set_name i (fn () => mk_prefix_binding (mk_setN i))) (1 upto live); |
|
710 in bs ~~ set_rhss end; |
|
711 val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs); |
|
712 |
|
713 val ((((bnf_map_term, raw_map_def), |
|
714 (bnf_set_terms, raw_set_defs)), |
|
715 (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) = |
|
716 no_defs_lthy |
|
717 |> maybe_define true map_bind_def |
|
718 ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs |
|
719 ||>> maybe_define true bd_bind_def |
|
720 ||> `(maybe_restore no_defs_lthy); |
|
721 |
|
722 val phi = Proof_Context.export_morphism lthy_old lthy; |
|
723 |
|
724 |
|
725 val bnf_map_def = Morphism.thm phi raw_map_def; |
|
726 val bnf_set_defs = map (Morphism.thm phi) raw_set_defs; |
|
727 val bnf_bd_def = Morphism.thm phi raw_bd_def; |
|
728 |
|
729 val bnf_map = Morphism.term phi bnf_map_term; |
|
730 |
|
731 (*TODO: handle errors*) |
|
732 (*simple shape analysis of a map function*) |
|
733 val ((alphas, betas), (Calpha, _)) = |
|
734 fastype_of bnf_map |
|
735 |> strip_typeN live |
|
736 |>> map_split dest_funT |
|
737 ||> dest_funT |
|
738 handle TYPE _ => error "Bad map function"; |
|
739 |
|
740 val Calpha_params = map TVar (Term.add_tvarsT Calpha []); |
|
741 |
|
742 val bnf_T = Morphism.typ phi T_rhs; |
|
743 val bad_args = Term.add_tfreesT bnf_T []; |
|
744 val _ = if null bad_args then () else error ("Locally fixed type arguments " ^ |
|
745 commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args)); |
|
746 |
|
747 val bnf_sets = |
|
748 map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms); |
|
749 val bnf_bd = |
|
750 Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ Calpha_params) |
|
751 (Morphism.term phi bnf_bd_term); |
|
752 |
|
753 (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*) |
|
754 val deads = (case Ds_opt of |
|
755 NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map [])) |
|
756 | SOME Ds => map (Morphism.typ phi) Ds); |
|
757 |
|
758 (*TODO: further checks of type of bnf_map*) |
|
759 (*TODO: check types of bnf_sets*) |
|
760 (*TODO: check type of bnf_bd*) |
|
761 (*TODO: check type of bnf_rel*) |
|
762 |
|
763 fun mk_bnf_map Ds As' Bs' = |
|
764 Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map; |
|
765 fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As')); |
|
766 fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As')); |
|
767 |
|
768 val (((As, Bs), Ds), names_lthy) = lthy |
|
769 |> mk_TFrees live |
|
770 ||>> mk_TFrees live |
|
771 ||>> mk_TFrees (length deads); |
|
772 val RTs = map2 (curry HOLogic.mk_prodT) As Bs; |
|
773 val pred2RTs = map2 mk_pred2T As Bs; |
|
774 val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst |
|
775 val CA = mk_bnf_T Ds As Calpha; |
|
776 val CR = mk_bnf_T Ds RTs Calpha; |
|
777 val setRs = |
|
778 map3 (fn R => fn T => fn U => |
|
779 HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs; |
|
780 |
|
781 (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO |
|
782 Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*) |
|
783 val OO_Grp = |
|
784 let |
|
785 val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs); |
|
786 val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs); |
|
787 val bnf_in = mk_in setRs (map (mk_bnf_t Ds RTs) bnf_sets) CR; |
|
788 in |
|
789 mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2) |
|
790 |> fold_rev Term.absfree Rs' |
|
791 end; |
|
792 |
|
793 val rel_rhs = the_default OO_Grp rel_rhs_opt; |
|
794 |
|
795 val rel_bind_def = |
|
796 (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b), |
|
797 rel_rhs); |
|
798 |
|
799 val wit_rhss = |
|
800 if null wit_rhss then |
|
801 [fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As, |
|
802 map2 (fn T => fn i => Term.absdummy T (Bound i)) As (live downto 1)) $ |
|
803 Const (@{const_name undefined}, CA))] |
|
804 else wit_rhss; |
|
805 val nwits = length wit_rhss; |
|
806 val wit_binds_defs = |
|
807 let |
|
808 val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)] |
|
809 else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits); |
|
810 in bs ~~ wit_rhss end; |
|
811 |
|
812 val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = |
|
813 lthy |
|
814 |> maybe_define (is_some rel_rhs_opt) rel_bind_def |
|
815 ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs |
|
816 ||> `(maybe_restore lthy); |
|
817 |
|
818 val phi = Proof_Context.export_morphism lthy_old lthy; |
|
819 val bnf_rel_def = Morphism.thm phi raw_rel_def; |
|
820 val bnf_rel = Morphism.term phi bnf_rel_term; |
|
821 fun mk_bnf_rel Ds As' Bs' = |
|
822 normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha) |
|
823 bnf_rel; |
|
824 |
|
825 val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; |
|
826 val bnf_wits = |
|
827 map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms; |
|
828 |
|
829 fun mk_OO_Grp Ds' As' Bs' = |
|
830 Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp; |
|
831 in |
|
832 (((alphas, betas, deads, Calpha), |
|
833 (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel), |
|
834 (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def), |
|
835 (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy) |
|
836 end; |
|
837 |
|
838 fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs |
|
839 ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) |
|
840 no_defs_lthy = |
|
841 let |
|
842 val fact_policy = mk_fact_policy no_defs_lthy; |
|
843 val bnf_b = qualify raw_bnf_b; |
|
844 val live = length raw_sets; |
|
845 |
|
846 val T_rhs = prep_typ no_defs_lthy raw_bnf_T; |
|
847 val map_rhs = prep_term no_defs_lthy raw_map; |
|
848 val set_rhss = map (prep_term no_defs_lthy) raw_sets; |
|
849 val bd_rhs = prep_term no_defs_lthy raw_bd; |
|
850 val wit_rhss = map (prep_term no_defs_lthy) raw_wits; |
|
851 val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt; |
|
852 |
|
853 fun err T = |
|
854 error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ |
|
855 " as unnamed BNF"); |
|
856 |
|
857 val (bnf_b, key) = |
|
858 if Binding.eq_name (bnf_b, Binding.empty) then |
|
859 (case T_rhs of |
|
860 Type (C, Ts) => if forall (can dest_TFree) Ts |
|
861 then (Binding.qualified_name C, C) else err T_rhs |
|
862 | T => err T) |
|
863 else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b); |
|
864 |
|
865 val (((alphas, betas, deads, Calpha), |
|
866 (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel), |
|
867 (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def), |
|
868 (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) = |
|
869 define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs |
|
870 ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy; |
|
871 |
|
872 val dead = length deads; |
|
873 |
|
874 val ((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), (Ts, T)) = lthy |
|
875 |> mk_TFrees live |
|
876 ||>> mk_TFrees live |
|
877 ||>> mk_TFrees live |
|
878 ||>> mk_TFrees dead |
|
879 ||>> mk_TFrees live |
|
880 ||>> mk_TFrees live |
|
881 ||> fst o mk_TFrees 1 |
|
882 ||> the_single |
|
883 ||> `(replicate live); |
|
884 |
|
885 val mk_bnf_map = mk_bnf_map_Ds Ds; |
|
886 val mk_bnf_t = mk_bnf_t_Ds Ds; |
|
887 val mk_bnf_T = mk_bnf_T_Ds Ds; |
|
888 |
|
889 val pred2RTs = map2 mk_pred2T As' Bs'; |
|
890 val pred2RTsAsCs = map2 mk_pred2T As' Cs; |
|
891 val pred2RTsBsCs = map2 mk_pred2T Bs' Cs; |
|
892 val pred2RT's = map2 mk_pred2T Bs' As'; |
|
893 val self_pred2RTs = map2 mk_pred2T As' As'; |
|
894 val transfer_domRTs = map2 mk_pred2T As' B1Ts; |
|
895 val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts; |
|
896 |
|
897 val CA' = mk_bnf_T As' Calpha; |
|
898 val CB' = mk_bnf_T Bs' Calpha; |
|
899 val CC' = mk_bnf_T Cs Calpha; |
|
900 val CB1 = mk_bnf_T B1Ts Calpha; |
|
901 val CB2 = mk_bnf_T B2Ts Calpha; |
|
902 |
|
903 val bnf_map_AsAs = mk_bnf_map As' As'; |
|
904 val bnf_map_AsBs = mk_bnf_map As' Bs'; |
|
905 val bnf_map_AsCs = mk_bnf_map As' Cs; |
|
906 val bnf_map_BsCs = mk_bnf_map Bs' Cs; |
|
907 val bnf_sets_As = map (mk_bnf_t As') bnf_sets; |
|
908 val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets; |
|
909 val bnf_bd_As = mk_bnf_t As' bnf_bd; |
|
910 fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel; |
|
911 |
|
912 val pre_names_lthy = lthy; |
|
913 val (((((((((((((((fs, gs), hs), x), y), zs), ys), As), |
|
914 As_copy), bs), Rs), Rs_copy), Ss), |
|
915 transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy |
|
916 |> mk_Frees "f" (map2 (curry op -->) As' Bs') |
|
917 ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs) |
|
918 ||>> mk_Frees "h" (map2 (curry op -->) As' Ts) |
|
919 ||>> yield_singleton (mk_Frees "x") CA' |
|
920 ||>> yield_singleton (mk_Frees "y") CB' |
|
921 ||>> mk_Frees "z" As' |
|
922 ||>> mk_Frees "y" Bs' |
|
923 ||>> mk_Frees "A" (map HOLogic.mk_setT As') |
|
924 ||>> mk_Frees "A" (map HOLogic.mk_setT As') |
|
925 ||>> mk_Frees "b" As' |
|
926 ||>> mk_Frees "R" pred2RTs |
|
927 ||>> mk_Frees "R" pred2RTs |
|
928 ||>> mk_Frees "S" pred2RTsBsCs |
|
929 ||>> mk_Frees "R" transfer_domRTs |
|
930 ||>> mk_Frees "S" transfer_ranRTs; |
|
931 |
|
932 val fs_copy = map2 (retype_free o fastype_of) fs gs; |
|
933 val x_copy = retype_free CA' y; |
|
934 |
|
935 val rel = mk_bnf_rel pred2RTs CA' CB'; |
|
936 val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; |
|
937 val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; |
|
938 |
|
939 val map_id0_goal = |
|
940 let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in |
|
941 mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA') |
|
942 end; |
|
943 |
|
944 val map_comp0_goal = |
|
945 let |
|
946 val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); |
|
947 val comp_bnf_map_app = HOLogic.mk_comp |
|
948 (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs)); |
|
949 in |
|
950 fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app)) |
|
951 end; |
|
952 |
|
953 fun mk_map_cong_prem x z set f f_copy = |
|
954 Logic.all z (Logic.mk_implies |
|
955 (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)), |
|
956 mk_Trueprop_eq (f $ z, f_copy $ z))); |
|
957 |
|
958 val map_cong0_goal = |
|
959 let |
|
960 val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy; |
|
961 val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x, |
|
962 Term.list_comb (bnf_map_AsBs, fs_copy) $ x); |
|
963 in |
|
964 fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq)) |
|
965 end; |
|
966 |
|
967 val set_map0s_goal = |
|
968 let |
|
969 fun mk_goal setA setB f = |
|
970 let |
|
971 val set_comp_map = |
|
972 HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs)); |
|
973 val image_comp_set = HOLogic.mk_comp (mk_image f, setA); |
|
974 in |
|
975 fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set)) |
|
976 end; |
|
977 in |
|
978 map3 mk_goal bnf_sets_As bnf_sets_Bs fs |
|
979 end; |
|
980 |
|
981 val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As); |
|
982 |
|
983 val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As); |
|
984 |
|
985 val set_bds_goal = |
|
986 let |
|
987 fun mk_goal set = |
|
988 Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As)); |
|
989 in |
|
990 map mk_goal bnf_sets_As |
|
991 end; |
|
992 |
|
993 val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC'; |
|
994 val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC'; |
|
995 val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss); |
|
996 val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss)); |
|
997 val le_rel_OO_goal = |
|
998 fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs)); |
|
999 |
|
1000 val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), |
|
1001 Term.list_comb (mk_OO_Grp Ds As' Bs', Rs))); |
|
1002 |
|
1003 val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal |
|
1004 card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal; |
|
1005 |
|
1006 fun mk_wit_goals (I, wit) = |
|
1007 let |
|
1008 val xs = map (nth bs) I; |
|
1009 fun wit_goal i = |
|
1010 let |
|
1011 val z = nth zs i; |
|
1012 val set_wit = nth bnf_sets_As i $ Term.list_comb (wit, xs); |
|
1013 val concl = HOLogic.mk_Trueprop |
|
1014 (if member (op =) I i then HOLogic.mk_eq (z, nth bs i) |
|
1015 else @{term False}); |
|
1016 in |
|
1017 fold_rev Logic.all (z :: xs) |
|
1018 (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl)) |
|
1019 end; |
|
1020 in |
|
1021 map wit_goal (0 upto live - 1) |
|
1022 end; |
|
1023 |
|
1024 val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs; |
|
1025 |
|
1026 val wit_goalss = |
|
1027 (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As); |
|
1028 |
|
1029 fun after_qed mk_wit_thms thms lthy = |
|
1030 let |
|
1031 val (axioms, nontriv_wit_thms) = apfst (mk_axioms live) (chop (length goals) thms); |
|
1032 |
|
1033 val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]}; |
|
1034 val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order]; |
|
1035 val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; |
|
1036 |
|
1037 fun mk_collect_set_map () = |
|
1038 let |
|
1039 val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T; |
|
1040 val collect_map = HOLogic.mk_comp |
|
1041 (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT, |
|
1042 Term.list_comb (mk_bnf_map As' Ts, hs)); |
|
1043 val image_collect = mk_collect |
|
1044 (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As) |
|
1045 defT; |
|
1046 (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*) |
|
1047 val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect)); |
|
1048 in |
|
1049 Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms))) |
|
1050 |> Thm.close_derivation |
|
1051 end; |
|
1052 |
|
1053 val collect_set_map = Lazy.lazy mk_collect_set_map; |
|
1054 |
|
1055 fun mk_in_mono () = |
|
1056 let |
|
1057 val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy; |
|
1058 val in_mono_goal = |
|
1059 fold_rev Logic.all (As @ As_copy) |
|
1060 (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop |
|
1061 (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA')))); |
|
1062 in |
|
1063 Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live)) |
|
1064 |> Thm.close_derivation |
|
1065 end; |
|
1066 |
|
1067 val in_mono = Lazy.lazy mk_in_mono; |
|
1068 |
|
1069 fun mk_in_cong () = |
|
1070 let |
|
1071 val prems_cong = map2 (curry mk_Trueprop_eq) As As_copy; |
|
1072 val in_cong_goal = |
|
1073 fold_rev Logic.all (As @ As_copy) |
|
1074 (Logic.list_implies (prems_cong, |
|
1075 mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))); |
|
1076 in |
|
1077 Goal.prove_sorry lthy [] [] in_cong_goal |
|
1078 (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1)) |
|
1079 |> Thm.close_derivation |
|
1080 end; |
|
1081 |
|
1082 val in_cong = Lazy.lazy mk_in_cong; |
|
1083 |
|
1084 val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms)); |
|
1085 val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms)); |
|
1086 |
|
1087 fun mk_map_cong () = |
|
1088 let |
|
1089 val prem0 = mk_Trueprop_eq (x, x_copy); |
|
1090 val prems = map4 (mk_map_cong_prem x_copy) zs bnf_sets_As fs fs_copy; |
|
1091 val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x, |
|
1092 Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy); |
|
1093 val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy) |
|
1094 (Logic.list_implies (prem0 :: prems, eq)); |
|
1095 in |
|
1096 Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms)) |
|
1097 |> Thm.close_derivation |
|
1098 end; |
|
1099 |
|
1100 val map_cong = Lazy.lazy mk_map_cong; |
|
1101 |
|
1102 val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms); |
|
1103 |
|
1104 val wit_thms = |
|
1105 if null nontriv_wit_thms then mk_wit_thms (map Lazy.force set_map) else nontriv_wit_thms; |
|
1106 |
|
1107 fun mk_in_bd () = |
|
1108 let |
|
1109 val bdT = fst (dest_relT (fastype_of bnf_bd_As)); |
|
1110 val bdTs = replicate live bdT; |
|
1111 val bd_bnfT = mk_bnf_T bdTs Calpha; |
|
1112 val surj_imp_ordLeq_inst = (if live = 0 then TrueI else |
|
1113 let |
|
1114 val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As'; |
|
1115 val funTs = map (fn T => bdT --> T) ranTs; |
|
1116 val ran_bnfT = mk_bnf_T ranTs Calpha; |
|
1117 val (revTs, Ts) = `rev (bd_bnfT :: funTs); |
|
1118 val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts]; |
|
1119 val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs) |
|
1120 (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs, |
|
1121 map Bound (live - 1 downto 0)) $ Bound live)); |
|
1122 val cts = [NONE, SOME (certify lthy tinst)]; |
|
1123 in |
|
1124 Drule.instantiate' cTs cts @{thm surj_imp_ordLeq} |
|
1125 end); |
|
1126 val bd = mk_cexp |
|
1127 (if live = 0 then ctwo |
|
1128 else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) |
|
1129 (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV bd_bnfT))); |
|
1130 val in_bd_goal = |
|
1131 fold_rev Logic.all As |
|
1132 (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd)); |
|
1133 in |
|
1134 Goal.prove_sorry lthy [] [] in_bd_goal |
|
1135 (mk_in_bd_tac live surj_imp_ordLeq_inst |
|
1136 (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms) |
|
1137 (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms) |
|
1138 bd_Card_order bd_Cinfinite bd_Cnotzero) |
|
1139 |> Thm.close_derivation |
|
1140 end; |
|
1141 |
|
1142 val in_bd = Lazy.lazy mk_in_bd; |
|
1143 |
|
1144 val rel_OO_Grp = #rel_OO_Grp axioms; |
|
1145 val rel_OO_Grps = no_refl [rel_OO_Grp]; |
|
1146 |
|
1147 fun mk_rel_Grp () = |
|
1148 let |
|
1149 val lhs = Term.list_comb (rel, map2 mk_Grp As fs); |
|
1150 val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs)); |
|
1151 val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs)); |
|
1152 in |
|
1153 Goal.prove_sorry lthy [] [] goal |
|
1154 (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id) |
|
1155 (Lazy.force map_comp) (map Lazy.force set_map)) |
|
1156 |> Thm.close_derivation |
|
1157 end; |
|
1158 |
|
1159 val rel_Grp = Lazy.lazy mk_rel_Grp; |
|
1160 |
|
1161 fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy |
|
1162 fun mk_rel_concl f = HOLogic.mk_Trueprop |
|
1163 (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy))); |
|
1164 |
|
1165 fun mk_rel_mono () = |
|
1166 let |
|
1167 val mono_prems = mk_rel_prems mk_leq; |
|
1168 val mono_concl = mk_rel_concl (uncurry mk_leq); |
|
1169 in |
|
1170 Goal.prove_sorry lthy [] [] |
|
1171 (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl))) |
|
1172 (K (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))) |
|
1173 |> Thm.close_derivation |
|
1174 end; |
|
1175 |
|
1176 fun mk_rel_cong () = |
|
1177 let |
|
1178 val cong_prems = mk_rel_prems (curry HOLogic.mk_eq); |
|
1179 val cong_concl = mk_rel_concl HOLogic.mk_eq; |
|
1180 in |
|
1181 Goal.prove_sorry lthy [] [] |
|
1182 (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl))) |
|
1183 (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1) |
|
1184 |> Thm.close_derivation |
|
1185 end; |
|
1186 |
|
1187 val rel_mono = Lazy.lazy mk_rel_mono; |
|
1188 val rel_cong = Lazy.lazy mk_rel_cong; |
|
1189 |
|
1190 fun mk_rel_eq () = |
|
1191 Goal.prove_sorry lthy [] [] |
|
1192 (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'), |
|
1193 HOLogic.eq_const CA')) |
|
1194 (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms))) |
|
1195 |> Thm.close_derivation; |
|
1196 |
|
1197 val rel_eq = Lazy.lazy mk_rel_eq; |
|
1198 |
|
1199 fun mk_rel_conversep () = |
|
1200 let |
|
1201 val relBsAs = mk_bnf_rel pred2RT's CB' CA'; |
|
1202 val lhs = Term.list_comb (relBsAs, map mk_conversep Rs); |
|
1203 val rhs = mk_conversep (Term.list_comb (rel, Rs)); |
|
1204 val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs)); |
|
1205 val le_thm = Goal.prove_sorry lthy [] [] le_goal |
|
1206 (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) |
|
1207 (Lazy.force map_comp) (map Lazy.force set_map)) |
|
1208 |> Thm.close_derivation |
|
1209 val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs)); |
|
1210 in |
|
1211 Goal.prove_sorry lthy [] [] goal |
|
1212 (K (mk_rel_conversep_tac le_thm (Lazy.force rel_mono))) |
|
1213 |> Thm.close_derivation |
|
1214 end; |
|
1215 |
|
1216 val rel_conversep = Lazy.lazy mk_rel_conversep; |
|
1217 |
|
1218 fun mk_rel_OO () = |
|
1219 Goal.prove_sorry lthy [] [] |
|
1220 (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs))) |
|
1221 (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) |
|
1222 (Lazy.force map_comp) (map Lazy.force set_map)) |
|
1223 |> Thm.close_derivation |
|
1224 |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]); |
|
1225 |
|
1226 val rel_OO = Lazy.lazy mk_rel_OO; |
|
1227 |
|
1228 fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}; |
|
1229 |
|
1230 val in_rel = Lazy.lazy mk_in_rel; |
|
1231 |
|
1232 fun mk_rel_flip () = |
|
1233 let |
|
1234 val rel_conversep_thm = Lazy.force rel_conversep; |
|
1235 val cts = map (SOME o certify lthy) Rs; |
|
1236 val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm; |
|
1237 in |
|
1238 unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD}) |
|
1239 |> singleton (Proof_Context.export names_lthy pre_names_lthy) |
|
1240 end; |
|
1241 |
|
1242 val rel_flip = Lazy.lazy mk_rel_flip; |
|
1243 |
|
1244 fun mk_rel_mono_strong () = |
|
1245 let |
|
1246 fun mk_prem setA setB R S a b = |
|
1247 HOLogic.mk_Trueprop |
|
1248 (mk_Ball (setA $ x) (Term.absfree (dest_Free a) |
|
1249 (mk_Ball (setB $ y) (Term.absfree (dest_Free b) |
|
1250 (HOLogic.mk_imp (R $ a $ b, S $ a $ b)))))); |
|
1251 val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: |
|
1252 map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys; |
|
1253 val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y); |
|
1254 in |
|
1255 Goal.prove_sorry lthy [] [] |
|
1256 (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl))) |
|
1257 (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map)) |
|
1258 |> Thm.close_derivation |
|
1259 end; |
|
1260 |
|
1261 val rel_mono_strong = Lazy.lazy mk_rel_mono_strong; |
|
1262 |
|
1263 fun mk_map_transfer () = |
|
1264 let |
|
1265 val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs; |
|
1266 val rel = mk_fun_rel |
|
1267 (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs)) |
|
1268 (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs)); |
|
1269 val concl = HOLogic.mk_Trueprop |
|
1270 (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts); |
|
1271 in |
|
1272 Goal.prove_sorry lthy [] [] |
|
1273 (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl) |
|
1274 (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel) |
|
1275 (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp)) |
|
1276 |> Thm.close_derivation |
|
1277 end; |
|
1278 |
|
1279 val map_transfer = Lazy.lazy mk_map_transfer; |
|
1280 |
|
1281 val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def; |
|
1282 |
|
1283 val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong |
|
1284 in_mono in_rel map_comp map_cong map_id map_transfer rel_eq rel_flip set_map |
|
1285 rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; |
|
1286 |
|
1287 val wits = map2 mk_witness bnf_wits wit_thms; |
|
1288 |
|
1289 val bnf_rel = |
|
1290 Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; |
|
1291 |
|
1292 val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms |
|
1293 defs facts wits bnf_rel; |
|
1294 in |
|
1295 (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf) |
|
1296 end; |
|
1297 |
|
1298 val one_step_defs = |
|
1299 no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]); |
|
1300 in |
|
1301 (key, goals, wit_goalss, after_qed, lthy, one_step_defs) |
|
1302 end; |
|
1303 |
|
1304 fun register_bnf key (bnf, lthy) = |
|
1305 (bnf, Local_Theory.declaration {syntax = false, pervasive = true} |
|
1306 (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy); |
|
1307 |
|
1308 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs = |
|
1309 (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => |
|
1310 let |
|
1311 fun mk_wits_tac set_maps = |
|
1312 K (TRYALL Goal.conjunction_tac) THEN' |
|
1313 (case triv_tac_opt of |
|
1314 SOME tac => tac set_maps |
|
1315 | NONE => fn {context = ctxt, prems} => |
|
1316 unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems}); |
|
1317 val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
|
1318 fun mk_wit_thms set_maps = |
|
1319 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) |
|
1320 |> Conjunction.elim_balanced (length wit_goals) |
|
1321 |> map2 (Conjunction.elim_balanced o length) wit_goalss |
|
1322 |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); |
|
1323 in |
|
1324 map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] []) |
|
1325 goals (map (fn tac => fn {context = ctxt, prems} => |
|
1326 unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs) |
|
1327 |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) |
|
1328 end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs; |
|
1329 |
|
1330 val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => |
|
1331 let |
|
1332 val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
|
1333 fun mk_triv_wit_thms tac set_maps = |
|
1334 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) |
|
1335 (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps) |
|
1336 |> Conjunction.elim_balanced (length wit_goals) |
|
1337 |> map2 (Conjunction.elim_balanced o length) wit_goalss |
|
1338 |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); |
|
1339 val (mk_wit_thms, nontriv_wit_goals) = |
|
1340 (case triv_tac_opt of |
|
1341 NONE => (fn _ => [], map (map (rpair [])) wit_goalss) |
|
1342 | SOME tac => (mk_triv_wit_thms tac, [])); |
|
1343 in |
|
1344 Proof.unfolding ([[(defs, [])]]) |
|
1345 (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms) |
|
1346 (map (single o rpair []) goals @ nontriv_wit_goals) lthy) |
|
1347 end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE |
|
1348 Binding.empty Binding.empty []; |
|
1349 |
|
1350 fun print_bnfs ctxt = |
|
1351 let |
|
1352 fun pretty_set sets i = Pretty.block |
|
1353 [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1, |
|
1354 Pretty.quote (Syntax.pretty_term ctxt (nth sets i))]; |
|
1355 |
|
1356 fun pretty_bnf (key, BNF {T = T, map = map, sets = sets, bd = bd, |
|
1357 live = live, lives = lives, dead = dead, deads = deads, ...}) = |
|
1358 Pretty.big_list |
|
1359 (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1, |
|
1360 Pretty.quote (Syntax.pretty_typ ctxt T)])) |
|
1361 ([Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int live), |
|
1362 Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)], |
|
1363 Pretty.block [Pretty.str "dead:", Pretty.brk 1, Pretty.str (string_of_int dead), |
|
1364 Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) deads)], |
|
1365 Pretty.block [Pretty.str (mapN ^ ":"), Pretty.brk 1, |
|
1366 Pretty.quote (Syntax.pretty_term ctxt map)]] @ |
|
1367 List.map (pretty_set sets) (0 upto length sets - 1) @ |
|
1368 [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1, |
|
1369 Pretty.quote (Syntax.pretty_term ctxt bd)]]); |
|
1370 in |
|
1371 Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt)))) |
|
1372 |> Pretty.writeln |
|
1373 end; |
|
1374 |
|
1375 val _ = |
|
1376 Outer_Syntax.improper_command @{command_spec "print_bnfs"} |
|
1377 "print all bounded natural functors" |
|
1378 (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of))); |
|
1379 |
|
1380 val _ = |
|
1381 Outer_Syntax.local_theory_to_proof @{command_spec "bnf"} |
|
1382 "register a type as a bounded natural functor" |
|
1383 (parse_opt_binding_colon -- Parse.typ --| |
|
1384 (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term -- |
|
1385 (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |-- |
|
1386 Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --| |
|
1387 (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term -- |
|
1388 (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |-- |
|
1389 Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) -- |
|
1390 Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) |
|
1391 >> bnf_cmd); |
|
1392 |
|
1393 end; |
|