diff -r 5f3387b7474f -r 8e0f0b2b51dd Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed May 04 15:27:04 2011 +0800
+++ b/Nominal/Nominal2_Base.thy	Mon May 09 04:46:43 2011 +0100
@@ -761,7 +761,7 @@
   unfolding permute_perm_def by simp
 
 (* the normal version of this lemma would cause loops *)
-lemma permute_eqvt_raw[eqvt_raw]:
+lemma permute_eqvt_raw [eqvt_raw]:
   shows "p \<bullet> permute \<equiv> permute"
 apply(simp add: fun_eq_iff permute_fun_def)
 apply(subst permute_eqvt)
@@ -827,26 +827,6 @@
   unfolding Ex1_def
   by (perm_simp) (rule refl)
 
-lemma mem_eqvt [eqvt]:
-  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (simp add: permute_fun_app_eq)
-
-lemma Collect_eqvt [eqvt]:
-  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
-  unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt [eqvt]:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def
-  by (perm_simp) (rule refl)
-
-lemma image_eqvt [eqvt]:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
 lemma if_eqvt [eqvt]:
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
@@ -897,7 +877,21 @@
   apply(rule theI'[OF unique])
   done
 
-subsubsection {* Equivariance set operations *}
+subsubsection {* Equivariance of Set operators *}
+
+lemma mem_eqvt [eqvt]:
+  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+  unfolding mem_def
+  by (rule permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+  unfolding Collect_def permute_fun_def ..
+
+lemma inter_eqvt [eqvt]:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def
+  by (perm_simp) (rule refl)
 
 lemma Bex_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
@@ -909,6 +903,11 @@
   unfolding Ball_def
   by (perm_simp) (rule refl)
 
+lemma image_eqvt [eqvt]:
+  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+  unfolding image_def
+  by (perm_simp) (rule refl)
+
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def
@@ -965,12 +964,12 @@
 subsubsection {* Equivariance for product operations *}
 
 lemma fst_eqvt [eqvt]:
-  "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
+  shows "p \<bullet> (fst x) = fst (p \<bullet> x)"
+  by (cases x) simp
 
 lemma snd_eqvt [eqvt]:
-  "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
+  shows "p \<bullet> (snd x) = snd (p \<bullet> x)"
+  by (cases x) simp
 
 lemma split_eqvt [eqvt]: 
   shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
@@ -1025,7 +1024,7 @@
 
 lemma union_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
+  by (induct S) (simp_all)
 
 lemma map_fset_eqvt [eqvt]: 
   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
@@ -1336,7 +1335,7 @@
 lemma plus_perm_eq:
   fixes p q::"perm"
   assumes asm: "supp p \<inter> supp q = {}"
-  shows "p + q  = q + p"
+  shows "p + q = q + p"
 unfolding perm_eq_iff
 proof
   fix a::"atom"
@@ -1419,7 +1418,7 @@
 
 instance prod :: (fs, fs) fs
 apply default
-apply (induct_tac x)
+apply (case_tac x)
 apply (simp add: supp_Pair finite_supp)
 done
 
@@ -1444,7 +1443,7 @@
 
 instance sum :: (fs, fs) fs
 apply default
-apply (induct_tac x)
+apply (case_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 done
 
@@ -1480,22 +1479,22 @@
   shows "supp [] = {}"
   by (simp add: supp_def)
 
+lemma fresh_Nil: 
+  shows "a \<sharp> []"
+  by (simp add: fresh_def supp_Nil)
+
 lemma supp_Cons: 
   shows "supp (x # xs) = supp x \<union> supp xs"
 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
+lemma fresh_Cons: 
+  shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
+  by (simp add: fresh_def supp_Cons)
+
 lemma supp_append:
   shows "supp (xs @ ys) = supp xs \<union> supp ys"
   by (induct xs) (auto simp add: supp_Nil supp_Cons)
 
-lemma fresh_Nil: 
-  shows "a \<sharp> []"
-  by (simp add: fresh_def supp_Nil)
-
-lemma fresh_Cons: 
-  shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
-  by (simp add: fresh_def supp_Cons)
-
 lemma fresh_append:
   shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
@@ -1540,7 +1539,7 @@
   using assms
   unfolding fresh_conv_MOST
   unfolding permute_fun_app_eq
-  by (elim MOST_rev_mp, simp)
+  by (elim MOST_rev_mp) (simp)
 
 lemma supp_fun_app:
   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
@@ -1554,13 +1553,11 @@
 definition
   "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 
-
 text {* equivariance of a function at a given argument *}
 
 definition
  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
 
-
 lemma eqvtI:
   shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
 unfolding eqvt_def
@@ -2031,6 +2028,19 @@
 
 section {* Induction principle for permutations *}
 
+lemma smaller_supp:
+  assumes a: "a \<in> supp p"
+  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)
+  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
+  ultimately 
+  show "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" by auto
+qed
+  
 
 lemma perm_struct_induct[consumes 1, case_names zero swap]:
   assumes S: "supp p \<subseteq> S"
@@ -2054,11 +2064,7 @@
       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)
       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
-      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
-      moreover
-      have "a \<notin> supp ?q" by (simp add: supp_perm)
-      then have "supp ?q \<noteq> supp p" using a0 by auto
-      ultimately have "supp ?q \<subset> supp p" using a2 by auto
+      have a2: "supp ?q \<subset> supp p" using a0 smaller_supp by simp
       then have "P ?q" using ih by simp
       moreover
       have "supp ?q \<subseteq> S" using as a2 by simp
@@ -2139,6 +2145,7 @@
   qed
 qed
 
+text {* same lemma as above, but proved with a different induction principle *}
 lemma supp_perm_eq_test:
   assumes "(supp x) \<sharp>* p"
   shows "p \<bullet> x = x"
@@ -2163,8 +2170,24 @@
 lemma perm_supp_eq:
   assumes a: "(supp p) \<sharp>* x"
   shows "p \<bullet> x = x"
-by (rule supp_perm_eq)
-   (simp add: fresh_star_supp_conv a)
+proof -
+  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> x = x"
+  proof (induct p rule: perm_struct_induct2)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap a b)
+    then have "a \<sharp> x" "b \<sharp> x" by simp_all
+    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  next
+    case (plus p1 p2)
+    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
+    then show "(p1 + p2) \<bullet> x = x" by simp
+  qed
+qed
+
 
 lemma supp_perm_perm_eq:
   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
@@ -2562,7 +2585,7 @@
   apply(simp)
   done
 
-lemma fresh_at_base_permute_iff[simp]:
+lemma fresh_at_base_permute_iff [simp]:
   fixes a::"'a::at_base"
   shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
   unfolding atom_eqvt[symmetric]