(* Edited by Jon Barwise, Handbook of mathematical logic, part B. Set Theory *)
(* Стараемся использовать только auto и metis. Иногда приходится также "..", "step", "rule" и последовательное применение нескольких методов, скажем, step, insert и auto *)

theory zfc_in_hol
imports Metis (* HOL содержит THE и undefined, но не содержит Hilbert choice *)
begin

no_notation
  Set.union ("op \<union>") and
  Set.union (infixl "\<union>" 65)

no_notation
  Set.subset  ("op \<subset>") and
  Set.subset  ("(_/ \<subset> _)" [51, 51] 50) and
  Set.subset_eq  ("op \<subseteq>") and
  Set.subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)

no_translations
  "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
  "{x}" \<rightleftharpoons> "CONST insert x {}"
no_syntax
  "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")

no_translations
  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
  "\<exists>!x\<in>A. P" \<rightharpoonup> "\<exists>!x. x \<in> A \<and> P"
  "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"

no_notation
  Set.not_member  ("op \<notin>") and
  Set.not_member  ("(_/ \<notin> _)" [51, 51] 50)

no_notation
  Set.member ("op \<in>") and
  Set.member ("(_/ \<in> _)" [51, 51] 50)

no_notation
  Groups.zero_class.zero ("0")

typedecl set

axiomatization
  elem :: "set \<Rightarrow> set \<Rightarrow> bool" (infixl "\<in>" 50)

abbreviation not_elem :: "set \<Rightarrow> set \<Rightarrow> bool" (infixl "\<notin>" 50) where
  "(x \<notin> y) \<equiv> \<not> (x \<in> y)"

abbreviation bounded_all :: "set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> bool" where
  "bounded_all A P \<equiv> (\<forall> x. x \<in> A \<longrightarrow> P x)"

abbreviation bounded_ex :: "set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> bool" where
  "bounded_ex A P \<equiv> (\<exists> x. x \<in> A \<and> P x)"

syntax
  "_Ball" :: "[pttrn, set, bool] \<Rightarrow> bool"
  "_Bex" :: "[pttrn, set, bool] \<Rightarrow> bool"
translations
  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST bounded_all A (\<lambda>x. P)"
  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST bounded_ex A (\<lambda>x. P)"

(* B.1 Axioms of Set Theory *)
(* 3. The axioms *)

(* Аксиомы, которые будем потом употреблять непосредственно, называем коротко. Если же будем использовать более удобные следствия, называем длинно *)

axiomatization where
  ext: "(\<forall> z. z \<in> x \<longleftrightarrow> z \<in> y) \<Longrightarrow> x = y" and
  separation_axiom: "(\<forall> x. \<phi> x \<longrightarrow> x \<in> y) \<Longrightarrow> (\<exists> z. \<forall> t. t \<in> z \<longleftrightarrow> \<phi> t)" and
  union_axiom: "\<exists> t. \<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z \<in> y)"

definition subset :: "set \<Rightarrow> set \<Rightarrow> bool" (infixl "\<subseteq>" 50) where
  subset_def: "x \<subseteq> y \<longleftrightarrow> (\<forall> z \<in> x. z \<in> y)"

axiomatization where
  power_set_axiom: "\<exists> z. \<forall> y. y \<in> z \<longleftrightarrow> y \<subseteq> x" and
  replacement_axiom: "\<exists> t. \<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z = F y)" and
  infinity_axiom: "\<exists> x. (\<exists> y \<in> x. \<forall> z. z \<notin> y) \<and> (\<forall> y \<in> x. \<exists> z \<in> x. \<forall> w. w \<in> z \<longleftrightarrow> (w \<in> y \<or> w = y))" and
  regularity_axiom: "y \<in> x \<Longrightarrow> (\<exists> y \<in> x. \<forall> z \<in> y. z \<notin> x)"

(* Все аксиомы, кроме аксиомы выбора, введены. Больше никаких axiomatization, кроме аксиомы выбора *)

(* 4. Development of set theory *)

lemma ext_iff: "x = y \<longleftrightarrow> (\<forall> z. z \<in> x \<longleftrightarrow> z \<in> y)"
using ext by auto

lemma the_set:
  assumes "\<forall> y. y \<in> x \<longleftrightarrow> P y"
  shows "(THE z. \<forall> y. y \<in> z \<longleftrightarrow> P y) = x"
by (step, insert assms ext, auto)

