# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271661931 -7200
# Node ID 869d1183e0823789eb742cb7910a0976a34ce780
# Parent  c7cdea70eacdcc30446f46201f30546d02ac1e00
tuned proofs

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
diff -r c7cdea70eacd -r 869d1183e082 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Sun Apr 18 18:01:22 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Mon Apr 19 09:25:31 2010 +0200
@@ -141,20 +141,38 @@
   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
   unfolding fresh_star_def fresh_def by blast
 
+lemma at_set_avoiding2:
+  assumes "finite xs"
+  and     "finite (supp c)" "finite (supp x)"
+  and     "xs \<sharp>* x"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
+
+lemma at_set_avoiding2_atom:
+  assumes "finite (supp c)" "finite (supp x)"
+  and     b: "xa \<sharp> x"
+  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
+  have c: "(p \<bullet> xa) \<sharp> c" using p1
+    unfolding fresh_star_def Ball_def 
+    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
+  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+  then show ?thesis by blast
+qed
 
 section {* The freshness lemma according to Andrew Pitts *}
 
-lemma fresh_conv_MOST: 
-  shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
-  unfolding fresh_def supp_def MOST_iff_cofinite by simp
-
-lemma fresh_apply:
-  assumes "a \<sharp> f" and "a \<sharp> x" 
-  shows "a \<sharp> f x"
-  using assms unfolding fresh_conv_MOST
-  unfolding permute_fun_app_eq [where f=f]
-  by (elim MOST_rev_mp, simp)
-
 lemma freshness_lemma:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
@@ -173,7 +191,8 @@
     next
       assume "a \<noteq> b"
       hence "atom a \<sharp> b" by (simp add: fresh_at_base)
-      with a3 have "atom a \<sharp> h b" by (rule fresh_apply)
+      with a3 have "atom a \<sharp> h b" 
+	by (rule fresh_fun_app)
       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
         by (rule swap_fresh_fresh)
       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
@@ -358,7 +377,7 @@
   using not_fresh_nat_of [unfolded fresh_def] by auto
 
 
-section {* Support for sets of atoms *}
+section {* Support for finite sets of atoms *}
 
 lemma supp_finite_atom_set:
   fixes S::"atom set"
@@ -447,36 +466,4 @@
   qed
 qed
 
-section {* at_set_avoiding2 *}
-
-lemma at_set_avoiding2:
-  assumes "finite xs"
-  and     "finite (supp c)" "finite (supp x)"
-  and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
-using assms
-apply(erule_tac c="(c, x)" in at_set_avoiding)
-apply(simp add: supp_Pair)
-apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
-done
-
-lemma at_set_avoiding2_atom:
-  assumes "finite (supp c)" "finite (supp x)"
-  and     b: "xa \<sharp> x"
-  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
-proof -
-  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
-  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
-    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
-  have c: "(p \<bullet> xa) \<sharp> c" using p1
-    unfolding fresh_star_def Ball_def 
-    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
-  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
-  then show ?thesis by blast
-qed
-
 end