--- a/src/HOL/Nat.thy Wed Feb 12 09:06:04 2014 +0100
+++ b/src/HOL/Nat.thy Wed Feb 12 10:59:25 2014 +0100
@@ -71,33 +71,81 @@
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"
+
+declare nat.sel[code del]
+
+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 old.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 nat_case_0 = nat.cases(1)
- and nat_case_Suc = nat.cases(2)
-
+hide_fact
+ nat_exhaust
+ nat_induct0
text {* Injectiveness and distinctness lemmas *}
@@ -632,14 +680,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_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
-by simp
-
-lemma def_nat_rec_Suc: "(!!n. f n == nat_rec 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
@@ -1905,13 +1945,13 @@
qed
-subsection {* aliasses *}
+subsection {* aliases *}
lemma nat_mult_1: "(1::nat) * n = n"
- by simp
+ by (rule mult_1_left)
lemma nat_mult_1_right: "n * (1::nat) = n"
- by simp
+ by (rule mult_1_right)
subsection {* size of a datatype value *}
@@ -1928,4 +1968,3 @@
hide_const (open) of_nat_aux
end
-