| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Real_Asymp/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Eventuallize.thySprache: Isabelle |
|||||||||||||||
|
section ‹Lifting theorems onto filters› theory Eventuallize imports Complex_Main begin text ‹ The following attribute and ML function lift a given theorem of the form prop‹∀x. A x ⟶ B x ⟶ C x› to prop‹eventually A F ==> eventually B F ==> eventually C F› . › ML ‹ EVENTUALLIZE = eventuallize : Proof.context -> thm -> int option -> thm Eventuallize : EVENTUALLIZE = dest_All (Const (🍋‹HOL.All›, _) $ Abs (x, T, t)) = (x, T, t) | dest_All (Const (🍋‹HOL.All›, T) $ f) = ("x", T |> dest_funT |> fst |> dest_funT |> fst, f $ Bound 0) | dest_All t = raise TERM ("dest_All", [t]) strip_imp (term‹(⟶)› $ a $ b) = apfst (cons a) (strip_imp b) | strip_imp t = ([], t) eventuallize ctxt thm n = let fun err n = raise THM ("Invalid index in eventuallize: " ^ Int.toString n, 0, [t val n_max = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_All |> #3 |> strip_imp |> f val _ = case n of NONE => () | SOME n => if n >= 0 andalso n <= n_max then () else err n val n = case n of SOME n => n | NONE => n_max fun conv n = if n < 2 then Conv.all_conv else Conv.arg_conv (conv (n - 1)) then_conv Conv.rewr_conv @{thm eq_reflection[OF imp_conjL [symmetric]]} val conv = Conv.arg_conv (Conv.binder_conv (K (conv n)) ctxt) val thm' = Conv.fconv_rule conv thm fun go n = if n < 2 then @{thm _} else @{thm eventually_conj} OF [@{thm _}, go (n in @{thm eventually_rev_mp[OF _ always_eventually]} OF [go n, thm'] end attribute_setup eventuallized = ‹ Scan.lift (Scan.option Parse.nat) >> (fn n => fn (ctxt, thm) => (NONE, SOME (Eventuallize.eventuallize (Context.proof_of ctxt) thm n))) › end
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09