equal
deleted
inserted
replaced
6 Definitions of |
6 Definitions of |
7 * traces: the possible execution traces |
7 * traces: the possible execution traces |
8 * reachable: the set of reachable states |
8 * reachable: the set of reachable states |
9 |
9 |
10 *) |
10 *) |
11 |
|
12 open Traces; |
|
13 |
|
14 |
11 |
15 (**** |
12 (**** |
16 Now simulate the inductive definition (illegal due to paired arguments) |
13 Now simulate the inductive definition (illegal due to paired arguments) |
17 |
14 |
18 inductive "reachable(Init,Acts)" |
15 inductive "reachable(Init,Acts)" |
36 |
33 |
37 Goal "[| act: Acts; s : reachable(Init,Acts) |] \ |
34 Goal "[| act: Acts; s : reachable(Init,Acts) |] \ |
38 \ ==> (s,s'): act --> s' : reachable(Init,Acts)"; |
35 \ ==> (s,s'): act --> s' : reachable(Init,Acts)"; |
39 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); |
36 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); |
40 by (etac exE 1); |
37 by (etac exE 1); |
41 be traces.induct 1; |
38 by (etac traces.induct 1); |
42 by (ALLGOALS Asm_simp_tac); |
39 by (ALLGOALS Asm_simp_tac); |
43 by (ALLGOALS (blast_tac (claset() addIs traces.intrs))); |
40 by (ALLGOALS (blast_tac (claset() addIs traces.intrs))); |
44 qed_spec_mp "reachable_Acts"; |
41 qed_spec_mp "reachable_Acts"; |
45 |
42 |
46 |
43 |
52 \ [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |] \ |
49 \ [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |] \ |
53 \ ==> P s' |] \ |
50 \ ==> P s' |] \ |
54 \ ==> P za"; |
51 \ ==> P za"; |
55 by (cut_facts_tac [major] 1); |
52 by (cut_facts_tac [major] 1); |
56 by Auto_tac; |
53 by Auto_tac; |
57 be traces.induct 1; |
54 by (etac traces.induct 1); |
58 by (ALLGOALS (blast_tac (claset() addIs prems))); |
55 by (ALLGOALS (blast_tac (claset() addIs prems))); |
59 qed "reachable_induct"; |
56 qed "reachable_induct"; |
60 |
57 |
61 structure reachable = |
58 structure reachable = |
62 struct |
59 struct |
69 |
66 |
70 (*The strongest invariant is the set of all reachable states!*) |
67 (*The strongest invariant is the set of all reachable states!*) |
71 Goalw [stable_def, constrains_def] |
68 Goalw [stable_def, constrains_def] |
72 "[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A"; |
69 "[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A"; |
73 by (rtac subsetI 1); |
70 by (rtac subsetI 1); |
74 be reachable.induct 1; |
71 by (etac reachable.induct 1); |
75 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
72 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
76 qed "strongest_invariant"; |
73 qed "strongest_invariant"; |
77 |
74 |
78 Goal "stable Acts (reachable(Init,Acts))"; |
75 Goal "stable Acts (reachable(Init,Acts))"; |
79 by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI] |
76 by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI] |