author | paulson |
Sat, 23 Sep 2000 16:02:01 +0200 | |
changeset 10064 | 1a77667b21ef |
parent 6718 | e869ff059252 |
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 = |
5563 | 12 |
floor :: int (*current position of the lift*) |
5277
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*) |
5563 | 15 |
req :: int set (*for each floor, whether the lift is requested*) |
5277
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 |
5563 | 20 |
Min, Max :: int (*least and greatest floors*) |
5277
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 |
5357 | 23 |
Min_le_Max "Min <= Max" |
5277
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 |
constdefs |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
26 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
27 |
(** Abbreviations: the "always" part **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
28 |
|
5320 | 29 |
above :: state set |
5357 | 30 |
"above == {s. EX i. floor s < i & i <= Max & i : req s}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
31 |
|
5320 | 32 |
below :: state set |
5357 | 33 |
"below == {s. EX i. Min <= i & i < floor s & i : req s}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
34 |
|
5320 | 35 |
queueing :: state set |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
36 |
"queueing == above Un below" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
37 |
|
5320 | 38 |
goingup :: state set |
5931 | 39 |
"goingup == above Int ({s. up s} Un -below)" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
40 |
|
5320 | 41 |
goingdown :: state set |
5931 | 42 |
"goingdown == below Int ({s. ~ up s} Un -above)" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
43 |
|
5320 | 44 |
ready :: state set |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
45 |
"ready == {s. stop s & ~ open s & move s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
46 |
|
5320 | 47 |
|
48 |
(** Further abbreviations **) |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
49 |
|
5320 | 50 |
moving :: state set |
51 |
"moving == {s. ~ stop s & ~ open s}" |
|
52 |
||
53 |
stopped :: state set |
|
5340 | 54 |
"stopped == {s. stop s & ~ open s & ~ move s}" |
5320 | 55 |
|
56 |
opened :: state set |
|
57 |
"opened == {s. stop s & open s & move s}" |
|
58 |
||
5340 | 59 |
closed :: state set (*but this is the same as ready!!*) |
5320 | 60 |
"closed == {s. stop s & ~ open s & move s}" |
61 |
||
5563 | 62 |
atFloor :: int => state set |
5320 | 63 |
"atFloor n == {s. floor s = n}" |
64 |
||
5563 | 65 |
Req :: int => state set |
5340 | 66 |
"Req n == {s. n : req s}" |
67 |
||
5320 | 68 |
|
69 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
70 |
(** The program **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
71 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
72 |
request_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
73 |
"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
|
74 |
& ~ stop s & floor s : req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
75 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
76 |
open_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
77 |
"open_act == |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
78 |
{(s,s'). s' = s (|open :=True, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
79 |
req := req s - {floor s}, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
80 |
move := True|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
81 |
& stop s & ~ open s & floor s : req s |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
82 |
& ~(move s & s: queueing)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
83 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
84 |
close_act :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
85 |
"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
|
86 |
|
5357 | 87 |
req_up :: "(state*state) set" |
88 |
"req_up == |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
89 |
{(s,s'). s' = s (|stop :=False, |
5563 | 90 |
floor := floor s + #1, |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
91 |
up := True|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
92 |
& s : (ready Int goingup)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
93 |
|
5357 | 94 |
req_down :: "(state*state) set" |
95 |
"req_down == |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
96 |
{(s,s'). s' = s (|stop :=False, |
5563 | 97 |
floor := floor s - #1, |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
98 |
up := False|) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
99 |
& s : (ready Int goingdown)}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
100 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
101 |
move_up :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
102 |
"move_up == |
5563 | 103 |
{(s,s'). s' = s (|floor := floor s + #1|) |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
104 |
& ~ stop s & up s & floor s ~: req 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 |
move_down :: "(state*state) set" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
107 |
"move_down == |
5563 | 108 |
{(s,s'). s' = s (|floor := floor s - #1|) |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
109 |
& ~ stop s & ~ up s & floor s ~: req s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
110 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
111 |
(*This action is omitted from prior treatments, which therefore are |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
112 |
unrealistic: nobody asks the lift to do anything! But adding this |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
113 |
action invalidates many of the existing progress arguments: various |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
114 |
"ensures" properties fail.*) |
5357 | 115 |
button_press :: "(state*state) set" |
116 |
"button_press == |
|
117 |
{(s,s'). EX n. s' = s (|req := insert n (req s)|) |
|
118 |
& Min <= n & n <= Max}" |
|
119 |
||
120 |
||
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6295
diff
changeset
|
121 |
Lift :: state program |
5357 | 122 |
(*for the moment, we OMIT button_press*) |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6295
diff
changeset
|
123 |
"Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
124 |
~ open s & req s = {}}, |
5596 | 125 |
{request_act, open_act, close_act, |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
126 |
req_up, req_down, move_up, move_down}, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
6718
diff
changeset
|
127 |
UNIV)" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
128 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
129 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
130 |
(** Invariants **) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
131 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
132 |
bounded :: state set |
5357 | 133 |
"bounded == {s. Min <= floor s & floor s <= Max}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
134 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
135 |
open_stop :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
136 |
"open_stop == {s. open s --> stop s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
137 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
138 |
open_move :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
139 |
"open_move == {s. open s --> move s}" |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
140 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
141 |
stop_floor :: state set |
5340 | 142 |
"stop_floor == {s. stop s & ~ move s --> floor s : req s}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
143 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
144 |
moving_up :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
145 |
"moving_up == {s. ~ stop s & up s --> |
5357 | 146 |
(EX f. floor s <= f & f <= Max & f : req s)}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
147 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
148 |
moving_down :: state set |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
149 |
"moving_down == {s. ~ stop s & ~ up s --> |
5357 | 150 |
(EX f. Min <= f & f <= floor s & f : req s)}" |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
151 |
|
5563 | 152 |
metric :: [int,state] => int |
5357 | 153 |
"metric == |
5563 | 154 |
%n s. if floor s < n then (if up s then n - floor s |
155 |
else (floor s - Min) + (n-Min)) |
|
156 |
else |
|
157 |
if n < floor s then (if up s then (Max - floor s) + (Max-n) |
|
158 |
else floor s - n) |
|
159 |
else #0" |
|
5340 | 160 |
|
161 |
locale floor = |
|
162 |
fixes |
|
5563 | 163 |
n :: int |
5340 | 164 |
assumes |
5357 | 165 |
Min_le_n "Min <= n" |
166 |
n_le_Max "n <= Max" |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6015
diff
changeset
|
167 |
defines |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
168 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
169 |
end |