Automatically define simp rules for permute

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,22 +603,24 @@ 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)
             then hd ts else Term.list_comb (ctor, ts)
           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) =>

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 \<Rightarrow> 'a"
-shows  "bij f \<Longrightarrow> |supp f| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' f (Eq x1 x2) = Eq (f x1) (f x2)"
-  "bij f \<Longrightarrow> |supp f| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' f (Neg x) = Neg (rrename_ifol' f x)"
-  "bij f \<Longrightarrow> |supp f| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' f (Conj F) = Conj (map_set\<^sub>k\<^sub>1 (rrename_ifol' f) F)"
-  "bij f \<Longrightarrow> |supp f| <o |UNIV::'a set| \<Longrightarrow> 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 \<Rightarrow> 'a) \<Longrightarrow> |supp f| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' f \<bottom> = \<bottom>"
-  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

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 \<Rightarrow> ivar)" "|supp f| <o |UNIV::ivar set|"
-  shows "irrename f (iVar a) = iVar (f a)"
-    "irrename f (iApp e1 es2) = iApp (irrename f e1) (smap (irrename f) es2)"
-    "irrename f (iLam xs e) = iLam (dsmap f xs) (irrename f e)"
-  unfolding iVar_def iApp_def iLam_def iterm.rrename_cctors[OF assms] map_iterm_pre_def comp_def
-    Abs_iterm_pre_inverse[OF UNIV_I] map_sum_def sum.case map_prod_def prod.case id_def
-    apply (rule refl)+
-  done
-
 thm iterm.strong_induct[of "\<lambda>\<rho>. A" "\<lambda>t \<rho>. 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| <o |UNIV::ivar set| \<Longrightarrow> \<exists>
 lemma iLam_irrename:
 "bij (\<sigma>::ivar\<Rightarrow>ivar) \<Longrightarrow> |supp \<sigma>| <o |UNIV:: ivar set| \<Longrightarrow>
  (\<And>a'. a' \<in> FFVars e - dsset (as::ivar dstream) \<Longrightarrow> \<sigma> a' = a') \<Longrightarrow> iLam as e = iLam (dsmap \<sigma> as) (irrename \<sigma> 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 \<notin> {x,xx} \<Longrightarrow> 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

thys/Infinitary_Lambda_Calculus/ILC_UBeta_depth.thy

@@ -189,7 +189,7 @@ unfolding G_def apply(elim disjE)
   apply(rule exI[of _ "smap (irrename \<sigma>) es"]) apply(rule exI[of _ "smap (irrename \<sigma>) 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) 
    . . . 
 
 

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

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 \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::ivar set| \<Longrightarrow> bsmall (supp \<sigma>) \<Longrightarrow> presSuper \<sigma> \<Longrightarrow> 
   super xs \<Longrightarrow> x \<in> dsset xs \<Longrightarrow> 
   renB \<sigma> (iVarB x) = iVarB (\<sigma> 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 (\<sigma> x)") 
@@ -126,15 +126,15 @@ unfolding renB_def iVarB_def apply(subst rrename_simps)
 lemma renB_iAppB[simp]: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::ivar set| \<Longrightarrow> bsmall (supp \<sigma>) \<Longrightarrow> presSuper \<sigma> \<Longrightarrow> 
    b1 \<in> B \<Longrightarrow> sset bs2 \<subseteq> B \<Longrightarrow>
    renB \<sigma> (iAppB b1 bs2) = iAppB (renB \<sigma> b1) (smap (renB \<sigma>) 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 .
 
 lemma renB_iLamB[simp]: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::ivar set| \<Longrightarrow> bsmall (supp \<sigma>) \<Longrightarrow> presSuper \<sigma> \<Longrightarrow> 
    b \<in> B \<Longrightarrow> super xs \<Longrightarrow> 
    renB \<sigma> (iLamB xs b) = iLamB (dsmap \<sigma> xs) (renB \<sigma> 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 .

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 \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> {b1,b2} \<subseteq> B \<Longrightarrow> 
    renB \<sigma> (AppB b1 b2) = AppB (renB \<sigma> b1) (renB \<sigma> 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)
 

thys/Pi_Calculus/Commitment.thy

@@ -349,6 +349,10 @@ local_setup \<open>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 = [[

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 \<Rightarrow> var)" "|supp f| <o |UNIV::var set|"
-  shows "rrename_term f Zero = Zero"
-    "rrename_term f (Sum e1 e2) = Sum (rrename_term f e1) (rrename_term f e2)"
-    "rrename_term f (Par e1 e2) = Par (rrename_term f e1) (rrename_term f e2)"
-    "rrename_term f (Bang e) = Bang (rrename_term f e)"
-    "rrename_term f (Match x y e) = Match (f x) (f y) (rrename_term f e)"
-    "rrename_term f (Out x y e) = Out (f x) (f y) (rrename_term f e)"
-    "rrename_term f (Inp x y e) = Inp (f x) (f y) (rrename_term f e)"
-    "rrename_term f (Res x e) = Res (f x) (rrename_term f e)"
-  unfolding Zero_def Sum_def Par_def Bang_def Match_def Out_def Inp_def Res_def term.rrename_cctors[OF assms] map_term_pre_def comp_def
-    Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case map_prod_def prod.case id_def
-    apply (rule refl)+
-  done
-
 lemma rrename_cong:
 assumes "bij f" "|supp f| <o |UNIV::var set|" "bij g" "|supp g| <o |UNIV::var set|"
 "(\<And>z. (z::var) \<in> FFVars P \<Longrightarrow> f z = g z)"