1(*===========================================================================*)
2(* Autopilot Specification Example                                           *)
3(*                                                                           *)
4(* The Hol98 part of an intended comparison between PVS, ACL2 and HOL98.     *)
5(* Copyright 1998, Mark Staples                                              *)
6(* Modifications (April,June 1998) Konrad Slind.                             *)
7(*===========================================================================*)
8
9open HolKernel boolLib Parse bossLib
10
11(*---------------------------------------------------------------------------*
12 * We'll track information on inferences.                                    *
13 *---------------------------------------------------------------------------*)
14
15val meter = Count.mk_meter();
16
17
18(*---------------------------------------------------------------------------*
19 * Start the theory.                                                         *
20 *---------------------------------------------------------------------------*)
21
22val _ = new_theory "autopilot";
23
24
25val _ = Hol_datatype `events = press_att_cws
26                     | press_cas_eng
27                     | press_alt_eng
28                     | press_fpa_sel
29                     | input_alt
30                     | input_fpa
31                     | input_cas
32                     | alt_reached
33                     | fpa_reached
34                     | alt_gets_near`;
35
36
37val _ = Hol_datatype `off_eng = off | engaged`;
38
39
40val _ = Hol_datatype `mode_status
41                     = armed
42                     | Mode of off_eng`;
43
44
45val _ = Hol_datatype `disp_status
46                     = pre_selected
47                     | current`;
48
49
50val _ = Hol_datatype `altitude_vals
51                     = away
52                     | near_pre_selected
53                     | at_pre_selected`;
54
55
56(*---------------------------------------------------------------------------*
57 * Define state-type projection and update functions.                        *
58 *---------------------------------------------------------------------------*)
59
60val _ = Hol_datatype `states = <| att_cws  : off_eng;
61                                  cas_eng  : off_eng;
62                                  fpa_sel  : off_eng;
63                                  alt_eng  : mode_status;
64                                  alt_disp : disp_status;
65                                  fpa_disp : disp_status;
66                                  cas_disp : disp_status;
67                                  altitude : altitude_vals |>`;
68
69
70(*---------------------------------------------------------------------------*
71 * State predicates.                                                         *
72 *---------------------------------------------------------------------------*)
73
74val tran_att_cws_def =
75 Define
76     `tran_att_cws st =
77         if st.att_cws = off
78         then st with
79                 <| att_cws := engaged;
80                    fpa_sel := off;
81                    alt_eng := Mode off;
82                   fpa_disp := current;
83                   alt_disp := current|>
84         else st`;
85
86
87val tran_cas_eng_def =
88 Define
89    `tran_cas_eng st =
90        if st.cas_eng = off
91          then st with cas_eng := engaged
92          else (st with <|cas_disp := current; cas_eng := off|>)`;
93
94
95val tran_fpa_sel_def =
96 Define
97    `tran_fpa_sel st =
98       if st.fpa_sel = off
99       then st with
100               <| fpa_sel := engaged;
101                  att_cws := off;
102                  alt_eng := Mode off;
103                 alt_disp := current|>
104       else (st with
105                <| fpa_sel := off;
106                  fpa_disp := current;
107                   att_cws := engaged;
108                   alt_eng := Mode off;
109                  alt_disp := current|>)`;
110
111val tran_alt_eng_def =
112 Define
113     `tran_alt_eng st =
114         if (st.alt_eng = Mode off) /\
115            (st.alt_disp = pre_selected)
116         then (if ~(st.altitude = away)
117               then st with
118                       <| att_cws := off;
119                          fpa_sel := off;
120                          alt_eng := Mode engaged;
121                         fpa_disp := current|>
122               else (st with
123                        <|att_cws := off;
124                          fpa_sel := engaged;
125                          alt_eng := armed|>))
126         else st`;
127
128val tran_input_alt_def =
129 Define
130     `tran_input_alt st =
131         if st.alt_eng = Mode off
132         then st with alt_disp := pre_selected
133         else if (st.alt_eng = armed) \/ (st.alt_eng = Mode engaged)
134              then st with
135                    <|alt_eng  := Mode off;
136                      alt_disp := pre_selected;
137                      att_cws  := engaged;
138                      fpa_sel  := off;
139                      fpa_disp := current|>
140              else st`;
141
142val tran_input_fpa_def =
143 Define
144     `tran_input_fpa st =
145         if st.fpa_sel = off
146         then st with fpa_disp := pre_selected
147         else st`;
148
149
150val tran_input_cas_def =
151 Define
152     `tran_input_cas st =
153         if st.cas_eng = off then st with cas_disp := pre_selected else st`;
154
155
156val tran_alt_gets_near_def =
157 Define
158     `tran_alt_gets_near st =
159         if st.alt_eng = armed
160         then st with
161                <|altitude := near_pre_selected;
162                  alt_eng  := Mode engaged;
163                  fpa_sel  := off;
164                  fpa_disp := current|>
165         else
166           (st with altitude := near_pre_selected)`;
167
168val tran_alt_reached_def =
169 Define
170     `tran_alt_reached st =
171        if st.alt_eng = armed
172        then st with
173              <|altitude := at_pre_selected;
174                alt_disp := current;
175                alt_eng  := Mode engaged;
176                fpa_sel  := off;
177                fpa_disp := current|>
178        else (st with <|altitude := at_pre_selected; alt_disp := current|>)`;
179
180val tran_fpa_reached_def =
181 Define
182     `tran_fpa_reached st = (st with fpa_disp := current)`;
183
184
185val tran_defs =
186  [ tran_att_cws_def, tran_alt_eng_def, tran_fpa_sel_def, tran_cas_eng_def,
187    tran_input_alt_def, tran_input_fpa_def, tran_input_cas_def,
188    tran_alt_reached_def, tran_fpa_reached_def, tran_alt_gets_near_def];
189
190
191(*---------------------------------------------------------------------------*
192 * The transition function.                                                  *
193 *---------------------------------------------------------------------------*)
194
195val nextstate_def =
196  Define
197     `(nextstate st press_att_cws  =  tran_att_cws st)
198  /\  (nextstate st press_alt_eng  =  tran_alt_eng st)
199  /\  (nextstate st press_fpa_sel  =  tran_fpa_sel st)
200  /\  (nextstate st press_cas_eng  =  tran_cas_eng st)
201  /\  (nextstate st input_alt      =  tran_input_alt st)
202  /\  (nextstate st input_fpa      =  tran_input_fpa st)
203  /\  (nextstate st input_cas      =  tran_input_cas st)
204  /\  (nextstate st alt_reached    =  tran_alt_reached st)
205  /\  (nextstate st fpa_reached    =  tran_fpa_reached st)
206  /\  (nextstate st alt_gets_near  =  tran_alt_gets_near st)`;
207
208
209(*---------------------------------------------------------------------------*
210 * Initial state.                                                            *
211 *---------------------------------------------------------------------------*)
212
213val st0_def =
214 Define
215    `st0 = <|att_cws  := engaged;
216             cas_eng  := off;
217             fpa_sel  := off;
218             alt_eng  := Mode off;
219             alt_disp := current;
220             fpa_disp := current;
221             cas_disp := current;
222             altitude := away|>`;
223
224
225val is_initial_def =
226 Define
227     `is_initial st =
228         (st.att_cws = engaged)  /\
229         (st.cas_eng = off)      /\
230         (st.fpa_sel = off)      /\
231         (st.alt_eng = Mode off) /\
232         (st.alt_disp = current) /\
233         (st.fpa_disp = current) /\
234         (st.cas_disp = current)`;
235
236
237val valid_state_def =
238 Define
239     `valid_state st =
240         ((st.att_cws = engaged) \/ (st.fpa_sel = engaged) \/
241          (st.alt_eng = Mode engaged))
242     /\  (~(st.alt_eng = Mode engaged) \/ ~(st.fpa_sel = engaged))
243     /\  ((st.att_cws = engaged)
244           ==> ~(st.alt_eng = Mode engaged) /\
245               ~(st.fpa_sel = engaged))
246     /\  ((st.alt_eng = armed) ==> (st.fpa_sel = engaged))`;
247
248
249(*---------------------------------------------------------------------------*
250 * Proofs. First we build the simplification set. Note that standard         *
251 * simplifications arising from datatype definitions get applied             *
252 * automatically, and thus can be considered to be in every simplification   *
253 * set.                                                                      *
254 *---------------------------------------------------------------------------*)
255
256val ap_ss = std_ss && [nextstate_def, valid_state_def];
257
258val st0_initial = prove (Term`is_initial st0`,
259 ZAP_TAC
260    (ap_ss && [is_initial_def,st0_def]) []);
261
262
263val is_initial_valid_state = prove(Term`is_initial st ==> valid_state st`,
264  ZAP_TAC
265    (ap_ss && [is_initial_def]) []);
266
267
268val st0_valid_state = prove (Term`valid_state st0`,
269  ZAP_TAC
270    (ap_ss && [is_initial_valid_state,st0_initial]) []);
271
272
273(*---------------------------------------------------------------------------*
274 * nextstate preserves valid_stateness.                                      *
275 * It takes approx. 17 seconds of runtime on 80Meg Pentium 133Mhz.           *
276 *---------------------------------------------------------------------------*)
277
278val nextstate_valid_state =
279Count.apply prove
280  (Term`!event. valid_state st ==> valid_state (nextstate st event)`,
281   Cases
282     THEN ZAP_TAC (ap_ss && tran_defs) []);
283
284
285(*---------------------------------------------------------------------------*
286 * Reachability. This could also be given as an inductive definition.        *
287 *---------------------------------------------------------------------------*)
288
289val reachable_in_def =
290 Define
291    `(reachable_in 0 st = is_initial st) /\
292     (reachable_in (SUC n) st =
293        ?pst ev. (st = nextstate pst ev) /\ reachable_in n pst)`;
294
295
296
297(*---------------------------------------------------------------------------*
298 * Every reachable state is valid.                                           *
299 *---------------------------------------------------------------------------*)
300
301val reachable_valid_state = prove
302 (Term`!n st. reachable_in n st ==> valid_state st`,
303  Induct THEN
304   ZAP_TAC (std_ss && [reachable_in_def])
305           [is_initial_valid_state,nextstate_valid_state]);
306
307
308(*---------------------------------------------------------------------------*
309 * A state is reachable if it is reachable in a finite number of steps.      *
310 *---------------------------------------------------------------------------*)
311
312val is_reachable_def = Define  `is_reachable st = ?n. reachable_in n st`;
313
314
315val is_reachable_valid_state = prove
316(Term`!st. is_reachable st ==> valid_state st`,
317  ZAP_TAC std_ss
318    [is_reachable_def,reachable_valid_state]);
319
320
321(*---------------------------------------------------------------------------*
322 * A couple of safety properties.                                            *
323 *---------------------------------------------------------------------------*)
324
325val safety1 = store_thm(
326  "safety1",
327  ``!event st.
328       valid_state st
329    /\ (st.fpa_sel = engaged)
330    /\ ((nextstate st event).fpa_sel = off)
331      ==>
332       ((nextstate st event).fpa_disp = current)``,
333Induct
334  THEN ZAP_TAC (ap_ss && tran_defs)  (tl (type_rws ``:off_eng``)));
335
336
337val safety2 = store_thm(
338  "safety2",
339  ``!event st.
340             valid_state st
341          /\ (st.alt_eng = Mode engaged)
342          /\ ~(event = input_alt)
343          /\ ((nextstate st event).alt_eng = Mode off)
344            ==>
345             ((nextstate st event).alt_disp = current)``,
346Induct
347  THEN ZAP_TAC (ap_ss && tran_defs)
348             (tl(type_rws ``:off_eng``) @ tl(type_rws ``:mode_status``)));
349
350
351(*---------------------------------------------------------------------------*
352 * Induction for reachable states.                                           *
353 *---------------------------------------------------------------------------*)
354
355val reachable_induct = prove
356(Term`!P. (!st. is_initial st ==> P st) /\
357          (!st e. is_reachable st ==> P (nextstate st e))
358          ==>
359          !st. is_reachable st ==> P st`,
360 RW_TAC std_ss [is_reachable_def]
361  THEN Cases_on `n`
362  THEN PROVE_TAC [reachable_in_def]);
363
364
365val _ = Count.report (Count.read meter);
366
367val _ = export_theory()
368