761 (* Frequently needed abbreviation: distinguish between idling and non-idling |
761 (* Frequently needed abbreviation: distinguish between idling and non-idling |
762 steps of the implementation, and try to solve the idling case by simplification |
762 steps of the implementation, and try to solve the idling case by simplification |
763 *) |
763 *) |
764 ML {* |
764 ML {* |
765 fun split_idle_tac ss simps i = |
765 fun split_idle_tac ss simps i = |
766 EVERY [TRY (rtac @{thm actionI} i), |
766 TRY (rtac @{thm actionI} i) THEN |
767 DatatypePackage.case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i, |
767 case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN |
768 rewrite_goals_tac @{thms action_rews}, |
768 rewrite_goals_tac @{thms action_rews} THEN |
769 forward_tac [temp_use @{thm Step1_4_7}] i, |
769 forward_tac [temp_use @{thm Step1_4_7}] i THEN |
770 asm_full_simp_tac (ss addsimps simps) i |
770 asm_full_simp_tac (ss addsimps simps) i |
771 ] |
|
772 *} |
771 *} |
773 (* ---------------------------------------------------------------------- |
772 (* ---------------------------------------------------------------------- |
774 Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
773 Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
775 the specification's next-state relation. |
774 the specification's next-state relation. |
776 *) |
775 *) |