# HG changeset patch
# User berghofe
# Date 1189071259 -7200
# Node ID 1ab46fbbb7f445e9250aad071ca4f35a9831f240
# Parent  aa3aacb22e6576e69a3c00c05d09043353736626
Integrated code generator setup into RealDef theory.

diff -r aa3aacb22e65 -r 1ab46fbbb7f4 src/HOL/Library/Executable_Real.thy
--- a/src/HOL/Library/Executable_Real.thy	Thu Sep 06 11:33:45 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-(*  Title:      HOL/Library/Executable_Real.thy
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Implementation of rational real numbers as pairs of integers *}
-
-theory Executable_Real
-imports Abstract_Rat "~~/src/HOL/Real/Real"
-begin
-
-hide (open) const Real
-
-definition
-  Real :: "int \<times> int \<Rightarrow> real"
-where
-  "Real = INum"
-
-code_datatype Real
-
-lemma Real_simp:
-  "Real (k, l) = real_of_int k / real_of_int l"
-  unfolding Real_def INum_def by simp
-
-lemma Real_zero [simp]: "Real 0\<^sub>N = 0"
-  by (simp add: Real_simp)
-
-lemma Real_lit [simp]: "Real i\<^sub>N = real_of_int i"
-  by (simp add: Real_simp)
-
-lemma zero_real_code [code]:
-  "0 = Real 0\<^sub>N" by simp
-
-lemma zero_real_code [code]:
-  "1 = Real 1\<^sub>N" by simp
-
-lemma [code, code unfold]:
-  "number_of k = real_of_int (number_of k)"
-  by (simp add: number_of_is_id real_number_of_def)
-
-instance real :: eq ..
-
-lemma real_eq_code [code]: "Real x = Real y \<longleftrightarrow> normNum x = normNum y"
-  unfolding Real_def INum_normNum_iff ..
-
-lemma real_less_eq_code [code]: "Real x \<le> Real y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
-proof -
-  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Real (normNum x) \<le> Real (normNum y)" 
-    by (simp add: Real_def del: normNum)
-  also have "\<dots> = (Real x \<le> Real y)" by (simp add: Real_def)
-  finally show ?thesis by simp
-qed
-
-lemma real_less_code [code]: "Real x < Real y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
-proof -
-  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Real (normNum x) < Real (normNum y)" 
-    by (simp add: Real_def del: normNum)
-  also have "\<dots> = (Real x < Real y)" by (simp add: Real_def)
-  finally show ?thesis by simp
-qed
-
-lemma real_add_code [code]: "Real x + Real y = Real (x +\<^sub>N y)"
-  unfolding Real_def by simp
-
-lemma real_mul_code [code]: "Real x * Real y = Real (x *\<^sub>N y)"
-  unfolding Real_def by simp
-
-lemma real_neg_code [code]: "- Real x = Real (~\<^sub>N x)"
-  unfolding Real_def by simp
-
-lemma real_sub_code [code]: "Real x - Real y = Real (x -\<^sub>N y)"
-  unfolding Real_def by simp
-
-lemma real_inv_code [code]: "inverse (Real x) = Real (Ninv x)"
-  unfolding Real_def Ninv real_divide_def by simp
-
-lemma real_div_code [code]: "Real x / Real y = Real (x \<div>\<^sub>N y)"
-  unfolding Real_def by simp
-
-code_modulename SML
-  RealDef Real
-  Executable_Real Real
-
-code_modulename OCaml
-  RealDef Real
-  Executable_Real Real
-
-code_modulename Haskell
-  RealDef Real
-  Executable_Real Real
-
-end