src/HOL/Nominal/Nominal.thy

   fixes a :: "'x"
   and   x :: "'a"
   shows "a\<sharp>(Some x) = a\<sharp>x"
   apply(simp add: fresh_def supp_some)
   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 *}
 (*=========================================================*)
 

 use "nominal_package.ML"
 setup "NominalAtoms.setup"
 
 (*****************************************)
 (* setup for induction principles method *)
+
 use "nominal_induct.ML";
 method_setup nominal_induct =
-  {* nominal_induct_method *}
+  {* NominalInduct.nominal_induct_method *}
   {* nominal induction *}
 
 (*******************************)
 (* permutation equality tactic *)
 use "nominal_permeq.ML";

 method_setup supports_simp_debug =
   {* supports_meth_debug *}
   {* tactic for deciding equalities involving permutations including debuging facilities *}
 
 end
-
-