author haftmann Mon Jan 21 08:43:27 2008 +0100 (2008-01-21) changeset 25928 042e877d9841 parent 25927 9c544dac6269 child 25929 6bfef23e26be
tuned code setup
 src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Library/Code_Index.thy file | annotate | diff | revisions src/HOL/Library/Code_Integer.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Int.thy	Fri Jan 18 20:34:28 2008 +0100
1.2 +++ b/src/HOL/Int.thy	Mon Jan 21 08:43:27 2008 +0100
1.3 @@ -1610,8 +1610,8 @@
1.4    with ge show ?thesis by fast
1.5  qed
1.6
1.7 -                     (* `set:int': dummy construction *)
1.8 -theorem int_gr_induct[case_names base step,induct set:int]:
1.9 +(* `set:int': dummy construction *)
1.10 +theorem int_gr_induct [case_names base step, induct set: int]:
1.11    assumes gr: "k < (i::int)" and
1.12          base: "P(k+1)" and
1.13          step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1.14 @@ -1737,16 +1737,13 @@
1.15
1.16  definition
1.17    int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
1.18 -  "int_aux n i = int n + i"
1.19 +  [code func del]: "int_aux = of_nat_aux"
1.20
1.21 -lemma [code]:
1.22 -  "int_aux 0 i  = i"
1.23 -  "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
1.24 -  by (simp add: int_aux_def)+
1.25 +lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
1.26
1.27  lemma [code, code unfold, code inline del]:
1.28 -  "int n = int_aux n 0"
1.29 -  by (simp add: int_aux_def)
1.30 +  "of_nat n = int_aux n 0"
1.31 +  by (simp add: int_aux_def of_nat_aux_def)
1.32
1.33  definition
1.34    nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
1.35 @@ -1760,6 +1757,8 @@
1.36  lemma [code]: "nat i = nat_aux i 0"
1.38
1.39 +hide (open) const int_aux nat_aux
1.40 +
1.41  lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
1.42    "(0\<Colon>int) = Numeral0"
1.43    by simp
1.44 @@ -1769,22 +1768,13 @@
1.45    by simp
1.46
1.47  code_modulename SML
1.48 -  IntDef Integer
1.49 +  Int Integer
1.50
1.51  code_modulename OCaml
1.52 -  IntDef Integer
1.53 +  Int Integer
1.54
1.56 -  IntDef Integer
1.57 -
1.58 -code_modulename SML
1.59 -  Numeral Integer
1.60 -
1.61 -code_modulename OCaml
1.62 -  Numeral Integer
1.63 -
1.65 -  Numeral Integer
1.66 +  Int Integer
1.67
1.68  types_code
1.69    "int" ("int")
```
```     2.1 --- a/src/HOL/Library/Code_Index.thy	Fri Jan 18 20:34:28 2008 +0100
2.2 +++ b/src/HOL/Library/Code_Index.thy	Mon Jan 21 08:43:27 2008 +0100
2.3 @@ -133,7 +133,7 @@
2.4
2.5  end
2.6
2.7 -lemma index_of_nat_code [code func]:
2.8 +lemma index_of_nat_code [code]:
2.9    "index_of_nat = of_nat"
2.10  proof
2.11    fix n :: nat
2.12 @@ -143,9 +143,21 @@
2.13      by (rule sym)
2.14  qed
2.15
2.16 -lemma nat_of_index_code [code func]:
2.17 -  "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
2.18 -  by (induct n) simp
2.19 +lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
2.20 +  by (cases i) auto
2.21 +
2.22 +definition
2.23 +  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
2.24 +where
2.25 +  "nat_of_index_aux i n = nat_of_index i + n"
2.26 +
2.27 +lemma nat_of_index_aux_code [code]:
2.28 +  "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
2.29 +  by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
2.30 +
2.31 +lemma nat_of_index_code [code]:
2.32 +  "nat_of_index i = nat_of_index_aux i 0"
2.33 +  by (simp add: nat_of_index_aux_def)
2.34
2.35
2.36  subsection {* ML interface *}
2.37 @@ -154,7 +166,7 @@
2.38  structure Index =
2.39  struct
2.40
2.41 -fun mk k = @{term index_of_nat} \$ HOLogic.mk_number @{typ index} k;
2.42 +fun mk k = HOLogic.mk_number @{typ index} k;
2.43
2.44  end;
2.45  *}
2.46 @@ -173,19 +185,15 @@
2.48
2.49  setup {*
2.50 -  fold (fn target => CodeTarget.add_pretty_numeral target false
2.51 -    @{const_name number_index_inst.number_of_index}
2.52 -    @{const_name Int.B0} @{const_name Int.B1}
2.53 -    @{const_name Int.Pls} @{const_name Int.Min}
2.54 -    @{const_name Int.Bit}
2.55 -  ) ["SML", "OCaml", "Haskell"]
2.56 +  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
2.57 +    false false) ["SML", "OCaml", "Haskell"]
2.58  *}
2.59
2.60  code_reserved SML Int int
2.61  code_reserved OCaml Pervasives int
2.62
2.63  code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.64 -  (SML "Int.+ ((_), (_))")
2.65 +  (SML "Int.+/ ((_),/ (_))")
2.66    (OCaml "Pervasives.+")
2.68
2.69 @@ -195,33 +203,33 @@
2.70    (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
2.71
2.72  code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.73 -  (SML "Int.* ((_), (_))")
2.74 +  (SML "Int.*/ ((_),/ (_))")
2.75    (OCaml "Pervasives.*")
2.77
2.78 +code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.79 +  (SML "Int.div/ ((_),/ (_))")
2.80 +  (OCaml "Pervasives.div")
2.82 +
2.83 +code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.84 +  (SML "Int.mod/ ((_),/ (_))")
2.85 +  (OCaml "Pervasives.mod")
2.87 +
2.88  code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
2.89    (SML "!((_ : Int.int) = _)")
2.90    (OCaml "!((_ : Pervasives.int) = _)")
2.92
2.93  code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
2.94 -  (SML "Int.<= ((_), (_))")
2.95 +  (SML "Int.<=/ ((_),/ (_))")
2.96    (OCaml "!((_ : Pervasives.int) <= _)")
2.98
2.99  code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
2.100 -  (SML "Int.< ((_), (_))")
2.101 +  (SML "Int.</ ((_),/ (_))")
2.102    (OCaml "!((_ : Pervasives.int) < _)")
2.104
2.105 -code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.106 -  (SML "IntInf.div ((_), (_))")
2.107 -  (OCaml "Big'_int.div'_big'_int")
2.109 -
2.110 -code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
2.111 -  (SML "IntInf.mod ((_), (_))")
2.112 -  (OCaml "Big'_int.mod'_big'_int")
2.114 -
2.115  end
```
```     3.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jan 18 20:34:28 2008 +0100
3.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Jan 21 08:43:27 2008 +0100
3.3 @@ -24,12 +24,8 @@
3.5
3.6  setup {*
3.7 -  fold (fn target => CodeTarget.add_pretty_numeral target true
3.8 -    @{const_name number_int_inst.number_of_int}
3.9 -    @{const_name Int.B0} @{const_name Int.B1}
3.10 -    @{const_name Int.Pls} @{const_name Int.Min}
3.11 -    @{const_name Int.Bit}
3.12 -  ) ["SML", "OCaml", "Haskell"]
3.13 +  fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
3.14 +    true true) ["SML", "OCaml", "Haskell"]
3.15  *}
3.16
3.17  code_const "Int.Pls" and "Int.Min" and "Int.Bit"
```
```     4.1 --- a/src/HOL/Nat.thy	Fri Jan 18 20:34:28 2008 +0100
4.2 +++ b/src/HOL/Nat.thy	Mon Jan 21 08:43:27 2008 +0100
4.3 @@ -1176,6 +1176,20 @@
4.4  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
4.6
4.7 +definition
4.8 +  of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
4.9 +where
4.10 +  [code func del]: "of_nat_aux n i = of_nat n + i"
4.11 +
4.12 +lemma of_nat_aux_code [code]:
4.13 +  "of_nat_aux 0 i = i"
4.14 +  "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *}