--- a/src/HOL/Int.thy Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Int.thy Mon Jan 21 08:43:27 2008 +0100
@@ -1610,8 +1610,8 @@
with ge show ?thesis by fast
qed
- (* `set:int': dummy construction *)
-theorem int_gr_induct[case_names base step,induct set:int]:
+(* `set:int': dummy construction *)
+theorem int_gr_induct [case_names base step, induct set: int]:
assumes gr: "k < (i::int)" and
base: "P(k+1)" and
step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
@@ -1737,16 +1737,13 @@
definition
int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
- "int_aux n i = int n + i"
+ [code func del]: "int_aux = of_nat_aux"
-lemma [code]:
- "int_aux 0 i = i"
- "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
- by (simp add: int_aux_def)+
+lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
lemma [code, code unfold, code inline del]:
- "int n = int_aux n 0"
- by (simp add: int_aux_def)
+ "of_nat n = int_aux n 0"
+ by (simp add: int_aux_def of_nat_aux_def)
definition
nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
@@ -1760,6 +1757,8 @@
lemma [code]: "nat i = nat_aux i 0"
by (simp add: nat_aux_def)
+hide (open) const int_aux nat_aux
+
lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
"(0\<Colon>int) = Numeral0"
by simp
@@ -1769,22 +1768,13 @@
by simp
code_modulename SML
- IntDef Integer
+ Int Integer
code_modulename OCaml
- IntDef Integer
+ Int Integer
code_modulename Haskell
- IntDef Integer
-
-code_modulename SML
- Numeral Integer
-
-code_modulename OCaml
- Numeral Integer
-
-code_modulename Haskell
- Numeral Integer
+ Int Integer
types_code
"int" ("int")
--- a/src/HOL/Library/Code_Index.thy Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy Mon Jan 21 08:43:27 2008 +0100
@@ -133,7 +133,7 @@
end
-lemma index_of_nat_code [code func]:
+lemma index_of_nat_code [code]:
"index_of_nat = of_nat"
proof
fix n :: nat
@@ -143,9 +143,21 @@
by (rule sym)
qed
-lemma nat_of_index_code [code func]:
- "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
- by (induct n) simp
+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
+ "nat_of_index_aux i n = nat_of_index i + n"
+
+lemma nat_of_index_aux_code [code]:
+ "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
+ by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
+
+lemma nat_of_index_code [code]:
+ "nat_of_index i = nat_of_index_aux i 0"
+ by (simp add: nat_of_index_aux_def)
subsection {* ML interface *}
@@ -154,7 +166,7 @@
structure Index =
struct
-fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;
+fun mk k = HOLogic.mk_number @{typ index} k;
end;
*}
@@ -173,19 +185,15 @@
(Haskell -)
setup {*
- fold (fn target => CodeTarget.add_pretty_numeral target false
- @{const_name number_index_inst.number_of_index}
- @{const_name Int.B0} @{const_name Int.B1}
- @{const_name Int.Pls} @{const_name Int.Min}
- @{const_name Int.Bit}
- ) ["SML", "OCaml", "Haskell"]
+ fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
+ false false) ["SML", "OCaml", "Haskell"]
*}
code_reserved SML Int int
code_reserved OCaml Pervasives int
code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.+ ((_), (_))")
+ (SML "Int.+/ ((_),/ (_))")
(OCaml "Pervasives.+")
(Haskell infixl 6 "+")
@@ -195,33 +203,33 @@
(Haskell "max/ (_/ -/ _)/ (0 :: Int)")
code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.* ((_), (_))")
+ (SML "Int.*/ ((_),/ (_))")
(OCaml "Pervasives.*")
(Haskell infixl 7 "*")
+code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+ (SML "Int.div/ ((_),/ (_))")
+ (OCaml "Pervasives.div")
+ (Haskell "div")
+
+code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+ (SML "Int.mod/ ((_),/ (_))")
+ (OCaml "Pervasives.mod")
+ (Haskell "mod")
+
code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "!((_ : Pervasives.int) = _)")
(Haskell infixl 4 "==")
code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.<= ((_), (_))")
+ (SML "Int.<=/ ((_),/ (_))")
(OCaml "!((_ : Pervasives.int) <= _)")
(Haskell infix 4 "<=")
code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.< ((_), (_))")
+ (SML "Int.</ ((_),/ (_))")
(OCaml "!((_ : Pervasives.int) < _)")
(Haskell infix 4 "<")
-code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "IntInf.div ((_), (_))")
- (OCaml "Big'_int.div'_big'_int")
- (Haskell "div")
-
-code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "IntInf.mod ((_), (_))")
- (OCaml "Big'_int.mod'_big'_int")
- (Haskell "mod")
-
end
--- a/src/HOL/Library/Code_Integer.thy Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy Mon Jan 21 08:43:27 2008 +0100
@@ -24,12 +24,8 @@
(Haskell -)
setup {*
- fold (fn target => CodeTarget.add_pretty_numeral target true
- @{const_name number_int_inst.number_of_int}
- @{const_name Int.B0} @{const_name Int.B1}
- @{const_name Int.Pls} @{const_name Int.Min}
- @{const_name Int.Bit}
- ) ["SML", "OCaml", "Haskell"]
+ fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
+ true true) ["SML", "OCaml", "Haskell"]
*}
code_const "Int.Pls" and "Int.Min" and "Int.Bit"
--- a/src/HOL/Nat.thy Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Nat.thy Mon Jan 21 08:43:27 2008 +0100
@@ -1176,6 +1176,20 @@
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
by (induct m) (simp_all add: add_ac left_distrib)
+definition
+ of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+ [code func del]: "of_nat_aux n i = of_nat n + i"
+
+lemma of_nat_aux_code [code]:
+ "of_nat_aux 0 i = i"
+ "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *}
+ by (simp_all add: of_nat_aux_def add_ac)
+
+lemma of_nat_code [code]:
+ "of_nat n = of_nat_aux n 0"
+ by (simp add: of_nat_aux_def)
+
end
context ordered_semidom