1open HolKernel Parse boolLib bossLib 2open progTheory pairTheory set_sepTheory arithmeticTheory; 3 4val _ = new_theory "temporal" 5val _ = ParseExtras.temp_loose_equality() 6 7 8(* --- definitions --- *) 9 10val TEMPORAL_def = Define ` 11 TEMPORAL ((to_set,next,instr,less,allow): ('a,'b,'c) processor) c exp = 12 !state seq r. 13 rel_sequence next seq state ==> 14 let f p state = SEP_REFINE (p * CODE_POOL instr c * r) less to_set state 15 \/ allow state in 16 exp f seq` 17 18val f = ``f: 'a set set -> 'b set`` 19val seq = ``seq: num -> 'b`` 20 21val NOW_def = Define `NOW p ^f seq = f p (seq 0)` 22val NEXT_def = Define `NEXT p ^f seq = p f (\n. seq (n + 1:num))` 23val EVENTUALLY_def = Define `EVENTUALLY p ^f seq = ?k. p f (\n. seq (n + k:num))` 24val ALWAYS_def = Define `ALWAYS p ^f seq = !k. p f (\n. seq (n + k:num))` 25 26val T_AND_def = Define `T_AND p q ^f ^seq = p ^f ^seq /\ q ^f ^seq` 27val T_IMPLIES_def = Define `T_IMPLIES p q ^f ^seq = p f seq ==> q f seq` 28 29val T_OR_F_def = Define `T_OR_F p post ^f ^seq = p ^f ^seq \/ 30 (EVENTUALLY (NOW post)) ^f ^seq` 31 32val SPEC_1_def = Define ` 33 SPEC_1 model pre code post err <=> 34 TEMPORAL model code 35 (T_IMPLIES (NOW pre) 36 (T_OR_F (NEXT (EVENTUALLY (NOW post))) err))`; 37 38(* --- theorems --- *) 39 40val INIT = `?to_set next instr less allow. model = (to_set,next,instr,less,allow)` 41 by METIS_TAC [PAIR] 42 43val SPEC_EQ_TEMPORAL = Q.store_thm("SPEC_EQ_TEMPORAL", 44 `SPEC model pre code post <=> 45 TEMPORAL model code (T_IMPLIES (NOW pre) (EVENTUALLY (NOW post)))`, 46 INIT 47 \\ ASM_SIMP_TAC std_ss 48 [SPEC_def, TEMPORAL_def, RUN_def, LET_DEF, PULL_FORALL, T_IMPLIES_def, 49 NOW_def, EVENTUALLY_def, rel_sequence_def] 50 \\ SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM, GSYM rel_sequence_def] 51 \\ METIS_TAC []); 52 53val TEMPORAL_ALWAYS = Q.store_thm("TEMPORAL_ALWAYS", 54 `TEMPORAL model code (ALWAYS p) <=> TEMPORAL model code p`, 55 INIT 56 \\ ASM_SIMP_TAC std_ss 57 [SPEC_def, TEMPORAL_def, RUN_def, LET_DEF, PULL_FORALL, 58 T_IMPLIES_def, NOW_def, ALWAYS_def] 59 \\ REPEAT STRIP_TAC 60 \\ EQ_TAC 61 \\ REPEAT STRIP_TAC 62 THEN1 (FIRST_X_ASSUM (MP_TAC o Q.SPECL [`state`, `seq`, `r`, `0`]) 63 \\ FULL_SIMP_TAC std_ss [] 64 \\ CONV_TAC (DEPTH_CONV ETA_CONV) 65 \\ SIMP_TAC std_ss []) 66 \\ FIRST_X_ASSUM MATCH_MP_TAC 67 \\ Q.EXISTS_TAC `seq k` 68 \\ FULL_SIMP_TAC std_ss [rel_sequence_def] 69 \\ REPEAT STRIP_TAC 70 \\ FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `n + k`) 71 \\ FULL_SIMP_TAC std_ss [ADD_CLAUSES]) 72 73val TEMPORAL_NEXT_IMP_EVENTUALLY = Q.store_thm("TEMPORAL_NEXT_IMP_EVENTUALLY", 74 `TEMPORAL model code (T_IMPLIES p1 (NEXT p2)) ==> 75 TEMPORAL model code (T_IMPLIES p1 (EVENTUALLY p2))`, 76 INIT 77 \\ ASM_SIMP_TAC std_ss 78 [TEMPORAL_def, LET_DEF, T_IMPLIES_def, NEXT_def, EVENTUALLY_def] 79 \\ METIS_TAC []) 80 81val SPEC_1_IMP_SPEC = store_thm("SPEC_1_IMP_SPEC", 82 ``SPEC_1 model pre code post err ==> 83 SPEC model pre code (post \/ err)``, 84 INIT 85 \\ FULL_SIMP_TAC std_ss [SPEC_1_def,SPEC_EQ_TEMPORAL,TEMPORAL_def,LET_DEF] 86 \\ REPEAT STRIP_TAC \\ RES_TAC 87 \\ FULL_SIMP_TAC std_ss [T_IMPLIES_def] \\ REPEAT STRIP_TAC \\ RES_TAC 88 \\ FULL_SIMP_TAC std_ss [T_OR_F_def] 89 \\ FULL_SIMP_TAC std_ss [NEXT_def,EVENTUALLY_def] 90 THEN1 (Q.EXISTS_TAC `k+1` \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 91 \\ POP_ASSUM MP_TAC 92 \\ SIMP_TAC std_ss [NOW_def,SEP_REFINE_def,SEP_CLAUSES] 93 \\ SIMP_TAC std_ss [SEP_DISJ_def] \\ METIS_TAC []) 94 THEN1 (Q.EXISTS_TAC `k` \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 95 \\ POP_ASSUM MP_TAC 96 \\ SIMP_TAC std_ss [NOW_def,SEP_REFINE_def,SEP_CLAUSES] 97 \\ SIMP_TAC std_ss [SEP_DISJ_def] \\ METIS_TAC [])); 98 99val SPEC_IMP_SPEC_1 = store_thm("SPEC_IMP_SPEC_1", 100 ``SPEC model pre code (post \/ err) ==> 101 let to_set = FST model in 102 let instr = FST (SND (SND model)) in 103 let less = FST (SND (SND (SND model))) in 104 (!s r. SEP_REFINE (pre * CODE_POOL instr code * r) less to_set s ==> 105 ~SEP_REFINE (post * CODE_POOL instr code * r) less to_set s) ==> 106 SPEC_1 model pre code post err``, 107 INIT \\ FULL_SIMP_TAC std_ss [] 108 \\ FULL_SIMP_TAC std_ss [SPEC_EQ_TEMPORAL,SPEC_1_def] 109 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,T_IMPLIES_def] 110 \\ REVERSE (REPEAT STRIP_TAC \\ RES_TAC 111 \\ FULL_SIMP_TAC std_ss [EVENTUALLY_def,NOW_def,T_OR_F_def,NEXT_def]) 112 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 113 \\ FULL_SIMP_TAC std_ss [SEP_REFINE_def,SEP_F_def] 114 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC] 115 THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] 116 \\ Cases_on `k` \\ FULL_SIMP_TAC std_ss [ADD1,SEP_DISJ_def] 117 \\ METIS_TAC []); 118 119val SEP_IMP_IMP_SEP_REFINE = prove( 120 ``SEP_IMP q1 q3 ==> 121 (!r1 r2 t2. 122 SEP_REFINE (q1 * r1 * r2) m f t2 ==> 123 SEP_REFINE (q3 * r1 * r2) m f t2)``, 124 FULL_SIMP_TAC std_ss [SEP_REFINE_def,GSYM STAR_ASSOC] 125 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC SEP_IMP_FRAME 126 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def] \\ METIS_TAC []); 127 128val SPEC_1_STRENGTHEN = store_thm("SPEC_1_STRENGTHEN", 129 ``!model p c q err. 130 SPEC_1 model p c q err ==> !r. SEP_IMP r p ==> 131 SPEC_1 model r c q err``, 132 STRIP_TAC \\ INIT \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 133 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,PULL_FORALL, 134 AND_IMP_INTRO,T_IMPLIES_def,ALWAYS_def,EVENTUALLY_def, 135 NOW_def,T_OR_F_def,SPEC_1_def] 136 \\ METIS_TAC [SEP_IMP_IMP_SEP_REFINE]); 137 138val SPEC_1_WEAKEN = store_thm("SPEC_1_WEAKEN", 139 ``!model p c r err. 140 SPEC_1 model p c r err ==> !q. SEP_IMP r q ==> 141 SPEC_1 model p c q err``, 142 STRIP_TAC \\ INIT \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 143 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,PULL_FORALL, 144 AND_IMP_INTRO,T_IMPLIES_def,ALWAYS_def,EVENTUALLY_def, 145 NOW_def,T_OR_F_def,SPEC_1_def,SEP_DISJ_def,SEP_CLAUSES,NEXT_def] 146 \\ METIS_TAC [SEP_IMP_IMP_SEP_REFINE]); 147 148val SPEC_1_FRAME = store_thm("SPEC_1_FRAME", 149 ``!model p c q err. SPEC_1 model p c q err ==> 150 !r. SPEC_1 model (p * r) c (q * r) (err * r)``, 151 STRIP_TAC \\ INIT \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 152 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,PULL_FORALL, 153 AND_IMP_INTRO,T_IMPLIES_def,ALWAYS_def,EVENTUALLY_def, 154 NOW_def,T_OR_F_def,SPEC_1_def,SEP_DISJ_def,SEP_CLAUSES,NEXT_def] 155 \\ NTAC 3 STRIP_TAC 156 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`state`,`seq`,`r * r'`]) 157 \\ FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]); 158 159val SPEC_MOVE_1_COND = store_thm("SPEC_MOVE_1_COND", 160 ``!model p c q g err. 161 SPEC_1 model (p * cond g) c q err <=> (g ==> SPEC_1 model p c q err)``, 162 STRIP_TAC \\ INIT \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 163 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,PULL_FORALL, 164 AND_IMP_INTRO,T_IMPLIES_def,ALWAYS_def,EVENTUALLY_def, 165 NOW_def,T_OR_F_def,SPEC_1_def,SEP_DISJ_def,SEP_CLAUSES,NEXT_def] 166 \\ FULL_SIMP_TAC std_ss [SEP_REFINE_def] 167 \\ Cases_on `g` \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 168 \\ FULL_SIMP_TAC std_ss [SEP_F_def] \\ METIS_TAC []); 169 170val SPEC_1_PRE_EXISTS = store_thm("SPEC_1_PRE_EXISTS", 171 ``!model p c q err. (!y. SPEC_1 model (p y) c q err) <=> 172 SPEC_1 model (SEP_EXISTS y. p y) c q err``, 173 STRIP_TAC \\ INIT \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 174 \\ FULL_SIMP_TAC std_ss [TEMPORAL_def,LET_DEF,PULL_FORALL, 175 AND_IMP_INTRO,T_IMPLIES_def,ALWAYS_def,EVENTUALLY_def, 176 NOW_def,T_OR_F_def,SPEC_1_def,SEP_DISJ_def,SEP_CLAUSES,NEXT_def] 177 \\ FULL_SIMP_TAC std_ss [SEP_REFINE_def,SEP_CLAUSES,SEP_EXISTS_THM] 178 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 179 \\ FIRST_X_ASSUM MATCH_MP_TAC \\ METIS_TAC []) 180 181val _ = export_theory() 182