src/HOL/ex/Codegenerator_Rat.thy
author haftmann
Tue Jan 16 08:12:09 2007 +0100 (2007-01-16)
changeset 22071 ebcfe7c2499d
child 22507 3572bc633d9a
permissions -rw-r--r--
refined and added example for ExecutableRat
haftmann@22071
     1
(*  Title:      HOL/Library/ExecutableRat.thy
haftmann@22071
     2
    ID:         $Id$
haftmann@22071
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@22071
     4
*)
haftmann@22071
     5
haftmann@22071
     6
header {* Simple example for executable rational numbers *}
haftmann@22071
     7
haftmann@22071
     8
theory Codegenerator_Rat
haftmann@22071
     9
imports ExecutableRat EfficientNat
haftmann@22071
    10
begin
haftmann@22071
    11
haftmann@22071
    12
definition
haftmann@22071
    13
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@22071
    14
  "foo r s t = (t + s) / t"
haftmann@22071
    15
haftmann@22071
    16
definition
haftmann@22071
    17
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@22071
    18
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@22071
    19
haftmann@22071
    20
definition
haftmann@22071
    21
  "R1 = Fract 3 7"
haftmann@22071
    22
haftmann@22071
    23
definition
haftmann@22071
    24
  "R2 = Fract (-7) 5"
haftmann@22071
    25
haftmann@22071
    26
definition
haftmann@22071
    27
  "R3 = Fract 11 (-9)"
haftmann@22071
    28
haftmann@22071
    29
definition
haftmann@22071
    30
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@22071
    31
haftmann@22071
    32
code_gen foobar (SML #) (SML -)
haftmann@22071
    33
ML {* ROOT.Codegenerator_Rat.foobar *}
haftmann@22071
    34
haftmann@22071
    35
code_module Foo
haftmann@22071
    36
  contains foobar
haftmann@22071
    37
ML {* Foo.foobar *}
haftmann@22071
    38
haftmann@22071
    39
end