# HG changeset patch
# User urbanc
# Date 1141836895 -3600
# Node ID a45baf1ac094e3f5ec29c238fd7673f03e725415
# Parent  03abed544f1e007376f0d6fa570b4d3120e451d0
tuned some of the proofs about fresh_fun

diff -r 03abed544f1e -r a45baf1ac094 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Mar 08 17:23:46 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Mar 08 17:54:55 2006 +0100
@@ -1488,7 +1488,7 @@
   hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
   then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
   from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
-  with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
+  hence "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by force
   with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
   hence "a\<notin>(supp x)" by (unfold supp_def, auto)
   with b1 show False by simp
@@ -2140,37 +2140,6 @@
   with b show "fr = h a" by force
 qed
 
-
-lemma fresh_fun_supports:
-  fixes h :: "'x\<Rightarrow>'a"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)" 
-  and     f1: "finite ((supp h)::'x set)"
-  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
-  shows "((supp h)::'x set) supports (fresh_fun h)"
-  apply(simp add: "op supports_def")
-  apply(fold fresh_def)
-  apply(auto)
-  apply(subgoal_tac "\<exists>(a''::'x). a''\<sharp>(h,a,b)")(*A*)
-  apply(erule exE)
-  apply(simp add: fresh_prod)
-  apply(auto)
-  apply(rotate_tac 2)
-  apply(drule fresh_fun_app[OF pt, OF at, OF f1, OF a])
-  apply(simp add: at_fresh[OF at])
-  apply(simp add: pt_fun_app_eq[OF at_pt_inst[OF at], OF at])
-  apply(auto simp add: at_calc[OF at])
-  apply(subgoal_tac "[(a, b)]\<bullet>h = h")(*B*)
-  apply(simp)
-  (*B*)
-  apply(rule pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
-  apply(assumption)+
-  (*A*)
-  apply(rule at_exists_fresh[OF at])
-  apply(simp add: supp_prod)
-  apply(simp add: f1 at_supp[OF at])
-  done
-
 lemma fresh_fun_equiv:
   fixes h :: "'x\<Rightarrow>'a"
   and   pi:: "'x prm"
@@ -2200,6 +2169,19 @@
   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
   show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
 qed
+
+lemma fresh_fun_supports:
+  fixes h :: "'x\<Rightarrow>'a"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)" 
+  and     f1: "finite ((supp h)::'x set)"
+  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+  shows "((supp h)::'x set) supports (fresh_fun h)"
+  apply(simp add: "op supports_def" fresh_def[symmetric])
+  apply(auto)
+  apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a])
+  apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
+  done
   
 section {* disjointness properties *}
 (*=================================*)