diff -r 8c53bcd5c0ae -r c9a1c6f50ff5 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Aug 30 14:35:37 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Sep 06 10:06:41 2013 +0100
@@ -212,7 +212,7 @@
 unfolding swap_def
 apply (rule Abs_perm_inverse)
 apply (rule permI)
-apply (auto simp add: bij_def inj_on_def surj_def)[1]
+apply (auto simp: bij_def inj_on_def surj_def)[1]
 apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]])
 apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]])
 apply (simp)
@@ -254,7 +254,7 @@
   shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)"
   using assms
   by (rule_tac Rep_perm_ext)
-     (auto simp add: Rep_perm_simps fun_eq_iff)
+     (auto simp: Rep_perm_simps fun_eq_iff)
 
 
 section {* Permutation Types *}
@@ -439,7 +439,7 @@
 
 instance
 apply default
-apply (auto simp add: permute_set_def)
+apply (auto simp: permute_set_def)
 done
 
 end
@@ -467,25 +467,25 @@
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
   unfolding permute_set_def
-  using a by (auto simp add: swap_atom)
+  using a by (auto simp: swap_atom)
 
 lemma swap_set_in:
   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
   shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
   unfolding permute_set_def
-  using a by (auto simp add: swap_atom)
+  using a by (auto simp: swap_atom)
 
 lemma swap_set_in_eq:
   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
   shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
   unfolding permute_set_def
-  using a by (auto simp add: swap_atom)
+  using a by (auto simp: swap_atom)
 
 lemma swap_set_both_in:
   assumes a: "a \<in> S" "b \<in> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
   unfolding permute_set_def
-  using a by (auto simp add: swap_atom)
+  using a by (auto simp: swap_atom)
 
 lemma mem_permute_iff:
   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
@@ -864,7 +864,7 @@
 lemma swap_eqvt [eqvt]:
   shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
   unfolding permute_perm_def
-  by (auto simp add: swap_atom perm_eq_iff)
+  by (auto simp: swap_atom perm_eq_iff)
 
 lemma uminus_eqvt [eqvt]:
   fixes p q::"perm"
@@ -969,7 +969,7 @@
 lemma Collect_eqvt [eqvt]:
   shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
   unfolding permute_set_eq permute_fun_def
-  by (auto simp add: permute_bool_def)
+  by (auto simp: permute_bool_def)
 
 lemma inter_eqvt [eqvt]:
   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
@@ -1501,7 +1501,7 @@
 apply (rule supports_perm)
 apply (rule finite_perm_lemma)
 apply (simp add: perm_swap_eq swap_eqvt)
-apply (auto simp add: perm_eq_iff swap_atom)
+apply (auto simp: perm_eq_iff swap_atom)
 done
 
 lemma fresh_perm: 
@@ -1511,7 +1511,7 @@
 
 lemma supp_swap:
   shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})"
-  by (auto simp add: supp_perm swap_atom)
+  by (auto simp: supp_perm swap_atom)
 
 lemma fresh_swap:
   shows "a \<sharp> (b \<rightleftharpoons> c) \<longleftrightarrow> (sort_of b \<noteq> sort_of c) \<or> b = c \<or> (a \<sharp> b \<and> a \<sharp> c)"
@@ -1531,12 +1531,12 @@
   shows "a \<sharp> (p + q)"
   using assms
   unfolding fresh_def
-  by (auto simp add: supp_perm)
+  by (auto simp: supp_perm)
 
 lemma supp_plus_perm:
   fixes p q::perm
   shows "supp (p + q) \<subseteq> supp p \<union> supp q"
-  by (auto simp add: supp_perm)
+  by (auto simp: supp_perm)
 
 lemma fresh_minus_perm:
   fixes p::perm
@@ -1725,7 +1725,7 @@
 
 lemma supp_append:
   shows "supp (xs @ ys) = supp xs \<union> supp ys"
-  by (induct xs) (auto simp add: supp_Nil supp_Cons)
+  by (induct xs) (auto simp: supp_Nil supp_Cons)
 
 lemma fresh_append:
   shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
@@ -1733,17 +1733,17 @@
 
 lemma supp_rev:
   shows "supp (rev xs) = supp xs"
-  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+  by (induct xs) (auto simp: supp_append supp_Cons supp_Nil)
 
 lemma fresh_rev:
   shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
-  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+  by (induct xs) (auto simp: fresh_append fresh_Cons fresh_Nil)
 
 lemma supp_removeAll:
   fixes x::"atom"
   shows "supp (removeAll x xs) = supp xs - {x}"
   by (induct xs)
-     (auto simp add: supp_Nil supp_Cons supp_atom)
+     (auto simp: supp_Nil supp_Cons supp_atom)
 
 lemma supp_of_atom_list:
   fixes as::"atom list"
@@ -2011,7 +2011,7 @@
   assumes "finite S"
   shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)"
   unfolding fresh_def