definition all :: "set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> set" where
  all_def: "all A P = (THE x. \<forall> y. y \<in> x \<longleftrightarrow> (y \<in> A \<and> P y))"

syntax
  "_Collect" :: "[pttrn, set, bool] \<Rightarrow> set"
translations
  "{x\<in>A. P}" \<rightleftharpoons> "CONST all A (\<lambda> x. P)"

lemma all_prop: "y \<in> all A P \<longleftrightarrow> (y \<in> A \<and> P y)"
proof -
  define \<phi> where phi_def: "\<phi> y = (y \<in> A \<and> P y)" for y
  hence "\<forall> y. \<phi> y \<longrightarrow> y \<in> A" by auto
  hence "\<exists> x. \<forall> y. y \<in> x \<longleftrightarrow> \<phi> y" using separation_axiom by auto
  then obtain x where "\<forall> y. y \<in> x \<longleftrightarrow> \<phi> y" by auto
  hence 1: "\<forall> y. y \<in> x \<longleftrightarrow> (y \<in> A \<and> P y)" using phi_def by auto
  thus ?thesis using the_set and all_def by auto
qed

lemma all_subset: "all A P \<subseteq> A"
unfolding subset_def and all_prop by auto

definition empty :: set ("0") where
  empty_def: "0 = {x \<in> undefined. False}"

lemma empty_prop: "x \<notin> 0" unfolding empty_def using all_prop by auto

lemma empty_false: "x \<in> 0 \<longleftrightarrow> False" using empty_prop by auto

lemma empty_iff: "x = 0 \<longleftrightarrow> (\<forall> y. y \<notin> x)" proof
  assume "x = 0"
  thus "\<forall> y. y \<notin> x" using empty_prop by auto
next
  assume "\<forall> y. y \<notin> x"
  thus "x = 0" using ext empty_prop by auto
qed

lemma reg:
  assumes "x \<noteq> 0"
  shows "\<exists> y \<in> x. \<forall> z \<in> y. z \<notin> x"
using empty_iff and regularity_axiom and assms by auto

definition powerset :: "set \<Rightarrow> set" where
  powerset_def: "powerset x = (THE y. \<forall> z. z \<in> y \<longleftrightarrow> z \<subseteq> x)"

lemma powerset_prop: "z \<in> powerset x \<longleftrightarrow> z \<subseteq> x"
proof -
  obtain y where "\<forall> z. z \<in> y \<longleftrightarrow> z \<subseteq> x" using power_set_axiom by auto
  thus ?thesis unfolding powerset_def using the_set by auto
qed

lemma empty_in_powerset: "0 \<in> powerset x" unfolding powerset_prop and subset_def using empty_prop by auto

lemma x_in_powerset: "x \<in> powerset x" unfolding powerset_prop and subset_def by auto

definition replace :: "(set \<Rightarrow> set) \<Rightarrow> set \<Rightarrow> set" where
  "replace F x = (THE t. \<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z = F y))"

lemma replace_prop: "z \<in> replace F x \<longleftrightarrow> (\<exists> y \<in> x. z = F y)"
proof -
  obtain t where "\<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z = F y)" using replacement_axiom ..
  thus ?thesis unfolding replace_def using the_set by auto
qed

lemma in_replace:
  assumes "y \<in> x"
  shows "F y \<in> replace F x"
unfolding replace_prop using assms by auto

definition two :: "set \<Rightarrow> set \<Rightarrow> set" where
  two_def: "two x y = (THE z. \<forall> t. t \<in> z \<longleftrightarrow> (t = x \<or> t = y))"

lemma two_prop: "t \<in> two x y \<longleftrightarrow> (t = x \<or> t = y)"
proof -
  define z where "z = replace (% w. if w = 0 then x else y) (powerset (powerset 0))"

  have "0 \<in> powerset (powerset 0)" using empty_in_powerset by auto
  hence "(% w. if w = 0 then x else y) 0 \<in> z" unfolding z_def by (rule in_replace)
  hence 1: "x \<in> z" by auto

  have "powerset 0 \<in> powerset (powerset 0)" using x_in_powerset by auto
  hence "(% w. if w = 0 then x else y) (powerset 0) \<in> z" unfolding z_def using in_replace by metis
  moreover have "0 \<in> powerset 0" using empty_in_powerset by auto
  hence "powerset 0 \<noteq> 0" using empty_prop by metis
  ultimately have 2: "y \<in> z" by auto

  have "\<forall> t. t \<in> z \<longrightarrow> (t = x \<or> t = y)" unfolding z_def and replace_prop by auto
  hence "\<forall> t. t \<in> z \<longleftrightarrow> (t = x \<or> t = y)" using 1 and 2 by auto
  thus ?thesis unfolding two_def using the_set by auto
