author bulwahn Sat, 09 Jul 2011 19:28:33 +0200 changeset 43733 a6ca7b83612f parent 43732 6b2bdc57155b child 43734 ea147bec4f72
adding code equations to execute floor and ceiling on rational and real numbers
 src/HOL/Archimedean_Field.thy file | annotate | diff | comparison | revisions src/HOL/Rat.thy file | annotate | diff | comparison | revisions src/HOL/RealDef.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Archimedean_Field.thy	Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy	Sat Jul 09 19:28:33 2011 +0200
@@ -271,7 +271,7 @@

definition
ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
-  [code del]: "ceiling x = - floor (- x)"
+  "ceiling x = - floor (- x)"

notation (xsymbols)
ceiling  ("\<lceil>_\<rceil>")```
```--- a/src/HOL/Rat.thy	Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/Rat.thy	Sat Jul 09 19:28:33 2011 +0200
@@ -1097,6 +1097,10 @@
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
qed

+lemma rat_floor_code [code]:
+  "floor p = (let (a, b) = quotient_of p in a div b)"
+by (cases p) (simp add: quotient_of_Fract floor_Fract)
+
instantiation rat :: equal
begin
```
```--- a/src/HOL/RealDef.thy	Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/RealDef.thy	Sat Jul 09 19:28:33 2011 +0200
@@ -1762,6 +1762,9 @@
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"