src/HOL/Real/RealDef.thy

 by simp
  
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
-
-subsection {* Implementation of rational real numbers as pairs of integers *}
-
-definition
-  Ratreal :: "int \<times> int \<Rightarrow> real"
-where
-  "Ratreal = INum"
-
-code_datatype Ratreal
-
-lemma Ratreal_simp:
-  "Ratreal (k, l) = real_of_int k / real_of_int l"
-  unfolding Ratreal_def INum_def by simp
-
-lemma Ratreal_zero [simp]: "Ratreal 0\<^sub>N = 0"
-  by (simp add: Ratreal_simp)
-
-lemma Ratreal_lit [simp]: "Ratreal i\<^sub>N = real_of_int i"
-  by (simp add: Ratreal_simp)
-
-lemma zero_real_code [code, code unfold]:
-  "0 = Ratreal 0\<^sub>N" by simp
-declare zero_real_code [symmetric, code post]
-
-lemma one_real_code [code, code unfold]:
-  "1 = Ratreal 1\<^sub>N" by simp
-declare one_real_code [symmetric, code post]
-
-instantiation real :: eq
-begin
-
-definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
-
-instance by default (simp add: eq_real_def)
-
-lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
-  unfolding Ratreal_def INum_normNum_iff eq ..
-
-end
-
-lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
-proof -
-  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) \<le> Ratreal (normNum y)" 
-    by (simp add: Ratreal_def del: normNum)
-  also have "\<dots> = (Ratreal x \<le> Ratreal y)" by (simp add: Ratreal_def)
-  finally show ?thesis by simp
-qed
-
-lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
-proof -
-  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) < Ratreal (normNum y)" 
-    by (simp add: Ratreal_def del: normNum)
-  also have "\<dots> = (Ratreal x < Ratreal y)" by (simp add: Ratreal_def)
-  finally show ?thesis by simp
-qed
-
-lemma real_add_code [code]: "Ratreal x + Ratreal y = Ratreal (x +\<^sub>N y)"
-  unfolding Ratreal_def by simp
-
-lemma real_mul_code [code]: "Ratreal x * Ratreal y = Ratreal (x *\<^sub>N y)"
-  unfolding Ratreal_def by simp
-
-lemma real_neg_code [code]: "- Ratreal x = Ratreal (~\<^sub>N x)"
-  unfolding Ratreal_def by simp
-
-lemma real_sub_code [code]: "Ratreal x - Ratreal y = Ratreal (x -\<^sub>N y)"
-  unfolding Ratreal_def by simp
-
-lemma real_inv_code [code]: "inverse (Ratreal x) = Ratreal (Ninv x)"
-  unfolding Ratreal_def Ninv real_divide_def by simp
-
-lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
-  unfolding Ratreal_def by simp
-
 instance real :: lordered_ring
 proof
   fix a::real
   show "abs a = sup a (-a)"
     by (auto simp add: real_abs_def sup_real_def)
 qed
+
+
+subsection {* Implementation of rational real numbers as pairs of integers *}
+
+definition
+  Ratreal :: "int \<times> int \<Rightarrow> real"
+where
+  "Ratreal = INum"
+
+code_datatype Ratreal
+
+lemma Ratreal_simp:
+  "Ratreal (k, l) = real_of_int k / real_of_int l"
+  unfolding Ratreal_def INum_def by simp
+
+lemma Ratreal_zero [simp]: "Ratreal 0\<^sub>N = 0"
+  by (simp add: Ratreal_simp)
+
+lemma Ratreal_lit [simp]: "Ratreal i\<^sub>N = real_of_int i"
+  by (simp add: Ratreal_simp)
+
+lemma zero_real_code [code, code unfold]:
+  "0 = Ratreal 0\<^sub>N" by simp
+declare zero_real_code [symmetric, code post]
+
+lemma one_real_code [code, code unfold]:
+  "1 = Ratreal 1\<^sub>N" by simp
+declare one_real_code [symmetric, code post]
+
+instantiation real :: eq
+begin
+
+definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x = y"
+
+instance by default (simp add: eq_real_def)
+
+lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
+  unfolding Ratreal_def INum_normNum_iff eq ..
+
+end
+
+lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
+proof -
+  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) \<le> Ratreal (normNum y)" 
+    by (simp add: Ratreal_def del: normNum)
+  also have "\<dots> = (Ratreal x \<le> Ratreal y)" by (simp add: Ratreal_def)
+  finally show ?thesis by simp
+qed
+
+lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
+proof -
+  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) < Ratreal (normNum y)" 
+    by (simp add: Ratreal_def del: normNum)
+  also have "\<dots> = (Ratreal x < Ratreal y)" by (simp add: Ratreal_def)
+  finally show ?thesis by simp
+qed
+
+lemma real_add_code [code]: "Ratreal x + Ratreal y = Ratreal (x +\<^sub>N y)"
+  unfolding Ratreal_def by simp
+
+lemma real_mul_code [code]: "Ratreal x * Ratreal y = Ratreal (x *\<^sub>N y)"
+  unfolding Ratreal_def by simp
+
+lemma real_neg_code [code]: "- Ratreal x = Ratreal (~\<^sub>N x)"
+  unfolding Ratreal_def by simp
+
+lemma real_sub_code [code]: "Ratreal x - Ratreal y = Ratreal (x -\<^sub>N y)"
+  unfolding Ratreal_def by simp
+
+lemma real_inv_code [code]: "inverse (Ratreal x) = Ratreal (Ninv x)"
+  unfolding Ratreal_def Ninv real_divide_def by simp
+
+lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
+  unfolding Ratreal_def by simp
 
 text {* Setup for SML code generator *}
 
 types_code
   real ("(int */ int)")