Hi Jiaqi Tan,
You will need to prove the first two conjuncts at some point. The second
one is already an assumption, so that's easy, but the first one looks like
it might be false. If you can prove them, then the remaining conjunct
(SPEC) should indeed be true by the SPEC_FRAME theorem. One way you could
do this is:
conj_asm1_tac >- (* proof for the first conjunct *) >>
conj_tac >- first_assum ACCEPT_TAC >>
metis_tac[SPEC_FRAME]
Cheers,
Ramana
On Sat, Aug 16, 2014 at 12:44 AM, Jiaqi Tan <tanji...@cmu.edu> wrote:
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
