src/HOL/Quotient.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39669 9e3b035841e4
     1.1 --- a/src/HOL/Quotient.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Mon Sep 13 11:13:15 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 ext_iff
     1.8 +  unfolding equivp_def reflp_def symp_def transp_def fun_eq_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: ext_iff)
    1.17 +  by (auto simp add: fun_eq_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: ext_iff id_def)
    1.26 +  by (simp add: fun_eq_iff id_def)
    1.27  
    1.28  lemma fun_rel_eq:
    1.29    shows "((op =) ===> (op =)) = (op =)"
    1.30 -  by (simp add: ext_iff)
    1.31 +  by (simp add: fun_eq_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 ext_iff
    1.40 +    unfolding fun_eq_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 ext_iff
    1.49 +    unfolding fun_eq_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 ext_iff
    1.58 +  unfolding fun_eq_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 ext_iff
    1.67 +  unfolding fun_eq_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 ext_iff
    1.76 +  unfolding fun_eq_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: ext_iff Babs_def in_respects equivp_reflp)
    1.85 +  by (simp add: fun_eq_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 ext_iff by simp_all
    1.94 +  unfolding o_def fun_eq_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 ext_iff by auto
   1.100 +  unfolding fun_rel_def o_def fun_eq_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: ext_iff)
   1.109 +  by (auto simp add: fun_eq_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: ext_iff)
   1.118 +  by (auto simp add: fun_eq_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: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
   1.127 +  by (simp add: fun_eq_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"