diff -r c7cdea70eacd -r 869d1183e082 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Sun Apr 18 18:01:22 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Mon Apr 19 09:25:31 2010 +0200
@@ -212,8 +212,8 @@
 
 lemma swap_cancel:
   "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
-by (rule Rep_perm_ext) 
-   (simp add: Rep_perm_simps expand_fun_eq)
+  by (rule Rep_perm_ext) 
+     (simp add: Rep_perm_simps expand_fun_eq)
 
 lemma swap_self [simp]:
   "(a \<rightleftharpoons> a) = 0"
@@ -302,7 +302,7 @@
 begin
 
 definition
-  "p \<bullet> a = Rep_perm p a"
+  "p \<bullet> a = (Rep_perm p) a"
 
 instance 
 apply(default)
@@ -351,8 +351,10 @@
 
 end
 
-lemma permute_self: "p \<bullet> p = p"
-unfolding permute_perm_def by (simp add: diff_minus add_assoc)
+lemma permute_self: 
+  shows "p \<bullet> p = p"
+  unfolding permute_perm_def 
+  by (simp add: diff_minus add_assoc)
 
 lemma permute_eqvt:
   shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
@@ -392,7 +394,7 @@
 
 lemma permute_fun_app_eq:
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
-unfolding permute_fun_def by simp
+  unfolding permute_fun_def by simp
 
 
 subsection {* Permutations for booleans *}
@@ -429,29 +431,33 @@
   fixes x::"'a::pt"
   and   p::"perm"
   shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
-  apply(auto simp add: permute_fun_def permute_bool_def mem_def)
+  unfolding permute_fun_def
+  unfolding permute_bool_def
+  apply(auto simp add: mem_def)
   apply(rule_tac x="- p \<bullet> x" in exI)
   apply(simp)
   done
 
 lemma permute_set_eq_image:
   shows "p \<bullet> X = permute p ` X"
-unfolding permute_set_eq by auto
+  unfolding permute_set_eq by auto
 
 lemma permute_set_eq_vimage:
   shows "p \<bullet> X = permute (- p) -` X"
-unfolding permute_fun_def permute_bool_def
-unfolding vimage_def Collect_def mem_def ..
+  unfolding permute_fun_def permute_bool_def
+  unfolding vimage_def Collect_def mem_def ..
 
 lemma swap_set_not_in:
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
-  using a by (auto simp add: permute_set_eq swap_atom)
+  unfolding permute_set_eq
+  using a by (auto simp add: 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"
-  using a by (auto simp add: permute_set_eq swap_atom)
+  unfolding permute_set_eq
+  using a by (auto simp add: swap_atom)
 
 
 subsection {* Permutations for units *}
@@ -461,8 +467,8 @@
 
 definition "p \<bullet> (u::unit) = u"
 
-instance proof
-qed (simp_all add: permute_unit_def)
+instance 
+by (default) (simp_all add: permute_unit_def)
 
 end
 
@@ -493,8 +499,8 @@
   "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
 | "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 
-instance proof
-qed (case_tac [!] x, simp_all)
+instance 
+by (default) (case_tac [!] x, simp_all)
 
 end
 
@@ -509,8 +515,8 @@
   "p \<bullet> [] = []"
 | "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 
-instance proof
-qed (induct_tac [!] x, simp_all)
+instance 
+by (default) (induct_tac [!] x, simp_all)
 
 end
 
@@ -525,8 +531,8 @@
   "p \<bullet> None = None"
 | "p \<bullet> (Some x) = Some (p \<bullet> x)"
 
-instance proof
-qed (induct_tac [!] x, simp_all)
+instance 
+by (default) (induct_tac [!] x, simp_all)
 
 end
 
@@ -537,8 +543,8 @@
 
 definition "p \<bullet> (c::char) = c"
 
-instance proof
-qed (simp_all add: permute_char_def)
+instance 
+by (default) (simp_all add: permute_char_def)
 
 end
 
@@ -547,8 +553,8 @@
 
 definition "p \<bullet> (n::nat) = n"
 
-instance proof
-qed (simp_all add: permute_nat_def)
+instance 
+by (default) (simp_all add: permute_nat_def)
 
 end
 
@@ -557,8 +563,8 @@
 
 definition "p \<bullet> (i::int) = i"
 
-instance proof
-qed (simp_all add: permute_int_def)
+instance 
+by (default) (simp_all add: permute_int_def)
 
 end
 
@@ -679,26 +685,28 @@
   have "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
     unfolding fresh_def supp_def by simp
   also have "\<dots> \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> p \<bullet> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
-    using bij_permute by (rule finite_Collect_bij [symmetric])
+    using bij_permute by (rule finite_Collect_bij[symmetric])
   also have "\<dots> \<longleftrightarrow> finite {b. p \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> p \<bullet> x}"
     by (simp only: permute_eqvt [of p] swap_eqvt)
   also have "\<dots> \<longleftrightarrow> finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"
     by (simp only: permute_eq_iff)
   also have "\<dots> \<longleftrightarrow> a \<sharp> x"
     unfolding fresh_def supp_def by simp
-  finally show ?thesis .
+  finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
 qed
 
 lemma fresh_eqvt:
   shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
-  by (simp add: permute_bool_def fresh_permute_iff)
+  unfolding permute_bool_def
+  by (simp add: fresh_permute_iff)
 
 lemma supp_eqvt:
   fixes  p  :: "perm"
   and    x   :: "'a::pt"
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
-  unfolding permute_fun_def Collect_def
+  unfolding Collect_def
+  unfolding permute_fun_def
   by (simp add: Not_eqvt fresh_eqvt)
 
 subsection {* supports *}
@@ -715,10 +723,10 @@
   and     a2: "finite S"
   shows "(supp x) \<subseteq> S"
 proof (rule ccontr)
-  assume "\<not>(supp x \<subseteq> S)"
+  assume "\<not> (supp x \<subseteq> S)"
   then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto
-  from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" by (unfold supports_def) (auto)
-  hence "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
+  from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto
+  then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
   with a2 have "finite {b. (a \<rightleftharpoons> b)\<bullet>x \<noteq> x}" by (simp add: finite_subset)
   then have "a \<notin> (supp x)" unfolding supp_def by simp
   with b1 show False by simp
@@ -738,11 +746,12 @@
 lemma supp_supports:
   fixes x :: "'a::pt"
   shows "(supp x) supports x"
-proof (unfold supports_def, intro strip)
+unfolding supports_def
+proof (intro strip)
   fix a b
   assume "a \<notin> (supp x) \<and> b \<notin> (supp x)"
   then have "a \<sharp> x" and "b \<sharp> x" by (simp_all add: fresh_def)
-  then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (rule swap_fresh_fresh)
+  then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
 qed
 
 lemma supp_is_least_supports:
@@ -837,7 +846,8 @@
 lemma supports_perm: 
   shows "{a. p \<bullet> a \<noteq> a} supports p"
   unfolding supports_def
-  by (simp add: perm_swap_eq swap_eqvt)
+  unfolding perm_swap_eq
+  by (simp add: swap_eqvt)
 
 lemma finite_perm_lemma: 
   shows "finite {a::atom. p \<bullet> a \<noteq> a}"
@@ -855,7 +865,8 @@
 
 lemma fresh_perm: 
   shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a"
-unfolding fresh_def by (simp add: supp_perm)
+  unfolding fresh_def 
+  by (simp add: supp_perm)
 
 lemma supp_swap:
   shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})"
