src/HOL/Fun.thy
changeset 39198 f967a16dfcdd
parent 39101 606432dd1896
child 39213 297cd703f1f0
     1.1 --- a/src/HOL/Fun.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  text{*As a simplification rule, it replaces all function equalities by
     1.6    first-order equalities.*}
     1.7 -lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
     1.8 +lemma ext_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 @@ -163,7 +163,7 @@
    1.13    by (simp add: inj_on_def)
    1.14  
    1.15  lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
    1.16 -  by (simp add: inj_on_def expand_fun_eq)
    1.17 +  by (simp add: inj_on_def ext_iff)
    1.18  
    1.19  lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
    1.20  by (simp add: inj_on_eq_iff)
    1.21 @@ -463,7 +463,7 @@
    1.22  by simp
    1.23  
    1.24  lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"
    1.25 -by (simp add: expand_fun_eq)
    1.26 +by (simp add: ext_iff)
    1.27  
    1.28  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    1.29  by (rule ext, auto)
    1.30 @@ -515,7 +515,7 @@
    1.31  lemma swap_triple:
    1.32    assumes "a \<noteq> c" and "b \<noteq> c"
    1.33    shows "swap a b (swap b c (swap a b f)) = swap a c f"
    1.34 -  using assms by (simp add: expand_fun_eq swap_def)
    1.35 +  using assms by (simp add: ext_iff swap_def)
    1.36  
    1.37  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.38  by (rule ext, simp add: fun_upd_def swap_def)