Skip to content

Commit

Permalink
Do not create a class if the bound is natLeq
Browse files Browse the repository at this point in the history
  • Loading branch information
@jvanbruegge
jvanbruegge committed Nov 26, 2024
1 parent 9dc29d6 commit 8da6bd7
Show file tree
Hide file tree
Showing 30 changed files with 1,006 additions and 1,438 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/build_theories.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ jobs:
build:
runs-on: ubuntu-latest
container:
image: jvanbruegge/isabelle:2024-inductive
image: jvanbruegge/isabelle:2024-bnf_lift
options: "--user root"

if: github.event_name != 'pull_request' || !github.event.pull_request.draft
Expand Down
22 changes: 7 additions & 15 deletions Tools/binder_inductive.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -298,10 +298,6 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
(mk_image (hd gs) $ (s $ x))
)))) perms supps xs;

val inf_UNIV_goals = map (fn T => HOLogic.mk_Trueprop (HOLogic.mk_not (
Const (@{const_name finite}, T --> @{typ bool}) $ HOLogic.mk_UNIV (HOLogic.dest_setT T)
))) bind_Ts;

val supp_small_goals = map2 (fn x => fn (s, _) => Logic.all x (HOLogic.mk_Trueprop (
mk_ordLess (mk_card_of (s $ x)) (mk_card_of (HOLogic.mk_UNIV (HOLogic.dest_setT (hd bind_Ts))))
))) xs supps;
Expand Down Expand Up @@ -506,7 +502,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
fun lookup name = the_single (#thms (the (
Facts.lookup context facts (Facts.intern facts name)
)));
in (lookup "Un_bound", lookup "UN_bound", lookup "large") end;
in (lookup "Un_bound", lookup "UN_bound", lookup "large'") end;

fun set_bd_UNIVs_of_mr_bnfs (Inr (Inr sugar)) = maps #card_of_FVars_bound_UNIVs (#quotient_fps sugar)
| set_bd_UNIVs_of_mr_bnfs x =
Expand All @@ -515,22 +511,18 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
| Inr (Inl bnf) => BNF_Def.set_bd_of_bnf bnf
in map (fn thm => @{thm ordLess_ordLeq_trans} OF [thm]) thms end

