equal
deleted
inserted
replaced
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 val [major,minor] = |
|
46 Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P"; |
|
47 by (rtac minor 1); |
|
48 by (auto_tac (claset(), simpset() addsimps [major])); |
|
49 qed "program_equalityE"; |
45 |
50 |
46 (*** These rules allow "lazy" definition expansion ***) |
51 (*** These rules allow "lazy" definition expansion ***) |
47 |
52 |
48 (*The program is not expanded, but its Init is*) |
53 (*The program is not expanded, but its Init is*) |
49 val [rew] = goal thy |
54 val [rew] = goal thy |