Skip to content

Implement fresh injection theorem #129

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
b4er wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Implement fresh injection theorem #129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
24093dc
remove code some duplication & generate fresh injection theorem (prov…
b4er Mar 19, 2026
6b71e70
bend apply script in VVSubst_Corec towards easier automation
b4er Mar 19, 2026
66d1b78
ML proof (draft)
b4er Mar 19, 2026
4c3d7ed
fix ML for least fixpoint
b4er Mar 19, 2026
d17e991
add correct T{1,2} lemmas in operations/
b4er Mar 23, 2026
369fdb3
clean ML proof
b4er Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
165 changes: 118 additions & 47 deletions Tools/mrbnf_fp.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1823,6 +1823,32 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
)) As;

val nbfrees = map (fn xs => length (fold (union (op=)) xs [])) bound_freesss;

fun mk_map_permute mrbnf deads fs permutes =
let
val nbounds = map length (hd raw_bound_setsss);
val rec_bound_fss = @{map 4} (fn nbound => fn f => fn rec_boundss => fst o fold_map (fn rec_bounds => fn hs =>
if length rec_bounds = 0 then (NONE, hs)
else if length rec_bounds = nbound then (SOME f, hs) else (SOME (hd hs), tl hs)
) rec_boundss) nbounds fs rec_boundsss hss;

val rec_ts = map2 (fn (permute, _) => fn rec_bound_fs =>
if forall (fn NONE => true | _ => false) rec_bound_fs then
HOLogic.id_const (Term.body_type (fastype_of permute))
else Term.list_comb (permute, map2 (fn g =>
fn NONE => HOLogic.id_const (fst (Term.dest_funT (fastype_of g)))
| SOME f => f
) fs rec_bound_fs)
) (replicate_rec permutes) (transpose rec_bound_fss);
val bfree_fs= flat (map2 replicate nbfrees fs);
in
MRBNF_Def.mk_map_comb_of_mrbnf deads
(map HOLogic.id_const plives @ rec_ts)
(map HOLogic.id_const pbounds @ flat (map2 (fn bounds => replicate (length bounds)) (hd raw_bound_setsss) fs))
(map (HOLogic.id_const o fst o Term.dest_funT o fastype_of) fs @ map HOLogic.id_const pfrees @ bfree_fs)
mrbnf
end;

