# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271879550 -7200
# Node ID 2b0cc308fd6abe08571f075e0b65b4cf6faf28c9
# Parent  24ae81462f3e47972ab3560735f303ab771aa716
tuned proofs

diff -r 24ae81462f3e -r 2b0cc308fd6a Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:31:07 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:52:30 2010 +0200
@@ -1079,26 +1079,6 @@
   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)"
-  assume b: "a \<notin> supp f \<union> supp x"
-  then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 
-    unfolding supp_def by auto
-  then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp
-  moreover 
-  have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"
-    by auto
-  ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"
-    using finite_subset by auto
-  then have "a \<notin> supp (f x)" unfolding supp_def
-    by (simp add: permute_fun_app_eq)
-  with a show "False" by simp
-qed
-    
 lemma fresh_fun_eqvt_app:
   assumes a: "\<forall>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
diff -r 24ae81462f3e -r 2b0cc308fd6a Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 21 21:31:07 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 21:52:30 2010 +0200
@@ -129,16 +129,22 @@
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition
+  Abs ("[_]set. _" [60, 60] 60)
+where
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_res ("[_]res. _" [60, 60] 60)
+where
   "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_lst ("[_]lst. _" [60, 60] 60)
+where
   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 is
   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
@@ -169,9 +175,8 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  apply(simp_all add: alphas_abs)
-  apply(lifting alphas_abs)
-  done
+  unfolding alphas_abs
+  by (lifting alphas_abs)
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -327,9 +332,8 @@
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
-  apply(rule_tac [!] fresh_fun_eqvt_app)
-  apply(simp_all add: eqvts_raw)
-  done
+  by (rule_tac [!] fresh_fun_eqvt_app)
+     (simp_all add: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
@@ -337,36 +341,32 @@
   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
   unfolding supp_conv_fresh
-  apply(auto dest!: aux_fresh)
-  apply(simp_all add: fresh_def supp_finite_atom_set a)
-  done
+  by (auto dest!: aux_fresh)
+     (simp_all add: fresh_def supp_finite_atom_set a)
 
 lemma supp_abs_subset2:
   assumes a: "finite (supp x)"
   shows "supp (Abs as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
-  apply(rule_tac [!] supp_is_subset)
-  apply(simp_all add: abs_supports a)
-  done
+  by (rule_tac [!] supp_is_subset)
+     (simp_all add: abs_supports a)
 
 lemma abs_finite_supp:
   assumes a: "finite (supp x)"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] subset_antisym)
-  apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
-  done
+  by (rule_tac [!] subset_antisym)
+     (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
 
 lemma supp_abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] abs_finite_supp)
-  apply(simp_all add: finite_supp)
-  done
+  by (rule_tac [!] abs_finite_supp)
+     (simp_all add: finite_supp)
 
 instance abs_gen :: (fs) fs
   apply(default)