From a2910b82556d70edefbba64104030f01a0de105a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Thu, 31 Oct 2024 22:54:43 +0000 Subject: [PATCH] Automate until permute_simps theorem --- Tools/mrbnf_fp.ML | 267 ++++++++++++++++++++++++++++++++- operations/Least_Fixpoint.thy | 10 +- operations/Least_Fixpoint2.thy | 23 ++- 3 files changed, 281 insertions(+), 19 deletions(-) diff --git a/Tools/mrbnf_fp.ML b/Tools/mrbnf_fp.ML index 941ea58..0001722 100644 --- a/Tools/mrbnf_fp.ML +++ b/Tools/mrbnf_fp.ML @@ -1480,7 +1480,272 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy = ])); in map (fn thm => Local_Defs.unfold0 lthy @{thms HOL.imp_ex HOL.imp_conjL} thm RS spec RS spec RS spec RS mp RS mp) thms end; - val _ = @{print} alpha_transs + val (As, _) = lthy + |> mk_Frees "A" (map (HOLogic.mk_setT o fst o Term.dest_funT o fastype_of) gs); + + val A_prems = map (fn A => HOLogic.mk_Trueprop ( + mk_ordLess (mk_card_of A) (mk_card_of (HOLogic.mk_UNIV (HOLogic.dest_setT (fastype_of A)))) + )) As; + + val nbfrees = map (fn xs => length (fold (union (op=)) xs [])) bound_freesss; + 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) + (map2 (fn A => fn bsets => mk_int_empty (foldl1 mk_Un (map (fn s => s $ Bound 0) bsets), A)) As bound_setss) + (alpha $ (#ctor raw $ x) $ (#ctor raw $ Bound 0)) + )); + in Goal.prove_sorry lthy (names (As @ [x])) A_prems goal (fn {context=ctxt, prems} => + let + val thms = @{map 5} (fn A => fn bsets => fn bfree_sets => fn rec_boundss => fn FVarss => + let + val bset = foldl1 mk_Un (map (fn bset => bset $ x) bsets); + val rec_sets' = @{map_filter 3} (fn rec_bounds => fn set => fn FVars => + if null rec_bounds then NONE else SOME (mk_UNION (set $ x) (fst FVars)) + ) rec_boundss rec_sets (replicate_rec FVarss); + val rec_set = mk_minus (foldl1 mk_Un (map (fn s => s $ x) bfree_sets @ rec_sets'), bset) + in infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [ + bset, mk_Un (mk_Un (A, bset), rec_set), rec_set + ]) @{thm eextend_fresh} end + ) As bound_setss bfree_setss rec_boundsss (transpose FVars_rawss); + in EVERY1 [ + EVERY' (map (fn thm => EVERY' [ + rtac ctxt (exE OF [thm]), + REPEAT_DETERM o resolve_tac ctxt (infinite_UNIV :: + @{thms ordLeq_ordLess_trans[OF card_of_diff]} + @ (MRBNF_Def.set_bd_of_mrbnf mrbnf RSS @{thm ordLess_ordLeq_trans}) + @ [MRBNF_Def.Un_bound_of_mrbnf mrbnf, MRBNF_Def.UNION_bound_of_mrbnf mrbnf] + @ [MRBNF_Def.var_large_of_mrbnf mrbnf] @ prems + @ flat FVars_raw_bd_UNIVs + ), + rtac ctxt @{thm Un_upper2}, + rtac ctxt @{thm Diff_disjoint}, + REPEAT_DETERM o etac ctxt conjE, + K (Local_Defs.unfold0_tac ctxt @{thms Un_Diff}) + ]) thms), + Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} => + let + val thmss = @{map 4} (fn (_, g) => fn bsets => fn rec_boundss => fn FVarss => + @{map_filter 3} (fn rec_bounds => fn rec_set => fn FVars => if null rec_bounds orelse rec_bounds = (0 upto length bsets - 1) then NONE else + SOME (infer_instantiate' ctxt (SOME g :: map (SOME o Thm.cterm_of ctxt) [ + mk_UNION (rec_set $ x) (fst FVars), foldl1 mk_Un (map (fn s => s $ x) bsets), + foldl1 mk_Un (map (fn i => nth bsets i $ x) rec_bounds) + ]) @{thm extend_id_on}) + ) rec_boundss rec_sets (replicate_rec FVarss) + ) params bound_setss rec_boundsss (transpose FVars_rawss); + in EVERY1 [ + EVERY' (map (fn thm => EVERY' [ + rtac ctxt (exE OF [thm]), + REPEAT_DETERM o assume_tac ctxt, + id_on_tac ctxt, + assume_tac ctxt, + etac ctxt @{thm Int_subset_empty2}, + rtac ctxt @{thm subset_trans[rotated]}, + rtac ctxt @{thm Un_upper1}, + rtac ctxt @{thm Un_upper2}, + rtac ctxt @{thm subsetI}, + rotate_tac ~1, + etac ctxt @{thm contrapos_pp}, + SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj}), + REPEAT_DETERM o etac ctxt conjE, + assume_tac ctxt, + REPEAT_DETERM o etac ctxt conjE + ]) (flat thmss)), + 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 raw_permutes) (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; + in EVERY1 [ + rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt map_t)] exI), + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf), + REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}) + ], + K (Local_Defs.unfold0_tac ctxt @{thms image_Un[symmetric]}), + REPEAT_DETERM o EVERY' [ + rtac ctxt conjI, + etac ctxt @{thm Int_subset_empty2}, + SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms Un_assoc}), + rtac ctxt @{thm Un_upper1} + ], + rtac ctxt (Drule.rotate_prems ~1 alpha_intro), + rtac ctxt (Drule.rotate_prems ~1 (iffD2 OF [nth (MRBNF_Def.mr_rel_map_of_mrbnf mrbnf) 2])), + K (Local_Defs.unfold0_tac ctxt @{thms inv_id id_o Grp_UNIV_id conversep_eq OO_eq}), + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_tac ctxt [0] @{thms inv_o_simp1}, + assume_tac ctxt + ], + K (Local_Defs.unfold0_tac ctxt [ + @{thm relcompp_conversep_Grp}, MRBNF_Def.mr_rel_id_of_mrbnf mrbnf RS sym + ]), + rtac ctxt (MRBNF_Def.rel_refl_strong_of_mrbnf mrbnf), + REPEAT_DETERM o resolve_tac ctxt (refl :: alpha_refls), + REPEAT_DETERM o (resolve_tac ctxt @{thms supp_id_bound bij_id} ORELSE' assume_tac ctxt), + TRY o id_on_tac ctxt, + REPEAT_DETERM o assume_tac ctxt + ] end + ) ctxt + ] end + ) ctxt + ] end + ) end + ) (#preds alphas) (#intrs alphas) raw_Ts mrbnfs deadss raw_bound_setsss raw_bfree_setsss raw_rec_setss raw_xs + + val avoid_raw_freshsss = @{map 3} (fn x => fn avoid => map2 (fn A => map (fn bset => + Goal.prove_sorry lthy (names (As @ [x])) A_prems (HOLogic.mk_Trueprop (mk_int_empty ( + bset $ (Term.list_comb (fst avoid $ x, As)), A + ))) (fn {context=ctxt, prems} => EVERY1 [ + K (Local_Defs.unfold0_tac ctxt [snd avoid]), + rtac ctxt @{thm someI2_ex}, + resolve_tac ctxt raw_refreshs, + K (Local_Defs.unfold0_tac ctxt @{thms Int_Un_distrib2 Un_empty}), + REPEAT_DETERM o resolve_tac ctxt prems, + REPEAT_DETERM o etac ctxt conjE, + assume_tac ctxt + ]) + )) As) raw_xs raw_avoids raw_bound_setsss; + + val quot_argTss = map2 (fn raw => fn quot => [ + #T raw --> #T raw --> @{typ bool}, + #T raw --> #abs_type (fst quot), + #abs_type (fst quot) --> #T raw + ]) raw_Ts quots; + val Quotient3s = @{map 6} (fn alpha => fn TT_abs => fn TT_rep => fn raw => fn quot => fn arg_Ts => + Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop ( + Const (@{const_name Quotient3}, arg_Ts ---> @{typ bool}) $ alpha $ TT_abs $ TT_rep + )) (fn {context=ctxt, ...} => EVERY1 [ + rtac ctxt @{thm quot_type.Quotient}, + rtac ctxt @{thm type_definition_quot_type}, + rtac ctxt (#type_definition (snd quot)), + rtac ctxt @{thm equivpI}, + rtac ctxt @{thm reflpI}, + resolve_tac ctxt alpha_refls, + rtac ctxt @{thm sympI}, + eresolve_tac ctxt alpha_syms, + rtac ctxt @{thm transpI}, + eresolve_tac ctxt alpha_transs, + assume_tac ctxt + ]) + ) (#preds alphas) TT_abss TT_reps raw_Ts quots quot_argTss; + + val TT_Quotients = @{map 8} (fn z => fn alpha => fn TT_abs => fn TT_rep => fn raw => fn quot => fn Quotient3 => fn arg_Ts => + Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (Const (@{const_name Quotient}, + arg_Ts ---> (#T raw --> #abs_type (fst quot) --> @{typ bool}) --> @{typ bool} + ) $ alpha $ TT_abs $ TT_rep $ (Term.absfree (dest_Free z) ( + HOLogic.eq_const (#abs_type (fst quot)) $ (TT_abs $ z) + )))) (fn {context=ctxt, ...} => EVERY1 [ + rtac ctxt @{thm QuotientI}, + rtac ctxt (@{thm Quotient3_abs_rep} OF [Quotient3]), + resolve_tac ctxt alpha_refls, + rtac ctxt (@{thm Quotient3_rel[symmetric]} OF [Quotient3]), + REPEAT_DETERM o rtac ctxt ext, + rtac ctxt iffI, + rtac ctxt conjI, + resolve_tac ctxt alpha_refls, + assume_tac ctxt, + etac ctxt conjE, + assume_tac ctxt + ]) + ) raw_zs (#preds alphas) TT_abss TT_reps raw_Ts quots Quotient3s quot_argTss; + + val TT_total_abs_eq_iffs = map2 (fn thm => fn alpha_refl => + thm RS @{thm Quotient_total_abs_eq_iff} OF [@{thm reflpI} OF [alpha_refl]] + ) TT_Quotients alpha_refls; + val TT_rep_abss = map2 (fn thm => fn alpha_refl => + thm RS @{thm Quotient_rep_abs} OF [alpha_refl] + ) TT_Quotients alpha_refls + val TT_abs_reps = TT_Quotients RSS @{thm Quotient_abs_rep}; + val TT_rep_abs_syms = map2 (curry (op RS)) TT_rep_abss alpha_syms; + + val TT_abs_ctors = @{map 7} (fn raw => fn x => fn TT_abs => fn ctor => fn mrbnf => fn deads => fn TT_total_abs_eq_iff => + let + val map_t = MRBNF_Def.mk_map_comb_of_mrbnf deads + (map HOLogic.id_const plives @ replicate_rec TT_abss) + (map HOLogic.id_const (pbounds @ bounds)) + (map HOLogic.id_const (frees @ pfrees @ bfrees)) mrbnf $ x; + val goal = mk_Trueprop_eq (TT_abs $ (#ctor raw $ x), fst ctor $ map_t); + in Goal.prove_sorry lthy (names [x]) [] goal (fn {context=ctxt, ...} => EVERY1 [ + K (Local_Defs.unfold0_tac ctxt [snd ctor]), + rtac ctxt (iffD2 OF [TT_total_abs_eq_iff]), + EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], + REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}, + K (Local_Defs.unfold0_tac ctxt @{thms id_o}), + resolve_tac ctxt (#intrs alphas), + REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id id_on_id eq_on_refl}, + K (Local_Defs.unfold0_tac ctxt ((MRBNF_Def.mr_rel_id_of_mrbnf mrbnf RS sym) :: raw_permute_ids)), + rtac ctxt (iffD2 OF [nth (MRBNF_Def.rel_map_of_mrbnf mrbnf) 1]), + K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_apply}), + rtac ctxt (MRBNF_Def.rel_refl_strong_of_mrbnf mrbnf), + REPEAT_DETERM o resolve_tac ctxt (refl :: TT_rep_abs_syms) + ]) end + ) raw_Ts raw_xs TT_abss ctors mrbnfs deadss TT_total_abs_eq_iffs; + + val permute_simps = @{map 7} (fn permute => fn ctor => fn x => fn mrbnf => fn deads => fn TT_total_abs_eq_iff => fn alpha_bij_eq_inv => + let + val map_t = MRBNF_Def.mk_map_comb_of_mrbnf deads + (map HOLogic.id_const plives @ map (fn (p, _) => Term.list_comb (p, fs)) (replicate_rec permutes)) + (map HOLogic.id_const pbounds @ flat (map2 (fn bsets => replicate (length bsets)) (hd raw_bound_setsss) fs)) + (fs @ map HOLogic.id_const pfrees @ bfree_fs) mrbnf $ x + val goal = mk_Trueprop_eq ( + Term.list_comb (fst permute, fs) $ (fst ctor $ x), + fst ctor $ map_t + ); + in Goal.prove_sorry lthy (names (fs @ [x])) f_prems goal (fn {context=ctxt, prems} => EVERY1 [ + K (Local_Defs.unfold_tac ctxt (snd ctor :: map snd permutes)), + EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound bij_id} @ prems), + K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}), + K (Local_Defs.unfold0_tac ctxt @{thms comp_def}), + rtac ctxt (iffD2 OF [TT_total_abs_eq_iff]), + rtac ctxt (alpha_bij_eq_inv OF prems RS iffD2), + EqSubst.eqsubst_tac ctxt [0] (map snd raw_permutes), + REPEAT_DETERM o resolve_tac ctxt (@{thms bij_imp_bij_inv supp_inv_bound} @ prems), + EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], + REPEAT_DETERM o resolve_tac ctxt (@{thms bij_imp_bij_inv supp_inv_bound supp_id_bound bij_id} @ prems), + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_tac ctxt [0] @{thms inv_o_simp1}, + resolve_tac ctxt prems + ], + K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}), + resolve_tac ctxt alpha_transs, + resolve_tac ctxt TT_rep_abss, + K (Local_Defs.unfold0_tac ctxt @{thms comp_def}), + resolve_tac ctxt (#intrs alphas), + REPEAT_DETERM o resolve_tac ctxt @{thms bij_id supp_id_bound id_on_id eq_on_refl}, + K (Local_Defs.unfold0_tac ctxt ((MRBNF_Def.mr_rel_id_of_mrbnf mrbnf RS sym) :: + MRBNF_Def.rel_map_of_mrbnf mrbnf @ raw_permute_ids) + ), + rtac ctxt (MRBNF_Def.rel_refl_strong_of_mrbnf mrbnf), + REPEAT_DETERM o rtac ctxt refl, + REPEAT_DETERM o EVERY' [ + resolve_tac ctxt (alpha_bij_eq_invs RSS iffD1), + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound bij_id} @ prems), + resolve_tac ctxt TT_rep_abs_syms + ] + ]) end + ) permutes ctors xs mrbnfs deadss TT_total_abs_eq_iffs alpha_bij_eq_invs; + + val _ = @{print} permute_simps in error "foo" end end \ No newline at end of file diff --git a/operations/Least_Fixpoint.thy b/operations/Least_Fixpoint.thy index 0fe57e2..f1a49aa 100644 --- a/operations/Least_Fixpoint.thy +++ b/operations/Least_Fixpoint.thy @@ -4737,14 +4737,16 @@ lemma permute_simps: (* END REPEAT_DETERM *) done -lemma permute_ids: - "permute_T1 id id x = x" - "permute_T2 id id x2 = x2" + +lemma permute_id0s: + "permute_T1 id id = id" + "permute_T2 id id = id" apply (unfold permute_T1_def permute_T2_def permute_raw_ids TT_abs_rep) + apply (unfold id_def[symmetric]) apply (rule refl)+ done -lemmas permute_id0s = permute_ids[THEN trans[OF _ id_apply[symmetric]], abs_def, THEN meta_eq_to_obj_eq] +lemmas permute_ids = trans[OF fun_cong[OF permute_id0s(1)] id_apply] trans[OF fun_cong[OF permute_id0s(2)] id_apply] lemma permute_comps: fixes f1::"'a::{var_T1_pre,var_T2_pre} \ 'a" and f2::"'b::{var_T1_pre,var_T2_pre} \ 'b" diff --git a/operations/Least_Fixpoint2.thy b/operations/Least_Fixpoint2.thy index a7ff995..41dc2e0 100644 --- a/operations/Least_Fixpoint2.thy +++ b/operations/Least_Fixpoint2.thy @@ -1223,7 +1223,7 @@ proof - apply assumption apply (rule supp_id_bound bij_id | assumption)+ apply (unfold id_o o_id triv_forall_equality) - + subgoal for g x f2 g' y f2' z apply (rule exI[of _ "g' \ g"]) apply (rule exI) @@ -1524,12 +1524,12 @@ lemmas TT_rep_abs_syms = alpha_syms[OF TT_rep_abs] lemma TT_abs_ctors: "TT_abs (raw_term_ctor x) = term_ctor (map_term_pre id id id TT_abs TT_abs TT_abs x)" apply (unfold term_ctor_def) apply (rule TT_total_abs_eq_iffs[THEN iffD2]) - apply (rule alpha_term.intros) - apply (rule supp_id_bound bij_id id_on_id eq_on_refl)+ - apply (unfold permute_raw_ids term_pre.mr_rel_id[symmetric]) apply (subst term_pre.map_comp) apply (rule supp_id_bound bij_id)+ apply (unfold id_o o_id) + apply (rule alpha_term.intros) + apply (rule supp_id_bound bij_id id_on_id eq_on_refl)+ + apply (unfold permute_raw_ids term_pre.mr_rel_id[symmetric]) apply (rule iffD2[OF term_pre.rel_map(2)]) apply (unfold comp_def) apply (rule term_pre.rel_refl_strong) @@ -1584,10 +1584,12 @@ lemma permute_ids: "permute_term id x = x" lemmas permute_id0s = permute_ids[THEN trans[OF _ id_apply[symmetric]], abs_def, THEN meta_eq_to_obj_eq] -lemma permute_comps: +lemma permute_comp0s: fixes f::"'a::var_term_pre \ 'a" assumes "bij f" "|supp f| f) x" + shows "permute_term g \ permute_term f = permute_term (g \ f)" + apply (rule ext) + apply (rule trans[OF comp_apply]) apply (unfold permute_term_def) apply (subst permute_raw_comps[symmetric]) apply (rule assms)+ @@ -1597,14 +1599,7 @@ lemma permute_comps: apply (rule TT_rep_abs) done -lemma permute_comp0s: - fixes f::"'a::var_term_pre \ 'a" - assumes "bij f" "|supp f| permute_term f = permute_term (g \ f)" - apply (rule ext) - apply (rule trans[OF comp_apply]) - apply (rule permute_comps[OF assms]) - done +lemmas permute_comps = trans[OF comp_apply[symmetric] fun_cong[OF permute_comp0s]] lemma permute_bijs: fixes f::"'a::var_term_pre \ 'a"