--- a/src/HOL/Tools/BNF/bnf_def.ML Sat Jun 25 09:50:40 2022 +0000
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Jun 27 15:54:18 2022 +0200
@@ -2,7 +2,8 @@
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Author: Martin Desharnais, TU Muenchen
- Copyright 2012, 2013, 2014
+ Author: Jan van Brügge, TU Muenchen
+ Copyright 2012, 2013, 2014, 2022
Definition of bounded natural functors.
*)
@@ -57,6 +58,7 @@
val bd_Cnotzero_of_bnf: bnf -> thm
val bd_card_order_of_bnf: bnf -> thm
val bd_cinfinite_of_bnf: bnf -> thm
+ val bd_regularCard_of_bnf: bnf -> thm
val collect_set_map_of_bnf: bnf -> thm
val in_bd_of_bnf: bnf -> thm
val in_cong_of_bnf: bnf -> thm
@@ -135,7 +137,7 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: bnf -> nonemptiness_witness list
- val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
+ val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy = Dont_Note | Note_Some | Note_All
@@ -198,15 +200,16 @@
set_map0: thm list,
bd_card_order: thm,
bd_cinfinite: thm,
+ bd_regularCard: thm,
set_bd: thm list,
le_rel_OO: thm,
rel_OO_Grp: thm,
pred_set: thm
};
-fun mk_axioms' (((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel), pred) =
+fun mk_axioms' ((((((((((id, comp), cong), map), c_o), cinf), creg), set_bd), le_rel_OO), rel), pred) =
{map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel, pred_set = pred};
+ bd_cinfinite = cinf, bd_regularCard = creg, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel, pred_set = pred};
fun dest_cons [] = raise List.Empty
| dest_cons (x :: xs) = (x, xs);
@@ -219,23 +222,25 @@
||>> chop n
||>> dest_cons
||>> dest_cons
+ ||>> dest_cons
||>> chop n
||>> dest_cons
||>> dest_cons
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel pred =
- [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel, pred];
+fun zip_axioms mid mcomp mcong smap bdco bdinf bdreg sbd le_rel_OO rel pred =
+ [mid, mcomp, mcong] @ smap @ [bdco, bdinf, bdreg] @ sbd @ [le_rel_OO, rel, pred];
-fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
- le_rel_OO, rel_OO_Grp, pred_set} =
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite,
+ bd_regularCard, set_bd, le_rel_OO, rel_OO_Grp, pred_set} =
{map_id0 = f map_id0,
map_comp0 = f map_comp0,
map_cong0 = f map_cong0,
set_map0 = map f set_map0,
bd_card_order = f bd_card_order,
bd_cinfinite = f bd_cinfinite,
+ bd_regularCard = f bd_regularCard,
set_bd = map f set_bd,
le_rel_OO = f le_rel_OO,
rel_OO_Grp = f rel_OO_Grp,
@@ -576,6 +581,7 @@
val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
+val bd_regularCard_of_bnf = #bd_regularCard o #axioms o rep_bnf;
val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
@@ -835,6 +841,7 @@
val bd_CnotzeroN = "bd_Cnotzero";
val bd_card_orderN = "bd_card_order";
val bd_cinfiniteN = "bd_cinfinite";
+val bd_regularCardN = "bd_regularCard";
val collect_set_mapN = "collect_set_map";
val in_bdN = "in_bd";
val in_monoN = "in_mono";
@@ -912,6 +919,7 @@
val notes =
[(bd_card_orderN, [#bd_card_order axioms]),
(bd_cinfiniteN, [#bd_cinfinite axioms]),
+ (bd_regularCardN, [#bd_regularCard axioms]),
(bd_Card_orderN, [#bd_Card_order facts]),
(bd_CinfiniteN, [#bd_Cinfinite facts]),
(bd_CnotzeroN, [#bd_Cnotzero facts]),
@@ -1404,10 +1412,12 @@
val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
+ val regularCard_bd_goal = HOLogic.mk_Trueprop (mk_regularCard bnf_bd_As);
+
val set_bds_goal =
let
fun mk_goal set =
- Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As));
+ Logic.all x (HOLogic.mk_Trueprop (mk_ordLess (mk_card_of (set $ x)) bnf_bd_As));
in
map mk_goal bnf_sets_As
end;
@@ -1427,7 +1437,7 @@
Term.list_comb (mk_pred_spec Ds As', Ps)));
val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
- card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal pred_set_goal;
+ card_order_bd_goal cinfinite_bd_goal regularCard_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal pred_set_goal;
val mk_wit_goals = mk_wit_goals bs zs bnf_sets_As;
fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
@@ -1562,11 +1572,12 @@
val in_bd_goal =
fold_rev Logic.all As
(HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
+ val weak_set_bds = map (fn thm => @{thm ordLess_imp_ordLeq} OF [thm]) (#set_bd axioms);
in
Goal.prove_sorry lthy [] [] in_bd_goal
(fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst
(Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
- (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
+ (map Lazy.force set_map) weak_set_bds (#bd_card_order axioms)
bd_Card_order bd_Cinfinite bd_Cnotzero)
|> Thm.close_derivation \<^here>
end;
@@ -2028,11 +2039,11 @@
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id
- map_ident0 map_ident map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0
- rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer
- rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp
- rel_transfer rel_eq_onp pred_transfer pred_True pred_map pred_rel pred_mono_strong0
- pred_mono_strong pred_mono pred_cong0 pred_cong pred_cong_simp;
+ map_ident0 map_ident map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong
+ rel_cong_simp rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep
+ rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp
+ pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono
+ pred_cong0 pred_cong pred_cong_simp;
val wits = map2 mk_witness bnf_wits wit_thms;