fun UNIV_cinfinite_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.UNIV_cinfinite_of_mrbnf mrbnf]
| UNIV_cinfinite_of_mr_bnf (Inr (Inr sugar)) = [MRBNF_Def.UNIV_cinfinite_of_mrbnf (hd (#pre_mrbnfs sugar))]
| UNIV_cinfinite_of_mr_bnf _ = []
val infinite_UNIVs = map (fn thm => @{thm cinfinite_imp_infinite} OF [thm]) (maps UNIV_cinfinite_of_mr_bnf (flat mr_bnfs));

val supp_smalls = prove_missing supp_small_goals supps_specified supp_smalls (fn ctxt => fn mr_bnfs => K (EVERY1 [
REPEAT_DETERM o resolve_tac ctxt (
@{thms emp_bound ordLeq_refl card_of_Card_order} @ [Un_bound, UN_bound, var_large]
@ maps set_bd_UNIVs_of_mr_bnfs mr_bnfs
@ maps set_bd_UNIVs_of_mr_bnfs mr_bnfs @ infinite_UNIVs
)
]));

fun UNIV_cinfinite_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.UNIV_cinfinite_of_mrbnf mrbnf]
| UNIV_cinfinite_of_mr_bnf (Inr (Inr sugar)) = [MRBNF_Def.UNIV_cinfinite_of_mrbnf (hd (#pre_mrbnfs sugar))]
| UNIV_cinfinite_of_mr_bnf _ = []

val infinite_UNIVs = map (fn goal => Goal.prove_sorry lthy [] [] goal (fn {context=ctxt, ...} => EVERY1 [
rtac ctxt @{thm cinfinite_imp_infinite},
resolve_tac ctxt (maps UNIV_cinfinite_of_mr_bnf (flat mr_bnfs))
])) inf_UNIV_goals;

val binder_mr_bnfs = map_filter (fn (s, _) => case MRBNF_Def.mrbnf_of lthy s of
SOME mrbnf => SOME (Inl mrbnf)
| NONE => (case BNF_Def.bnf_of lthy s of
Expand Down
60 changes: 31 additions & 29 deletions Tools/mrbnf_comp.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,9 +204,11 @@ fun clean_compose_mrbnf const_policy qualify binding outer inners (unfold_set, l
in ([class], Local_Theory.exit_global lthy) end
) lthy
end;
val ((class, coclass), lthy) = lthy
|> mk_class "var_" sort
||>> mk_class "covar_" cosort;
val ((class, coclass), lthy) = case sort of
@{sort var} => ((@{sort var}, @{sort covar}), lthy)
| _ => lthy
|> mk_class "var_" sort
||>> mk_class "covar_" cosort;

val ((((((oDs, iDss), As), As'), Fs), Bs), names_lthy) = lthy
|> mk_TFrees' (map Type.sort_of_atyp (deads_of_mrbnf outer))
Expand Down Expand Up @@ -475,7 +477,10 @@ fun clean_compose_mrbnf const_policy qualify binding outer inners (unfold_set, l
wit = wit_tac
};

val class_thms =
val class_thms = case bd' of
Const (@{const_name natLeq}, _) =>
((@{sort var}, @{thm var_class.large}, @{thm var_class.regular}), (@{sort covar}, K @{thm covar_class.large}))
| _ =>
let
val ifco = bd_infinite_regular_card_order_of_mrbnf

Expand Down Expand Up @@ -1409,36 +1414,33 @@ fun seal_mrbnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds m
wit = wit_tac
};

fun mk_class prfx xs f lthy =
(Class_Declaration.class (qualify (Binding.name (prfx ^ Binding.name_of b))) [] xs [] #>> single ##> f ##> Local_Theory.exit_global |> Local_Theory.background_theory_result) lthy
val (class, lthy3) = mk_class "var_" (class_of_mrbnf mrbnf) I lthy;

val class_thms = class_thms_of_mrbnf mrbnf;
val covar_large' = @{thm ordIso_ordLeq_trans} OF [
@{thm cardSuc_invar_ordIso[THEN iffD2]} OF [
@{thm infinite_regular_card_order.Card_order} OF [bd_infinite_regular_card_order],
@{thm infinite_regular_card_order.Card_order} OF [bd_infinite_regular_card_order_of_mrbnf mrbnf],
@{thm ordIso_symmetric} OF [bd_ordIso]
],
#covar_large class_thms
]
val (coclass, lthy) = mk_class "covar_" (coclass_of_mrbnf mrbnf) (fn ctxt =>
let val subclass_tac = Locale.intro_locales_tac {strict = true, eager = true} ctxt []
in Class_Declaration.prove_subclass subclass_tac (the_single class) ctxt end
) lthy3;

val class_thms =
val (class_thms, lthy) = case mrbnf_bd' of
Const (@{const_name natLeq}, _) =>
(((@{sort var}, @{thm var_class.large}, @{thm var_class.regular}), (@{sort covar}, K @{thm covar_class.large})), lthy)
| _ =>
let
fun mk_class prfx xs f lthy =
(Class_Declaration.class (qualify (Binding.name (prfx ^ Binding.name_of b))) [] xs [] #>> single ##> f ##> Local_Theory.exit_global |> Local_Theory.background_theory_result) lthy
val (class, lthy3) = mk_class "var_" (class_of_mrbnf mrbnf) I lthy;

val class_thms = class_thms_of_mrbnf mrbnf;
val covar_large' = @{thm ordIso_ordLeq_trans} OF [
@{thm cardSuc_invar_ordIso[THEN iffD2]} OF [
@{thm infinite_regular_card_order.Card_order} OF [bd_infinite_regular_card_order],
@{thm infinite_regular_card_order.Card_order} OF [bd_infinite_regular_card_order_of_mrbnf mrbnf],
@{thm ordIso_symmetric} OF [bd_ordIso]
],
#covar_large class_thms
]
val (coclass, lthy) = mk_class "covar_" (coclass_of_mrbnf mrbnf) (fn ctxt =>
let val subclass_tac = Locale.intro_locales_tac {strict = true, eager = true} ctxt []
in Class_Declaration.prove_subclass subclass_tac (the_single class) ctxt end
) lthy3;
val var_large' = @{thm ordIso_ordLeq_trans} OF [
@{thm card_of_cong} OF [@{thm ordIso_symmetric} OF [bd_ordIso]],
#var_large class_thms
]
in
(
(class, var_large', #var_regular class_thms),
(coclass, K covar_large')
)
end
in (((class, var_large', #var_regular class_thms), (coclass, K covar_large')), lthy) end

val (mrbnf', lthy') =
mrbnf_def Hardly_Inline (user_policy Note_Some) true qualify tacs (SOME all_deads) (SOME class_thms)
Expand Down
185 changes: 97 additions & 88 deletions Tools/mrbnf_def.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1282,7 +1282,7 @@ val natLeq_boundN = "natLeq_bound";
val UNIV_cinfiniteN = "UNIV_cinfinite";
val supp_comp_boundN = "supp_comp_bound";
val Un_boundN = "Un_bound";
val UNION_boundN = "UNION_bound";
val UNION_boundN = "UN_bound";
val mr_rel_congN = "mr_rel_cong";
val mr_in_relN = "mr_in_rel";
val mr_le_rel_OON = "mr_le_rel_OO";
Expand Down Expand Up @@ -1708,7 +1708,10 @@ fun define_mrbnf_consts const_policy fact_policy internal Ds_opt classes_opt map
val ((class, var_large, var_regular), (mk_covar_type_class, mk_covar_large), lthy) = case classes_opt of
SOME ((class, var_large, var_regular), (coclass, mk_covar_large)) =>
((class, unfold_bd_def var_large, var_regular), (K (pair coclass), fn (sort, lthy) => unfold_bd_def' lthy (mk_covar_large (sort, lthy))), lthy)
| NONE =>
| NONE => case mrbnf_bd_raw of
Const (@{const_name natLeq}, _) =>
((@{sort var}, @{thm var_class.large}, @{thm var_class.regular}), (K (pair @{sort covar}), K @{thm covar_class.large}), lthy)
| _ =>
let
val (class, lthy) = case sort_opt of
SOME class => (class, lthy)
Expand Down Expand Up @@ -2204,97 +2207,103 @@ fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term
covar_large = covar_large
};

val UNIV_cinfinite =
val (UNIV_cinfinite, Un_bound, UNION_bound, lthy) = case class of
@{sort var} => (@{thm var_class.UNIV_cinfinite}, @{thm var_class.Un_bound}, @{thm var_class.UN_bound}, lthy)
| _ =>
let
val goal = TFree (Name.aT, class)
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_cinfinite
|> HOLogic.mk_Trueprop;
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm cinfinite_mono}, rtac ctxt var_large, rtac ctxt conjunct1,
rtac ctxt bd_Cinfinite])
|> Thm.close_derivation \<^here>
end;
val supp_the_inv_bound = @{thm supp_the_inv_bound_gen} OF
[conjI OF [UNIV_cinfinite, @{thm card_of_Card_order}]];
val UNIV_cinfinite =
let
val goal = TFree (Name.aT, class)
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_cinfinite
|> HOLogic.mk_Trueprop;
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm cinfinite_mono}, rtac ctxt var_large, rtac ctxt conjunct1,
rtac ctxt bd_Cinfinite])
|> Thm.close_derivation \<^here>
end;

val Un_bound =
let
val (T, Tc) = lthy |> mk_TFrees 1 ||> fst o mk_TFrees' [class] |> apply2 hd;
val (A1, A2) = mk_Frees "A" (map HOLogic.mk_setT [T, T]) lthy |> dest_cons o fst ||> hd;
fun mk_card_bound t = Tc
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_ordLess (mk_card_of t)
|> HOLogic.mk_Trueprop;
val goal = [A1, A2, mk_union (A1, A2)]
|> map mk_card_bound
|> foldr1 Logic.mk_implies
|> fold_rev Logic.all [A1, A2];
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm card_of_Un_ordLess_infinite},
rtac ctxt (unfold_thms ctxt @{thms cinfinite_def Field_card_of} UNIV_cinfinite),
REPEAT_DETERM_N 2 o assume_tac ctxt])
|> Thm.close_derivation \<^here>
end;
val Un_bound =
let
val (T, Tc) = lthy |> mk_TFrees 1 ||> fst o mk_TFrees' [class] |> apply2 hd;
val (A1, A2) = mk_Frees "A" (map HOLogic.mk_setT [T, T]) lthy |> dest_cons o fst ||> hd;
fun mk_card_bound t = Tc
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_ordLess (mk_card_of t)
|> HOLogic.mk_Trueprop;
val goal = [A1, A2, mk_union (A1, A2)]
|> map mk_card_bound
|> foldr1 Logic.mk_implies
|> fold_rev Logic.all [A1, A2];
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm card_of_Un_ordLess_infinite},
rtac ctxt (unfold_thms ctxt @{thms cinfinite_def Field_card_of} UNIV_cinfinite),
REPEAT_DETERM_N 2 o assume_tac ctxt])
|> Thm.close_derivation \<^here>
end;

