Hi Ramana and Anthony, It turns out that my original goal was indeed not solvable. I had some earlier proof steps prior to the point in my email where I just had to instantiate some variables in EXISTS_TAC correctly for the conjuncts to turn out correctly.
Thank you for the pointers! Regards, Jiaqi On Sat, Aug 16, 2014 at 2:44 AM, Ramana Kumar <[email protected]> wrote: > 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 <[email protected]> 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 >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
