src/HOL/Product_Type.thy
changeset 39302 d7728f65b353
parent 39272 0b61951d2682
child 40590 b994d855dbd2
--- a/src/HOL/Product_Type.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -151,7 +151,7 @@
 next
   fix a c :: 'a and b d :: 'b
   have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
-    by (auto simp add: Pair_Rep_def ext_iff)
+    by (auto simp add: Pair_Rep_def fun_eq_iff)
   moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
     by (auto simp add: prod_def)
   ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
@@ -394,7 +394,7 @@
   (Haskell "fst" and "snd")
 
 lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
-  by (simp add: ext_iff split: prod.split)
+  by (simp add: fun_eq_iff split: prod.split)
 
 lemma fst_eqD: "fst (x, y) = a ==> x = a"
   by simp
@@ -423,11 +423,11 @@
   by (rule split_conv [THEN iffD1])
 
 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
-  by (simp add: ext_iff split: prod.split)
+  by (simp add: fun_eq_iff split: prod.split)
 
 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
-  by (simp add: ext_iff split: prod.split)
+  by (simp add: fun_eq_iff split: prod.split)
 
 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   by (cases x) simp
@@ -797,25 +797,25 @@
   "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
 
 lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
-  by (simp add: ext_iff scomp_def prod_case_unfold)
+  by (simp add: fun_eq_iff scomp_def prod_case_unfold)
 
 lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
   by (simp add: scomp_unfold prod_case_unfold)
 
 lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
-  by (simp add: ext_iff scomp_apply)
+  by (simp add: fun_eq_iff scomp_apply)
 
 lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
-  by (simp add: ext_iff scomp_apply)
+  by (simp add: fun_eq_iff scomp_apply)
 
 lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
-  by (simp add: ext_iff scomp_unfold)
+  by (simp add: fun_eq_iff scomp_unfold)
 
 lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
-  by (simp add: ext_iff scomp_unfold fcomp_def)
+  by (simp add: fun_eq_iff scomp_unfold fcomp_def)
 
 lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
-  by (simp add: ext_iff scomp_unfold fcomp_apply)
+  by (simp add: fun_eq_iff scomp_unfold fcomp_apply)
 
 code_const scomp
   (Eval infixl 3 "#->")
@@ -919,11 +919,11 @@
 
 lemma apfst_id [simp] :
   "apfst id = id"
-  by (simp add: ext_iff)
+  by (simp add: fun_eq_iff)
 
 lemma apsnd_id [simp] :
   "apsnd id = id"
-  by (simp add: ext_iff)
+  by (simp add: fun_eq_iff)
 
 lemma apfst_eq_conv [simp]:
   "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
@@ -1130,7 +1130,7 @@
   assumes "f ` A = A'" and "g ` B = B'"
   shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
 unfolding image_def
-proof(rule set_ext,rule iffI)
+proof(rule set_eqI,rule iffI)
   fix x :: "'a \<times> 'c"
   assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
   then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast