author  paulson 
Tue, 01 Sep 1998 10:10:11 +0200  
changeset 5410  5ed7547a7f74 
parent 5357  6efb2b87610c 
child 5424  771a68a468cc 
permissions  rwrr 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

1 
(* Title: HOL/UNITY/Lift 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

2 
ID: $Id$ 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

4 
Copyright 1998 University of Cambridge 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

5 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

6 
The LiftControl Example 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

7 
*) 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

8 

5340  9 

5357  10 
(*To move 0 < metric n s out of the assumptions for case splitting*) 
11 
val rev_mp' = read_instantiate_sg (sign_of thy) 

12 
[("P", "0 < metric ?n ?s")] rev_mp; 

13 

14 
val Suc_lessD_contra = Suc_lessD COMP rev_contrapos; 

15 
val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra; 

5340  16 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

17 
val always_defs = [above_def, below_def, queueing_def, 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

18 
goingup_def, goingdown_def, ready_def]; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

19 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

20 
val cmd_defs = [Lprg_def, 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

21 
request_act_def, open_act_def, close_act_def, 
5357  22 
req_up_def, req_down_def, move_up_def, move_down_def, 
23 
button_press_def]; 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

24 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

25 
Goalw [Lprg_def] "id : Acts Lprg"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

26 
by (Simp_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

27 
qed "id_in_Acts"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

28 
AddIffs [id_in_Acts]; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

29 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

30 

5357  31 
val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post 
32 
and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un); 

33 
(* [ LeadsTo Lprg B C; LeadsTo Lprg A B ] ==> LeadsTo Lprg (A Un B) C *) 

34 

35 

36 
val metric_simps = 

37 
[metric_def, vimage_def, 

38 
not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq, 

39 
Suc_lessD_contra, Suc_lessD_contra', 

40 
less_not_refl2, less_not_refl3]; 

41 

42 

43 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

44 
(*split_all_tac causes a big blowup*) 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

45 
claset_ref() := claset() delSWrapper "split_all_tac"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

46 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

47 
(*Simplification for records*) 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

48 
Addsimps (thms"state.update_defs"); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

49 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

50 
Addsimps [Suc_le_eq]; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

51 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

52 
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def, 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

53 
moving_up_def, moving_down_def]; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

54 

5357  55 
AddIffs [Min_le_Max]; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

56 

5320  57 

58 
val nat_exhaust_le_pred = 

59 
read_instantiate_sg (sign_of thy) [("P", "?m <= ?y1")] nat.exhaust; 

60 

61 
val nat_exhaust_pred_le = 

62 
read_instantiate_sg (sign_of thy) [("P", "?y1 <= ?m")] nat.exhaust; 

63 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

64 
Goal "m < n ==> m <= n1"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

65 
by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

66 
qed "less_imp_le_pred"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

67 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

68 
Goalw [Lprg_def] "Invariant Lprg open_stop"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

