equal
deleted
inserted
replaced
243 |
243 |
244 Goal "drop_prog i F = project UNIV (lift_map i) F"; |
244 Goal "drop_prog i F = project UNIV (lift_map i) F"; |
245 by (rtac program_equalityI 1); |
245 by (rtac program_equalityI 1); |
246 by (simp_tac (simpset() addsimps [drop_set_correct]) 1); |
246 by (simp_tac (simpset() addsimps [drop_set_correct]) 1); |
247 by (simp_tac (simpset() |
247 by (simp_tac (simpset() |
248 addsimps [lift_export Acts_project, |
248 addsimps [Acts_project, drop_act_correct]) 1); |
249 drop_act_correct]) 1); |
249 by (rtac (insert_absorb RS sym) 1); |
|
250 by (rtac (Id_in_Acts RSN (2,image_eqI)) 1); |
|
251 by (rtac (project_set_UNIV RS lift_export project_act_Id RS sym) 1); |
250 qed "drop_prog_correct"; |
252 qed "drop_prog_correct"; |
251 |
253 |
252 |
254 |
253 (*** More Lemmas ***) |
255 (*** More Lemmas ***) |
254 |
256 |