src/HOL/Library/FuncSet.thy
changeset 39198 f967a16dfcdd
parent 38656 d5d342611edb
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  lemma compose_assoc:
     1.5      "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
     1.6        ==> compose A h (compose A g f) = compose A (compose B h g) f"
     1.7 -by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
     1.8 +by (simp add: ext_iff Pi_def compose_def restrict_def)
     1.9  
    1.10  lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
    1.11  by (simp add: compose_def restrict_def)
    1.12 @@ -151,18 +151,18 @@
    1.13  
    1.14  lemma restrict_ext:
    1.15      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.16 -  by (simp add: expand_fun_eq Pi_def restrict_def)
    1.17 +  by (simp add: ext_iff Pi_def restrict_def)
    1.18  
    1.19  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.20    by (simp add: inj_on_def restrict_def)
    1.21  
    1.22  lemma Id_compose:
    1.23      "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
    1.24 -  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
    1.25 +  by (auto simp add: ext_iff compose_def extensional_def Pi_def)
    1.26  
    1.27  lemma compose_Id:
    1.28      "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
    1.29 -  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
    1.30 +  by (auto simp add: ext_iff compose_def extensional_def Pi_def)
    1.31  
    1.32  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
    1.33    by (auto simp add: restrict_def)
    1.34 @@ -205,7 +205,7 @@
    1.35  lemma extensionalityI:
    1.36    "[| f \<in> extensional A; g \<in> extensional A;
    1.37        !!x. x\<in>A ==> f x = g x |] ==> f = g"
    1.38 -by (force simp add: expand_fun_eq extensional_def)
    1.39 +by (force simp add: ext_iff extensional_def)
    1.40  
    1.41  lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
    1.42  by (unfold inv_into_def) (fast intro: someI2)