--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Jan 15 16:45:12 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Jan 15 17:48:38 2025 +0100
@@ -322,7 +322,7 @@
shows "P a"
by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
-lemma suc_underS:
+lemma suc_underS':
assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
shows "b \<in> underS (suc B)"
using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Jan 15 16:45:12 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Jan 15 17:48:38 2025 +0100
@@ -59,6 +59,7 @@
val bd_card_order_of_bnf: bnf -> thm
val bd_cinfinite_of_bnf: bnf -> thm
val bd_regularCard_of_bnf: bnf -> thm
+ val bd_def_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
@@ -251,14 +252,15 @@
type defs = {
map_def: thm,
set_defs: thm list,
+ bd_def: thm,
rel_def: thm,
pred_def: thm
}
-fun mk_defs map sets rel pred = {map_def = map, set_defs = sets, rel_def = rel, pred_def = pred};
+fun mk_defs map sets bd rel pred = {map_def = map, bd_def = bd, set_defs = sets, rel_def = rel, pred_def = pred};
-fun map_defs f {map_def, set_defs, rel_def, pred_def} =
- {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, pred_def = f pred_def};
+fun map_defs f {map_def, set_defs, bd_def, rel_def, pred_def} =
+ {map_def = f map_def, set_defs = map f set_defs, bd_def = f bd_def, rel_def = f rel_def, pred_def = f pred_def};
val morph_defs = map_defs o Morphism.thm;
@@ -582,6 +584,7 @@
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 bd_def_of_bnf = #bd_def o #defs 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;
@@ -1005,8 +1008,10 @@
val notes =
[(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
(mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
+ (mk_def_binding bd_of_bnf, bd_def_of_bnf bnf),
(mk_def_binding pred_of_bnf, pred_def_of_bnf bnf)] @
@{map 2} (pair o mk_def_binding o K) (sets_of_bnf bnf) (set_defs_of_bnf bnf)
+ |> filter_out (fn (b, thm) => Thm.is_reflexive thm)
|> map (fn (b, thm) => ((b, []), [([thm], [])]));
in
lthy
@@ -2042,7 +2047,7 @@
val inj_map_strong = Lazy.lazy mk_inj_map_strong;
- val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_pred_def;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_bd_def bnf_rel_def bnf_pred_def;
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
--- a/src/HOL/Tools/BNF/bnf_lift.ML Wed Jan 15 16:45:12 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Wed Jan 15 17:48:38 2025 +0100
@@ -436,7 +436,7 @@
(* get the bnf for RepT *)
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
- bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
+ bnf_of_typ true Hardly_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
val set_bs =
@@ -670,7 +670,7 @@
[card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @
[le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
- val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+ val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
tactics wit_tac NONE map_b rel_b pred_b set_bs
(((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
lthy;
@@ -852,7 +852,7 @@
map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
- bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs
+ bnf_of_typ true Hardly_Inline (Binding.qualify true absT_name) flatten_tyargs
[] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy);
val live = length alphas;
val _ = (if live = 0 then error "No live variables" else ());
@@ -1889,7 +1889,7 @@
| mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt
| mk_wit_tacs _ _ _ = all_tac;
- val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+ val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs
(((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy;
--- a/src/HOL/Tools/inductive.ML Wed Jan 15 16:45:12 2025 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Jan 15 17:48:38 2025 +0100
@@ -21,7 +21,7 @@
signature INDUCTIVE =
sig
type result =
- {preds: term list, elims: thm list, raw_induct: thm,
+ {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
val transform_result: morphism -> result -> result
type info = {names: string list, coind: bool} * result
@@ -180,17 +180,18 @@
(** context data **)
type result =
- {preds: term list, elims: thm list, raw_induct: thm,
+ {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
-fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
+fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs, def, mono} =
let
val term = Morphism.term phi;
val thm = Morphism.thm phi;
val fact = Morphism.fact phi;
in
- {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
- induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
+ {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, def = thm def,
+ induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs,
+ mono = thm mono}
end;
type info = {names: string list, coind: bool} * result;
@@ -1152,6 +1153,8 @@
raw_induct = rulify lthy3 raw_induct,
induct = induct,
inducts = inducts,
+ def = fp_def,
+ mono = mono,
eqs = eqs'};
val lthy4 = lthy3
--- a/src/HOL/Tools/inductive_set.ML Wed Jan 15 16:45:12 2025 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Jan 15 17:48:38 2025 +0100
@@ -463,7 +463,7 @@
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof lthy)) monos;
- val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
+ val ({preds, intrs, elims, raw_induct, eqs, def, mono, ...}, lthy1) =
Inductive.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
@@ -513,7 +513,7 @@
(map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in
({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
- raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},
+ raw_induct = raw_induct', preds = map fst defs, eqs = eqs', def = def, mono = mono},
lthy4)
end;