author  paulson 
Fri, 07 May 1999 10:50:28 +0200  
changeset 6614  2d47dee036b5 
parent 6570  a7d7985050a9 
child 6676  62d1e642da30 
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 

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 blowup*) 
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 

5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset

35 
(*The order in which they are applied seems to be critical...*) 
5563  36 
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

37 

6139  38 
val metric_simps = [metric_def, vimage_def]; 
5563  39 

5340  40 

5648  41 
Addsimps [Lprg_def RS def_prg_Init]; 
42 
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

43 

566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset

44 
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

45 
[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

46 
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

47 
button_press_def]); 
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset

48 

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

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

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

51 

5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset

52 
Addsimps (map simp_of_set always_defs); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

53 

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

54 

5583  55 
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; 
6614  56 
(* [ Lprg: B LeadsTo C; Lprg: A LeadsTo B ] ==> Lprg: (A Un B) LeadsTo C *) 
5357  57 

58 

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

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

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

61 

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

62 
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

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

64 

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

66 

5320  67 

6570  68 
Goal "Lprg : Always open_stop"; 
69 
by (rtac AlwaysI 1); 

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

70 
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

71 
by (constrains_tac 1); 
5277
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 

6570  74 
Goal "Lprg : Always stop_floor"; 
75 
by (rtac AlwaysI 1); 

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

76 
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

77 
by (constrains_tac 1); 
5277
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*) 
6570  81 
Goal "Lprg : Always open_move"; 
82 
by (rtac AlwaysI 1); 

83 
by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2); 

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

84 
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

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

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

87 

6570  88 
Goal "Lprg : Always moving_up"; 
89 
by (rtac AlwaysI 1); 

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

90 
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

91 
by (constrains_tac 1); 
5563  92 
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

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

94 

6570  95 
Goal "Lprg : Always moving_down"; 
96 
by (rtac AlwaysI 1); 

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

97 
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

98 
by (constrains_tac 1); 
5563  99 
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

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

101 

6570  102 
Goal "Lprg : Always bounded"; 
103 
by (rtac AlwaysI 1); 

104 
by (rtac (Always_Int_rule [moving_up, moving_down] RS Always_StableI) 2); 

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

105 
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

106 
by (constrains_tac 1); 
5563  107 
by (ALLGOALS Clarify_tac); 
108 
by (REPEAT_FIRST distinct_tac); 

6161  109 
by Auto_tac; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

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

111 

5320  112 

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

113 

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

115 

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

116 

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

119 

5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset

120 
Addsimps (map simp_of_set abbrev_defs); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff
changeset

121 

5340  122 

