1signature REAL_ASYMP = sig
2val tac : bool -> Proof.context -> int -> tactic
3end
4
5functor Real_Asymp (Exp : EXPANSION_INTERFACE) : REAL_ASYMP = struct
6
7open Lazy_Eval
8
9val dest_arg = dest_comb #> snd
10
11fun 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>\<open>Topological_Spaces.nhds\<close>, _) $ _ => SOME Exp.prove_nhds
18      | \<^term>\<open>at (0 :: real)\<close> => SOME Exp.prove_at_0
19      | \<^term>\<open>at_left (0 :: real)\<close> => SOME Exp.prove_at_left_0
20      | \<^term>\<open>at_right (0 :: real)\<close> => SOME Exp.prove_at_right_0
21      | \<^term>\<open>at_infinity :: real filter\<close> => SOME Exp.prove_at_infinity
22      | \<^term>\<open>at_top :: real filter\<close> => SOME Exp.prove_at_top
23      | \<^term>\<open>at_bot :: real filter\<close> => 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
35fun prove_eventually_at_top ectxt p =
36  case Envir.eta_long [] p of
37    Abs (x, \<^typ>\<open>Real.real\<close>, Const (rel, _) $ f $ g) => ((
38      let
39        val (f, g) = apply2 (fn t => Abs (x, \<^typ>\<open>Real.real\<close>, t)) (f, g)
40        val _ = if rel = \<^const_name>\<open>Orderings.less\<close> 
41                    orelse rel = \<^const_name>\<open>Orderings.less_eq\<close> 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
53fun 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>\<open>smallo\<close> => Exp.prove_smallo
62      | \<^const_name>\<open>bigo\<close> => Exp.prove_bigo
63      | \<^const_name>\<open>bigtheta\<close> => Exp.prove_bigtheta
64      | \<^const_name>\<open>asymp_equiv\<close> => 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
70val filter_substs = 
71  @{thms at_left_to_top at_right_to_top at_left_to_top' at_right_to_top' at_bot_mirror}
72val filterlim_substs = map (fn thm => thm RS @{thm filterlim_conv_filtermap}) filter_substs
73val eventually_substs = map (fn thm => thm RS @{thm eventually_conv_filtermap}) filter_substs
74
75fun 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
82val repeat'_conv = Conv.repeat_conv o changed_conv
83
84fun 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>\<open>real_asymp_nat_reify\<close>
99        val thms2 =
100           Named_Theorems.get ctxt \<^named_theorems>\<open>real_asymp_int_reify\<close>
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
113fun 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>\<open>HOL.Trueprop\<close> $ t => (case t of
121              Const (\<^const_name>\<open>Filter.filterlim\<close>, _) $ _ $ _ $ _ =>
122                Conv.fun_conv (Conv.fun_conv (Conv.arg_conv conv))
123            | Const (\<^const_name>\<open>Filter.eventually\<close>, _) $ _ $ _ =>
124                Conv.fun_conv (Conv.arg_conv conv)
125            | Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (_ $ _ $ _) =>
126                Conv.combination_conv (Conv.arg_conv conv) (Conv.arg_conv conv)
127            | Const (\<^const_name>\<open>Landau_Symbols.asymp_equiv\<close>, _) $ _ $ _ $ _ =>
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
144datatype ('a, 'b) sum = Inl of 'a | Inr of 'b
145
146fun prove_eventually ectxt p filter =
147  case filter of
148    \<^term>\<open>Filter.at_top :: real filter\<close> => (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))
152and prove_limit ectxt f filter filter' =
153  case filter' of
154    \<^term>\<open>Filter.at_top :: real filter\<close> => (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))
158and 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>\<open>HOL.Trueprop\<close> $ t => ((case t of
172            \<^term>\<open>Filter.filterlim :: (real \<Rightarrow> real) \<Rightarrow> _\<close> $ f $ filter $ filter' =>
173              (prove_limit ectxt f filter filter' handle TERM _ => no_tac | THM _ => no_tac)
174          | \<^term>\<open>Filter.eventually :: (real \<Rightarrow> bool) \<Rightarrow> _\<close> $ p $ filter =>
175              (prove_eventually ectxt p filter handle TERM _ => no_tac | THM _ => no_tac)
176          | \<^term>\<open>Set.member :: (real => real) => _\<close> $ f $ 
177              (l $ \<^term>\<open>at_top :: real filter\<close> $ g) =>
178                (prove_landau ectxt l f g handle TERM _ => no_tac | THM _ => no_tac)
179          | (l as \<^term>\<open>Landau_Symbols.asymp_equiv :: (real\<Rightarrow>real)\<Rightarrow>_\<close>) $ 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
196and tac verbose ctxt = tac' verbose (Inl ctxt)
197
198end
199
200structure Real_Asymp_Basic = Real_Asymp(Multiseries_Expansion_Basic)
201