# HG changeset patch
# User wenzelm
# Date 1133349815 -3600
# Node ID bbfd64cc91abaff6d502d9cd5acf8d80a3d90b12
# Parent  4eaa654c92f2e9ac5034ab25d2a2c24b9e275efa
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;

diff -r 4eaa654c92f2 -r bbfd64cc91ab src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Nov 30 01:01:15 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Nov 30 12:23:35 2005 +0100
@@ -241,6 +241,15 @@
   done
 
 
+text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
+
+lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) == PROP C"
+  by (simp add: fresh_def supp_unit)
+
+lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) == (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
+  by rule (simp_all add: fresh_prod)
+
+
 section {* Abstract Properties for Permutations and  Atoms *}
 (*=========================================================*)
 
@@ -2581,9 +2590,10 @@
 
 (*****************************************)
 (* setup for induction principles method *)
+
 use "nominal_induct.ML";
 method_setup nominal_induct =
-  {* nominal_induct_method *}
+  {* NominalInduct.nominal_induct_method *}
   {* nominal induction *}
 
 (*******************************)
@@ -2607,5 +2617,3 @@
   {* tactic for deciding equalities involving permutations including debuging facilities *}
 
 end
-
-