src/HOL/Library/ExecutableRat.thy
 author chaieb Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) changeset 23315 df3a7e9ebadb parent 23021 f602a131eaa1 permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/ExecutableRat.thy

     2     ID:         $Id$

     3     Author:     Florian Haftmann, TU Muenchen

     4 *)

     5

     6 header {* Executable implementation of rational numbers in HOL *}

     7

     8 theory ExecutableRat

     9 imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes"

    10 begin

    11

    12 text {*

    13   Actually \emph{nothing} is proved about this implementation.

    14 *}

    15

    16 subsection {* Representation and operations of executable rationals *}

    17

    18 datatype erat = Rat bool nat nat

    19

    20 axiomatization

    21   div_zero :: erat

    22

    23 fun

    24   common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where

    25   "common (p1, q1) (p2, q2) = (

    26      let

    27        q' = q1 * q2 div gcd (q1, q2)

    28      in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"

    29

    30 definition

    31   minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where

    32   "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"

    33

    34 fun

    35   add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where

    36   "add_sign (True, n) (True, m) = (True, n + m)"

    37 | "add_sign (False, n) (False, m) = (False, n + m)"

    38 | "add_sign (True, n) (False, m) = minus_sign n m"

    39 | "add_sign (False, n) (True, m) = minus_sign m n"

    40

    41 definition

    42   erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where

    43   "erat_of_quotient k1 k2 = (

    44     let

    45       l1 = nat (abs k1);

    46       l2 = nat (abs k2);

    47       m = gcd (l1, l2)

    48     in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"

    49

    50 instance erat :: zero

    51   zero_rat_def: "0 \<equiv> Rat True 0 1" ..

    52

    53 instance erat :: one

    54   one_rat_def: "1 \<equiv> Rat True 1 1" ..

    55

    56 instance erat :: plus

    57   add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>

    58         let

    59           ((r1, r2), den) = common (p1, q1) (p2, q2);

    60           (sign, num) = add_sign (a1, r1) (a2, r2)

    61         in Rat sign num den" ..

    62

    63 instance erat :: minus

    64   uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow>

    65         if p = 0 then Rat True 0 1

    66         else Rat (\<not> a) p q" ..

    67

    68 instance erat :: times

    69   times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>

    70         let

    71           p = p1 * p2;

    72           q = q1 * q2;

    73           m = gcd (p, q)

    74         in Rat (a1 = a2) (p div m) (q div m)" ..

    75

    76 instance erat :: inverse

    77   inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow>

    78         if p = 0 then div_zero

    79         else Rat a q p" ..

    80

    81 instance erat :: ord

    82   le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>

    83         (\<not> a1 \<and> a2) \<or>

    84         (\<not> (a1 \<and> \<not> a2) \<and>

    85           (let

    86             ((r1, r2), dummy) = common (p1, q1) (p2, q2)

    87           in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..

    88

    89

    90 subsection {* Code generator setup *}

    91

    92 subsubsection {* code lemmas *}

    93

    94 lemma number_of_rat [code unfold]:

    95   "(number_of k \<Colon> rat) = Fract k 1"

    96   unfolding Fract_of_int_eq rat_number_of_def by simp

    97

    98 lemma rat_minus [code func]:

    99   "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..

   100

   101 lemma rat_divide [code func]:

   102   "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..

   103

   104 instance rat :: eq ..

   105

   106 subsubsection {* names *}

   107

   108 code_modulename SML

   109   ExecutableRat Rational

   110

   111 code_modulename OCaml

   112   ExecutableRat Rational

   113

   114 code_modulename Haskell

   115   ExecutableRat Rational

   116

   117 subsubsection {* rat as abstype *}

   118

   119 code_const div_zero

   120   (SML "raise/ Fail/ \"Division by zero\"")

   121   (OCaml "failwith \"Division by zero\"")

   122   (Haskell "error/ \"Division by zero\"")

   123

   124 code_abstype rat erat where

   125   Fract \<equiv> erat_of_quotient

   126   "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"

   127   "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"

   128   "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"

   129   "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"

   130   "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"

   131   "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"

   132   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"

   133   "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"

   134

   135 types_code

   136   rat ("{*erat*}")

   137

   138 consts_code

   139   div_zero ("(raise/ (Fail/ \"Division by zero\"))")

   140   Fract ("({*erat_of_quotient*} (_) (_))")

   141   "0 \<Colon> rat" ("({*Rat True 0 1*})")

   142   "1 \<Colon> rat" ("({*Rat True 1 1*})")

   143   "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")

   144   "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")

   145   "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")

   146   "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")

   147   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")

   148   "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")

   149

   150 end