--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Apr 07 17:56:22 2016 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Apr 07 17:56:26 2016 +0200
@@ -43,9 +43,6 @@
lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
unfolding bij_betw_def by auto
-lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
- unfolding bij_betw_def by auto
-
lemma f_the_inv_into_f_bij_betw:
"bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Apr 07 17:56:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Apr 07 17:56:26 2016 +0200
@@ -169,11 +169,11 @@
val n = length alg_sets;
fun set_tac thm =
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
- rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
+ rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
val alg_tac =
CONJ_WRAP' (fn (set_maps, alg_set) =>
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
- rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
+ rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
(set_mapss ~~ alg_sets);