60 Addsimps [Acts_eq, Init_eq]; |
60 Addsimps [Acts_eq, Init_eq]; |
61 |
61 |
62 |
62 |
63 (** The notation of equality for type "program" **) |
63 (** The notation of equality for type "program" **) |
64 |
64 |
65 Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; |
65 |
66 by (subgoals_tac ["EX x. Rep_Program F = x", |
66 Goal "mk_program (Init F, Acts F) = F"; |
67 "EX x. Rep_Program G = x"] 1); |
67 by (cut_inst_tac [("x", "F")] Rep_Program 1); |
68 by (REPEAT (Blast_tac 2)); |
|
69 by (Clarify_tac 1); |
|
70 by (auto_tac (claset(), rep_ss)); |
68 by (auto_tac (claset(), rep_ss)); |
71 by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); |
69 by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); |
72 by (asm_full_simp_tac rep_ss 1); |
70 by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1); |
|
71 qed "surjective_mk_program"; |
|
72 |
|
73 Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; |
|
74 by (stac (surjective_mk_program RS sym) 1); |
|
75 by (stac (surjective_mk_program RS sym) 1 THEN Force_tac 1); |
73 qed "program_equalityI"; |
76 qed "program_equalityI"; |
74 |
77 |
75 val [major,minor] = |
78 val [major,minor] = |
76 Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P"; |
79 Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P"; |
77 by (rtac minor 1); |
80 by (rtac minor 1); |
78 by (auto_tac (claset(), simpset() addsimps [major])); |
81 by (auto_tac (claset(), simpset() addsimps [major])); |
79 qed "program_equalityE"; |
82 qed "program_equalityE"; |
80 |
83 |
|
84 Addsimps [surjective_mk_program]; |
|
85 |
81 |
86 |
82 (*** These rules allow "lazy" definition expansion |
87 (*** These rules allow "lazy" definition expansion |
83 They avoid expanding the full program, which is a large expression |
88 They avoid expanding the full program, which is a large expression |
84 ***) |
89 ***) |
85 |
90 |