src/HOL/Rat.thy
 changeset 70350 571ae57313a4 parent 70347 e5cd5471c18a child 70356 4a327c061870
```     1.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
1.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
1.3 @@ -629,7 +629,8 @@
1.4  instantiation rat :: floor_ceiling
1.5  begin
1.6
1.7 -definition [code del]: "\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
1.8 +definition floor_rat :: "rat \<Rightarrow> int"
1.9 +  where"\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
1.10
1.11  instance
1.12  proof
1.13 @@ -639,7 +640,7 @@
1.14
1.15  end
1.16
1.17 -lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b"
1.18 +lemma floor_Fract [simp]: "\<lfloor>Fract a b\<rfloor> = a div b"
1.19    by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
1.20
1.21
1.22 @@ -788,6 +789,10 @@
1.23      by (induct a) (simp add: of_rat_rat Fract_of_int_eq [symmetric])
1.24  qed
1.25
1.26 +lemma abs_of_rat [simp]:
1.27 +  "\<bar>of_rat r\<bar> = (of_rat \<bar>r\<bar> :: 'a :: linordered_field)"
1.28 +  by (cases "r \<ge> 0") (simp_all add: not_le of_rat_minus)
1.29 +
1.30  text \<open>Collapse nested embeddings.\<close>
1.31  lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
1.33 @@ -801,6 +806,14 @@
1.34  lemma of_rat_neg_numeral_eq [simp]: "of_rat (- numeral w) = - numeral w"
1.35    using of_rat_of_int_eq [of "- numeral w"] by simp
1.36
1.37 +lemma of_rat_floor [simp]:
1.38 +  "\<lfloor>of_rat r\<rfloor> = \<lfloor>r\<rfloor>"
1.39 +  by (cases r) (simp add: Fract_of_int_quotient of_rat_divide floor_divide_of_int_eq)
1.40 +
1.41 +lemma of_rat_ceiling [simp]:
1.42 +  "\<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>"
1.43 +  using of_rat_floor [of "- r"] by (simp add: of_rat_minus ceiling_def)
1.44 +
1.45  lemmas zero_rat = Zero_rat_def
1.46  lemmas one_rat = One_rat_def
1.47
```