# HG changeset patch
# User berghofe
# Date 1235586840 -3600
# Node ID 9c3b1c136d1f6217bef41b0c0a382bf711628399
# Parent  2fb0b721e9c256835c4f7505c311d4ac5c38a1c2
Added lemmas for normalizing freshness results involving fresh_star.

diff -r 2fb0b721e9c2 -r 9c3b1c136d1f src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Feb 25 18:53:34 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Feb 25 19:34:00 2009 +0100
@@ -397,6 +397,18 @@
 
 lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
 
+text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
+
+lemma fresh_star_unit_elim: 
+  shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+  and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp_all add: fresh_star_def fresh_def supp_unit)
+
+lemma fresh_star_prod_elim: 
+  shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
+  and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
+  by (rule, simp_all add: fresh_star_prod)+
+
 section {* Abstract Properties for Permutations and  Atoms *}
 (*=========================================================*)
 
diff -r 2fb0b721e9c2 -r 9c3b1c136d1f src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 18:53:34 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 19:34:00 2009 +0100
@@ -1,5 +1,4 @@
-(*  ID:         $Id$
-    Author:     Christian Urban and Makarius
+(*  Author:     Christian Urban and Makarius
 
 The nominal induct proof method.
 *)
@@ -24,7 +23,8 @@
 
 val split_all_tuples =
   Simplifier.full_simplify (HOL_basic_ss addsimps
-    [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]);
+    [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
+    @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
 
 
 (* prepare rule *)