123 
(** 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

124 

5357  125 
(** Lift_1 **) 
126 

6536  127 
Goal "Lprg : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"; 
5340  128 
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

129 
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

130 
qed "E_thm01"; (*lem_lift_1_5*) 
5340  131 

6536  132 
Goal "Lprg : (Req n Int stopped  atFloor n) LeadsTo \ 
6139  133 
\ (Req n Int opened  atFloor n)"; 
5340  134 
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

135 
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

136 
qed "E_thm02"; (*lem_lift_1_1*) 
5340  137 

6536  138 
Goal "Lprg : (Req n Int opened  atFloor n) LeadsTo \ 
6139  139 
\ (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

140 
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

141 
qed "E_thm03"; (*lem_lift_1_2*) 
5340  142 

6536  143 
Goal "Lprg : (Req n Int closed Int (atFloor n  queueing)) \ 
144 
\ 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

145 
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

146 
qed "E_thm04"; (*lem_lift_1_7*) 
5340  147 

148 

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

151 
Open_locale "floor"; 

152 

5357  153 
val Min_le_n = thm "Min_le_n"; 
154 
val n_le_Max = thm "n_le_Max"; 

155 

156 
AddIffs [Min_le_n, n_le_Max]; 

5340  157 

5563  158 
val le_MinD = Min_le_n RS zle_anti_sym; 
159 
val Max_leD = n_le_Max RSN (2,zle_anti_sym); 

5357  160 

5563  161 
AddSDs [le_MinD, zleI RS le_MinD, 
162 
Max_leD, zleI RS Max_leD]; 

5357  163 

164 
(*lem_lift_2_0 

165 
NOT an ensures property, but a mere inclusion; 

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

6536  167 
Goal "Lprg : (Req n Int closed  (atFloor n  queueing)) \ 
168 
\ LeadsTo ((closed Int goingup Int Req n) Un \ 

6139  169 
\ (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

170 
by (rtac subset_imp_LeadsTo 1); 
5563  171 
by (auto_tac (claset() addSEs [int_neqE], simpset())); 
5340  172 
qed "E_thm05c"; 
173 

5357  174 
(*lift_2*) 
6536  175 
Goal "Lprg : (Req n Int closed  (atFloor n  queueing)) \ 
176 
\ 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

177 
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

178 
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

179 
by (ensures_tac "req_up" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

180 
by Auto_tac; 
5340  181 
qed "lift_2"; 
182 

183 

5357  184 
(** Towards lift_4 ***) 
5563  185 

5357  186 

187 
(*lem_lift_4_1 *) 

5563  188 
Goal "#0 < N ==> \ 
6536  189 
\ Lprg : (moving Int Req n Int {s. metric n s = N} Int \ 
190 
\ {s. floor s ~: req s} Int {s. up s}) \ 

191 
\ LeadsTo \ 

6139  192 
\ (moving Int Req n Int {s. metric n s < N})"; 
5357  193 
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

194 
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

195 
by Safe_tac; 
5357  196 
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) 
5563  197 
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

198 
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

199 
by (REPEAT_FIRST distinct_tac); 
5563  200 
(** LEVEL 6 **) 
5583  201 
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
202 
[zle_def] @ metric_simps @ zcompare_rls))); 

5357  203 
qed "E_thm12a"; 
204 

205 

206 

207 
(*lem_lift_4_3 *) 

5563  208 
Goal "#0 < N ==> \ 
6536  209 
\ Lprg : (moving Int Req n Int {s. metric n s = N} Int \ 
210 
\ {s. floor s ~: req s}  {s. up s}) \ 

211 
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; 

5357  212 
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

213 
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

214 
by Safe_tac; 
5357  215 
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) 
5563  216 
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

217 
by (REPEAT_FIRST (eresolve_tac mov_metrics)); 
5563  218 
by (REPEAT_FIRST distinct_tac); 
219 
(** LEVEL 6 **) 

6139  220 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); 
5357  221 
qed "E_thm12b"; 
222 

223 
(*lift_4*) 

6536  224 
Goal "#0<N ==> Lprg : (moving Int Req n Int {s. metric n s = N} Int \ 
225 
\ {s. floor s ~: req s}) LeadsTo \ 

5563  226 
\ (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

227 
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); 
5583  228 
by (etac E_thm12b 3); 
229 
by (etac E_thm12a 2); 

5357  230 
by (Blast_tac 1); 
231 
qed "lift_4"; 

232 

233 

234 
(** towards lift_5 **) 

235 

236 
(*lem_lift_5_3*) 

5563  237 
Goal "#0<N \ 
6536  238 
\ ==> Lprg : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \ 
5563  239 
\ (moving Int Req n Int {s. metric n s < N})"; 
5357  240 
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

241 
by (ensures_tac "req_up" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

242 
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

243 
by (REPEAT_FIRST (eresolve_tac mov_metrics)); 
6139  244 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); 
6128  245 
by (Blast_tac 1); 
5357  246 
qed "E_thm16a"; 
247 

248 
(*lem_lift_5_1 has ~goingup instead of goingdown*) 

5563  249 
Goal "#0<N ==> \ 
6536  250 
\ Lprg : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ 
5563  251 
\ (moving Int Req n Int {s. metric n s < N})"; 
5357  252 
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

253 
by (ensures_tac "req_down" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

254 
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

255 
by (REPEAT_FIRST (eresolve_tac mov_metrics)); 
6139  256 
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); 
6128  257 
by (Blast_tac 1); 
5357  258 
qed "E_thm16b"; 
259 

260 

261 

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

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

5563  264 
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"; 
265 
by (asm_simp_tac (simpset() addsimps metric_simps) 1); 

5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset

266 
by (force_tac (claset() delrules [impCE] addEs [impCE], 
6139  267 
simpset() addsimps conj_comms) 1); 
5357  268 
qed "E_thm16c"; 
269 

270 

271 
(*lift_5*) 

6536  272 
Goal "#0<N ==> Lprg : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ 
5563  273 
\ (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

274 
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); 
5583  275 
by (etac E_thm16b 3); 
276 
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

277 
by (dtac E_thm16c 1); 
5357  278 
by (Blast_tac 1); 
279 
qed "lift_5"; 