qed

definition union_all :: "set \<Rightarrow> set" where
  union_all_def: "union_all x = (THE t. \<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z \<in> y))"

lemma union_all_prop: "z \<in> union_all x \<longleftrightarrow> (\<exists> y \<in> x. z \<in> y)"
proof -
  obtain t where "\<forall> z. z \<in> t \<longleftrightarrow> (\<exists> y \<in> x. z \<in> y)" using union_axiom ..
  thus ?thesis unfolding union_all_def using the_set by auto
qed

definition union :: "set \<Rightarrow> set \<Rightarrow> set" (infixl "\<union>" 65) where
  union_def: "x \<union> y = union_all (two x y)"

lemma union_prop: "z \<in> x \<union> y \<longleftrightarrow> (z \<in> x \<or> z \<in> y)" unfolding union_def using union_all_prop and two_prop by auto

definition cons :: "set \<Rightarrow> set \<Rightarrow> set" where "cons x y = two x x \<union> y"

lemma cons_prop: "z \<in> cons x y \<longleftrightarrow> z = x \<or> z \<in> y" unfolding cons_def and two_prop and union_prop by auto

nonterminal "is"
syntax
  "" :: "set \<Rightarrow> is"  ("_")
  "_Enum" :: "[set, is] \<Rightarrow> is"  ("_,/ _")
  "_Finset" :: "is \<Rightarrow> set"  ("{(_)}")
translations
  "{x, xs}" == "CONST cons x {xs}"
  "{x}" == "CONST cons x 0"

lemma x_cons_x: "cons x (cons x y) = cons x y"
by (rule ext, unfold cons_prop, auto)

lemma x_eq_y:
  assumes "{x} = {y}"
  shows "x = y"
using assms [unfolded ext_iff, unfolded cons_prop, unfolded empty_false] by auto

lemma x_cons_y_eq_z:
  assumes "{x, y} = {z}"
  shows "x = z" and "y = z"
using assms [unfolded ext_iff, unfolded cons_prop, unfolded empty_false] by auto

definition pair :: "set \<Rightarrow> set \<Rightarrow> set" where
  "pair x y = {{x}, {x, y}}"

lemma pair_lemma:
  assumes "pair x x = pair z t"
  shows "x = z" and "x = t"
proof -
  have "pair x x = {{x}}" unfolding pair_def and x_cons_x by auto
  hence "{{x}} = {{z}, {z, t}}" unfolding assms unfolding pair_def by auto
  hence "{z, t} = {x}" using x_cons_y_eq_z by metis
  thus "x = z" and "x = t" using x_cons_y_eq_z by metis+
qed

lemma two_lemma:
  assumes "{x, y} = {z, t}"
  shows "(x = z \<and> y = t) \<or> (x = t \<and> y = z)"
using assms [unfolded ext_iff, unfolded cons_prop empty_false] by metis

lemma pair_prop: "pair x y = pair z t \<longleftrightarrow> (x = z \<and> y = t)"
proof
  assume 1: "pair x y = pair z t"
  hence "z = t \<longrightarrow> (x = z \<and> y = t)" using pair_lemma by metis
  moreover {
    have "{x} = {z} \<and> {x, y} = {z, t} \<or> {x} = {z, t} \<and> {x, y} = {z}" using 1 and two_lemma and pair_def by auto
    moreover assume "z \<noteq> t"
    hence "{x} \<noteq> {z, t}" using x_cons_y_eq_z by metis
    ultimately have 2: "{x} = {z} \<and> {x, y} = {z, t}" by auto
    hence "x = z" using x_eq_y by auto
    hence "x = z \<and> y = t" using 2 and two_lemma by auto
  }
  ultimately show "x = z \<and> y = t" by auto
qed auto

definition sc_def: "Sc x = x \<union> {x}"

(* 5. Ordinals *)

definition transitive :: "set \<Rightarrow> bool" where
  transitive_def: "transitive x \<longleftrightarrow> (\<forall> y \<in> x. y \<subseteq> x)"

definition ordinal :: "set \<Rightarrow> bool" where
  ordinal_def: "ordinal x \<longleftrightarrow> transitive x \<and> (\<forall> y \<in> x. transitive y)"

