53 by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); |
53 by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); |
54 by(fast_tac (HOL_cs addEs [wp_mono]) 1); |
54 by(fast_tac (HOL_cs addEs [wp_mono]) 1); |
55 qed_spec_mp "vc_mono"; |
55 qed_spec_mp "vc_mono"; |
56 |
56 |
57 goal VC.thy |
57 goal VC.thy |
58 "!P c Q. |- {P}c{Q} --> \ |
58 "!!P c Q. |- {P}c{Q} ==> \ |
59 \ (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))"; |
59 \ (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))"; |
60 by (rtac hoare.mutual_induct 1); |
60 by (etac hoare.induct 1); |
61 by(res_inst_tac [("x","Askip")] exI 1); |
61 by(res_inst_tac [("x","Askip")] exI 1); |
62 by(Simp_tac 1); |
62 by(Simp_tac 1); |
63 by(res_inst_tac [("x","Aass x a")] exI 1); |
63 by(res_inst_tac [("x","Aass x a")] exI 1); |
64 by(Simp_tac 1); |
64 by(Simp_tac 1); |
65 by(SELECT_GOAL(safe_tac HOL_cs)1); |
65 by(SELECT_GOAL(safe_tac HOL_cs)1); |
68 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
68 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
69 by(SELECT_GOAL(safe_tac HOL_cs)1); |
69 by(SELECT_GOAL(safe_tac HOL_cs)1); |
70 by(res_inst_tac [("x","Aif b ac aca")] exI 1); |
70 by(res_inst_tac [("x","Aif b ac aca")] exI 1); |
71 by(Asm_simp_tac 1); |
71 by(Asm_simp_tac 1); |
72 by(SELECT_GOAL(safe_tac HOL_cs)1); |
72 by(SELECT_GOAL(safe_tac HOL_cs)1); |
73 by(res_inst_tac [("x","Awhile b P ac")] exI 1); |
73 by(res_inst_tac [("x","Awhile b Pa ac")] exI 1); |
74 by(Asm_simp_tac 1); |
74 by(Asm_simp_tac 1); |
75 by(SELECT_GOAL(safe_tac HOL_cs)1); |
75 by (safe_tac HOL_cs); |
76 by(res_inst_tac [("x","ac")] exI 1); |
76 by(res_inst_tac [("x","ac")] exI 1); |
77 by(Asm_simp_tac 1); |
77 by(Asm_simp_tac 1); |
78 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
78 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
79 qed_spec_mp "vc_complete"; |
79 qed "vc_complete"; |
80 |
80 |
81 goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)"; |
81 goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)"; |
82 by(acom.induct_tac "c" 1); |
82 by(acom.induct_tac "c" 1); |
83 by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); |
83 by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); |
84 qed "vcwp_vc_wp"; |
84 qed "vcwp_vc_wp"; |