Skip to content

Commit bf5502f

Browse files
jvanbrueggejvanbruegge
committed
Add automation for refreshability
1 parent 6c5946d commit bf5502f

File tree

4 files changed

+140
-64
lines changed

4 files changed

+140
-64
lines changed

‎Tools/binder_inductive.ML‎

Lines changed: 68 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
379379
val goals = map (single o rpair []) (
380380
keep_perm perm_id0_goals @ keep_perm perm_comp_goals @ keep_both supp_seminat_goals
381381
@ keep_both perm_support_goals @ keep_supp supp_small_goals @ flat (keep_binders B_small_goals)
382-
@ option No_Equiv [G_equiv_goal] [] @ [G_refresh_goal]
382+
@ option No_Equiv [G_equiv_goal] [] @ option No_Refresh [G_refresh_goal] []
383383
);
384384
fun after_qed thmss lthy =
385385
let
@@ -430,15 +430,14 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
430430
val m2 = length (filter not one_specified);
431431
val m3 = length (filter not supps_specified);
432432
val m4 = length (filter not binders_specified);
433-
val (((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_equivs), G_refresh) = map hd thmss
433+
val (((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_equivs), G_refreshs) = map hd thmss
434434
|> chop (n - m)
435435
||>> chop (n - m)
436436
||>> chop (n - m2)
437437
||>> chop (n - m2)
438438
||>> chop (num_vars * (n - m3))
439439
||>> chop (length bind_ts - m4)
440-
||>> chop (option No_Equiv 1 0)
441-
||> hd;
440+
||>> chop (option No_Equiv 1 0);
442441

443442
fun map_id0_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_id0_of_mrbnf mrbnf]
444443
| map_id0_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_id0_of_bnf bnf]
@@ -586,18 +585,13 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
586585

587586
val perm_ids = map (fn thm => thm RS fun_cong RS @{thm trans[OF _ id_apply]}) perm_id0s;
588587

589-
val _ = @{print} (map snd perms)
590588
val G_equiv = if member (op=) options No_Equiv then hd G_equivs else
591589
Goal.prove_sorry lthy [] [] G_equiv_goal (fn {context=ctxt, ...} => EVERY1 [
592590
K (Local_Defs.unfold0_tac ctxt [snd G]),
593591
REPEAT_DETERM o EVERY' [
594592
TRY o etac ctxt @{thm disj_forward},
595-
SELECT_GOAL (print_tac ctxt "0"),
596593
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
597-
K (print_tac ctxt "0.1"),
598-
(*hyp_subst_tac ctxt,*)
599594
REPEAT_DETERM_N (length param_Ts + 1) o etac ctxt @{thm subst[OF sym]},
600-
K (print_tac ctxt "0.2"),
601595
Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
602596
let
603597
val (fs, args) = map (Thm.term_of o snd) params
@@ -615,70 +609,114 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
615609
val equiv_simps = Named_Theorems.get ctxt "MRBNF_Recursor.equiv_simps"
616610
val monos = Inductive.get_monos ctxt
617611
val set_maps = maps set_map_of_mr_bnf mr_bnfs;
618-
val _ = @{print} equiv
619-
val _ = @{print} (map (Thm.cterm_of ctxt) ts)
620-
val _ = @{print} set_maps
621-
val _ = @{print} (flat (map_filter (Option.map #permute_simps) param_sugars))
622612
in EVERY1 [
623-
K (print_tac ctxt "1"),
624613
EVERY' (map (fn t => rtac ctxt (
625614
infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] exI
626615
)) ts),
627-
K (print_tac ctxt "1.1"),
628616
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map snd perms)),
629617
rtac ctxt conjI,
630-
631-
K (print_tac ctxt "1.2"),
632618
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms image_Un} @ equiv_simps)),
633619
REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<union>)"]},
634620
REPEAT_DETERM1 o EVERY' [
635-
K (print_tac ctxt "1.3"),
636621
resolve_tac ctxt @{thms image_single[symmetric] image_empty refl} ORELSE' EVERY' [
637622
resolve_tac ctxt (map (fn thm => thm RS sym) (set_maps @ equiv_simps) @ equiv_simps),
638623
REPEAT_DETERM o assume_tac ctxt
639624
]
640625
],
641-
K (print_tac ctxt "2"),
642626
K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
643627
K (Local_Defs.unfold0_tac ctxt @{thms id_def[symmetric]}),
644628
REPEAT_DETERM o EVERY' [
645629
TRY o rtac ctxt conjI,
646630
SELECT_GOAL (EVERY1 [
647-
K (print_tac ctxt "foo"),
648-
REPEAT_DETERM1 o (K (print_tac ctxt "wat") THEN' FIRST' [
631+
REPEAT_DETERM1 o FIRST' [
649632
assume_tac ctxt,
650633
eresolve_tac ctxt [conjE],
651634
resolve_tac ctxt @{thms conjI refl TrueI bij_imp_bij_inv supp_inv_bound},
652635
rtac ctxt impI THEN' eresolve_tac ctxt @{thms injD[OF bij_is_inj, rotated -1]},
653636
EVERY' [
654-
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{print}(map_filter (try (fn thm => thm RS sym)) equiv_commute))),
637+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map_filter (try (fn thm => thm RS sym)) equiv_commute)),
655638
REPEAT_DETERM1 o EVERY' [
656639
EqSubst.eqsubst_tac ctxt [0] (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_comps),
657-
K (print_tac ctxt "comp"),
658640
REPEAT_DETERM1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_inv_bound bij_imp_bij_inv})
659641
],
660642
K (Local_Defs.unfold0_tac ctxt @{thms inv_o_simp1 inv_o_simp2 inv_simp1 inv_simp2}),
661643
K (Local_Defs.unfold0_tac ctxt (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_ids)),
662-
K (print_tac ctxt "after_comp"),
663644
assume_tac ctxt
664645
],
665646
eresolve_tac ctxt (map_filter (try (fn thm => Drule.rotate_prems ~1 thm)) equiv),
666647
CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (equiv @ equiv_simps @ flat (map_filter (Option.map #permute_simps) param_sugars))),
667-
(*EqSubst.eqsubst_tac ctxt [0] equiv,*)
668648
eresolve_tac ctxt (map (fn thm => Drule.rotate_prems ~1 (thm RS mp)) monos),
669649
resolve_tac ctxt monos,
670650
CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (flat (map_filter (Option.map (map (fn thm => thm RS sym) o #permute_simps)) param_sugars)))
671-
])
651+
]
672652
])
673-
],
674-
K (print_tac ctxt "3")
653+
]
675654
] end
676-
) ctxt,
677-
K (print_tac ctxt "4")
655+
) ctxt
678656
]
679657
]);
680658
val _ = @{print} G_equiv
681659

