src/HOL/BNF_Least_Fixpoint.thy
changeset 58159 e3d1912a0c8f
parent 58147 967444d352b8
child 58179 2de7b0313de3
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:06:32 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:31:37 2014 +0200
     1.3 @@ -66,13 +66,12 @@
     1.4  lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
     1.5    unfolding bij_betw_def by auto
     1.6  
     1.7 -lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
     1.8 -  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
     1.9 +lemma f_the_inv_into_f_bij_betw:
    1.10 +  "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    1.11    unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    1.12  
    1.13  lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    1.14 -  by (subst (asm) internalize_card_of_ordLeq)
    1.15 -    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    1.16 +  by (subst (asm) internalize_card_of_ordLeq) (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    1.17  
    1.18  lemma bij_betwI':
    1.19    "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);