improvements for codegen 2
authorhaftmann
Wed Sep 20 12:24:28 2006 +0200 (2006-09-20)
changeset 2064112554634e552
parent 20640 05e6042394b9
child 20642 cfe2b0803a51
improvements for codegen 2
src/HOL/Library/EfficientNat.thy
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Sep 20 12:24:11 2006 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Sep 20 12:24:28 2006 +0200
     1.3 @@ -51,37 +51,22 @@
     1.4  *}
     1.5    int ("(_)")
     1.6  
     1.7 -definition
     1.8 -  "nat_plus m n = nat (int m + int n)"
     1.9 -  "nat_minus m n = nat (int m - int n)"
    1.10 -  "nat_mult m n = nat (int m * int n)"
    1.11 -  "nat_div m n = nat (fst (divAlg (int m, int n)))"
    1.12 -  "nat_mod m n = nat (snd (divAlg (int m, int n)))"
    1.13 -  "nat_less m n = (int m < int n)"
    1.14 -  "nat_less_equal m n = (int m <= int n)"
    1.15 -  "nat_eq m n = (int m = int n)"
    1.16 +ML {* set Toplevel.debug *}
    1.17 +setup {*
    1.18 +  CodegenData.del_datatype "nat"
    1.19 +*}
    1.20  
    1.21  code_type nat
    1.22    (SML target_atom "IntInf.int")
    1.23    (Haskell target_atom "Integer")
    1.24  
    1.25 -code_const "0::nat" and Suc (*all constructors of nat must be hidden*)
    1.26 -  (SML target_atom "(0 :: IntInf.int)" and "IntInf.+ (_, 1)")
    1.27 -  (Haskell target_atom "0" and "(+) 1 _")
    1.28 -
    1.29 -code_const nat and int
    1.30 -  (SML target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)" and "_")
    1.31 -  (Haskell target_atom "(\\n :: Int -> if n < 0 then 0 else n)" and "_")
    1.32 +code_const int
    1.33 +  (SML "_")
    1.34 +  (Haskell "_")
    1.35  
    1.36 -text {*
    1.37 -  Eliminate @{const "0::nat"} and @{const "1::nat"}
    1.38 -  by unfolding in place.
    1.39 -*}
    1.40 -
    1.41 -lemma [code inline]:
    1.42 -  "0 = nat 0"
    1.43 -  "1 = nat 1"
    1.44 -by (simp_all add: expand_fun_eq)
    1.45 +definition
    1.46 +  nat_of_int :: "int \<Rightarrow> nat"
    1.47 +  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
    1.48  
    1.49  text {*
    1.50  Case analysis on natural numbers is rephrased using a conditional
    1.51 @@ -99,38 +84,72 @@
    1.52  using their counterparts on the integers:
    1.53  *}
    1.54  
    1.55 -lemma [code]: "m + n = nat (int m + int n)"
    1.56 -  by arith
    1.57 -lemma [code]: "m - n = nat (int m - int n)"
    1.58 -  by arith
    1.59 -lemma [code]: "m * n = nat (int m * int n)"
    1.60 -  by (simp add: zmult_int)
    1.61 -lemma [code]: "m div n = nat (int m div int n)"
    1.62 -  by (simp add: zdiv_int [symmetric])
    1.63 -lemma [code]: "m mod n = nat (int m mod int n)"
    1.64 -  by (simp add: zmod_int [symmetric])
    1.65 -lemma [code]: "(m < n) = (int m < int n)"
    1.66 -  by simp
    1.67 +code_constname
    1.68 +  nat_of_int "IntDef.nat_of_int"
    1.69 +
    1.70 +code_const nat_of_int
    1.71 +  (SML "_")
    1.72 +  (Haskell "_")
    1.73  
    1.74 -lemma [code func, code inline]: "m + n = nat_plus m n"
    1.75 -  unfolding nat_plus_def by arith
    1.76 -lemma [code func, code inline]: "m - n = nat_minus m n"
    1.77 -  unfolding nat_minus_def by arith
    1.78 -lemma [code func, code inline]: "m * n = nat_mult m n"
    1.79 -  unfolding nat_mult_def by (simp add: zmult_int)
    1.80 -lemma [code func, code inline]: "m div n = nat_div m n"
    1.81 -  unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp
    1.82 -lemma [code func, code inline]: "m mod n = nat_mod m n"
    1.83 -  unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp
    1.84 -lemma [code func, code inline]: "(m < n) = nat_less m n"
    1.85 -  unfolding nat_less_def by simp
    1.86 -lemma [code func, code inline]: "(m <= n) = nat_less_equal m n"
    1.87 -  unfolding nat_less_equal_def by simp
    1.88 -lemma [code func, code inline]: "OperationalEquality.eq m n = nat_eq m n"
    1.89 -  unfolding nat_eq_def eq_def by simp
    1.90 +lemma [code func]: "0 = nat_of_int 0"
    1.91 +  by (simp add: nat_of_int_def)
    1.92 +lemma [code func, code inline]:  "1 = nat_of_int 1"
    1.93 +  by (simp add: nat_of_int_def)
    1.94 +lemma [code func]: "Suc n = n + 1"
    1.95 +  by simp
    1.96 +lemma [code, code inline]: "m + n = nat (int m + int n)"
    1.97 +  by arith
    1.98 +lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
    1.99 +  by (simp add: nat_of_int_def)
   1.100 +lemma [code, code inline]: "m - n = nat (int m - int n)"
   1.101 +  by arith
   1.102 +lemma [code, code inline]: "m * n = nat (int m * int n)"
   1.103 +  unfolding zmult_int by simp
   1.104 +lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
   1.105 +proof -
   1.106 +  have "int (m * n) = int m * int n"
   1.107 +    by (induct m) (simp_all add: zadd_zmult_distrib)
   1.108 +  then have "m * n = nat (int m * int n)" by auto
   1.109 +  also have "\<dots> = nat_of_int (int m * int n)"
   1.110 +  proof -
   1.111 +    have "int m \<ge> 0" and "int n \<ge> 0" by auto
   1.112 +    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
   1.113 +    with nat_of_int_def show ?thesis by auto
   1.114 +  qed
   1.115 +  finally show ?thesis .
   1.116 +qed  
   1.117 +lemma [code]: "m div n = nat (int m div int n)"
   1.118 +  unfolding zdiv_int [symmetric] by simp
   1.119 +lemma [code func]: "m div n = fst (Divides.divmod m n)"
   1.120 +  unfolding divmod_def by simp
   1.121 +lemma [code]: "m mod n = nat (int m mod int n)"
   1.122 +  unfolding zmod_int [symmetric] by simp
   1.123 +lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   1.124 +  unfolding divmod_def by simp
   1.125 +lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
   1.126 +  by simp
   1.127 +lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
   1.128 +  by simp
   1.129 +lemma [code func, code inline]: "OperationalEquality.eq m n \<longleftrightarrow> OperationalEquality.eq (int m) (int n)"
   1.130 +  unfolding eq_def by simp
   1.131 +lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
   1.132 +proof (cases "k < 0")
   1.133 +  case True then show ?thesis by simp
   1.134 +next
   1.135 +  case False then show ?thesis by (simp add: nat_of_int_def)
   1.136 +qed
   1.137  lemma [code func]:
   1.138 -  "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))"
   1.139 -  unfolding nat_eq_def nat_minus_def int_aux_def by simp
   1.140 +  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
   1.141 +proof -
   1.142 +  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
   1.143 +  proof -
   1.144 +    assume prem: "n > 0"
   1.145 +    then have "int n - 1 \<ge> 0" by auto
   1.146 +    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
   1.147 +    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
   1.148 +  qed
   1.149 +  then show ?thesis unfolding int_aux_def by simp
   1.150 +qed
   1.151  
   1.152  
   1.153  subsection {* Preprocessors *}