equal
deleted
inserted
replaced
108 (** (rename h) is bijective <=> h is bijective **) |
108 (** (rename h) is bijective <=> h is bijective **) |
109 |
109 |
110 lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))" |
110 lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))" |
111 apply (rule bijI) |
111 apply (rule bijI) |
112 apply (blast intro: Extend.inj_extend) |
112 apply (blast intro: Extend.inj_extend) |
113 apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI) |
113 apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI) |
114 apply (subst inv_inv_eq [of h, symmetric], assumption) |
114 apply (simplesubst inv_inv_eq [of h, symmetric], assumption) |
115 apply (subst extend_inv, simp add: bij_imp_bij_inv) |
115 apply (subst extend_inv, simp add: bij_imp_bij_inv) |
116 apply (simp add: inv_inv_eq) |
116 apply (simp add: inv_inv_eq) |
117 apply (rule Extend.extend_inverse) |
117 apply (rule Extend.extend_inverse) |
118 apply (simp add: bij_imp_bij_inv) |
118 apply (simp add: bij_imp_bij_inv) |
119 done |
119 done |