src/HOL/Fun.thy
 changeset 39302 d7728f65b353 parent 39213 297cd703f1f0 child 40602 91e583511113
```     1.1 --- a/src/HOL/Fun.thy	Mon Sep 13 08:43:48 2010 +0200
1.2 +++ b/src/HOL/Fun.thy	Mon Sep 13 11:13:15 2010 +0200
1.3 @@ -11,15 +11,13 @@
1.4
1.5  text{*As a simplification rule, it replaces all function equalities by
1.6    first-order equalities.*}
1.7 -lemma ext_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.8 +lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.9  apply (rule iffI)
1.10  apply (simp (no_asm_simp))
1.11  apply (rule ext)
1.12  apply (simp (no_asm_simp))
1.13  done
1.14
1.15 -lemmas expand_fun_eq = ext_iff
1.16 -
1.17  lemma apply_inverse:
1.18    "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
1.19    by auto
1.20 @@ -165,7 +163,7 @@
1.22
1.23  lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
1.24 -  by (simp add: inj_on_def ext_iff)
1.25 +  by (simp add: inj_on_def fun_eq_iff)
1.26
1.27  lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
1.29 @@ -465,7 +463,7 @@
1.30  by simp
1.31
1.32  lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"