equal
deleted
inserted
replaced
33 by (rtac subsetI 1); |
33 by (rtac subsetI 1); |
34 by (etac reachable.induct 1); |
34 by (etac reachable.induct 1); |
35 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
35 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
36 qed "invariant_includes_reachable"; |
36 qed "invariant_includes_reachable"; |
37 |
37 |
38 (*If "A" includes the initial states and is stable then "A" is invariant. |
38 |
39 Result is trivial from the definition, but it is handy.*) |
39 (** Natural deduction rules for "invariant prg A" **) |
|
40 |
40 Goal "[| (Init prg)<=A; stable (Acts prg) A |] ==> invariant prg A"; |
41 Goal "[| (Init prg)<=A; stable (Acts prg) A |] ==> invariant prg A"; |
41 by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
42 by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
42 qed "invariantI"; |
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); |
43 |
50 |
44 |
51 |
45 (** Conjoining invariants **) |
52 (** Conjoining invariants **) |
46 |
53 |
47 Goal "[| invariant prg A; invariant prg B |] \ |
54 Goal "[| invariant prg A; invariant prg B |] \ |