14 by (etac traces.induct 2); |
14 by (etac traces.induct 2); |
15 be reachable.induct 1; |
15 be reachable.induct 1; |
16 by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs)))); |
16 by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs)))); |
17 qed "reachable_equiv_traces"; |
17 qed "reachable_equiv_traces"; |
18 |
18 |
19 Goal "stable (Acts prg) (reachable prg)"; |
19 Goal "acts <= Acts prg ==> stable acts (reachable prg)"; |
20 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
20 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
21 qed "stable_reachable"; |
21 qed "stable_reachable"; |
22 |
22 |
23 (*The set of all reachable states is an invariant...*) |
|
24 Goal "invariant prg (reachable prg)"; |
|
25 by (simp_tac (simpset() addsimps [invariant_def]) 1); |
|
26 by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1); |
|
27 qed "invariant_reachable"; |
|
28 |
|
29 (*...in fact the strongest invariant!*) |
|
30 Goal "invariant prg A ==> reachable prg <= A"; |
|
31 by (full_simp_tac |
|
32 (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); |
|
33 by (rtac subsetI 1); |
|
34 by (etac reachable.induct 1); |
|
35 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
|
36 qed "invariant_includes_reachable"; |
|
37 |
|
38 |
|
39 (** Natural deduction rules for "invariant prg A" **) |
|
40 |
|
41 Goal "[| (Init prg)<=A; stable (Acts prg) A |] ==> invariant prg A"; |
|
42 by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
43 qed "invariantI"; |
|
44 |
|
45 Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A"; |
|
46 by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
47 qed "invariantD"; |
|
48 |
|
49 bind_thm ("invariantE", invariantD RS conjE); |
|
50 |
|
51 |
|
52 (** Conjoining invariants **) |
|
53 |
|
54 Goal "[| invariant prg A; invariant prg B |] \ |
|
55 \ ==> invariant prg (A Int B)"; |
|
56 by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1); |
|
57 by Auto_tac; |
|
58 qed "invariant_Int"; |
|
59 |
|
60 (*Delete the nearest invariance assumption (which will be the second one |
|
61 used by invariant_Int) *) |
|
62 val invariant_thin = |
|
63 read_instantiate_sg (sign_of thy) |
|
64 [("V", "invariant ?Prg ?A")] thin_rl; |
|
65 |
|
66 (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) |
|
67 val invariant_Int_tac = dtac invariant_Int THEN' |
|
68 assume_tac THEN' |
|
69 etac invariant_thin; |
|
70 |
|
71 (*Combines two invariance THEOREMS into one.*) |
|
72 val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int); |
|
73 |
|
74 |
|