author | wenzelm |
Tue, 16 Jan 2018 09:30:00 +0100 | |
changeset 67443 | 3abf6a722518 |
parent 63146 | f1ecba0272f9 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Lift.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
5 |
The Lift-Control Example. |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
8 |
theory Lift |
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
9 |
imports "../UNITY_Main" |
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
10 |
begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
record state = |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
13 |
floor :: "int" \<comment> \<open>current position of the lift\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
14 |
"open" :: "bool" \<comment> \<open>whether the door is opened at floor\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
15 |
stop :: "bool" \<comment> \<open>whether the lift is stopped at floor\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
16 |
req :: "int set" \<comment> \<open>for each floor, whether the lift is requested\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
17 |
up :: "bool" \<comment> \<open>current direction of movement\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
18 |
move :: "bool" \<comment> \<open>whether moving takes precedence over opening\<close> |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
36866 | 20 |
axiomatization |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
21 |
Min :: "int" and \<comment> \<open>least and greatest floors\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
22 |
Max :: "int" \<comment> \<open>least and greatest floors\<close> |
36866 | 23 |
where |
13806 | 24 |
Min_le_Max [iff]: "Min \<le> Max" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
27 |
\<comment> \<open>Abbreviations: the "always" part\<close> |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
|
36866 | 29 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
30 |
above :: "state set" |
36866 | 31 |
where "above = {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
36866 | 33 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
34 |
below :: "state set" |
36866 | 35 |
where "below = {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
|
36866 | 37 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
38 |
queueing :: "state set" |
36866 | 39 |
where "queueing = above \<union> below" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
|
36866 | 41 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
42 |
goingup :: "state set" |
36866 | 43 |
where "goingup = above \<inter> ({s. up s} \<union> -below)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
|
36866 | 45 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
46 |
goingdown :: "state set" |
36866 | 47 |
where "goingdown = below \<inter> ({s. ~ up s} \<union> -above)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
|
36866 | 49 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
50 |
ready :: "state set" |
36866 | 51 |
where "ready = {s. stop s & ~ open s & move s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
53 |
\<comment> \<open>Further abbreviations\<close> |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
54 |
|
36866 | 55 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
56 |
moving :: "state set" |
36866 | 57 |
where "moving = {s. ~ stop s & ~ open s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
|
36866 | 59 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
60 |
stopped :: "state set" |
36866 | 61 |
where "stopped = {s. stop s & ~ open s & ~ move s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
|
36866 | 63 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
64 |
opened :: "state set" |
36866 | 65 |
where "opened = {s. stop s & open s & move s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
|
36866 | 67 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
68 |
closed :: "state set" \<comment> \<open>but this is the same as ready!!\<close> |
36866 | 69 |
where "closed = {s. stop s & ~ open s & move s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
|
36866 | 71 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
72 |
atFloor :: "int => state set" |
36866 | 73 |
where "atFloor n = {s. floor s = n}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
74 |
|
36866 | 75 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
76 |
Req :: "int => state set" |
36866 | 77 |
where "Req n = {s. n \<in> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
78 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
79 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
80 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
81 |
\<comment> \<open>The program\<close> |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
82 |
|
36866 | 83 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
84 |
request_act :: "(state*state) set" |
36866 | 85 |
where "request_act = {(s,s'). s' = s (|stop:=True, move:=False|) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
86 |
& ~ stop s & floor s \<in> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
87 |
|
36866 | 88 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
89 |
open_act :: "(state*state) set" |
36866 | 90 |
where "open_act = |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
91 |
{(s,s'). s' = s (|open :=True, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
92 |
req := req s - {floor s}, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
93 |
move := True|) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
94 |
& stop s & ~ open s & floor s \<in> req s |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
95 |
& ~(move s & s \<in> queueing)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
96 |
|
36866 | 97 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
98 |
close_act :: "(state*state) set" |
36866 | 99 |
where "close_act = {(s,s'). s' = s (|open := False|) & open s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
100 |
|
36866 | 101 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
102 |
req_up :: "(state*state) set" |
36866 | 103 |
where "req_up = |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
104 |
{(s,s'). s' = s (|stop :=False, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
105 |
floor := floor s + 1, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
106 |
up := True|) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
107 |
& s \<in> (ready \<inter> goingup)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
108 |
|
36866 | 109 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
110 |
req_down :: "(state*state) set" |
36866 | 111 |
where "req_down = |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
112 |
{(s,s'). s' = s (|stop :=False, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
113 |
floor := floor s - 1, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
114 |
up := False|) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
115 |
& s \<in> (ready \<inter> goingdown)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
116 |
|
36866 | 117 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
118 |
move_up :: "(state*state) set" |
36866 | 119 |
where "move_up = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
120 |
{(s,s'). s' = s (|floor := floor s + 1|) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
121 |
& ~ stop s & up s & floor s \<notin> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
122 |
|
36866 | 123 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
124 |
move_down :: "(state*state) set" |
36866 | 125 |
where "move_down = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
126 |
{(s,s'). s' = s (|floor := floor s - 1|) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
127 |
& ~ stop s & ~ up s & floor s \<notin> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
128 |
|
36866 | 129 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
130 |
button_press :: "(state*state) set" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
131 |
\<comment> \<open>This action is omitted from prior treatments, which therefore are |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
132 |
unrealistic: nobody asks the lift to do anything! But adding this |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
133 |
action invalidates many of the existing progress arguments: various |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
134 |
"ensures" properties fail. Maybe it should be constrained to only |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
135 |
allow button presses in the current direction of travel, like in a |
63146 | 136 |
real lift.\<close> |
36866 | 137 |
where "button_press = |
13806 | 138 |
{(s,s'). \<exists>n. s' = s (|req := insert n (req s)|) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
139 |
& Min \<le> n & n \<le> Max}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
140 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
141 |
|
36866 | 142 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
143 |
Lift :: "state program" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
144 |
\<comment> \<open>for the moment, we OMIT \<open>button_press\<close>\<close> |
36866 | 145 |
where "Lift = mk_total_program |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
146 |
({s. floor s = Min & ~ up s & move s & stop s & |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
147 |
~ open s & req s = {}}, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
148 |
{request_act, open_act, close_act, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
149 |
req_up, req_down, move_up, move_down}, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
150 |
UNIV)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
151 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
152 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63146
diff
changeset
|
153 |
\<comment> \<open>Invariants\<close> |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
154 |
|
36866 | 155 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
156 |
bounded :: "state set" |
36866 | 157 |
where "bounded = {s. Min \<le> floor s & floor s \<le> Max}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
158 |
|
36866 | 159 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
160 |
open_stop :: "state set" |
36866 | 161 |
where "open_stop = {s. open s --> stop s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
162 |
|
36866 | 163 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
164 |
open_move :: "state set" |
36866 | 165 |
where "open_move = {s. open s --> move s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
166 |
|
36866 | 167 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
168 |
stop_floor :: "state set" |
36866 | 169 |
where "stop_floor = {s. stop s & ~ move s --> floor s \<in> req s}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
170 |
|
36866 | 171 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
172 |
moving_up :: "state set" |
36866 | 173 |
where "moving_up = {s. ~ stop s & up s --> |
13806 | 174 |
(\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
175 |
|
36866 | 176 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
177 |
moving_down :: "state set" |
36866 | 178 |
where "moving_down = {s. ~ stop s & ~ up s --> |
13806 | 179 |
(\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
180 |
|
36866 | 181 |
definition |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
182 |
metric :: "[int,state] => int" |
36866 | 183 |
where "metric = |
184 |
(%n s. if floor s < n then (if up s then n - floor s |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
185 |
else (floor s - Min) + (n-Min)) |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
186 |
else |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
187 |
if n < floor s then (if up s then (Max - floor s) + (Max-n) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16184
diff
changeset
|
188 |
else floor s - n) |
36866 | 189 |
else 0)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
190 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
191 |
locale Floor = |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
192 |
fixes n |
13806 | 193 |
assumes Min_le_n [iff]: "Min \<le> n" |
194 |
and n_le_Max [iff]: "n \<le> Max" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
195 |
|
13806 | 196 |
lemma not_mem_distinct: "[| x \<notin> A; y \<in> A |] ==> x \<noteq> y" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
197 |
by blast |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
198 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
199 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
200 |
declare Lift_def [THEN def_prg_Init, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
201 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
202 |
declare request_act_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
203 |
declare open_act_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
204 |
declare close_act_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
205 |
declare req_up_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
206 |
declare req_down_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
207 |
declare move_up_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
208 |
declare move_down_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
209 |
declare button_press_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
210 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
211 |
(*The ALWAYS properties*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
212 |
declare above_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
213 |
declare below_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
214 |
declare queueing_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
215 |
declare goingup_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
216 |
declare goingdown_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
217 |
declare ready_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
218 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
219 |
(*Basic definitions*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
220 |
declare bounded_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
221 |
open_stop_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
222 |
open_move_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
223 |
stop_floor_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
224 |
moving_up_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
225 |
moving_down_def [simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
226 |
|
13806 | 227 |
lemma open_stop: "Lift \<in> Always open_stop" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
228 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
229 |
apply (unfold Lift_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
230 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
231 |
|
13806 | 232 |
lemma stop_floor: "Lift \<in> Always stop_floor" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
233 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
234 |
apply (unfold Lift_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
235 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
236 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
237 |
(*This one needs open_stop, which was proved above*) |
13806 | 238 |
lemma open_move: "Lift \<in> Always open_move" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
239 |
apply (cut_tac open_stop) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
240 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
241 |
apply (unfold Lift_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
242 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
243 |
|
13806 | 244 |
lemma moving_up: "Lift \<in> Always moving_up" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
245 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
246 |
apply (unfold Lift_def, safety) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
13812
diff
changeset
|
247 |
apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
248 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
249 |
|
13806 | 250 |
lemma moving_down: "Lift \<in> Always moving_down" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
251 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
252 |
apply (unfold Lift_def, safety) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
13812
diff
changeset
|
253 |
apply (blast dest: order_le_imp_less_or_eq) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
254 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
255 |
|
13806 | 256 |
lemma bounded: "Lift \<in> Always bounded" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
257 |
apply (cut_tac moving_up moving_down) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
258 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14378
diff
changeset
|
259 |
apply (unfold Lift_def, safety, auto) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
260 |
apply (drule not_mem_distinct, assumption, arith)+ |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
261 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
262 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
263 |
|
63146 | 264 |
subsection\<open>Progress\<close> |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
265 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
266 |
declare moving_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
267 |
declare stopped_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
268 |
declare opened_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
269 |
declare closed_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
270 |
declare atFloor_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
271 |
declare Req_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
272 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
273 |
|
63146 | 274 |
text\<open>The HUG'93 paper mistakenly omits the Req n from these!\<close> |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
275 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
276 |
(** Lift_1 **) |
13806 | 277 |
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
278 |
apply (cut_tac stop_floor) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
279 |
apply (unfold Lift_def, ensures_tac "open_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
280 |
done (*lem_lift_1_5*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
281 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
282 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
283 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
284 |
|
13806 | 285 |
lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
286 |
(Req n \<inter> opened - atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
287 |
apply (cut_tac stop_floor) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
288 |
apply (unfold Lift_def, ensures_tac "open_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
289 |
done (*lem_lift_1_1*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
290 |
|
13806 | 291 |
lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
292 |
(Req n \<inter> closed - (atFloor n - queueing))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
293 |
apply (unfold Lift_def, ensures_tac "close_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
294 |
done (*lem_lift_1_2*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
295 |
|
13806 | 296 |
lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing)) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
297 |
LeadsTo (opened \<inter> atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
298 |
apply (unfold Lift_def, ensures_tac "open_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
299 |
done (*lem_lift_1_7*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
300 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
301 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
302 |
(** Lift 2. Statements of thm05a and thm05b were wrong! **) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
303 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
304 |
lemmas linorder_leI = linorder_not_less [THEN iffD1] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
305 |
|
46912 | 306 |
context Floor |
307 |
begin |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
308 |
|
46912 | 309 |
lemmas le_MinD = Min_le_n [THEN order_antisym] |
310 |
and Max_leD = n_le_Max [THEN [2] order_antisym] |
|
311 |
||
312 |
declare le_MinD [dest!] |
|
313 |
and linorder_leI [THEN le_MinD, dest!] |
|
314 |
and Max_leD [dest!] |
|
315 |
and linorder_leI [THEN Max_leD, dest!] |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
316 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
317 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
318 |
(*lem_lift_2_0 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
319 |
NOT an ensures_tac property, but a mere inclusion |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
320 |
don't know why script lift_2.uni says ENSURES*) |
46912 | 321 |
lemma E_thm05c: |
13806 | 322 |
"Lift \<in> (Req n \<inter> closed - (atFloor n - queueing)) |
323 |
LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union> |
|
324 |
(closed \<inter> goingdown \<inter> Req n))" |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
13812
diff
changeset
|
325 |
by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
326 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
327 |
(*lift_2*) |
46912 | 328 |
lemma lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing)) |
13806 | 329 |
LeadsTo (moving \<inter> Req n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
330 |
apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
331 |
apply (unfold Lift_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
332 |
apply (ensures_tac [2] "req_down") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
333 |
apply (ensures_tac "req_up", auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
334 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
335 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
336 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
337 |
(** Towards lift_4 ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
338 |
|
62390 | 339 |
declare if_split_asm [split] |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
340 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
341 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
342 |
(*lem_lift_4_1 *) |
46912 | 343 |
lemma E_thm12a: |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
344 |
"0 < N ==> |
13806 | 345 |
Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> |
346 |
{s. floor s \<notin> req s} \<inter> {s. up s}) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
347 |
LeadsTo |
13806 | 348 |
(moving \<inter> Req n \<inter> {s. metric n s < N})" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
349 |
apply (cut_tac moving_up) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
350 |
apply (unfold Lift_def, ensures_tac "move_up", safe) |
13806 | 351 |
(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
352 |
apply (erule linorder_leI [THEN order_antisym, symmetric]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
353 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
354 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
355 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
356 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
357 |
(*lem_lift_4_3 *) |
46912 | 358 |
lemma E_thm12b: "0 < N ==> |
13806 | 359 |
Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> |
360 |
{s. floor s \<notin> req s} - {s. up s}) |
|
361 |
LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
362 |
apply (cut_tac moving_down) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
363 |
apply (unfold Lift_def, ensures_tac "move_down", safe) |
13806 | 364 |
(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
365 |
apply (erule linorder_leI [THEN order_antisym, symmetric]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
366 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
367 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
368 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
369 |
(*lift_4*) |
46912 | 370 |
lemma lift_4: |
13806 | 371 |
"0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> |
372 |
{s. floor s \<notin> req s}) LeadsTo |
|
373 |
(moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
374 |
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
375 |
LeadsTo_Un [OF E_thm12a E_thm12b]], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
376 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
377 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
378 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
379 |
(** towards lift_5 **) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
380 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
381 |
(*lem_lift_5_3*) |
46912 | 382 |
lemma E_thm16a: "0<N |
13806 | 383 |
==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo |
384 |
(moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
385 |
apply (cut_tac bounded) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
386 |
apply (unfold Lift_def, ensures_tac "req_up") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
387 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
388 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
389 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
390 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
391 |
(*lem_lift_5_1 has ~goingup instead of goingdown*) |
46912 | 392 |
lemma E_thm16b: "0<N ==> |
13806 | 393 |
Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo |
394 |
(moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
395 |
apply (cut_tac bounded) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
396 |
apply (unfold Lift_def, ensures_tac "req_down") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
397 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
398 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
399 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
400 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
401 |
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
402 |
i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
46912 | 403 |
lemma E_thm16c: |
13806 | 404 |
"0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
405 |
by (force simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
406 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
407 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
408 |
(*lift_5*) |
46912 | 409 |
lemma lift_5: |
13806 | 410 |
"0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo |
411 |
(moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
412 |
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
413 |
LeadsTo_Un [OF E_thm16a E_thm16b]]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
414 |
apply (drule E_thm16c, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
415 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
416 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
417 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
418 |
(** towards lift_3 **) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
419 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
420 |
(*lemma used to prove lem_lift_3_1*) |
46912 | 421 |
lemma metric_eq_0D [dest]: |
13806 | 422 |
"[| metric n s = 0; Min \<le> floor s; floor s \<le> Max |] ==> floor s = n" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
423 |
by (force simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
424 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
425 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
426 |
(*lem_lift_3_1*) |
46912 | 427 |
lemma E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo |
13806 | 428 |
(stopped \<inter> atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
429 |
apply (cut_tac bounded) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
430 |
apply (unfold Lift_def, ensures_tac "request_act", auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
431 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
432 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
433 |
(*lem_lift_3_5*) |
46912 | 434 |
lemma E_thm13: |
13806 | 435 |
"Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) |
436 |
LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
437 |
apply (unfold Lift_def, ensures_tac "request_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
438 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
439 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
440 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
441 |
(*lem_lift_3_6*) |
46912 | 442 |
lemma E_thm14: "0 < N ==> |
13806 | 443 |
Lift \<in> |
444 |
(stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) |
|
445 |
LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
446 |
apply (unfold Lift_def, ensures_tac "open_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
447 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
448 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
449 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
450 |
(*lem_lift_3_7*) |
46912 | 451 |
lemma E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N}) |
13806 | 452 |
LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
453 |
apply (unfold Lift_def, ensures_tac "close_act") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
454 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
455 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
456 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
457 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
458 |
(** the final steps **) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
459 |
|
46912 | 460 |
lemma lift_3_Req: "0 < N ==> |
13806 | 461 |
Lift \<in> |
462 |
(moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) |
|
463 |
LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
464 |
apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
465 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
466 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
467 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
468 |
(*Now we observe that our integer metric is really a natural number*) |
46912 | 469 |
lemma Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
470 |
apply (rule bounded [THEN Always_weaken]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
471 |
apply (auto simp add: metric_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
472 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
473 |
|
46912 | 474 |
lemmas R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11] |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
475 |
|
46912 | 476 |
lemma lift_3: "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
477 |
apply (rule Always_nonneg [THEN integ_0_le_induct]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
478 |
apply (case_tac "0 < z") |
13806 | 479 |
(*If z \<le> 0 then actually z = 0*) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
480 |
prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
481 |
apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
482 |
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
483 |
LeadsTo_Un [OF lift_4 lift_3_Req]], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
484 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
485 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
486 |
|
46912 | 487 |
lemma lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
488 |
apply (rule LeadsTo_Trans) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
489 |
prefer 2 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
490 |
apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
491 |
apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
492 |
apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
493 |
apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
494 |
apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
495 |
apply (rule open_move [THEN Always_LeadsToI]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
496 |
apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
497 |
(*The case split is not essential but makes the proof much faster.*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
498 |
apply (case_tac "open x", auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
499 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
500 |
|
46912 | 501 |
end |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
502 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
503 |
end |