Hi,
I have the following goal (using the theorems in examples/machine-code) in
HOL4 which I am trying to prove:
val mw2 =
([([``SEP_IMP (aPC offset'' * r) (aPC offset'' * s')``,
``(s = aPC offset'' * s') ∧ SEP_IMP (aPC offset'' * r) s ⇒
SPEC2 x (aPC offset' * q) c2 (aPC offset'' * s')``,
``(q' = aPC offset' * q) ∧ SEP_IMP (aPC offset' * q) q' ⇒
SPEC2 x (aPC offset * p) c1 (aPC offset' * q)``,
``SEP_IMP (aPC offset'' * r) s``,
``s = aPC offset'' * s'``,
``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * r)``,
``q' = aPC offset' * q``],
``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')``)],
fn): goal list * validation
The goal is "SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')", which appears to
be true (by one of the conjuncts in boolTheory.IMP_CLAUSES), but I am
unable to prove it.
When I run "METIS_TAC []" on this goal interactively (by typing it in) from
the HOL shell, I get "[.....] |- SPEC x (aPC offset * p) (c1 ∪ c2) (aPC
offset'' * s') ⇒ SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')",
and when I run "METIS_TAC []" by pasting it into the shell (as the last
tactic in my list of THEN'ed tactics), I get the error:
"Exception-
HOL_ERR
{message = "", origin_function = "CHOOSE", origin_structure = "Thm"}
raised
"
Two of my tactics before reaching the above state are:
(Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset' * q) s ==>
eee`
((Q.X_CHOOSE_THEN `q` (Q.X_CHOOSE_TAC `offset'`)) o (Q.SPECL [`q'`])))
and
(Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset'' * r) s ==>
eee` ((Q.X_CHOOSE_THEN `s'` (Q.X_CHOOSE_TAC `offset''`)) o (Q.SPECL [`s`])))
Could the Q.PAT_ASSUM (or X_CHOOSE_TAC) be causing problems? When I call
Q.PAT_ASSUM and I use X_CHOOSE_TAC to instantiate existentially quantified
variables with some variable, does that add extra assumptions to the
theorem being selected from the assumptions before adding it to the goals?
Thank you!
Regards,
Jiaqi
------------------------------------------------------------------------------
Want excitement?
Manually upgrade your production database.
When you want reliability, choose Perforce.
Perforce version control. Predictably reliable.
http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
