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.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.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.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.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.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.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)