# HG changeset patch
# User haftmann
# Date 1168931529 -3600
# Node ID ebcfe7c2499d81db3dcf3243b916f9e44ba524be
# Parent  a10ad9d71eaf90add8ec65ca83dcf4933c11fd8f
refined and added example for ExecutableRat

diff -r a10ad9d71eaf -r ebcfe7c2499d src/HOL/ex/Codegenerator_Rat.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Codegenerator_Rat.thy	Tue Jan 16 08:12:09 2007 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOL/Library/ExecutableRat.thy
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Simple example for executable rational numbers *}
+
+theory Codegenerator_Rat
+imports ExecutableRat EfficientNat
+begin
+
+definition
+  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
+  "foo r s t = (t + s) / t"
+
+definition
+  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
+  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
+
+definition
+  "R1 = Fract 3 7"
+
+definition
+  "R2 = Fract (-7) 5"
+
+definition
+  "R3 = Fract 11 (-9)"
+
+definition
+  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
+
+code_gen foobar (SML #) (SML -)
+ML {* ROOT.Codegenerator_Rat.foobar *}
+
+code_module Foo
+  contains foobar
+ML {* Foo.foobar *}
+
+end