# HG changeset patch
# User haftmann
# Date 1147335955 -7200
# Node ID a677ac8c9b10751cc9f5161e636df74ea7e6b72b
# Parent  81fe44909dd5046d3efaad1d26e8cb27d78927c0
fixed codegen bug, cleanup

diff -r 81fe44909dd5 -r a677ac8c9b10 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Wed May 10 16:23:21 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Thu May 11 10:25:55 2006 +0200
@@ -23,39 +23,28 @@
 instance erat :: inverse ..
 instance erat :: ord ..
 
-consts
+definition
   norm :: "erat \<Rightarrow> erat"
-  common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int"
-  of_quotient :: "int * int \<Rightarrow> erat"
-  of_rat :: "rat \<Rightarrow> erat"
-  to_rat :: "erat \<Rightarrow> rat"
-
-defs
-  norm_def [simp]: "norm r == case r of (Rat a p q) \<Rightarrow>
+  norm_def [simp]: "norm r = (case r of (Rat a p q) \<Rightarrow>
      if p = 0 then Rat True 0 1
      else
        let
          absp = abs p
        in let
          m = zgcd (absp, q)
-       in Rat (a = (0 <= p)) (absp div m) (q div m)"
-  common_def [simp]: "common r == case r of ((p1, q1), (p2, q2)) \<Rightarrow>
+       in Rat (a = (0 <= p)) (absp div m) (q div m))"
+  common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int"
+  common_def [simp]: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
        let q' = q1 * q2 div int (gcd (nat q1, nat q2))
-       in ((p1 * (q' div q1), p2 * (q' div q2)), q')"
-  of_quotient_def [simp]: "of_quotient r == case r of (a, b) \<Rightarrow>
-       norm (Rat True a b)"
-  of_rat_def [simp]: "of_rat r == of_quotient (THE s. s : Rep_Rat r)"
-  to_rat_def [simp]: "to_rat r == case r of (Rat a p q) \<Rightarrow>
-       if a then Fract p q else Fract (uminus p) q"
-
-consts
-  zero :: erat
-  one :: erat
-  add :: "erat \<Rightarrow> erat \<Rightarrow> erat"
-  neg :: "erat \<Rightarrow> erat"
-  mult :: "erat \<Rightarrow> erat \<Rightarrow> erat"
-  inv :: "erat \<Rightarrow> erat"
-  le :: "erat \<Rightarrow> erat \<Rightarrow> bool"
+       in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
+  of_quotient :: "int * int \<Rightarrow> erat"
+  of_quotient_def [simp]: "of_quotient r = (case r of (a, b) \<Rightarrow>
+       norm (Rat True a b))"
+  of_rat :: "rat \<Rightarrow> erat"
+  of_rat_def [simp]: "of_rat r = of_quotient (THE s. s : Rep_Rat r)"
+  to_rat :: "erat \<Rightarrow> rat"
+  to_rat_def [simp]: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
+       if a then Fract p q else Fract (uminus p) q)"
 
 defs (overloaded)
   zero_rat_def [simp]: "0 == Rat False 0 1"
@@ -86,6 +75,9 @@
   haskell (target_atom "{*erat*}")
 
 code_syntax_const
+  "arbitrary :: erat"
+    ml ("raise/ (Fail/ \"non-defined rational number\")")
+    haskell ("error/ \"non-defined rational number\"")
   Fract
     ml ("{*of_quotient*}")
     haskell ("{*of_quotient*}")