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