diff -r e73bd379e839 -r e8732350a29f Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Dec 30 10:00:09 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Dec 31 12:12:59 2010 +0000
@@ -1407,8 +1407,34 @@
   done
 
 
-section {* Fresh-Star *}
+section {* Freshness and Fresh-Star *}
+
+lemma fresh_Unit_elim: 
+  shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_Unit)
+
+lemma fresh_Pair_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_Pair)
 
+(* 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_Pair)
+
+lemma fresh_PairD:
+  shows "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x"
+  and   "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
+  by (simp_all add: fresh_Pair)
+
+ML {*
+  val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs;
+*}
+
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
 
 text {* The fresh-star generalisation of fresh is used in strong
   induction principles. *}
@@ -1473,7 +1499,7 @@
   "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def)
 
-lemma fresh_star_unit_elim: 
+lemma fresh_star_Unit_elim: 
   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def fresh_Unit)