Skip to content

Commit

Permalink
Use permute and support inference for all uses of binder_inductive
Browse files Browse the repository at this point in the history
  • Loading branch information
@jvanbruegge
jvanbruegge committed Sep 19, 2024
1 parent 954977d commit 6e4b598
Show file tree
Hide file tree
Showing 16 changed files with 225 additions and 246 deletions.
9 changes: 7 additions & 2 deletions Tools/binder_induction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,14 @@ fun extract_vars ctxt var t =
SOME mrbnf => MRBNF_Def.sets_of_mrbnf mrbnf
| NONE => (case BNF_Def.bnf_of ctxt name of
SOME bnf => BNF_Def.sets_of_bnf bnf
| NONE => error ("Type is neither a set nor a (MR)BNF: " ^ name)
| NONE => (case MRBNF_FP_Def_Sugar.fp_result_of ctxt name of
SOME sugar => #FVars (hd (filter (
fn quot => fst (dest_Type (#T quot)) = name
) (#quotient_fps sugar)))
| NONE => []
)
);
val subst = Term.subst_atomic_types (rev (map TVar (Term.add_tvars (hd sets) [])) ~~ Ts);
val subst = Term.subst_atomic_types (rev (map TVar (fold Term.add_tvars sets [])) ~~ Ts);
val sets' = map_filter (fn (T, s) => if Term.exists_subtype (curry (op=) var) T then
SOME (T, subst s) else NONE) (Ts ~~ sets);
val (ts, ts') = split_list (map (fn (T, s) => extract_deep T (case fastype_of t of
Expand Down
80 changes: 51 additions & 29 deletions Tools/binder_inductive.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,12 +149,14 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
||>> apfst hd o mk_Frees "p" [rho]
||>> apfst hd o mk_Frees "P" [param_Ts @ [rho] ---> @{typ bool}];

fun mk_map_comb mr_bnf fs =
fun mk_map_comb name mr_bnf fs =
let
val mapx = case mr_bnf of
Inl mrbnf => MRBNF_Def.map_of_mrbnf mrbnf
| Inr (Inl bnf) => BNF_Def.map_of_bnf bnf
| Inr (Inr sugar) => #rename (hd (#quotient_fps sugar))
| Inr (Inr sugar) => #rename (hd (filter (fn quot =>
fst (dest_Type (#T quot)) = name
) (#quotient_fps sugar)))
val Ts = fst (split_last (Term.binder_types (fastype_of mapx)));
val tyenv = Sign.typ_match (Proof_Context.theory_of no_defs_lthy) (
Ts ---> @{typ bool},
Expand Down Expand Up @@ -187,7 +189,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
| NONE => mr_bnf
else mr_bnf;
val mr_bnfs = fold (union ((op=) o apply2 fst)) mr_bnfs [];
val perm = mk_map_comb mr_bnf fs
val perm = mk_map_comb s mr_bnf fs
in (if member (op=) (map fst mr_bnfs) s then (mr_bnfs, perm) else ((s, mr_bnf) :: mr_bnfs, perm)) end
end
| _ => ([], HOLogic.id_const T)
Expand All @@ -205,7 +207,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
val raw_supps = map2 (fn s => fn x => if YXML.content_of s = "_" then
Inl (Term.absfree (dest_Free x) (case Binder_Induction.extract_vars no_defs_lthy (hd var_Ts) x of
(SOME t, _) => t
| (NONE, _) => mk_bot (fastype_of x))
| (NONE, _) => mk_bot (hd var_Ts)) (* TODO: multiple var kinds *)
) else Inr (Syntax.read_term no_defs_lthy s)
) (supps @ replicate (length param_Ts - length supps) "_") xs;

Expand All @@ -228,6 +230,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
val thy = Proof_Context.theory_of no_defs_lthy;
fun mk_match mk_T ts = map2 (fn t => fn T =>
let
val _ = @{print} (Thm.cterm_of no_defs_lthy t, T, mk_T T)
val t = Logic.varify_types_global t;
val tyenv = Sign.typ_match thy (fastype_of t, mk_T T) Vartab.empty;
in Envir.subst_term (tyenv, Vartab.empty) t end
Expand Down Expand Up @@ -429,9 +432,9 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
||>> apfst hd o chop 1
||> hd;

fun map_id0_of_mr_bnf (Inl mrbnf) = MRBNF_Def.map_id0_of_mrbnf mrbnf
| map_id0_of_mr_bnf (Inr (Inl bnf)) = BNF_Def.map_id0_of_bnf bnf
| map_id0_of_mr_bnf (Inr (Inr sugar)) = #rename_id0 (hd (#quotient_fps sugar))
fun map_id0_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_id0_of_mrbnf mrbnf]
| map_id0_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_id0_of_bnf bnf]
| map_id0_of_mr_bnf (Inr (Inr sugar)) = map #rename_id0 (#quotient_fps sugar)

fun prove_missing goals specified thms tac = fst (@{fold_map 4} (
fn true => (fn _ => fn _ => fn _ => fn acc => (hd acc, tl acc))
Expand All @@ -442,32 +445,32 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =

fun map_comp_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_comp_of_mrbnf mrbnf, MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]
| map_comp_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_comp_of_bnf bnf, BNF_Def.map_comp0_of_bnf bnf RS sym]
| map_comp_of_mr_bnf (Inr (Inr sugar)) =
let val quot = hd (#quotient_fps sugar) in
[#rename_comp quot, #rename_comp0 quot] end
| map_comp_of_mr_bnf (Inr (Inr sugar)) = maps (fn quot =>
[#rename_comp quot, #rename_comp0 quot]
) (#quotient_fps sugar)

val perm_id0s = prove_missing perm_id0_goals perms_specified perm_id0s (fn ctxt => fn mr_bnfs => K (EVERY1 [
K (Local_Defs.unfold0_tac ctxt (map map_id0_of_mr_bnf mr_bnfs)),
K (Local_Defs.unfold0_tac ctxt (maps map_id0_of_mr_bnf mr_bnfs)),
rtac ctxt refl
]));
val perm_comps = prove_missing perm_comp_goals perms_specified perm_comps (fn ctxt => fn mr_bnfs => K (EVERY1 [
K (Local_Defs.unfold0_tac ctxt (maps map_comp_of_mr_bnf mr_bnfs)),
K (Local_Defs.unfold0_tac ctxt (@{thms id_apply id_o o_id} @ maps map_comp_of_mr_bnf mr_bnfs)),
rtac ctxt refl
]));

fun set_map_of_mr_bnf (Inl mrbnf) = MRBNF_Def.set_map_of_mrbnf mrbnf
| set_map_of_mr_bnf (Inr (Inl bnf)) = BNF_Def.set_map_of_bnf bnf
| set_map_of_mr_bnf (Inr (Inr sugar)) = #FVars_renames (hd (#quotient_fps sugar))
| set_map_of_mr_bnf (Inr (Inr sugar)) = maps #FVars_renames (#quotient_fps sugar)

val supp_seminats = prove_missing supp_seminat_goals one_specified supp_seminats (fn ctxt => fn mr_bnfs => K (EVERY1 [
K (Local_Defs.unfold0_tac ctxt (
@{thms image_comp[unfolded comp_def] image_UN[symmetric] image_Un[symmetric]}
@{thms image_empty image_comp[unfolded comp_def] image_UN[symmetric] image_Un[symmetric]}
@ maps set_map_of_mr_bnf mr_bnfs
)),
rtac ctxt @{thm subset_refl}
]));

fun map_cong_id_of_mr_bnf (Inr (Inr sugar)) = #rename_cong_id (#inner (hd (#quotient_fps sugar)))
fun map_cong_id_of_mr_bnf (Inr (Inr sugar)) = map (#rename_cong_id o #inner) (#quotient_fps sugar)
| map_cong_id_of_mr_bnf x =
let
val thm1 = case x of
Expand All @@ -476,7 +479,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
val thm2 = case x of
Inl mrbnf => MRBNF_Def.map_id_of_mrbnf mrbnf
| Inr (Inl bnf) => BNF_Def.map_id_of_bnf bnf
in Local_Defs.unfold0 no_defs_lthy @{thms id_apply} (trans OF [thm1, thm2]) end
in [Local_Defs.unfold0 no_defs_lthy @{thms id_apply} (trans OF [thm1, thm2])] end

val perm_supports = prove_missing perm_support_goals one_specified perm_supports (fn ctxt => fn mr_bnfs => fn i =>
let
Expand All @@ -485,18 +488,19 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
val Inl set = nth raw_supps i
val sets = Uns_aux (snd (Term.dest_abs_global set)) [];
val n = length sets;
in EVERY1 [
in rtac ctxt @{thm id_apply} 1 ORELSE EVERY1 [
EVERY' (map (fn i => EVERY' [
REPEAT_DETERM o EVERY' [
resolve_tac ctxt (map map_cong_id_of_mr_bnf mr_bnfs),
resolve_tac ctxt (maps map_cong_id_of_mr_bnf mr_bnfs),
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id})
],
REPEAT_DETERM o rtac ctxt @{thm id_apply},
dtac ctxt meta_spec,
dtac ctxt meta_mp,
K (prefer_tac 2),
assume_tac ctxt,
rtac ctxt (BNF_Util.mk_UnIN n i),
REPEAT_DETERM o (rtac ctxt @{thm UN_I} ORELSE' assume_tac ctxt)
REPEAT_DETERM o (resolve_tac ctxt @{thms UN_I id_apply} ORELSE' assume_tac ctxt)
]) (1 upto n))
] end);

Expand All @@ -509,15 +513,16 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
)));
in (lookup "Un_bound", lookup "UN_bound", lookup "large") end;

fun set_bd_UNIVs_of_mr_bnfs (Inr (Inr sugar)) = #card_of_FVars_bound_UNIVs (hd (#quotient_fps sugar))
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 =
let val thms = case x of
Inl mrbnf => MRBNF_Def.set_bd_of_mrbnf mrbnf
| Inr (Inl bnf) => BNF_Def.set_bd_of_bnf bnf
in map (fn thm => @{thm ordLess_ordLeq_trans} OF [thm]) thms end

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 ordLeq_refl card_of_Card_order} @ [Un_bound, UN_bound, var_large]
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
)
]));
Expand All @@ -531,23 +536,40 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
resolve_tac ctxt (maps UNIV_cinfinite_of_mr_bnf (flat mr_bnfs))
])) inf_UNIV_goals;

