equal
deleted
inserted
replaced
62 apply (rule Extend.inj_extend_act) |
62 apply (rule Extend.inj_extend_act) |
63 apply simp |
63 apply simp |
64 apply (simp add: bij_extend_act_eq_project_act) |
64 apply (simp add: bij_extend_act_eq_project_act) |
65 apply (rule surjI) |
65 apply (rule surjI) |
66 apply (rule Extend.extend_act_inverse) |
66 apply (rule Extend.extend_act_inverse) |
67 apply (blast intro: bij_imp_bij_inv good_map_bij) |
67 apply (blast intro: bij_imp_bij_inv) |
68 done |
68 done |
69 |
69 |
70 lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))" |
70 lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))" |
71 apply (frule bij_imp_bij_inv [THEN bij_extend_act]) |
71 apply (frule bij_imp_bij_inv [THEN bij_extend_act]) |
72 apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq) |
72 apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq) |