src/HOL/Quotient.thy
changeset 38317 cb8e2ac6397b
parent 37986 3b3187adf292
child 38702 72fd257f4343
     1.1 --- a/src/HOL/Quotient.thy	Tue Aug 10 22:26:23 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Aug 11 13:30:24 2010 +0800
     1.3 @@ -136,16 +136,6 @@
     1.4    shows "((op =) ===> (op =)) = (op =)"
     1.5    by (simp add: expand_fun_eq)
     1.6  
     1.7 -lemma fun_rel_id:
     1.8 -  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
     1.9 -  shows "(R1 ===> R2) f g"
    1.10 -  using a by simp
    1.11 -
    1.12 -lemma fun_rel_id_asm:
    1.13 -  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
    1.14 -  shows "A \<longrightarrow> (R1 ===> R2) f g"
    1.15 -  using a by auto
    1.16 -
    1.17  
    1.18  subsection {* Quotient Predicate *}
    1.19  
    1.20 @@ -597,7 +587,7 @@
    1.21  lemma quot_rel_rsp:
    1.22    assumes a: "Quotient R Abs Rep"
    1.23    shows "(R ===> R ===> op =) R R"
    1.24 -  apply(rule fun_rel_id)+
    1.25 +  apply(rule fun_relI)+
    1.26    apply(rule equals_rsp[OF a])
    1.27    apply(assumption)+
    1.28    done