src/HOL/IntDiv.thy
changeset 26507 6da615cef733
parent 26480 544cef16045b
child 27651 16a26996c30e
     1.1 --- a/src/HOL/IntDiv.thy	Wed Apr 02 12:32:53 2008 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Apr 02 15:58:26 2008 +0200
     1.3 @@ -1486,6 +1486,45 @@
     1.4  
     1.5  text {* code generator setup *}
     1.6  
     1.7 +context ring_1
     1.8 +begin
     1.9 +
    1.10 +lemma of_int_num [code func]:
    1.11 +  "of_int k = (if k = 0 then 0 else if k < 0 then
    1.12 +     - of_int (- k) else let
    1.13 +       (l, m) = divAlg (k, 2);
    1.14 +       l' = of_int l
    1.15 +     in if m = 0 then l' + l' else l' + l' + 1)"
    1.16 +proof -
    1.17 +  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
    1.18 +    of_int k = of_int (k div 2 * 2 + 1)"
    1.19 +  proof -
    1.20 +    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
    1.21 +    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
    1.22 +    moreover assume "k mod 2 \<noteq> 0"
    1.23 +    ultimately have "k mod 2 = 1" by arith
    1.24 +    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    1.25 +    ultimately show ?thesis by auto
    1.26 +  qed
    1.27 +  have aux2: "\<And>x. of_int 2 * x = x + x"
    1.28 +  proof -
    1.29 +    fix x
    1.30 +    have int2: "(2::int) = 1 + 1" by arith
    1.31 +    show "of_int 2 * x = x + x"
    1.32 +    unfolding int2 of_int_add left_distrib by simp
    1.33 +  qed
    1.34 +  have aux3: "\<And>x. x * of_int 2 = x + x"
    1.35 +  proof -
    1.36 +    fix x
    1.37 +    have int2: "(2::int) = 1 + 1" by arith
    1.38 +    show "x * of_int 2 = x + x" 
    1.39 +    unfolding int2 of_int_add right_distrib by simp
    1.40 +  qed
    1.41 +  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
    1.42 +qed
    1.43 +
    1.44 +end
    1.45 +
    1.46  code_modulename SML
    1.47    IntDiv Integer
    1.48