54 val map_def_of_bnf: BNF -> thm |
54 val map_def_of_bnf: BNF -> thm |
55 val map_id'_of_bnf: BNF -> thm |
55 val map_id'_of_bnf: BNF -> thm |
56 val map_id_of_bnf: BNF -> thm |
56 val map_id_of_bnf: BNF -> thm |
57 val map_wppull_of_bnf: BNF -> thm |
57 val map_wppull_of_bnf: BNF -> thm |
58 val map_wpull_of_bnf: BNF -> thm |
58 val map_wpull_of_bnf: BNF -> thm |
|
59 val rel_as_srel_of_bnf: BNF -> thm |
59 val rel_def_of_bnf: BNF -> thm |
60 val rel_def_of_bnf: BNF -> thm |
|
61 val rel_flip_of_bnf: BNF -> thm |
60 val set_bd_of_bnf: BNF -> thm list |
62 val set_bd_of_bnf: BNF -> thm list |
61 val set_defs_of_bnf: BNF -> thm list |
63 val set_defs_of_bnf: BNF -> thm list |
62 val set_natural'_of_bnf: BNF -> thm list |
64 val set_natural'_of_bnf: BNF -> thm list |
63 val set_natural_of_bnf: BNF -> thm list |
65 val set_natural_of_bnf: BNF -> thm list |
64 val sets_of_bnf: BNF -> term list |
66 val sets_of_bnf: BNF -> term list |
180 in_mono: thm lazy, |
182 in_mono: thm lazy, |
181 in_srel: thm lazy, |
183 in_srel: thm lazy, |
182 map_comp': thm lazy, |
184 map_comp': thm lazy, |
183 map_id': thm lazy, |
185 map_id': thm lazy, |
184 map_wppull: thm lazy, |
186 map_wppull: thm lazy, |
|
187 rel_as_srel: thm lazy, |
|
188 rel_flip: thm lazy, |
185 set_natural': thm lazy list, |
189 set_natural': thm lazy list, |
186 srel_cong: thm lazy, |
190 srel_cong: thm lazy, |
187 srel_mono: thm lazy, |
191 srel_mono: thm lazy, |
188 srel_Id: thm lazy, |
192 srel_Id: thm lazy, |
189 srel_Gr: thm lazy, |
193 srel_Gr: thm lazy, |
190 srel_converse: thm lazy, |
194 srel_converse: thm lazy, |
191 srel_O: thm lazy |
195 srel_O: thm lazy |
192 }; |
196 }; |
193 |
197 |
194 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel |
198 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel |
195 map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse |
199 map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong srel_mono srel_Id |
196 srel_O = { |
200 srel_Gr srel_converse srel_O = { |
197 bd_Card_order = bd_Card_order, |
201 bd_Card_order = bd_Card_order, |
198 bd_Cinfinite = bd_Cinfinite, |
202 bd_Cinfinite = bd_Cinfinite, |
199 bd_Cnotzero = bd_Cnotzero, |
203 bd_Cnotzero = bd_Cnotzero, |
200 collect_set_natural = collect_set_natural, |
204 collect_set_natural = collect_set_natural, |
201 in_cong = in_cong, |
205 in_cong = in_cong, |
202 in_mono = in_mono, |
206 in_mono = in_mono, |
203 in_srel = in_srel, |
207 in_srel = in_srel, |
204 map_comp' = map_comp', |
208 map_comp' = map_comp', |
205 map_id' = map_id', |
209 map_id' = map_id', |
206 map_wppull = map_wppull, |
210 map_wppull = map_wppull, |
|
211 rel_as_srel = rel_as_srel, |
|
212 rel_flip = rel_flip, |
207 set_natural' = set_natural', |
213 set_natural' = set_natural', |
208 srel_cong = srel_cong, |
214 srel_cong = srel_cong, |
209 srel_mono = srel_mono, |
215 srel_mono = srel_mono, |
210 srel_Id = srel_Id, |
216 srel_Id = srel_Id, |
211 srel_Gr = srel_Gr, |
217 srel_Gr = srel_Gr, |
238 in_mono = Lazy.map f in_mono, |
246 in_mono = Lazy.map f in_mono, |
239 in_srel = Lazy.map f in_srel, |
247 in_srel = Lazy.map f in_srel, |
240 map_comp' = Lazy.map f map_comp', |
248 map_comp' = Lazy.map f map_comp', |
241 map_id' = Lazy.map f map_id', |
249 map_id' = Lazy.map f map_id', |
242 map_wppull = Lazy.map f map_wppull, |
250 map_wppull = Lazy.map f map_wppull, |
|
251 rel_as_srel = Lazy.map f rel_as_srel, |
|
252 rel_flip = Lazy.map f rel_flip, |
243 set_natural' = map (Lazy.map f) set_natural', |
253 set_natural' = map (Lazy.map f) set_natural', |
244 srel_cong = Lazy.map f srel_cong, |
254 srel_cong = Lazy.map f srel_cong, |
245 srel_mono = Lazy.map f srel_mono, |
255 srel_mono = Lazy.map f srel_mono, |
246 srel_Id = Lazy.map f srel_Id, |
256 srel_Id = Lazy.map f srel_Id, |
247 srel_Gr = Lazy.map f srel_Gr, |
257 srel_Gr = Lazy.map f srel_Gr, |
356 val map_comp_of_bnf = #map_comp o #axioms o rep_bnf; |
366 val map_comp_of_bnf = #map_comp o #axioms o rep_bnf; |
357 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf; |
367 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf; |
358 val map_cong_of_bnf = #map_cong o #axioms o rep_bnf; |
368 val map_cong_of_bnf = #map_cong o #axioms o rep_bnf; |
359 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; |
369 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; |
360 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf; |
370 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf; |
|
371 val rel_as_srel_of_bnf = Lazy.force o #rel_as_srel o #facts o rep_bnf; |
361 val rel_def_of_bnf = #rel_def o #defs o rep_bnf; |
372 val rel_def_of_bnf = #rel_def o #defs o rep_bnf; |
|
373 val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf; |
362 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; |
374 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; |
363 val set_defs_of_bnf = #set_defs o #defs o rep_bnf; |
375 val set_defs_of_bnf = #set_defs o #defs o rep_bnf; |
364 val set_natural_of_bnf = #set_natural o #axioms o rep_bnf; |
376 val set_natural_of_bnf = #set_natural o #axioms o rep_bnf; |
365 val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf; |
377 val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf; |
366 val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf; |
378 val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf; |
488 val map_id'N = "map_id'"; |
500 val map_id'N = "map_id'"; |
489 val map_compN = "map_comp"; |
501 val map_compN = "map_comp"; |
490 val map_comp'N = "map_comp'"; |
502 val map_comp'N = "map_comp'"; |
491 val map_congN = "map_cong"; |
503 val map_congN = "map_cong"; |
492 val map_wpullN = "map_wpull"; |
504 val map_wpullN = "map_wpull"; |
|
505 val rel_as_srelN = "rel_as_srel"; |
|
506 val rel_flipN = "rel_flip"; |
|
507 val set_naturalN = "set_natural"; |
|
508 val set_natural'N = "set_natural'"; |
|
509 val set_bdN = "set_bd"; |
493 val srel_IdN = "srel_Id"; |
510 val srel_IdN = "srel_Id"; |
494 val srel_GrN = "srel_Gr"; |
511 val srel_GrN = "srel_Gr"; |
495 val srel_converseN = "srel_converse"; |
512 val srel_converseN = "srel_converse"; |
496 val srel_monoN = "srel_mono" |
513 val srel_monoN = "srel_mono" |
497 val srel_ON = "srel_comp"; |
514 val srel_ON = "srel_comp"; |
498 val srel_O_GrN = "srel_comp_Gr"; |
515 val srel_O_GrN = "srel_comp_Gr"; |
499 val set_naturalN = "set_natural"; |
|
500 val set_natural'N = "set_natural'"; |
|
501 val set_bdN = "set_bd"; |
|
502 |
516 |
503 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline; |
517 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline; |
504 |
518 |
505 datatype fact_policy = |
519 datatype fact_policy = |
506 Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms; |
520 Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms; |
693 ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts) |
707 ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts) |
694 ||>> mk_Frees "b" As' |
708 ||>> mk_Frees "b" As' |
695 ||>> mk_Frees' "S" setRTs |
709 ||>> mk_Frees' "S" setRTs |
696 ||>> mk_Frees "S" setRTs |
710 ||>> mk_Frees "S" setRTs |
697 ||>> mk_Frees "T" setRTsBsCs |
711 ||>> mk_Frees "T" setRTsBsCs |
698 ||>> mk_Frees' "Q" QTs; |
712 ||>> mk_Frees' "R" QTs; |
699 |
713 |
700 (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*) |
714 (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*) |
701 val O_Gr = |
715 val O_Gr = |
702 let |
716 let |
703 val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); |
717 val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); |
712 val (T, U) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of t)); |
726 val (T, U) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of t)); |
713 val x = Free (x_name, T); |
727 val x = Free (x_name, T); |
714 val y = Free (y_name, U); |
728 val y = Free (y_name, U); |
715 in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end; |
729 in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end; |
716 |
730 |
|
731 val sQs = |
|
732 map3 (fn Q => fn T => fn U => |
|
733 HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs'; |
|
734 |
717 val rel_rhs = (case raw_rel_opt of |
735 val rel_rhs = (case raw_rel_opt of |
718 NONE => |
736 NONE => |
719 fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y') |
737 fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y') |
720 (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, map3 (fn Q => fn T => fn U => |
738 (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs))) |
721 HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs'))) |
|
722 | SOME raw_rel => prep_term no_defs_lthy raw_rel); |
739 | SOME raw_rel => prep_term no_defs_lthy raw_rel); |
723 |
740 |
724 val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); |
741 val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); |
725 |
742 |
726 val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = |
743 val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = |
1088 |> Thm.close_derivation |
1105 |> Thm.close_derivation |
1089 end; |
1106 end; |
1090 |
1107 |
1091 val in_srel = mk_lazy mk_in_srel; |
1108 val in_srel = mk_lazy mk_in_srel; |
1092 |
1109 |
|
1110 val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair}; |
|
1111 val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases}; |
|
1112 |
|
1113 fun mk_rel_as_srel () = |
|
1114 unfold_thms lthy mem_Collect_etc |
|
1115 (funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq) |
|
1116 RS eqset_imp_iff_pair RS sym) |
|
1117 |> Drule.zero_var_indexes; |
|
1118 |
|
1119 val rel_as_srel = mk_lazy mk_rel_as_srel; |
|
1120 |
|
1121 fun mk_rel_flip () = |
|
1122 let |
|
1123 val srel_converse_thm = Lazy.force srel_converse; |
|
1124 val Rs' = Term.add_vars (prop_of srel_converse_thm) []; |
|
1125 val cts = map (pairself (certify lthy)) (map Var Rs' ~~ sQs); |
|
1126 val srel_converse_thm' = Drule.cterm_instantiate cts srel_converse_thm; |
|
1127 in |
|
1128 unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc) |
|
1129 (srel_converse_thm' RS eqset_imp_iff_pair) |
|
1130 |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1 |
|
1131 end; |
|
1132 |
|
1133 val rel_flip = mk_lazy mk_rel_flip; |
|
1134 |
1093 val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def; |
1135 val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def; |
1094 |
1136 |
1095 val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong |
1137 val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong |
1096 in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id |
1138 in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong |
1097 srel_Gr srel_converse srel_O; |
1139 srel_mono srel_Id srel_Gr srel_converse srel_O; |
1098 |
1140 |
1099 val wits = map2 mk_witness bnf_wits wit_thms; |
1141 val wits = map2 mk_witness bnf_wits wit_thms; |
1100 |
1142 |
1101 val bnf_rel = |
1143 val bnf_rel = |
1102 Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; |
1144 Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; |
1139 let |
1181 let |
1140 val notes = |
1182 val notes = |
1141 [(map_comp'N, [Lazy.force (#map_comp' facts)]), |
1183 [(map_comp'N, [Lazy.force (#map_comp' facts)]), |
1142 (map_congN, [#map_cong axioms]), |
1184 (map_congN, [#map_cong axioms]), |
1143 (map_id'N, [Lazy.force (#map_id' facts)]), |
1185 (map_id'N, [Lazy.force (#map_id' facts)]), |
|
1186 (rel_as_srelN, [Lazy.force (#rel_as_srel facts)]), |
|
1187 (rel_flipN, [Lazy.force (#rel_flip facts)]), |
1144 (set_natural'N, map Lazy.force (#set_natural' facts)), |
1188 (set_natural'N, map Lazy.force (#set_natural' facts)), |
1145 (srel_O_GrN, srel_O_Grs), |
1189 (srel_O_GrN, srel_O_Grs), |
1146 (srel_IdN, [Lazy.force (#srel_Id facts)]), |
1190 (srel_IdN, [Lazy.force (#srel_Id facts)]), |
1147 (srel_GrN, [Lazy.force (#srel_Gr facts)]), |
1191 (srel_GrN, [Lazy.force (#srel_Gr facts)]), |
1148 (srel_converseN, [Lazy.force (#srel_converse facts)]), |
1192 (srel_converseN, [Lazy.force (#srel_converse facts)]), |