introduce real_of typeclass for real :: 'a => real

--- a/src/HOL/Library/Extended_Real.thy	Mon Aug 25 16:06:41 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon Aug 25 14:24:05 2014 +0200
@@ -91,21 +91,22 @@
   shows "-a = -b \<longleftrightarrow> a = b"
   by (cases rule: ereal2_cases[of a b]) simp_all
 
-function of_ereal :: "ereal \<Rightarrow> real" where
-  "of_ereal (ereal r) = r"
-| "of_ereal \<infinity> = 0"
-| "of_ereal (-\<infinity>) = 0"
+instantiation ereal :: real_of
+begin
+
+function real_ereal :: "ereal \<Rightarrow> real" where
+  "real_ereal (ereal r) = r"
+| "real_ereal \<infinity> = 0"
+| "real_ereal (-\<infinity>) = 0"
   by (auto intro: ereal_cases)
 termination by default (rule wf_empty)
 
-defs (overloaded)
-  real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"
+instance ..
+end
 
 lemma real_of_ereal[simp]:
   "real (- x :: ereal) = - (real x)"
-  "real (ereal r) = r"
-  "real (\<infinity>::ereal) = 0"
-  by (cases x) (simp_all add: real_of_ereal_def)
+  by (cases x) simp_all
 
 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
 proof safe
@@ -216,7 +217,7 @@
 instance ereal :: numeral ..
 
 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
-  unfolding real_of_ereal_def zero_ereal_def by simp
+  unfolding zero_ereal_def by simp
 
 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)"
   unfolding zero_ereal_def abs_ereal.simps by simp

--- a/src/HOL/Library/Float.thy	Mon Aug 25 16:06:41 2014 +0200
+++ b/src/HOL/Library/Float.thy	Mon Aug 25 14:24:05 2014 +0200
@@ -15,9 +15,15 @@
   morphisms real_of_float float_of
   unfolding float_def by auto
 
-defs (overloaded)
+instantiation float :: real_of
+begin
+
+definition real_float :: "float \<Rightarrow> real" where
   real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
 
+instance ..
+end
+
 lemma type_definition_float': "type_definition real float_of float"
   using type_definition_float unfolding real_of_float_def .
 

--- a/src/HOL/Real.thy	Mon Aug 25 16:06:41 2014 +0200
+++ b/src/HOL/Real.thy	Mon Aug 25 14:24:05 2014 +0200
@@ -1000,13 +1000,24 @@
 where
   "real_of_rat \<equiv> of_rat"
 
-consts
-  (*overloaded constant for injecting other types into "real"*)
-  real :: "'a => real"
+class real_of =
+  fixes real :: "'a \<Rightarrow> real"
+
+instantiation nat :: real_of
+begin
+
+definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat" 
 
-defs (overloaded)
-  real_of_nat_def [code_unfold]: "real == real_of_nat"
-  real_of_int_def [code_unfold]: "real == real_of_int"
+instance ..
+end
+
+instantiation int :: real_of
+begin
+
+definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int" 
+
+instance ..
+end
 
 declare [[coercion_enabled]]
 declare [[coercion "real::nat\<Rightarrow>real"]]

--- a/src/HOL/TPTP/THF_Arith.thy	Mon Aug 25 16:06:41 2014 +0200
+++ b/src/HOL/TPTP/THF_Arith.thy	Mon Aug 25 14:24:05 2014 +0200
@@ -51,7 +51,7 @@
 
 overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
 begin
-  definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)"
+  definition "real_to_rat (x\<Colon>real) = (inv of_rat x\<Colon>rat)"
 end
 
 overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
@@ -85,6 +85,6 @@
 by (metis Rats_of_rat rat_to_real_def real_is_rat_def)
 
 lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
-by (metis injI of_rat_eq_iff rat_to_real_def)
+by (metis injI of_rat_eq_iff)
 
 end