--- a/Nominal/Nominal2_Base_Exec.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Nominal2_Base_Exec.thy	Thu May 24 10:17:32 2012 +0200
@@ -110,20 +110,15 @@
 lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is
   "\<lambda>p. if sort_respecting p then p else 0" by simp
 
-(*lemma sort_respecting_Rep_perm [simp, intro]:
-  "sort_respecting (Rep_perm p)"
-  using Rep_perm [of p] by simp*)
-
 lemma Rep_perm_mk_perm [simp]:
   "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)"
   by (simp add: mk_perm_def Abs_perm_inverse)
 
-(*lemma mk_perm_Rep_perm [simp, code abstype]:
-  "mk_perm (Rep_perm dxs) = dxs"
-  by (simp add: mk_perm_def Rep_perm_inverse)*)
-
 instance perm :: size ..
 
+
+subsection {* Permutations form a (multiplicative) group *}
+
 instantiation perm :: group_add
 begin
 
@@ -158,6 +153,9 @@
 
 end
 
+
+section {* Implementation of swappings *}
+
 lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm"  ("'(_ \<rightleftharpoons> _')")
   is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" .
 
@@ -1013,6 +1011,9 @@
 unfolding finite_def
 by (perm_simp) (rule refl)
 
+lemma Let_eqvt [eqvt]:
+  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
 
 subsubsection {* Equivariance for product operations *}
 
@@ -2721,6 +2722,40 @@
   shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b"
   by (simp add: fresh_star_def fresh_atom_at_base)
 
+lemma if_fresh_at_base [simp]:
+  shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s"
+  and   "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s"
+by (simp_all add: fresh_at_base)
+
+simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>
+  let
+    fun first_is_neg lhs rhs [] = NONE
+      | first_is_neg lhs rhs (thm::thms) =
+          (case Thm.prop_of thm of
+             _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) =>
+               (if l = lhs andalso r = rhs then SOME(thm)
+                else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym})
+                else NONE)
+           | _ => first_is_neg lhs rhs thms)
+
+    val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
+    val prems = Simplifier.prems_of ss
+      |> filter (fn thm => case Thm.prop_of thm of
+           _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false)
+      |> map (simplify (HOL_basic_ss addsimps simp_thms))
+      |> map HOLogic.conj_elims
+      |> flat
+  in
+    case term_of ctrm of
+      @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) =>
+         (case first_is_neg lhs rhs prems of
+            SOME(thm) => SOME(thm RS @{thm Eq_TrueI})
+          | NONE => NONE)
+    | _ => NONE
+  end
+*}
+
+
 instance at_base < fs
 proof qed (simp add: supp_at_base)