Theory ZF_Miscellanea

section‹Various results missing from ZF.›

theory ZF_Miscellanea
  imports
    ZF
    Nat_Miscellanea
begin

definition
  SepReplace :: "[i, i⇒i, i⇒ o] ⇒ i" where
  "SepReplace(A,b,Q) ≡ {y . x∈A, y=b(x) ∧ Q(x)}"

syntax
  "_SepReplace"  :: "[i, pttrn, i, o] ⇒ i"  ("(1{_ ../ _ ∈ _, _})")
translations
  "{b .. x∈A, Q}" => "CONST SepReplace(A, λx. b, λx. Q)"

lemma Sep_and_Replace : "{b(x) .. x∈A, P(x) } = {b(x) . x∈{y∈A. P(y)}}"
  by (auto simp add:SepReplace_def)

lemma SepReplace_subset : "A⊆A'⟹ {b .. x∈A, Q}⊆{b .. x∈A', Q}"
  by (auto simp add:SepReplace_def)

lemma SepReplace_iff [simp]: "y∈{b(x) .. x∈A, P(x)} ⟷ (∃x∈A. y=b(x) & P(x))"
  by (auto simp add:SepReplace_def)

lemma SepReplace_dom_implies :
  "(⋀ x . x ∈A ⟹ b(x) = b'(x))⟹ {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (simp add:SepReplace_def)

lemma SepReplace_pred_implies :
  "∀x. Q(x)⟶ b(x) = b'(x)⟹ {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (force simp add:SepReplace_def)

lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"
  by(simp_all add: apply_Pair)

lemma vimage_fun_sing :
  assumes "f∈A→B" "b∈B"
  shows "{a∈A . f`a=b} = f-``{b}"
using assms vimage_singleton_iff function_apply_equality Pi_iff funcI by auto

lemma image_fun_subset : "S∈A→B ⟹ C⊆A⟹ {S ` x . x∈ C} = S``C"
  using image_function[symmetric,of S C] domain_of_fun Pi_iff by auto

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

lemma Diff_bij :
  assumes "∀A∈F. X ⊆ A" shows "(λA∈F. A-X) ∈ bij(F, {A-X. A∈F})"
  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 "b∈B"
  shows "(λx∈A. b) : A → B"
  using assms lam_type by force

lemma vimage_lam : "(λx∈A. f(x)) -`` B = { x∈A . 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 "f∈Pi(A,B)" "b ∈ range(f)"
  shows "∃a∈A. 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


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

lemma minimum_in : "⟦ well_ord(A,r); B⊆A; B≠0 ⟧ ⟹ 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 "(λb∈B. minimum(r, {a∈A. h`a=b})) ∈ inj(B,A)"
proof -
  let ?f="λb∈B. minimum(r, {a∈A. h`a=b})"
  have "minimum(r, {a ∈ A . h ` a = b}) ∈ {a∈A. h`a=b}" if "b∈B" for b
  proof -
    from ‹h ∈ surj(A,B)› that
    have "{a∈A. h`a=b} ≠ 0"
      unfolding surj_def by blast
    with ‹well_ord(A,r)›
    show "minimum(r,{a∈A. h`a=b}) ∈ {a∈A. h`a=b}"
      using minimum_in by blast
  qed
  moreover from this
  have "?f : B → A"
      using lam_type[of B _ "λ_.A"] by simp
  moreover
  have "?f ` w = ?f ` x ⟹ w = x" if "w∈B" "x∈B" for w x
  proof -
    from calculation that
    have "w = h ` minimum(r,{a∈A. h`a=w})"
         "x = h ` minimum(r,{a∈A. h`a=x})"
      by simp_all
    moreover
    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
    qed
  ultimately
  show ?thesis
    unfolding inj_def by blast
qed

lemma well_ord_surj_imp_lepoll :
  assumes "well_ord(A,r)" "h ∈ surj(A,B)"
  shows "B≲A"
   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
  then
  show " Pow({a}) ⊆ {0, {a}}" by auto
qed

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 . B∈Pow(A) ⟹ C ≠ {a} ∪ B" "C ⊆ {a} ∪ A" "D ∈ C"
    moreover from this
    have "∀x∈C . x=a ∨ x∈A" by auto
    moreover from calculation
    consider (a) "D=a" | (b) "D∈A" by auto
    from this
    have "D∈A"
    proof(cases)
      case a
      with calculation show ?thesis by auto
    next
      case b
      then show ?thesis by simp
    qed
  }
  then show "⋀x xa. (∀xa∈Pow(A). x ≠ {a} ∪ xa) ⟹ x ⊆ cons(a, A) ⟹ xa ∈ x ⟹ xa ∈ A"
    by auto
qed

lemma app_nm :
  assumes "n∈nat" "m∈nat" "f∈n→m" "x ∈ nat"
  shows "f`x ∈ nat"
proof(cases "x∈n")
  case True
  then show ?thesis using assms in_n_in_nat apply_type by simp
next
  case False
  then show ?thesis using assms apply_0 domain_of_fun by simp
qed

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

end