author | wenzelm |
Tue, 17 Nov 1998 14:07:25 +0100 | |
changeset 5906 | 1f58694fc3e2 |
parent 5783 | 95ac0bf10518 |
child 6024 | cb87f103d114 |
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 |
|
5563 | 9 |
Goal "~ z < w ==> (z < w + #1) = (z = w)"; |
10 |
by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1); |
|
11 |
qed "not_zless_zless1_eq"; |
|
12 |
||
13 |
||
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
14 |
(*split_all_tac causes a big blow-up*) |
5706 | 15 |
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
|
16 |
|
5563 | 17 |
Delsimps [split_paired_All]; |
18 |
||
19 |
Goal "[| x ~: A; y : A |] ==> x ~= y"; |
|
20 |
by (Blast_tac 1); |
|
21 |
qed "not_mem_distinct"; |
|
22 |
||
23 |
fun distinct_tac i = |
|
24 |
dtac zle_neq_implies_zless i THEN |
|
25 |
eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN |
|
26 |
assume_tac i; |
|
27 |
||
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 |
(** 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
|
30 |
val mov_metric1 = read_instantiate_sg (sign_of thy) |
5596 | 31 |
[("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
|
32 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
33 |
val mov_metric2 = read_instantiate_sg (sign_of thy) |
5596 | 34 |
[("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
|
35 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
36 |
val mov_metric3 = read_instantiate_sg (sign_of thy) |
5596 | 37 |
[("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
|
38 |
|
5563 | 39 |
val mov_metric4 = read_instantiate_sg (sign_of thy) |
5596 | 40 |
[("P", "(?x <= metric ?n ?s)")] rev_mp; |
5563 | 41 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
42 |
(*The order in which they are applied seems to be critical...*) |
5563 | 43 |
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4]; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
44 |
|
5357 | 45 |
|
5563 | 46 |
val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos; |
47 |
val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra; |
|
48 |
||
49 |
||
50 |
val metric_simps = |
|
51 |
[metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv, |
|
52 |
order_less_imp_not_eq, order_less_imp_not_eq2, |
|
53 |
not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq, |
|
54 |
zless_zadd1_contra, zless_zadd1_contra', |
|
55 |
zless_not_refl2, zless_not_refl3]; |
|
56 |
||
5340 | 57 |
|
5648 | 58 |
Addsimps [Lprg_def RS def_prg_Init]; |
59 |
program_defs_ref := [Lprg_def]; |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
60 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
61 |
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
|
62 |
[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
|
63 |
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
|
64 |
button_press_def]); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
65 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
66 |
val always_defs = [above_def, below_def, queueing_def, |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
67 |
goingup_def, goingdown_def, ready_def]; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
68 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
69 |
Addsimps (map simp_of_set always_defs); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
70 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
71 |
|
5583 | 72 |
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; |
5648 | 73 |
(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *) |
5357 | 74 |
|
75 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
76 |
(*Simplification for records*) |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
77 |
Addsimps (thms"state.update_defs"); |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
78 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
79 |
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
|
80 |
moving_up_def, moving_down_def]; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
81 |
|
5357 | 82 |
AddIffs [Min_le_Max]; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
83 |
|
5320 | 84 |
|
85 |
val nat_exhaust_le_pred = |
|
86 |
read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust; |
|
87 |
||
88 |
val nat_exhaust_pred_le = |
|
89 |
read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust; |
|
90 |
||
5648 | 91 |
Goal "Lprg : Invariant open_stop"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
92 |
by (rtac InvariantI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
93 |
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
|
94 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
95 |
qed "open_stop"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
96 |
|
5648 | 97 |
Goal "Lprg : Invariant stop_floor"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
98 |
by (rtac InvariantI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
99 |
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
|
100 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
101 |
qed "stop_floor"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
102 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
103 |
(*This one needs open_stop, which was proved above*) |
5648 | 104 |
Goal "Lprg : Invariant open_move"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
105 |
by (rtac InvariantI 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
106 |
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
107 |
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
|
108 |
by (constrains_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
109 |
qed "open_move"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
110 |
|
5648 | 111 |
Goal "Lprg : Invariant moving_up"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
112 |
by (rtac InvariantI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
113 |
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
|
114 |
by (constrains_tac 1); |
5563 | 115 |
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
|
116 |
qed "moving_up"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
117 |
|
5648 | 118 |
Goal "Lprg : Invariant moving_down"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
119 |
by (rtac InvariantI 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
120 |
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
|
121 |
by (constrains_tac 1); |
5563 | 122 |
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
|
123 |
qed "moving_down"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
124 |
|
5648 | 125 |
Goal "Lprg : Invariant bounded"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
126 |
by (rtac InvariantI 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
127 |
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
128 |
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
|
129 |
by (constrains_tac 1); |
5563 | 130 |
by (ALLGOALS Clarify_tac); |
131 |
by (REPEAT_FIRST distinct_tac); |
|
132 |
by (ALLGOALS |
|
133 |
(asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls))); |
|
134 |
by (ALLGOALS |
|
135 |
(blast_tac (claset() addDs [zle_imp_zless_or_eq] |
|
136 |
addIs [zless_trans]))); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
137 |
qed "bounded"; |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
138 |
|
5320 | 139 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
140 |
|
5320 | 141 |
(*** Progress ***) |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
142 |
|
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
143 |
|
5320 | 144 |
val abbrev_defs = [moving_def, stopped_def, |
5340 | 145 |
opened_def, closed_def, atFloor_def, Req_def]; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
146 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
147 |
Addsimps (map simp_of_set abbrev_defs); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset
|
148 |
|
5340 | 149 |
|
150 |
(** 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
|
151 |
|
5357 | 152 |
(** Lift_1 **) |
153 |
||
5648 | 154 |
Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)"; |
5340 | 155 |
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
|
156 |
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
|
157 |
qed "E_thm01"; (*lem_lift_1_5*) |
5340 | 158 |
|
5648 | 159 |
Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \ |
5340 | 160 |
\ (Req n Int opened - atFloor n)"; |
161 |
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
|
162 |
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
|
163 |
qed "E_thm02"; (*lem_lift_1_1*) |
5340 | 164 |
|
5648 | 165 |
Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \ |
5340 | 166 |
\ (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
|
167 |
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
|
168 |
qed "E_thm03"; (*lem_lift_1_2*) |
5340 | 169 |
|
5648 | 170 |
Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \ |
5340 | 171 |
\ (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
|
172 |
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
|
173 |
qed "E_thm04"; (*lem_lift_1_7*) |
5340 | 174 |
|
175 |
||
5357 | 176 |
(** Lift 2. Statements of thm05a and thm05b were wrong! **) |
5340 | 177 |
|
178 |
Open_locale "floor"; |
|
179 |
||
5357 | 180 |
val Min_le_n = thm "Min_le_n"; |
181 |
val n_le_Max = thm "n_le_Max"; |
|
182 |
||
183 |
AddIffs [Min_le_n, n_le_Max]; |
|
5340 | 184 |
|
5563 | 185 |
val le_MinD = Min_le_n RS zle_anti_sym; |
186 |
val Max_leD = n_le_Max RSN (2,zle_anti_sym); |
|
5357 | 187 |
|
5563 | 188 |
AddSDs [le_MinD, zleI RS le_MinD, |
189 |
Max_leD, zleI RS Max_leD]; |
|
5357 | 190 |
|
191 |
(*lem_lift_2_0 |
|
192 |
NOT an ensures property, but a mere inclusion; |
|
193 |
don't know why script lift_2.uni says ENSURES*) |
|
5648 | 194 |
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \ |
5340 | 195 |
\ ((closed Int goingup Int Req n) Un \ |
196 |
\ (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
|
197 |
by (rtac subset_imp_LeadsTo 1); |
5563 | 198 |
by (auto_tac (claset() addSEs [int_neqE], simpset())); |
5340 | 199 |
qed "E_thm05c"; |
200 |
||
5357 | 201 |
(*lift_2*) |
5648 | 202 |
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \ |
5340 | 203 |
\ (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
|
204 |
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
|
205 |
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
|
206 |
by (ensures_tac "req_up" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
207 |
by Auto_tac; |
5340 | 208 |
qed "lift_2"; |
209 |
||
210 |
||
5357 | 211 |
(** Towards lift_4 ***) |
5563 | 212 |
|
5357 | 213 |
|
214 |
(*lem_lift_4_1 *) |
|
5563 | 215 |
Goal "#0 < N ==> \ |
5648 | 216 |
\ Lprg : LeadsTo \ |
5563 | 217 |
\ (moving Int Req n Int {s. metric n s = N} Int \ |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
218 |
\ {s. floor s ~: req s} Int {s. up s}) \ |
5563 | 219 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 220 |
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
|
221 |
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
|
222 |
by Safe_tac; |
5357 | 223 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
5563 | 224 |
by (etac (zleI RS zle_anti_sym 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
|
225 |
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
|
226 |
by (REPEAT_FIRST distinct_tac); |
5563 | 227 |
(** LEVEL 6 **) |
5583 | 228 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps |
229 |
[zle_def] @ metric_simps @ zcompare_rls))); |
|
5357 | 230 |
qed "E_thm12a"; |
231 |
||
232 |
||
233 |
||
234 |
(*lem_lift_4_3 *) |
|
5563 | 235 |
Goal "#0 < N ==> \ |
5648 | 236 |
\ Lprg : LeadsTo \ |
5563 | 237 |
\ (moving Int Req n Int {s. metric n s = N} Int \ |
5357 | 238 |
\ {s. floor s ~: req s} - {s. up s}) \ |
5563 | 239 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 240 |
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
|
241 |
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
|
242 |
by Safe_tac; |
5357 | 243 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
5563 | 244 |
by (etac (zleI RS zle_anti_sym 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
|
245 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
5563 | 246 |
by (REPEAT_FIRST distinct_tac); |
247 |
(** LEVEL 6 **) |
|
5583 | 248 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps |
249 |
[zle_def] @ metric_simps @ zcompare_rls))); |
|
5783 | 250 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
5357 | 251 |
qed "E_thm12b"; |
252 |
||
253 |
(*lift_4*) |
|
5648 | 254 |
Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \ |
5357 | 255 |
\ {s. floor s ~: req s}) \ |
5563 | 256 |
\ (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
|
257 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 258 |
by (etac E_thm12b 3); |
259 |
by (etac E_thm12a 2); |
|
5357 | 260 |
by (Blast_tac 1); |
261 |
qed "lift_4"; |
|
262 |
||
263 |
||
264 |
(** towards lift_5 **) |
|
265 |
||
266 |
(*lem_lift_5_3*) |
|
5563 | 267 |
Goal "#0<N \ |
5648 | 268 |
\ ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \ |
5563 | 269 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 270 |
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
|
271 |
by (ensures_tac "req_up" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
272 |
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
|
273 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
5563 | 274 |
by (ALLGOALS |
275 |
(asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls))); |
|
276 |
(** LEVEL 5 **) |
|
277 |
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1); |
|
278 |
by Auto_tac; |
|
5583 | 279 |
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1); |
5357 | 280 |
qed "E_thm16a"; |
281 |
||
282 |
(*lem_lift_5_1 has ~goingup instead of goingdown*) |
|
5563 | 283 |
Goal "#0<N ==> \ |
5648 | 284 |
\ Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \ |
5563 | 285 |
\ (moving Int Req n Int {s. metric n s < N})"; |
5357 | 286 |
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
|
287 |
by (ensures_tac "req_down" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
288 |
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
|
289 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
5563 | 290 |
by (ALLGOALS |
5783 | 291 |
(asm_simp_tac (simpset() addsimps [zle_def] @ |
5596 | 292 |
metric_simps @ zcompare_rls))); |
5563 | 293 |
(** LEVEL 5 **) |
5583 | 294 |
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1); |
295 |
by (etac exE 1); |
|
296 |
by (etac ssubst 1); |
|
297 |
by Auto_tac; |
|
298 |
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1); |
|
5357 | 299 |
qed "E_thm16b"; |
300 |
||
301 |
||
302 |
||
303 |
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
|
304 |
i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
|
5563 | 305 |
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"; |
306 |
by (asm_simp_tac (simpset() addsimps metric_simps) 1); |
|
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset
|
307 |
by (force_tac (claset() delrules [impCE] addEs [impCE], |
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset
|
308 |
simpset() addsimps conj_comms) 1); |
5357 | 309 |
qed "E_thm16c"; |
310 |
||
311 |
||
312 |
(*lift_5*) |
|
5648 | 313 |
Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N}) \ |
5563 | 314 |
\ (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
|
315 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 316 |
by (etac E_thm16b 3); |
317 |
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
|
318 |
by (dtac E_thm16c 1); |
5357 | 319 |
by (Blast_tac 1); |
320 |
qed "lift_5"; |
|
321 |
||
322 |
||
323 |
(** towards lift_3 **) |
|
324 |
||
325 |
(*lemma used to prove lem_lift_3_1*) |
|
5563 | 326 |
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
|
327 |
by (etac rev_mp 1); |
5563 | 328 |
(*force simplification of "metric..." while in conclusion part*) |
329 |
by (asm_simp_tac (simpset() addsimps metric_simps) 1); |
|
330 |
by (auto_tac (claset() addIs [zleI, zle_anti_sym], |
|
5583 | 331 |
simpset() addsimps zcompare_rls@[zadd_int, integ_of_Min])); |
5563 | 332 |
(*trans_tac (or decision procedures) could do the rest*) |
333 |
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2); |
|
334 |
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1); |
|
335 |
by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]))); |
|
336 |
by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp)); |
|
337 |
by (REPEAT_FIRST (etac ssubst)); |
|
5583 | 338 |
by (auto_tac (claset(), simpset() addsimps [zadd_int])); |
5357 | 339 |
qed "metric_eq_0D"; |
340 |
||
341 |
AddDs [metric_eq_0D]; |
|
342 |
||
343 |
||
344 |
(*lem_lift_3_1*) |
|
5648 | 345 |
Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0}) \ |
5357 | 346 |
\ (stopped Int atFloor n)"; |
347 |
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
|
348 |
by (ensures_tac "request_act" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
349 |
by Auto_tac; |
5357 | 350 |
qed "E_thm11"; |
351 |
||
352 |
(*lem_lift_3_5*) |
|
5648 | 353 |
Goal "Lprg : LeadsTo \ |
5563 | 354 |
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
355 |
\ (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
|
356 |
by (ensures_tac "request_act" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
357 |
by (auto_tac (claset(), simpset() addsimps metric_simps)); |
5357 | 358 |
qed "E_thm13"; |
359 |
||
360 |
(*lem_lift_3_6*) |
|
5563 | 361 |
Goal "#0 < N ==> \ |
5648 | 362 |
\ Lprg : LeadsTo \ |
5563 | 363 |
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
364 |
\ (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
|
365 |
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
|
366 |
by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
367 |
by (auto_tac (claset(), simpset() addsimps metric_simps)); |
5357 | 368 |
qed "E_thm14"; |
369 |
||
370 |
(*lem_lift_3_7*) |
|
5648 | 371 |
Goal "Lprg : LeadsTo \ |
5563 | 372 |
\ (opened Int Req n Int {s. metric n s = N}) \ |
373 |
\ (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
|
374 |
by (ensures_tac "close_act" 1); |
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset
|
375 |
by (auto_tac (claset(), simpset() addsimps metric_simps)); |
5357 | 376 |
qed "E_thm15"; |
377 |
||
378 |
||
379 |
(** the final steps **) |
|
380 |
||
5563 | 381 |
Goal "#0 < N ==> \ |
5648 | 382 |
\ Lprg : LeadsTo \ |
5563 | 383 |
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
384 |
\ (moving Int Req n Int {s. metric n s < N})"; |
|
5479 | 385 |
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] |
386 |
addIs [LeadsTo_Trans]) 1); |
|
5357 | 387 |
qed "lift_3_Req"; |
388 |
||
389 |
||
5563 | 390 |
|
391 |
(*Now we observe that our integer metric is really a natural number*) |
|
392 |
Goal "reachable Lprg <= {s. #0 <= metric n s}"; |
|
393 |
by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1); |
|
394 |
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1); |
|
395 |
by (auto_tac (claset(), |
|
396 |
simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd])); |
|
397 |
by (REPEAT_FIRST (etac ssubst)); |
|
5583 | 398 |
by (auto_tac (claset(), simpset() addsimps [zadd_int])); |
5563 | 399 |
qed "reach_nonneg"; |
400 |
||
401 |
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken; |
|
402 |
||
5648 | 403 |
Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)"; |
5563 | 404 |
by (rtac (reach_nonneg RS integ_0_le_induct) 1); |
405 |
by (case_tac "#0 < z" 1); |
|
406 |
(*If z <= #0 then actually z = #0*) |
|
407 |
by (fold_tac [zle_def]); |
|
408 |
by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
409 |
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
|
410 |
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
5583 | 411 |
by (rtac lift_3_Req 3); |
412 |
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
|
413 |
by Auto_tac; |
5357 | 414 |
qed "lift_3"; |
415 |
||
416 |
||
5648 | 417 |
Goal "Lprg : LeadsTo (Req n) (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
|
418 |
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
|
419 |
by (rtac (E_thm04 RS LeadsTo_Un) 2); |
5583 | 420 |
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
|
421 |
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
|
422 |
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
|
423 |
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
|
424 |
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
|
425 |
by (rtac E_thm02 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
426 |
by (rtac (open_move RS Invariant_LeadsToI) 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
427 |
by (rtac (open_stop RS Invariant_LeadsToI) 1); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
428 |
by (rtac subset_imp_LeadsTo 1); |
5340 | 429 |
by (Clarify_tac 1); |
5484 | 430 |
(*The case split is not essential but makes Blast_tac much faster. |
431 |
Must also be careful to prevent simplification from looping*) |
|
432 |
by (case_tac "open x" 1); |
|
433 |
by (ALLGOALS (rotate_tac ~1)); |
|
434 |
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
|
435 |
by (Blast_tac 1); |
5340 | 436 |
qed "lift_1"; |
437 |
||
5583 | 438 |
Close_locale(); |