69 
by (rtac InvariantI 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

70 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

71 
by (constrains_tac (cmd_defs@always_defs) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

72 
qed "open_stop"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

73 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

74 
Goalw [Lprg_def] "Invariant Lprg stop_floor"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

75 
by (rtac InvariantI 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

76 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

77 
by (constrains_tac (cmd_defs@always_defs) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

78 
qed "stop_floor"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

79 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

80 
(*This one needs open_stop, which was proved above*) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

81 
Goal "Invariant Lprg open_move"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

82 
by (rtac InvariantI 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

83 
br (open_stop RS Invariant_ConstrainsI RS StableI) 2; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

84 
bw Lprg_def; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

85 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

86 
by (constrains_tac (cmd_defs@always_defs) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

87 
qed "open_move"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

88 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

89 
Goalw [Lprg_def] "Invariant Lprg moving_up"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

90 
by (rtac InvariantI 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

91 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

92 
by (constrains_tac (cmd_defs@always_defs) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

93 
by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

94 
qed "moving_up"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

95 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

96 
Goalw [Lprg_def] "Invariant Lprg moving_down"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

97 
by (rtac InvariantI 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

98 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

99 
by (constrains_tac (cmd_defs@always_defs) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

100 
by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

101 
by (auto_tac (claset(), 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

102 
simpset() addsimps [gr_implies_gr0 RS le_pred_eq])); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

103 
qed "moving_down"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

104 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

105 

5320  106 
Goal "Invariant Lprg bounded"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

107 
by (rtac InvariantI 1); 
5320  108 
br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2; 
109 
bw Lprg_def; 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

110 
by (Force_tac 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

111 
by (constrains_tac (cmd_defs@always_defs) 1); 
5320  112 
by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le])); 
113 
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); 

114 
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq])); 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

115 
qed "bounded"; 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

116 

5320  117 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

118 

5320  119 
(*** Progress ***) 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

120 

e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

121 

5320  122 
val abbrev_defs = [moving_def, stopped_def, 
5340  123 
opened_def, closed_def, atFloor_def, Req_def]; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

124 

5320  125 
val defs = cmd_defs@always_defs@abbrev_defs; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

126 

5340  127 

128 
(** The HUG'93 paper mistakenly omits the Req n from these! **) 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

129 

5357  130 
(** Lift_1 **) 
131 

132 
(*lem_lift_1_5*) 

5320  133 
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)"; 
5340  134 
by (cut_facts_tac [stop_floor] 1); 
5320  135 
by (ensures_tac defs "open_act" 1); 
5340  136 
qed "E_thm01"; 
137 

5357  138 
(*lem_lift_1_1*) 
5340  139 
Goal "LeadsTo Lprg (Req n Int stopped  atFloor n) \ 
140 
\ (Req n Int opened  atFloor n)"; 

141 
by (cut_facts_tac [stop_floor] 1); 

142 
by (ensures_tac defs "open_act" 1); 

143 
qed "E_thm02"; 

144 

5357  145 
(*lem_lift_1_2*) 
5340  146 
Goal "LeadsTo Lprg (Req n Int opened  atFloor n) \ 
147 
\ (Req n Int closed  (atFloor n  queueing))"; 

148 
by (ensures_tac defs "close_act" 1); 

149 
qed "E_thm03"; 

150 

5357  151 

152 
(*lem_lift_1_7*) 

5340  153 
Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n  queueing)) \ 
154 
\ (opened Int atFloor n)"; 

155 
by (ensures_tac defs "open_act" 1); 

156 
qed "E_thm04"; 

157 

158 

5357  159 
(** Lift 2. Statements of thm05a and thm05b were wrong! **) 
5340  160 

161 
Open_locale "floor"; 

162 

5357  163 
val Min_le_n = thm "Min_le_n"; 
164 
val n_le_Max = thm "n_le_Max"; 

165 

166 
AddIffs [Min_le_n, n_le_Max]; 

5340  167 

5357  168 
val le_MinD = Min_le_n RS le_anti_sym; 
169 
val Max_leD = n_le_Max RSN (2,le_anti_sym); 

170 

171 
AddSDs [le_MinD, leI RS le_MinD, 

172 
Max_leD, leI RS Max_leD]; 

173 

174 
(*lem_lift_2_0 

175 
NOT an ensures property, but a mere inclusion; 

176 
don't know why script lift_2.uni says ENSURES*) 

5340  177 
Goal "LeadsTo Lprg (Req n Int closed  (atFloor n  queueing)) \ 
178 
\ ((closed Int goingup Int Req n) Un \ 

179 
\ (closed Int goingdown Int Req n))"; 

180 
br subset_imp_LeadsTo 1; 

181 
by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs)); 

182 
qed "E_thm05c"; 

183 

5357  184 
(*lift_2*) 
5340  185 
Goal "LeadsTo Lprg (Req n Int closed  (atFloor n  queueing)) \ 
186 
\ (moving Int Req n)"; 

187 
br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1; 

5357  188 
by (ensures_tac defs "req_down" 2); 
189 
by (ensures_tac defs "req_up" 1); 

5340  190 
qed "lift_2"; 
191 

192 

5357  193 
(** Towards lift_4 ***) 
5340  194 

5357  195 
Goal "[ x ~: A; y : A ] ==> x ~= y"; 
196 
by (Blast_tac 1); 

197 
qed "not_mem_distinct"; 

198 

199 
fun distinct_tac i = 

200 
dtac le_neq_implies_less i THEN 

201 
eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN 

202 
assume_tac i; 

203 

204 

205 
(*lem_lift_4_1 *) 

206 
Goal "0 < N ==> \ 

207 
\ LeadsTo Lprg \ 

208 
\ (moving Int Req n Int (metric n `` {N}) Int \ 

209 
\ {s. floor s ~: req s} Int {s. up s}) \ 

210 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

211 
by (cut_facts_tac [moving_up] 1); 

212 
by (ensures_tac defs "move_up" 1); 

213 
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) 

214 
be (leI RS le_anti_sym RS sym) 1; 

215 
by (eres_inst_tac [("P", "?x < metric n s")] notE 2); 

216 
by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3); 

217 
by (REPEAT_FIRST (etac rev_mp')); 

218 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); 

219 
by (distinct_tac 1); 

220 
by (auto_tac 

221 
(claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)] 

222 
addIs [diff_Suc_less_diff], 

223 
simpset())); 

224 
qed "E_thm12a"; 

225 

226 

227 
(*This rule helps eliminate occurrences of (floor s  1) *) 

228 
val less_floor_imp = read_instantiate_sg (sign_of thy) 

