# HG changeset patch
# User urbanc
# Date 1163604235 -3600
# Node ID c29146dc14f10f9ddec4545f58a56b5127c7e868
# Parent  18efe191bd5f86a59c4284323a5b74ef6c19a599
replaced exists_fresh lemma with a version formulated with obtains;
old lemma is available as exists_fresh' (still needed in apply-scripts)

diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Nov 15 16:23:55 2006 +0100
@@ -225,7 +225,7 @@
     show ?case 
     proof (simp)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
 	by (force simp add: fresh_prod fresh_atm)
@@ -243,7 +243,7 @@
     show ?case
     proof (simp add: subst_eqvt)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
 	by (force simp add: fresh_prod fresh_atm)
@@ -320,7 +320,7 @@
     show ?case 
     proof (simp)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
 	by (force simp add: fresh_prod fresh_atm)
@@ -342,7 +342,7 @@
     show ?case
     proof (simp)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
 	by (force simp add: fresh_prod at_fresh[OF at_name_inst])
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 15 16:23:55 2006 +0100
@@ -535,7 +535,7 @@
     have b3: "X\<sharp>\<Gamma>" by fact
     have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh)
     have "\<exists>C::tyvrs. C\<sharp>(pi\<bullet>X,pi\<bullet>S2,pi\<bullet>T2,pi\<bullet>S1,pi\<bullet>T1,pi\<bullet>\<Gamma>,x)"
