equal
deleted
inserted
replaced
77 lemma [code]: |
77 lemma [code]: |
78 "k mod l = int_of_integer (of_int k mod of_int l)" |
78 "k mod l = int_of_integer (of_int k mod of_int l)" |
79 by simp |
79 by simp |
80 |
80 |
81 lemma [code]: |
81 lemma [code]: |
|
82 "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)" |
|
83 unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv |
|
84 by transfer simp |
|
85 |
|
86 lemma [code]: |
82 "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" |
87 "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" |
83 by transfer (simp add: equal) |
88 by transfer (simp add: equal) |
84 |
89 |
85 lemma [code]: |
90 lemma [code]: |
86 "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l" |
91 "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l" |