src/HOL/Nat.thy
changeset 44325 84696670feb1
parent 44278 1220ecb81e8f
child 44817 b63e445c8f6d
     1.1 --- a/src/HOL/Nat.thy	Sat Aug 20 01:33:58 2011 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Aug 20 01:39:27 2011 +0200
     1.3 @@ -22,10 +22,7 @@
     1.4  
     1.5  typedecl ind
     1.6  
     1.7 -axiomatization
     1.8 -  Zero_Rep :: ind and
     1.9 -  Suc_Rep :: "ind => ind"
    1.10 -where
    1.11 +axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
    1.12    -- {* the axiom of infinity in 2 parts *}
    1.13    Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    1.14    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.15 @@ -34,10 +31,9 @@
    1.16  
    1.17  text {* Type definition *}
    1.18  
    1.19 -inductive Nat :: "ind \<Rightarrow> bool"
    1.20 -where
    1.21 -    Zero_RepI: "Nat Zero_Rep"
    1.22 -  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    1.23 +inductive Nat :: "ind \<Rightarrow> bool" where
    1.24 +  Zero_RepI: "Nat Zero_Rep"
    1.25 +| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    1.26  
    1.27  typedef (open Nat) nat = "{n. Nat n}"
    1.28    using Nat.Zero_RepI by auto
    1.29 @@ -142,10 +138,9 @@
    1.30  instantiation nat :: "{minus, comm_monoid_add}"
    1.31  begin
    1.32  
    1.33 -primrec plus_nat
    1.34 -where
    1.35 +primrec plus_nat where
    1.36    add_0:      "0 + n = (n\<Colon>nat)"
    1.37 -  | add_Suc:  "Suc m + n = Suc (m + n)"
    1.38 +| add_Suc:  "Suc m + n = Suc (m + n)"
    1.39  
    1.40  lemma add_0_right [simp]: "m + 0 = (m::nat)"
    1.41    by (induct m) simp_all
    1.42 @@ -158,8 +153,7 @@
    1.43  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
    1.44    by simp
    1.45  
    1.46 -primrec minus_nat
    1.47 -where
    1.48 +primrec minus_nat where
    1.49    diff_0 [code]: "m - 0 = (m\<Colon>nat)"
    1.50  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.51  
    1.52 @@ -188,10 +182,9 @@
    1.53  definition
    1.54    One_nat_def [simp]: "1 = Suc 0"
    1.55  
    1.56 -primrec times_nat
    1.57 -where
    1.58 +primrec times_nat where
    1.59    mult_0:     "0 * n = (0\<Colon>nat)"
    1.60 -  | mult_Suc: "Suc m * n = n + (m * n)"
    1.61 +| mult_Suc: "Suc m * n = n + (m * n)"
    1.62  
    1.63  lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
    1.64    by (induct m) simp_all
    1.65 @@ -364,7 +357,7 @@
    1.66  
    1.67  primrec less_eq_nat where
    1.68    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    1.69 -  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    1.70 +| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    1.71  
    1.72  declare less_eq_nat.simps [simp del]
    1.73  lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
    1.74 @@ -1200,8 +1193,8 @@
    1.75  begin
    1.76  
    1.77  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.78 -    "funpow 0 f = id"
    1.79 -  | "funpow (Suc n) f = f o funpow n f"
    1.80 +  "funpow 0 f = id"
    1.81 +| "funpow (Suc n) f = f o funpow n f"
    1.82  
    1.83  end
    1.84  
    1.85 @@ -1267,7 +1260,7 @@
    1.86  
    1.87  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.88    "of_nat_aux inc 0 i = i"
    1.89 -  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    1.90 +| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    1.91  
    1.92  lemma of_nat_code:
    1.93    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"