author | paulson |
Thu, 06 Aug 1998 15:47:26 +0200 | |
changeset 5277 | e4297d03e5d2 |
child 5320 | 79b326bceafb |
permissions | -rw-r--r-- |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Lift.thy |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
5 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
6 |
The Lift-Control Example |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
7 |
*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
8 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
9 |
Lift = SubstAx + |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
10 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
11 |
record state = |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
12 |
floor :: nat (*current position of the lift*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
13 |
open :: bool (*whether the door is open at floor*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
14 |
stop :: bool (*whether the lift is stopped at floor*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
15 |
req :: nat set (*for each floor, whether the lift is requested*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
16 |
up :: bool (*current direction of movement*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
17 |
move :: bool (*whether moving takes precedence over opening*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
18 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
19 |
consts |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
20 |
min, max :: nat (*least and greatest floors*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
21 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
22 |
rules |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
23 |
min_le_max "min <= max" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
24 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
25 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
26 |
constdefs |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
27 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
28 |
(** Abbreviations: the "always" part **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
29 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
30 |
above :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
31 |
"above == {s. EX i. floor s < i & i <= max & i : req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
32 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
33 |
below :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
34 |
"below == {s. EX i. min <= i & i < floor s & i : req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
35 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
36 |
queueing :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
37 |
"queueing == above Un below" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
38 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
39 |
goingup :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
40 |
"goingup == above Int ({s. up s} Un Compl below)" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
41 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
42 |
goingdown :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
43 |
"goingdown == below Int ({s. ~ up s} Un Compl above)" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
44 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
45 |
ready :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
46 |
"ready == {s. stop s & ~ open s & move s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
47 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
48 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
49 |
(** The program **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
50 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
51 |
request_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
52 |
"request_act == {(s,s'). s' = s (|stop:=True, move:=False|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
53 |
& ~ stop s & floor s : req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
54 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
55 |
open_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
56 |
"open_act == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
57 |
{(s,s'). s' = s (|open :=True, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
58 |
req := req s - {floor s}, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
59 |
move := True|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
60 |
& stop s & ~ open s & floor s : req s |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
61 |
& ~(move s & s: queueing)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
62 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
63 |
close_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
64 |
"close_act == {(s,s'). s' = s (|open := False|) & open s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
65 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
66 |
req_up_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
67 |
"req_up_act == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
68 |
{(s,s'). s' = s (|stop :=False, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
69 |
floor := Suc (floor s), |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
70 |
up := True|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
71 |
& s : (ready Int goingup)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
72 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
73 |
req_down_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
74 |
"req_down_act == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
75 |
{(s,s'). s' = s (|stop :=False, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
76 |
floor := floor s - 1, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
77 |
up := False|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
78 |
& s : (ready Int goingdown)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
79 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
80 |
move_up :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
81 |
"move_up == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
82 |
{(s,s'). s' = s (|floor := Suc (floor s)|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
83 |
& ~ stop s & up s & floor s ~: req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
84 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
85 |
move_down :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
86 |
"move_down == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
87 |
{(s,s'). s' = s (|floor := floor s - 1|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
88 |
& ~ stop s & ~ up s & floor s ~: req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
89 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
90 |
Lprg :: state program |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
91 |
"Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s & |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
92 |
~ open s & req s = {}}, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
93 |
Acts = {id, request_act, open_act, close_act, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
94 |
req_up_act, req_down_act, move_up, move_down}|)" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
95 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
96 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
97 |
(** Invariants **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
98 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
99 |
bounded :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
100 |
"bounded == {s. min <= floor s & floor s <= max}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
101 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
102 |
(** ??? |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
103 |
(~ stop s & up s --> floor s < max) & |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
104 |
(~ stop s & ~ up s --> min < floor s)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
105 |
**) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
106 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
107 |
open_stop :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
108 |
"open_stop == {s. open s --> stop s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
109 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
110 |
open_move :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
111 |
"open_move == {s. open s --> move s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
112 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
113 |
stop_floor :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
114 |
"stop_floor == {s. open s & ~ move s --> floor s : req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
115 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
116 |
moving_up :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
117 |
"moving_up == {s. ~ stop s & up s --> |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
118 |
(EX f. floor s <= f & f <= max & f : req s)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
119 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
120 |
moving_down :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
121 |
"moving_down == {s. ~ stop s & ~ up s --> |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
122 |
(EX f. min <= f & f <= floor s & f : req s)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
123 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
124 |
valid :: "state set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
125 |
"valid == bounded Int open_stop Int open_move" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
126 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
127 |
end |