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 -

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