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