229 
[("n", "floor ?s")] less_eq_Suc_add RS exE; 

230 

231 
(*lem_lift_4_3 *) 

232 
Goal "0 < N ==> \ 

233 
\ LeadsTo Lprg \ 

234 
\ (moving Int Req n Int (metric n `` {N}) Int \ 

235 
\ {s. floor s ~: req s}  {s. up s}) \ 

236 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

237 
by (cut_facts_tac [moving_down] 1); 

238 
by (ensures_tac defs "move_down" 1); 

239 
by (ALLGOALS distinct_tac); 

240 
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); 

241 
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) 

242 
be (leI RS le_anti_sym RS sym) 1; 

243 
by (eres_inst_tac [("P", "?x < metric n s")] notE 2); 

244 
by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3); 

245 
by (REPEAT_FIRST (etac rev_mp')); 

246 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); 

247 
by (auto_tac 

248 
(claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)] 

249 
addIs [diff_le_Suc_diff, diff_less_Suc_diff], 

250 
simpset() addsimps [trans_le_add1])); 

251 
qed "E_thm12b"; 

252 

253 

254 
(*lift_4*) 

255 
Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n `` {N}) Int \ 

256 
\ {s. floor s ~: req s}) \ 

257 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

258 
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1; 

259 
by (etac E_thm12b 4); 

260 
by (etac E_thm12a 3); 

261 
by (rtac id_in_Acts 2); 

262 
by (Blast_tac 1); 

263 
qed "lift_4"; 

264 

265 

266 
(** towards lift_5 **) 

267 

268 
(*lem_lift_5_3*) 

269 
Goal "0<N \ 

270 
\ ==> LeadsTo Lprg (closed Int Req n Int (metric n `` {N}) Int goingup) \ 

271 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

272 
by (cut_facts_tac [bounded] 1); 

273 
by (ensures_tac defs "req_up" 1); 

274 
by (REPEAT_FIRST (etac rev_mp')); 

275 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); 

276 
by (auto_tac (claset() addIs [diff_Suc_less_diff], 

277 
simpset() addsimps [arith1, arith2])); 

278 
qed "E_thm16a"; 

279 

280 
(*arith1 comes from 

281 
1. !!s i. 

282 
[ n : req s; stop s; ~ open s; move s; floor s < i; i <= Max; 

283 
i : req s; ALL i. i < floor s > Min <= i > i ~: req s; 

284 
~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n; 

285 
Suc (floor s) < n; 0 < floor s  Min ] 

286 
==> n  Suc (floor s) < floor s  Min + (n  Min) 

287 
*) 

288 

289 
(*arith2 comes from 

290 
2. !!s i. 

291 
[ Min <= floor s; ... 

292 
n : req s; stop s; ~ open s; move s; floor s < i; i <= Max; 

293 
i : req s; ALL i. i < floor s > Min <= i > i ~: req s; 

294 
~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s); 

295 
Suc (floor s) < n; Min < n ] 

296 
==> n  Suc (floor s) < floor s  Min + (n  Min) 

297 
*) 

5340  298 

5357  299 
(*lem_lift_5_1 has ~goingup instead of goingdown*) 
300 
Goal "0<N ==> \ 

301 
\ LeadsTo Lprg (closed Int Req n Int (metric n `` {N}) Int goingdown) \ 

302 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

303 
by (cut_facts_tac [bounded] 1); 

304 
by (ensures_tac defs "req_down" 1); 

305 
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); 

306 
by (REPEAT_FIRST (etac rev_mp')); 

307 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); 

308 
by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], 

309 
simpset() addsimps [trans_le_add1, arith3, arith4])); 

310 
qed "E_thm16b"; 

311 

312 
(*arith3 comes from 

313 
1. !!s i x. 

314 
[ floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max; 

315 
~ open s; n : req s; move s; Min <= i; i : req s; 

316 
ALL ia. ia <= Max > Suc (i + x) < ia > ia ~: req s; 

317 
~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x; 

318 
Suc (i + x) < Max ] 

319 
==> i + x  n < Max  Suc (i + x) + (Max  n) 

320 
*) 

321 

322 
(*arith4 comes from 

323 
2. !!s i x. 

324 
[ floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max; 

325 
~ open s; n : req s; move s; Min <= i; i : req s; 

326 
ALL ia. ia <= Max > Suc (i + x) < ia > ia ~: req s; 

327 
~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x; 

328 
n < Max ] 

329 
==> i + x  n < Max  Suc (i + x) + (Max  n) 

330 
*) 

331 

332 

333 

334 
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, 

335 
i.e. the trivial disjunction, leading to an asymmetrical proof.*) 

336 
Goal "0<N ==> Req n Int (metric n ``{N}) <= goingup Un goingdown"; 

