equal
deleted
inserted
replaced
35 [("P", "(?x <= metric ?n ?s)")] rev_mp; |
35 [("P", "(?x <= metric ?n ?s)")] rev_mp; |
36 |
36 |
37 (*The order in which they are applied seems to be critical...*) |
37 (*The order in which they are applied seems to be critical...*) |
38 val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4]; |
38 val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4]; |
39 |
39 |
40 |
|
41 val metric_simps = [metric_def, vimage_def]; |
40 val metric_simps = [metric_def, vimage_def]; |
42 |
41 |
43 |
42 |
44 Addsimps [Lprg_def RS def_prg_Init]; |
43 Addsimps [Lprg_def RS def_prg_Init]; |
45 program_defs_ref := [Lprg_def]; |
44 program_defs_ref := [Lprg_def]; |
107 by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2); |
106 by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2); |
108 by (Force_tac 1); |
107 by (Force_tac 1); |
109 by (constrains_tac 1); |
108 by (constrains_tac 1); |
110 by (ALLGOALS Clarify_tac); |
109 by (ALLGOALS Clarify_tac); |
111 by (REPEAT_FIRST distinct_tac); |
110 by (REPEAT_FIRST distinct_tac); |
112 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]))); |
111 by Auto_tac; |
113 qed "bounded"; |
112 qed "bounded"; |
114 |
113 |
115 |
114 |
116 |
115 |
117 (*** Progress ***) |
116 (*** Progress ***) |
244 by (cut_facts_tac [bounded] 1); |
243 by (cut_facts_tac [bounded] 1); |
245 by (ensures_tac "req_up" 1); |
244 by (ensures_tac "req_up" 1); |
246 by Auto_tac; |
245 by Auto_tac; |
247 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
246 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
248 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
247 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
249 (** LEVEL 5 **) |
|
250 by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1); |
|
251 by (Blast_tac 1); |
248 by (Blast_tac 1); |
252 qed "E_thm16a"; |
249 qed "E_thm16a"; |
253 |
250 |
254 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
251 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
255 Goal "#0<N ==> \ |
252 Goal "#0<N ==> \ |
258 by (cut_facts_tac [bounded] 1); |
255 by (cut_facts_tac [bounded] 1); |
259 by (ensures_tac "req_down" 1); |
256 by (ensures_tac "req_down" 1); |
260 by Auto_tac; |
257 by Auto_tac; |
261 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
258 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
262 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
259 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
263 (** LEVEL 5 **) |
|
264 by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1); |
|
265 by (Blast_tac 1); |
260 by (Blast_tac 1); |
266 qed "E_thm16b"; |
261 qed "E_thm16b"; |
267 |
262 |
268 |
263 |
269 |
264 |