val UNION_bound =
let
val ((Ta, Tb), Tc) = lthy
|> mk_TFrees 2
|>> apsnd hd o dest_cons
||> hd o fst o mk_TFrees' [class];
val ((I, A), i) = lthy
|> yield_singleton (mk_Frees "I") (HOLogic.mk_setT Ta)
||>> yield_singleton (mk_Frees "A") (Ta --> HOLogic.mk_setT Tb)
||> fst o yield_singleton (mk_Frees "i") Ta;
fun mk_card_bound t = Tc
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_ordLess (mk_card_of t)
|> HOLogic.mk_Trueprop;
val goal = [mk_card_bound I,
(HOLogic.mk_mem (i, I) |> HOLogic.mk_Trueprop, A $ i |> mk_card_bound)
|> Logic.mk_implies |> Logic.all i,
mk_UNION I (A $ i |> Term.absfree (dest_Free i)) |> mk_card_bound]
|> foldr1 Logic.mk_implies
|> fold_rev Logic.all [I, A];
val bound_Card_order = thm_instantiate_terms lthy [SOME (HOLogic.mk_UNIV Tc)]
@{thm card_of_Card_order};
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm regularCard_UNION}, rtac ctxt bound_Card_order,
rtac ctxt UNIV_cinfinite, rtac ctxt var_regular, assume_tac ctxt,
Goal.assume_rule_tac ctxt])
|> Thm.close_derivation \<^here>
end;
val UNION_bound =
let
val ((Ta, Tb), Tc) = lthy
|> mk_TFrees 2
|>> apsnd hd o dest_cons
||> hd o fst o mk_TFrees' [class];
val ((I, A), i) = lthy
|> yield_singleton (mk_Frees "I") (HOLogic.mk_setT Ta)
||>> yield_singleton (mk_Frees "A") (Ta --> HOLogic.mk_setT Tb)
||> fst o yield_singleton (mk_Frees "i") Ta;
fun mk_card_bound t = Tc
|> HOLogic.mk_UNIV
|> mk_card_of
|> mk_ordLess (mk_card_of t)
|> HOLogic.mk_Trueprop;
val goal = [mk_card_bound I,
(HOLogic.mk_mem (i, I) |> HOLogic.mk_Trueprop, A $ i |> mk_card_bound)
|> Logic.mk_implies |> Logic.all i,
mk_UNION I (A $ i |> Term.absfree (dest_Free i)) |> mk_card_bound]
|> foldr1 Logic.mk_implies
|> fold_rev Logic.all [I, A];
val bound_Card_order = thm_instantiate_terms lthy [SOME (HOLogic.mk_UNIV Tc)]
@{thm card_of_Card_order};
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
EVERY1 [rtac ctxt @{thm regularCard_UNION}, rtac ctxt bound_Card_order,
rtac ctxt UNIV_cinfinite, rtac ctxt var_regular, assume_tac ctxt,
Goal.assume_rule_tac ctxt])
|> Thm.close_derivation \<^here>
end;

