author | nipkow |
Sun, 04 Nov 2018 12:07:24 +0100 | |
changeset 69232 | 2b913054a9cf |
parent 69064 | 5840724b1d71 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
68630 | 1 |
(* |
2 |
File: Real_Asymp_Approx.thy |
|
3 |
Author: Manuel Eberl, TU München |
|
4 |
||
5 |
Integrates the approximation method into the real_asymp framework as a sign oracle |
|
6 |
to automatically prove positivity/negativity of real constants |
|
7 |
*) |
|
8 |
theory Real_Asymp_Approx |
|
9 |
imports Real_Asymp "HOL-Decision_Procs.Approximation" |
|
10 |
begin |
|
11 |
||
12 |
text \<open> |
|
13 |
For large enough constants (such as @{term "exp (exp 10000 :: real)"}), the |
|
14 |
@{method approximation} method can require a huge amount of time and memory, effectively not |
|
15 |
terminating and causing the entire prover environment to crash. |
|
16 |
||
17 |
To avoid causing such situations, we first check the plausibility of the fact to prove using |
|
18 |
floating-point arithmetic and only run the approximation method if the floating point evaluation |
|
19 |
supports the claim. In particular, exorbitantly large numbers like the one above will lead to |
|
20 |
floating point overflow, which makes the check fail. |
|
21 |
\<close> |
|
22 |
||
23 |
ML \<open> |
|
24 |
signature REAL_ASYMP_APPROX = |
|
25 |
sig |
|
26 |
val real_asymp_approx : bool Config.T |
|
27 |
val sign_oracle_tac : Proof.context -> int -> tactic |
|
28 |
val eval : term -> real |
|
29 |
end |
|
30 |
||
31 |
structure Real_Asymp_Approx : REAL_ASYMP_APPROX = |
|
32 |
struct |
|
33 |
||
34 |
val real_asymp_approx = |
|
35 |
Attrib.setup_config_bool @{binding real_asymp_approx} (K true) |
|
36 |
||
37 |
val nan = Real.fromInt 0 / Real.fromInt 0 |
|
38 |
fun clamp n = if n < 0 then 0 else n |
|
39 |
||
40 |
fun eval_nat (@{term "(+) :: nat => _"} $ a $ b) = bin (op +) (a, b) |
|
41 |
| eval_nat (@{term "(-) :: nat => _"} $ a $ b) = bin (clamp o op -) (a, b) |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68630
diff
changeset
|
42 |
| eval_nat (@{term "(*) :: nat => _"} $ a $ b) = bin (op *) (a, b) |
68630 | 43 |
| eval_nat (@{term "(div) :: nat => _"} $ a $ b) = bin Int.div (a, b) |
44 |
| eval_nat (@{term "(^) :: nat => _"} $ a $ b) = bin (fn (a,b) => Integer.pow a b) (a, b) |
|
45 |
| eval_nat (t as (@{term "numeral :: _ => nat"} $ _)) = snd (HOLogic.dest_number t) |
|
46 |
| eval_nat (@{term "0 :: nat"}) = 0 |
|
47 |
| eval_nat (@{term "1 :: nat"}) = 1 |
|
48 |
| eval_nat (@{term "Nat.Suc"} $ a) = un (fn n => n + 1) a |
|
49 |
| eval_nat _ = ~1 |
|
50 |
and un f a = |
|
51 |
let |
|
52 |
val a = eval_nat a |
|
53 |
in |
|
54 |
if a >= 0 then f a else ~1 |
|
55 |
end |
|
56 |
and bin f (a, b) = |
|
57 |
let |
|
58 |
val (a, b) = apply2 eval_nat (a, b) |
|
59 |
in |
|
60 |
if a >= 0 andalso b >= 0 then f (a, b) else ~1 |
|
61 |
end |
|
62 |
||
63 |
fun sgn n = |
|
64 |
if n < Real.fromInt 0 then Real.fromInt (~1) else Real.fromInt 1 |
|
65 |
||
66 |
fun eval (@{term "(+) :: real => _"} $ a $ b) = eval a + eval b |
|
67 |
| eval (@{term "(-) :: real => _"} $ a $ b) = eval a - eval b |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68630
diff
changeset
|
68 |
| eval (@{term "(*) :: real => _"} $ a $ b) = eval a * eval b |
68630 | 69 |
| eval (@{term "(/) :: real => _"} $ a $ b) = |
70 |
let val a = eval a; val b = eval b in |
|
71 |
if Real.==(b, Real.fromInt 0) then nan else a / b |
|
72 |
end |
|
73 |
| eval (@{term "inverse :: real => _"} $ a) = Real.fromInt 1 / eval a |
|
74 |
| eval (@{term "uminus :: real => _"} $ a) = Real.~ (eval a) |
|
75 |
| eval (@{term "exp :: real => _"} $ a) = Math.exp (eval a) |
|
76 |
| eval (@{term "ln :: real => _"} $ a) = |
|
77 |
let val a = eval a in if a > Real.fromInt 0 then Math.ln a else nan end |
|
78 |
| eval (@{term "(powr) :: real => _"} $ a $ b) = |
|
79 |
let |
|
80 |
val a = eval a; val b = eval b |
|
81 |
in |
|
82 |
if a < Real.fromInt 0 orelse not (Real.isFinite a) orelse not (Real.isFinite b) then |
|
83 |
nan |
|
84 |
else if Real.==(a, Real.fromInt 0) then |
|
85 |
Real.fromInt 0 |
|
86 |
else |
|
87 |
Math.pow (a, b) |
|
88 |
end |
|
89 |
| eval (@{term "(^) :: real => _"} $ a $ b) = |
|
90 |
let |
|
91 |
fun powr x y = |
|
92 |
if not (Real.isFinite x) orelse y < 0 then |
|
93 |
nan |
|
94 |
else if x < Real.fromInt 0 andalso y mod 2 = 1 then |
|
95 |
Real.~ (Math.pow (Real.~ x, Real.fromInt y)) |
|
96 |
else |
|
97 |
Math.pow (Real.abs x, Real.fromInt y) |
|
98 |
in |
|
99 |
powr (eval a) (eval_nat b) |
|
100 |
end |
|
101 |
| eval (@{term "root :: nat => real => _"} $ n $ a) = |
|
102 |
let val a = eval a; val n = eval_nat n in |
|
103 |
if n = 0 then Real.fromInt 0 |
|
104 |
else sgn a * Math.pow (Real.abs a, Real.fromInt 1 / Real.fromInt n) end |
|
105 |
| eval (@{term "sqrt :: real => _"} $ a) = |
|
106 |
let val a = eval a in sgn a * Math.sqrt (abs a) end |
|
107 |
| eval (@{term "log :: real => _"} $ a $ b) = |
|
108 |
let |
|
109 |
val (a, b) = apply2 eval (a, b) |
|
110 |
in |
|
111 |
if b > Real.fromInt 0 andalso a > Real.fromInt 0 andalso Real.!= (a, Real.fromInt 1) then |
|
112 |
Math.ln b / Math.ln a |
|
113 |
else |
|
114 |
nan |
|
115 |
end |
|
116 |
| eval (t as (@{term "numeral :: _ => real"} $ _)) = |
|
117 |
Real.fromInt (snd (HOLogic.dest_number t)) |
|
118 |
| eval (@{term "0 :: real"}) = Real.fromInt 0 |
|
119 |
| eval (@{term "1 :: real"}) = Real.fromInt 1 |
|
120 |
| eval _ = nan |
|
121 |
||
122 |
fun sign_oracle_tac ctxt i = |
|
123 |
let |
|
124 |
fun tac {context = ctxt, concl, ...} = |
|
125 |
let |
|
126 |
val b = |
|
127 |
case HOLogic.dest_Trueprop (Thm.term_of concl) of |
|
128 |
@{term "(<) :: real \<Rightarrow> _"} $ lhs $ rhs => |
|
129 |
let |
|
130 |
val (x, y) = apply2 eval (lhs, rhs) |
|
131 |
in |
|
132 |
Real.isFinite x andalso Real.isFinite y andalso x < y |
|
133 |
end |
|
134 |
| @{term "HOL.Not"} $ (@{term "(=) :: real \<Rightarrow> _"} $ lhs $ rhs) => |
|
135 |
let |
|
136 |
val (x, y) = apply2 eval (lhs, rhs) |
|
137 |
in |
|
138 |
Real.isFinite x andalso Real.isFinite y andalso Real.!= (x, y) |
|
139 |
end |
|
140 |
| _ => false |
|
141 |
in |
|
142 |
if b then HEADGOAL (Approximation.approximation_tac 10 [] NONE ctxt) else no_tac |
|
143 |
end |
|
144 |
in |
|
145 |
if Config.get ctxt real_asymp_approx then |
|
146 |
Subgoal.FOCUS tac ctxt i |
|
147 |
else |
|
148 |
no_tac |
|
149 |
end |
|
150 |
||
151 |
end |
|
152 |
\<close> |
|
153 |
||
154 |
setup \<open> |
|
155 |
Context.theory_map ( |
|
156 |
Multiseries_Expansion.register_sign_oracle |
|
157 |
(@{binding approximation_tac}, Real_Asymp_Approx.sign_oracle_tac)) |
|
158 |
\<close> |
|
159 |
||
160 |
lemma "filterlim (\<lambda>n. (1 + (2 / 3 :: real) ^ (n + 1)) ^ 2 ^ n / 2 powr (4 / 3) ^ (n - 1)) |
|
161 |
at_top at_top" |
|
162 |
proof - |
|
163 |
have [simp]: "ln 4 = 2 * ln (2 :: real)" |
|
164 |
using ln_realpow[of 2 2] by simp |
|
165 |
show ?thesis by (real_asymp simp: field_simps ln_div) |
|
166 |
qed |
|
167 |
||
168 |
end |