@@ -886,8 +897,9 @@
   fixes p::perm
   shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
   unfolding fresh_def
-  apply(auto simp add: supp_perm)
-  apply(metis permute_minus_cancel)+
+  unfolding supp_perm
+  apply(simp)
+  apply(metis permute_minus_cancel)
   done
 
 lemma supp_minus_perm:
@@ -901,7 +913,7 @@
 
 lemma plus_perm_eq:
   fixes p q::"perm"
-  assumes asm: "supp p \<inter>  supp q = {}"
+  assumes asm: "supp p \<inter> supp q = {}"
   shows "p + q  = q + p"
 unfolding expand_perm_eq
 proof
@@ -1023,8 +1035,28 @@
 
 section {* Support and freshness for applications *}
 
+lemma fresh_conv_MOST: 
+  shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
+  unfolding fresh_def supp_def 
+  unfolding MOST_iff_cofinite by simp
+
+lemma fresh_fun_app:
+  assumes "a \<sharp> f" and "a \<sharp> x" 
+  shows "a \<sharp> f x"
+  using assms 
+  unfolding fresh_conv_MOST
+  unfolding permute_fun_app_eq 
+  by (elim MOST_rev_mp, simp)
+
 lemma supp_fun_app:
   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
+  using fresh_fun_app
+  unfolding fresh_def
+  by auto
+
+(* alternative proof *)
+lemma 
+  shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
 proof (rule subsetCI)
   fix a::"atom"
   assume a: "a \<in> supp (f x)"
@@ -1042,25 +1074,19 @@
   with a show "False" by simp
 qed
     
-lemma fresh_fun_app:
-  shows "a \<sharp> (f, x) \<Longrightarrow> a \<sharp> f x"
-unfolding fresh_def
-using supp_fun_app
-by (auto simp add: supp_Pair)
-
 lemma fresh_fun_eqvt_app:
   assumes a: "\<forall>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
-  from a have b: "supp f = {}"
+  from a have "supp f = {}"
     unfolding supp_def by simp
-  show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
+  then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
     unfolding fresh_def
-    using supp_fun_app b
+    using supp_fun_app 
     by auto
 qed
 
-(* nominal infrastructure *)
+section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"
 
 end