val lthy = Local_Theory.background_theory (fn thy =>
let
val lthy = Named_Target.init [] (hd coclass) thy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("large", covar_large)
]) lthy) handle ERROR _ => lthy;
in Local_Theory.exit_global lthy end
) lthy;
val lthy = Local_Theory.background_theory (fn thy =>
let
val lthy = Named_Target.init [] (hd class) thy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("Un_bound", Un_bound),
("UN_bound", UNION_bound),
("cinfinite", UNIV_cinfinite)
]) lthy) handle ERROR _ => lthy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("large", var_large),
("regular", var_regular)
]) lthy) handle ERROR _ => lthy;
in Local_Theory.exit_global lthy end
) lthy;
val lthy = Local_Theory.background_theory (fn thy =>
let
val lthy = Named_Target.init [] (hd coclass) thy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("large", covar_large)
]) lthy) handle ERROR _ => lthy;
in Local_Theory.exit_global lthy end
) lthy;
val lthy = Local_Theory.background_theory (fn thy =>
let
val lthy = Named_Target.init [] (hd class) thy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("Un_bound", Un_bound),
("UN_bound", UNION_bound),
("UNIV_cinfinite", UNIV_cinfinite),
("large'", var_large)
]) lthy) handle ERROR _ => lthy;
val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
("large", var_large_raw),
("regular", var_regular)
]) lthy) handle ERROR _ => lthy;
in Local_Theory.exit_global lthy end
) lthy;
in (UNIV_cinfinite, Un_bound, UNION_bound, lthy) end;

