equal
deleted
inserted
replaced
999 |
999 |
1000 lemma rat_divide_code [code]: |
1000 lemma rat_divide_code [code]: |
1001 "Fract a b / Fract c d = Fract_norm (a * d) (b * c)" |
1001 "Fract a b / Fract c d = Fract_norm (a * d) (b * c)" |
1002 by simp |
1002 by simp |
1003 |
1003 |
|
1004 definition (in term_syntax) |
|
1005 valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where |
|
1006 [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l" |
|
1007 |
|
1008 notation fcomp (infixl "o>" 60) |
|
1009 notation scomp (infixl "o\<rightarrow>" 60) |
|
1010 |
|
1011 instantiation rat :: random |
|
1012 begin |
|
1013 |
|
1014 definition |
|
1015 "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair ( |
|
1016 let j = Code_Index.int_of (denom + 1) |
|
1017 in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))" |
|
1018 |
|
1019 instance .. |
|
1020 |
|
1021 end |
|
1022 |
|
1023 no_notation fcomp (infixl "o>" 60) |
|
1024 no_notation scomp (infixl "o\<rightarrow>" 60) |
|
1025 |
1004 hide (open) const Fract_norm |
1026 hide (open) const Fract_norm |
1005 |
1027 |
1006 text {* Setup for SML code generator *} |
1028 text {* Setup for SML code generator *} |
1007 |
1029 |
1008 types_code |
1030 types_code |