-  by (auto simp add: supp_finite_atom_set assms)
+  by (auto simp: supp_finite_atom_set assms)
 
 lemma Union_supports_set:
   shows "(\<Union>x \<in> S. supp x) supports S"
@@ -2029,7 +2029,7 @@
   fixes S::"('a::fs set)"
   assumes fin: "finite S"   
   shows "finite (\<Union>x\<in>S. supp x)"
-  using fin by (induct) (auto simp add: finite_supp)
+  using fin by (induct) (auto simp: finite_supp)
 
 lemma Union_included_in_supp:
   fixes S::"('a::fs set)"
@@ -2189,7 +2189,7 @@
 lemma supp_of_multiset_union:
   fixes M N::"('a::fs) multiset"
   shows "supp (M + N) = supp M \<union> supp N"
-  by (auto simp add: supp_of_multisets)
+  by (auto simp: supp_of_multisets)
 
 lemma supp_empty_mset [simp]:
   shows "supp {#} = {}"
@@ -2274,7 +2274,7 @@
 lemma supp_finfun_update:
   shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)"
 using fresh_finfun_update
-by (auto simp add: fresh_def supp_Pair)
+by (auto simp: fresh_def supp_Pair)
     
 instance finfun :: (fs, fs) fs
   apply(default)
@@ -2326,7 +2326,7 @@
 
 lemma fresh_star_supp_conv:
   shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
-by (auto simp add: fresh_star_def fresh_def)
+by (auto simp: fresh_star_def fresh_def)
 
 lemma fresh_star_perm_set_conv:
   fixes p::"perm"
@@ -2343,25 +2343,25 @@
   shows "bs \<sharp>* as"
 using fresh
 unfolding fresh_star_def fresh_def
-by (auto simp add: supp_finite_atom_set fin)
+by (auto simp: supp_finite_atom_set fin)
 
 lemma atom_fresh_star_disjoint:
   assumes fin: "finite bs" 
   shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})"
 
 unfolding fresh_star_def fresh_def
-by (auto simp add: supp_finite_atom_set fin)
+by (auto simp: supp_finite_atom_set fin)
 
 
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
-  by (auto simp add: fresh_star_def fresh_Pair)
+  by (auto simp: fresh_star_def fresh_Pair)
 
 lemma fresh_star_list:
   shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
   and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
   and   "as \<sharp>* []"
-by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
+by (auto simp: fresh_star_def fresh_Nil fresh_Cons fresh_append)
 
 lemma fresh_star_set:
   fixes xs::"('a::fs) list"
@@ -2381,11 +2381,11 @@
 
 lemma fresh_star_Un:
   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
-  by (auto simp add: fresh_star_def)
+  by (auto simp: fresh_star_def)
 
 lemma fresh_star_insert:
   shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
-  by (auto simp add: fresh_star_def)
+  by (auto simp: fresh_star_def)
 
 lemma fresh_star_Un_elim:
   "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
@@ -2440,7 +2440,7 @@
   shows "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p"
 proof -
   have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subseteq> supp p"
-    unfolding supp_perm by (auto simp add: swap_atom)
+    unfolding supp_perm by (auto simp: swap_atom)
   moreover
   have "a \<notin> supp ((p \<bullet> a \<rightleftharpoons> a) + p)" by (simp add: supp_perm)
   then have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<noteq> supp p" using a by auto
@@ -2469,7 +2469,7 @@
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
       then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
-        using as by (auto simp add: supp_atom supp_perm swap_atom)
+        using as by (auto simp: supp_atom supp_perm swap_atom)
       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
       have a2: "supp ?q \<subset> supp p" using a0 smaller_supp by simp
       then have "P ?q" using ih by simp
@@ -2517,7 +2517,7 @@
     then have "p = 0"
       by (induct p rule: perm_struct_induct) (simp_all)
   }
-  then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp add: supp_zero_perm)
+  then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp: supp_zero_perm)
 qed
 
 lemma supp_perm_pair:
@@ -2527,12 +2527,12 @@
   { assume "supp p \<subseteq> {a, b}"
     then have "p = 0 \<or> p = (b \<rightleftharpoons> a)"
       apply (induct p rule: perm_struct_induct) 
-      apply (auto simp add: swap_cancel supp_zero_perm supp_swap)
+      apply (auto simp: swap_cancel supp_zero_perm supp_swap)
       apply (simp add: swap_commute)
       done
   }
   then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" 
-    by (auto simp add: supp_zero_perm supp_swap split: if_splits)
+    by (auto simp: supp_zero_perm supp_swap split: if_splits)
 qed
 
 lemma supp_perm_eq:
@@ -2679,7 +2679,7 @@
     hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "y \<notin> supp p" "sort_of y = sort_of x"
       by simp_all
     hence py: "p \<bullet> y = y" "x \<noteq> y" using `x \<in> As`
-      by (auto simp add: supp_perm)
+      by (auto simp: supp_perm)
     let ?q = "(x \<rightleftharpoons> y) + p"
     have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
       unfolding insert_eqvt
@@ -2728,7 +2728,7 @@
 apply(rule_tac x="p" in exI)
 apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
