src/HOL/Hilbert_Choice.thy
changeset 35216 7641e8d831d2
parent 35115 446c5063e4fd
child 35416 d8d7d1b785af
equal deleted inserted replaced
35215:a03462cbf86f 35216:7641e8d831d2
    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