src/HOL/Nat.thy
changeset 55417 01fbfb60c33e
parent 55415 05f5fdb8d093
child 55423 07dea66779f3
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -71,33 +71,79 @@
     1.4  lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
     1.5    by (rule iffI, rule Suc_Rep_inject) simp_all
     1.6  
     1.7 +lemma nat_induct0:
     1.8 +  fixes n
     1.9 +  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.10 +  shows "P n"
    1.11 +using assms
    1.12 +apply (unfold Zero_nat_def Suc_def)
    1.13 +apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.14 +apply (erule Nat_Rep_Nat [THEN Nat.induct])
    1.15 +apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
    1.16 +done
    1.17 +
    1.18 +wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]]
    1.19 +  apply atomize_elim
    1.20 +  apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.21 + apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
    1.22 +   Suc_Rep_inject' Rep_Nat_inject)
    1.23 +apply (simp only: Suc_not_Zero)
    1.24 +done
    1.25 +
    1.26 +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    1.27 +setup {* Sign.mandatory_path "old" *}
    1.28 +
    1.29  rep_datatype "0 \<Colon> nat" Suc
    1.30 -  apply (unfold Zero_nat_def Suc_def)
    1.31 -  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.32 -   apply (erule Nat_Rep_Nat [THEN Nat.induct])
    1.33 -   apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
    1.34 -    apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
    1.35 -      Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
    1.36 -      Suc_Rep_not_Zero_Rep [symmetric]
    1.37 -      Suc_Rep_inject' Rep_Nat_inject)
    1.38 -  done
    1.39 +  apply (erule nat_induct0, assumption)
    1.40 + apply (rule nat.inject)
    1.41 +apply (rule nat.distinct(1))
    1.42 +done
    1.43 +
    1.44 +setup {* Sign.parent_path *}
    1.45 +
    1.46 +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    1.47 +setup {* Sign.mandatory_path "nat" *}
    1.48 +
    1.49 +declare
    1.50 +  old.nat.inject[iff del]
    1.51 +  old.nat.distinct(1)[simp del, induct_simp del]
    1.52 +
    1.53 +lemmas induct = old.nat.induct
    1.54 +lemmas inducts = old.nat.inducts
    1.55 +lemmas recs = old.nat.recs
    1.56 +lemmas cases = nat.case
    1.57 +lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
    1.58 +
    1.59 +setup {* Sign.parent_path *}
    1.60 +
    1.61 +abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
    1.62 +  "rec_nat \<equiv> old.rec_nat"
    1.63 +
    1.64 +hide_const Nat.pred -- {* hide everything related to the selector *}
    1.65 +hide_fact
    1.66 +  nat.case_eq_if
    1.67 +  nat.collapse
    1.68 +  nat.expand
    1.69 +  nat.sel
    1.70 +  nat.sel_exhaust
    1.71 +  nat.sel_split
    1.72 +  nat.sel_split_asm
    1.73 +
    1.74 +lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
    1.75 +  -- {* for backward compatibility -- names of variables differ *}
    1.76 +  "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
    1.77 +by (rule nat.exhaust)
    1.78  
    1.79  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.80    -- {* for backward compatibility -- names of variables differ *}
    1.81    fixes n
    1.82 -  assumes "P 0"
    1.83 -    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.84 +  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.85    shows "P n"
    1.86 -  using assms by (rule nat.induct)
    1.87 -
    1.88 -declare nat.exhaust [case_names 0 Suc, cases type: nat]
    1.89 +using assms by (rule nat.induct)
    1.90  
    1.91 -lemmas nat_rec_0 = nat.recs(1)
    1.92 -  and nat_rec_Suc = nat.recs(2)
    1.93 -
    1.94 -lemmas case_nat_0 = nat.cases(1)
    1.95 -  and case_nat_Suc = nat.cases(2)
    1.96 -   
    1.97 +hide_fact
    1.98 +  nat_exhaust
    1.99 +  nat_induct0
   1.100  
   1.101  text {* Injectiveness and distinctness lemmas *}
   1.102  
   1.103 @@ -632,14 +678,6 @@
   1.104  
   1.105  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   1.106  
   1.107 -text {* These two rules ease the use of primitive recursion.
   1.108 -NOTE USE OF @{text "=="} *}
   1.109 -lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
   1.110 -by simp
   1.111 -
   1.112 -lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
   1.113 -by simp
   1.114 -
   1.115  lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   1.116  by (cases n) simp_all
   1.117  
   1.118 @@ -1928,4 +1966,3 @@
   1.119  hide_const (open) of_nat_aux
   1.120  
   1.121  end
   1.122 -