Email Gateway (Aug 22 2022 at 13:06): Email Gateway (Aug 22 2022 at 13:06):From: Simon Wimmer <wimmersimon@gmail.com>
Dear Eisbach experts,
I have an Eisbach method, which per default acts as "structured method"
(like rule).
However, I would like to turn it into a "simple method" (like simp, blast
and friends) by essentially mimicking the behaviour of
apply -
apply <Eisbach method>
Browsing the manuals and the source of method.ml, I wasn't able to figure
out a way to do so. Is there an easy one?
Simon
Email Gateway (Aug 22 2022 at 13:06):From: Daniel Matichuk <Daniel.Matichuk@nicta.com.au>
Hi Simon,
Eisbach methods aren’t really structured or unstructured, they inherit that from the methods they comprise. This behaviour comes from how the combinators work, i.e. if you write “(-, rule)” then the “rule” invocation gets the using context. There is certainly a case for treating this more explicitly in Eisbach: I was never convinced one way or the other what a sensible default should be.
My understanding is that you want to hide the “using” context from the Eisbach method, choosing instead to insert it into the goal state first. You are always free to write your own higher-order method in order to do this sort of fiddling:
method_setup simple_method =
‹Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
val insert' = Method.Basic (K (Method.insert facts))
val m' = Method.Combinator (Method.no_combinator_info, Method.Then, [insert', m])
in Method_Closure.method_evaluate m' ctxt [] end)›
method use_spec = simple_method ‹erule spec›
lemma
assumes P: "∀x. P x"
shows "P x"
using P
by use_spec
-Dan
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 01:05 UTC