src/HOL/Quotient.thy
 changeset 39198 f967a16dfcdd parent 38861 27c7b620758c child 39302 d7728f65b353
```     1.1 --- a/src/HOL/Quotient.thy	Mon Sep 06 22:58:06 2010 +0200
1.2 +++ b/src/HOL/Quotient.thy	Tue Sep 07 10:05:19 2010 +0200
1.3 @@ -34,7 +34,7 @@
1.4
1.5  lemma equivp_reflp_symp_transp:
1.6    shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
1.7 -  unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
1.8 +  unfolding equivp_def reflp_def symp_def transp_def ext_iff
1.9    by blast
1.10
1.11  lemma equivp_reflp:
1.12 @@ -97,7 +97,7 @@
1.13
1.14  lemma eq_comp_r:
1.15    shows "((op =) OOO R) = R"
1.16 -  by (auto simp add: expand_fun_eq)
1.17 +  by (auto simp add: ext_iff)
1.18
1.19  subsection {* Respects predicate *}
1.20
1.21 @@ -130,11 +130,11 @@
1.22
1.23  lemma fun_map_id:
1.24    shows "(id ---> id) = id"
1.25 -  by (simp add: expand_fun_eq id_def)
1.26 +  by (simp add: ext_iff id_def)
1.27
1.28  lemma fun_rel_eq:
1.29    shows "((op =) ===> (op =)) = (op =)"
1.30 -  by (simp add: expand_fun_eq)
1.31 +  by (simp add: ext_iff)
1.32
1.33
1.34  subsection {* Quotient Predicate *}
1.35 @@ -209,7 +209,7 @@
1.36    have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
1.37      using q1 q2
1.38      unfolding Quotient_def
1.39 -    unfolding expand_fun_eq
1.40 +    unfolding ext_iff
1.41      by simp
1.42    moreover
1.43    have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
1.44 @@ -219,7 +219,7 @@
1.45    moreover
1.46    have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
1.47          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
1.48 -    unfolding expand_fun_eq
1.49 +    unfolding ext_iff
1.50      apply(auto)
1.51      using q1 q2 unfolding Quotient_def
1.52      apply(metis)
1.53 @@ -238,7 +238,7 @@
1.54  lemma abs_o_rep:
1.55    assumes a: "Quotient R Abs Rep"
1.56    shows "Abs o Rep = id"
1.57 -  unfolding expand_fun_eq
1.58 +  unfolding ext_iff
1.59    by (simp add: Quotient_abs_rep[OF a])
1.60
1.61  lemma equals_rsp:
1.62 @@ -253,7 +253,7 @@
1.63    assumes q1: "Quotient R1 Abs1 Rep1"
1.64    and     q2: "Quotient R2 Abs2 Rep2"
1.65    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
1.66 -  unfolding expand_fun_eq
1.67 +  unfolding ext_iff
1.68    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
1.69    by simp
1.70
1.71 @@ -261,7 +261,7 @@
1.72    assumes q1: "Quotient R1 Abs1 Rep1"
1.73    and     q2: "Quotient R2 Abs2 Rep2"
1.74    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
1.75 -  unfolding expand_fun_eq
1.76 +  unfolding ext_iff
1.77    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
1.78    by simp
1.79
1.80 @@ -445,7 +445,7 @@
1.81     is an equivalence this may be useful in regularising *)
1.82  lemma babs_reg_eqv:
1.83    shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
1.84 -  by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
1.85 +  by (simp add: ext_iff Babs_def in_respects equivp_reflp)
1.86
1.87
1.88  (* 3 lemmas needed for proving repabs_inj *)
1.89 @@ -617,12 +617,12 @@
1.90    shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
1.91    and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
1.92    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
1.93 -  unfolding o_def expand_fun_eq by simp_all
1.94 +  unfolding o_def ext_iff by simp_all
1.95
1.96  lemma o_rsp:
1.97    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
1.98    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
1.99 -  unfolding fun_rel_def o_def expand_fun_eq by auto
1.100 +  unfolding fun_rel_def o_def ext_iff by auto
1.101
1.102  lemma cond_prs:
1.103    assumes a: "Quotient R absf repf"
1.104 @@ -633,7 +633,7 @@
1.105    assumes q: "Quotient R Abs Rep"
1.106    shows "(id ---> Rep ---> Rep ---> Abs) If = If"
1.107    using Quotient_abs_rep[OF q]
1.108 -  by (auto simp add: expand_fun_eq)
1.109 +  by (auto simp add: ext_iff)
1.110
1.111  lemma if_rsp:
1.112    assumes q: "Quotient R Abs Rep"
1.113 @@ -645,7 +645,7 @@
1.114    and     q2: "Quotient R2 Abs2 Rep2"
1.115    shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
1.116    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
1.117 -  by (auto simp add: expand_fun_eq)
1.118 +  by (auto simp add: ext_iff)
1.119
1.120  lemma let_rsp:
1.121    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
1.122 @@ -659,7 +659,7 @@
1.123    assumes a1: "Quotient R1 Abs1 Rep1"
1.124    and     a2: "Quotient R2 Abs2 Rep2"
1.125    shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
1.126 -  by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
1.127 +  by (simp add: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
1.128
1.129  locale quot_type =
1.130    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```