Theory ZF_Miscellanea

section‹Various results missing from ZF.›

theory ZF_Miscellanea

lemma rex_mono :
  assumes " d  A . P(d)" "AB"
  shows " d  B. P(d)"
  using assms by auto

lemma function_subset:
  "function(f)  gf  function(g)"
  unfolding function_def subset_def by auto

lemma converse_refl : "refl(A,r)  refl(A,converse(r))"
  unfolding refl_def by simp

lemma Ord_lt_subset : "Ord(b)  a<b  ab"
  by(intro subsetI,frule ltD,rule_tac Ord_trans,simp_all)

lemma funcI : "f  A  B  a  A  b= f ` a  a, b  f"
  by(simp_all add: apply_Pair)

lemma vimage_fun_sing:
  assumes "fAB" "bB"
  shows "{aA . f`a=b} = f-``{b}"
  using assms vimage_singleton_iff function_apply_equality Pi_iff funcI by auto

lemma image_fun_subset: "SAB  CA {S ` x . x C} = S``C"
  using image_function[symmetric,of S C] domain_of_fun Pi_iff by auto

lemma inj_range_Diff:
  assumes "f  inj(A,A')"
  shows "f``A - f``T = f``(A - T)"
    using inj_equality[OF _ _ assms] by auto

lemma subset_Diff_Un: "X  A  A = (A - X)  X " by auto

lemma Diff_bij:
  assumes "AF. X  A" shows "(λAF. A-X)  bij(F, {A-X. AF})"
  using assms unfolding bij_def inj_def surj_def
  by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto

lemma function_space_nonempty:
  assumes "bB"
  shows "(λxA. b) : A  B"
  using assms lam_type by force

lemma lam_constant_eq_cartprod: "(λ_A. y) = A × {y}"
  unfolding lam_def by auto

lemma vimage_lam: "(λxA. f(x)) -`` B = { xA . f(x)  B }"
  using lam_funtype[of A f, THEN [2] domain_type]
    lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
  by auto blast

lemma range_fun_subset_codomain:
  assumes "h:B  C"
  shows "range(h)  C"
  unfolding range_def domain_def converse_def using range_type[OF _ assms] by auto

lemma Pi_rangeD:
  assumes "fPi(A,B)" "b  range(f)"
  shows "aA. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b]
    domain_type[OF _ assms(1)] by auto

lemma Pi_range_eq: "f  Pi(A,B)  range(f) = {f ` x . x  A}"
  using Pi_rangeD[of f A B] apply_rangeI[of f A B]
  by blast

lemma Pi_vimage_subset : "f  Pi(A,B)  f-``C  A"
  unfolding Pi_def by auto

  minimum :: "i  i  i" where
  "minimum(r,B)  THE b. first(b,B,r)"

lemma minimum_in': "minimum(r,B)  B  {0}"
  using the_0 first_is_elem unfolding minimum_def
  by (cases "∃!b. first(b, B, r)")
    (auto dest!:theI[of "λb. first(b, B, r)"])

lemma minimum_in: " well_ord(A,r); BA; B0   minimum(r,B)  B"
  using the_first_in unfolding minimum_def by simp

lemma well_ord_surj_imp_inj_inverse:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "(λbB. minimum(r, {aA. h`a=b}))  inj(B,A)"
proof -
  let ?f="λbB. minimum(r, {aA. h`a=b})"
  have "minimum(r, {a  A . h ` a = b})  {aA. h`a=b}" if "bB" for b
  proof -
    from h  surj(A,B) that
    have "{aA. h`a=b}  0"
      unfolding surj_def by blast
    with well_ord(A,r)
    show "minimum(r,{aA. h`a=b})  {aA. h`a=b}"
      using minimum_in by blast
  moreover from this
  have "?f : B  A"
    using lam_type[of B _ "λ_.A"] by simp
  have "?f ` w = ?f ` x  w = x" if "wB" "xB" for w x
  proof -
    from calculation that
    have "w = h ` minimum(r,{aA. h`a=w})"
      "x = h ` minimum(r,{aA. h`a=x})"
      by simp_all
    assume "?f ` w = ?f ` x"
    moreover from this and that
    have "minimum(r, {a  A . h ` a = w}) = minimum(r, {a  A . h ` a = x})"
      unfolding minimum_def by simp_all
    moreover from calculation(1,2,4)
    show "w=x" by simp
  show ?thesis
    unfolding inj_def by blast

lemma well_ord_surj_imp_lepoll:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "BA"
  unfolding lepoll_def using well_ord_surj_imp_inj_inverse[OF assms]
  by blast

― ‹New result›
lemma surj_imp_well_ord:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "s. well_ord(B,s)"
  using assms lepoll_well_ord[OF well_ord_surj_imp_lepoll]
  by force

lemma Pow_sing : "Pow({a}) = {0,{a}}"
proof(intro equalityI,simp_all)
  have "z  {0,{a}}" if "z  {a}" for z
    using that by auto
  show " Pow({a})  {0, {a}}" by auto

lemma Pow_cons:
  shows "Pow(cons(a,A)) = Pow(A)  {{a}  X . X: Pow(A)}"
  using Un_Pow_subset Pow_sing
proof(intro equalityI,auto simp add:Un_Pow_subset)
    fix C D
    assume " B . BPow(A)  C  {a}  B" "C  {a}  A" "D  C"
    moreover from this
    have "xC . x=a  xA" by auto
    moreover from calculation
    consider (a) "D=a" | (b) "DA" by auto
    from this
    have "DA"
      case a
      with calculation show ?thesis by auto
      case b
      then show ?thesis by simp
  then show "x xa. (xaPow(A). x  {a}  xa)  x  cons(a, A)  xa  x  xa  A"
    by auto

lemma app_nm :
  assumes "nnat" "mnat" "fnm" "x  nat"
  shows "f`x  nat"
proof(cases "xn")
  case True
  then show ?thesis using assms in_n_in_nat apply_type by simp
  case False
  then show ?thesis using assms apply_0 domain_of_fun by simp

lemma Upair_eq_cons: "Upair(a,b) = {a,b}"
  unfolding cons_def by auto

lemma converse_apply_eq : "converse(f) ` x = (f -`` {x})"
  unfolding apply_def vimage_def by simp

lemmas app_fun = apply_iff[THEN iffD1]

lemma Finite_imp_lesspoll_nat:
  assumes "Finite(A)"
  shows "A  nat"
  using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans
    n_lesspoll_nat eq_lesspoll_trans
  unfolding Finite_def lesspoll_def by auto

definition curry :: "[i,i,i]  i" where
  "curry(A,B,f)  λxA . λyB . f`x,y"

lemma curry_type :
  assumes "f  A×B  C"
  shows "curry(A,B,f)  A  (B  C)"
  using assms lam_funtype
  unfolding curry_def
  by auto