tuned code setup
authorhaftmann
Mon Jan 21 08:43:27 2008 +0100 (2008-01-21)
changeset 25928042e877d9841
parent 25927 9c544dac6269
child 25929 6bfef23e26be
tuned code setup
src/HOL/Int.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Nat.thy
     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.37    by (simp add: nat_aux_def)
    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.55  code_modulename Haskell
    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.64 -code_modulename Haskell
    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.47    (Haskell -)
    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.67    (Haskell infixl 6 "+")
    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.76    (Haskell infixl 7 "*")
    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.81 +  (Haskell "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.86 +  (Haskell "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.91    (Haskell infixl 4 "==")
    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.97    (Haskell infix 4 "<=")
    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.103    (Haskell infix 4 "<")
   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.108 -  (Haskell "div")
   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.113 -  (Haskell "mod")
   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.4    (Haskell -)
     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.5    by (induct m) (simp_all add: add_ac left_distrib)
     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 *}
    4.15 +  by (simp_all add: of_nat_aux_def add_ac)
    4.16 +
    4.17 +lemma of_nat_code [code]:
    4.18 +  "of_nat n = of_nat_aux n 0"
    4.19 +  by (simp add: of_nat_aux_def)
    4.20 +
    4.21  end
    4.22  
    4.23  context ordered_semidom