69 |
69 |
70 (*** Progress under weak fairness ***) |
70 (*** Progress under weak fairness ***) |
71 |
71 |
72 Addsimps [atMost_Int_atLeast]; |
72 Addsimps [atMost_Int_atLeast]; |
73 |
73 |
74 Goal |
74 Goal "[| ALL m. constrains acts {m} (maxfg m); \ |
75 "[| ALL m. constrains acts {m} (maxfg m); \ |
|
76 \ ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \ |
75 \ ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \ |
77 \ n: common; id: acts |] \ |
76 \ n: common; id: acts |] \ |
78 \ ==> leadsTo acts (atMost n) common"; |
77 \ ==> leadsTo acts (atMost n) common"; |
79 by (rtac leadsTo_weaken_R 1); |
78 by (rtac leadsTo_weaken_R 1); |
80 by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1); |
79 by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1); |
81 by (ALLGOALS Asm_simp_tac); |
80 by (ALLGOALS Asm_simp_tac); |
82 by (rtac subset_refl 2); |
81 by (rtac subset_refl 2); |
83 by (blast_tac (claset() addDs [PSP_stable2] |
82 by (blast_tac (claset() addDs [psp_stable2] |
84 addIs [common_stable, leadsTo_weaken_R]) 1); |
83 addIs [common_stable, leadsTo_weaken_R]) 1); |
85 val lemma = result(); |
84 val lemma = result(); |
86 |
85 |
87 (*The "ALL m: Compl common" form echoes CMT6.*) |
86 (*The "ALL m: Compl common" form echoes CMT6.*) |
88 Goal |
87 Goal "[| ALL m. constrains acts {m} (maxfg m); \ |
89 "[| ALL m. constrains acts {m} (maxfg m); \ |
|
90 \ ALL m: Compl common. leadsTo acts {m} (greaterThan m); \ |
88 \ ALL m: Compl common. leadsTo acts {m} (greaterThan m); \ |
91 \ n: common; id: acts |] \ |
89 \ n: common; id: acts |] \ |
92 \ ==> leadsTo acts (atMost (LEAST n. n: common)) common"; |
90 \ ==> leadsTo acts (atMost (LEAST n. n: common)) common"; |
93 by (rtac lemma 1); |
91 by (rtac lemma 1); |
94 by (ALLGOALS Asm_simp_tac); |
92 by (ALLGOALS Asm_simp_tac); |