-      by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1)
+      by (rule exists_fresh', simp add: fs_tyvrs1)
     then obtain C::"tyvrs" where  f1: "C\<noteq>(pi\<bullet>X)" and f2: "C\<sharp>(pi\<bullet>S1)" and f3: "C\<sharp>(pi\<bullet>T1)"
       and f4: "C\<sharp>(pi\<bullet>S2)" and f5: "C\<sharp>(pi\<bullet>T2)" and f6: "C\<sharp>(pi\<bullet>\<Gamma>)" and f7: "C\<sharp>x"
       by (auto simp add: fresh_prod fresh_atm)
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Nov 15 16:23:55 2006 +0100
@@ -92,7 +92,7 @@
     show ?case 
     proof (simp)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
 	by (force simp add: fresh_prod fresh_atm)
@@ -110,7 +110,7 @@
     show ?case
     proof (simp add: subst_eqvt)
       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+	by (rule exists_fresh', simp add: fs_name1)
       then obtain c::"name" 
 	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
 	by (force simp add: fresh_prod fresh_atm)
@@ -318,7 +318,7 @@
     have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
     have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+      by (rule exists_fresh', simp add: fs_name1)
     then obtain c::"name" 
       where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
       by (force simp add: fresh_prod at_fresh[OF at_name_inst])
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Nov 15 16:23:55 2006 +0100
@@ -102,7 +102,7 @@
     have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
     have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
-      by (rule exists_fresh, simp add: fs_name1)
+      by (rule exists_fresh', simp add: fs_name1)
     then obtain c::"name" 
       where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
       by (force simp add: fresh_prod fresh_atm)
@@ -159,7 +159,7 @@
     have f: "a\<sharp>\<Gamma>" by fact
     then have f': "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)"  by (simp add: fresh_bij)
     have "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
-      by (rule exists_fresh, simp add: fs_name1)
+      by (rule exists_fresh', simp add: fs_name1)
     then obtain c::"name" 
       where fs: "c\<noteq>(pi\<bullet>a)" "c\<sharp>x" "c\<sharp>(pi\<bullet>t)" "c\<sharp>(pi\<bullet>\<Gamma>)"
       by (force simp add: fresh_prod fresh_atm)    
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Nov 15 16:23:55 2006 +0100
@@ -338,19 +338,23 @@
 
 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
 
-lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
+lemma fresh_unit_elim: 
+  shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_def supp_unit)
 
-lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
+lemma fresh_prod_elim: 
+  shows "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
   by rule (simp_all add: fresh_prod)
 
 lemma fresh_prodD:
-    "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x"
-    "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
+  shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x"
+  and   "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
   by (simp_all add: fresh_prod)
 
+(* setup for the simplifier to automatically unsplit freshness in products *)
+
 ML_setup {*
-  val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD") :: mksimps_pairs;
+  val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs;
   change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
 *}
 
@@ -717,29 +721,38 @@
 apply(rule at_prm_eq_refl)
 done
 
---"there always exists an atom not being in a finite set"
+--"there always exists an atom that is not being in a finite set"
 lemma ex_in_inf:
   fixes   A::"'x set"
   assumes at: "at TYPE('x)"
   and     fs: "finite A"
-  shows "\<exists>c::'x. c\<notin>A"
+  obtains c::"'x" where "c\<notin>A"
 proof -
   from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
     by (simp add: Diff_infinite_finite)
   hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
-  hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
-  thus "\<exists>c::'x. c\<notin>A" by force
+  then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
+  then have "c\<notin>A" by simp
+  then show ?thesis using prems by simp 
 qed
 
---"there always exists a fresh name for an object with finite support"
+text {* there always exists a fresh name for an object with finite support *}
+lemma at_exists_fresh': 
+  fixes  x :: "'a"
+  assumes at: "at TYPE('x)"
+  and     fs: "finite ((supp x)::'x set)"
+  shows "\<exists>c::'x. c\<sharp>x"
+  by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs])
+
 lemma at_exists_fresh: 
   fixes  x :: "'a"
   assumes at: "at TYPE('x)"
   and     fs: "finite ((supp x)::'x set)"
-  shows "\<exists>c::'x. c\<sharp>x"
-  by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
+  obtains c::"'x" where  "c\<sharp>x"
+  by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
 
-lemma at_finite_select: "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
+lemma at_finite_select: 
+  shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
   apply (drule Diff_infinite_finite)
   apply (simp add: at_def)
   apply blast
@@ -1635,6 +1648,7 @@
 qed
 
 section {* equivaraince for some connectives *}
+(* FIXME: maybe not really needed *)
 
 lemma pt_all_eqvt:
   fixes  pi :: "'x prm"
@@ -2776,7 +2790,7 @@
   shows "b\<sharp>([a].x)"
   proof -
     have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 
-    proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+    proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
       show "finite ((supp ([a].x))::'x set)" using f
 	by (simp add: abs_fun_finite_supp[OF pt, OF at])	
     qed
@@ -2807,7 +2821,7 @@
   shows "b\<sharp>x"
 proof -
   have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
-  proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+  proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
     show "finite ((supp ([a].x))::'x set)" using f
       by (simp add: abs_fun_finite_supp[OF pt, OF at])	
   qed
@@ -2834,7 +2848,7 @@
   shows "a\<sharp>([a].x)"
 proof -
   have "\<exists>c::'x. c\<sharp>(a,x)"
-    by  (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f) 
+    by  (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 
   then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 
                 and   fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
   have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Nov 15 16:23:55 2006 +0100
@@ -684,6 +684,7 @@
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
        val pt_rev_pi           = thm "Nominal.pt_rev_pi";
        val at_exists_fresh     = thm "Nominal.at_exists_fresh";
+       val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
 
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
@@ -764,6 +765,7 @@
             ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
+            ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
             ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_at [at_fresh]
diff -r 18efe191bd5f -r c29146dc14f1 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 15 16:23:55 2006 +0100
@@ -1595,7 +1595,7 @@
 
     (** uniqueness **)
 
-    val exists_fresh = PureThy.get_thms thy11 (Name "exists_fresh");
+    val exists_fresh' = PureThy.get_thms thy11 (Name "exists_fresh'");
     val fs_atoms = map (fn Type (s, _) => PureThy.get_thm thy11
       (Name ("fs_" ^ Sign.base_name s ^ "1"))) dt_atomTs;
     val fresh_atm = PureThy.get_thms thy11 (Name "fresh_atm");
@@ -1636,7 +1636,7 @@
           (fn _ => EVERY
             [cut_facts_tac ths 1,
              REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
-             resolve_tac exists_fresh 1,
+             resolve_tac exists_fresh' 1,
              asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
         val (([cx], ths), ctxt') = Obtain.result
           (fn _ => EVERY