Email Gateway (Aug 18 2022 at 15:58): Email Gateway (Aug 18 2022 at 15:58):From: John Munroe <munddr@gmail.com>
Hello all
I'm having my first attempt in writing a tactic and I'm trying to
translate 'using' in Isar into a tactic. Should I be using
proof.put_facts for this? If so, how do I retrieve the current proof
state?
Any help will be appreciated!
John
Email Gateway (Aug 18 2022 at 15:58):From: Alexander Krauss <krauss@in.tum.de>
Hi John,
Unlike Isar proof methods, tactics operate only on the goal state and do
not take chained facts. On that level you can simply pass additional
facts as ML arguments. To provide a method to the user that takes
chained facts, use Method.METHOD (see Pure/Isar/method.ML).
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 15:58):From: John Munroe <munddr@gmail.com>
On Tue, Sep 28, 2010 at 9:42 PM, Alexander Krauss <krauss@in.tum.de> wrote:
Hi John,
I'm having my first attempt in writing a tactic and I'm trying to
translate 'using' in Isar into a tactic. Should I be using
proof.put_facts for this? If so, how do I retrieve the current proof
state?Unlike Isar proof methods, tactics operate only on the goal state and do not
take chained facts. On that level you can simply pass additional facts as ML
arguments. To provide a method to the user that takes chained facts, use
Method.METHOD (see Pure/Isar/method.ML).
I see. But how do I pass additional facts as arguments? Which function
should I pass to?
TIA
John
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 15:58):From: John Munroe <munddr@gmail.com>
Unlike Isar proof methods, tactics operate only on the goal state and do not
take chained facts. On that level you can simply pass additional facts as ML
arguments. To provide a method to the user that takes chained facts, use
Method.METHOD (see Pure/Isar/method.ML).
I see. But how do I pass additional facts as arguments? Which function
should I pass to?
Just some further information: I'd like to apply the auto_tac with
additional facts.
Thanks
John
TIA
John
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 15:58):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
If the facts have no particular form, you can add them as assumptions using Method.insert_tac. E.g.
Method.insert_tac my_extra_facts 1
THEN
auto_tac (cs, ss)
Jasmin
Email Gateway (Aug 18 2022 at 15:59):From: Makarius <makarius@sketis.net>
Maybe you actually want to augment the clasimpset context of auto_tac,
which is actually a pair over claset * simpset. There are various ML
operators for that, such as addIs or addsimps; see the infix declarations
at the start of the following source files:
src/Pure/meta_simplifier.ML
src/Provers/classical.ML
src/Provers/clasimp.ML
Makarius
Last updated: Apr 18 2024 at 01:05 UTC