src/HOL/Nominal/Examples/CR.thy

     hence "a\<sharp>s2" using i2 by simp
     thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact)
   qed
 qed
 
+lemma one_fresh_preserv_automatic:
+  fixes a :: "name"
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  and     b: "a\<sharp>t"
+  shows "a\<sharp>s"
+using a b
+apply(nominal_induct avoiding: a rule: One.strong_induct)
+apply(auto simp add: abs_fresh fresh_atm fresh_fact)
+done
+
 lemma subst_rename: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
 by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)

   assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
   using a
   apply -
   apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
-  apply(auto simp add: lam.distinct lam.inject alpha)
+  apply(auto simp add: lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   apply(rule conjI)
-  apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric])
-  apply(simp)
-  apply(rule pt_name3)
-  apply(rule at_ds5[OF at_name_inst])
-  apply(frule_tac a="a" in one_fresh_preserv)
-  apply(assumption)
-  apply(rule conjI)
-  apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
-  apply(simp add: calc_atm)
-  apply(force intro!: One.eqvt)
-  done
+  apply(perm_simp)
+  apply(simp add: fresh_left calc_atm)
+  apply(simp add: One.eqvt)
+  apply(simp add: one_fresh_preserv)
+done  
+
 
 lemma one_app: 
   assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
   shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)"