cleanup
authorhaftmann
Wed Nov 22 10:20:16 2006 +0100 (2006-11-22)
changeset 214561c2b9df41e98
parent 21455 b6be1d1b66c5
child 21457 84a21cf15923
cleanup
src/HOL/Nat.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Nov 22 10:20:15 2006 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Nov 22 10:20:16 2006 +0100
     1.3 @@ -46,9 +46,6 @@
     1.4    show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
     1.5  qed
     1.6  
     1.7 -instance nat :: "{ord, zero, one}" ..
     1.8 -
     1.9 -
    1.10  text {* Abstract constants and syntax *}
    1.11  
    1.12  consts
    1.13 @@ -58,19 +55,14 @@
    1.14  local
    1.15  
    1.16  defs
    1.17 -  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
    1.18    Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.19 -  One_nat_def:  "1 == Suc 0"
    1.20 -
    1.21 -  -- {* nat operations *}
    1.22    pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
    1.23  
    1.24 +instance nat :: "{ord, zero, one}"
    1.25 +  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
    1.26 +  One_nat_def [simp]: "1 == Suc 0"
    1.27    less_def: "m < n == (m, n) : trancl pred_nat"
    1.28 -
    1.29 -  le_def: "m \<le> (n::nat) == ~ (n < m)"
    1.30 -
    1.31 -declare One_nat_def [simp]
    1.32 -
    1.33 +  le_def: "m \<le> (n::nat) == ~ (n < m)" ..
    1.34  
    1.35  text {* Induction *}
    1.36  
    1.37 @@ -481,7 +473,7 @@
    1.38  
    1.39  text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
    1.40  
    1.41 -instance nat :: "{plus, minus, times, power}" ..
    1.42 +instance nat :: "{plus, minus, times}" ..
    1.43  
    1.44  primrec
    1.45    add_0:    "0 + n = n"
    1.46 @@ -1059,16 +1051,16 @@
    1.47  instance nat :: eq ..
    1.48  
    1.49  lemma [code func]:
    1.50 -  "Code_Generator.eq (0\<Colon>nat) 0 = True" unfolding eq_def by auto
    1.51 +  "(0\<Colon>nat) = 0 \<longleftrightarrow> True" by auto
    1.52  
    1.53  lemma [code func]:
    1.54 -  "Code_Generator.eq (Suc n) (Suc m) = Code_Generator.eq n m" unfolding eq_def by auto
    1.55 +  "Suc n = Suc m \<longleftrightarrow> n = m" by auto
    1.56  
    1.57  lemma [code func]:
    1.58 -  "Code_Generator.eq (Suc n) 0 = False" unfolding eq_def by auto
    1.59 +  "Suc n = 0 \<longleftrightarrow> False" by auto
    1.60  
    1.61  lemma [code func]:
    1.62 -  "Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
    1.63 +  "0 = Suc m \<longleftrightarrow> False" by auto
    1.64  
    1.65  
    1.66  subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
     2.1 --- a/src/HOL/Power.thy	Wed Nov 22 10:20:15 2006 +0100
     2.2 +++ b/src/HOL/Power.thy	Wed Nov 22 10:20:16 2006 +0100
     2.3 @@ -311,6 +311,8 @@
     2.4  
     2.5  subsection{*Exponentiation for the Natural Numbers*}
     2.6  
     2.7 +instance nat :: power ..
     2.8 +
     2.9  primrec (power)
    2.10    "p ^ 0 = 1"
    2.11    "p ^ (Suc n) = (p::nat) * (p ^ n)"