969 by simp |
969 by simp |
970 |
970 |
971 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
971 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
972 by simp |
972 by simp |
973 |
973 |
|
974 subsection{*Code generation using Isabelle's rats*} |
|
975 |
|
976 types_code |
|
977 real ("Rat.rat") |
|
978 attach (term_of) {* |
|
979 fun term_of_real x = |
|
980 let |
|
981 val rT = HOLogic.realT |
|
982 val (p, q) = Rat.quotient_of_rat x |
|
983 in if q = 1 then HOLogic.mk_number rT p |
|
984 else Const("HOL.divide",[rT,rT] ---> rT) $ |
|
985 (HOLogic.mk_number rT p) $ (HOLogic.mk_number rT q) |
|
986 end; |
|
987 *} |
|
988 attach (test) {* |
|
989 fun gen_real i = |
|
990 let val p = random_range 0 i; val q = random_range 0 i; |
|
991 val r = if q=0 then Rat.rat_of_int i else Rat.rat_of_quotient(p,q) |
|
992 in if one_of [true,false] then r else Rat.neg r end; |
|
993 *} |
|
994 |
|
995 consts_code |
|
996 "0 :: real" ("Rat.zero") |
|
997 "1 :: real" ("Rat.one") |
|
998 "uminus :: real \<Rightarrow> real" ("Rat.neg") |
|
999 "op + :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.add") |
|
1000 "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult") |
|
1001 "inverse :: real \<Rightarrow> real" ("Rat.inv") |
|
1002 "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le") |
|
1003 "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("(Rat.ord (_, _) = LESS)") |
|
1004 "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq") |
|
1005 "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int") |
|
1006 "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})") |
|
1007 |
|
1008 |
|
1009 lemma [code, code unfold]: |
|
1010 "number_of k = real (number_of k :: int)" |
|
1011 by simp |
|
1012 |
974 end |
1013 end |