# HG changeset patch
# User urbanc
# Date 1163781150 -3600
# Node ID 26b51f724fe6ed3dbb8fed20492bae11a538469f
# Parent  eb85850d3eb7baeee3c75a51b8675db969fc0bc8
added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)

diff -r eb85850d3eb7 -r 26b51f724fe6 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 02:20:03 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 17:32:30 2006 +0100
@@ -101,11 +101,9 @@
     have k1: "a\<sharp>\<Gamma>" by fact
     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)
-    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)
+    obtain c::"name" where "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (erule exists_fresh[OF fs_name1])
+    then have 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 (simp_all add: fresh_atm[symmetric]) 
     from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)"  by (simp add: fresh_bij)
     have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
       by (simp only: pt_name2, rule perm_fresh_fresh)
@@ -158,11 +156,9 @@
     have ih1: "\<And>(pi::name prm) x. P x (pi\<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
     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)
-    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)    
+    obtain  c::"name" where "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (erule exists_fresh[OF fs_name1])
+    then have fs: "c\<noteq>(pi\<bullet>a)" "c\<sharp>x" "c\<sharp>(pi\<bullet>t)" "c\<sharp>(pi\<bullet>\<Gamma>)"
+      by (simp_all add: fresh_atm[symmetric])    
     let ?pi'="[(pi\<bullet>a,c)]@pi"
     have eq: "((pi\<bullet>a,c)#pi)\<bullet>a = c" by (simp add: calc_atm)
     have p1': "(?pi'\<bullet>((a,\<tau>)#\<Gamma>))\<turnstile>(?pi'\<bullet>t):\<sigma>" using p1 by (simp only: eqvt_typing)
diff -r eb85850d3eb7 -r 26b51f724fe6 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Nov 17 02:20:03 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Fri Nov 17 17:32:30 2006 +0100
@@ -346,13 +346,17 @@
   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)
 
+(* this rule needs to be added before the fresh_prodD is *)
+(* added to the simplifier with mksimps                  *) 
+lemma [simp]:
+  shows "a\<sharp>x1 \<Longrightarrow> a\<sharp>x2 \<Longrightarrow> a\<sharp>(x1,x2)"
+  by (simp add: fresh_prod)
+
 lemma fresh_prodD:
   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;
   change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));