1section \<open>Lifting theorems onto filters\<close> 2theory Eventuallize 3 imports Complex_Main 4begin 5 6text \<open> 7 The following attribute and ML function lift a given theorem of the form 8 \<^prop>\<open>\<forall>x. A x \<longrightarrow> B x \<longrightarrow> C x\<close> 9 to 10 \<^prop>\<open>eventually A F \<Longrightarrow> eventually B F \<Longrightarrow> eventually C F\<close> . 11\<close> 12 13ML \<open> 14signature EVENTUALLIZE = 15sig 16val eventuallize : Proof.context -> thm -> int option -> thm 17end 18 19structure Eventuallize : EVENTUALLIZE = 20struct 21 22fun dest_All (Const (\<^const_name>\<open>HOL.All\<close>, _) $ Abs (x, T, t)) = (x, T, t) 23 | dest_All (Const (\<^const_name>\<open>HOL.All\<close>, T) $ f) = 24 ("x", T |> dest_funT |> fst |> dest_funT |> fst, f $ Bound 0) 25 | dest_All t = raise TERM ("dest_All", [t]) 26 27fun strip_imp (\<^term>\<open>(\<longrightarrow>)\<close> $ a $ b) = apfst (cons a) (strip_imp b) 28 | strip_imp t = ([], t) 29 30fun eventuallize ctxt thm n = 31 let 32 fun err n = raise THM ("Invalid index in eventuallize: " ^ Int.toString n, 0, [thm]) 33 val n_max = 34 thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_All |> #3 |> strip_imp |> fst |> length 35 val _ = case n of NONE => () | SOME n => 36 if n >= 0 andalso n <= n_max then () else err n 37 val n = case n of SOME n => n | NONE => n_max 38 fun conv n = 39 if n < 2 then Conv.all_conv else Conv.arg_conv (conv (n - 1)) then_conv 40 Conv.rewr_conv @{thm eq_reflection[OF imp_conjL [symmetric]]} 41 val conv = Conv.arg_conv (Conv.binder_conv (K (conv n)) ctxt) 42 val thm' = Conv.fconv_rule conv thm 43 fun go n = if n < 2 then @{thm _} else @{thm eventually_conj} OF [@{thm _}, go (n - 1)] 44 in 45 @{thm eventually_rev_mp[OF _ always_eventually]} OF [go n, thm'] 46 end 47 48end 49\<close> 50 51attribute_setup eventuallized = \<open> 52 Scan.lift (Scan.option Parse.nat) >> 53 (fn n => fn (ctxt, thm) => 54 (NONE, SOME (Eventuallize.eventuallize (Context.proof_of ctxt) thm n))) 55\<close> 56 57end