18 (*Simplification for records*) |
18 (*Simplification for records*) |
19 Addsimps (thms"state.update_defs"); |
19 Addsimps (thms"state.update_defs"); |
20 Addsimps [simp_of_set invFG_def]; |
20 Addsimps [simp_of_set invFG_def]; |
21 |
21 |
22 |
22 |
23 Goal "Invariant (Join prgF prgG) invFG"; |
23 Goal "Invariant (prgF Join prgG) invFG"; |
24 by (rtac InvariantI 1); |
24 by (rtac InvariantI 1); |
25 by (Force_tac 1); |
25 by (Force_tac 1); |
26 by (rtac (constrains_imp_Constrains RS StableI) 1); |
26 by (rtac (constrains_imp_Constrains RS StableI) 1); |
27 by (auto_tac (claset(), simpset() addsimps [constrains_Join])); |
27 by (auto_tac (claset(), simpset() addsimps [constrains_Join])); |
28 by (constrains_tac 2); |
28 by (constrains_tac 2); |
29 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset())); |
29 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset())); |
30 by (constrains_tac 1); |
30 by (constrains_tac 1); |
31 qed "invFG"; |
31 qed "invFG"; |
32 |
32 |
33 Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \ |
33 Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \ |
34 \ ({s. NF s = k} Int {s. BB s})"; |
34 \ ({s. NF s = k} Int {s. BB s})"; |
35 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
35 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
36 by (ensures_tac "cmdG" 2); |
36 by (ensures_tac "cmdG" 2); |
37 by (constrains_tac 1); |
37 by (constrains_tac 1); |
38 qed "lemma2_1"; |
38 qed "lemma2_1"; |
39 |
39 |
40 Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; |
40 Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; |
41 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
41 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
42 by (constrains_tac 2); |
42 by (constrains_tac 2); |
43 by (ensures_tac "cmdF" 1); |
43 by (ensures_tac "cmdF" 1); |
44 qed "lemma2_2"; |
44 qed "lemma2_2"; |
45 |
45 |
46 |
46 |
47 Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}"; |
47 Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}"; |
48 by (rtac LeadsTo_weaken_R 1); |
48 by (rtac LeadsTo_weaken_R 1); |
49 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] |
49 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] |
50 GreaterThan_bounded_induct 1); |
50 GreaterThan_bounded_induct 1); |
51 by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
51 by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
52 (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*) |
52 (*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*) |
53 by (rtac LeadsTo_Diff 1); |
53 by (rtac LeadsTo_Diff 1); |
54 by (rtac lemma2_2 2); |
54 by (rtac lemma2_2 2); |
55 by (rtac LeadsTo_Trans 1); |
55 by (rtac LeadsTo_Trans 1); |
56 by (rtac lemma2_2 2); |
56 by (rtac lemma2_2 2); |
57 by (rtac lemma2_1 1); |
57 by (rtac lemma2_1 1); |