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