Email Gateway (Aug 18 2022 at 16:43): Email Gateway (Aug 18 2022 at 16:43):From: Victor Porton <porton@narod.ru>
I developed the first version of my first real theory, ZF_Addons.thy,
suggested additions to core of Isabelle/ZF
I suggest to add it to IsarMathLib but because it is my first work in this
area I want first hear your replies. Is it done in a good way? What may be
changed? What may be simplified? What else you may suggest?
Should I import Main_ZF here? If not what to import instead?
theory ZF_Addons
imports Main_ZF
begin
lemma inj_inj_range: "f: inj(A,B) ==> f : inj(A,range(f))"
apply (unfold inj_def)
apply (auto simp add: Pi_iff function_def)
done
lemma inj_bij_range: "f: inj(A,B) ==> f : bij(A,range(f))"
apply (auto simp add: bij_def inj_inj_range)
apply (blast intro: inj_is_fun fun_is_surj elim:)
done
lemma range_subset: "f: A->B ==> range(f) <= B"
proof -
assume "f: A->B"
hence "f: Pow(A*B)" by (simp add: Pi_def)
hence "f <= A*B" by auto
moreover
hence "range(A*B) <= B" by auto
ultimately show "range(f) <= B" by auto
qed
end;
\--
Victor Porton - http://portonvictor.org
Email Gateway (Aug 18 2022 at 16:43):From: Lawrence Paulson <lp15@cam.ac.uk>
Thank you for your suggestions and contributions. I suggest that you work for a couple of months on a set theory development of some sort. At the end of that period, you will probably have accumulated a small library of general-purpose results that we can consider for incorporation into Isabelle/ZF itself. Just send them to me.
Larry Paulson
Last updated: Apr 27 2024 at 01:05 UTC