10 *) |
10 *) |
11 |
11 |
12 Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}"; |
12 Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}"; |
13 by Safe_tac; |
13 by Safe_tac; |
14 by (etac traces.induct 2); |
14 by (etac traces.induct 2); |
15 be reachable.induct 1; |
15 by (etac 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 "acts <= Acts prg ==> stable acts (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 Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)"; |
23 Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)"; |
24 auto(); |
24 by Auto_tac; |
25 qed "Acts_eq"; |
25 qed "Acts_eq"; |
26 |
26 |
27 Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)"; |
27 Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)"; |
28 auto(); |
28 by Auto_tac; |
29 qed "Init_eq"; |
29 qed "Init_eq"; |
30 |
30 |
31 AddIffs [Acts_eq, Init_eq]; |
31 AddIffs [Acts_eq, Init_eq]; |
|
32 |
|
33 |
|
34 (*** These three rules allow "lazy" definition expansion ***) |
|
35 |
|
36 val [rew] = goal thy |
|
37 "[| prg == (|Init=init, Acts=acts|) |] \ |
|
38 \ ==> Init prg = init & Acts prg = acts"; |
|
39 by (rewtac rew); |
|
40 by Auto_tac; |
|
41 qed "def_prg_simps"; |
|
42 |
|
43 val [rew] = goal thy |
|
44 "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; |
|
45 by (rewtac rew); |
|
46 by Auto_tac; |
|
47 qed "def_act_simp"; |
|
48 |
|
49 fun simp_of_act def = def RS def_act_simp; |
|
50 |
|
51 val [rew] = goal thy |
|
52 "[| A == B |] ==> (x : A) = (x : B)"; |
|
53 by (rewtac rew); |
|
54 by Auto_tac; |
|
55 qed "def_set_simp"; |
|
56 |
|
57 fun simp_of_set def = def RS def_set_simp; |
|
58 |