val supp_the_inv_bound = @{thm supp_the_inv_bound_gen} OF
[conjI OF [UNIV_cinfinite, @{thm card_of_Card_order}]];
val supp_comp_bound =
let
val Tc = lthy |> fst o mk_TFrees' [class] |> the_single;
Expand Down
8 changes: 4 additions & 4 deletions Tools/mrbnf_vvsubst.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2157,11 +2157,11 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
let
val vname = short_type_name (fst (dest_Type (#T quot)));
val notes =
[(vname ^ "_cctor", [vvsubst_cctor]),
(vname ^ "_vvsubst_permute", [vvsubst_permute]),
(vname ^ "_set_simps", pset_simps)
[("vvsubst_cctor", [vvsubst_cctor]),
("vvsubst_permute", [vvsubst_permute]),
("set_ctor_simps", pset_simps)
] |> (map (fn (thmN, thms) =>
((Binding.name thmN, []), [(thms, [])])
((Binding.qualify true vname (Binding.name thmN), []), [(thms, [])])
));
in Local_Theory.notes notes lthy end
) (#quotient_fps fp_res) vvsubst_cctors vvsubst_permutes pset_simpss lthy;
Expand Down
3 changes: 3 additions & 0 deletions Tools/parser.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,9 @@ fun create_binder_specs specs lthy =
Typedecl.basic_typedecl {final = true} (b, length params, Mixfix.reset_pos mixfix)
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs lthy;

val fake_lthy = Local_Theory.type_notation true Syntax.mode_input
[(@{typ "('a, 'b) var_selector"}, Infix (Input.string "::", 999, Position.no_range))] fake_lthy;

val (specs, fake_lthy) = fold_map (create_binder_spec fake_T_names) specs fake_lthy;
in snd (MRBNF_Sugar.create_binder_datatype (hd specs) lthy) end;

Expand Down
Loading

0 comments on commit 8da6bd7

Please sign in to comment.