From af4c85392c94655b9b959a16d69497e813261f22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Fri, 18 Oct 2024 12:50:15 +0100 Subject: [PATCH 1/2] Automate simp rules for permute/rrename --- Tools/mrbnf_sugar.ML | 73 ++++++++++++++++++++++++++++++++------------ 1 file changed, 53 insertions(+), 20 deletions(-) diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML index 5595acde..7958910a 100644 --- a/Tools/mrbnf_sugar.ML +++ b/Tools/mrbnf_sugar.ML @@ -14,6 +14,7 @@ type spec = { type binder_sugar = { map_simps: thm list, set_simpss: thm list list, + permute_simps: thm list, subst_simps: thm list option, bsetss: term option list list, bset_bounds: thm list, @@ -55,6 +56,7 @@ type spec = { type binder_sugar = { map_simps: thm list, set_simpss: thm list list, + permute_simps: thm list, subst_simps: thm list option, bsetss: term option list list, bset_bounds: thm list, @@ -64,9 +66,10 @@ type binder_sugar = { ctors: (term * thm) list }; -fun morph_binder_sugar phi { map_simps, set_simpss, subst_simps, mrbnf, +fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf, strong_induct, distinct, ctors, bsetss, bset_bounds } = { map_simps = map (Morphism.thm phi) map_simps, + permute_simps = map (Morphism.thm phi) permute_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, @@ -505,10 +508,13 @@ fun create_binder_datatype (spec : spec) lthy = UN_single }; val nvars = length vars; - fun mk_map_simps lthy fs mk_supp_bound_opt mk_imsupp mapx tac = + fun mk_map_simps lthy do_noclash fs mk_supp_bound_opt mk_imsupp_opt mk_extra_prems extra_apply_args mapx tac = let val mapx = Term.list_comb (mapx, fs); - val prems = map_filter (Option.map HOLogic.mk_Trueprop o mk_supp_bound_opt) fs; + val (prem_fs, prems) = split_list (map_filter (fn f => case mk_supp_bound_opt f of + NONE => NONE + | SOME t => SOME (f, HOLogic.mk_Trueprop t) + ) fs); fun mk_map (T as Type (n, Ts)) = (case MRBNF_Def.mrbnf_of lthy n of SOME mrbnf => @@ -524,7 +530,7 @@ fun create_binder_datatype (spec : spec) lthy = else Term.list_comb (inner_map, gs) end | NONE => HOLogic.id_const T) | mk_map (T as TFree _) = - (if member (op=) frees T then + (if member (op=) (frees @ extra_apply_args) T then case List.find (fn Free (_, T') => domain_type T' = Term.typ_subst_atomic replace T) fs of SOME t => t | NONE => HOLogic.id_const T @@ -576,16 +582,19 @@ fun create_binder_datatype (spec : spec) lthy = | NONE => replicate nvars NONE in map2 (fn b => fn FVars => map_filter I (map2 (mk_set (b::recs) FVars) tys xs)) vars FVars end; val bound_sets = mk_sets bounds [] NONE; - fun get_fs T = filter (fn t' => HOLogic.dest_setT (fastype_of (mk_imsupp t' T)) = T) fs; + fun get_fs T = filter (fn t' => case mk_imsupp_opt t' T of + NONE => false + | SOME t => HOLogic.dest_setT (fastype_of t) = T + ) fs; val imsupp_prems = maps (map_filter (fn t => case Term.subst_atomic_types replace t of (Const (@{const_name Set.insert}, _) $ (t as Free (_, T)) $ _) => (case get_fs T of [] => NONE - | xs => SOME (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_mem (t, foldl1 mk_Un (map (fn f => mk_imsupp f T) xs)))))) + | xs => SOME (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_mem (t, foldl1 mk_Un (map (fn f => the (mk_imsupp_opt f T)) xs)))))) | t => let val T = HOLogic.dest_setT (fastype_of t); in case get_fs T of [] => NONE - | xs => SOME (HOLogic.mk_Trueprop (mk_int_empty (t, foldl1 mk_Un (map (fn f => mk_imsupp f T) xs)))) + | xs => SOME (HOLogic.mk_Trueprop (mk_int_empty (t, foldl1 mk_Un (map (fn f => the (mk_imsupp_opt f T)) xs)))) end )) bound_sets; @@ -594,14 +603,16 @@ fun create_binder_datatype (spec : spec) lthy = val free_rec_vars = subtract (op=) (map (nth rec_vars) (flat (#binding_rel spec))) rec_vars; val free_sets = collect_sets (mk_sets frees free_rec_vars (SOME (#FVars quotient))); - val noclash_prems = map_filter (Option.map HOLogic.mk_Trueprop) (map2 (fn a => fn b => case (a, b) of - (SOME (Const (@{const_name Set.insert}, _) $ x $ _), SOME (Const (@{const_name Set.insert}, _) $ y $ _)) => - SOME (HOLogic.mk_not (HOLogic.mk_eq (x, y))) - | (SOME (Const (@{const_name Set.insert}, _) $ x $ _), SOME ys) => SOME (HOLogic.mk_not (HOLogic.mk_mem (x, ys))) - | (SOME xs, SOME (Const (@{const_name Set.insert}, _) $ y $ _)) => SOME (HOLogic.mk_not (HOLogic.mk_mem (y, xs))) - | (SOME free, SOME bound) => SOME (mk_int_empty (free, bound)) - | _ => NONE - ) bound_sets' free_sets); + val noclash_prems = if do_noclash then + map_filter (Option.map HOLogic.mk_Trueprop) (map2 (fn a => fn b => case (a, b) of + (SOME (Const (@{const_name Set.insert}, _) $ x $ _), SOME (Const (@{const_name Set.insert}, _) $ y $ _)) => + SOME (HOLogic.mk_not (HOLogic.mk_eq (x, y))) + | (SOME (Const (@{const_name Set.insert}, _) $ x $ _), SOME ys) => SOME (HOLogic.mk_not (HOLogic.mk_mem (x, ys))) + | (SOME xs, SOME (Const (@{const_name Set.insert}, _) $ y $ _)) => SOME (HOLogic.mk_not (HOLogic.mk_mem (y, xs))) + | (SOME free, SOME bound) => SOME (mk_int_empty (free, bound)) + | _ => NONE + ) bound_sets' free_sets) + else []; val rhs = if length ts = 1 andalso member (op=) frees (hd tys) andalso fastype_of (hd ts) = range_type (fastype_of quotient_ctor) @@ -609,7 +620,7 @@ fun create_binder_datatype (spec : spec) lthy = val goal = mk_Trueprop_eq ( mapx $ Term.list_comb (ctor, xs), rhs ); - in Goal.prove_sorry lthy (names (fs @ xs)) (prems @ imsupp_prems @ noclash_prems) goal (fn {context=ctxt, prems} => + in Goal.prove_sorry lthy (names (fs @ xs)) (flat (map2 (fn p => fn f => mk_extra_prems f @ [p]) prems prem_fs) @ imsupp_prems @ noclash_prems) goal (fn {context=ctxt, prems} => Local_Defs.unfold0_tac ctxt [ctor_def] THEN tac ctxt prems ) end ) ctors (#ctors spec) end; @@ -640,7 +651,27 @@ fun create_binder_datatype (spec : spec) lthy = K (Local_Defs.unfold0_tac ctxt @{thms id_def}), rtac ctxt refl ]; - in mk_map_simps lthy fs (SOME o MRBNF_Recursor.mk_supp_bound) (fn t => fn _ => mk_imsupp t) mapx tac end; + 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; + + val permute_simps = + let + val (fs, _) = lthy + |> mk_Frees "f" (map (fn a => a --> a) vars); + val Ts' = snd (dest_Type qT); + val mapx = Term.subst_atomic_types (Ts' ~~ vars) (#rename quotient); + fun tac ctxt prems = EVERY1 [ + rtac ctxt (trans OF [#rename_ctor (#inner quotient)]), + K (Local_Defs.unfold0_tac ctxt (thms @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf @ [ + MRBNF_Def.map_def_of_mrbnf pre_mrbnf, + #Abs_inverse (snd info) OF @{thms UNIV_I} + ])), + REPEAT_DETERM o resolve_tac ctxt prems, + K (Local_Defs.unfold0_tac ctxt @{thms id_apply}), + rtac ctxt refl + ]; + in mk_map_simps lthy false fs (SOME o MRBNF_Recursor.mk_supp_bound) (K (K NONE)) + (single o HOLogic.mk_Trueprop o mk_bij) bounds mapx tac + end; val cmin_UNIV = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); val Cinfinite_card = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_conj ( @@ -662,12 +693,12 @@ fun create_binder_datatype (spec : spec) lthy = domain_type (domain_type (fastype_of s)) = domain_type (fastype_of h) ) (#SSupps tvsubst_res)); fun mk_supp_bound h = Option.map (fn s => mk_ordLess (mk_card_of s) cmin_UNIV) (mk_supp h); - fun mk_imsupp h T = foldl1 mk_Un (map_filter (fn f => Option.map (fn t => t $ f) ( + fun mk_imsupp h T = SOME (foldl1 mk_Un (map_filter (fn f => Option.map (fn t => t $ f) ( List.find (fn s => domain_type (fastype_of s) = fastype_of h andalso domain_type (fastype_of s) = fastype_of f andalso HOLogic.dest_setT (range_type (fastype_of s)) = T ) (flat (#IImsuppss tvsubst_res)) - )) fs); + )) fs)); fun tac ctxt prems = EVERY1 [ K (Local_Defs.unfold0_tac ctxt (map (Thm.symmetric o snd) (#VVrs tvsubst_res))), EVERY' [ @@ -706,7 +737,7 @@ fun create_binder_datatype (spec : spec) lthy = rtac ctxt refl ] ]; - in mk_map_simps lthy fs mk_supp_bound mk_imsupp (#tvsubst tvsubst_res) tac end; + in mk_map_simps lthy true fs mk_supp_bound mk_imsupp (K []) [] (#tvsubst tvsubst_res) tac end; in (lthy, SOME (tvsubst_res, tvsubst_simps)) end else (lthy, NONE); @@ -716,6 +747,7 @@ fun create_binder_datatype (spec : spec) lthy = val sugar = { map_simps = map_simps, set_simpss = set_simpss, + permute_simps = permute_simps, strong_induct = strong_induct, subst_simps = Option.map snd tvsubst_opt, bsetss = bset_optss, @@ -733,6 +765,7 @@ fun create_binder_datatype (spec : spec) lthy = ("induct", [induct], [induct_attrib]), ("set", flat set_simpss, simp), ("map", map_simps, simp), + ("permute", permute_simps, simp), ("distinct", distinct, simp) ] @ the_default [] (Option.map (fn (_, tvsubst_simps) => [("subst", tvsubst_simps, simp)]) tvsubst_opt) ) |> (map (fn (thmN, thms, attrs) => From c248fc921aee25aa6a1d75a82297fbbc122cdd9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Fri, 18 Oct 2024 12:50:48 +0100 Subject: [PATCH 2/2] Remove manually defined simp rules for rrename --- thys/Infinitary_FOL/InfFOL.thy | 16 ++---------- thys/Infinitary_Lambda_Calculus/ILC.thy | 26 ++++++------------- .../ILC_UBeta_depth.thy | 2 +- .../Super_Recursor.thy | 4 +-- .../Translation_ILC_to_LC.thy | 6 ++--- .../Translation_LC_to_ILC.thy | 2 +- thys/Pi_Calculus/Commitment.thy | 4 +++ thys/Pi_Calculus/Pi.thy | 20 -------------- thys/STLC/STLC.thy | 10 ------- thys/Untyped_Lambda_Calculus/LC.thy | 24 +++++------------ 10 files changed, 28 insertions(+), 86 deletions(-) diff --git a/thys/Infinitary_FOL/InfFOL.thy b/thys/Infinitary_FOL/InfFOL.thy index 7573891b..c992c12b 100644 --- a/thys/Infinitary_FOL/InfFOL.thy +++ b/thys/Infinitary_FOL/InfFOL.thy @@ -199,20 +199,8 @@ apply (rule k1_Cinfinite) apply (rule kregular) done -lemma ifol'_rrename_simps[simp]: -fixes f::"'a::var_ifol'_pre \ 'a" -shows "bij f \ |supp f| rrename_ifol' f (Eq x1 x2) = Eq (f x1) (f x2)" - "bij f \ |supp f| rrename_ifol' f (Neg x) = Neg (rrename_ifol' f x)" - "bij f \ |supp f| rrename_ifol' f (Conj F) = Conj (map_set\<^sub>k\<^sub>1 (rrename_ifol' f) F)" - "bij f \ |supp f| rrename_ifol' f (All x3 x4) = All (map_set\<^sub>k\<^sub>2 f x3) (rrename_ifol' f x4)" - apply (auto simp: ifol'_vvsubst_rrename[symmetric])[3] - apply (unfold All_def ifol'.rrename_cctors map_ifol'_pre_def comp_def Abs_ifol'_pre_inverse[OF UNIV_I] - map_sum.simps map_prod_simp - ) - apply (rule refl) - done lemma rrename_Bot_simp[simp]: "bij (f::'a::var_ifol'_pre \ 'a) \ |supp f| rrename_ifol' f \ = \" - unfolding Bot_def ifol'_rrename_simps map_set\<^sub>k\<^sub>1_def map_fun_def comp_def Abs_set\<^sub>k\<^sub>1_inverse[OF UNIV_I] + unfolding Bot_def ifol'.permute map_set\<^sub>k\<^sub>1_def map_fun_def comp_def Abs_set\<^sub>k\<^sub>1_inverse[OF UNIV_I] unfolding id_def map_bset_bempty by (rule refl) @@ -381,7 +369,7 @@ binder_inductive deduct apply (assumption | rule bij_imp_bij_inv supp_inv_bound)+ apply (subst inv_o_simp1, assumption) apply (unfold ifol'.rrename_id0s set\<^sub>k.map_id) - apply (metis bij_imp_bij_inv ifol'.rrename_comps ifol'.rrename_ids ifol'_rrename_simps(3) in_k1_equiv' inv_o_simp1 supp_inv_bound) + apply (metis bij_imp_bij_inv ifol'.rrename_comps ifol'.rrename_ids ifol'.permute(3) in_k1_equiv' inv_o_simp1 supp_inv_bound) apply (metis ifol'.rrename_bijs ifol'.rrename_inv_simps inv_o_simp1 inv_simp1 set\<^sub>k.map_id) apply (metis ifol'.rrename_bijs ifol'.rrename_inv_simps inv_o_simp1 inv_simp1 set\<^sub>k.map_id) subgoal for f V diff --git a/thys/Infinitary_Lambda_Calculus/ILC.thy b/thys/Infinitary_Lambda_Calculus/ILC.thy index 4e902c01..f00b686c 100644 --- a/thys/Infinitary_Lambda_Calculus/ILC.thy +++ b/thys/Infinitary_Lambda_Calculus/ILC.thy @@ -234,16 +234,6 @@ lemma itvsubst_VVr_func[simp]: "itvsubst VVr t = t" done done -proposition irrename_simps[simp]: - assumes "bij (f::ivar \ ivar)" "|supp f| \. A" "\t \. P t", rule_format, no_vars] @@ -258,7 +248,7 @@ next case (iLam x1 x2) thm iterm.subst then show ?case using f g apply simp - by (metis iLam.hyps(4) irrename_simps(3) iterm.map_cong0 iterm_vvsubst_rrename) + by (metis iLam.hyps(4) iterm.permute(3) iterm.map_cong0 iterm_vvsubst_rrename) qed (auto simp: f g) lemma itvsubst_cong: @@ -396,7 +386,7 @@ lemma iLam_avoid: "|A::ivar set| \ lemma iLam_irrename: "bij (\::ivar\ivar) \ |supp \| (\a'. a' \ FFVars e - dsset (as::ivar dstream) \ \ a' = a') \ iLam as e = iLam (dsmap \ as) (irrename \ e)" -by (metis irrename_simps(3) iterm.rrename_cong_ids iterm.set(3)) +by (metis iterm.permute(3) iterm.rrename_cong_ids iterm.set(3)) (* Bound properties (needed as auxiliaries): *) @@ -510,14 +500,14 @@ using SSupp_irrename_bound s(1) s(2) by auto (* Action of swapping (a particular renaming) on variables *) lemma irrename_swap_Var1[simp]: "irrename (id(x := xx, xx := x)) (iVar (x::ivar)) = iVar xx" -apply(subst irrename_simps(1)) by auto +apply(subst iterm.permute(1)) by auto lemma irrename_swap_Var2[simp]: "irrename (id(x := xx, xx := x)) (iVar (xx::ivar)) = iVar x" -apply(subst irrename_simps(1)) by auto +apply(subst iterm.permute(1)) by auto lemma irrename_swap_Var3[simp]: "z \ {x,xx} \ irrename (id(x := xx, xx := x)) (iVar (z::ivar)) = iVar z" -apply(subst irrename_simps(1)) by auto +apply(subst iterm.permute(1)) by auto lemma irrename_swap_Var[simp]: "irrename (id(x := xx, xx := x)) (iVar (z::ivar)) = iVar (if z = x then xx else if z = xx then x else z)" -apply(subst irrename_simps(1)) by auto +apply(subst iterm.permute(1)) by auto (* Compositionality properties of renaming and term-for-variable substitution *) @@ -1359,7 +1349,7 @@ next show "R (irrename f (iApp e1 es2)) (renB f b)" unfolding b using 0 - using b12(1) b12(2) f(1) f(2) irrename_simps(2) renB_iAppB by auto + using b12(1) b12(2) f(1) f(2) iterm.permute(2) renB_iAppB by auto qed next case (iLam xs t) @@ -1560,7 +1550,7 @@ next subgoal by fact subgoal by fact . show "R (irrename f (iLam xs t)) (renB f b)" - unfolding 0 using RR apply(subst irrename_simps) + unfolding 0 using RR apply(subst iterm.permute) subgoal using f by auto subgoal using f by auto subgoal apply(subst renB_iLamB) using f b' by auto . qed diff --git a/thys/Infinitary_Lambda_Calculus/ILC_UBeta_depth.thy b/thys/Infinitary_Lambda_Calculus/ILC_UBeta_depth.thy index 89022ef5..af400c4e 100644 --- a/thys/Infinitary_Lambda_Calculus/ILC_UBeta_depth.thy +++ b/thys/Infinitary_Lambda_Calculus/ILC_UBeta_depth.thy @@ -189,7 +189,7 @@ unfolding G_def apply(elim disjE) apply(rule exI[of _ "smap (irrename \) es"]) apply(rule exI[of _ "smap (irrename \) es'"]) apply(cases t) unfolding isPerm_def small_def Tperm_def apply (simp add: iterm.rrename_comp0s stream.map_comp smap2_smap) - by (metis (no_types, lifting) comp_apply irrename_simps(3) presSuper_def stream.map_cong presBnd_presSuper) + by (metis (no_types, lifting) comp_apply iterm.permute(3) presSuper_def stream.map_cong presBnd_presSuper) . . . diff --git a/thys/Infinitary_Lambda_Calculus/Super_Recursor.thy b/thys/Infinitary_Lambda_Calculus/Super_Recursor.thy index a86faa41..f494f019 100644 --- a/thys/Infinitary_Lambda_Calculus/Super_Recursor.thy +++ b/thys/Infinitary_Lambda_Calculus/Super_Recursor.thy @@ -406,7 +406,7 @@ next show "R (irrename f (iApp e1 es2)) (renB f b)" unfolding b using 0 - using gd b12(1) b12(2) f irrename_simps(2) renB_iAppB by auto + using gd b12(1) b12(2) f iterm.permute(2) renB_iAppB by auto qed next case (iLam xs t) @@ -669,7 +669,7 @@ next subgoal using f(3) presSuper_def xs' by blast . show "R (irrename f (iLam xs t)) (renB f b)" - unfolding 0 using RR apply(subst irrename_simps) + unfolding 0 using RR apply(subst iterm.permute) subgoal using f by auto subgoal using f by auto subgoal apply(subst renB_iLamB) using xs' f b' by auto . qed diff --git a/thys/Infinitary_Lambda_Calculus/Translation_ILC_to_LC.thy b/thys/Infinitary_Lambda_Calculus/Translation_ILC_to_LC.thy index 1709b888..8166d963 100644 --- a/thys/Infinitary_Lambda_Calculus/Translation_ILC_to_LC.thy +++ b/thys/Infinitary_Lambda_Calculus/Translation_ILC_to_LC.thy @@ -115,7 +115,7 @@ unfolding renB_def FVarsB_def apply safe lemma renB_iVarB[simp]: "bij \ \ |supp \| bsmall (supp \) \ presSuper \ \ super xs \ x \ dsset xs \ renB \ (iVarB x) = iVarB (\ x)" -unfolding renB_def iVarB_def apply(subst rrename_simps) +unfolding renB_def iVarB_def apply(subst term.permute) subgoal by (auto simp add: bij_restr) subgoal by (auto simp add: card_supp_restr) subgoal unfolding restr_def apply(cases "theSN x", cases "theSN (\ x)") @@ -126,7 +126,7 @@ unfolding renB_def iVarB_def apply(subst rrename_simps) lemma renB_iAppB[simp]: "bij \ \ |supp \| bsmall (supp \) \ presSuper \ \ b1 \ B \ sset bs2 \ B \ renB \ (iAppB b1 bs2) = iAppB (renB \ b1) (smap (renB \) bs2)" -unfolding renB_def iAppB_def apply(subst rrename_simps) +unfolding renB_def iAppB_def apply(subst term.permute) subgoal by (auto simp add: bij_restr) subgoal by (auto simp add: card_supp_restr) subgoal by auto . @@ -134,7 +134,7 @@ unfolding renB_def iAppB_def apply(subst rrename_simps) lemma renB_iLamB[simp]: "bij \ \ |supp \| bsmall (supp \) \ presSuper \ \ b \ B \ super xs \ renB \ (iLamB xs b) = iLamB (dsmap \ xs) (renB \ b)" -unfolding renB_def iLamB_def apply(subst rrename_simps) +unfolding renB_def iLamB_def apply(subst term.permute) subgoal by (auto simp add: bij_restr) subgoal by (auto simp add: card_supp_restr) subgoal using restr_def superOf_subOf by auto . diff --git a/thys/Infinitary_Lambda_Calculus/Translation_LC_to_ILC.thy b/thys/Infinitary_Lambda_Calculus/Translation_LC_to_ILC.thy index 1bb2a3fe..17803c49 100644 --- a/thys/Infinitary_Lambda_Calculus/Translation_LC_to_ILC.thy +++ b/thys/Infinitary_Lambda_Calculus/Translation_LC_to_ILC.thy @@ -181,7 +181,7 @@ using bij_ext card_supp_ext by (auto simp: ext_dstnth_superOf) lemma renB_AppB: "bij \ \ |supp \| {b1,b2} \ B \ renB \ (AppB b1 b2) = AppB (renB \ b1) (renB \ b2)" unfolding renB_def AppB_def fun_eq_iff apply safe -apply(subst irrename_simps) +apply(subst iterm.permute) using bij_ext card_supp_ext by auto (metis (mono_tags, lifting) comp_apply stream.map_comp stream.map_cong) diff --git a/thys/Pi_Calculus/Commitment.thy b/thys/Pi_Calculus/Commitment.thy index e9fa6217..42d89a52 100644 --- a/thys/Pi_Calculus/Commitment.thy +++ b/thys/Pi_Calculus/Commitment.thy @@ -349,6 +349,10 @@ local_setup \MRBNF_Sugar.register_binder_sugar "Commitment.commit" { (@{term Binp}, @{thm Binp_def}), (@{term Cmt}, @{thm refl}) ], + permute_simps = @{thms + rrename_commit_Finp rrename_commit_Fout rrename_commit_Bout + rrename_commit_Binp rrename_commit_Tau + }, map_simps = [], distinct = [], bsetss = [[ diff --git a/thys/Pi_Calculus/Pi.thy b/thys/Pi_Calculus/Pi.thy index ac52e58f..ff765d46 100644 --- a/thys/Pi_Calculus/Pi.thy +++ b/thys/Pi_Calculus/Pi.thy @@ -75,26 +75,6 @@ proof- thus ?thesis by auto qed - - -(* *) -(* Properties of renaming (variable-for-variable substitution) *) - -proposition rrename_simps[simp]: - assumes "bij (f::var \ var)" "|supp f| z. (z::var) \ FFVars P \ f z = g z)" diff --git a/thys/STLC/STLC.thy b/thys/STLC/STLC.thy index 0c5e42b6..bef92a5f 100644 --- a/thys/STLC/STLC.thy +++ b/thys/STLC/STLC.thy @@ -75,16 +75,6 @@ corollary SSupp_upd_VVr_bound: "|SSupp_tvsubst (tvVVr_tvsubst(a:=(t::'a::var_ter lemma supp_subset_id_on: "supp f \ A \ id_on (B - A) f" unfolding supp_def id_on_def by blast -lemma rrename_simps[simp]: - assumes "bij (f::'a::var_terms_pre \ 'a)" "|supp f| e) = Abs (f x) \ (rrename_terms f e)" - unfolding Var_def App_def Abs_def terms.rrename_cctors[OF assms] map_terms_pre_def comp_def - Abs_terms_pre_inverse[OF UNIV_I] map_sum_def sum.case map_prod_def prod.case id_def - apply (rule refl)+ - done - lemma App_inject[simp]: "(App a b = App c d) = (a = c \ b = d)" proof assume "App a b = App c d" diff --git a/thys/Untyped_Lambda_Calculus/LC.thy b/thys/Untyped_Lambda_Calculus/LC.thy index 23ed87c7..ea7615e2 100644 --- a/thys/Untyped_Lambda_Calculus/LC.thy +++ b/thys/Untyped_Lambda_Calculus/LC.thy @@ -123,16 +123,6 @@ lemma tvsubst_VVr_func[simp]: "tvsubst VVr t = t" unfolding id_def[symmetric] term_pre.map_id apply (rule refl) done - done - -proposition rrename_simps[simp]: - assumes "bij (f::var \ var)" "|supp f| \x' lemma Lam_rrename: "bij (\::var\var) \ |supp \| (\a'. a' \FFVars_term e - {a::var} \ \ a' = a') \ Lam a e = Lam (\ a) (rrename \ e)" -by (metis rrename_simps(3) term.rrename_cong_ids term.set(3)) +by (metis term.permute(3) term.rrename_cong_ids term.set(3)) (* Bound properties (needed as auxiliaries): *) @@ -407,14 +397,14 @@ using IImsupp_rrename_update_bound[OF assms] (* Action of swapping (a particular renaming) on variables *) lemma rrename_swap_Var1[simp]: "rrename (id(x := xx, xx := x)) (Var (x::var)) = Var xx" -apply(subst rrename_simps(1)) by auto +apply(subst term.permute(1)) by auto lemma rrename_swap_Var2[simp]: "rrename (id(x := xx, xx := x)) (Var (xx::var)) = Var x" -apply(subst rrename_simps(1)) by auto +apply(subst term.permute(1)) by auto lemma rrename_swap_Var3[simp]: "z \ {x,xx} \ rrename (id(x := xx, xx := x)) (Var (z::var)) = Var z" -apply(subst rrename_simps(1)) by auto +apply(subst term.permute(1)) by auto lemma rrename_swap_Var[simp]: "rrename (id(x := xx, xx := x)) (Var (z::var)) = Var (if z = x then xx else if z = xx then x else z)" -apply(subst rrename_simps(1)) by auto +apply(subst term.permute(1)) by auto (* Compositionality properties of renaming and term-for-variable substitution *) @@ -1003,7 +993,7 @@ next R_B Un_iff bot.extremum insert_Diff insert_subset) subgoal apply(drule R_App_elim) by (smt (verit, del_insts) R.simps R_B bot.extremum insert_subset renB_AppB - rrename_simps(2)) . + term.permute(2)) . next case (Lam x t) note Lamm = Lam[rule_format] @@ -1162,7 +1152,7 @@ next subgoal by fact subgoal by fact . show "R (rrename f (Lam x t)) (renB f b)" - unfolding 0 using RR apply(subst rrename_simps) + unfolding 0 using RR apply(subst term.permute) subgoal using f by auto subgoal using f by auto subgoal apply(subst renB_LamB) using f b' by auto .