equal
deleted
inserted
replaced
28 AddIffs [[subset_UNIV, finite_graph] MRS finite_subset]; |
28 AddIffs [[subset_UNIV, finite_graph] MRS finite_subset]; |
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 (rtac AlwaysI 1); |
33 by (always_tac 1); |
34 by Auto_tac; (*for the initial state; proof of stability remains*) |
|
35 by (constrains_tac 1); |
|
36 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); |
34 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); |
37 qed "reach_invariant"; |
35 qed "reach_invariant"; |
38 |
36 |
39 |
37 |
40 (*** Fixedpoint ***) |
38 (*** Fixedpoint ***) |