src/HOL/Library/Quotient_Product.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 40465 2989f9f3aa10
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    assumes q1: "Quotient R1 Abs1 Rep1"
     1.5    assumes q2: "Quotient R2 Abs2 Rep2"
     1.6    shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
     1.7 -  apply(simp add: ext_iff)
     1.8 +  apply(simp add: fun_eq_iff)
     1.9    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.10    done
    1.11  
    1.12 @@ -65,7 +65,7 @@
    1.13    assumes q1: "Quotient R1 Abs1 Rep1"
    1.14    assumes q2: "Quotient R2 Abs2 Rep2"
    1.15    shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    1.16 -  apply(simp add: ext_iff)
    1.17 +  apply(simp add: fun_eq_iff)
    1.18    apply(simp add: Quotient_abs_rep[OF q1])
    1.19    done
    1.20  
    1.21 @@ -79,7 +79,7 @@
    1.22    assumes q1: "Quotient R1 Abs1 Rep1"
    1.23    assumes q2: "Quotient R2 Abs2 Rep2"
    1.24    shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    1.25 -  apply(simp add: ext_iff)
    1.26 +  apply(simp add: fun_eq_iff)
    1.27    apply(simp add: Quotient_abs_rep[OF q2])
    1.28    done
    1.29  
    1.30 @@ -91,7 +91,7 @@
    1.31    assumes q1: "Quotient R1 Abs1 Rep1"
    1.32    and     q2: "Quotient R2 Abs2 Rep2"
    1.33    shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
    1.34 -  by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.35 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.36  
    1.37  lemma [quot_respect]:
    1.38    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
    1.39 @@ -103,7 +103,7 @@
    1.40    and     q2: "Quotient R2 abs2 rep2"
    1.41    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    1.42    prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
    1.43 -  by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.44 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.45  
    1.46  lemma [quot_preserve]:
    1.47    shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
    1.48 @@ -118,6 +118,6 @@
    1.49  
    1.50  lemma prod_rel_eq[id_simps]:
    1.51    shows "prod_rel (op =) (op =) = (op =)"
    1.52 -  by (simp add: ext_iff)
    1.53 +  by (simp add: fun_eq_iff)
    1.54  
    1.55  end