refined and added example for ExecutableRat
authorhaftmann
Tue Jan 16 08:06:55 2007 +0100 (2007-01-16)
changeset 2206739d5d42116c4
parent 22066 78b151461b89
child 22068 00bed5ac9884
refined and added example for ExecutableRat
src/HOL/IsaMakefile
src/HOL/Library/ExecutableRat.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jan 16 08:06:52 2007 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jan 16 08:06:55 2007 +0100
     1.3 @@ -616,7 +616,8 @@
     1.4    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
     1.5    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy 	\
     1.6    ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
     1.7 -  ex/Codegenerator.thy ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
     1.8 +  ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
     1.9 +  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
    1.10    ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy	\
    1.11    ex/Guess.thy ex/Hebrew.thy			\
    1.12    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
     2.1 --- a/src/HOL/Library/ExecutableRat.thy	Tue Jan 16 08:06:52 2007 +0100
     2.2 +++ b/src/HOL/Library/ExecutableRat.thy	Tue Jan 16 08:06:55 2007 +0100
     2.3 @@ -10,97 +10,100 @@
     2.4  begin
     2.5  
     2.6  text {*
     2.7 -  Actually nothing is proved about the implementation.
     2.8 +  Actually \emph{nothing} is proved about the implementation.
     2.9  *}
    2.10  
    2.11 -
    2.12 -section {* HOL definitions *}
    2.13 -
    2.14 -datatype erat = Rat bool int int
    2.15 -
    2.16 -instance erat :: zero ..
    2.17 -instance erat :: one ..
    2.18 -instance erat :: plus ..
    2.19 -instance erat :: minus ..
    2.20 -instance erat :: times ..
    2.21 -instance erat :: inverse ..
    2.22 -instance erat :: ord ..
    2.23 +subsection {* Representation and operations of executable rationals *}
    2.24  
    2.25 -definition
    2.26 -  norm :: "erat \<Rightarrow> erat" where
    2.27 -  "norm r = (case r of (Rat a p q) \<Rightarrow>
    2.28 -     if p = 0 then Rat True 0 1
    2.29 -     else
    2.30 -       let
    2.31 -         absp = abs p
    2.32 -       in let
    2.33 -         m = zgcd (absp, q)
    2.34 -       in Rat (a = (0 <= p)) (absp div m) (q div m))"
    2.35 -
    2.36 -definition
    2.37 -  common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" where
    2.38 -  "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
    2.39 -       let q' = q1 * q2 div int (gcd (nat q1, nat q2))
    2.40 -       in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
    2.41 -
    2.42 -definition
    2.43 -  of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
    2.44 -  "of_quotient a b = norm (Rat True a b)"
    2.45 -
    2.46 -definition
    2.47 -  of_rat :: "rat \<Rightarrow> erat" where
    2.48 -  "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)"
    2.49 -
    2.50 -definition
    2.51 -  to_rat :: "erat \<Rightarrow> rat" where
    2.52 -  "to_rat r = (case r of (Rat a p q) \<Rightarrow>
    2.53 -       if a then Fract p q else Fract (uminus p) q)"
    2.54 -
    2.55 -definition
    2.56 -  eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool" where
    2.57 -  "eq_erat r s = (norm r = norm s)"
    2.58 +datatype erat = Rat bool nat nat
    2.59  
    2.60  axiomatization
    2.61    div_zero :: erat
    2.62  
    2.63 -defs (overloaded)
    2.64 -  zero_rat_def: "0 == Rat True 0 1"
    2.65 -  one_rat_def: "1 == Rat True 1 1"
    2.66 -  add_rat_def: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    2.67 +fun
    2.68 +  common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where
    2.69 +  "common (p1, q1) (p2, q2) = (
    2.70 +     let
    2.71 +       q' = q1 * q2 div gcd (q1, q2)
    2.72 +     in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
    2.73 +
    2.74 +definition
    2.75 +  minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where
    2.76 +  "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
    2.77 +
    2.78 +fun
    2.79 +  add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
    2.80 +  "add_sign (True, n) (True, m) = (True, n + m)"
    2.81 +  "add_sign (False, n) (False, m) = (False, n + m)"
    2.82 +  "add_sign (True, n) (False, m) = minus_sign n m"
    2.83 +  "add_sign (False, n) (True, m) = minus_sign m n"
    2.84 +
    2.85 +definition
    2.86 +  erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
    2.87 +  "erat_of_quotient k1 k2 = (
    2.88 +    let
    2.89 +      l1 = nat (abs k1);
    2.90 +      l2 = nat (abs k2);
    2.91 +      m = gcd (l1, l2)
    2.92 +    in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
    2.93 +
    2.94 +instance erat :: zero
    2.95 +  zero_rat_def: "0 \<equiv> Rat True 0 1" ..
    2.96 +
    2.97 +instance erat :: one
    2.98 +  one_rat_def: "1 \<equiv> Rat True 1 1" ..
    2.99 +
   2.100 +instance erat :: plus
   2.101 +  add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
   2.102          let
   2.103 -          ((r1, r2), den) = common ((p1, q1), (p2, q2))
   2.104 -        in let
   2.105 -          num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2)
   2.106 -        in norm (Rat True num den)"
   2.107 -  uminus_rat_def: "- r == case r of Rat a p q \<Rightarrow>
   2.108 -        if p = 0 then Rat a p q
   2.109 -        else Rat (\<not> a) p q"
   2.110 -  times_rat_def: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
   2.111 -        norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))"
   2.112 -  inverse_rat_def: "inverse r == case r of Rat a p q \<Rightarrow>
   2.113 +          ((r1, r2), den) = common (p1, q1) (p2, q2);
   2.114 +          (sign, num) = add_sign (a1, r1) (a2, r2)
   2.115 +        in Rat sign num den" ..
   2.116 +
   2.117 +instance erat :: minus
   2.118 +  uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow>
   2.119 +        if p = 0 then Rat True 0 1
   2.120 +        else Rat (\<not> a) p q" ..
   2.121 +  
   2.122 +instance erat :: times
   2.123 +  times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
   2.124 +        let
   2.125 +          p = p1 * p2;
   2.126 +          q = q1 * q2;
   2.127 +          m = gcd (p, q)
   2.128 +        in Rat (a1 = a2) (p div m) (q div m)" ..
   2.129 +
   2.130 +instance erat :: inverse
   2.131 +  inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow>
   2.132          if p = 0 then div_zero
   2.133 -        else Rat a q p"
   2.134 -  le_rat_def: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
   2.135 +        else Rat a q p" ..
   2.136 +
   2.137 +instance erat :: ord
   2.138 +  le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
   2.139          (\<not> a1 \<and> a2) \<or>
   2.140          (\<not> (a1 \<and> \<not> a2) \<and>
   2.141            (let
   2.142 -            ((r1, r2), dummy) = common ((p1, q1), (p2, q2))
   2.143 -          in if a1 then r1 <= r2 else r2 <= r1))"
   2.144 +            ((r1, r2), dummy) = common (p1, q1) (p2, q2)
   2.145 +          in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
   2.146  
   2.147  
   2.148 -section {* code lemmas *}
   2.149 +subsection {* Code generator setup *}
   2.150 +
   2.151 +subsubsection {* code lemmas *}
   2.152  
   2.153  lemma number_of_rat [code unfold]:
   2.154    "(number_of k \<Colon> rat) \<equiv> Fract k 1"
   2.155    unfolding Fract_of_int_eq rat_number_of_def by simp
   2.156  
   2.157 -declare divide_inverse [where ?'a = rat, code func]
   2.158 +lemma rat_minus [code func]:
   2.159 +  "(a\<Colon>rat) - b = a + (- b)" unfolding ab_group_add_class.diff_minus ..
   2.160 +
   2.161 +lemma rat_divide [code func]:
   2.162 +  "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
   2.163  
   2.164  instance rat :: eq ..
   2.165 -instance erat :: eq ..
   2.166  
   2.167 -
   2.168 -section {* code names *}
   2.169 +subsubsection {* names *}
   2.170  
   2.171  code_modulename SML
   2.172    ExecutableRat Rational
   2.173 @@ -109,14 +112,19 @@
   2.174    ExecutableRat Rational
   2.175  
   2.176  
   2.177 -section {* rat as abstype *}
   2.178 +subsubsection {* rat as abstype *}
   2.179  
   2.180  lemma [code func]: -- {* prevents eq constraint *}
   2.181    shows "All = All"
   2.182      and "contents = contents" by rule+
   2.183  
   2.184 +code_const div_zero
   2.185 +  (SML "raise/ Fail/ \"Division by zero\"")
   2.186 +  (OCaml "failwith \"Division by zero\"")
   2.187 +  (Haskell "error/ \"Division by zero\"")
   2.188 +
   2.189  code_abstype rat erat where
   2.190 -  Fract \<equiv> of_quotient
   2.191 +  Fract \<equiv> erat_of_quotient
   2.192    "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
   2.193    "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
   2.194    "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   2.195 @@ -124,45 +132,21 @@
   2.196    "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   2.197    "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
   2.198    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   2.199 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
   2.200 -
   2.201 -code_const div_zero
   2.202 -  (SML "raise/ Fail/ \"Division by zero\"")
   2.203 -  (OCaml "failwith \"Division by zero\"")
   2.204 -  (Haskell "error/ \"Division by zero\"")
   2.205 -
   2.206 -code_gen
   2.207 -  Fract
   2.208 -  "0 \<Colon> rat"
   2.209 -  "1 \<Colon> rat"
   2.210 -  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
   2.211 -  "uminus \<Colon> rat \<Rightarrow> rat"
   2.212 -  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
   2.213 -  "inverse \<Colon> rat \<Rightarrow> rat"
   2.214 -  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
   2.215 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
   2.216 -  (SML #)
   2.217 -
   2.218 -
   2.219 -section {* type serializations *}
   2.220 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   2.221  
   2.222  types_code
   2.223    rat ("{*erat*}")
   2.224  
   2.225 -
   2.226 -section {* const serializations *}
   2.227 -
   2.228  consts_code
   2.229 -  div_zero ("raise/ (Fail/ \"non-defined rational number\")")
   2.230 -  Fract ("{*of_quotient*}")
   2.231 -  HOL.zero :: rat ("{*0::erat*}")
   2.232 -  HOL.one :: rat ("{*1::erat*}")
   2.233 -  HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   2.234 -  uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}")
   2.235 -  HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   2.236 -  inverse :: "rat \<Rightarrow> rat" ("{*inverse :: erat \<Rightarrow> erat*}")
   2.237 -  divide :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
   2.238 -  Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   2.239 -  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_erat*}")
   2.240 +  div_zero ("(raise/ (Fail/ \"Division by zero\"))")
   2.241 +  Fract ("({*erat_of_quotient*} (_) (_))")
   2.242 +  HOL.zero :: rat ("({*Rat True 0 1*})")
   2.243 +  HOL.one :: rat ("({*Rat True 1 1*})")
   2.244 +  HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   2.245 +  HOL.uminus :: "rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   2.246 +  HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   2.247 +  HOL.inverse :: "rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   2.248 +  Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   2.249 +  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   2.250  
   2.251  end
     3.1 --- a/src/HOL/ex/ROOT.ML	Tue Jan 16 08:06:52 2007 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jan 16 08:06:55 2007 +0100
     3.3 @@ -11,6 +11,7 @@
     3.4  no_document time_use_thy "CodeCollections";
     3.5  no_document time_use_thy "CodeEval";
     3.6  no_document time_use_thy "CodeRandom";
     3.7 +no_document time_use_thy "Codegenerator_Rat";
     3.8  no_document time_use_thy "Codegenerator";
     3.9  
    3.10  time_use_thy "Higher_Order_Logic";