diff -r 548703affff5 -r a1a436f09ec6 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Tue Oct 28 17:53:46 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Wed Oct 29 11:33:40 2008 +0100
@@ -27,6 +27,9 @@
   by (rule index_of_nat_inverse) 
     (unfold index_def, rule UNIV_I)
 
+lemma [measure_function]:
+  "is_measure nat_of_index" by (rule is_measure_trivial)
+
 lemma index:
   "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
 proof
@@ -143,70 +146,73 @@
 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
 begin
 
-lemma zero_index_code [code inline, code]:
-  "(0\<Colon>index) = Numeral0"
-  by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
-  using zero_index_code ..
-
 definition [simp, code del]:
   "(1\<Colon>index) = index_of_nat 1"
 
-lemma one_index_code [code inline, code]:
-  "(1\<Colon>index) = Numeral1"
-  by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
-  using one_index_code ..
-
 definition [simp, code del]:
   "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
 
-lemma plus_index_code [code]:
-  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
-  by simp
-
 definition [simp, code del]:
   "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
 
 definition [simp, code del]:
   "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
 
-lemma times_index_code [code]:
-  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
-  by simp
-
 definition [simp, code del]:
   "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
 
 definition [simp, code del]:
   "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
 
-lemma div_index_code [code]:
-  "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
-  by simp
-
-lemma mod_index_code [code]:
-  "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
-  by simp
-
 definition [simp, code del]:
   "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
 
 definition [simp, code del]:
   "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
 
-lemma less_eq_index_code [code]:
+instance by default (auto simp add: left_distrib index)
+
+end
+
+lemma zero_index_code [code inline, code]:
+  "(0\<Colon>index) = Numeral0"
+  by (simp add: number_of_index_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>index)"
+  using zero_index_code ..
+
+lemma one_index_code [code inline, code]:
+  "(1\<Colon>index) = Numeral1"
+  by (simp add: number_of_index_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>index)"
+  using one_index_code ..
+
+lemma plus_index_code [code nbe]:
+  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
+  by simp
+
+definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
+  [simp, code del]: "subtract_index = op -"
+
+lemma subtract_index_code [code nbe]:
+  "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)"
+  by simp
+
+lemma minus_index_code [code]:
+  "n - m = subtract_index n m"
+  by simp
+
+lemma times_index_code [code nbe]:
+  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
+  by simp
+
+lemma less_eq_index_code [code nbe]:
   "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   by simp
 
-lemma less_index_code [code]:
+lemma less_index_code [code nbe]:
   "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   by simp
 
-instance by default (auto simp add: left_distrib index)
-
-end
-
 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
 
 lemma index_of_nat_code [code]:
@@ -222,9 +228,7 @@
 lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
   by (cases i) auto
 
-definition
-  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
-where
+definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   "nat_of_index_aux i n = nat_of_index i + n"
 
 lemma nat_of_index_aux_code [code]:
@@ -235,39 +239,7 @@
   "nat_of_index i = nat_of_index_aux i 0"
   by (simp add: nat_of_index_aux_def)
 
-
-text {* Measure function (for termination proofs) *}
-
-lemma [measure_function]:
-  "is_measure nat_of_index" by (rule is_measure_trivial)
-
-subsection {* ML interface *}
-
-ML {*
-structure Index =
-struct
-
-fun mk k = HOLogic.mk_number @{typ index} k;
-
-end;
-*}
-
-
-subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
-  @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
-  operations *}
-
-definition
-  minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
-where
-  [code del]: "minus_index_aux = op -"
-
-lemma [code]: "op - = minus_index_aux"
-  using minus_index_aux_def ..
-
-definition
-  div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
-where
+definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   [code del]: "div_mod_index n m = (n div m, n mod m)"
 
 lemma [code]:
@@ -283,6 +255,18 @@
   unfolding div_mod_index_def by simp
 
 
+subsection {* ML interface *}
+
+ML {*
+structure Index =
+struct
+
+fun mk k = HOLogic.mk_number @{typ index} k;
+
+end;
+*}
+
+
 subsection {* Code generator setup *}
 
 text {* Implementation of indices by bounded integers *}
@@ -308,7 +292,7 @@
   (OCaml "Pervasives.( + )")
   (Haskell infixl 6 "+")
 
-code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")