val binder_mrbnfs = map_filter (
Option.mapPartial (MRBNF_Def.mrbnf_of lthy o fst) o try dest_Type o snd
) (
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
SOME bnf => SOME (Inr (Inl bnf))
| NONE => (case MRBNF_FP_Def_Sugar.fp_result_of lthy s of
SOME sugar => SOME (Inr (Inr sugar))
| NONE => NONE
)
)
) (map_filter (try dest_Type o snd) (
fold Term.add_frees (flat bind_ts) []
);
));

val bset_bounds = maps (fn Type (s, _) => (case MRBNF_Sugar.binder_sugar_of lthy s of
SOME sugar => #bset_bounds sugar
| NONE => [])
| _ => []) param_Ts;
val Bs_small = Goal.prove_sorry lthy [] [] Bs_small_goal (fn {context=ctxt, ...} => EVERY1 [
K (Local_Defs.unfold0_tac ctxt [snd G]),
REPEAT_DETERM o EVERY' [
TRY o etac ctxt disjE,
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
hyp_subst_tac ctxt,
REPEAT_DETERM o resolve_tac ctxt (
@{thms emp_bound iffD2[OF insert_bound]}
@ infinite_UNIVs
@ maps (map (fn thm => @{thm ordLess_ordLeq_trans} OF [thm]) o MRBNF_Def.set_bd_of_mrbnf) binder_mrbnfs
@ map MRBNF_Def.var_large_of_mrbnf binder_mrbnfs
@{thms emp_bound iffD2[OF insert_bound] ordLeq_refl}
@ infinite_UNIVs @ [Un_bound, UN_bound]
@ maps (fn thm => [thm, @{thm ordLess_ordLeq_trans} OF [thm]]) (
maps set_bd_UNIVs_of_mr_bnfs binder_mr_bnfs
)
@ maps (
fn Inl mrbnf => [MRBNF_Def.var_large_of_mrbnf mrbnf]
| _ => []
) binder_mr_bnfs
@ bset_bounds
)
]
]);
Expand Down
4 changes: 2 additions & 2 deletions Tools/mrbnf_fp_def_sugar.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,9 +255,9 @@ structure Data = Generic_Data (
fun merge data : T = Symtab.merge (K true) data;
);

