231 frequently_bex_finite_distrib |
231 frequently_bex_finite_distrib |
232 frequently_all |
232 frequently_all |
233 frequently_imp_iff |
233 frequently_imp_iff |
234 |
234 |
235 ML \<open> |
235 ML \<open> |
236 fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) => |
236 fun eventually_elim_tac facts = |
237 let |
237 CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => |
238 val mp_thms = facts RL @{thms eventually_rev_mp} |
238 let |
239 val raw_elim_thm = |
239 val mp_thms = facts RL @{thms eventually_rev_mp} |
240 (@{thm allI} RS @{thm always_eventually}) |
240 val raw_elim_thm = |
241 |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms |
241 (@{thm allI} RS @{thm always_eventually}) |
242 |> fold (fn _ => fn thm => @{thm impI} RS thm) facts |
242 |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms |
243 val cases_prop = |
243 |> fold (fn _ => fn thm => @{thm impI} RS thm) facts |
244 Thm.prop_of |
244 val cases_prop = |
245 (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))) |
245 Thm.prop_of |
246 val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])] |
246 (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))) |
247 in |
247 val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])] |
248 CASES cases (resolve_tac ctxt [raw_elim_thm] i) |
248 in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end) |
249 end) |
|
250 \<close> |
249 \<close> |
251 |
250 |
252 method_setup eventually_elim = \<open> |
251 method_setup eventually_elim = \<open> |
253 Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt)) |
252 Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1)) |
254 \<close> "elimination of eventually quantifiers" |
253 \<close> "elimination of eventually quantifiers" |
255 |
254 |
256 subsubsection \<open>Finer-than relation\<close> |
255 subsubsection \<open>Finer-than relation\<close> |
257 |
256 |
258 text \<open>@{term "F \<le> F'"} means that filter @{term F} is finer than |
257 text \<open>@{term "F \<le> F'"} means that filter @{term F} is finer than |