Hi Felix,
>However, I discovered the following curious effect: The steps that
>previously failed without REWRITE_TAC can also be solved using *only*
>GOAL_TAC. For example, in the proof I posted a while ago, the following
>step will work.
>
> (\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then &1
>else &0)) [6] by GOAL_TAC,FUN_EQ_THM;
>
>However, if I drop "GOAL_TAC" it will fail with an inference time-out. But
>if I understood you correctly, then GOAL_TAC does nothing but "logging" of
>the relevant subgoal, correct? So what is going on here?
The reason is that "HOL_BY" really tries to _solve_ the
goal, so without leaving subgoals. However, if you give
a tactic yourself, it is allowed to produce subgoals.
These subgoals then have to be trivially solvable by the
statements that are referred to in the by list, and this
last process uses some variant of REWRITE_TAC, I think.
So, if you just put "ALL_TAC", the "do nothing" tactic
(which is what GOAL_TAC really is:
let GOAL_TAC g =
current_goalstack := (mk_goalstate g)::!current_goalstack;
ALL_TAC g;;
), then effectively you are running some kind of REWRITE_TAC,
which as you observed was good enough.
HOL_BY really needs to be modified in such a way that this
thing doesn't happen. But how?
Freek
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
