62 val intrs = [reachable_Init, reachable_Acts] |
62 val intrs = [reachable_Init, reachable_Acts] |
63 val induct = reachable_induct |
63 val induct = reachable_induct |
64 end; |
64 end; |
65 |
65 |
66 |
66 |
67 (*The strongest invariant is the set of all reachable states!*) |
67 |
68 Goalw [stable_def, constrains_def] |
68 Goal "stable Acts (reachable(Init,Acts))"; |
69 "[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A"; |
69 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
|
70 qed "stable_reachable"; |
|
71 |
|
72 (*The set of all reachable states is an invariant...*) |
|
73 Goal "invariant (Init,Acts) (reachable(Init,Acts))"; |
|
74 by (simp_tac (simpset() addsimps [invariant_def]) 1); |
|
75 by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1); |
|
76 qed "invariant_reachable"; |
|
77 |
|
78 (*...in fact the strongest invariant!*) |
|
79 Goal "invariant (Init,Acts) A ==> reachable(Init,Acts) <= A"; |
|
80 by (full_simp_tac |
|
81 (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); |
70 by (rtac subsetI 1); |
82 by (rtac subsetI 1); |
71 by (etac reachable.induct 1); |
83 by (etac reachable.induct 1); |
72 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
84 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
73 qed "strongest_invariant"; |
85 qed "invariant_includes_reachable"; |
74 |
86 |
75 Goal "stable Acts (reachable(Init,Acts))"; |
87 (*If "A" includes the initial states and is stable then "A" is invariant. |
76 by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI] |
88 Result is trivial from the definition, but it is handy.*) |
77 addIs reachable.intrs) 1)); |
89 Goal "[| Init<=A; stable Acts A |] ==> invariant (Init,Acts) A"; |
78 qed "stable_reachable"; |
90 by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
91 qed "invariantI"; |
|
92 |
|
93 |
|
94 (** Conjoining invariants **) |
|
95 |
|
96 Goal "[| invariant (Init,Acts) A; invariant (Init,Acts) B |] \ |
|
97 \ ==> invariant (Init,Acts) (A Int B)"; |
|
98 by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1); |
|
99 by Auto_tac; |
|
100 qed "invariant_Int"; |
|
101 |
|
102 (*Delete the nearest invariance assumption (which will be the second one |
|
103 used by invariant_Int) *) |
|
104 val invariant_thin = |
|
105 read_instantiate_sg (sign_of thy) |
|
106 [("V", "invariant ?Prg ?A")] thin_rl; |
|
107 |
|
108 (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) |
|
109 val invariant_Int_tac = dtac invariant_Int THEN' |
|
110 assume_tac THEN' |
|
111 etac invariant_thin; |
|
112 |
|
113 (*Combines two invariance THEOREMS into one.*) |
|
114 val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int); |
|
115 |
|
116 |