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.21    by (simp add: inj_on_def)
    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.28  by (simp add: inj_on_eq_iff)
    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)"
    1.33 -by (simp add: ext_iff)
    1.34 +by (simp add: fun_eq_iff)
    1.35  
    1.36  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    1.37  by (rule ext, auto)
    1.38 @@ -517,7 +515,7 @@
    1.39  lemma swap_triple:
    1.40    assumes "a \<noteq> c" and "b \<noteq> c"
    1.41    shows "swap a b (swap b c (swap a b f)) = swap a c f"
    1.42 -  using assms by (simp add: ext_iff swap_def)
    1.43 +  using assms by (simp add: fun_eq_iff swap_def)
    1.44  
    1.45  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.46  by (rule ext, simp add: fun_upd_def swap_def)