equal
deleted
inserted
replaced
14 |
14 |
15 definition int_of_real :: "real \<Rightarrow> int" |
15 definition int_of_real :: "real \<Rightarrow> int" |
16 where "int_of_real x = (SOME y. real_of_int y = x)" |
16 where "int_of_real x = (SOME y. real_of_int y = x)" |
17 |
17 |
18 definition real_is_int :: "real \<Rightarrow> bool" |
18 definition real_is_int :: "real \<Rightarrow> bool" |
19 where "real_is_int x = (EX (u::int). x = real_of_int u)" |
19 where "real_is_int x = (\<exists>(u::int). x = real_of_int u)" |
20 |
20 |
21 lemma real_is_int_def2: "real_is_int x = (x = real_of_int (int_of_real x))" |
21 lemma real_is_int_def2: "real_is_int x = (x = real_of_int (int_of_real x))" |
22 by (auto simp add: real_is_int_def int_of_real_def) |
22 by (auto simp add: real_is_int_def int_of_real_def) |
23 |
23 |
24 lemma real_is_int_real[simp]: "real_is_int (real_of_int (x::int))" |
24 lemma real_is_int_real[simp]: "real_is_int (real_of_int (x::int))" |