--- a/Nominal/Ex/Exec/Lambda_Exec.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Ex/Exec/Lambda_Exec.thy	Thu May 24 10:17:32 2012 +0200
@@ -458,10 +458,6 @@
 value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))"
 value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*)
 
-lemma [eqvt]:
-  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-  unfolding Let_def permute_fun_app_eq ..
-
 end
 
 

--- a/Nominal/Ex/SFT/Consts.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Ex/SFT/Consts.thy	Thu May 24 10:17:32 2012 +0200
@@ -285,10 +285,10 @@
   apply (rule lam2_fast_app, rule Lam_A, simp_all)
   done
 
-definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
+definition "NUM \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
 
-lemma supp_Num[simp]:
-  "supp Num = {}"
-  by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
+lemma supp_NUM[simp]:
+  "supp NUM = {}"
+  by (auto simp only: NUM_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
 
 end

--- a/Nominal/Ex/SFT/Theorem.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Ex/SFT/Theorem.thy	Thu May 24 10:17:32 2012 +0200
@@ -1,15 +1,15 @@
-header {* The main lemma about Num and the Second Fixed Point Theorem *}
+header {* The main lemma about NUM and the Second Fixed Point Theorem *}
 
 theory Theorem imports Consts begin
 
-lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6
+lemmas [simp] = b3[OF bI] b1 b4 b5 supp_NUM[unfolded NUM_def supp_ltgt] NUM_def lam.fresh[unfolded fresh_def] fresh_def b6
 lemmas app = Ltgt1_app
 
-lemma Num:
-  shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
+lemma NUM:
+  shows "NUM \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
 proof (induct M rule: lam.induct)
   case (Var n)
-  have "Num \<cdot> \<lbrace>Var n\<rbrace> = Num \<cdot> (VAR \<cdot> Var n)" by simp
+  have "NUM \<cdot> \<lbrace>Var n\<rbrace> = NUM \<cdot> (VAR \<cdot> Var n)" by simp
   also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (VAR \<cdot> Var n)" by simp
   also have "... \<approx> VAR \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
   also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using VAR_app .
@@ -17,50 +17,50 @@
   also have "... \<approx> F1 \<cdot> Var n" using A_app(1) .
   also have "... \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var n)" using F_app(1) .
   also have "... = \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>" by simp
-  finally show "Num \<cdot> \<lbrace>Var n\<rbrace> \<approx> \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>".
+  finally show "NUM \<cdot> \<lbrace>Var n\<rbrace> \<approx> \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>".
 next
   case (App M N)
-  assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>"
-  have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
+  assume IH: "NUM \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "NUM \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>"
+  have "NUM \<cdot> \<lbrace>M \<cdot> N\<rbrace> = NUM \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
   also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
   also have "... \<approx> APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
   also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using APP_app .
   also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
-  also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp
-  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .
-  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp
+  also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> NUM" using A_app(2) by simp
+  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (NUM \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (NUM \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .
+  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (NUM \<cdot> \<lbrace>N\<rbrace>)" using IH by simp
   also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp
-  finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>".
+  finally show "NUM \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>".
 next
   case (Lam x P)
-  assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>"
-  have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
+  assume IH: "NUM \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>"
+  have "NUM \<cdot> \<lbrace>\<integral> x. P\<rbrace> = NUM \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
   also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
   also have "... \<approx> Abs \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
   also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 0 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Abs_app .
   also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
   also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) .
-  also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp
-  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Var x)))" by (rule F3_app) simp_all
-  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp
+  also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> NUM" by simp
+  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (NUM \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Var x)))" by (rule F3_app) simp_all
+  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (NUM \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp
   also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp
   also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp
-  finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" .
+  finally show "NUM \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" .
 qed
 
-lemmas [simp] = Ap Num
-lemmas [simp del] = fresh_def Num_def
+lemmas [simp] = Ap NUM
+lemmas [simp del] = fresh_def NUM_def
 
 theorem SFP:
   fixes F :: lam
   shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"
 proof -
   obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
-  def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))"
+  def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (NUM \<cdot> Var x)))"
   def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"
   have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..
-  also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..
-  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp
+  also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (NUM \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..
+  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (NUM \<cdot> \<lbrace>W\<rbrace>))" by simp
   also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp
   also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp
   also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..

--- a/Nominal/GPerm.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/GPerm.thy	Thu May 24 10:17:32 2012 +0200
@@ -36,12 +36,12 @@
   by (metis valid_perm_def image_set length_map len_set_eq_distinct)
 
 definition
-  perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool" (infix "\<approx>" 50)
+  perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool"
 where
-  "x \<approx> y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)"
+  "perm_eq x y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)"
 
 lemma perm_eq_sym[sym]:
-  "x \<approx> y \<Longrightarrow> y \<approx> x"
+  "perm_eq x y \<Longrightarrow> perm_eq y x"
   by (auto simp add: perm_eq_def)
 
 lemma perm_eq_equivp:
@@ -159,7 +159,7 @@
   by (metis uminus_perm_raw_def)
 
 lemma uminus_perm_raw_rsp[simp]:
-  "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"
+  "perm_eq x y \<Longrightarrow> perm_eq (map swap_pair x) (map swap_pair y)"
   by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
 lemma fst_snd_map_pair[simp]:
@@ -233,11 +233,11 @@
   done
 
 lemma perm_add_raw_rsp[simp]:
-  "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"
+  "perm_eq x y \<Longrightarrow> perm_eq xa ya \<Longrightarrow> perm_eq (perm_add_raw x xa) (perm_add_raw y ya)"
   by (simp add: fun_eq_iff perm_add_apply perm_eq_def)
 
 lemma [simp]:
-  "a \<approx> a \<longleftrightarrow> valid_perm a"
+  "perm_eq a a \<longleftrightarrow> valid_perm a"
   by (simp_all add: perm_eq_def)
 
 instantiation gperm :: (type) group_add
@@ -276,7 +276,7 @@
   by (induct y) (auto split: if_splits)
 
 lemma perm_eq_not_eq_same:
-  "x \<approx> y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}"
+  "perm_eq x y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}"
   unfolding perm_eq_def set_eq_iff
   apply auto
   apply (subgoal_tac "perm_apply x a = b")
@@ -315,7 +315,7 @@
   by (metis in_set_in_dpr2 pair_perm_apply perm_apply_in_set valid_perm_def)
 
 lemma dest_perm_raw_eq[simp]:
-  "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = (x \<approx> y)"
+  "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = perm_eq x y"
   apply (auto simp add: perm_eq_def)
   apply (metis in_set_in_dpr3 fun_eq_iff)
   unfolding dest_perm_raw_def
@@ -371,8 +371,8 @@
   by simp (rule sorted_sort_id[OF sorted_sort])
 
 lemma valid_dest_perm_raw_eq[simp]:
-  "valid_perm p \<Longrightarrow> dest_perm_raw p \<approx> p"
-  "valid_perm p \<Longrightarrow> p \<approx> dest_perm_raw p"
+  "valid_perm p \<Longrightarrow> perm_eq (dest_perm_raw p) p"
+  "valid_perm p \<Longrightarrow> perm_eq p (dest_perm_raw p)"
   by (simp_all add: dest_perm_raw_eq[symmetric])
 
 lemma mk_perm_dest_perm[code abstype]:

--- a/Nominal/Nominal2_Base.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu May 24 10:17:32 2012 +0200
@@ -1093,6 +1093,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 *}
 

--- 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)