src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -71,33 +71,79 @@
 lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
   by (rule iffI, rule Suc_Rep_inject) simp_all
 
+lemma nat_induct0:
+  fixes n
+  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+  shows "P n"
+using assms
+apply (unfold Zero_nat_def Suc_def)
+apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
+apply (erule Nat_Rep_Nat [THEN Nat.induct])
+apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
+done
+
+wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]]
+  apply atomize_elim
+  apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
+ apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
+   Suc_Rep_inject' Rep_Nat_inject)
+apply (simp only: Suc_not_Zero)
+done
+
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
 rep_datatype "0 \<Colon> nat" Suc
-  apply (unfold Zero_nat_def Suc_def)
-  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
-   apply (erule Nat_Rep_Nat [THEN Nat.induct])
-   apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
-    apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
-      Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
-      Suc_Rep_not_Zero_Rep [symmetric]
-      Suc_Rep_inject' Rep_Nat_inject)
-  done
+  apply (erule nat_induct0, assumption)
+ apply (rule nat.inject)
+apply (rule nat.distinct(1))
+done
+
+setup {* Sign.parent_path *}
+
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "nat" *}
+
+declare
+  old.nat.inject[iff del]
+  old.nat.distinct(1)[simp del, induct_simp del]
+
+lemmas induct = old.nat.induct
+lemmas inducts = old.nat.inducts
+lemmas recs = old.nat.recs
+lemmas cases = nat.case
+lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
+
+setup {* Sign.parent_path *}
+
+abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
+  "rec_nat \<equiv> old.rec_nat"
+
+hide_const Nat.pred -- {* hide everything related to the selector *}
+hide_fact
+  nat.case_eq_if
+  nat.collapse
+  nat.expand
+  nat.sel
+  nat.sel_exhaust
+  nat.sel_split
+  nat.sel_split_asm
+
+lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
+  -- {* for backward compatibility -- names of variables differ *}
+  "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
+by (rule nat.exhaust)
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]:
   -- {* for backward compatibility -- names of variables differ *}
   fixes n
-  assumes "P 0"
-    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   shows "P n"
-  using assms by (rule nat.induct)
-
-declare nat.exhaust [case_names 0 Suc, cases type: nat]
+using assms by (rule nat.induct)
 
-lemmas nat_rec_0 = nat.recs(1)
-  and nat_rec_Suc = nat.recs(2)
-
-lemmas case_nat_0 = nat.cases(1)
-  and case_nat_Suc = nat.cases(2)
-   
+hide_fact
+  nat_exhaust
+  nat_induct0
 
 text {* Injectiveness and distinctness lemmas *}
 
@@ -632,14 +678,6 @@
 
 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
 
-text {* These two rules ease the use of primitive recursion.
-NOTE USE OF @{text "=="} *}
-lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
-by simp
-
-lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
-by simp
-
 lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
 by (cases n) simp_all
 
@@ -1928,4 +1966,3 @@
 hide_const (open) of_nat_aux
 
 end
-