68630
|
1 |
signature REAL_ASYMP_DIAG = sig
|
|
2 |
|
|
3 |
val pretty_limit : Proof.context -> term -> Pretty.T
|
|
4 |
|
|
5 |
val limit_cmd :
|
|
6 |
Proof.context -> (Facts.ref * Token.src list) list list -> string -> string option -> unit
|
|
7 |
val limit : Proof.context -> thm list -> term -> term -> Multiseries_Expansion.limit_result
|
|
8 |
|
|
9 |
val expansion_cmd :
|
|
10 |
Proof.context -> (Facts.ref * Token.src list) list list -> bool * int ->
|
|
11 |
string -> string option -> unit
|
|
12 |
val expansion :
|
|
13 |
Proof.context -> thm list -> bool * int -> term -> term -> term * Asymptotic_Basis.basis
|
|
14 |
|
|
15 |
end
|
|
16 |
|
|
17 |
structure Real_Asymp_Diag : REAL_ASYMP_DIAG = struct
|
|
18 |
|
|
19 |
open Lazy_Eval
|
|
20 |
open Multiseries_Expansion
|
|
21 |
|
69597
|
22 |
fun pretty_limit _ (Const (\<^const_name>\<open>at_top\<close>, _)) = Pretty.str "\<infinity>"
|
|
23 |
| pretty_limit _ (Const (\<^const_name>\<open>at_bot\<close>, _)) = Pretty.str "-\<infinity>"
|
|
24 |
| pretty_limit _ (Const (\<^const_name>\<open>at_infinity\<close>, _)) = Pretty.str "\<plusminus>\<infinity>"
|
|
25 |
| pretty_limit ctxt (Const (\<^const_name>\<open>at_within\<close>, _) $ c $
|
|
26 |
(Const (\<^const_name>\<open>greaterThan\<close>, _) $ _)) =
|
68630
|
27 |
Pretty.block [Syntax.pretty_term ctxt c, Pretty.str "\<^sup>+"]
|
69597
|
28 |
| pretty_limit ctxt (Const (\<^const_name>\<open>at_within\<close>, _) $ c $
|
|
29 |
(Const (\<^const_name>\<open>lessThan\<close>, _) $ _)) =
|
68630
|
30 |
Pretty.block [Syntax.pretty_term ctxt c, Pretty.str "\<^sup>-"]
|
69597
|
31 |
| pretty_limit ctxt (Const (\<^const_name>\<open>at_within\<close>, _) $ c $ Const ("UNIV", _)) =
|
68630
|
32 |
Syntax.pretty_term ctxt c
|
69597
|
33 |
| pretty_limit ctxt (Const (\<^const_name>\<open>nhds\<close>, _) $ c) =
|
68630
|
34 |
Syntax.pretty_term ctxt c
|
|
35 |
| pretty_limit _ t = raise TERM ("pretty_limit", [t])
|
|
36 |
|
|
37 |
fun reduce_to_at_top flt t = Envir.beta_eta_contract (
|
|
38 |
case flt of
|
69597
|
39 |
\<^term>\<open>at_top :: real filter\<close> => t
|
|
40 |
| \<^term>\<open>at_bot :: real filter\<close> =>
|
|
41 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (-x)\<close>, t)
|
|
42 |
| \<^term>\<open>at_left 0 :: real filter\<close> =>
|
|
43 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (-inverse x)\<close>, t)
|
|
44 |
| \<^term>\<open>at_right 0 :: real filter\<close> =>
|
|
45 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (inverse x)\<close>, t)
|
|
46 |
| \<^term>\<open>at_within :: real => _\<close> $ c $ (\<^term>\<open>greaterThan :: real \<Rightarrow> _\<close> $ c') =>
|
68630
|
47 |
if c aconv c' then
|
69597
|
48 |
Term.betapply (Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) c x. f (c + inverse x)\<close>, t), c)
|
68630
|
49 |
else
|
|
50 |
raise TERM ("Unsupported filter for real_limit", [flt])
|
69597
|
51 |
| \<^term>\<open>at_within :: real => _\<close> $ c $ (\<^term>\<open>lessThan :: real \<Rightarrow> _\<close> $ c') =>
|
68630
|
52 |
if c aconv c' then
|
69597
|
53 |
Term.betapply (Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) c x. f (c - inverse x)\<close>, t), c)
|
68630
|
54 |
else
|
|
55 |
raise TERM ("Unsupported filter for real_limit", [flt])
|
|
56 |
| _ =>
|
|
57 |
raise TERM ("Unsupported filter for real_limit", [flt]))
|
|
58 |
|
69597
|
59 |
fun mk_uminus (\<^term>\<open>uminus :: real => real\<close> $ c) = c
|
|
60 |
| mk_uminus c = Term.betapply (\<^term>\<open>uminus :: real => real\<close>, c)
|
68630
|
61 |
|
|
62 |
fun transfer_expansion_from_at_top' flt t = Envir.beta_eta_contract (
|
|
63 |
case flt of
|
69597
|
64 |
\<^term>\<open>at_top :: real filter\<close> => t
|
|
65 |
| \<^term>\<open>at_bot :: real filter\<close> =>
|
|
66 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (-x)\<close>, t)
|
|
67 |
| \<^term>\<open>at_left 0 :: real filter\<close> =>
|
|
68 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (-inverse x)\<close>, t)
|
|
69 |
| \<^term>\<open>at_right 0 :: real filter\<close> =>
|
|
70 |
Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) x. f (inverse x)\<close>, t)
|
|
71 |
| \<^term>\<open>at_within :: real => _\<close> $ c $ (\<^term>\<open>greaterThan :: real \<Rightarrow> _\<close> $ c') =>
|
68630
|
72 |
if c aconv c' then
|
69597
|
73 |
Term.betapply (Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) c x. f (inverse (x - c))\<close>, t), c)
|
68630
|
74 |
else
|
|
75 |
raise TERM ("Unsupported filter for real_limit", [flt])
|
69597
|
76 |
| \<^term>\<open>at_within :: real => _\<close> $ c $ (\<^term>\<open>lessThan :: real \<Rightarrow> _\<close> $ c') =>
|
68630
|
77 |
if c aconv c' then
|
69597
|
78 |
Term.betapply (Term.betapply (\<^term>\<open>%(f::real\<Rightarrow>real) c x. f (inverse (c - x))\<close>, t), c)
|
68630
|
79 |
else
|
|
80 |
raise TERM ("Unsupported filter for real_limit", [flt])
|
|
81 |
| _ =>
|
|
82 |
raise TERM ("Unsupported filter for real_limit", [flt]))
|
|
83 |
|
|
84 |
|
|
85 |
fun transfer_expansion_from_at_top flt =
|
|
86 |
let
|
69597
|
87 |
fun go idx (t as (\<^term>\<open>(powr) :: real => _\<close> $
|
|
88 |
(\<^term>\<open>inverse :: real \<Rightarrow> _\<close> $ Bound n) $ e)) =
|
68630
|
89 |
if n = idx then
|
69597
|
90 |
Envir.beta_eta_contract (\<^term>\<open>(powr) :: real => _\<close> $ Bound n $ mk_uminus e)
|
68630
|
91 |
else
|
|
92 |
t
|
69597
|
93 |
| go idx (t as (\<^term>\<open>(powr) :: real => _\<close> $ (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $
|
|
94 |
(\<^term>\<open>inverse :: real \<Rightarrow> _\<close> $ Bound n)) $ e)) =
|
68630
|
95 |
if n = idx then
|
69597
|
96 |
Envir.beta_eta_contract (\<^term>\<open>(powr) :: real => _\<close> $
|
68630
|
97 |
(mk_uminus (Bound n)) $ mk_uminus e)
|
|
98 |
else
|
|
99 |
t
|
69597
|
100 |
| go idx (t as (\<^term>\<open>(powr) :: real => _\<close> $ (\<^term>\<open>inverse :: real \<Rightarrow> _\<close> $
|
|
101 |
(\<^term>\<open>(-) :: real \<Rightarrow> _\<close> $ Bound n $ c)) $ e)) =
|
68630
|
102 |
if n = idx then
|
69597
|
103 |
Envir.beta_eta_contract (\<^term>\<open>(powr) :: real => _\<close> $
|
|
104 |
(\<^term>\<open>(-) :: real => _\<close> $ Bound n $ c) $ mk_uminus e)
|
68630
|
105 |
else
|
|
106 |
t
|
69597
|
107 |
| go idx (t as (\<^term>\<open>(powr) :: real => _\<close> $ (\<^term>\<open>inverse :: real \<Rightarrow> _\<close> $
|
|
108 |
(\<^term>\<open>(-) :: real \<Rightarrow> _\<close> $ c $ Bound n)) $ e)) =
|
68630
|
109 |
if n = idx then
|
69597
|
110 |
Envir.beta_eta_contract (\<^term>\<open>(powr) :: real => _\<close> $
|
|
111 |
(\<^term>\<open>(-) :: real => _\<close> $ c $ Bound n) $ mk_uminus e)
|
68630
|
112 |
else
|
|
113 |
t
|
|
114 |
| go idx (s $ t) = go idx s $ go idx t
|
|
115 |
| go idx (Abs (x, T, t)) = Abs (x, T, go (idx + 1) t)
|
|
116 |
| go _ t = t
|
|
117 |
in
|
|
118 |
transfer_expansion_from_at_top' flt #> go (~1)
|
|
119 |
end
|
|
120 |
|
|
121 |
fun gen_limit prep_term prep_flt prep_facts res ctxt facts t flt =
|
|
122 |
let
|
|
123 |
val t = prep_term ctxt t
|
|
124 |
val flt = prep_flt ctxt flt
|
|
125 |
val ctxt = Variable.auto_fixes t ctxt
|
|
126 |
val t = reduce_to_at_top flt t
|
|
127 |
val facts = prep_facts ctxt facts
|
|
128 |
val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
|
|
129 |
val (bnds, basis) = expand_term_bounds ectxt t Asymptotic_Basis.default_basis
|
|
130 |
in
|
|
131 |
res ctxt (limit_of_expansion_bounds ectxt (bnds, basis))
|
|
132 |
end
|
|
133 |
|
|
134 |
fun pretty_limit_result ctxt (Exact_Limit lim) = pretty_limit ctxt lim
|
|
135 |
| pretty_limit_result ctxt (Limit_Bounds (l, u)) =
|
|
136 |
let
|
|
137 |
fun pretty s (SOME l) = [Pretty.block [Pretty.str s, pretty_limit ctxt l]]
|
|
138 |
| pretty _ NONE = []
|
|
139 |
val ps = pretty "Lower bound: " l @ pretty "Upper bound: " u
|
|
140 |
in
|
|
141 |
if null ps then Pretty.str "No bounds found." else Pretty.chunks ps
|
|
142 |
end
|
|
143 |
|
|
144 |
val limit_cmd =
|
|
145 |
gen_limit
|
|
146 |
(fn ctxt =>
|
|
147 |
Syntax.parse_term ctxt
|
69597
|
148 |
#> Type.constraint \<^typ>\<open>real => real\<close>
|
68630
|
149 |
#> Syntax.check_term ctxt)
|
|
150 |
(fn ctxt => fn flt =>
|
|
151 |
case flt of
|
69597
|
152 |
NONE => \<^term>\<open>at_top :: real filter\<close>
|
68630
|
153 |
| SOME flt =>
|
|
154 |
flt
|
|
155 |
|> Syntax.parse_term ctxt
|
69597
|
156 |
|> Type.constraint \<^typ>\<open>real filter\<close>
|
68630
|
157 |
|> Syntax.check_term ctxt)
|
|
158 |
(fn ctxt => flat o flat o map (map (Proof_Context.get_fact ctxt o fst)))
|
|
159 |
(fn ctxt => pretty_limit_result ctxt #> Pretty.writeln)
|
|
160 |
|
|
161 |
val limit = gen_limit Syntax.check_term Syntax.check_term (K I) (K I)
|
|
162 |
|
|
163 |
|
|
164 |
fun gen_expansion prep_term prep_flt prep_facts res ctxt facts (n, strict) t flt =
|
|
165 |
let
|
|
166 |
val t = prep_term ctxt t
|
|
167 |
val flt = prep_flt ctxt flt
|
|
168 |
val ctxt = Variable.auto_fixes t ctxt
|
|
169 |
val t = reduce_to_at_top flt t
|
|
170 |
val facts = prep_facts ctxt facts
|
|
171 |
val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
|
|
172 |
val basis = Asymptotic_Basis.default_basis
|
|
173 |
val (thm, basis) = expand_term ectxt t basis
|
|
174 |
val (exp, error) = extract_terms (strict, n) ectxt basis (get_expansion thm)
|
|
175 |
val exp = transfer_expansion_from_at_top flt exp
|
|
176 |
val error =
|
|
177 |
case error of
|
|
178 |
SOME (L $ flt' $ f) => SOME (L $ flt' $ transfer_expansion_from_at_top flt f)
|
|
179 |
| _ => error
|
|
180 |
val t =
|
|
181 |
case error of
|
|
182 |
NONE => exp
|
|
183 |
| SOME err =>
|
69597
|
184 |
Term.betapply (Term.betapply (\<^term>\<open>expansion_with_remainder_term\<close>, exp), err)
|
68630
|
185 |
in
|
|
186 |
res ctxt (t, basis)
|
|
187 |
end
|
|
188 |
|
|
189 |
fun print_basis_elem ctxt t =
|
68828
|
190 |
Syntax.pretty_term (Config.put Syntax_Trans.eta_contract false ctxt)
|
68630
|
191 |
(Envir.eta_long [] t)
|
|
192 |
|
|
193 |
val expansion_cmd =
|
|
194 |
gen_expansion
|
|
195 |
(fn ctxt =>
|
|
196 |
Syntax.parse_term ctxt
|
69597
|
197 |
#> Type.constraint \<^typ>\<open>real => real\<close>
|
68630
|
198 |
#> Syntax.check_term ctxt)
|
|
199 |
(fn ctxt => fn flt =>
|
|
200 |
case flt of
|
69597
|
201 |
NONE => \<^term>\<open>at_top :: real filter\<close>
|
68630
|
202 |
| SOME flt =>
|
|
203 |
flt
|
|
204 |
|> Syntax.parse_term ctxt
|
69597
|
205 |
|> Type.constraint \<^typ>\<open>real filter\<close>
|
68630
|
206 |
|> Syntax.check_term ctxt)
|
|
207 |
(fn ctxt => flat o flat o map (map (Proof_Context.get_fact ctxt o fst)))
|
|
208 |
(fn ctxt => fn (exp, basis) =>
|
|
209 |
Pretty.writeln (Pretty.chunks (
|
|
210 |
[Pretty.str "Expansion:",
|
|
211 |
Pretty.indent 2 (Syntax.pretty_term ctxt exp),
|
|
212 |
Pretty.str "Basis:"] @
|
|
213 |
map (Pretty.indent 2 o print_basis_elem ctxt) (Asymptotic_Basis.get_basis_list basis))))
|
|
214 |
|
|
215 |
val expansion = gen_expansion Syntax.check_term (K I) (K I) (K I)
|
|
216 |
|
|
217 |
end
|
|
218 |
|
|
219 |
local
|
|
220 |
|
|
221 |
fun parse_opts opts dflt =
|
|
222 |
let
|
|
223 |
val p = map (fn (s, p) => Args.$$$ s |-- Args.colon |-- p) opts
|
|
224 |
in
|
|
225 |
Scan.repeat (Scan.first p) >> (fn xs => fold I xs dflt)
|
|
226 |
end
|
|
227 |
|
|
228 |
val limit_opts =
|
|
229 |
[("limit", Parse.term >> (fn t => fn {facts, ...} => {limit = SOME t, facts = facts})),
|
|
230 |
("facts", Parse.and_list1 Parse.thms1 >>
|
|
231 |
(fn thms => fn {limit, facts} => {limit = limit, facts = facts @ thms}))]
|
|
232 |
|
|
233 |
val dflt_limit_opts = {limit = NONE, facts = []}
|
|
234 |
|
|
235 |
val expansion_opts =
|
|
236 |
[("limit", Parse.term >> (fn t => fn {terms, facts, ...} =>
|
|
237 |
{limit = SOME t, terms = terms, facts = facts})),
|
|
238 |
("facts", Parse.and_list1 Parse.thms1 >>
|
|
239 |
(fn thms => fn {limit, terms, facts} =>
|
|
240 |
{limit = limit, terms = terms, facts = facts @ thms})),
|
|
241 |
("terms", Parse.nat -- Scan.optional (Args.parens (Args.$$$ "strict") >> K true) false >>
|
|
242 |
(fn trms => fn {limit, facts, ...} => {limit = limit, terms = trms, facts = facts}))]
|
|
243 |
|
|
244 |
val dflt_expansion_opts = {limit = NONE, facts = [], terms = (3, false)}
|
|
245 |
|
|
246 |
in
|
|
247 |
|
|
248 |
val _ =
|
69597
|
249 |
Outer_Syntax.command \<^command_keyword>\<open>real_limit\<close>
|
68630
|
250 |
"semi-automatically compute limits of real functions"
|
|
251 |
((Parse.term -- parse_opts limit_opts dflt_limit_opts) >>
|
|
252 |
(fn (t, {limit = flt, facts = thms}) =>
|
|
253 |
(Toplevel.keep (fn state =>
|
|
254 |
Real_Asymp_Diag.limit_cmd (Toplevel.context_of state) thms t flt))))
|
|
255 |
|
|
256 |
val _ =
|
69597
|
257 |
Outer_Syntax.command \<^command_keyword>\<open>real_expansion\<close>
|
68630
|
258 |
"semi-automatically compute expansions of real functions"
|
|
259 |
(Parse.term -- parse_opts expansion_opts dflt_expansion_opts >>
|
|
260 |
(fn (t, {limit = flt, terms = n_strict, facts = thms}) =>
|
|
261 |
(Toplevel.keep (fn state =>
|
|
262 |
Real_Asymp_Diag.expansion_cmd (Toplevel.context_of state) thms (swap n_strict) t flt))))
|
|
263 |
|
|
264 |
end |