val register_fp_results = fold (fn fp_result as { quotient_fps = ({ T = Type (s, _), ...} :: _), ...} =>
val register_fp_results = fold (fn fp_result as { quotient_fps, ...} => fold (fn { T = Type (s, _), ...} =>
Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.none}
(fn phi => Data.map (Symtab.update (s, morph_fp_result phi fp_result))));
(fn phi => Data.map (Symtab.update (s, morph_fp_result phi fp_result)))) quotient_fps);

fun fp_result_of_generic context =
Option.map (morph_fp_result (Morphism.transfer_morphism (Context.theory_of context)))
Expand Down
6 changes: 5 additions & 1 deletion Tools/mrbnf_sugar.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ type binder_sugar = {
set_simpss: thm list list,
subst_simps: thm list option,
bsetss: term option list list,
bset_bounds: thm list,
mrbnf: MRBNF_Def.mrbnf,
strong_induct: thm,
distinct: thm list,
Expand Down Expand Up @@ -56,18 +57,20 @@ type binder_sugar = {
set_simpss: thm list list,
subst_simps: thm list option,
bsetss: term option list list,
bset_bounds: thm list,
mrbnf: MRBNF_Def.mrbnf,
strong_induct: thm,
distinct: thm list,
ctors: (term * thm) list
};

fun morph_binder_sugar phi { map_simps, set_simpss, subst_simps, mrbnf,
strong_induct, distinct, ctors, bsetss } = {
strong_induct, distinct, ctors, bsetss, bset_bounds } = {
map_simps = map (Morphism.thm phi) map_simps,
set_simpss = map (map (Morphism.thm phi)) set_simpss,
subst_simps = Option.map (map (Morphism.thm phi)) subst_simps,
bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
bset_bounds = map (Morphism.thm phi) bset_bounds,
mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
strong_induct = Morphism.thm phi strong_induct,
distinct = map (Morphism.thm phi) distinct,
Expand Down Expand Up @@ -706,6 +709,7 @@ fun create_binder_datatype (spec : spec) lthy =
strong_induct = strong_induct,
subst_simps = Option.map snd tvsubst_opt,
bsetss = bset_optss,
bset_bounds = [],
mrbnf = mrbnf,
distinct = distinct,
ctors = ctors
Expand Down
5 changes: 0 additions & 5 deletions thys/Infinitary_FOL/InfFOL.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -352,11 +352,6 @@ inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (in
| AllE: "\<lbrakk> \<Delta> \<turnstile> All V f ; supp \<rho> \<subseteq> set\<^sub>k\<^sub>2 V \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f\<lbrakk>\<rho>\<rbrakk>"

binder_inductive deduct
for perms: "\<lambda>f. map_set\<^sub>k (rrename_ifol' f)" rrename_ifol'
and supps: "\<lambda>e1. \<Union>(FFVars_ifol' ` set\<^sub>k e1)" FFVars_ifol'
apply (auto simp: ifol'.rrename_id0s set\<^sub>k.map_id0 set\<^sub>k.map_comp set\<^sub>k.set_map ifol'.rrename_comp0s ifol'.rrename_comps ifol'.FFVars_rrenames)[6]
apply (metis UN_I ifol'.rrename_cong_ids set\<^sub>k.map_ident_strong)
apply (auto intro!: var_ifol'_pre_class.UN_bound simp: ifol'.rrename_cong_ids set\<^sub>k.set_bd ifol'.set_bd_UNIV infinite_UNIV small_set\<^sub>k\<^sub>2[unfolded small_def])[5]
subgoal for R B \<sigma> x1 x2
unfolding induct_rulify_fallback split_beta
apply (elim disj_forward exE)
Expand Down
Loading

0 comments on commit 6e4b598

Please sign in to comment.