1open HolKernel boolLib bossLib 2open set_sepTheory progTheory temporalTheory stateTheory 3 4val _ = new_theory "temporal_state" 5 6infix \\ 7val op \\ = op THEN; 8 9(* ------------------------------------------------------------------------ *) 10 11val TEMPORAL_NEXT_def = Define` 12 TEMPORAL_NEXT 13 ((to_set,next,instr,less,avoid): ('a, 'b, 'c) processor) p c q = 14 TEMPORAL (to_set,next,instr,$=,K F) c (T_IMPLIES (NOW p) (NEXT (NOW q)))` 15 16(* ------------------------------------------------------------------------ *) 17 18val INIT = 19 strip_tac 20 \\ `?to_set next instr less avoid. x = (to_set,next,instr,less,avoid)` 21 by metis_tac [pairTheory.PAIR] 22 23val TEMPORAL_NEXT_MOVE_COND = Q.store_thm("TEMPORAL_NEXT_MOVE_COND", 24 `!x p c q g. 25 TEMPORAL_NEXT x (p * cond g) c q <=> g ==> TEMPORAL_NEXT x p c q`, 26 INIT 27 \\ Cases_on `g` 28 \\ simp [SEP_F_def, TEMPORAL_NEXT_def, TEMPORAL_def, SEP_CLAUSES, 29 SEP_REFINE_def, T_IMPLIES_def, NOW_def] 30 ) 31 32val TEMPORAL_NEXT_FRAME = Q.store_thm("TEMPORAL_NEXT_FRAME", 33 `!x p c q. TEMPORAL_NEXT x p c q ==> !r. TEMPORAL_NEXT x (p * r) c (q * r)`, 34 INIT 35 \\ simp [GSYM STAR_ASSOC, TEMPORAL_NEXT_def, TEMPORAL_def, 36 T_IMPLIES_def, NOW_def, NEXT_def] 37 \\ REPEAT strip_tac 38 \\ qpat_assum `!a. b` 39 (qspecl_then [`state`, `seq`, `r * r'`] imp_res_tac) 40 \\ fs [AC STAR_COMM STAR_ASSOC] 41 ) 42 43val TEMPORAL_NEXT_DUPLICATE_COND = Q.store_thm("TEMPORAL_NEXT_DUPLICATE_COND", 44 `!x p c q g. 45 TEMPORAL_NEXT x (p * cond g) c q ==> 46 TEMPORAL_NEXT x (p * cond g) c (q * cond g)`, 47 simp [TEMPORAL_NEXT_MOVE_COND, SEP_CLAUSES] 48 ) 49 50val TEMPORAL_NEXT_FALSE_PRE = Q.store_thm("TEMPORAL_NEXT_FALSE_PRE", 51 `!x c q. TEMPORAL_NEXT x SEP_F c q`, 52 INIT 53 \\ simp [SEP_F_def, TEMPORAL_NEXT_def, TEMPORAL_def, SEP_CLAUSES, 54 SEP_REFINE_def, T_IMPLIES_def, NOW_def] 55 ) 56 57(* ------------------------------------------------------------------------ *) 58 59val CODE_POOL_EMP = Q.prove( 60 `!instr. CODE_POOL instr {} = emp`, 61 simp [CODE_POOL_def, emp_def] 62 ) 63 64val SPLIT_STATE_cor = METIS_PROVE [SPLIT_STATE] 65 ``p (SELECT_STATE m y s) ==> 66 ?u v. SPLIT (STATE m s) (u, v) /\ p u /\ (\v. v = FRAME_STATE m y s) v`` 67 68val TEMPORAL_STATE_SEMANTICS = Q.store_thm("TEMPORAL_STATE_SEMANTICS", 69 `!m next instr less avoid p q. 70 TEMPORAL_NEXT (STATE m, next, instr, less, avoid) p {} q = 71 !state y seq. 72 p (SELECT_STATE m y (seq 0)) /\ rel_sequence next seq state ==> 73 q (SELECT_STATE m y (seq 1)) /\ 74 (FRAME_STATE m y (seq 0) = FRAME_STATE m y (seq 1))`, 75 simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def, 76 CODE_POOL_EMP, SEP_CLAUSES] 77 \\ simp [STAR_def, SEP_REFINE_def] 78 \\ REPEAT strip_tac 79 \\ Tactical.REVERSE eq_tac 80 \\ REPEAT strip_tac 81 >- (full_simp_tac std_ss [SPLIT_STATE] 82 \\ metis_tac []) 83 \\ imp_res_tac SPLIT_STATE_cor 84 \\ res_tac 85 \\ full_simp_tac bool_ss [SPLIT_STATE] 86 \\ metis_tac [FRAME_SET_EQ] 87 ) 88 89val IMP_TEMPORAL = Q.prove( 90 `!m next instr less avoid p q. 91 (!y s. 92 p (SELECT_STATE m y s) ==> 93 ?v. (next s = SOME v) /\ q (SELECT_STATE m y v) /\ 94 (FRAME_STATE m y s = FRAME_STATE m y v)) ==> 95 TEMPORAL_NEXT (STATE m, NEXT_REL (=) next, instr, less, avoid) p {} q`, 96 rewrite_tac [TEMPORAL_STATE_SEMANTICS] 97 \\ REPEAT strip_tac 98 \\ `NEXT_REL (=) next (seq 0) (seq (SUC 0))` 99 by ( 100 `?x. NEXT_REL (=) next (seq 0) x` 101 by (res_tac 102 \\ qexists_tac `v` 103 \\ asm_simp_tac std_ss [NEXT_REL_def] 104 \\ qexists_tac `seq 0` 105 \\ asm_simp_tac std_ss [] 106 \\ full_simp_tac bool_ss [rel_sequence_def] 107 ) 108 \\ metis_tac [rel_sequence_def] 109 ) 110 \\ full_simp_tac std_ss [NEXT_REL_def] 111 \\ qpat_assum `!y:'b set. P` (qspecl_then [`y`,`seq 0`] imp_res_tac) 112 \\ metis_tac [optionTheory.SOME_11] 113 ) 114 115val TEMPORAL_NEXT_CODE = Q.store_thm("TEMPORAL_NEXT_CODE", 116 `!x p c q. 117 TEMPORAL_NEXT x (CODE_POOL (FST (SND (SND x))) c * p) {} 118 (CODE_POOL (FST (SND (SND x))) c * q) = 119 TEMPORAL_NEXT x p c q`, 120 INIT 121 \\ simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def, 122 CODE_POOL_EMP, SEP_CLAUSES, 123 AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] 124 ) 125 126val TEMPORAL_MOVE_CODE = Q.store_thm("TEMPORAL_MOVE_CODE", 127 `!to_set next instr less avoid p c q. 128 TEMPORAL_NEXT (to_set,next,instr,less,avoid) 129 (p * CODE_POOL instr c) {} (q * CODE_POOL instr c) = 130 TEMPORAL_NEXT (to_set,next,instr,less,avoid) p c q`, 131 simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def, 132 CODE_POOL_EMP, SEP_CLAUSES] 133 ) 134 135val IMP_TEMPORAL = Theory.save_thm ("IMP_TEMPORAL", 136 IMP_TEMPORAL 137 |> Q.SPECL [`m`, `next`, `instr: 'd -> 'b # 'c -> bool`, `less`, `avoid`, 138 `p * CODE_POOL instr (c: 'd -> bool)`, 139 `q * CODE_POOL instr (c: 'd -> bool)`] 140 |> REWRITE_RULE [TEMPORAL_MOVE_CODE] 141 |> Q.GENL [`m`, `next`, `instr`, `less`, `avoid`, `c`, `p`, `q`] 142 ) 143 144(* ------------------------------------------------------------------------ *) 145 146fun SPECC_FRAME_RULE frame th = 147 Thm.SPEC frame (Drule.MATCH_MP TEMPORAL_NEXT_FRAME th) 148 149val SEP_ARRAY_TEMPORAL_FRAME = Q.store_thm("SEP_ARRAY_TEMPORAL_FRAME", 150 `!x (prefix: 'a word list) (postfix: 'a word list) p c q m i a l1 l2. 151 (LENGTH l2 = LENGTH l1) /\ 152 TEMPORAL_NEXT x (p * SEP_ARRAY m i a l1) c (q * SEP_ARRAY m i a l2) ==> 153 TEMPORAL_NEXT x (p * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 154 (prefix ++ l1 ++ postfix)) c 155 (q * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 156 (prefix ++ l2 ++ postfix))`, 157 REPEAT strip_tac 158 \\ rewrite_tac [set_sepTheory.SEP_ARRAY_APPEND] 159 \\ pop_assum 160 (assume_tac o 161 SPECC_FRAME_RULE 162 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i 163 (a - n2w (LENGTH prefix) * i) (prefix: 'a word list)``) 164 \\ pop_assum 165 (assume_tac o 166 SPECC_FRAME_RULE 167 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i 168 (a - n2w (LENGTH (prefix: 'a word list)) * i + 169 n2w (LENGTH (prefix ++ l1)) * i) 170 (postfix: 'a word list)``) 171 \\ full_simp_tac (srw_ss()++helperLib.star_ss) [] 172 ) 173 174(* ------------------------------------------------------------------------ *) 175 176val () = export_theory () 177