[isabelle] ZF_Addons.thy



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.