Integrated code generator setup into Rational theory.

--- a/src/HOL/Library/Executable_Rat.thy	Thu Sep 06 11:32:28 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(*  Title:      HOL/Library/Executable_Rat.thy
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Implementation of rational numbers as pairs of integers *}
-
-theory Executable_Rat
-imports Abstract_Rat "~~/src/HOL/Real/Rational"
-begin
-
-hide (open) const Rat
-
-definition
-  Rat :: "int \<times> int \<Rightarrow> rat"
-where
-  "Rat = INum"
-
-code_datatype Rat
-
-lemma Rat_simp:
-  "Rat (k, l) = rat_of_int k / rat_of_int l"
-  unfolding Rat_def INum_def by simp
-
-lemma Rat_zero [simp]: "Rat 0\<^sub>N = 0"
-  by (simp add: Rat_simp)
-
-lemma Rat_lit [simp]: "Rat i\<^sub>N = rat_of_int i"
-  by (simp add: Rat_simp)
-
-lemma zero_rat_code [code]:
-  "0 = Rat 0\<^sub>N" by simp
-
-lemma zero_rat_code [code]:
-  "1 = Rat 1\<^sub>N" by simp
-
-lemma [code, code unfold]:
-  "number_of k = rat_of_int (number_of k)"
-  by (simp add: number_of_is_id rat_number_of_def)
-
-definition
-  [code func del]: "Fract' (b\<Colon>bool) k l = Fract k l"
-
-lemma [code]:
-  "Fract k l = Fract' (l \<noteq> 0) k l"
-  unfolding Fract'_def ..
-
-lemma [code]:
-  "Fract' True k l = (if l \<noteq> 0 then Rat (k, l) else Fract 1 0)"
-  by (simp add: Fract'_def Rat_simp Fract_of_int_quotient [of k l])
-
-lemma [code]:
-  "of_rat (Rat (k, l)) = (if l \<noteq> 0 then of_int k / of_int l else 0)"
-  by (cases "l = 0")
-    (auto simp add: Rat_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
-
-instance rat :: eq ..
-
-lemma rat_eq_code [code]: "Rat x = Rat y \<longleftrightarrow> normNum x = normNum y"
-  unfolding Rat_def INum_normNum_iff ..
-
-lemma rat_less_eq_code [code]: "Rat x \<le> Rat y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
-proof -
-  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Rat (normNum x) \<le> Rat (normNum y)" 
-    by (simp add: Rat_def del: normNum)
-  also have "\<dots> = (Rat x \<le> Rat y)" by (simp add: Rat_def)
-  finally show ?thesis by simp
-qed
-
-lemma rat_less_code [code]: "Rat x < Rat y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
-proof -
-  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Rat (normNum x) < Rat (normNum y)" 
-    by (simp add: Rat_def del: normNum)
-  also have "\<dots> = (Rat x < Rat y)" by (simp add: Rat_def)
-  finally show ?thesis by simp
-qed
-
-lemma rat_add_code [code]: "Rat x + Rat y = Rat (x +\<^sub>N y)"
-  unfolding Rat_def by simp
-
-lemma rat_mul_code [code]: "Rat x * Rat y = Rat (x *\<^sub>N y)"
-  unfolding Rat_def by simp
-
-lemma rat_neg_code [code]: "- Rat x = Rat (~\<^sub>N x)"
-  unfolding Rat_def by simp
-
-lemma rat_sub_code [code]: "Rat x - Rat y = Rat (x -\<^sub>N y)"
-  unfolding Rat_def by simp
-
-lemma rat_inv_code [code]: "inverse (Rat x) = Rat (Ninv x)"
-  unfolding Rat_def Ninv divide_rat_def by simp
-
-lemma rat_div_code [code]: "Rat x / Rat y = Rat (x \<div>\<^sub>N y)"
-  unfolding Rat_def by simp
-
-code_modulename SML
-  Rational Rational
-  Executable_Rat Rational
-
-code_modulename OCaml
-  Rational Rational
-  Executable_Rat Rational
-
-code_modulename Haskell
-  Rational Rational
-  Executable_Rat Rational
-
-end