-apply(auto simp add: fresh_star_def)
+apply(auto simp: fresh_star_def)
 done
 
 lemma at_set_avoiding3:
@@ -2742,7 +2742,7 @@
 apply(rule_tac x="p" in exI)
 apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
-apply(auto simp add: fresh_star_def)
+apply(auto simp: fresh_star_def)
 done
 
 lemma at_set_avoiding2_atom:
@@ -2781,7 +2781,7 @@
     have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp
     moreover 
     have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
-      using ** by (auto simp add: insert_eqvt)
+      using ** by (auto simp: insert_eqvt)
     ultimately 
     have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
   }
@@ -2789,11 +2789,11 @@
   { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
     have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def
-      by (auto simp add: swap_atom)
+      by (auto simp: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
 	using ** 
-	apply (auto simp add: supp_perm insert_eqvt)
+	apply (auto simp: supp_perm insert_eqvt)
 	apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
 	apply(auto)[1]
 	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
@@ -2804,7 +2804,7 @@
         unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
-	using ** by (auto simp add: insert_eqvt)
+	using ** by (auto simp: insert_eqvt)
       ultimately 
       have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
         unfolding q'_def using supp_plus_perm by blast
@@ -2823,7 +2823,7 @@
   then obtain q 
     where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))"
     using set_renaming_perm by blast
-  from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp add: inter_eqvt)
+  from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp: inter_eqvt)
   moreover
   have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" 
     apply(auto)
@@ -2850,7 +2850,7 @@
     have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
     then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp 
     moreover 
-    have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
+    have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp: insert_eqvt)
     ultimately 
     have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
   }
@@ -2858,11 +2858,11 @@
   { assume 2: "a \<notin> set bs"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
     have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" 
-      unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom)
+      unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
 	using **
-	apply (auto simp add: supp_perm insert_eqvt)
+	apply (auto simp: supp_perm insert_eqvt)
 	apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
 	apply(auto)[1]
 	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
@@ -2873,7 +2873,7 @@
         unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
-	using ** by (auto simp add: insert_eqvt)
+	using ** by (auto simp: insert_eqvt)
       ultimately 
       have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
         unfolding q'_def using supp_plus_perm by blast
@@ -2950,31 +2950,39 @@
 
 
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
-  let
-    fun first_is_neg lhs rhs [] = NONE
-      | first_is_neg lhs rhs (thm::thms) =
+  case term_of ctrm of @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) =>
+    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 first_is_neg lhs rhs thms)  
-           | _ => first_is_neg lhs rhs thms)
-
-    val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
-    val prems = Simplifier.prems_of ctxt
-      |> filter (fn thm => case Thm.prop_of thm of                    
-           _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false)
-      |> map (simplify (put_simpset HOL_basic_ss  ctxt 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
+        | _ => first_is_neg lhs rhs thms)
+
+      val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
+      val prems = Simplifier.prems_of ctxt
+         |> filter (fn thm => case Thm.prop_of thm of                    
+            _ $ (Const (@{const_name fresh}, ty) $ (_ $ a) $ b) => 
+            (let 
+               val atms = a :: HOLogic.strip_tuple b
+             in
+               member (op=) atms lhs andalso member (op=) atms rhs
+             end) 
+            | _ => false)
+         |> map (simplify (put_simpset HOL_basic_ss  ctxt addsimps simp_thms))
+         |> map HOLogic.conj_elims
+         |> flat
+
+       
+    in 
+      case first_is_neg lhs rhs prems of
+        SOME(thm) => SOME(thm RS @{thm Eq_TrueI})
+      | NONE => NONE
+    end
+  | _ => NONE
 *}
 
 
@@ -3025,12 +3033,12 @@
   assumes fin: "finite (supp x)"
   obtains a::"'a::at_base" where "atom a \<sharp> x"
 using obtain_at_base[where X="supp x"]
-by (auto simp add: fresh_def fin)
+by (auto simp: fresh_def fin)
 
 lemma obtain_fresh:
   fixes x::"'b::fs"
   obtains a::"'a::at_base" where "atom a \<sharp> x"
-  by (rule obtain_fresh') (auto simp add: finite_supp)
+  by (rule obtain_fresh') (auto simp: finite_supp)
 
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
@@ -3266,7 +3274,7 @@
   shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
 proof -
   from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
-    by (auto simp add: fresh_Pair)
+    by (auto simp: fresh_Pair)
   show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
   proof (intro exI allI impI)
     fix a :: 'a
@@ -3306,7 +3314,7 @@
   assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
   assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
   from a x y show "x = y" 
-    by (auto simp add: fresh_Pair)
+    by (auto simp: fresh_Pair)
 qed
 
 text {* packaging the freshness lemma into a function *}
@@ -3341,7 +3349,7 @@
   assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
   shows "Fresh h = h a"
   apply (rule Fresh_apply)
-  apply (auto simp add: fresh_Pair intro: a)
+  apply (auto simp: fresh_Pair intro: a)
   done
 
 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm =>