[isabelle] tacticals, functionality of ORELSE



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
-------------------------------





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.