src/HOL/Fun.thy
changeset 13637 02aa63636ab8
parent 13585 db4005b40cc6
child 13910 f9a9ef16466f
     1.1 --- a/src/HOL/Fun.thy	Thu Oct 10 14:19:17 2002 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Oct 10 14:21:20 2002 +0200
     1.3 @@ -109,12 +109,6 @@
     1.4  lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
     1.5  by (unfold comp_def, blast)
     1.6  
     1.7 -text{*Lemma for proving injectivity of representation functions for
     1.8 -datatypes involving function types*}
     1.9 -lemma inj_fun_lemma:
    1.10 -  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"
    1.11 -by (simp add: comp_def expand_fun_eq)
    1.12 -
    1.13  
    1.14  subsection{*The Injectivity Predicate, @{term inj}*}
    1.15  
    1.16 @@ -126,6 +120,9 @@
    1.17      "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
    1.18  by (simp add: inj_on_def)
    1.19  
    1.20 +theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
    1.21 +  by (unfold inj_on_def, blast)
    1.22 +
    1.23  lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
    1.24  by (simp add: inj_on_def)
    1.25  
    1.26 @@ -133,9 +130,6 @@
    1.27  lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
    1.28  by (force simp add: inj_on_def)
    1.29  
    1.30 -lemma inj_o: "[| inj f; f o g = f o h |] ==> g = h"
    1.31 -by (simp add: comp_def inj_on_def expand_fun_eq)
    1.32 -
    1.33  
    1.34  subsection{*The Predicate @{term inj_on}: Injectivity On A Restricted Domain*}
    1.35  
    1.36 @@ -392,11 +386,9 @@
    1.37  val image_compose = thm "image_compose";
    1.38  val image_eq_UN = thm "image_eq_UN";
    1.39  val UN_o = thm "UN_o";
    1.40 -val inj_fun_lemma = thm "inj_fun_lemma";
    1.41  val datatype_injI = thm "datatype_injI";
    1.42  val injD = thm "injD";
    1.43  val inj_eq = thm "inj_eq";
    1.44 -val inj_o = thm "inj_o";
    1.45  val inj_onI = thm "inj_onI";
    1.46  val inj_on_inverseI = thm "inj_on_inverseI";
    1.47  val inj_onD = thm "inj_onD";
    1.48 @@ -447,6 +439,7 @@
    1.49  val fun_upd_other = thm "fun_upd_other";
    1.50  val fun_upd_upd = thm "fun_upd_upd";
    1.51  val fun_upd_twist = thm "fun_upd_twist";
    1.52 +val range_ex1_eq = thm "range_ex1_eq";
    1.53  *}
    1.54  
    1.55  end