author hoelzl Mon Nov 14 11:50:52 2011 +0100 (2011-11-14 ago) changeset 45483 34d07cf7d207 parent 45482 8f32682f78fe child 45485 7a0975c9dd26
 src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Library/Code_Real_Approx_By_Float.thy file | annotate | diff | revisions src/HOL/Library/ROOT.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 14 09:25:05 2011 +0100
1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 14 11:50:52 2011 +0100
1.3 @@ -435,6 +435,7 @@
1.4    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
1.5    Library/Code_Char_ord.thy Library/Code_Integer.thy			\
1.6    Library/Code_Natural.thy Library/Code_Prolog.thy			\
1.7 +  Library/Code_Real_Approx_By_Float.thy					\
1.8    Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
1.10    Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy	\
```
```     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 11:50:52 2011 +0100
2.3 @@ -0,0 +1,148 @@
2.4 +(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
2.5 +
2.6 +theory Code_Real_Approx_By_Float
2.7 +imports Complex_Main "~~/src/HOL/Library/Code_Integer"
2.8 +begin
2.9 +
2.10 +text{* \textbf{WARNING} This theory implements mathematical reals by machine
2.11 +reals (floats). This is inconsistent. See the proof of False at the end of
2.12 +the theory, where an equality on mathematical reals is (incorrectly)
2.13 +disproved by mapping it to machine reals.
2.14 +
2.15 +The value command cannot display real results yet.
2.16 +
2.17 +The only legitimate use of this theory is as a tool for code generation
2.18 +purposes. *}
2.19 +
2.20 +code_type real
2.21 +  (SML   "real")
2.22 +  (OCaml "float")
2.23 +
2.24 +code_const Ratreal
2.25 +  (SML "error/ \"Bad constant: Ratreal\"")
2.26 +
2.27 +code_const "0 :: real"
2.28 +  (SML   "0.0")
2.29 +  (OCaml "0.0")
2.30 +declare zero_real_code[code_unfold del]
2.31 +
2.32 +code_const "1 :: real"
2.33 +  (SML   "1.0")
2.34 +  (OCaml "1.0")
2.35 +declare one_real_code[code_unfold del]
2.36 +
2.37 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
2.38 +  (SML   "Real.== ((_), (_))")
2.39 +  (OCaml "Pervasives.(=)")
2.40 +
2.41 +code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
2.42 +  (SML   "Real.<= ((_), (_))")
2.43 +  (OCaml "Pervasives.(<=)")
2.44 +
2.45 +code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
2.46 +  (SML   "Real.< ((_), (_))")
2.47 +  (OCaml "Pervasives.(<)")
2.48 +
2.49 +code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
2.50 +  (SML   "Real.+ ((_), (_))")
2.51 +  (OCaml "Pervasives.( +. )")
2.52 +
2.53 +code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
2.54 +  (SML   "Real.* ((_), (_))")
2.55 +  (OCaml "Pervasives.( *. )")
2.56 +
2.57 +code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
2.58 +  (SML   "Real.- ((_), (_))")
2.59 +  (OCaml "Pervasives.( -. )")
2.60 +
2.61 +code_const "uminus :: real \<Rightarrow> real"
2.62 +  (SML   "Real.~")
2.63 +  (OCaml "Pervasives.( ~-. )")
2.64 +
2.65 +code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
2.66 +  (SML   "Real.'/ ((_), (_))")
2.67 +  (OCaml "Pervasives.( '/. )")
2.68 +
2.69 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
2.70 +  (SML   "Real.== ((_:real), (_))")
2.71 +
2.72 +code_const "sqrt :: real \<Rightarrow> real"
2.73 +  (SML   "Math.sqrt")
2.74 +  (OCaml "Pervasives.sqrt")
2.75 +declare sqrt_def[code del]
2.76 +
2.77 +definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
2.78 +
2.79 +lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
2.80 +  unfolding real_exp_def ..
2.81 +
2.82 +code_const real_exp
2.83 +  (SML   "Math.exp")
2.84 +  (OCaml "Pervasives.exp")
2.85 +declare real_exp_def[code del]
2.86 +declare exp_def[code del]
2.87 +
2.88 +hide_const (open) real_exp
2.89 +
2.90 +code_const ln
2.91 +  (SML   "Math.ln")
2.92 +  (OCaml "Pervasives.ln")
2.93 +declare ln_def[code del]
2.94 +
2.95 +code_const cos
2.96 +  (SML   "Math.cos")
2.97 +  (OCaml "Pervasives.cos")
2.98 +declare cos_def[code del]
2.99 +
2.100 +code_const sin
2.101 +  (SML   "Math.sin")
2.102 +  (OCaml "Pervasives.sin")
2.103 +declare sin_def[code del]
2.104 +
2.105 +code_const pi
2.106 +  (SML   "Math.pi")
2.107 +  (OCaml "Pervasives.pi")
2.108 +declare pi_def[code del]
2.109 +
2.110 +code_const arctan
2.111 +  (SML   "Math.atan")
2.112 +  (OCaml "Pervasives.atan")
2.113 +declare arctan_def[code del]
2.114 +
2.115 +code_const arccos
2.116 +  (SML   "Math.scos")
2.117 +  (OCaml "Pervasives.acos")
2.118 +declare arccos_def[code del]
2.119 +
2.120 +code_const arcsin
2.121 +  (SML   "Math.asin")
2.122 +  (OCaml "Pervasives.asin")
2.123 +declare arcsin_def[code del]
2.124 +
2.125 +definition real_of_int :: "int \<Rightarrow> real" where
2.126 +  "real_of_int \<equiv> of_int"
2.127 +
2.128 +code_const real_of_int
2.129 +  (SML "Real.fromInt")
2.130 +  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
2.131 +
2.132 +lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
2.133 +  unfolding real_of_int_def ..
2.134 +
2.135 +hide_const (open) real_of_int
2.136 +
2.137 +declare number_of_real_code [code_unfold del]
2.138 +
2.139 +lemma "False"
2.140 +proof-
2.141 +  have "cos(pi/2) = 0" by(rule cos_pi_half)
2.142 +  moreover have "cos(pi/2) \<noteq> 0" by eval
2.143 +  ultimately show "False" by blast
2.144 +qed
2.145 +
2.146 +definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
2.147 +
2.148 +export_code test
2.149 +  in OCaml file -
2.150 +
2.151 +end
```
```     3.1 --- a/src/HOL/Library/ROOT.ML	Mon Nov 14 09:25:05 2011 +0100
3.2 +++ b/src/HOL/Library/ROOT.ML	Mon Nov 14 11:50:52 2011 +0100
3.3 @@ -3,4 +3,5 @@
3.4
3.5  use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
3.6    "Product_Lattice",
3.7 -  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
3.8 +  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
3.9 +  "Code_Real_Approx_By_Float" ];
```