337 
by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1); 

338 
by (Blast_tac 1); 

339 
qed "E_thm16c"; 

340 

341 

342 
(*lift_5*) 

343 
Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n `` {N})) \ 

344 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

345 
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1; 

346 
by (etac E_thm16b 4); 

347 
by (etac E_thm16a 3); 

348 
by (rtac id_in_Acts 2); 

349 
bd E_thm16c 1; 

350 
by (Blast_tac 1); 

351 
qed "lift_5"; 

352 

353 

354 
(** towards lift_3 **) 

355 

356 
(*lemma used to prove lem_lift_3_1*) 

357 
Goal "[ metric n s = 0; Min <= floor s; floor s <= Max ] ==> floor s = n"; 

358 
be rev_mp 1; 

359 
by (asm_simp_tac (simpset() addsimps metric_simps) 1); 

360 
auto(); 

361 
qed "metric_eq_0D"; 

362 

363 
AddDs [metric_eq_0D]; 

364 

365 

366 
(*lem_lift_3_1*) 

367 
Goal "LeadsTo Lprg (moving Int Req n Int (metric n `` {0})) \ 

368 
\ (stopped Int atFloor n)"; 

369 
by (cut_facts_tac [bounded] 1); 

370 
by (ensures_tac defs "request_act" 1); 

371 
qed "E_thm11"; 

372 

373 
(*lem_lift_3_5*) 

374 
Goal "LeadsTo Lprg \ 

375 
\ (moving Int Req n Int (metric n `` {N}) Int {s. floor s : req s}) \ 

376 
\ (stopped Int Req n Int (metric n `` {N}) Int {s. floor s : req s})"; 

377 
by (ensures_tac defs "request_act" 1); 

378 
by (asm_simp_tac (simpset() addsimps metric_simps) 1); 

379 
qed "E_thm13"; 

380 

381 
(*lem_lift_3_6*) 

382 
Goal "0 < N ==> \ 

383 
\ LeadsTo Lprg \ 

384 
\ (stopped Int Req n Int (metric n `` {N}) Int {s. floor s : req s}) \ 

385 
\ (opened Int Req n Int (metric n `` {N}))"; 

386 
by (ensures_tac defs "open_act" 1); 

387 
by (REPEAT_FIRST (etac rev_mp')); 

388 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); 

389 
qed "E_thm14"; 

390 

391 
(*lem_lift_3_7*) 

392 
Goal "LeadsTo Lprg \ 

393 
\ (opened Int Req n Int (metric n `` {N})) \ 

394 
\ (closed Int Req n Int (metric n `` {N}))"; 

395 
by (ensures_tac defs "close_act" 1); 

396 
by (asm_simp_tac (simpset() addsimps metric_simps) 1); 

397 
qed "E_thm15"; 

398 

399 

400 
(** the final steps **) 

401 

402 
Goal "0 < N ==> \ 

403 
\ LeadsTo Lprg \ 

404 
\ (moving Int Req n Int (metric n `` {N}) Int {s. floor s : req s}) \ 

405 
\ (moving Int Req n Int (metric n `` lessThan N))"; 

406 
(*Blast_tac: PROOF FAILED*) 

407 
by (best_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] 

408 
addIs [LeadsTo_Trans]) 1); 

409 
qed "lift_3_Req"; 

410 

411 

412 
Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)"; 

413 
br (allI RS LessThan_induct) 1; 

414 
by (exhaust_tac "m" 1); 

415 
auto(); 

416 
br E_thm11 1; 

417 
br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1; 

418 
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1; 

419 
br lift_3_Req 4; 

420 
br lift_4 3; 

421 
auto(); 

422 
qed "lift_3"; 

423 

424 

425 
Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)"; 

5340  426 
br LeadsTo_Trans 1; 
427 
br (E_thm04 RS LeadsTo_Un) 2; 

428 
br LeadsTo_Un_post' 2; 

429 
br (E_thm01 RS LeadsTo_Trans_Un') 2; 

430 
br (lift_3 RS LeadsTo_Trans_Un') 2; 

431 
br (lift_2 RS LeadsTo_Trans_Un') 2; 

432 
br (E_thm03 RS LeadsTo_Trans_Un') 2; 

433 
br E_thm02 2; 

434 
br (open_move RS Invariant_LeadsToI) 1; 

435 
br (open_stop RS Invariant_LeadsToI) 1; 

436 
br subset_imp_LeadsTo 1; 

437 
by (rtac id_in_Acts 2); 

438 
bws defs; 

439 
by (Clarify_tac 1); 

440 
(*stops simplification from looping*) 

5357  441 
by (Full_simp_tac 1); 
5340  442 
by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1)); 
443 
qed "lift_1"; 

444 

5357  445 
Close_locale; 
5340  446 

447 