src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Thu Dec 13 07:09:04 2007 +0100 (2007-12-13)
changeset 25616 28d373f1482a
parent 24530 1bac25879117
child 25933 7fc0f4065251
permissions -rw-r--r--
added div/mod examples
haftmann@24195
     1
(*  Title:      HOL/ex/Codegenerator_Pretty.thy
haftmann@24195
     2
    ID:         $Id$
haftmann@24195
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@24195
     4
*)
haftmann@24195
     5
haftmann@24195
     6
header {* Simple examples for pretty numerals and such *}
haftmann@24195
     7
haftmann@24195
     8
theory Codegenerator_Pretty
berghofe@24530
     9
imports "~~/src/HOL/Real/RealDef" Efficient_Nat
haftmann@24195
    10
begin
haftmann@24195
    11
haftmann@24195
    12
definition
haftmann@24195
    13
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@24195
    14
  "foo r s t = (t + s) / t"
haftmann@24195
    15
haftmann@24195
    16
definition
haftmann@24195
    17
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@24195
    18
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24195
    19
haftmann@24195
    20
definition
haftmann@24195
    21
  "R1 = Fract 3 7"
haftmann@24195
    22
haftmann@24195
    23
definition
haftmann@24195
    24
  "R2 = Fract (-7) 5"
haftmann@24195
    25
haftmann@24195
    26
definition
haftmann@24195
    27
  "R3 = Fract 11 (-9)"
haftmann@24195
    28
haftmann@24195
    29
definition
haftmann@24195
    30
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@24195
    31
haftmann@24195
    32
definition
haftmann@24195
    33
  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
haftmann@24195
    34
  "foo' r s t = (t + s) / t"
haftmann@24195
    35
haftmann@24195
    36
definition
haftmann@24195
    37
  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
haftmann@24195
    38
  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24195
    39
haftmann@24195
    40
definition
haftmann@24195
    41
  "R1' = real_of_rat (Fract 3 7)"
haftmann@24195
    42
haftmann@24195
    43
definition
haftmann@24195
    44
  "R2' = real_of_rat (Fract (-7) 5)"
haftmann@24195
    45
haftmann@24195
    46
definition
haftmann@24195
    47
  "R3' = real_of_rat (Fract 11 (-9))"
haftmann@24195
    48
haftmann@24195
    49
definition
haftmann@24195
    50
  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
haftmann@24195
    51
haftmann@25616
    52
definition
haftmann@25616
    53
  "(doodle :: nat) = 1705 div 42 * 42 + 1705 mod 42"
haftmann@25616
    54
haftmann@25616
    55
export_code foobar foobar' doodle in SML module_name Foo
haftmann@24195
    56
  in OCaml file -
haftmann@24195
    57
  in Haskell file -
haftmann@25616
    58
ML {* (Foo.foobar, Foo.foobar', Foo.doodle) *}
haftmann@24195
    59
haftmann@24195
    60
end