660+
val G_refresh = if member (op=) options No_Refresh then hd (G_refreshs) else
661+
let
662+
val var_rules = map (fn thm =>
663+
let val t = Logic.unvarify_global (Thm.prop_of thm)
664+
in (map Free (rev (Term.add_frees t [])), t) end
665+
) intrs;
666+
667+
fun collect_permutes _ (Free _) = []
668+
| collect_permutes _ (Var _) = []
669+
| collect_permutes _ (Bound _) = []
670+
| collect_permutes _ (Const _) = []
671+
| collect_permutes vars (Abs (_, _, t)) = collect_permutes vars t
672+
| collect_permutes vars (t as (t1 $ t2)) = case try (dest_Type o Term.body_type o fastype_of) t of
673+
NONE => collect_permutes vars t1 @ collect_permutes vars t2
674+
| SOME (s, _) => (case MRBNF_Sugar.binder_sugar_of no_defs_lthy s of
675+
NONE => collect_permutes vars t1 @ collect_permutes vars t2
676+
| SOME sugar =>
677+
let val (ctor, args) = Term.strip_comb t
678+
in case (map_filter I (map_index (fn (i, (t, _)) =>
679+
if (op=) (apply2 (fst o dest_Const) (t, ctor)) then
680+
SOME i else NONE
681+
) (#ctors sugar))) of
682+
[] => collect_permutes vars t1 @ collect_permutes vars t2
683+
| ctor_idx::_ => (case nth (hd (#bsetss sugar)) ctor_idx of
684+
NONE => maps (collect_permutes vars) args
685+
| SOME _ =>
686+
let
687+
val arg_Ts = Term.binder_types (fastype_of ctor);
688+
val permute_bounds = nth (#permute_bounds sugar) ctor_idx;
689+
val var_args = map (fn t => if member (op=) vars t then SOME t else NONE) args;
690+
val result = map_filter I (map2 (fn NONE => K NONE
691+
| SOME perm => Option.map (fn x => (x, perm))
692+
) permute_bounds var_args);
693+
694+
val tyenv = @{fold 2} (fn NONE => K I | SOME perm => fn T =>
695+
Sign.typ_match (Proof_Context.theory_of no_defs_lthy) (body_type (fastype_of perm), T)
696+
) permute_bounds arg_Ts Vartab.empty;
697+
698+
in map (apsnd (Envir.subst_term (tyenv, Vartab.empty))) result
699+
@ maps (collect_permutes vars) args
700+
end
701+
)
702+
end
703+
);
704+
fun isNONE NONE = true
705+
| isNONE _ = false
706+
val permute_bounds = map (distinct (op=) o uncurry collect_permutes) var_rules;
707+
val matrix = map2 (fn (vars, _) => fn perms =>
708+
let val inner = map (AList.lookup (op=) perms) vars;
709+
in if forall isNONE inner then NONE else SOME inner end
710+
) var_rules permute_bounds;
711+
val _ = @{print} (map (Option.map (map (Option.map (Thm.cterm_of lthy)))) matrix)
712+
in Goal.prove_sorry lthy [] [] G_refresh_goal (fn {context=ctxt, ...} => EVERY1 [
713+
K (Local_Defs.unfold0_tac ctxt (snd G :: map snd perms)),
714+
Subgoal.FOCUS (fn {context=ctxt, prems, ...} =>
715+
refreshability_tac false (map fst supps) matrix (nth prems 2) (nth prems 1) supp_smalls (map snd supps) ctxt
716+
) ctxt
717+
]) end;
718+
val _ = @{print} G_refresh
719+
682720
fun mk_induct mono = Drule.rotate_prems ~1 (
683721
apply_n @{thm le_funD} n (@{thm lfp_induct} OF [mono])
684722
RS @{thm le_boolD}

‎Tools/mrbnf_sugar.ML‎

Lines changed: 37 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ type binder_sugar = {
1717
permute_simps: thm list,
1818
subst_simps: thm list option,
1919
bsetss: term option list list,
20+
permute_bounds: term option list list,
2021
bset_bounds: thm list,
2122
mrbnf: MRBNF_Def.mrbnf,
2223
strong_induct: thm,
@@ -59,6 +60,7 @@ type binder_sugar = {
5960
permute_simps: thm list,
6061
subst_simps: thm list option,
6162
bsetss: term option list list,
63+
permute_bounds: term option list list,
6264
bset_bounds: thm list,
6365
mrbnf: MRBNF_Def.mrbnf,
6466
strong_induct: thm,
@@ -67,12 +69,13 @@ type binder_sugar = {
6769
};
6870

6971
fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf,
70-
strong_induct, distinct, ctors, bsetss, bset_bounds } = {
72+
strong_induct, distinct, ctors, bsetss, bset_bounds, permute_bounds } = {
7173
map_simps = map (Morphism.thm phi) map_simps,
7274
permute_simps = map (Morphism.thm phi) permute_simps,
7375
set_simpss = map (map (Morphism.thm phi)) set_simpss,
7476
subst_simps = Option.map (map (Morphism.thm phi)) subst_simps,
7577
bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
78+
permute_bounds = map (map (Option.map (Morphism.term phi))) permute_bounds,
7679
bset_bounds = map (Morphism.thm phi) bset_bounds,
7780
mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
7881
strong_induct = Morphism.thm phi strong_induct,
@@ -334,8 +337,7 @@ fun create_binder_datatype (spec : spec) lthy =
334337
val bounds = map_filter (fn (x, MRBNF_Def.Bound_Var) => SOME (TFree x) | _ => NONE) (#vars spec);
335338
val frees = map_filter (fn (x, MRBNF_Def.Free_Var) => SOME (TFree x) | _ => NONE) (#vars spec);
336339

337-
(* TODO: Use mrbnf sets here (only relevant for passive variables) *)
338-
val (bset_optss, set_simpss) = split_list (map (fn FVars =>
340+
val param_vars = map (fn FVars =>
339341
let
340342
fun get_var vars = hd (filter (fn T =>
341343
Term.typ_subst_atomic replace T = HOLogic.dest_setT (range_type (fastype_of FVars))
@@ -345,7 +347,12 @@ fun create_binder_datatype (spec : spec) lthy =
345347
val rec_bounds = map (nth rec_vars) (the_default [] (
346348
Option.mapPartial (try (nth (#binding_rel spec))) (get_index bound bounds)
347349
));
348-
in split_list (map2 (fn (ctor, _) => fn (_, tys) =>
350+
in (free, bound, rec_bounds) end
351+
) (#FVars quotient);
352+
353+
(* TODO: Use mrbnf sets here (only relevant for passive variables) *)
354+
val (bset_optss, set_simpss) = split_list (map2 (fn FVars => fn (free, bound, rec_bounds) =>
355+
split_list (map2 (fn (ctor, _) => fn (_, tys) =>
349356
let
350357
val (xs, _) = lthy
351358
|> mk_Frees "x" tys;
@@ -406,9 +413,10 @@ fun create_binder_datatype (spec : spec) lthy =
406413
]
407414
])) end
408415
) ctors (#ctors spec))
409-
end) (#FVars quotient));
416+
) (#FVars quotient) param_vars);
410417

411418
val ctors_tys = ctors ~~ map snd (#ctors spec);
419+
412420
val distinct = flat (flat (map_index (fn (i, ((ctor, ctor_def), tys1)) => map_index (fn (j, ((ctor2, ctor2_def), tys2)) =>
413421
let
414422
val ((xs, ys), _) = names_lthy
@@ -653,10 +661,10 @@ fun create_binder_datatype (spec : spec) lthy =
653661
];
654662
in mk_map_simps lthy true fs (SOME o MRBNF_Recursor.mk_supp_bound) (fn t => fn _ => SOME (mk_imsupp t)) (K []) [] mapx tac end;
655663

664+
val (fs, _) = lthy
665+
|> mk_Frees "f" (map (fn a => a --> a) vars);
656666
val permute_simps =
657667
let
658-
val (fs, _) = lthy
659-
|> mk_Frees "f" (map (fn a => a --> a) vars);
660668
val Ts' = snd (dest_Type qT);
661669
val mapx = Term.subst_atomic_types (Ts' ~~ vars) (#rename quotient);
662670
fun tac ctxt prems = EVERY1 [
@@ -673,6 +681,27 @@ fun create_binder_datatype (spec : spec) lthy =
673681
(single o HOLogic.mk_Trueprop o mk_bij) bounds mapx tac
674682
end;
675683

684+
val permute_boundss = map2 (fn (_, tys) => fn permute_simp =>
685+
let
686+
val (xs, _) = lthy
687+
|> mk_Frees "x" (map (Term.typ_subst_atomic replace) tys);
688+
val permute_args = Thm.prop_of permute_simp
689+
|> Logic.strip_imp_concl
690+
|> HOLogic.dest_Trueprop
691+
|> snd o HOLogic.dest_eq
692+
|> Logic.unvarify_global
693+
|> snd o Term.strip_comb;
694+
695+
val bound = map (fn T =>
696+
map (fn (_, bound, rec_bounds) => member (op=) (bound::rec_bounds) T) param_vars
697+
) tys;
698+
in @{map 3} (fn x => fn t => fn bn => if not (exists I bn) then NONE else SOME (
699+
fold_rev (fn (b, f) => fn t => Term.absfree (dest_Free f) (if b then t else
700+
Term.subst_atomic [(f, HOLogic.id_const (domain_type (fastype_of f)))] t
701+
)) (bn ~~ fs) (Term.absfree (dest_Free x) t)
702+
)) xs permute_args bound end
703+
) ctors_tys permute_simps;
704+
676705
val cmin_UNIV = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars);
677706
val Cinfinite_card = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_conj (
678707
mk_cinfinite cmin_UNIV, mk_Card_order cmin_UNIV
@@ -751,6 +780,7 @@ fun create_binder_datatype (spec : spec) lthy =
751780
strong_induct = strong_induct,
752781
subst_simps = Option.map snd tvsubst_opt,
753782
bsetss = bset_optss,
783+
permute_bounds = permute_boundss,
754784
bset_bounds = [],
755785
mrbnf = mrbnf,
756786
distinct = distinct,

‎thys/MRBNF_FP.thy‎

Lines changed: 29 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -347,14 +347,25 @@ lemma extend_fresh:
347347
unfolding Int_Un_distrib fun_eq_iff o_apply id_apply
348348
by blast
349349

350+
named_theorems refresh_extends
351+
named_theorems refresh_smalls
352+
named_theorems refresh_simps
353+
named_theorems refresh_intros
354+
named_theorems refresh_elims
355+
350356
ML \<open>
351357
local
352358
open BNF_Util
353359
open BNF_FP_Util
354360
in
355361
356-
fun refreshability_tac verbose supps renames instss G_thm eqvt_thm extend_thms small_thms simp_thms intro_thms elim_thms ctxt =
362+
fun refreshability_tac verbose supps instss G_thm eqvt_thm smalls simps ctxt =
357363
let
364+
val extend_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_extends";
365+
val small_thms = smalls @ Named_Theorems.get ctxt "MRBNF_FP.refresh_smalls";
366+
val simp_thms = simps @ Named_Theorems.get ctxt "MRBNF_FP.refresh_simps";
367+
val intro_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_intros";
368+
val elim_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_elims";
358369
val n = length supps;
359370
fun case_tac NONE _ prems ctxt = HEADGOAL (Method.insert_tac ctxt prems THEN'
360371
K (if verbose then print_tac ctxt "pre_simple_auto" else all_tac)) THEN SOLVE (auto_tac ctxt)
@@ -375,15 +386,17 @@ val _ = prems |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
375386
|> Library.foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>);
376387
val fresh = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt B), SOME (Thm.cterm_of ctxt A)]
377388
@{thm extend_fresh};
389+
val _ = (verbose ? @{print tracing}) fresh
378390

379391
fun case_inner_tac fs fprems ctxt =
380-
let
392+
let
393+
val _ = (verbose ? @{print tracing}) fs
381394
val f = hd fs |> snd |> Thm.term_of;
382395
val ex_f = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt f)] exI;
383396
val ex_B' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt (mk_image f $ B))] exI;
384397
val args = params |> map (snd #> Thm.term_of);
385398
val xs = @{map 2} (fn i => fn a => Thm.cterm_of ctxt
386-
(case i of SOME i => nth renames i $ f $ a | NONE => a)) insts args;
399+
(case i of SOME t => t $ f $ a | NONE => a)) insts args;
387400
val _ = fprems |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
388401
val eqvt_thm = eqvt_thm OF take 2 fprems;
389402
val extra_assms = assms RL (eqvt_thm :: extend_thms);
@@ -403,22 +416,22 @@ val _ = extra_assms |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
403416
addSEs elim_thms) 0 10) THEN_ALL_NEW (SELECT_GOAL (print_tac ctxt "auto failed")))
404417
end;
405418
val small_ctxt = ctxt addsimps small_thms;
406-
in
407-
HEADGOAL (rtac ctxt (fresh RS exE) THEN'
408-
SELECT_GOAL (auto_tac (small_ctxt addsimps [hd defs])) THEN'
409-
REPEAT_DETERM_N 2 o (asm_simp_tac small_ctxt) THEN'
410-
SELECT_GOAL (unfold_tac ctxt @{thms Int_Un_distrib Un_empty}) THEN'
411-
REPEAT_DETERM o etac ctxt conjE THEN'
419+
in EVERY1 [
420+
rtac ctxt (fresh RS exE),
421+
SELECT_GOAL (auto_tac (small_ctxt addsimps [hd defs])),
422+
REPEAT_DETERM_N 2 o (asm_simp_tac small_ctxt),
423+
SELECT_GOAL (unfold_tac ctxt @{thms Int_Un_distrib Un_empty}),
424+
REPEAT_DETERM o etac ctxt conjE,
412425
Subgoal.SUBPROOF (fn focus =>
413-
case_inner_tac (#params focus) (#prems focus) (#context focus)) ctxt)
414-
end;
426+
case_inner_tac (#params focus) (#prems focus) (#context focus)) ctxt
427+
] end;
415428
in
416-
unfold_tac ctxt @{thms conj_disj_distribL ex_disj_distrib} THEN
417-
HEADGOAL (
418-
rtac ctxt (G_thm RSN (2, cut_rl)) THEN'
419-
REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE conjE disj_forward}) THEN'
429+
unfold_tac ctxt @{thms conj_disj_distribL ex_disj_distrib} THEN EVERY1 [
430+
rtac ctxt (G_thm RSN (2, cut_rl)),
431+
REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE conjE disj_forward}),
420432
EVERY' (map (fn insts => Subgoal.SUBPROOF (fn focus =>
421-
case_tac insts (#params focus) (#prems focus) (#context focus)) ctxt) instss))
433+
case_tac insts (#params focus) (#prems focus) (#context focus)) ctxt) instss)
434+
]
422435
end;
423436

424437
end;

0 commit comments

Comments
 (0)