author | wenzelm |
Thu, 05 Aug 1999 22:11:43 +0200 | |
changeset 7179 | 6ffe5067d5cc |
parent 7079 | eec20608c791 |
child 7221 | 13e43b7456a1 |
permissions | -rw-r--r-- |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Lift |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
5 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
6 |
The Lift-Control Example |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
7 |
*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
8 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
9 |
(*split_all_tac causes a big blow-up*) |
5706 | 10 |
claset_ref() := claset() delSWrapper record_split_name; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
11 |
|
5563 | 12 |
Goal "[| x ~: A; y : A |] ==> x ~= y"; |
13 |
by (Blast_tac 1); |
|
14 |
qed "not_mem_distinct"; |
|
15 |
||
16 |
fun distinct_tac i = |
|
17 |
dtac zle_neq_implies_zless i THEN |
|
18 |
eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN |
|
19 |
assume_tac i; |
|
20 |
||
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
21 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
22 |
(** Rules to move "metric n s" out of the assumptions, for case splitting **) |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
23 |
val mov_metric1 = read_instantiate_sg (sign_of thy) |
5596 | 24 |
[("P", "?x < metric ?n ?s")] rev_mp; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
25 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
26 |
val mov_metric2 = read_instantiate_sg (sign_of thy) |
5596 | 27 |
[("P", "?x = metric ?n ?s")] rev_mp; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
28 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
29 |
val mov_metric3 = read_instantiate_sg (sign_of thy) |
5596 | 30 |
[("P", "~ (?x < metric ?n ?s)")] rev_mp; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
31 |
|
5563 | 32 |
val mov_metric4 = read_instantiate_sg (sign_of thy) |
5596 | 33 |
[("P", "(?x <= metric ?n ?s)")] rev_mp; |
5563 | 34 |
|
6916 | 35 |
val mov_metric5 = read_instantiate_sg (sign_of thy) |
36 |
[("P", "?x ~= metric ?n ?s")] rev_mp; |
|
37 |
||
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
38 |
(*The order in which they are applied seems to be critical...*) |
6916 | 39 |
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4, |
40 |
mov_metric5]; |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
41 |
|
6139 | 42 |
val metric_simps = [metric_def, vimage_def]; |
5563 | 43 |
|
5340 | 44 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
45 |
Addsimps [Lift_def RS def_prg_Init]; |
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
46 |
program_defs_ref := [Lift_def]; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
47 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
48 |
Addsimps (map simp_of_act |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
49 |
[request_act_def, open_act_def, close_act_def, |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
50 |
req_up_def, req_down_def, move_up_def, move_down_def, |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
51 |
button_press_def]); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
52 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
53 |
val always_defs = [above_def, below_def, queueing_def, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
54 |
goingup_def, goingdown_def, ready_def]; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
55 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
56 |
Addsimps (map simp_of_set always_defs); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
57 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
58 |
|
5583 | 59 |
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
60 |
(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *) |
5357 | 61 |
|
62 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
63 |
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
64 |
moving_up_def, moving_down_def]; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
65 |
|
5357 | 66 |
AddIffs [Min_le_Max]; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
67 |
|
5320 | 68 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
69 |
Goal "Lift : Always open_stop"; |
6570 | 70 |
by (rtac AlwaysI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
71 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
72 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
73 |
qed "open_stop"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
74 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
75 |
Goal "Lift : Always stop_floor"; |
6570 | 76 |
by (rtac AlwaysI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
77 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
78 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
79 |
qed "stop_floor"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
80 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
81 |
(*This one needs open_stop, which was proved above*) |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
82 |
Goal "Lift : Always open_move"; |
6570 | 83 |
by (rtac AlwaysI 1); |
84 |
by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
85 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
86 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
87 |
qed "open_move"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
88 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
89 |
Goal "Lift : Always moving_up"; |
6570 | 90 |
by (rtac AlwaysI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
91 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
92 |
by (constrains_tac 1); |
7000
6920cf9b8623
rewrite add1_zle_eq is no longer in the default simpset
paulson
parents:
6916
diff
changeset
|
93 |
by (auto_tac (claset(), |
6920cf9b8623
rewrite add1_zle_eq is no longer in the default simpset
paulson
parents:
6916
diff
changeset
|
94 |
simpset() addsimps [add1_zle_eq])); |
5563 | 95 |
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
96 |
qed "moving_up"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
97 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
98 |
Goal "Lift : Always moving_down"; |
6570 | 99 |
by (rtac AlwaysI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
100 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
101 |
by (constrains_tac 1); |
5563 | 102 |
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
103 |
qed "moving_down"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
104 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
105 |
Goal "Lift : Always bounded"; |
6570 | 106 |
by (rtac AlwaysI 1); |
6740 | 107 |
by (rtac (Always_Int_rule [moving_up, moving_down] RS |
108 |
Always_ConstrainsI RS StableI) 2); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
109 |
by (Force_tac 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
110 |
by (constrains_tac 1); |
5563 | 111 |
by (ALLGOALS Clarify_tac); |
112 |
by (REPEAT_FIRST distinct_tac); |
|
6161 | 113 |
by Auto_tac; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
114 |
qed "bounded"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
115 |
|
5320 | 116 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
117 |
|
5320 | 118 |
(*** Progress ***) |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
119 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
120 |
|
5320 | 121 |
val abbrev_defs = [moving_def, stopped_def, |
5340 | 122 |
opened_def, closed_def, atFloor_def, Req_def]; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
123 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
124 |
Addsimps (map simp_of_set abbrev_defs); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
125 |
|
5340 | 126 |
|
127 |
(** The HUG'93 paper mistakenly omits the Req n from these! **) |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
128 |
|
5357 | 129 |
(** Lift_1 **) |
130 |
||
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
131 |
Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"; |
5340 | 132 |
by (cut_facts_tac [stop_floor] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
133 |
by (ensures_tac "open_act" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
134 |
qed "E_thm01"; (*lem_lift_1_5*) |
5340 | 135 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
136 |
Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \ |
6139 | 137 |
\ (Req n Int opened - atFloor n)"; |
5340 | 138 |
by (cut_facts_tac [stop_floor] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
139 |
by (ensures_tac "open_act" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
140 |
qed "E_thm02"; (*lem_lift_1_1*) |
5340 | 141 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
142 |
Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \ |
6139 | 143 |
\ (Req n Int closed - (atFloor n - queueing))"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
144 |
by (ensures_tac "close_act" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
145 |
qed "E_thm03"; (*lem_lift_1_2*) |
5340 | 146 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
147 |
Goal "Lift : (Req n Int closed Int (atFloor n - queueing)) \ |
6536 | 148 |
\ LeadsTo (opened Int atFloor n)"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
149 |
by (ensures_tac "open_act" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
150 |
qed "E_thm04"; (*lem_lift_1_7*) |
5340 | 151 |
|
152 |
||
5357 | 153 |
(** Lift 2. Statements of thm05a and thm05b were wrong! **) |
5340 | 154 |
|
155 |
Open_locale "floor"; |
|
156 |
||
5357 | 157 |
val Min_le_n = thm "Min_le_n"; |
158 |
val n_le_Max = thm "n_le_Max"; |
|
159 |
||
160 |
AddIffs [Min_le_n, n_le_Max]; |
|
5340 | 161 |
|
6676 | 162 |
val le_MinD = Min_le_n RS order_antisym; |
163 |
val Max_leD = n_le_Max RSN (2,order_antisym); |
|
5357 | 164 |
|
6676 | 165 |
val linorder_leI = linorder_not_less RS iffD1; |
166 |
||
167 |
AddSDs [le_MinD, linorder_leI RS le_MinD, |
|
168 |
Max_leD, linorder_leI RS Max_leD]; |
|
5357 | 169 |
|
170 |
(*lem_lift_2_0 |
|
171 |
NOT an ensures property, but a mere inclusion; |
|
172 |
don't know why script lift_2.uni says ENSURES*) |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
173 |
Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ |
6536 | 174 |
\ LeadsTo ((closed Int goingup Int Req n) Un \ |
6139 | 175 |
\ (closed Int goingdown Int Req n))"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
176 |
by (rtac subset_imp_LeadsTo 1); |
5563 | 177 |
by (auto_tac (claset() addSEs [int_neqE], simpset())); |
5340 | 178 |
qed "E_thm05c"; |
179 |
||
5357 | 180 |
(*lift_2*) |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
181 |
Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ |
6536 | 182 |
\ LeadsTo (moving Int Req n)"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
183 |
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
184 |
by (ensures_tac "req_down" 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
185 |
by (ensures_tac "req_up" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
186 |
by Auto_tac; |
5340 | 187 |
qed "lift_2"; |
188 |
||
189 |
||
5357 | 190 |
(** Towards lift_4 ***) |
5563 | 191 |
|
5357 | 192 |
|
193 |
(*lem_lift_4_1 *) |
|
5563 | 194 |
Goal "#0 < N ==> \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
195 |
\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
6536 | 196 |
\ {s. floor s ~: req s} Int {s. up s}) \ |
197 |
\ LeadsTo \ |
|
6139 | 198 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 199 |
by (cut_facts_tac [moving_up] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
200 |
by (ensures_tac "move_up" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
201 |
by Safe_tac; |
5357 | 202 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
6676 | 203 |
by (etac (linorder_leI RS order_antisym RS sym) 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
204 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
205 |
by (REPEAT_FIRST distinct_tac); |
5563 | 206 |
(** LEVEL 6 **) |
5583 | 207 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps |
208 |
[zle_def] @ metric_simps @ zcompare_rls))); |
|
5357 | 209 |
qed "E_thm12a"; |
210 |
||
211 |
||
212 |
||
213 |
(*lem_lift_4_3 *) |
|
5563 | 214 |
Goal "#0 < N ==> \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
215 |
\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
6536 | 216 |
\ {s. floor s ~: req s} - {s. up s}) \ |
217 |
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; |
|
5357 | 218 |
by (cut_facts_tac [moving_down] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
219 |
by (ensures_tac "move_down" 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
220 |
by Safe_tac; |
5357 | 221 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
6676 | 222 |
by (etac (linorder_leI RS order_antisym RS sym) 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
223 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
5563 | 224 |
by (REPEAT_FIRST distinct_tac); |
225 |
(** LEVEL 6 **) |
|
6139 | 226 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
5357 | 227 |
qed "E_thm12b"; |
228 |
||
229 |
(*lift_4*) |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
230 |
Goal "#0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
6536 | 231 |
\ {s. floor s ~: req s}) LeadsTo \ |
5563 | 232 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
233 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 234 |
by (etac E_thm12b 3); |
235 |
by (etac E_thm12a 2); |
|
5357 | 236 |
by (Blast_tac 1); |
237 |
qed "lift_4"; |
|
238 |
||
239 |
||
240 |
(** towards lift_5 **) |
|
241 |
||
242 |
(*lem_lift_5_3*) |
|
5563 | 243 |
Goal "#0<N \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
244 |
\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \ |
5563 | 245 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 246 |
by (cut_facts_tac [bounded] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
247 |
by (ensures_tac "req_up" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
248 |
by Auto_tac; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
249 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
6139 | 250 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
6128 | 251 |
by (Blast_tac 1); |
5357 | 252 |
qed "E_thm16a"; |
253 |
||
7079
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
254 |
(*Must sometimes delete them because they introduce multiplication*) |
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
255 |
val metric_ss = simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv] |
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
256 |
addsimps metric_simps; |
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
257 |
|
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
258 |
|
5357 | 259 |
(*lem_lift_5_1 has ~goingup instead of goingdown*) |
5563 | 260 |
Goal "#0<N ==> \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
261 |
\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ |
5563 | 262 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 263 |
by (cut_facts_tac [bounded] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
264 |
by (ensures_tac "req_down" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
265 |
by Auto_tac; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
266 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
7079
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
267 |
by (ALLGOALS (asm_simp_tac (metric_ss addsimps zcompare_rls))); |
6128 | 268 |
by (Blast_tac 1); |
5357 | 269 |
qed "E_thm16b"; |
270 |
||
271 |
||
272 |
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
|
273 |
i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
|
5563 | 274 |
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"; |
7079
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
275 |
by (asm_simp_tac metric_ss 1); |
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset
|
276 |
by (force_tac (claset() delrules [impCE] addEs [impCE], |
6139 | 277 |
simpset() addsimps conj_comms) 1); |
5357 | 278 |
qed "E_thm16c"; |
279 |
||
280 |
||
281 |
(*lift_5*) |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
282 |
Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ |
5563 | 283 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
284 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 285 |
by (etac E_thm16b 3); |
286 |
by (etac E_thm16a 2); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
287 |
by (dtac E_thm16c 1); |
5357 | 288 |
by (Blast_tac 1); |
289 |
qed "lift_5"; |
|
290 |
||
291 |
||
292 |
(** towards lift_3 **) |
|
293 |
||
294 |
(*lemma used to prove lem_lift_3_1*) |
|
5563 | 295 |
Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
296 |
by (etac rev_mp 1); |
5563 | 297 |
(*force simplification of "metric..." while in conclusion part*) |
7079
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
298 |
by (asm_simp_tac metric_ss 1); |
5357 | 299 |
qed "metric_eq_0D"; |
300 |
||
301 |
AddDs [metric_eq_0D]; |
|
302 |
||
303 |
||
304 |
(*lem_lift_3_1*) |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
305 |
Goal "Lift : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \ |
5357 | 306 |
\ (stopped Int atFloor n)"; |
307 |
by (cut_facts_tac [bounded] 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
308 |
by (ensures_tac "request_act" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
309 |
by Auto_tac; |
5357 | 310 |
qed "E_thm11"; |
311 |
||
6916 | 312 |
val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics)) |
7079
eec20608c791
removed the combine_coeff simproc because linear arith does not handle
paulson
parents:
7000
diff
changeset
|
313 |
THEN auto_tac (claset(), metric_ss); |
6916 | 314 |
|
5357 | 315 |
(*lem_lift_3_5*) |
6536 | 316 |
Goal |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
317 |
"Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
6536 | 318 |
\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
319 |
by (ensures_tac "request_act" 1); |
6916 | 320 |
by metric_tac; |
5357 | 321 |
qed "E_thm13"; |
322 |
||
323 |
(*lem_lift_3_6*) |
|
5563 | 324 |
Goal "#0 < N ==> \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
325 |
\ Lift : \ |
5563 | 326 |
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
6536 | 327 |
\ LeadsTo (opened Int Req n Int {s. metric n s = N})"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
328 |
by (ensures_tac "open_act" 1); |
6916 | 329 |
by metric_tac; |
5357 | 330 |
qed "E_thm14"; |
331 |
||
332 |
(*lem_lift_3_7*) |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
333 |
Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \ |
6536 | 334 |
\ LeadsTo (closed Int Req n Int {s. metric n s = N})"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
335 |
by (ensures_tac "close_act" 1); |
6916 | 336 |
by metric_tac; |
5357 | 337 |
qed "E_thm15"; |
338 |
||
339 |
||
340 |
(** the final steps **) |
|
341 |
||
5563 | 342 |
Goal "#0 < N ==> \ |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
343 |
\ Lift : \ |
5563 | 344 |
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
6536 | 345 |
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; |
5479 | 346 |
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] |
347 |
addIs [LeadsTo_Trans]) 1); |
|
5357 | 348 |
qed "lift_3_Req"; |
349 |
||
350 |
||
5563 | 351 |
(*Now we observe that our integer metric is really a natural number*) |
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
352 |
Goal "Lift : Always {s. #0 <= metric n s}"; |
6570 | 353 |
by (rtac (bounded RS Always_weaken) 1); |
6916 | 354 |
by metric_tac; |
6570 | 355 |
qed "Always_nonneg"; |
5563 | 356 |
|
6570 | 357 |
val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken; |
5563 | 358 |
|
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
359 |
Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"; |
6570 | 360 |
by (rtac (Always_nonneg RS integ_0_le_induct) 1); |
5563 | 361 |
by (case_tac "#0 < z" 1); |
362 |
(*If z <= #0 then actually z = #0*) |
|
363 |
by (fold_tac [zle_def]); |
|
6676 | 364 |
by (force_tac (claset() addIs [R_thm11, order_antisym], simpset()) 2); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
365 |
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
366 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 367 |
by (rtac lift_3_Req 3); |
368 |
by (rtac lift_4 2); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
369 |
by Auto_tac; |
5357 | 370 |
qed "lift_3"; |
371 |
||
372 |
||
6718
e869ff059252
renamed Lprg to Lift; simplified proof of Always_nonneg
paulson
parents:
6676
diff
changeset
|
373 |
Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
374 |
by (rtac LeadsTo_Trans 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
375 |
by (rtac (E_thm04 RS LeadsTo_Un) 2); |
5583 | 376 |
by (rtac LeadsTo_Un_post 2); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
377 |
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
378 |
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
379 |
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
380 |
by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
381 |
by (rtac E_thm02 2); |
6570 | 382 |
by (rtac (open_move RS Always_LeadsToI) 1); |
383 |
by (rtac (open_stop RS Always_LeadsToI) 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
384 |
by (rtac subset_imp_LeadsTo 1); |
5340 | 385 |
by (Clarify_tac 1); |
5484 | 386 |
(*The case split is not essential but makes Blast_tac much faster. |
387 |
Must also be careful to prevent simplification from looping*) |
|
388 |
by (case_tac "open x" 1); |
|
389 |
by (ALLGOALS (rotate_tac ~1)); |
|
390 |
by (ALLGOALS Asm_full_simp_tac); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
391 |
by (Blast_tac 1); |
5340 | 392 |
qed "lift_1"; |
393 |
||
6024 | 394 |
Close_locale "floor"; |