Email Gateway (Aug 18 2022 at 09:34): Email Gateway (Aug 18 2022 at 09:34):From: Alexander Sauerbier <sandor@cs.tu-berlin.de>
Hello,
I'm experimenting with writing new tactics using tacticals.
And I stepped into a problem... (maybe I just didn't get the
functionality of ORELSE yet)
I reduced my problem to this code:
---------snip-------------
fun tobool "1" = "True"
| tobool "0" = "False"
fun testtac [] i = all_tac
| testtac list i = (res_inst_tac[("x", (hd list) )] exI i) THEN (testtac (tl list) i);
fun testtac1 [] i = all_tac
| testtac1 list i = (res_inst_tac[("x", (hd list) )] exI i)
ORELSE (res_inst_tac[("x", tobool(hd list) )] exI i) THEN (testtac1 (tl list) i);
Goal "(EX (x::int). EX (z::int). (x::int) - x = z)";
by (testtac ["-1000000", "0"] 1); (* works fine *)
auto();
Goal "(EX (x::int). EX (z::int). (x::int) - x = z)";
by (testtac1 ["-1000000", "0"] 1); (* doesn't work, Exception-Match is raised. *)
auto();
---------/snip-------------
If I understand it correctly, /testtac1/ should do exactly the same as
/testtac/, because ORELSE should just try the tactic on operator's left
side and ignore the tactic on the right side... but obviously I didn't
understand it correctly.
Can you give me some hints, please?
(I'm using Poly/ML 4.0 and Isabelle2002.)
Thanks in advance.
Best regards,
alexander sauerbier
Email Gateway (Aug 18 2022 at 09:34):From: Lawrence Paulson <lp15@cam.ac.uk>
When testtac1 is called, ML evaluates both arguments of ORELSE, which
are tactic-valued expressions. The second argument raises exception
Match before ORELSE is even called.
Larry Paulson
Last updated: May 03 2024 at 04:19 UTC