equal
deleted
inserted
replaced
15 val rep_ss = simpset() addsimps |
15 val rep_ss = simpset() addsimps |
16 [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, |
16 [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, |
17 Rep_Program_inverse, Abs_Program_inverse]; |
17 Rep_Program_inverse, Abs_Program_inverse]; |
18 |
18 |
19 |
19 |
20 Goal "Id: Acts prg"; |
20 Goal "Id: Acts F"; |
21 by (cut_inst_tac [("x", "prg")] Rep_Program 1); |
21 by (cut_inst_tac [("x", "F")] Rep_Program 1); |
22 by (auto_tac (claset(), rep_ss)); |
22 by (auto_tac (claset(), rep_ss)); |
23 qed "Id_in_Acts"; |
23 qed "Id_in_Acts"; |
24 AddIffs [Id_in_Acts]; |
24 AddIffs [Id_in_Acts]; |
25 |
25 |
26 |
26 |
33 qed "Acts_eq"; |
33 qed "Acts_eq"; |
34 |
34 |
35 Addsimps [Acts_eq, Init_eq]; |
35 Addsimps [Acts_eq, Init_eq]; |
36 |
36 |
37 |
37 |
38 Goal "[| Init prg = Init prg'; Acts prg = Acts prg' |] ==> prg = prg'"; |
38 Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; |
39 by (cut_inst_tac [("p", "Rep_Program prg")] surjective_pairing 1); |
39 by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1); |
40 by (auto_tac (claset(), rep_ss)); |
40 by (auto_tac (claset(), rep_ss)); |
41 by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1); |
41 by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1); |
42 by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1); |
42 by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1); |
43 qed "program_equalityI"; |
43 qed "program_equalityI"; |
44 |
44 |
45 |
45 |
46 (*** These three rules allow "lazy" definition expansion ***) |
46 (*** These three rules allow "lazy" definition expansion ***) |
47 |
47 |
48 val [rew] = goal thy |
48 val [rew] = goal thy |
49 "[| prg == mk_program (init,acts) |] \ |
49 "[| F == mk_program (init,acts) |] \ |
50 \ ==> Init prg = init & Acts prg = insert Id acts"; |
50 \ ==> Init F = init & Acts F = insert Id acts"; |
51 by (rewtac rew); |
51 by (rewtac rew); |
52 by Auto_tac; |
52 by Auto_tac; |
53 qed "def_prg_simps"; |
53 qed "def_prg_simps"; |
54 |
54 |
55 val [rew] = goal thy |
55 val [rew] = goal thy |
69 fun simp_of_set def = def RS def_set_simp; |
69 fun simp_of_set def = def RS def_set_simp; |
70 |
70 |
71 |
71 |
72 (*** traces and reachable ***) |
72 (*** traces and reachable ***) |
73 |
73 |
74 Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}"; |
74 Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"; |
75 by Safe_tac; |
75 by Safe_tac; |
76 by (etac traces.induct 2); |
76 by (etac traces.induct 2); |
77 by (etac reachable.induct 1); |
77 by (etac reachable.induct 1); |
78 by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs)))); |
78 by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs))); |
79 qed "reachable_equiv_traces"; |
79 qed "reachable_equiv_traces"; |
80 |
80 |
81 Goal "acts <= Acts prg ==> stable acts (reachable prg)"; |
81 Goal "Init F <= reachable F"; |
82 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
82 by (blast_tac (claset() addIs reachable.intrs) 1); |
|
83 qed "Init_subset_reachable"; |
|
84 |
|
85 Goal "acts <= Acts F ==> stable acts (reachable F)"; |
|
86 by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); |
83 qed "stable_reachable"; |
87 qed "stable_reachable"; |