equal
deleted
inserted
replaced
59 lemma some_equality [intro]: |
59 lemma some_equality [intro]: |
60 "[| P a; !!x. P x ==> x=a |] ==> (SOME x. P x) = a" |
60 "[| P a; !!x. P x ==> x=a |] ==> (SOME x. P x) = a" |
61 by (blast intro: someI2) |
61 by (blast intro: someI2) |
62 |
62 |
63 lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a" |
63 lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a" |
64 by (blast intro: some_equality) |
64 by blast |
65 |
65 |
66 lemma some_eq_ex: "P (SOME x. P x) = (\<exists>x. P x)" |
66 lemma some_eq_ex: "P (SOME x. P x) = (\<exists>x. P x)" |
67 by (blast intro: someI) |
67 by (blast intro: someI) |
68 |
68 |
69 lemma some_eq_trivial [simp]: "(SOME y. y=x) = x" |
69 lemma some_eq_trivial [simp]: "(SOME y. y=x) = x" |
106 apply (simp add: inv_into_def inj_on_def) |
106 apply (simp add: inv_into_def inj_on_def) |
107 apply (blast intro: someI2) |
107 apply (blast intro: someI2) |
108 done |
108 done |
109 |
109 |
110 lemma inv_f_f: "inj f ==> inv f (f x) = x" |
110 lemma inv_f_f: "inj f ==> inv f (f x) = x" |
111 by (simp add: inv_into_f_f) |
111 by simp |
112 |
112 |
113 lemma f_inv_into_f: "y : f`A ==> f (inv_into A f y) = y" |
113 lemma f_inv_into_f: "y : f`A ==> f (inv_into A f y) = y" |
114 apply (simp add: inv_into_def) |
114 apply (simp add: inv_into_def) |
115 apply (fast intro: someI2) |
115 apply (fast intro: someI2) |
116 done |
116 done |