29 |
29 |
30 Addsimps [simp_of_set reach_invariant_def]; |
30 Addsimps [simp_of_set reach_invariant_def]; |
31 |
31 |
32 Goal "Rprg : Always reach_invariant"; |
32 Goal "Rprg : Always reach_invariant"; |
33 by (always_tac 1); |
33 by (always_tac 1); |
34 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); |
34 by (blast_tac (claset() addIs rtranclIs) 1); |
35 qed "reach_invariant"; |
35 qed "reach_invariant"; |
36 |
36 |
37 |
37 |
38 (*** Fixedpoint ***) |
38 (*** Fixedpoint ***) |
39 |
39 |
40 (*If it reaches a fixedpoint, it has found a solution*) |
40 (*If it reaches a fixedpoint, it has found a solution*) |
41 Goalw [fixedpoint_def] |
41 Goalw [fixedpoint_def] |
42 "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"; |
42 "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"; |
43 by (rtac equalityI 1); |
43 by (rtac equalityI 1); |
44 by (auto_tac (claset() addSIs [ext], simpset())); |
44 by (auto_tac (claset() addSIs [ext], simpset())); |
45 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2); |
45 by (blast_tac (claset() addIs rtranclIs) 2); |
46 by (etac rtrancl_induct 1); |
46 by (etac rtrancl_induct 1); |
47 by Auto_tac; |
47 by Auto_tac; |
48 qed "fixedpoint_invariant_correct"; |
48 qed "fixedpoint_invariant_correct"; |
49 |
49 |
50 Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] |
50 Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] |