280 

281 

282 
(** towards lift_3 **) 

283 

284 
(*lemma used to prove lem_lift_3_1*) 

5563  285 
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

286 
by (etac rev_mp 1); 
5563  287 
(*force simplification of "metric..." while in conclusion part*) 
288 
by (asm_simp_tac (simpset() addsimps metric_simps) 1); 

5357  289 
qed "metric_eq_0D"; 
290 

291 
AddDs [metric_eq_0D]; 

292 

293 

294 
(*lem_lift_3_1*) 

6536  295 
Goal "Lprg : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \ 
5357  296 
\ (stopped Int atFloor n)"; 
297 
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

298 
by (ensures_tac "request_act" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

299 
by Auto_tac; 
5357  300 
qed "E_thm11"; 
301 

302 
(*lem_lift_3_5*) 

6536  303 
Goal 
304 
"Lprg : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ 

305 
\ 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

306 
by (ensures_tac "request_act" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

307 
by (auto_tac (claset(), simpset() addsimps metric_simps)); 
5357  308 
qed "E_thm13"; 
309 

310 
(*lem_lift_3_6*) 

5563  311 
Goal "#0 < N ==> \ 
6536  312 
\ Lprg : \ 
5563  313 
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ 
6536  314 
\ 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

315 
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

316 
by (REPEAT_FIRST (eresolve_tac mov_metrics)); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

317 
by (auto_tac (claset(), simpset() addsimps metric_simps)); 
5357  318 
qed "E_thm14"; 
319 

320 
(*lem_lift_3_7*) 

6536  321 
Goal "Lprg : (opened Int Req n Int {s. metric n s = N}) \ 
322 
\ 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

323 
by (ensures_tac "close_act" 1); 
5424
771a68a468cc
modified proofs for new constrains_tac and ensures_tac
paulson
parents:
5410
diff
changeset

324 
by (auto_tac (claset(), simpset() addsimps metric_simps)); 
5357  325 
qed "E_thm15"; 
326 

327 

328 
(** the final steps **) 

329 

5563  330 
Goal "#0 < N ==> \ 
6536  331 
\ Lprg : \ 
5563  332 
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ 
6536  333 
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; 
5479  334 
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] 
335 
addIs [LeadsTo_Trans]) 1); 

5357  336 
qed "lift_3_Req"; 
337 

338 

5563  339 

340 
(*Now we observe that our integer metric is really a natural number*) 

6570  341 
Goal "Lprg : Always {s. #0 <= metric n s}"; 
342 
by (rtac (bounded RS Always_weaken) 1); 

5563  343 
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1); 
344 
by (auto_tac (claset(), 

345 
simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd])); 

346 
by (REPEAT_FIRST (etac ssubst)); 

5583  347 
by (auto_tac (claset(), simpset() addsimps [zadd_int])); 
6570  348 
qed "Always_nonneg"; 
5563  349 

6570  350 
val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken; 
5563  351 

6536  352 
Goal "Lprg : (moving Int Req n) LeadsTo (stopped Int atFloor n)"; 
6570  353 
by (rtac (Always_nonneg RS integ_0_le_induct) 1); 
5563  354 
by (case_tac "#0 < z" 1); 
355 
(*If z <= #0 then actually z = #0*) 

356 
by (fold_tac [zle_def]); 

357 
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

358 
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

359 
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); 
5583  360 
by (rtac lift_3_Req 3); 
361 
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

362 
by Auto_tac; 
5357  363 
qed "lift_3"; 
364 

365 

6536  366 
Goal "Lprg : (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

367 
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

368 
by (rtac (E_thm04 RS LeadsTo_Un) 2); 
5583  369 
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

370 
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

371 
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

372 
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

373 
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

374 
by (rtac E_thm02 2); 
6570  375 
by (rtac (open_move RS Always_LeadsToI) 1); 
376 
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

377 
by (rtac subset_imp_LeadsTo 1); 
5340  378 
by (Clarify_tac 1); 
5484  379 
(*The case split is not essential but makes Blast_tac much faster. 
380 
Must also be careful to prevent simplification from looping*) 

381 
by (case_tac "open x" 1); 

382 
by (ALLGOALS (rotate_tac ~1)); 

383 
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

384 
by (Blast_tac 1); 
5340  385 
qed "lift_1"; 
386 

6024  387 
Close_locale "floor"; 