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.32    by (induct n) (simp_all add: of_rat_add)
    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