30 by (constrains_tac [prgG_def,cmdG_def] 2); |
30 by (constrains_tac [prgG_def,cmdG_def] 2); |
31 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset())); |
31 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset())); |
32 by (constrains_tac [prgF_def,cmdF_def] 1); |
32 by (constrains_tac [prgF_def,cmdF_def] 1); |
33 qed "invFG"; |
33 qed "invFG"; |
34 |
34 |
35 Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}"; |
35 Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \ |
|
36 \ ({s. NF s = k} Int {s. BB s})"; |
36 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
37 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
37 by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2); |
38 by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2); |
38 by (constrains_tac [prgF_def,cmdF_def] 1); |
39 by (constrains_tac [prgF_def,cmdF_def] 1); |
39 qed "lemma2_1"; |
40 qed "lemma2_1"; |
40 |
41 |
41 Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}"; |
42 Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; |
42 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
43 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
43 by (constrains_tac [prgG_def,cmdG_def] 2); |
44 by (constrains_tac [prgG_def,cmdG_def] 2); |
44 by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1); |
45 by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1); |
45 qed "lemma2_2"; |
46 qed "lemma2_2"; |
46 |
47 |