lemma zero_ordinal: "ordinal 0" unfolding ordinal_def and transitive_def and subset_def using empty_prop by auto

lemma next_ordinal:
  assumes "ordinal x"
  shows "ordinal (Sc x)"
proof (unfold ordinal_def, step)
  have "transitive x" using assms unfolding ordinal_def by auto
  thus "transitive (Sc x)" unfolding transitive_def and sc_def and subset_def and union_prop and cons_prop using empty_prop by auto
next
  fix y
  assume "y \<in> Sc x"
  hence "y = x \<or> y \<in> x" unfolding sc_def and union_prop and cons_prop using empty_prop by auto
  thus "transitive y" proof
    assume "y = x"
    thus "transitive y" using `ordinal x` unfolding ordinal_def by auto
  next
    assume "y \<in> x"
    thus "transitive y" using `ordinal x` unfolding ordinal_def by auto
  qed
qed

lemma ordinal_elem_is_ordinal:
  assumes "ordinal x" and "y \<in> x"
  shows "ordinal y"
proof (unfold ordinal_def, step)
  show "transitive y" using assms unfolding ordinal_def by auto
  fix z
  assume "z \<in> y"
  show "transitive z" proof (unfold transitive_def, step)
    fix t
    assume "t \<in> z"
    moreover have "z \<in> x" using `ordinal x` unfolding ordinal_def and transitive_def and subset_def using `z \<in> y` and `y \<in> x` by metis
    hence "transitive z" using `ordinal x` unfolding ordinal_def by auto
    ultimately show "t \<subseteq> z" unfolding transitive_def by auto
  qed
qed

lemma x_not_in_x: "x \<notin> x"
proof -
  have "x \<in> {x}" using cons_prop by auto
  hence "{x} \<noteq> 0" using empty_prop by auto
  then obtain y where y_def: "y \<in> {x} \<and> (\<forall> z \<in> y. z \<notin> {x})" using reg by auto
  hence "y = x" unfolding cons_prop using empty_prop by auto
  hence "\<forall> z \<in> x. z \<notin> {x}" using y_def by auto
  hence "\<forall> z \<in> x. z \<noteq> x" unfolding cons_prop by auto
  thus "x \<notin> x" by auto
qed

lemma ordinals_transitive:
  assumes "a \<in> b"
  assumes "b \<in> c"
  assumes "ordinal c"
  shows "a \<in> c"
using assms unfolding ordinal_def and transitive_def and subset_def by metis

(* 5.3. Theorem *)
(* Это трансфинитная индукция для всего класса ординалов целиком. Но тем не менее мы пока не доказали, что для любого множества есть биективный ему ординал, т. е. пока возможно, что все ординалы "маленькие", просто для этих "маленьких" ординалов мы что-то умеем доказывать по индукции *)
theorem th5_3:
  assumes "\<forall> a. ordinal a \<longrightarrow> ((\<forall> b \<in> a. \<phi> b) \<longrightarrow> \<phi> a)"
  assumes "ordinal a0"
  shows "\<phi> a0"
proof (rule ccontr)
  assume "\<not> \<phi> a0"
  define x where "x = {c \<in> a0. \<not> \<phi> c}"
  {
    assume "x = 0"
    hence "\<forall> c. c \<notin> x" using empty_prop by auto
    hence "\<forall> c \<in> a0. \<phi> c" unfolding x_def and all_prop by auto
    hence "\<phi> a0" using assms by auto
    hence False using `\<not> \<phi> a0` by auto
  }
  then obtain a where a_def: "a \<in> x \<and> (\<forall> z \<in> a. z \<notin> x)" using reg by auto
  {
    fix b
    assume "b \<in> a"
    moreover have "x \<subseteq> a0" using x_def and all_subset by auto
    hence "a \<in> a0" using a_def and subset_def by auto
    ultimately have "b \<in> a0" using ordinals_transitive and assms by blast
    moreover have "b \<notin> x" using `b \<in> a` and a_def by auto
    ultimately have "\<phi> b" unfolding x_def unfolding all_prop by auto
  }
  moreover have "ordinal a" using a_def unfolding x_def unfolding all_prop using `ordinal a0` and ordinal_elem_is_ordinal by auto
  ultimately have "\<phi> a" using assms by auto
  thus False using a_def unfolding x_def and all_prop by auto
qed