removed duplicate lemma
authortraytel
Thu Apr 07 17:56:26 2016 +0200 (2016-04-07)
changeset 6290675ca185db27f
parent 62905 52c5a25e0c96
child 62907 9ad0bac25a84
removed duplicate lemma
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:26 2016 +0200
     1.3 @@ -43,9 +43,6 @@
     1.4  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
     1.5    unfolding bij_betw_def by auto
     1.6  
     1.7 -lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
     1.8 -  unfolding bij_betw_def by auto
     1.9 -
    1.10  lemma f_the_inv_into_f_bij_betw:
    1.11    "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.12    unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Apr 07 17:56:22 2016 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Apr 07 17:56:26 2016 +0200
     2.3 @@ -169,11 +169,11 @@
     2.4      val n = length alg_sets;
     2.5      fun set_tac thm =
     2.6        EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
     2.7 -        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
     2.8 +        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
     2.9      val alg_tac =
    2.10        CONJ_WRAP' (fn (set_maps, alg_set) =>
    2.11          EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
    2.12 -          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
    2.13 +          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
    2.14            rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
    2.15        (set_mapss ~~ alg_sets);
    2.16