src/HOL/Nat.thy
changeset 25510 38c15efe603b
parent 25502 9200b36280c0
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Nat.thy	Fri Nov 30 16:23:52 2007 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Nov 30 20:13:03 2007 +0100
     1.3 @@ -54,9 +54,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -instance nat :: zero
     1.8 -  Zero_nat_def: "0 == Abs_Nat Zero_Rep" ..
     1.9 -lemmas [code func del] = Zero_nat_def
    1.10 +instantiation nat :: zero
    1.11 +begin
    1.12 +
    1.13 +definition Zero_nat_def [code func del]:
    1.14 +  "0 = Abs_Nat Zero_Rep"
    1.15 +
    1.16 +instance ..
    1.17 +
    1.18 +end
    1.19  
    1.20  defs
    1.21    Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.22 @@ -155,11 +161,18 @@
    1.23    pred_nat :: "(nat * nat) set" where
    1.24    "pred_nat = {(m, n). n = Suc m}"
    1.25  
    1.26 -instance nat :: ord
    1.27 -  less_def: "m < n == (m, n) : pred_nat^+"
    1.28 -  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
    1.29 +instantiation nat :: ord
    1.30 +begin
    1.31 +
    1.32 +definition
    1.33 +  less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+"
    1.34  
    1.35 -lemmas [code func del] = less_def le_def
    1.36 +definition
    1.37 +  le_def [code func del]:   "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m"
    1.38 +
    1.39 +instance ..
    1.40 +
    1.41 +end
    1.42  
    1.43  lemma wf_pred_nat: "wf pred_nat"
    1.44    apply (unfold wf_def pred_nat_def, clarify)
    1.45 @@ -1488,8 +1501,8 @@
    1.46  text {* the lattice order on @{typ nat} *}
    1.47  
    1.48  instance nat :: distrib_lattice
    1.49 -  "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
    1.50 -  "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
    1.51 +  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
    1.52 +  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
    1.53    by intro_classes
    1.54      (simp_all add: inf_nat_def sup_nat_def)
    1.55