equal
deleted
inserted
replaced
56 |
56 |
57 Goal "Domain (Restrict A r) = A Int Domain r"; |
57 Goal "Domain (Restrict A r) = A Int Domain r"; |
58 by (Blast_tac 1); |
58 by (Blast_tac 1); |
59 qed "Domain_Restrict"; |
59 qed "Domain_Restrict"; |
60 |
60 |
61 Goal "(Restrict A r) ^^ B = r ^^ (A Int B)"; |
61 Goal "(Restrict A r) ``` B = r ``` (A Int B)"; |
62 by (Blast_tac 1); |
62 by (Blast_tac 1); |
63 qed "Image_Restrict"; |
63 qed "Image_Restrict"; |
64 |
64 |
65 Addsimps [Domain_Restrict, Image_Restrict]; |
65 Addsimps [Domain_Restrict, Image_Restrict]; |
66 |
66 |
306 by (rtac inj_on_inverseI 1); |
306 by (rtac inj_on_inverseI 1); |
307 by (rtac extend_act_inverse 1); |
307 by (rtac extend_act_inverse 1); |
308 qed "inj_extend_act"; |
308 qed "inj_extend_act"; |
309 |
309 |
310 Goalw [extend_set_def, extend_act_def] |
310 Goalw [extend_set_def, extend_act_def] |
311 "extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)"; |
311 "extend_act h act ``` (extend_set h A) = extend_set h (act ``` A)"; |
312 by (Force_tac 1); |
312 by (Force_tac 1); |
313 qed "extend_act_Image"; |
313 qed "extend_act_Image"; |
314 Addsimps [extend_act_Image]; |
314 Addsimps [extend_act_Image]; |
315 |
315 |
316 Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)"; |
316 Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)"; |