moved some code lemmas for Numerals here
authorhaftmann
Wed Apr 02 15:58:26 2008 +0200 (2008-04-02)
changeset 265076da615cef733
parent 26506 c4202c67fe3e
child 26508 4cd7c4f936bb
moved some code lemmas for Numerals here
src/HOL/Int.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Int.thy	Wed Apr 02 12:32:53 2008 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Apr 02 15:58:26 2008 +0200
     1.3 @@ -1797,9 +1797,125 @@
     1.4  
     1.5  subsection {* Configuration of the code generator *}
     1.6  
     1.7 -instance int :: eq ..
     1.8 +code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
     1.9 +
    1.10 +lemmas pred_succ_numeral_code [code func] =
    1.11 +  pred_bin_simps succ_bin_simps
    1.12 +
    1.13 +lemmas plus_numeral_code [code func] =
    1.14 +  add_bin_simps
    1.15 +  arith_extra_simps(1) [where 'a = int]
    1.16 +
    1.17 +lemmas minus_numeral_code [code func] =
    1.18 +  minus_bin_simps
    1.19 +  arith_extra_simps(2) [where 'a = int]
    1.20 +  arith_extra_simps(5) [where 'a = int]
    1.21 +
    1.22 +lemmas times_numeral_code [code func] =
    1.23 +  mult_bin_simps
    1.24 +  arith_extra_simps(4) [where 'a = int]
    1.25 +
    1.26 +instantiation int :: eq
    1.27 +begin
    1.28 +
    1.29 +definition [code func del]: "eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
    1.30 +
    1.31 +instance by default (simp add: eq_int_def)
    1.32 +
    1.33 +end
    1.34 +
    1.35 +lemma eq_number_of_int_code [code func]:
    1.36 +  "eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq k l"
    1.37 +  unfolding eq_int_def number_of_is_id ..
    1.38 +
    1.39 +lemma eq_int_code [code func]:
    1.40 +  "eq Int.Pls Int.Pls \<longleftrightarrow> True"
    1.41 +  "eq Int.Pls Int.Min \<longleftrightarrow> False"
    1.42 +  "eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq Int.Pls k2"
    1.43 +  "eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
    1.44 +  "eq Int.Min Int.Pls \<longleftrightarrow> False"
    1.45 +  "eq Int.Min Int.Min \<longleftrightarrow> True"
    1.46 +  "eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
    1.47 +  "eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq Int.Min k2"
    1.48 +  "eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq Int.Pls k1"
    1.49 +  "eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
    1.50 +  "eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
    1.51 +  "eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq Int.Min k1"
    1.52 +  "eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq k1 k2"
    1.53 +  "eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
    1.54 +  "eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
    1.55 +  "eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq k1 k2"
    1.56 +  unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
    1.57 +    eq_number_of_int_code [symmetric, of Int.Min]
    1.58 +    eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
    1.59 +    eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
    1.60 +    eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
    1.61 +    eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
    1.62 +  by (simp_all add: eq Pls_def,
    1.63 +    simp_all only: Min_def succ_def pred_def number_of_is_id)
    1.64 +    (auto simp add: iszero_def)
    1.65  
    1.66 -code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
    1.67 +lemma less_eq_number_of_int_code [code func]:
    1.68 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    1.69 +  unfolding number_of_is_id ..
    1.70 +
    1.71 +lemma less_eq_int_code [code func]:
    1.72 +  "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
    1.73 +  "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
    1.74 +  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
    1.75 +  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
    1.76 +  "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
    1.77 +  "Int.Min \<le> Int.Min \<longleftrightarrow> True"
    1.78 +  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
    1.79 +  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
    1.80 +  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
    1.81 +  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
    1.82 +  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
    1.83 +  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
    1.84 +  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
    1.85 +  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
    1.86 +  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
    1.87 +  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
    1.88 +  unfolding less_eq_number_of_int_code [symmetric, of Int.Pls] 
    1.89 +    less_eq_number_of_int_code [symmetric, of Int.Min]
    1.90 +    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
    1.91 +    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
    1.92 +    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
    1.93 +    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
    1.94 +  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
    1.95 +    (auto simp add: neg_def linorder_not_less group_simps
    1.96 +      zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
    1.97 +
    1.98 +lemma less_number_of_int_code [code func]:
    1.99 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   1.100 +  unfolding number_of_is_id ..
   1.101 +
   1.102 +lemma less_int_code [code func]:
   1.103 +  "Int.Pls < Int.Pls \<longleftrightarrow> False"
   1.104 +  "Int.Pls < Int.Min \<longleftrightarrow> False"
   1.105 +  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
   1.106 +  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
   1.107 +  "Int.Min < Int.Pls \<longleftrightarrow> True"
   1.108 +  "Int.Min < Int.Min \<longleftrightarrow> False"
   1.109 +  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   1.110 +  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
   1.111 +  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.112 +  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.113 +  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.114 +  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
   1.115 +  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.116 +  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.117 +  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.118 +  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
   1.119 +  unfolding less_number_of_int_code [symmetric, of Int.Pls] 
   1.120 +    less_number_of_int_code [symmetric, of Int.Min]
   1.121 +    less_number_of_int_code [symmetric, of "Int.Bit0 k1"]
   1.122 +    less_number_of_int_code [symmetric, of "Int.Bit1 k1"]
   1.123 +    less_number_of_int_code [symmetric, of "Int.Bit0 k2"]
   1.124 +    less_number_of_int_code [symmetric, of "Int.Bit1 k2"]
   1.125 +  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
   1.126 +    (auto simp add: neg_def group_simps zle_add1_eq_le [symmetric] del: iffI,
   1.127 +      auto simp only: Bit0_def Bit1_def)
   1.128  
   1.129  definition
   1.130    int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
     2.1 --- a/src/HOL/IntDiv.thy	Wed Apr 02 12:32:53 2008 +0200
     2.2 +++ b/src/HOL/IntDiv.thy	Wed Apr 02 15:58:26 2008 +0200
     2.3 @@ -1486,6 +1486,45 @@
     2.4  
     2.5  text {* code generator setup *}
     2.6  
     2.7 +context ring_1
     2.8 +begin
     2.9 +
    2.10 +lemma of_int_num [code func]:
    2.11 +  "of_int k = (if k = 0 then 0 else if k < 0 then
    2.12 +     - of_int (- k) else let
    2.13 +       (l, m) = divAlg (k, 2);
    2.14 +       l' = of_int l
    2.15 +     in if m = 0 then l' + l' else l' + l' + 1)"
    2.16 +proof -
    2.17 +  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
    2.18 +    of_int k = of_int (k div 2 * 2 + 1)"
    2.19 +  proof -
    2.20 +    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
    2.21 +    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
    2.22 +    moreover assume "k mod 2 \<noteq> 0"
    2.23 +    ultimately have "k mod 2 = 1" by arith
    2.24 +    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    2.25 +    ultimately show ?thesis by auto
    2.26 +  qed
    2.27 +  have aux2: "\<And>x. of_int 2 * x = x + x"
    2.28 +  proof -
    2.29 +    fix x
    2.30 +    have int2: "(2::int) = 1 + 1" by arith
    2.31 +    show "of_int 2 * x = x + x"
    2.32 +    unfolding int2 of_int_add left_distrib by simp
    2.33 +  qed
    2.34 +  have aux3: "\<And>x. x * of_int 2 = x + x"
    2.35 +  proof -
    2.36 +    fix x
    2.37 +    have int2: "(2::int) = 1 + 1" by arith
    2.38 +    show "x * of_int 2 = x + x" 
    2.39 +    unfolding int2 of_int_add right_distrib by simp
    2.40 +  qed
    2.41 +  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
    2.42 +qed
    2.43 +
    2.44 +end
    2.45 +
    2.46  code_modulename SML
    2.47    IntDiv Integer
    2.48