*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] ZF_Addons.thy*From*: Victor Porton <porton at narod.ru>*Date*: Fri, 17 Dec 2010 01:18:43 +0300*Envelope-from*: porton@yandex.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;

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

Victor Porton - http://portonvictor.org

**Follow-Ups**:**Re: [isabelle] ZF_Addons.thy***From:*Lawrence Paulson

- Previous by Date: [isabelle] Other novice question
- Next by Date: [isabelle] Functions vs. relations
- Previous by Thread: [isabelle] Other novice question
- Next by Thread: Re: [isabelle] ZF_Addons.thy
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list