# Re: [isabelle] ZF_Addons.thy

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
On 16 Dec 2010, at 22:18, Victor Porton wrote:
> 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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*