equal
deleted
inserted
replaced
87 |
87 |
88 lemma [code]: |
88 lemma [code]: |
89 "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
89 "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
90 by transfer rule |
90 by transfer rule |
91 |
91 |
92 lemma (in ring_1) of_int_code: |
92 lemma (in ring_1) of_int_code_if: |
93 "of_int k = (if k = 0 then 0 |
93 "of_int k = (if k = 0 then 0 |
94 else if k < 0 then - of_int (- k) |
94 else if k < 0 then - of_int (- k) |
95 else let |
95 else let |
96 (l, j) = divmod_int k 2; |
96 (l, j) = divmod_int k 2; |
97 l' = 2 * of_int l |
97 l' = 2 * of_int l |
98 in if j = 0 then l' else l' + 1)" |
98 in if j = 0 then l' else l' + 1)" |
99 proof - |
99 proof - |
100 from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
100 from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
101 show ?thesis |
101 show ?thesis |
102 by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1 |
102 by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric]) |
103 of_int_add [symmetric]) (simp add: * mult_commute) |
103 (simp add: * mult_commute) |
104 qed |
104 qed |
105 |
105 |
106 declare of_int_code [code] |
106 declare of_int_code_if [code] |
107 |
107 |
108 lemma [code]: |
108 lemma [code]: |
109 "nat = nat_of_integer \<circ> of_int" |
109 "nat = nat_of_integer \<circ> of_int" |
110 by transfer (simp add: fun_eq_iff) |
110 by transfer (simp add: fun_eq_iff) |
111 |
111 |