|
1 signature REAL_ASYMP = sig |
|
2 val tac : bool -> Proof.context -> int -> tactic |
|
3 end |
|
4 |
|
5 functor Real_Asymp (Exp : EXPANSION_INTERFACE) : REAL_ASYMP = struct |
|
6 |
|
7 open Lazy_Eval |
|
8 |
|
9 val dest_arg = dest_comb #> snd |
|
10 |
|
11 fun prove_limit_at_top ectxt f filter = |
|
12 let |
|
13 val ctxt = get_ctxt ectxt |
|
14 val basis = Asymptotic_Basis.default_basis |
|
15 val prover = |
|
16 case filter of |
|
17 Const (@{const_name "Topological_Spaces.nhds"}, _) $ _ => SOME Exp.prove_nhds |
|
18 | @{term "at (0 :: real)"} => SOME Exp.prove_at_0 |
|
19 | @{term "at_left (0 :: real)"} => SOME Exp.prove_at_left_0 |
|
20 | @{term "at_right (0 :: real)"} => SOME Exp.prove_at_right_0 |
|
21 | @{term "at_infinity :: real filter"} => SOME Exp.prove_at_infinity |
|
22 | @{term "at_top :: real filter"} => SOME Exp.prove_at_top |
|
23 | @{term "at_bot :: real filter"} => SOME Exp.prove_at_bot |
|
24 | _ => NONE |
|
25 val lim_thm = Option.map (fn prover => prover ectxt (Exp.expand_term ectxt f basis)) prover |
|
26 in |
|
27 case lim_thm of |
|
28 NONE => no_tac |
|
29 | SOME lim_thm => |
|
30 HEADGOAL ( |
|
31 resolve_tac ctxt [lim_thm, lim_thm RS @{thm filterlim_mono'}] |
|
32 THEN_ALL_NEW (TRY o resolve_tac ctxt @{thms at_within_le_nhds at_within_le_at nhds_leI})) |
|
33 end |
|
34 |
|
35 fun prove_eventually_at_top ectxt p = |
|
36 case Envir.eta_long [] p of |
|
37 Abs (x, @{typ Real.real}, Const (rel, _) $ f $ g) => (( |
|
38 let |
|
39 val (f, g) = apply2 (fn t => Abs (x, @{typ Real.real}, t)) (f, g) |
|
40 val _ = if rel = @{const_name "Orderings.less"} |
|
41 orelse rel = @{const_name "Orderings.less_eq"} then () |
|
42 else raise TERM ("prove_eventually_at_top", [p]) |
|
43 val ctxt = get_ctxt ectxt |
|
44 val basis = Asymptotic_Basis.default_basis |
|
45 val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis |
|
46 val thm = Exp.prove_eventually_less ectxt (thm1, thm2, basis) |
|
47 in |
|
48 HEADGOAL (resolve_tac ctxt [thm, thm RS @{thm eventually_lt_imp_eventually_le}]) |
|
49 end) |
|
50 handle TERM _ => no_tac | THM _ => no_tac) |
|
51 | _ => raise TERM ("prove_eventually_at_top", [p]) |
|
52 |
|
53 fun prove_landau ectxt l f g = |
|
54 let |
|
55 val ctxt = get_ctxt ectxt |
|
56 val l' = l |> dest_Const |> fst |
|
57 val basis = Asymptotic_Basis.default_basis |
|
58 val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis |
|
59 val prover = |
|
60 case l' of |
|
61 @{const_name smallo} => Exp.prove_smallo |
|
62 | @{const_name bigo} => Exp.prove_bigo |
|
63 | @{const_name bigtheta} => Exp.prove_bigtheta |
|
64 | @{const_name asymp_equiv} => Exp.prove_asymp_equiv |
|
65 | _ => raise TERM ("prove_landau", [f, g]) |
|
66 in |
|
67 HEADGOAL (resolve_tac ctxt [prover ectxt (thm1, thm2, basis)]) |
|
68 end |
|
69 |
|
70 val filter_substs = |
|
71 @{thms at_left_to_top at_right_to_top at_left_to_top' at_right_to_top' at_bot_mirror} |
|
72 val filterlim_substs = map (fn thm => thm RS @{thm filterlim_conv_filtermap}) filter_substs |
|
73 val eventually_substs = map (fn thm => thm RS @{thm eventually_conv_filtermap}) filter_substs |
|
74 |
|
75 fun changed_conv conv ct = |
|
76 let |
|
77 val thm = conv ct |
|
78 in |
|
79 if Thm.is_reflexive thm then raise CTERM ("changed_conv", [ct]) else thm |
|
80 end |
|
81 |
|
82 val repeat'_conv = Conv.repeat_conv o changed_conv |
|
83 |
|
84 fun preproc_exp_log_natintfun_conv ctxt = |
|
85 let |
|
86 fun reify_power_conv x _ ct = |
|
87 let |
|
88 val thm = Conv.rewr_conv @{thm reify_power} ct |
|
89 in |
|
90 if exists_subterm (fn t => t aconv x) (Thm.term_of ct |> dest_arg) then |
|
91 thm |
|
92 else |
|
93 raise CTERM ("reify_power_conv", [ct]) |
|
94 end |
|
95 fun conv (x, ctxt) = |
|
96 let |
|
97 val thms1 = |
|
98 Named_Theorems.get ctxt @{named_theorems real_asymp_nat_reify} |
|
99 val thms2 = |
|
100 Named_Theorems.get ctxt @{named_theorems real_asymp_int_reify} |
|
101 val ctxt' = put_simpset HOL_basic_ss ctxt addsimps (thms1 @ thms2) |
|
102 in |
|
103 repeat'_conv ( |
|
104 Simplifier.rewrite ctxt' |
|
105 then_conv Conv.bottom_conv (Conv.try_conv o reify_power_conv (Thm.term_of x)) ctxt) |
|
106 end |
|
107 in |
|
108 Thm.eta_long_conversion |
|
109 then_conv Conv.abs_conv conv ctxt |
|
110 then_conv Thm.eta_conversion |
|
111 end |
|
112 |
|
113 fun preproc_tac ctxt = |
|
114 let |
|
115 fun natint_tac {context = ctxt, concl = goal, ...} = |
|
116 let |
|
117 val conv = preproc_exp_log_natintfun_conv ctxt |
|
118 val conv = |
|
119 case Thm.term_of goal of |
|
120 @{term "HOL.Trueprop"} $ t => (case t of |
|
121 Const (@{const_name Filter.filterlim}, _) $ _ $ _ $ _ => |
|
122 Conv.fun_conv (Conv.fun_conv (Conv.arg_conv conv)) |
|
123 | Const (@{const_name Filter.eventually}, _) $ _ $ _ => |
|
124 Conv.fun_conv (Conv.arg_conv conv) |
|
125 | Const (@{const_name Set.member}, _) $ _ $ (_ $ _ $ _) => |
|
126 Conv.combination_conv (Conv.arg_conv conv) (Conv.arg_conv conv) |
|
127 | Const (@{const_name Landau_Symbols.asymp_equiv}, _) $ _ $ _ $ _ => |
|
128 Conv.combination_conv (Conv.fun_conv (Conv.arg_conv conv)) conv |
|
129 | _ => Conv.all_conv) |
|
130 | _ => Conv.all_conv |
|
131 in |
|
132 HEADGOAL (CONVERSION (Conv.try_conv (Conv.arg_conv conv))) |
|
133 end |
|
134 in |
|
135 SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms real_asymp_preproc}) |
|
136 THEN' TRY o resolve_tac ctxt @{thms real_asymp_real_nat_transfer real_asymp_real_int_transfer} |
|
137 THEN' TRY o resolve_tac ctxt |
|
138 @{thms filterlim_at_leftI filterlim_at_rightI filterlim_atI' landau_reduce_to_top} |
|
139 THEN' TRY o resolve_tac ctxt @{thms smallo_imp_smallomega bigo_imp_bigomega} |
|
140 THEN' TRY o Subgoal.FOCUS_PREMS natint_tac ctxt |
|
141 THEN' TRY o resolve_tac ctxt @{thms real_asymp_nat_intros real_asymp_int_intros} |
|
142 end |
|
143 |
|
144 datatype ('a, 'b) sum = Inl of 'a | Inr of 'b |
|
145 |
|
146 fun prove_eventually ectxt p filter = |
|
147 case filter of |
|
148 @{term "Filter.at_top :: real filter"} => (prove_eventually_at_top ectxt p |
|
149 handle TERM _ => no_tac | THM _ => no_tac) |
|
150 | _ => HEADGOAL (CONVERSION (Conv.rewrs_conv eventually_substs) |
|
151 THEN' tac' (#verbose (#ctxt ectxt)) (Inr ectxt)) |
|
152 and prove_limit ectxt f filter filter' = |
|
153 case filter' of |
|
154 @{term "Filter.at_top :: real filter"} => (prove_limit_at_top ectxt f filter |
|
155 handle TERM _ => no_tac | THM _ => no_tac) |
|
156 | _ => HEADGOAL (CONVERSION (Conv.rewrs_conv filterlim_substs) |
|
157 THEN' tac' (#verbose (#ctxt ectxt)) (Inr ectxt)) |
|
158 and tac' verbose ctxt_or_ectxt = |
|
159 let |
|
160 val ctxt = case ctxt_or_ectxt of Inl ctxt => ctxt | Inr ectxt => get_ctxt ectxt |
|
161 fun tac {context = ctxt, prems, concl = goal, ...} = |
|
162 (if verbose then print_tac ctxt "real_asymp: Goal after preprocessing" else all_tac) THEN |
|
163 let |
|
164 val ectxt = |
|
165 case ctxt_or_ectxt of |
|
166 Inl _ => |
|
167 Multiseries_Expansion.mk_eval_ctxt ctxt |> add_facts prems |> set_verbose verbose |
|
168 | Inr ectxt => ectxt |
|
169 in |
|
170 case Thm.term_of goal of |
|
171 @{term "HOL.Trueprop"} $ t => ((case t of |
|
172 @{term "Filter.filterlim :: (real \<Rightarrow> real) \<Rightarrow> _"} $ f $ filter $ filter' => |
|
173 (prove_limit ectxt f filter filter' handle TERM _ => no_tac | THM _ => no_tac) |
|
174 | @{term "Filter.eventually :: (real \<Rightarrow> bool) \<Rightarrow> _"} $ p $ filter => |
|
175 (prove_eventually ectxt p filter handle TERM _ => no_tac | THM _ => no_tac) |
|
176 | @{term "Set.member :: (real => real) => _"} $ f $ |
|
177 (l $ @{term "at_top :: real filter"} $ g) => |
|
178 (prove_landau ectxt l f g handle TERM _ => no_tac | THM _ => no_tac) |
|
179 | (l as @{term "Landau_Symbols.asymp_equiv :: (real\<Rightarrow>real)\<Rightarrow>_"}) $ f $ _ $ g => |
|
180 (prove_landau ectxt l f g handle TERM _ => no_tac | THM _ => no_tac) |
|
181 | _ => no_tac) THEN distinct_subgoals_tac) |
|
182 | _ => no_tac |
|
183 end |
|
184 fun tac' i = Subgoal.FOCUS_PREMS tac ctxt i handle TERM _ => no_tac | THM _ => no_tac |
|
185 val at_tac = |
|
186 HEADGOAL (resolve_tac ctxt |
|
187 @{thms filterlim_split_at eventually_at_left_at_right_imp_at landau_at_top_imp_at |
|
188 asymp_equiv_at_top_imp_at}) |
|
189 THEN PARALLEL_ALLGOALS tac' |
|
190 in |
|
191 (preproc_tac ctxt |
|
192 THEN' preproc_tac ctxt |
|
193 THEN' (SELECT_GOAL at_tac ORELSE' tac')) |
|
194 THEN_ALL_NEW (TRY o SELECT_GOAL (SOLVE (HEADGOAL (Simplifier.asm_full_simp_tac ctxt)))) |
|
195 end |
|
196 and tac verbose ctxt = tac' verbose (Inl ctxt) |
|
197 |
|
198 end |
|
199 |
|
200 structure Real_Asymp_Basic = Real_Asymp(Multiseries_Expansion_Basic) |