machine-code/hoare-triple/progScript.sml

34   SPEC ((to_set,next,instr,less,allow):('a,'b,'c)processor) p c q =
61   ``!x. RUN x p q = SPEC x p {} q``,
67   ``!x p c q. SPEC x p c q ==> !r. SPEC x (p * r) c (q * r)``,
74   ``!x c q. SPEC x SEP_F c q``,
81   ``!x p c q. SPEC x p c q ==> !r. SEP_IMP r p ==> SPEC x r c q``,
89   ``!x p c q. SPEC x p c q ==> !r. SEP_IMP q r ==> SPEC x p c r``,
101   ``!x p c q. SPEC x p c q ==> !r1 r2. SEP_IMP r1 p /\ SEP_IMP q r2 ==> SPEC x r1 c r2``,
114   ``!x p c q. SPEC x (CODE_POOL (FST (SND (SND x))) c * p) {}
116               SPEC x p c q``,
121   ``!x p c q. SPEC x p c q ==> !c'. SPEC x p (c UNION c') q``,
130        (b /\ i ==> SPEC x p c1 q) ==> (~b /\ j ==> SPEC x p c2 q) ==>
131        ((if b then i else j) ==> SPEC x p (c1 UNION c2) q)``,
139   ``!x p c q. SPEC x p c q ==> !c'. c SUBSET c' ==> SPEC x p c' q``,
146   ``!x:('a,'b,'c)processor p c. SPEC x p c p``,
163       SPEC x p1 c (q1 \/ m) /\ SPEC x (m \/ p2) c q2 ==>
164       SPEC x (p1 \/ p2) c (q1 \/ q2)``,
180       SPEC x p1 c1 (q1 \/ m) /\ SPEC x (m \/ p2) c2 q2 ==>
181       SPEC x (p1 \/ p2) (c1 UNION c2) (q1 \/ q2)``,
185   ``!x p c1 m c2 q. SPEC x p c1 m /\ SPEC x m c2 q ==> SPEC x p (c1 UNION c2) q``,
192       SPEC x (q1 * q3) c q2 ==> SPEC x p c (q1 * q4) ==>
193       SEP_IMP q4 q3 ==> SPEC x p c q2``,
200        (b1 ==> SPEC x (m * q') c2 q) ==>
201        (b2 ==> SPEC x p c1 (m * p')) ==>
202        (b1 /\ b2) ==> SPEC x (p * q') (c1 UNION c2) (q * p')``,
210        (b1 ==> SPEC x (m * q') c2 q) ==>
211        (b2 ==> SPEC x p c1 (m * p' \/ d)) ==>
212        (b1 /\ b2) ==> SPEC x (p * q') (c1 UNION c2) (q * p' \/ d * q')``,
218   \\ POP_ASSUM (MP_TAC o Q.SPEC `p'`)
228   ``!x p p' c q. (!y:'var. SPEC x (p * p' y) c q) = SPEC x (p * ~ p') c q``,
234   ``!x p c q. (!y:'var. SPEC x (p y) c q) = SPEC x (SEP_EXISTS y. p y) c q``,
243   ``!x p c q q' y:'var. SPEC x p c (q * q' y) ==> SPEC x p c (q * ~ q')``,
247   ``!x p c q g. SPEC x (p * cond g) c q = g ==> SPEC x p c q``,
253   ``!x p c q g. SPEC x (p * cond g) c q ==> SPEC x (p * cond g) c (q * cond g)``,
258        SPEC x (p * cond b1) c1 q ==>
259        SPEC x (p * cond b2) c2 q ==>
260        SPEC x (p * cond (b1 \/ b2)) (c1 UNION c2) q``,
266   ``SPEC m (p * cond b) c q = SPEC m (p * cond b) c (q * cond b)``,
270   ``!x p c q. SPEC x p c q ==> !r. SPEC x p c (q \/ r)``,
272   \\ POP_ASSUM (MATCH_MP_TAC o Q.SPEC `q \/ r`)
276   ``!x p1 p2 c q. SPEC x (p1 \/ p2) c q = SPEC x p1 c q /\ SPEC x p2 c q``,
281   ``!x p c q r. SPEC x p c (q \/ r) ==> SPEC x (p \/ r) c (q \/ r)``,
287   ``(!x. SPEC m (P x) c (Q x)) ==> SPEC m (SEP_EXISTS x. P x) c (SEP_EXISTS x. Q x)``,
289   \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `x`)
295       (!x y. g x /\ p x /\ (y = f1 x) ==> SPEC m (res x) c (res y)) /\
296       (!x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res x) c (res' y)) ==>
297       (!x. TAILREC_PRE f1 g p x ==> SPEC m (res x) c (res' (TAILREC f1 f2 g x)))``,
303       (!z x y. g x /\ p x /\ (y = f1 x) ==> SPEC m (res z x) c (res z y)) /\
304       (!z x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res z x) c (res' z y)) ==>
305       (!z x. TAILREC_PRE f1 g p x ==> SPEC m (res z x) c (res' z (TAILREC f1 f2 g x)))``,
311       (!x y. ISL (FST (f x)) /\ SND (f x) /\ (y = OUTL (FST (f x))) ==> SPEC m (res x) c (res y)) /\
312       (!x y. ~ISL (FST (f x)) /\ SND (f x) /\ (y = OUTR (FST (f x))) ==> SPEC m (res x) c (res' y)) ==>
313       (!x. SHORT_TAILREC_PRE f x ==> SPEC m (res x) c (res' (SHORT_TAILREC f x)))``,
319       (!z x y. ISL (FST (f x)) /\ SND (f x) /\ (y = OUTL (FST (f x))) ==> SPEC m (res z x) c (res z y)) /\
320       (!z x y. ~ISL (FST (f x)) /\ SND (f x) /\ (y = OUTR (FST (f x))) ==> SPEC m (res z x) c (res' z y)) ==>
321       (!z x. SHORT_TAILREC_PRE f x ==> SPEC m (res z x) c (res' z (SHORT_TAILREC f x)))``,