--- a/src/HOL/Quotient.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Quotient.thy Tue Sep 07 10:05:19 2010 +0200
@@ -34,7 +34,7 @@
lemma equivp_reflp_symp_transp:
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
- unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
+ unfolding equivp_def reflp_def symp_def transp_def ext_iff
by blast
lemma equivp_reflp:
@@ -97,7 +97,7 @@
lemma eq_comp_r:
shows "((op =) OOO R) = R"
- by (auto simp add: expand_fun_eq)
+ by (auto simp add: ext_iff)
subsection {* Respects predicate *}
@@ -130,11 +130,11 @@
lemma fun_map_id:
shows "(id ---> id) = id"
- by (simp add: expand_fun_eq id_def)
+ by (simp add: ext_iff id_def)
lemma fun_rel_eq:
shows "((op =) ===> (op =)) = (op =)"
- by (simp add: expand_fun_eq)
+ by (simp add: ext_iff)
subsection {* Quotient Predicate *}
@@ -209,7 +209,7 @@
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
using q1 q2
unfolding Quotient_def
- unfolding expand_fun_eq
+ unfolding ext_iff
by simp
moreover
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
@@ -219,7 +219,7 @@
moreover
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- unfolding expand_fun_eq
+ unfolding ext_iff
apply(auto)
using q1 q2 unfolding Quotient_def
apply(metis)
@@ -238,7 +238,7 @@
lemma abs_o_rep:
assumes a: "Quotient R Abs Rep"
shows "Abs o Rep = id"
- unfolding expand_fun_eq
+ unfolding ext_iff
by (simp add: Quotient_abs_rep[OF a])
lemma equals_rsp:
@@ -253,7 +253,7 @@
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
- unfolding expand_fun_eq
+ unfolding ext_iff
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
by simp
@@ -261,7 +261,7 @@
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
- unfolding expand_fun_eq
+ unfolding ext_iff
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
by simp
@@ -445,7 +445,7 @@
is an equivalence this may be useful in regularising *)
lemma babs_reg_eqv:
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
- by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
+ by (simp add: ext_iff Babs_def in_respects equivp_reflp)
(* 3 lemmas needed for proving repabs_inj *)
@@ -617,12 +617,12 @@
shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
- unfolding o_def expand_fun_eq by simp_all
+ unfolding o_def ext_iff by simp_all
lemma o_rsp:
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
- unfolding fun_rel_def o_def expand_fun_eq by auto
+ unfolding fun_rel_def o_def ext_iff by auto
lemma cond_prs:
assumes a: "Quotient R absf repf"
@@ -633,7 +633,7 @@
assumes q: "Quotient R Abs Rep"
shows "(id ---> Rep ---> Rep ---> Abs) If = If"
using Quotient_abs_rep[OF q]
- by (auto simp add: expand_fun_eq)
+ by (auto simp add: ext_iff)
lemma if_rsp:
assumes q: "Quotient R Abs Rep"
@@ -645,7 +645,7 @@
and q2: "Quotient R2 Abs2 Rep2"
shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
- by (auto simp add: expand_fun_eq)
+ by (auto simp add: ext_iff)
lemma let_rsp:
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
@@ -659,7 +659,7 @@
assumes a1: "Quotient R1 Abs1 Rep1"
and a2: "Quotient R2 Abs2 Rep2"
shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
- by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
+ by (simp add: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
locale quot_type =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"