equal
deleted
inserted
replaced
17 Addsimps [tl_not_self]; |
17 Addsimps [tl_not_self]; |
18 |
18 |
19 (* ---------------------------- Action lemmas ---------------------------- *) |
19 (* ---------------------------- Action lemmas ---------------------------- *) |
20 |
20 |
21 (* Dequeue is visible *) |
21 (* Dequeue is visible *) |
22 Goal "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"; |
22 Goalw [angle_def,Deq_def] "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"; |
23 by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def])); |
23 by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1)); |
24 qed "Deq_visible"; |
24 qed "Deq_visible"; |
25 |
25 |
26 (* Enabling condition for dequeue -- NOT NEEDED *) |
26 (* Enabling condition for dequeue -- NOT NEEDED *) |
27 Goalw [temp_rewrite Deq_visible] |
27 Goalw [temp_rewrite Deq_visible] |
28 "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"; |
28 "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"; |