86 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline |
86 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline |
87 datatype fact_policy = Dont_Note | Note_Some | Note_All |
87 datatype fact_policy = Dont_Note | Note_Some | Note_All |
88 |
88 |
89 val bnf_note_all: bool Config.T |
89 val bnf_note_all: bool Config.T |
90 val user_policy: fact_policy -> Proof.context -> fact_policy |
90 val user_policy: fact_policy -> Proof.context -> fact_policy |
|
91 val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context -> |
|
92 Proof.context |
91 |
93 |
92 val print_bnfs: Proof.context -> unit |
94 val print_bnfs: Proof.context -> unit |
93 val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> |
95 val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> |
94 ({prems: thm list, context: Proof.context} -> tactic) list -> |
96 ({prems: thm list, context: Proof.context} -> tactic) list -> |
95 ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> |
97 ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> |
520 |
522 |
521 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; |
523 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; |
522 |
524 |
523 val smart_max_inline_size = 25; (*FUDGE*) |
525 val smart_max_inline_size = 25; (*FUDGE*) |
524 |
526 |
|
527 fun note_bnf_thms fact_policy qualify b bnf = |
|
528 let |
|
529 val axioms = axioms_of_bnf bnf; |
|
530 val facts = facts_of_bnf bnf; |
|
531 val wits = wits_of_bnf bnf; |
|
532 in |
|
533 (if fact_policy = Note_All then |
|
534 let |
|
535 val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); |
|
536 val notes = |
|
537 [(bd_card_orderN, [#bd_card_order axioms]), |
|
538 (bd_cinfiniteN, [#bd_cinfinite axioms]), |
|
539 (bd_Card_orderN, [#bd_Card_order facts]), |
|
540 (bd_CinfiniteN, [#bd_Cinfinite facts]), |
|
541 (bd_CnotzeroN, [#bd_Cnotzero facts]), |
|
542 (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), |
|
543 (in_bdN, [Lazy.force (#in_bd facts)]), |
|
544 (in_monoN, [Lazy.force (#in_mono facts)]), |
|
545 (in_relN, [Lazy.force (#in_rel facts)]), |
|
546 (map_compN, [#map_comp axioms]), |
|
547 (map_idN, [#map_id axioms]), |
|
548 (map_transferN, [Lazy.force (#map_transfer facts)]), |
|
549 (map_wpullN, [#map_wpull axioms]), |
|
550 (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), |
|
551 (set_mapN, #set_map axioms), |
|
552 (set_bdN, #set_bd axioms)] @ |
|
553 (witNs ~~ wit_thmss_of_bnf bnf) |
|
554 |> map (fn (thmN, thms) => |
|
555 ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []), |
|
556 [(thms, [])])); |
|
557 in |
|
558 Local_Theory.notes notes #> snd |
|
559 end |
|
560 else |
|
561 I) |
|
562 #> (if fact_policy <> Dont_Note then |
|
563 let |
|
564 val notes = |
|
565 [(map_comp'N, [Lazy.force (#map_comp' facts)], []), |
|
566 (map_cong0N, [#map_cong0 axioms], []), |
|
567 (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs), |
|
568 (map_id'N, [Lazy.force (#map_id' facts)], []), |
|
569 (rel_eqN, [Lazy.force (#rel_eq facts)], []), |
|
570 (rel_flipN, [Lazy.force (#rel_flip facts)], []), |
|
571 (set_map'N, map Lazy.force (#set_map' facts), []), |
|
572 (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []), |
|
573 (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), |
|
574 (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), |
|
575 (rel_monoN, [Lazy.force (#rel_mono facts)], []), |
|
576 (rel_OON, [Lazy.force (#rel_OO facts)], [])] |
|
577 |> filter_out (null o #2) |
|
578 |> map (fn (thmN, thms, attrs) => |
|
579 ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), |
|
580 attrs), [(thms, [])])); |
|
581 in |
|
582 Local_Theory.notes notes #> snd |
|
583 end |
|
584 else |
|
585 I) |
|
586 end; |
|
587 |
525 |
588 |
526 (* Define new BNFs *) |
589 (* Define new BNFs *) |
527 |
590 |
528 fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs |
591 fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs |
529 (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy = |
592 (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy = |
1171 Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; |
1234 Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; |
1172 |
1235 |
1173 val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts |
1236 val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts |
1174 wits bnf_rel; |
1237 wits bnf_rel; |
1175 in |
1238 in |
1176 (bnf, lthy |
1239 (bnf, lthy |> note_bnf_thms fact_policy qualify b bnf) |
1177 |> (if fact_policy = Note_All then |
|
1178 let |
|
1179 val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); |
|
1180 val notes = |
|
1181 [(bd_card_orderN, [#bd_card_order axioms]), |
|
1182 (bd_cinfiniteN, [#bd_cinfinite axioms]), |
|
1183 (bd_Card_orderN, [#bd_Card_order facts]), |
|
1184 (bd_CinfiniteN, [#bd_Cinfinite facts]), |
|
1185 (bd_CnotzeroN, [#bd_Cnotzero facts]), |
|
1186 (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), |
|
1187 (in_bdN, [Lazy.force (#in_bd facts)]), |
|
1188 (in_monoN, [Lazy.force (#in_mono facts)]), |
|
1189 (in_relN, [Lazy.force (#in_rel facts)]), |
|
1190 (map_compN, [#map_comp axioms]), |
|
1191 (map_idN, [#map_id axioms]), |
|
1192 (map_transferN, [Lazy.force (#map_transfer facts)]), |
|
1193 (map_wpullN, [#map_wpull axioms]), |
|
1194 (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), |
|
1195 (set_mapN, #set_map axioms), |
|
1196 (set_bdN, #set_bd axioms)] @ |
|
1197 (witNs ~~ wit_thms) |
|
1198 |> map (fn (thmN, thms) => |
|
1199 ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []), |
|
1200 [(thms, [])])); |
|
1201 in |
|
1202 Local_Theory.notes notes #> snd |
|
1203 end |
|
1204 else |
|
1205 I) |
|
1206 |> (if fact_policy <> Dont_Note then |
|
1207 let |
|
1208 val notes = |
|
1209 [(map_comp'N, [Lazy.force (#map_comp' facts)], []), |
|
1210 (map_cong0N, [#map_cong0 axioms], []), |
|
1211 (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs), |
|
1212 (map_id'N, [Lazy.force (#map_id' facts)], []), |
|
1213 (rel_eqN, [Lazy.force (#rel_eq facts)], []), |
|
1214 (rel_flipN, [Lazy.force (#rel_flip facts)], []), |
|
1215 (set_map'N, map Lazy.force (#set_map' facts), []), |
|
1216 (rel_OO_GrpN, rel_OO_Grps, []), |
|
1217 (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), |
|
1218 (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), |
|
1219 (rel_monoN, [Lazy.force (#rel_mono facts)], []), |
|
1220 (rel_OON, [Lazy.force (#rel_OO facts)], [])] |
|
1221 |> filter_out (null o #2) |
|
1222 |> map (fn (thmN, thms, attrs) => |
|
1223 ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), |
|
1224 attrs), [(thms, [])])); |
|
1225 in |
|
1226 Local_Theory.notes notes #> snd |
|
1227 end |
|
1228 else |
|
1229 I)) |
|
1230 end; |
1240 end; |
1231 |
1241 |
1232 val one_step_defs = |
1242 val one_step_defs = |
1233 no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]); |
1243 no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]); |
1234 in |
1244 in |