src/HOL/Quotient.thy
changeset 38702 72fd257f4343
parent 38317 cb8e2ac6397b
child 38859 053c69cb4a0e
     1.1 --- a/src/HOL/Quotient.thy	Tue Aug 24 20:09:30 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Aug 25 11:17:33 2010 +0900
     1.3 @@ -571,7 +571,8 @@
     1.4  apply metis
     1.5  done
     1.6  
     1.7 -lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
     1.8 +lemma bex1_bexeq_reg:
     1.9 +  shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
    1.10    apply (simp add: Ex1_def Bex1_rel_def in_respects)
    1.11    apply clarify
    1.12    apply auto
    1.13 @@ -582,6 +583,23 @@
    1.14    apply auto
    1.15    done
    1.16  
    1.17 +lemma bex1_bexeq_reg_eqv:
    1.18 +  assumes a: "equivp R"
    1.19 +  shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
    1.20 +  using equivp_reflp[OF a]
    1.21 +  apply (intro impI)
    1.22 +  apply (elim ex1E)
    1.23 +  apply (rule mp[OF bex1_bexeq_reg])
    1.24 +  apply (rule_tac a="x" in ex1I)
    1.25 +  apply (subst in_respects)
    1.26 +  apply (rule conjI)
    1.27 +  apply assumption
    1.28 +  apply assumption
    1.29 +  apply clarify
    1.30 +  apply (erule_tac x="xa" in allE)
    1.31 +  apply simp
    1.32 +  done
    1.33 +
    1.34  subsection {* Various respects and preserve lemmas *}
    1.35  
    1.36  lemma quot_rel_rsp: