src/HOL/Divides.thy
changeset 35673 178caf872f95
parent 35644 d20cf282342e
child 35815 10e723e54076
     1.1 --- a/src/HOL/Divides.thy	Mon Mar 08 14:41:56 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 09 15:47:15 2010 +0100
     1.3 @@ -376,7 +376,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class ring_div = semiring_div + idom
     1.8 +class ring_div = semiring_div + comm_ring_1
     1.9  begin
    1.10  
    1.11  text {* Negation respects modular equivalence. *}
    1.12 @@ -2353,47 +2353,6 @@
    1.13  apply (rule Divides.div_less_dividend, simp_all)
    1.14  done
    1.15  
    1.16 -text {* code generator setup *}
    1.17 -
    1.18 -context ring_1
    1.19 -begin
    1.20 -
    1.21 -lemma of_int_num [code]:
    1.22 -  "of_int k = (if k = 0 then 0 else if k < 0 then
    1.23 -     - of_int (- k) else let
    1.24 -       (l, m) = divmod_int k 2;
    1.25 -       l' = of_int l
    1.26 -     in if m = 0 then l' + l' else l' + l' + 1)"
    1.27 -proof -
    1.28 -  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
    1.29 -    of_int k = of_int (k div 2 * 2 + 1)"
    1.30 -  proof -
    1.31 -    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
    1.32 -    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
    1.33 -    moreover assume "k mod 2 \<noteq> 0"
    1.34 -    ultimately have "k mod 2 = 1" by arith
    1.35 -    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    1.36 -    ultimately show ?thesis by auto
    1.37 -  qed
    1.38 -  have aux2: "\<And>x. of_int 2 * x = x + x"
    1.39 -  proof -
    1.40 -    fix x
    1.41 -    have int2: "(2::int) = 1 + 1" by arith
    1.42 -    show "of_int 2 * x = x + x"
    1.43 -    unfolding int2 of_int_add left_distrib by simp
    1.44 -  qed
    1.45 -  have aux3: "\<And>x. x * of_int 2 = x + x"
    1.46 -  proof -
    1.47 -    fix x
    1.48 -    have int2: "(2::int) = 1 + 1" by arith
    1.49 -    show "x * of_int 2 = x + x" 
    1.50 -    unfolding int2 of_int_add right_distrib by simp
    1.51 -  qed
    1.52 -  from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
    1.53 -qed
    1.54 -
    1.55 -end
    1.56 -
    1.57  lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
    1.58  proof
    1.59    assume H: "x mod n = y mod n"
    1.60 @@ -2482,6 +2441,7 @@
    1.61                         mod_div_equality' [THEN eq_reflection]
    1.62                         zmod_zdiv_equality' [THEN eq_reflection]
    1.63  
    1.64 +
    1.65  subsubsection {* Code generation *}
    1.66  
    1.67  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.68 @@ -2515,6 +2475,45 @@
    1.69    then show ?thesis by (simp add: divmod_int_pdivmod)
    1.70  qed
    1.71  
    1.72 +context ring_1
    1.73 +begin
    1.74 +
    1.75 +lemma of_int_num [code]:
    1.76 +  "of_int k = (if k = 0 then 0 else if k < 0 then
    1.77 +     - of_int (- k) else let
    1.78 +       (l, m) = divmod_int k 2;
    1.79 +       l' = of_int l
    1.80 +     in if m = 0 then l' + l' else l' + l' + 1)"
    1.81 +proof -
    1.82 +  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
    1.83 +    of_int k = of_int (k div 2 * 2 + 1)"
    1.84 +  proof -
    1.85 +    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
    1.86 +    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
    1.87 +    moreover assume "k mod 2 \<noteq> 0"
    1.88 +    ultimately have "k mod 2 = 1" by arith
    1.89 +    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    1.90 +    ultimately show ?thesis by auto
    1.91 +  qed
    1.92 +  have aux2: "\<And>x. of_int 2 * x = x + x"
    1.93 +  proof -
    1.94 +    fix x
    1.95 +    have int2: "(2::int) = 1 + 1" by arith
    1.96 +    show "of_int 2 * x = x + x"
    1.97 +    unfolding int2 of_int_add left_distrib by simp
    1.98 +  qed
    1.99 +  have aux3: "\<And>x. x * of_int 2 = x + x"
   1.100 +  proof -
   1.101 +    fix x
   1.102 +    have int2: "(2::int) = 1 + 1" by arith
   1.103 +    show "x * of_int 2 = x + x" 
   1.104 +    unfolding int2 of_int_add right_distrib by simp
   1.105 +  qed
   1.106 +  from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
   1.107 +qed
   1.108 +
   1.109 +end
   1.110 +
   1.111  code_modulename SML
   1.112    Divides Arith
   1.113