equal
deleted
inserted
replaced
119 (*A convenient way of finding a closed form for inv h*) |
119 (*A convenient way of finding a closed form for inv h*) |
120 lemma fst_inv_equalityI: |
120 lemma fst_inv_equalityI: |
121 assumes surj_h: "surj h" |
121 assumes surj_h: "surj h" |
122 and prem: "!! x y. g (h(x,y)) = x" |
122 and prem: "!! x y. g (h(x,y)) = x" |
123 shows "fst (inv h z) = g z" |
123 shows "fst (inv h z) = g z" |
124 apply (unfold inv_def) |
124 by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range) |
125 apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE]) |
|
126 apply (rule someI2) |
|
127 apply (drule_tac [2] f = g in arg_cong) |
|
128 apply (auto simp add: prem) |
|
129 done |
|
130 |
125 |
131 |
126 |
132 subsection{*Trivial properties of f, g, h*} |
127 subsection{*Trivial properties of f, g, h*} |
133 |
128 |
134 lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" |
129 lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" |