val raw_refreshs = @{map 9} (fn alpha => fn alpha_intro => fn raw => fn mrbnf => fn deads => fn bound_setss => fn bfree_setss => fn rec_sets => fn x =>
let
val goal = HOLogic.mk_Trueprop (mk_ex ("y", fastype_of x) (fold_rev (curry HOLogic.mk_conj)
Expand Down Expand Up @@ -1888,28 +1914,8 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
Subgoal.FOCUS_PARAMS (fn {context=ctxt, params=hs, ...} =>
let
val gs = map (Thm.term_of o snd) params;
val hss = fst (fold_map (chop o length) hss (map (Thm.term_of o snd) hs));
val nbounds = map length (hd raw_bound_setsss);
val rec_bound_fss = @{map 4} (fn nbound => fn f => fn rec_boundss => fst o fold_map (fn rec_bounds => fn hs =>
if length rec_bounds = 0 then (NONE, hs)
else if length rec_bounds = nbound then (SOME f, hs) else (SOME (hd hs), tl hs)
) rec_boundss) nbounds gs rec_boundsss hss;

val rec_ts = map2 (fn (permute, _) => fn rec_bound_fs =>
if forall (fn NONE => true | _ => false) rec_bound_fs then
HOLogic.id_const (Term.body_type (fastype_of permute))
else Term.list_comb (permute, map2 (fn g =>
fn NONE => HOLogic.id_const (fst (Term.dest_funT (fastype_of g)))
| SOME f => f
) gs rec_bound_fs)
) (replicate_rec permute_raws) (transpose rec_bound_fss);
val bfree_fs = flat (map2 replicate nbfrees gs);

val map_t = MRBNF_Def.mk_map_comb_of_mrbnf deads
(map HOLogic.id_const plives @ rec_ts)
(map HOLogic.id_const pbounds @ flat (map2 (fn bounds => replicate (length bounds)) (hd raw_bound_setsss) gs))
(map (HOLogic.id_const o fst o Term.dest_funT o fastype_of) fs @ map HOLogic.id_const pfrees @ bfree_fs)
mrbnf $ x;

val map_t = mk_map_permute mrbnf deads gs permute_raws $ x;
in EVERY1 [
rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt map_t)] exI),
REPEAT_DETERM o EVERY' [
Expand Down Expand Up @@ -2213,7 +2219,7 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
val (ys, _) = lthy
|> mk_Frees "y" (map fastype_of xs);

val TT_inject0s = @{map 9} (fn x => fn y => fn bsetss => fn bfsetss => fn rec_sets => fn deads => fn mrbnf => fn ctor => fn raw =>
fun mk_gen_inject extra_prems x y bsetss bfsetss rec_sets deads mrbnf ctor =
let
val id_on_prems = @{map 6} (fn f => fn bsets => fn bfsets => fn bfree_boundss => fn rec_boundss => fn FVars_raws => mk_id_on (foldl1 mk_Un (
map2 (fn bfset => fn bfree_bounds =>
Expand Down Expand Up @@ -2242,34 +2248,19 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
else ([], hs) end
) rec_boundss rec_sets (replicate_rec FVars) hs)) fs bsetss rec_boundsss (transpose FVarsss) hss));

(* TODO: remove code duplication *)
val nbounds = map length (hd raw_bound_setsss);
val rec_bound_fss = @{map 4} (fn nbound => fn f => fn rec_boundss => fst o fold_map (fn rec_bounds => fn hs =>
if length rec_bounds = 0 then (NONE, hs)
else if length rec_bounds = nbound then (SOME f, hs) else (SOME (hd hs), tl hs)
) rec_boundss) nbounds fs rec_boundsss hss;

val rec_ts = map2 (fn (permute, _) => fn rec_bound_fs =>
if forall (fn NONE => true | _ => false) rec_bound_fs then
HOLogic.id_const (Term.body_type (fastype_of permute))
else Term.list_comb (permute, map2 (fn g =>
fn NONE => HOLogic.id_const (fst (Term.dest_funT (fastype_of g)))
| SOME f => f
) fs rec_bound_fs)
) (replicate_rec permutes) (transpose rec_bound_fss);
val bfree_fs = flat (map2 replicate nbfrees fs);

val map_t = MRBNF_Def.mk_map_comb_of_mrbnf deads
(map HOLogic.id_const plives @ rec_ts)
(map HOLogic.id_const pbounds @ flat (map2 (fn bounds => replicate (length bounds)) (hd raw_bound_setsss) fs))
(map (HOLogic.id_const o fst o Term.dest_funT o fastype_of) fs @ map HOLogic.id_const pfrees @ bfree_fs)
mrbnf $ x;
val map_t = mk_map_permute mrbnf deads fs permutes $ x;

val rhs = fold_rev (mk_ex o dest_Free) (fs @ flat hss) (fold_rev (curry HOLogic.mk_conj)
(map HOLogic.dest_Trueprop f_prems @ id_on_prems @ h_prems)
(map HOLogic.dest_Trueprop f_prems @ id_on_prems @ extra_prems @ h_prems)
(HOLogic.mk_eq (map_t, y))
);
val goal = mk_Trueprop_eq (HOLogic.mk_eq (fst ctor $ x, fst ctor $ y), rhs);
in
mk_Trueprop_eq (HOLogic.mk_eq (fst ctor $ x, fst ctor $ y), rhs)
end;

val TT_inject0s = @{map 9} (fn x => fn y => fn bsetss => fn bfsetss => fn rec_sets => fn deads => fn mrbnf => fn ctor => fn raw =>
let
val goal = mk_gen_inject [] x y bsetss bfsetss rec_sets deads mrbnf ctor;
in Goal.prove_sorry lthy (names [x, y]) [] goal (fn {context=ctxt, ...} => EVERY1 [
K (Local_Defs.unfold_tac ctxt (snd ctor :: map snd permutes)),
rtac ctxt trans,
Expand Down Expand Up @@ -2836,6 +2827,84 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
]) end
) permutes zs FVarsss alpha_bijs TT_total_abs_eq_iffs;

val TT_fresh_injects = @{map 9} (fn x => fn y => fn bsetss => fn bfsetss => fn rec_sets => fn deads => fn mrbnf => fn ctor => fn TT_inject0 =>
let
val card_hyps = map (fn A =>
let val bd = fastype_of A |> HOLogic.dest_setT |> HOLogic.mk_UNIV |> mk_card_of in
mk_ordLess (mk_card_of A) bd |> HOLogic.mk_Trueprop
end
) As;

fun mk_avoids_hyps z = map2 (fn A => fn bsets =>
mk_int_empty (foldl1 mk_Un (map (fn s => s $ z) bsets), A) |> HOLogic.mk_Trueprop
) As bsetss;

val imsupp_prems = map2 (fn f => fn A => mk_int_empty (mk_imsupp f, A)) fs As;

val concl = mk_gen_inject imsupp_prems x y bsetss bfsetss rec_sets deads mrbnf ctor;

val goal = Logic.list_implies (card_hyps @ mk_avoids_hyps x @ mk_avoids_hyps y, concl);

val pre_set_bd_UNIVs = MRBNF_Def.set_bd_UNIV_of_mrbnf mrbnf;
val bound_set_bd_offset =
length pre_set_bd_UNIVs - length bsetss - length (flat bfsetss) - length rec_sets;
val bd_thms = maps MRBNF_Def.set_bd_of_mrbnf mrbnfs @ pre_set_bd_UNIVs @ flat FVars_bd_UNIVs;

val mem_simps = @{thms Un_Diff_cancel Un_Diff_cancel2 Un_Diff Un_assoc UnI1 UnI2 Un_left_commute UN_I};
in
Goal.prove_sorry lthy (names (As @ [x, y])) [] goal (fn {context=ctxt, ...} => EVERY
((HEADGOAL o EVERY')
[EqSubst.eqsubst_tac ctxt [0] [TT_inject0],
rtac ctxt @{thm iffI[symmetric]},
REPEAT_DETERM o etac ctxt @{thm exE},
REPEAT_DETERM o etac ctxt @{thm conjE},
Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
EVERY1 (map (fn (_, ct) =>
rtac ctxt (infer_instantiate' ctxt [NONE, SOME ct] @{thm exI})
) params)
) ctxt,
REPEAT_DETERM o FIRST' [rtac ctxt @{thm conjI}, assume_tac ctxt],
REPEAT_DETERM o etac ctxt @{thm exE},
REPEAT_DETERM o etac ctxt @{thm conjE},
rotate_tac (5 * nvars)] ::

maps (fn set_bd_UNIV =>
[HEADGOAL (forward_tac ctxt [set_bd_UNIV RSN (2, @{thm ex_avoiding_bij[rotated 4]})]),
(REPEAT_DETERM o HEADGOAL) (assume_tac ctxt ORELSE'
resolve_tac ctxt (@{thms UN_bound Un_bound infinite_UNIV ordLeq_ordLess_trans[OF card_of_diff]} @ bd_thms)),
HEADGOAL (rotate_tac 1)]
) (pre_set_bd_UNIVs |> drop bound_set_bd_offset |> take nvars) @

[(HEADGOAL o EVERY')
[dresolve_tac ctxt @{thms sym},
Subgoal.FOCUS_PARAMS_FIXED (HEADGOAL o hyp_subst_tac_thin true o #context) ctxt],

(REPEAT_DETERM o HEADGOAL) (eresolve_tac ctxt @{thms exE conjE}),
HEADGOAL (Subgoal.FOCUS_PARAMS (fn {params, ...} =>
(HEADGOAL o EVERY' o map (fn (_, g) =>
resolve_tac ctxt [infer_instantiate' ctxt [NONE, SOME g] @{thm exI}]
)) (drop nvars params)
) ctxt),

(REPEAT_DETERM o HEADGOAL) (rtac ctxt @{thm conjI} THEN' assume_tac ctxt),

HEADGOAL (Subgoal.FOCUS_PARAMS_FIXED (fn {context=ctxt, ...} =>
HEADGOAL (REPEAT_DETERM_N nvars o
(EqSubst.eqsubst_asm_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf) THEN_ALL_NEW
FIRST' [resolve_tac ctxt @{thms supp_id_bound bij_id}, assume_tac ctxt, K all_tac]))
) ctxt),

HEADGOAL (rtac ctxt (MRBNF_Def.map_cong0_of_mrbnf mrbnf)),

(REPEAT_DETERM o HEADGOAL o FIRST')
[resolve_tac ctxt (permute_congs @ @{thms refl supp_id_bound bij_id}),
etac ctxt @{thm fresh_agree_on_bound} THEN_ALL_NEW assume_tac ctxt,
etac ctxt @{thm fresh_agree_on_top} THEN_ALL_NEW assume_tac ctxt,
etac ctxt @{thm fresh_agree_on},
SOLVED' (MRBNF_Util.asm_simp_only_tac ctxt mem_simps)] ]))
end
) xs ys bound_setsss bfree_setsss rec_setss deadss mrbnfs ctors TT_inject0s;

val permute_cong_ids = map (fn thm => Local_Defs.unfold0 lthy (@{thm id_apply} :: permute_ids) (thm OF (
replicate (2 * nvars) @{thm _} @ flat (replicate nvars @{thms bij_id supp_id_bound})
))) permute_congs;
Expand Down Expand Up @@ -2893,6 +2962,7 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
FVarss = map fst (nth FVars_rawss i),
noclash = nth raw_noclashs i,
inject = #inject raw,
fresh_inject = #inject raw,
permute_ctor = snd (nth permute_raws i),
permute_id0 = nth permute_raw_id0s i,
permute_id = nth permute_raw_ids i,
Expand Down Expand Up @@ -2928,6 +2998,7 @@ fun construct_binder_fp fp_kind models binding_relation lthy =
FVarss = map fst (nth FVarsss i),
noclash = nth noclashs i,
inject = nth TT_inject0s i,
fresh_inject = nth TT_fresh_injects i,
permute_ctor = nth permute_simps i,
permute_id0 = nth permute_id0s i,
permute_id = nth permute_ids i,
Expand Down
12 changes: 8 additions & 4 deletions Tools/mrbnf_fp_def_sugar.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ sig
inner: 'a,

inject: thm,
fresh_inject: thm,
permute_ctor: thm,
permute_id0: thm,
permute_id: thm,
Expand Down Expand Up @@ -120,6 +121,7 @@ type 'a fp_result_T = {
inner: 'a,

inject: thm,
fresh_inject: thm,
permute_ctor: thm,
permute_id0: thm,
permute_id: thm,
Expand All @@ -132,16 +134,17 @@ type 'a fp_result_T = {
card_of_FVars_bound_UNIVs: thm list
};

fun morph_fp_result_T morph phi { T, ctor, permute, FVarss, noclash, inner, inject, permute_ctor,
permute_id0, permute_id, permute_comp0, permute_comp, FVars_ctors, FVars_permutes, FVars_intross,
card_of_FVars_bounds, card_of_FVars_bound_UNIVs } = {
fun morph_fp_result_T morph phi { T, ctor, permute, FVarss, noclash, inner, inject, fresh_inject,
permute_ctor, permute_id0, permute_id, permute_comp0, permute_comp, FVars_ctors, FVars_permutes,
FVars_intross, card_of_FVars_bounds, card_of_FVars_bound_UNIVs } = {
T = Morphism.typ phi T,
ctor = Morphism.term phi ctor,
permute = Morphism.term phi permute,
FVarss = map (Morphism.term phi) FVarss,
noclash = BNF_Util.map_prod (Morphism.term phi) (Morphism.thm phi) noclash,
inner = morph phi inner,
inject = Morphism.thm phi inject,
fresh_inject = Morphism.thm phi fresh_inject,
permute_ctor = Morphism.thm phi permute_ctor,
permute_id0 = Morphism.thm phi permute_id0,
permute_id = Morphism.thm phi permute_id,
Expand Down Expand Up @@ -340,7 +343,8 @@ fun note_fp_result (fp_res : fp_result) lthy =
("rep_abs", [#rep_abs (#inner quot)]),
("rep_abs_sym", [#rep_abs_sym (#inner quot)]),
("abs_ctor", [#abs_ctor (#inner quot)]),
("TT_inject0", [#inject quot])
("TT_inject0", [#inject quot]),
("fresh_inject", [#fresh_inject quot])
];

fun note_always (quot : quotient_result fp_result_T) = [
Expand Down
Loading
Loading