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