Hi,
I am using the Hoare logic in examples/machine-code, and I encountered this
subgoal in a proof I am working on:
val msf1111 =
([([``SPEC x (cond ms * p') {(offset,ins)} q``,
``c = {(offset,ins)}``,
``p = cond ms * p'``],
``(p * r = cond ms * p') ∧ (c = {(offset,ins)}) ∧
SPEC x (cond ms * p') {(offset,ins)} (q * r)``)],
fn): goal list * validation
It seems like the first and second conjuncts "(p * r = cond ms * p')" and
"(c = {(offset,ins)})" in the goal term are just syntactic rewrites that
can be rewritten into the third conjunct, "SPEC x (cond ms * p')
{(offset,ins)} (q * r)".
I am trying to prove the goal using the SPEC_FRAME theorem (Hoare logic
frame rule, "|- ∀x p c q. SPEC x p c q ⇒ ∀r. SPEC x (p * r) c (q * r)"),
but I can't get the goal to match the form in SPEC_FRAME because of the
first two conjuncts ("(p * r = cond ms * p')" and "(c = {(offset,ins)})")
in the goal term. Is there any way to force the first two conjuncts to be
rewritten into the pre- and post-conditions of the SPEC term in the goal
term so that I can use the SPEC_FRAME theorem to prove the goal?
Or am I misunderstanding the meaning of the first two conjuncts ("(p * r =
cond ms * p')" and "(c = {(offset,ins)})") in the goal term?
Thank you!
Regards,
Jiaqi Tan
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
