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