src/HOL/Presburger.thy
 changeset 23856 ebec38420a85 parent 23685 1b0f4071946c child 24075 366d4d234814
```     1.1 --- a/src/HOL/Presburger.thy	Thu Jul 19 21:47:42 2007 +0200
1.2 +++ b/src/HOL/Presburger.thy	Thu Jul 19 21:47:43 2007 +0200
1.3 @@ -703,4 +703,37 @@
1.4    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
1.5    less_number_of
1.6
1.7 +
1.8 +lemma of_int_num [code func]:
1.9 +  "of_int k = (if k = 0 then 0 else if k < 0 then
1.10 +     - of_int (- k) else let
1.11 +       (l, m) = divAlg (k, 2);
1.12 +       l' = of_int l
1.13 +     in if m = 0 then l' + l' else l' + l' + 1)"
1.14 +proof -
1.15 +  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow>
1.16 +    of_int k = of_int (k div 2 * 2 + 1)"
1.17 +  proof -
1.18 +    assume "k mod 2 \<noteq> 0"
1.19 +    then have "k mod 2 = 1" by arith
1.20 +    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
1.21 +    ultimately show ?thesis by auto
1.22 +  qed
1.23 +  have aux2: "\<And>x. of_int 2 * x = x + x"
1.24 +  proof -
1.25 +    fix x
1.26 +    have int2: "(2::int) = 1 + 1" by arith
1.27 +    show "of_int 2 * x = x + x"
1.28 +    unfolding int2 of_int_add left_distrib by simp
1.29 +  qed
1.30 +  have aux3: "\<And>x. x * of_int 2 = x + x"
1.31 +  proof -
1.32 +    fix x
1.33 +    have int2: "(2::int) = 1 + 1" by arith
1.34 +    show "x * of_int 2 = x + x"
1.35 +    unfolding int2 of_int_add right_distrib by simp
1.36 +  qed
1.37 +  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
1.38 +qed
1.39 +
1.40  end
```