Theory ZFfin

(*  Author:     Štěpán Holub, Department of Algebra, Charles University
    Author:     Zuzana Haniková, Institute of Computer Science of the Czech Academy of Sciences
*)

chapter ‹Fragments of Zermelo-Fraenkel set theory without infinity›
theory ZFfin
imports Main
begin

text ‹We explore axiomatizations of the theory of hereditarily finite sets, their fragments and relationships between them.›

section Preliminaries

― ‹General auxiliary simplification rule›
lemma ex_or_iff_or [simp]: "(∃w. (w = x ∨ w = y) ∧ P u w) ⟷ (P u x ∨ P u y)"
   by blast

― ‹A tautology recording the behaviour of bounded quantifiers. The logical equivalence between the axiom schemata ‹regsch› and ‹epsind› below is a particular instance.›
lemma abstract_foundation_iff: "((∃x. P x) ⟶ (∃x. B x ∧ P x)) ⟷ (∀ x. B x ⟶ ¬ P x) ⟶ (∀ x. ¬ P x)"
  by auto

section ‹Signature›

subsection ‹Membership and basic set-theoretic notions›

locale set_signature =
  fixes membership :: "'a ⇒ 'a ⇒ bool" (infix "ε" 50)

begin

text ‹General relation between regularity schema and epsilon-induction scheme. Applying the above remark about B-induction and B-foundation›

thm abstract_foundation_iff[of "λ x. ¬ P x" "λ x. (∀ y. y ε x ⟶ (P y))", unfolded not_not, symmetric]
thm abstract_foundation_iff[of  "λ y. P y" "λ x. (∀ y. y ε x ⟶ ¬ (P y))", unfolded not_not]

subsection ‹Set theoretical notions›

text ‹We use "M" (as in "Menge") for our defined versions of set-theoretical concepts, built upon membership.›

definition subsetM :: "'a ⇒ 'a ⇒ bool" ("_ ⊆⇩M _" [51,51] 53) where
  "subsetM x y ≡ (∀ z. z ε x ⟶ z ε y)"

lemma subsetM_refl[simp]: "x ⊆⇩M x" 
  unfolding subsetM_def by blast

lemma subsetM_trans[simp]: assumes "x ⊆⇩M y" "y ⊆⇩M z" shows "x ⊆⇩M z"
  using assms subsetM_def by simp

definition proper_subsetM :: "'a ⇒ 'a ⇒ bool" ("_ ⊂⇩M _" [50,50] 50) where
  "proper_subsetM x y ≡ (∀ z::'a. z ε x ⟶ z ε y)  ∧ x ≠ y" 

named_theorems set_defs
lemmas[set_defs] = proper_subsetM_def subsetM_def 

lemma proper_subset_def': "x ⊂⇩M y ⟷ x ⊆⇩M y ∧ x ≠ y"
  unfolding set_defs by blast

lemma proper_subsetI: "x ⊆⇩M y ⟹ x ≠ y ⟹ x ⊂⇩M y"
  unfolding set_defs by blast

lemma proper_subsetM_irrefl[simp]: "¬ x ⊂⇩M x"
  unfolding set_defs by simp     

definition transM:: "'a ⇒ bool" where
 "transM x ≡ ∀ y. y ε x ⟶ y ⊆⇩M x "

text ‹Hilbert's description operator @{term The} is used to define sets that are determined by their elements. 
Resulting set-theoretic operations can and will be used in appropriate contexts only that guarantee
the existence of corresponding sets, and their unicity (provable with extensionality).›

definition collectM :: "('a ⇒ bool) ⇒ 'a"  where
 "collectM Q ≡ THE z . (∀ u . (u ε z ⟷ Q u))"

definition emptysetM ("∅") where 
  "emptysetM ≡ collectM (λ x. x ≠ x)"

definition separationM :: "'a ⇒ ('a ⇒ bool) ⇒ 'a" where
 "separationM y Q ≡ collectM (λ u. u ε y ∧ Q u)"

definition powersetM :: "'a ⇒ 'a" ("𝔓") where
  "powersetM x ≡ collectM (λ u. u ⊆⇩M x)"

definition binunionM :: "'a ⇒ 'a ⇒ 'a" (infixl "∪⇩M" 55) where
  "binunionM x y ≡ collectM (λ u. u ε x ∨ u ε y)"

definition intersectionM :: "'a ⇒ 'a ⇒ 'a" ("_ ∩⇩M _" [55,54] 60) where
  "intersectionM x y ≡ collectM (λ u. u ε x ∧ u ε y)"

lemma intersection_symm: "x ∩⇩M y = y ∩⇩M x"
  unfolding intersectionM_def by metis

definition unionM :: "'a ⇒ 'a" ("⋃⇩M")  where
  "unionM x ≡ collectM (λ u. (∃ v. v ε x ∧ u ε v))"

definition differenceM :: "'a ⇒ 'a ⇒ 'a" (" _ ∖⇩M _") where
  "differenceM x y ≡ collectM (λ u. u ε x ∧ ¬ u ε y )"

definition singletonM :: "'a ⇒ 'a" ("{_}⇩M" 70) where
  "singletonM x ≡ collectM (λ u. u = x)"

definition pairM :: "'a ⇒ 'a ⇒ 'a" ("{_,_}⇩M" [51,51] 60) where
  "pairM x y ≡ collectM (λ u. u = x ∨ u = y)"

― ‹Set successor. Also known as adjunction.›
definition setsucM :: "'a ⇒ 'a ⇒ 'a" ("𝔰𝔲𝔠") where
  "setsucM x y ≡ collectM (λ u. u ε x ∨ u = y)"

definition replaceM :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a" where
   "replaceM P x ≡ collectM (λ u. ∃ v. v ε x ∧ P v u)"

definition leastM :: "('a ⇒ bool) ⇒ 'a" ("⋂⇩M") where
 "leastM Q ≡ collectM (λ u. ∀ y. Q y ⟶ u ε y)"

text ‹Least transitive superset›
definition least_tsM :: "'a ⇒ 'a" where
  "least_tsM x = ⋂⇩M (λ y. transM y ∧ x ⊆⇩M y)"

definition ordered_pairM :: "'a ⇒ 'a ⇒ 'a" ("⟨_,_⟩" [51,51] 60) where
  "ordered_pairM a b ≡ {{a}⇩M,{a,b}⇩M}⇩M"

definition relationM :: "'a ⇒ bool" where
  "relationM x ≡ ∀ v. v ε x ⟶ (∃ a b. v = ⟨a,b⟩)"

definition rel_inverseM :: "'a ⇒ 'a" where
  "rel_inverseM r ≡ collectM (λ u. ∃ a b. ⟨a,b⟩ ε r ∧ u = ⟨b,a⟩)"

definition functionM :: "'a ⇒ bool" where
  "functionM x ≡ relationM x ∧  (∀ a b c. ⟨a,b⟩ ε x ∧ ⟨a,c⟩ ε x ⟶ b = c)"

lemma funD: "functionM f ⟹ ⟨a,b⟩ ε f ⟹ ⟨a,c⟩ ε f ⟹  b = c"
  unfolding functionM_def by blast

definition domM :: "'a ⇒ 'a" where
  "domM r ≡ collectM (λ u. ∃ v. ⟨u,v⟩ ε r)"

definition rngM :: "'a ⇒ 'a" where
  "rngM r ≡ collectM (λ u. ∃ v. ⟨v,u⟩ ε r)"

definition one_oneM :: "'a ⇒ bool" where
  "one_oneM f ≡ functionM f ∧  (∀ a b c. ⟨b,a⟩ ε f ∧ ⟨c,a⟩ ε f ⟶ b = c)"

lemma one_one_inj: "one_oneM f ⟹ ⟨b,a⟩ ε f ⟹ ⟨c,a⟩ ε f ⟹  b = c"
  unfolding one_oneM_def by blast

lemma one_oneI: assumes "∀ v. v ε f ⟶ (∃ a b. v = ⟨a,b⟩)" "(∀ a b c. ⟨b,a⟩ ε f ∧ ⟨c,a⟩ ε f ⟶ b = c)" "(∀ a b c. ⟨a,b⟩ ε f ∧ ⟨a,c⟩ ε f ⟶ b = c)"
  shows "one_oneM f"
  using assms unfolding one_oneM_def functionM_def relationM_def by blast+

lemma one_oneD1: "one_oneM f ⟹ ∀ v. v ε f ⟶ (∃ a b. v = ⟨a,b⟩)"
  unfolding one_oneM_def functionM_def relationM_def by blast

lemma one_oneD2: "one_oneM f ⟹ (∀ a b c. ⟨b,a⟩ ε f ∧ ⟨c,a⟩ ε f ⟶ b = c)"
  unfolding one_oneM_def functionM_def relationM_def by blast 

lemma one_oneD3: "one_oneM f ⟹ (∀ a b c. ⟨a,b⟩ ε f ∧ ⟨a,c⟩ ε f ⟶ b = c)"
  unfolding one_oneM_def functionM_def relationM_def by blast

definition set_equivalent :: "'a ⇒ 'a ⇒ bool" ("_ ≈⇩M _" [51,51] 52) where
  "set_equivalent x y ≡ (∃ f. one_oneM f ∧ x = domM f ∧ y = rngM f)"

definition cartesian_productM :: "'a ⇒ 'a ⇒ 'a"  ("_ ×⇩M _ " [51,51] 60) where
  "cartesian_productM x y ≡ collectM (λ u. ∃ v⇩1 v⇩2. v⇩1 ε x ∧ v⇩2 ε y ∧ u = ⟨v⇩1,v⇩2⟩)"

definition composeM :: "'a ⇒ 'a ⇒ 'a" ("_ ∘⇩M _" [51,51] 60) where
  "f ∘⇩M g = collectM (λ u. ∃ a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩)"

definition tarski_fin :: "'a ⇒ bool" where
   "tarski_fin x ≡ ∀ y. (∀ z. z ε y ⟶ z ⊆⇩M x) ⟶ (∃ z. z ε y) ⟶ (∃ z. z ε y ∧ ¬(∃ w. w ε y ∧ z ⊂⇩M w))"

lemma tarski_subset_tarski: assumes "tarski_fin x" "y ⊆⇩M x" shows "tarski_fin y"
  using assms unfolding tarski_fin_def subsetM_def by presburger

definition dedekind_fin :: "'a ⇒ bool" where
   "dedekind_fin x ≡ ∀ y. (y ⊂⇩M x ⟶ ¬ x ≈⇩M y)"

― ‹‹x› is regular if it contains no infinite ‹ε›-decreasing chain as a subset›
definition regular :: "'a ⇒ bool" where
   "regular x ≡ ∀ y. y ⊆⇩M x ⟶  (∃ z. z ε y) ⟶ (∃ z. z ε y ∧ (∀ v. ¬ (v ε z ∧ v ε y)))"

― ‹Ordinals and natural numbers›

definition epschain :: "'a ⇒ bool" where
  "epschain x ≡ transM x ∧ (∀ y z. y ε x ∧ z ε x ⟶ y ε z ∨ y = z ∨ z ε y)"

― ‹In theories that do not rely on the regularity axiom, ordinals are explicitly assumed not to contain infinite ‹ε›-decreasing chains›
definition ordM :: "'a ⇒ bool" where
  "ordM x ≡ epschain x ∧ regular x"

lemma ordM_I: "regular x ⟹ epschain x ⟹ ordM x"
  using ordM_def by blast

lemma ordM_regular[simp]: "ordM x ⟹ regular x"
  unfolding ordM_def by blast

lemma ordM_D1: "ordM x ⟹ y ε x ⟹ y ⊆⇩M x"
  using ordM_def unfolding transM_def epschain_def by blast

lemma ordM_trans: assumes "ordM v"  "w ε u" "u ε v"  shows "w ε v"
  using assms ordM_D1 subsetM_def by blast

lemma ordM_D2: "ordM x ⟹ y ε x ⟹ z ε x ⟹ y ε z ∨ y = z ∨ z ε y"
  using ordM_def epschain_def by blast

definition is_sucM :: "'a ⇒ bool" where
  "is_sucM x ≡ ∃ y. (∀ z. z ε x ⟷ z ε y ∨ z = y)" 

― ‹A natural number is an ordinal ‹x› such that: ‹x› and all its elements are either empty or a successor›
definition natM :: "'a ⇒ bool" where
  "natM x ≡ ordM x ∧ (∀ v. (v ε x ∨ v = x) ⟶ (∃ u. u ε v) ⟶ is_sucM v)"

lemma natM_I: "ordM x ⟹ is_sucM x ⟹ (⋀ v. ∃ u. u ε v ⟹ v ε x ⟹ is_sucM v) ⟹ natM x"
  unfolding natM_def by blast

lemma nat_is_suc: "natM x ⟹ ∃ u. u ε x ⟹ is_sucM x"
  unfolding natM_def by blast

lemma nat_mem_is_suc: "natM x ⟹ v ε x ⟹ ∃ u. u ε v ⟹ is_sucM v"
  unfolding natM_def by blast

lemma natM_D: "natM x ⟹ ordM x"
  using natM_def by blast

definition cardinality :: "'a ⇒ 'a ⇒ bool" where
  "cardinality x n ≡ natM n ∧ x ≈⇩M n"

lemmas[set_defs] = transM_def epschain_def ordM_def tarski_fin_def is_sucM_def natM_def functionM_def relationM_def one_oneM_def rngM_def domM_def regular_def cardinality_def set_equivalent_def

subsection ‹Set relations and properties›

text ‹We represent a set formula as the predicate it defines. 
A predicate assigns truth values to assignments. 
We consider countably many variables ‹x⇩i›, represented by natural numbers.
An assignment maps variables to elements of the domain, i.e., it maps ‹nat› to ‹'a›.
Predicates defined by set formulas are defined inductively.
›

inductive SetFormulaPredicate :: "((nat ⇒ 'a) ⇒ bool) ⇒ bool"
  where 
  SFP_mem: "⋀ m n. SetFormulaPredicate (λ Ξ. (Ξ m) ε (Ξ n))" ― ‹formula ‹x⇩m ε x⇩n››
| SFP_eq: "⋀ m n. SetFormulaPredicate (λ Ξ. (Ξ m) = (Ξ n))"  ― ‹formula ‹x⇩m = x⇩n››
| SFP_neg: "SetFormulaPredicate P ⟹ SetFormulaPredicate (λ Ξ. ¬ P Ξ)" ― ‹formula ‹¬ φ››
| SFP_disj: "SetFormulaPredicate P ⟹ SetFormulaPredicate Q 
        ⟹ SetFormulaPredicate (λ Ξ. P Ξ ∨ Q Ξ)"  ― ‹formula ‹φ ∨ ψ››
| SFP_all: "⋀ n. SetFormulaPredicate P ⟹ SetFormulaPredicate (λ Ξ. ∀ a. P (Ξ(n:=a)))"
    ― ‹formula ‹∀ x⇩n. φ››

named_theorems SFP_rules 
lemmas[SFP_rules] = SFP_mem SFP_eq SFP_neg SFP_disj SFP_all

text ‹Every set-theoretically definable predicate depends on finitely many values. Such values correspond to free variables.›

lemma bounded_free: assumes "SetFormulaPredicate P"
  shows "∃ m. ∀ Ξ Ξ'. (∀ i < m. Ξ i = Ξ' i) ⟶  P(Ξ) = P (Ξ')"
proof (rule SetFormulaPredicate.induct[OF assms, of "λ Q. (∃ m. ∀ Ξ Ξ'. (∀ i < m. Ξ i = Ξ' i) ⟶  Q(Ξ) = Q (Ξ'))"])
  let ?Q = "λ x. True"
  show "∃max. ∀Ξ Ξ'. (∀i< max. Ξ i = Ξ' i) ⟶ (Ξ m ε Ξ n) = (Ξ' m ε Ξ' n)" for m n :: nat
    by (rule exI[of _ "Suc(max m n)"]) force   
  show "∃max. ∀Ξ Ξ'. (∀i< max. Ξ i = Ξ' i) ⟶ (Ξ m = Ξ n) = (Ξ' m = Ξ' n)" for m n :: nat
    by (rule exI[of _ "Suc(max m n)"]) force   
next
  fix Q :: "(nat ⇒ 'a) ⇒ bool"
  assume "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'"
  then obtain m where "∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'"
    by blast
  then have "∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ (¬ Q Ξ) = (¬ Q Ξ')" 
    by simp
  thus "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ (¬ Q Ξ) = (¬ Q Ξ')"
    by blast
next
  fix Q R :: "(nat ⇒ 'a) ⇒ bool"
  assume "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'" "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ R Ξ = R Ξ'"
  then obtain max_Q max_R where "∀Ξ Ξ'. (∀i<max_Q. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'" "∀Ξ Ξ'. (∀i<max_R. Ξ i = Ξ' i) ⟶ R Ξ = R Ξ'"
    by blast
  hence "∀Ξ Ξ'. (∀i<(max max_Q max_R). Ξ i = Ξ' i) ⟶ (Q Ξ ∨ R Ξ) = (Q Ξ' ∨ R Ξ')"
    unfolding less_max_iff_disj by metis
  thus "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ (Q Ξ ∨ R Ξ) = (Q Ξ' ∨ R Ξ')"
    by blast
next
  fix Q :: "(nat ⇒ 'a) ⇒ bool" and n :: nat
  assume "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'"
  then obtain max where max: "(∀i<max. Ξ i = Ξ' i) ⟶ Q Ξ = Q Ξ'" for Ξ Ξ'
    by blast
  have "(∀i<max. Ξ i = Ξ' i) ⟶ (∀a. Q (Ξ(n := a))) = (∀a. Q (Ξ'(n := a)))" for Ξ Ξ'
    using max[of "Ξ(n := _)" "Ξ'(n := _)"] by force
  thus "∃m. ∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ (∀a. Q (Ξ(n := a))) = (∀a. Q (Ξ'(n := a)))"  
    by blast
qed

―‹Renaming variables in any way (not necessarily permuting them) preserves the property of being a set-theoretically definable predicate.›
lemma transform_variables: assumes "SetFormulaPredicate P"
  shows "SetFormulaPredicate (λ Ξ. P (λ n. Ξ(f n)))"
  using assms
proof(induction arbitrary: f rule:  SetFormulaPredicate.inducts)
  case (SFP_mem m n)
  then show ?case 
    using set_signature.SFP_mem by blast
next
  case (SFP_eq m n)
  then show ?case 
    using set_signature.SFP_eq  by blast
next
  case (SFP_neg P)                       
  then show ?case
    using SetFormulaPredicate.SFP_neg  by simp 
next
  case (SFP_disj P Q)
  then show ?case using SetFormulaPredicate.SFP_disj by simp
next
  case (SFP_all P n)
  then show ?case
  proof-
    obtain k  where k: "(∀i < k. Ξ i = Ξ' i) ⟹ P Ξ = P Ξ'" for Ξ Ξ' :: "nat ⇒ 'a"
      using bounded_free[OF ‹SetFormulaPredicate P›] by blast
    obtain M where M_bound: "(∀ b < k. f b < M)"
      using finite_imageI[OF finite_Collect_less_nat, of f k, unfolded finite_nat_set_iff_bounded]
      by blast
    let ?M = "Suc (M + n)"
    let ?Q = "λa Ξ. P ((λb. Ξ (f b))(n:=a))" 
    have M: "(∀i < ?M. Ξ i = Ξ' i) ⟹ ?Q a Ξ = ?Q a Ξ'" for Ξ Ξ' :: "nat ⇒ 'a" and a
      by (rule k[of "(λb. Ξ (f b))(n := a)" "(λb. Ξ' (f b))(n := a)"]) (use M_bound in auto) 
    have fsimp: "(λb. (Ξ(p := a)) ((f(n := p)) b)) = (λb. (Ξ(p := a)) (f b))(n:=a)"  for Ξ :: "nat ⇒ 'a"  and a p
      by auto
    have M_irrelevant: "P ((λb. (Ξ(?M := a)) (f b))(n := a)) =  P ((λb. Ξ (f b))(n := a))" for Ξ a
      by (rule M) simp
    show ?thesis
      using set_signature.SFP_all[OF SFP_all(2)[of "f(n:=?M)"], of ?M]
      unfolding fsimp M_irrelevant. 
  qed
qed

lemma update_variable[intro]: assumes "SetFormulaPredicate P"
  shows "SetFormulaPredicate (λ Ξ. P(Ξ(n:= Ξ m)))"
proof-
  have aux: "(λ a. Ξ ((id(n:=m)) a)) = (Ξ (n:=Ξ m))" for Ξ :: "nat ⇒ 'a"
    by force
  show ?thesis
    by (rule transform_variables[OF assms, of "id (n:=m)", unfolded aux]) 
qed

lemma swap_variables: assumes "SetFormulaPredicate P"
  shows "SetFormulaPredicate (λ Ξ. P (Ξ(k := Ξ l, l := Ξ k)))"
proof-
  have "(λn. Ξ ((id(k := l, l := k)) n)) = Ξ(k := Ξ l, l := Ξ k)" for Ξ :: "nat ⇒ 'a"
    by fastforce
  from transform_variables[OF assms, of "id(k:=l,l:=k)", unfolded this]
  show ?thesis.
qed

text ‹A rule allowing to get rid of quantifiers when proving that a predicate is a ‹SetFormulaPredicate››

lemma sfp_all_rule4 [SFP_rules]: assumes "⋀ m. SetFormulaPredicate (λ Ξ. Q (Ξ m) (Ξ k1) (Ξ k2) (Ξ k3) (Ξ k4))" 
  shows "SetFormulaPredicate (λ Ξ. ∀ y. Q y (Ξ k1) (Ξ k2) (Ξ k3) (Ξ k4))"
  using SFP_all[OF assms, of "k1+k2+k3+k4+1" "k1+k2+k3+k4+1"] by simp

named_theorems logsimps
lemmas[logsimps] = not_not
lemma reduce_ex [logsimps]: "(λΞ. (∃z. Q z Ξ)) = (λΞ. ¬ (∀ z. ¬ (Q z Ξ)))"
  by blast
lemma reduce_and [logsimps]: "(λ Ξ. (P Ξ) ∧ (Q Ξ)) = (λ Ξ. (¬ ((¬ (P Ξ)) ∨ (¬ (Q Ξ)))))"
  by blast
lemma reduce_imp[logsimps]: "(λ Ξ. (P Ξ) ⟶ (Q Ξ)) = (λ Ξ. (¬ (P Ξ) ∨ (Q Ξ)))"
  by blast
lemma reduce_iff[logsimps]: "(λ Ξ. (P Ξ) ⟷ (Q Ξ)) = (λΞ. ¬ (¬ (¬ P Ξ ∨ Q Ξ) ∨ ¬ (¬ Q Ξ ∨ P Ξ)))"
  unfolding iff_conv_conj_imp unfolding logsimps  by blast
  
lemma SFP_const[intro,simp]: "SetFormulaPredicate (λΞ. b)"
  by (induct b) (use SFP_eq[of 0 0] SFP_neg[OF SFP_eq[of 0 0]] in force)+ 

lemma SFP_ex: assumes "SetFormulaPredicate P" shows "SetFormulaPredicate (λ Ξ. (∃ z. P (Ξ (m := z))))"
  unfolding logsimps by (rule SFP_neg, rule SFP_all, rule SFP_neg, fact)

lemma SFP_replace: assumes "SetFormulaPredicate P" and fresh_m: "∀ Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶  P Ξ = P Ξ'"
  shows "SetFormulaPredicate(λΞ. ∃z. ∀v. (v ε z) = (∃u. u ε Ξ m ∧ P (Ξ (0:=u,1:=v))))"
proof-
  let ?f = "id(0:= m+1, 1:= m+2)"
  let ?P = "λ Ξ. P (Ξ(0 := Ξ(m+1),1:=Ξ(m+2)))"
  have idsimp: "(λn. Ξ (?f n)) = Ξ (0:= Ξ(m+1),1 :=Ξ(m+2))" for Ξ :: "nat ⇒ 'a" by fastforce
  have Psimp: "P (Ξ(m + 3 := z, m + 2 := v, m + 1 := u, 0 := (Ξ(m + 3 := z, m + 2 := v, m + 1 := u)) (m + 1),1 := (Ξ(m + 3 := z, m + 2 := v, m + 1 := u)) (m + 2))) 
    = P (Ξ (0:=u,1:=v))" for Ξ v u z 
    by (rule fresh_m[rule_format]) force    
  have sfp: "SetFormulaPredicate ?P"
    using transform_variables[OF assms(1), of ?f] unfolding idsimp.
  have "SetFormulaPredicate (λΞ. ¬ Ξ (m+1) ε Ξ m ∨ ¬ ?P Ξ)"
    by (rule SFP_rules)+ fact
  from SFP_all[OF this, of "m+1", simplified fun_upd_same fun_upd_other]
  have "SetFormulaPredicate (λΞ. ∀z. ¬ z ε Ξ m ∨ ¬ ?P (Ξ(m + 1 := z)))"
    unfolding logsimps by simp
  have "SetFormulaPredicate (λ Ξ. (Ξ (m+2) ε Ξ (m+3)) = (∃u. u ε Ξ m ∧ ?P (Ξ(m+1 := u))))"
    unfolding logsimps by (rule SFP_rules | fact)+
  from SFP_all[OF this, of "m+2", simplified fun_upd_same fun_upd_other]
  have "SetFormulaPredicate (λΞ. ∀a. (a ε Ξ (m + 3)) = (∃u. u ε Ξ m ∧ ?P (Ξ(m + 2 := a, m + 1 := u))))" by simp
  note aux = SFP_all[OF SFP_neg[OF this], of "m+3", simplified fun_upd_same fun_upd_other]
  have " SetFormulaPredicate
   (λΞ. ∃ z. (∀v. (v ε z) = (∃u. u ε Ξ m ∧ ?P (Ξ(m + 3 := z, m + 2 := v, m + 1 := u)))))"
    unfolding logsimps using SFP_neg[OF aux[unfolded logsimps]] by simp  
  then show "SetFormulaPredicate (λΞ. ∃z. ∀v. (v ε z) = (∃u. u ε Ξ m ∧ P (Ξ(0 := u, 1 := v))))"
    unfolding Psimp.
qed

text ‹A (binary) relation is set-theoretically definable if the predicate it defines by assigning values to variables ‹x⇩0› and ‹x⇩1› is set-theoretically definable. 
The value of the relation therefore cannot depend on other variables than ‹x⇩0› and ‹x⇩1›. In other words, if a formula ‹φ› defining a set-theoretically definable relation contains a free variable ‹x⇩k, 1 < k›, then it is equivalent to ‹∀ x⇩k. φ› ›

definition SetRelation :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
  where
   "SetRelation P ≡ SetFormulaPredicate (λ Ξ. P (Ξ 0) (Ξ 1))"

text ‹A set-theoretically definable property is defined similarly.›

definition SetProperty :: "('a ⇒  bool) ⇒ bool"
  where
   "SetProperty P ≡ SetFormulaPredicate (λ Ξ. P (Ξ 0))"

subsubsection ‹Auxiliary proofs for specific useful set-relations and set-properties›

lemma SR_neg[simp, intro]: "SetRelation P ⟹ SetRelation (λ x y. ¬ P x y)"
  unfolding SetRelation_def by (rule SFP_rules)

lemma SR_sym[simp, intro]: assumes "SetRelation P" shows "SetRelation (λ x y. P y x)"
  using swap_variables[OF assms[unfolded SetRelation_def], of 0 1, simplified fun_upd_same fun_upd_other]
  unfolding SetRelation_def.

lemma SR_neq[simp]: "SetRelation (≠)"
  unfolding SetRelation_def using SFP_eq SFP_neg by blast

lemma SP_const[simp]: "SetProperty (λ x. b)"
  unfolding SetProperty_def using SFP_const.
     
lemma SP_neg[simp, intro]: "SetProperty P ⟹ SetProperty (λ x. ¬ P x)"
  unfolding  SetProperty_def using SFP_neg. 

lemma SP_tarski[simp]: "SetProperty tarski_fin"
  unfolding SetProperty_def  logsimps set_defs by (rule SFP_rules)+

lemma SP_setsuc[simp]: "SetProperty is_sucM"
  unfolding SetProperty_def  logsimps set_defs by (rule SFP_rules)+

lemma SP_nat[simp]: "SetProperty natM"
  unfolding SetProperty_def  logsimps set_defs by (rule SFP_rules)+

lemma empty_mem_ord': assumes "ordM x" "∃ z. z ε x" 
  shows "∃ emp. (∀ u. ¬ u ε emp) ∧ emp ε x" 
proof-
  obtain u where "u ε x" "∀ y. y ε u ⟶ ¬ y ε x"
    using ‹ordM x›  ‹∃ z. z ε x› ordM_def regular_def subsetM_refl by metis
  have "y ε u ⟶ y ε x" for y
    using ‹ordM x› ‹u ε x› ordM_D1 subsetM_def by blast 
  hence "¬ y ε u" for y
    using ‹∀ y. y ε u ⟶ ¬ y ε x› by simp
  then show ?thesis
    using ‹u ε x› by blast  
qed

end

section ‹Axiomatizations of hereditarily finite sets›

subsection ‹Finiteness axioms›

text ‹The aim of each of the axioms is to guarantee that each element of the domain will be finite.›

text ‹Usual axiom: there is no inductive set.›
locale L_fin = set_signature + 
   assumes fin: "¬ (∃ x. ∅ ε x ∧ (∀ y. y ε x ⟶ setsucM y y ε x))"

text ‹Induction schema for set formulas, a.k.a. set induction schema or just set induction. 
Not to be confused with epsilon induction.›
locale L_setind = set_signature +
  assumes setind: "⋀ P. SetFormulaPredicate P ⟹ 
    P(Ξ(0:= ∅)) ⟶ (∀ x y. P(Ξ(0:= x)) ⟶ P (Ξ(0:= setsucM x y))) ⟶ (∀ x. P(Ξ(0:= x)))"
begin

lemma setind_SP:   assumes "SetProperty P" and "P ∅" and step:  "∀ x y. P x ⟶ P (setsucM x y)"
  shows  "P x"
  using setind[of "λ Ξ. P (Ξ 0)", folded SetProperty_def, OF assms(1), simplified] ‹P ∅› step by blast  

lemma setind_var:   assumes "SetFormulaPredicate P" "P(Ξ(n:= ∅))" and step: "∀ x y. P(Ξ(n:= x)) ⟶ P (Ξ(n:= setsucM x y))"
  shows "P(Ξ(n:= x))"
proof-
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where m_def: "P Ξ = P Ξ'" if "∀i<m. Ξ i = Ξ' i" for Ξ Ξ'
    by blast
  let ?f = "id(0 := Suc (n + m), n:= 0)"
  let ?Q = "λ Ξ. (P (λ b. Ξ (?f  b)))"
  let ?X = "Ξ(Suc (n + m):= Ξ 0)"
  have sfpq:  "SetFormulaPredicate ?Q"
    using transform_variables[OF ‹SetFormulaPredicate P›] by simp
  have small: "∀ i < m. (?X (0 := u)) (?f i) = (Ξ(n := u)) i" for u
    by auto
  have equiv: "(?Q (?X (0 := u))) ⟷ (P (Ξ(n := u)))" for u
    by (rule m_def[of  "λ b. (?X (0 := u))(?f b)" "Ξ(n := u)"]) (rule small) 
  show "P(Ξ(n:= x))"
   unfolding equiv[symmetric]
   by (rule setind[rule_format, OF sfpq, of ?X], unfold equiv)
   (use assms in blast)+
qed

end

locale L_dedekind = set_signature + 
   assumes dedekind: "∀ x. dedekind_fin x"

locale L_tarski = set_signature + 
  assumes tarski: "∀ y. tarski_fin y"

subsection Extensionality

locale L_setext = set_signature +
  assumes setext: "x = y ⟷ (∀ z. z ε x ⟷ z ε y)"

begin

text ‹set in HOL is defined as a class. Therefore, the following comprehension is an axiom.›
lemma "x ∈ {u. P u} ⟷ P x"
   using mem_Collect_eq.

text ‹In case of (our) M-sets, only uniqueness, not existence is guaranteed by extensionality.›

lemma collect_def': 
  assumes "∀ u. (u ε w ⟷ Q u)"
  shows "collectM Q = w"
proof-
  let ?P = "λ z. (∀ u. u ε z ⟷ Q u)"
  have unique: "z' = w" if "?P z'" for z'
    unfolding setext[rule_format, of z' w] 
    using that assms by blast
  then show ?thesis
    using theI[of ?P w, OF assms unique] unfolding collectM_def by blast 
qed

lemma collect_def_ex: ― ‹A formulation useful in proofs›
  assumes "∃ w. ∀ u . (u ε w ⟷ Q u)"
  shows "u ε collectM Q ⟷ Q u"
  using assms collect_def' assms by auto

lemma proper_subset_diff[simp] : "y ⊂⇩M x ⟹ ∃ z. z ε x ∧ ¬ z ε y" 
  unfolding proper_subsetM_def setext by blast

lemma subsetM_antisym: "y ⊆⇩M x ⟹ x ⊆⇩M y ⟹ x = y" 
  unfolding subsetM_def setext by blast

lemma proper_subsetM_trans[simp]: assumes "x ⊂⇩M y" "y ⊂⇩M z" shows "x ⊂⇩M z"
proof (unfold proper_subsetM_def, rule conjI)
  show "(∀ u. u ε x ⟶ u ε z)"
    using assms proper_subsetM_def by simp
  show "x ≠ z"
    by (rule notI) (use assms proper_subsetM_def  setext[of z y] in auto)
qed

lemma emptyset_mem_ord: assumes "ordM x" "∃ z. z ε x" shows "∅ ε x"
  using empty_mem_ord'[OF assms] collect_def'[of _ "λ x. x ≠ x"] emptysetM_def by force

end                                                        
                                             
subsection ‹Empty set›  

locale L_empty = set_signature + 
  assumes empty: "∃ x. ∀ y. (¬ y ε x)"

text ‹Since the empty set is defined@{term collectM}, and hence Hilbert's @{term The}, nothing useful can be said about ‹∅› without extensionality.›
locale L_setext_empty = L_setext + L_empty

begin

― ‹Here we can already prove that @{term ∅}, has the intended meaning.›
lemma empty_is_empty[simp]: "∀ y. (¬ y ε ∅)"
proof-
  have ex: "∃ x. ∀ z. z ε x ⟷ z ≠ z"
    using empty by auto
  from collect_def_ex[OF this, folded emptysetM_def]
  show ?thesis 
    unfolding emptysetM_def collectM_def by auto
qed

lemma emptyset_def'[set_defs]: "x = ∅ ⟷ (∀ u. ¬ u ε x)"
  unfolding setext by simp

lemma empty_mem_false [set_defs]: "u ε ∅ ⟷ False"
  using emptyset_def'  by simp

lemma setsuc_empty_sing:  "setsucM ∅ x = {x}⇩M"
  unfolding singletonM_def setsucM_def empty_mem_false by simp

lemma SFP_empty_n [simp]: "SetFormulaPredicate (λΞ. Ξ n = ∅)"
  unfolding SetProperty_def  logsimps set_defs by (rule SFP_rules)+

lemma SP_empty[simp]: "SetProperty (λx. x = ∅)"
  unfolding SetProperty_def by simp

lemma SFP_empty_n' [simp]: "SetFormulaPredicate (λΞ. ∀u. ¬ u ε Ξ n)"
  using SFP_empty_n emptyset_def' by simp

lemma empty_dedekind[simp]: shows "dedekind_fin ∅"
  unfolding dedekind_fin_def set_defs by auto

lemma subset_of_empty[simp]: "u ⊆⇩M ∅ ⟷ u = ∅"
  unfolding subsetM_def emptyset_def' by simp

lemma empty_tarski[simp]: shows "tarski_fin ∅"
  unfolding tarski_fin_def proper_subsetM_def by auto

lemma nemp_setI[intro]: "x ε y ⟹ y ≠ ∅"
  by force

lemma nemp_setI_ex: "∃ x. x ε y ⟹ y ≠ ∅"
  by force

lemma empty_is_subset: "∅ ⊆⇩M A"
  unfolding subsetM_def by force

lemma empty_regular[simp]: "regular ∅"
  unfolding regular_def by simp

lemma empty_trans[simp]: "transM ∅"
  unfolding transM_def by simp

lemma emp_natM[simp]: "natM ∅"
  by (simp add: natM_def ordM_def epschain_def) 

lemma binunion_emp[simp]: "∅ ∪⇩M t = t" "t ∪⇩M ∅ = t"
  unfolding setext[of _ t] binunionM_def using empty_is_empty
    collect_def'[of t "λ u. u ε t"] by simp_all

end

subsection ‹Set pair›

text ‹Pairing is a simple set construction which can be easily obtained by set successor and empty set. It is interesting on its own, in particular in a context without the empty set axiom.›

locale L_pair = set_signature + 
  assumes pair: "∀ x y. ∃ z. ∀ v. v ε z ⟷ v = x ∨ v = y"

locale L_setext_pair = L_setext + L_pair

begin

lemma singleton_def'[set_defs]: "u ε {y}⇩M ⟷  u = y"
proof-
  have "∃ x. ∀ u. u ε x ⟷  u = y" 
    using pair by meson
  from collect_def_ex[OF this[rule_format], folded singletonM_def]
  show ?thesis.
qed

lemma singleton_eq[set_defs]: "u = {y}⇩M ⟷  (∀ v. v ε u ⟷ v = y)"
  unfolding setext  set_defs by blast

lemma pair_def'[set_defs]: "u ε {x,y}⇩M ⟷ u = x ∨ u = y"
  using collect_def_ex[OF pair[rule_format], folded pairM_def].

lemma pair_eq [set_defs]: "w = {x,y}⇩M ⟷ (∀ u. (u ε w) ⟷  u = x ∨ u = y)"
  unfolding setext[of w] set_defs by simp 

lemma regular_not_self_mem: assumes "regular x" shows "¬ x ε x"
proof
  assume "x ε x"
  with assms[unfolded regular_def, rule_format, of "{x}⇩M"]
  show False
    unfolding subsetM_def singleton_def' by blast
qed

lemma ordered_pair_unique[simp]: "⟨u,v⟩ = ⟨u',v'⟩ ⟷ u = u' ∧ v = v'"
  unfolding setext[of "{_,_}⇩M"] ordered_pairM_def using pair_def' singleton_def' by metis 

lemma sing_eq_iff: "{a}⇩M = {b}⇩M ⟷ a = b"
  unfolding setext[of "{_}⇩M"] singleton_def' by metis 

lemma sing_eq_pair_iff: "{a}⇩M = {b,c}⇩M ⟷ a = b ∧ b = c" 
  unfolding setext[of "{_}⇩M"] pair_def' singleton_def' by metis 

lemma sing_eq_pair_iff': "{b,c}⇩M = {a}⇩M ⟷ a = b ∧ b = c" 
  using sing_eq_pair_iff by metis

lemma SFP_mem_ordered_pair[SFP_rules]: "SetFormulaPredicate (λ Ξ. Ξ k ε ⟨Ξ l, Ξ m⟩)"
  unfolding ordered_pairM_def set_defs logsimps by (rule SFP_rules)+

lemma SFP_eq_ordered_pair [SFP_rules]: "SetFormulaPredicate (λ Ξ. Ξ k = ⟨Ξ l,Ξ m⟩)"
  unfolding setext logsimps by (rule SFP_rules)+

lemma SFP_ordered_pair_mem[SFP_rules]: "SetFormulaPredicate (λΞ. ⟨Ξ k,Ξ l⟩ ε Ξ m)"
proof-
  have "SetFormulaPredicate (λΞ. ∃ u. u = ⟨Ξ k,Ξ l⟩ ∧ u ε Ξ m)"
    unfolding setext logsimps by (rule SFP_rules)+
  thus ?thesis
    by simp
qed   

end

subsection ‹Set successor›

text ‹Also known as adjunction. Enables constructing sets in steps. This axiom plays an important role in the fragment of set theory axiomatized by extensionality, empty set and set successor (see  ‹L_setext_empty_setsuc› below), mutually interpretable with Robinson's arithmetic Q.›

locale L_setsuc = set_signature + 
  assumes setsuc: "∀ x y. ∃ z. ∀ u. u ε z ⟷ u ε x ∨ u = y"


locale L_setext_setsuc  = L_setext + L_setsuc 
― ‹some statements  do not need the empty set›

begin

lemma setsuc_def'[set_defs, simp]: "u ε setsucM x y ⟷ (u ε x ∨ u = y)"
  using collect_def_ex[OF setsuc[rule_format]] unfolding setsucM_def.

lemma setsuc_triv[simp]: "y ε x ⟹ setsucM x y = x"
   unfolding setext[of _ x] setsuc_def' by blast

lemma is_suc_def': "is_sucM x ⟷ (∃ y. x = setsucM y y)"
  unfolding is_sucM_def setsuc_def' setext..

lemma trans_suc_trans: "transM  x ⟹ transM (setsucM x x)"
  unfolding transM_def set_defs by blast

lemma epschain_suc_epschain: "epschain  x ⟹ epschain (setsucM x x)"
  unfolding epschain_def  using trans_suc_trans
  using setsuc_def' by auto

lemma ord_pred_fun: assumes "ordM x" "ordM y" "setsucM x x = setsucM y y" 
  shows "x = y"
  using assms unfolding setext[of x] setext[of "setsucM x x"] set_defs by metis

lemma SFP_setsuc_mem[SFP_rules]: "SetFormulaPredicate (λΞ. Ξ k ε setsucM (Ξ l) (Ξ m))"
  unfolding  setsuc_def'  by (rule SFP_rules)+ 

lemma SFP_setsuc_eq[SFP_rules]: "SetFormulaPredicate (λΞ. Ξ k = setsucM (Ξ l) (Ξ m))"
  unfolding setsuc_def' setext logsimps by (rule SFP_rules)+ 

end

locale L_empty_setsuc  = L_empty + L_setsuc 
― ‹some statements do not need extensionality›

begin

sublocale L_pair
proof (unfold_locales, rule allI, rule allI)
  fix x y
  obtain empty where emp: "∀ u. ¬ u ε empty"
    using empty by blast
  obtain sing where "∀ u. u ε sing ⟷  u = x"
    using setsuc[rule_format, of empty x] emp by blast
  then obtain pair where "∀v. (v ε pair) = (v = x ∨ v = y)" 
    using setsuc[rule_format, of sing y] by blast
  then show "∃z. ∀v. (v ε z) = (v = x ∨ v = y)"
    by blast
qed

lemma singleton_setsuc: shows "∃ y. ∀ u. u ε y ⟷ u = z"
proof-
  obtain emp where "∀ u. ¬ u ε emp"
    using empty by blast 
  then show ?thesis
    using setsuc[rule_format, of emp z] by blast 
qed

lemma pair_setsuc: shows "∃ y. ∀ u. u ε y ⟷ u = z⇩1 ∨ u = z⇩2"
proof-
  obtain z1 where "∀ u. u ε z1 ⟷ u = z⇩1"
    using singleton_setsuc by blast 
  then show ?thesis
    using setsuc[rule_format, of z1 z⇩2] by simp
qed

lemma triple_setsuc:  shows "∃ y. ∀ u. u ε y ⟷ u = z⇩1 ∨ u = z⇩2 ∨ u = z⇩3"
proof-
  obtain z2 where "∀ u. u ε z2 ⟷ u = z⇩1 ∨ u = z⇩2"
    using pair_setsuc by blast 
  then show ?thesis
    using setsuc[rule_format, of z2 z⇩3] by simp
qed

lemma regular_antisym_mem: assumes "regular x" "z⇩1 ε x" "z⇩2 ε x" shows "¬ (z⇩1 ε z⇩2 ∧ z⇩2 ε z⇩1)"
proof
  obtain pair where pair: "∀ u. u ε pair ⟷ u = z⇩1 ∨ u = z⇩2"
    using pair_setsuc by blast
  assume "z⇩1 ε z⇩2 ∧ z⇩2 ε z⇩1"
  with ‹regular x›[unfolded regular_def, rule_format, of pair]
  show False
     unfolding subsetM_def using ‹z⇩1 ε x› ‹z⇩2 ε x› pair by auto 
qed

lemma regular_antisym2_mem: assumes "regular x" "z⇩1 ε x" "z⇩2 ε x" "z⇩3 ε x" shows "¬ (z⇩1 ε z⇩2 ∧ z⇩2 ε z⇩3 ∧ z⇩3 ε z⇩1)"
proof
  obtain triple where triple: "∀ u. u ε triple ⟷ u = z⇩1 ∨ u = z⇩2 ∨ u = z⇩3"
    using triple_setsuc by blast
  assume "z⇩1 ε z⇩2 ∧ z⇩2 ε z⇩3 ∧ z⇩3 ε z⇩1"
  with ‹regular x›[unfolded regular_def, rule_format, of triple]
  show False
     unfolding subsetM_def using ‹z⇩1 ε x› ‹z⇩2 ε x› ‹z⇩3 ε x› triple by auto 
qed

lemma ord_mem_ord: assumes  "ordM v" "u ε v" shows "ordM u"
  unfolding ordM_def epschain_def conj_assoc[symmetric]
proof (rule conjI, rule conjI)
  have "regular v" "u ⊆⇩M v"
    using ‹ordM v› ordM_D1 ‹u ε v› ordM_def by blast+
  then show "regular u"
    unfolding regular_def using subsetM_trans[OF _ ‹u ⊆⇩M v›] by blast
  have "u ⊆⇩M v" "epschain v" "regular v" "transM v"
    using assms unfolding natM_def ordM_def transM_def epschain_def by blast+
  thus "∀y z. y ε u ∧ z ε u ⟶ y ε z ∨ y = z ∨ z ε y"
    using ‹ordM v› unfolding ordM_def subsetM_def epschain_def by blast
  show "transM u"
    unfolding transM_def set_defs
  proof (rule allI, rule impI, rule allI, rule impI)
    fix z y
    assume "y ε u" "z ε y"
    hence "z ε v" "y ε v" 
      using ‹u ε v› ‹transM v› unfolding transM_def set_defs by blast+
    have "u ≠ z"
      using regular_antisym_mem[OF ‹regular v› ‹y ε v› ‹z ε v›] ‹y ε u› ‹z ε y› by blast
    have "¬ u ε z"
      using regular_antisym2_mem[OF ‹regular v› ‹u ε v› ‹z ε v› ‹y ε v›] ‹y ε u› ‹z ε y› by blast
    show "z ε u"
      using ordM_D2[OF ‹ordM v› ‹u ε v› ‹z ε v›] ‹u ≠ z› ‹¬ u ε z› by blast
  qed
qed   

end

locale L_setext_empty_setsuc  = L_setext + L_empty + L_setsuc 

begin

sublocale L_setext_empty
 by unfold_locales

sublocale L_setext_setsuc
  by unfold_locales

sublocale L_empty_setsuc
  by unfold_locales

sublocale L_setext_pair
  by unfold_locales

lemma empty_mem_ord: assumes "ordM x" "x ≠ ∅" shows "∅ ε x"
proof-
  have "∃ z. z ε x"
    using ‹x ≠ ∅›  by (simp add: setext) 
  then obtain u where "u ε x" "∀ y. y ε u ⟶ ¬ y ε x"
    using ‹ordM x›  ordM_def regular_def subsetM_refl by metis
  have "y ε u ⟶ y ε x" for y
    using ‹ordM x› ‹u ε x› ordM_D1 subsetM_def by blast 
  hence "u = ∅"
    using ‹∀ y. y ε u ⟶ ¬ y ε x›
    by (simp add: emptyset_def') 
  then show "∅ ε x"
    using ‹u ε x› by blast  
qed

lemma SP_injective [simp]: "SetProperty (λx. ∀a b c. ⟨b,a⟩ ε x ∧ ⟨c,a⟩ ε x ⟶ b = c)"
  unfolding set_defs logsimps SetProperty_def by (rule SFP_rules)+

lemma SP_unique_image [simp]: "SetProperty (λx. ∀a b c. ⟨a,b⟩ ε x ∧ ⟨a,c⟩ ε x ⟶ b = c)"
  unfolding set_defs logsimps SetProperty_def by (rule SFP_rules)+

lemma SFP_compose [simp,intro]: "SetFormulaPredicate (λ Ξ. ∃a b c. ⟨a,b⟩ ε Ξ k ∧ ⟨b,c⟩ ε Ξ l ∧ Ξ m = ⟨a,c⟩)"
proof-
  have sfp: "SetFormulaPredicate (λ Ξ. ⟨Ξ (k+l+m+3),Ξ (k+l+m+4)⟩ ε Ξ k ∧ ⟨Ξ (k+l+m+4),Ξ (k+l+m+5)⟩ ε Ξ l ∧ Ξ m = ⟨Ξ (k+l+m+3), Ξ (k+l+m+5)⟩)"
    unfolding logsimps by (rule SFP_rules)+
  show ?thesis
    using SFP_ex[OF SFP_ex[OF SFP_ex], of _ "k+l+m+3" "k+l+m+4" "k+l+m+5", OF sfp] by simp 
qed

lemma SP_function[simp]: "SetProperty (λ x. functionM x)"
  unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+

lemma SP_one_one[simp]: "SetProperty (λ x. one_oneM x)"
  unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+

lemma dom_SR [simp]: "SetRelation (λx u. ∃w. x = ⟨u,w⟩)"
      unfolding SetRelation_def logsimps by (rule SFP_rules)+

lemma rng_SR [simp]: "SetRelation (λx u. ∃w. x = ⟨w,u⟩)"
      unfolding SetRelation_def logsimps by (rule SFP_rules)+

end 

locale L_binunion = set_signature + 
  assumes binunion: "∀ x y. ∃ z. ∀ v. v ε z ⟷ (v ε x ∨ v ε y)"

locale L_setext_binunion = L_setext + L_binunion 

begin

lemma binunion_def'[set_defs]: "u ε x ∪⇩M y ⟷ u ε x ∨ u ε y"
  unfolding binunionM_def
  using collect_def_ex[OF binunion[rule_format], of u]
  by force


end

locale L_setext_pair_binunion = L_setext + L_pair + L_binunion
― ‹A specific minimalist combination of axioms that guarantees the existence of both ordered pair and set successor›

begin

sublocale L_setext_binunion
  by unfold_locales

sublocale L_setext_pair
  by unfold_locales

sublocale  L_setsuc
proof (unfold_locales, (rule allI)+, rule exI, rule allI)
  show "u ε x ∪⇩M {y}⇩M ⟷ (u ε x ∨ u = y)" for x y u 
    unfolding binunion_def' singleton_def' by blast
qed

sublocale L_setext_setsuc
  by unfold_locales

lemma SFP_ordered_pair_setsuc_eq[SFP_rules]: "SetFormulaPredicate (λΞ. Ξ k = ⟨Ξ l, setsucM (Ξ m) (Ξ n)⟩)"
proof-
―‹An explicit proof avoiding too many quantifiers, beyond reach of @{thm sfp_all_rule4}›
  let ?Q = "λ Ξ. Ξ (m+n+l+k+1) = setsucM (Ξ m) (Ξ n) ∧ Ξ k = ⟨Ξ l,Ξ (m+n+l+k+1)⟩"
  thm SFP_ex[of ?Q "m+n+l+k+1", simplified]
  show ?thesis
    by (rule SFP_ex[of ?Q "m+n+l+k+1", simplified], unfold logsimps) (rule SFP_rules)+
qed

end

subsection Regularity

locale  L_reg = set_signature +
  assumes reg: "∀ x. (∃ y. y ε x) ⟶ (∃ y. y ε x ∧ (∀ v. ¬ (v ε y ∧ v ε x)))"

begin

lemma any_reg[simp]: "regular x"
  using reg unfolding regular_def by blast

text ‹Note that ‹¬ x ε x› cannot be proved without existence of a singleton.›

end

lemma (in set_signature) reg_all_regular_iff:
  "L_reg (ε) ⟷ (∀ x. regular x)"
proof
  assume "L_reg (ε)"
  then interpret L_reg "(ε)".
  show "∀ x. regular x"
    using reg unfolding regular_def by blast
next
  assume all_reg: "∀ x. regular x"
  show "L_reg (ε)"
    by unfold_locales (meson all_reg regular_def set_signature.subsetM_refl)  
qed

text ‹Schema of regularity›
locale L_regsch = set_signature +
  assumes regsch: "SetFormulaPredicate P ⟹ (∃ x. P (Ξ (0:=x))) ⟶  (∃ x. P (Ξ (0:=x)) ∧ (∀ y. y ε x ⟶ ¬ P (Ξ (0:=y))))"

begin

text ‹‹regsch› is stronger than normal regularity in the absence of infinity axiom, since one cannot prove the existence of transitive supersets/closures. See ‹not_reg_setind_implies_regsch› in‹ZFfin_regsch_model.thy››

sublocale L_reg
proof
  have SFP: "SetFormulaPredicate (λΞ. Ξ 0 ε Ξ 1)"
    by (rule SFP_rules)
  show "∀x. (∃y. y ε x) ⟶ (∃y. y ε x ∧ (∀v. ¬ (v ε y ∧ v ε x)))" 
    using regsch[OF SFP, unfolded fun_upd_apply] by force
qed

lemma regsch_epsind:
   "SetFormulaPredicate Q ⟹ (∀ x. (∀y. (y ε x ⟶ Q (Ξ (0:=y))))  ⟶  Q (Ξ (0:=x))) ⟶  (∀ x. Q (Ξ (0:=x)))"
  using regsch[of "λ x. ¬ Q x" Ξ] using SFP_neg by blast 

lemma regsch_mem_not_refl: "¬ u ε u"
proof
  assume "u ε u"
  hence ex: "∃x. (undefined(1 := u, 0 := x)) 0 = (undefined(1 := u, 0 := x)) 1"
    by force
  have sfp: "SetFormulaPredicate (λΞ. (Ξ 0) = (Ξ 1))"
    by (rule SFP_rules)
  from regsch[of "λ Ξ. (Ξ 0) = (Ξ 1)", rule_format, OF sfp ex]
  show False
    using ‹u ε u› by auto
qed

end 

text ‹Epsilon induction schema is logically equivalent to the regularity schema (that is, regardless of what ‹ε› means), see @{thm abstract_foundation_iff} above.›

locale L_epsind = set_signature + 
  assumes epsind: "SetFormulaPredicate Q ⟹ (∀ x. (∀y. (y ε x ⟶ Q (Ξ (0:=y))))  ⟶  Q (Ξ (0:=x))) ⟶  (∀ x. Q (Ξ (0:=x)))"

begin

lemma epsind_regsch: assumes "SetFormulaPredicate P" "∃ x. P (Ξ (0:=x))" 
  shows "∃ x. P (Ξ (0:=x)) ∧ (∀ y. y ε x ⟶ ¬ P (Ξ (0:=y)))"   
proof-
  have SP: "SetFormulaPredicate (λ x. ¬ P x)"
    using ‹SetFormulaPredicate P› by (simp add: SFP_rules)
  show ?thesis
    unfolding  abstract_foundation_iff[of "λ x. ∀ y. y ε x ⟶ ¬ P (Ξ(0:=y))" "λ x. ¬ P (Ξ(0:=x))", unfolded not_not]
    using  epsind[OF SP, rule_format, of Ξ] ‹∃ x. P (Ξ (0:=x))›
    by blast+
qed

sublocale L_regsch
  using epsind_regsch by unfold_locales blast

end 

subsection Separation

text ‹Separation is often an alternative to set successor. It allows one to construct ``from above'' many sets that set successor builds ``from below''.›

locale L_sep = set_signature + 
  assumes sep: "SetFormulaPredicate P ⟹ ∀x. ∃ z. ∀ u. (u ε z ⟷  u ε x ∧ P (Ξ(0:= u)))" 

begin

sublocale L_empty
  by unfold_locales (use sep[OF SFP_const[of False]] in force) 

lemma sep_var: assumes "SetFormulaPredicate P" shows "∀x. ∃ z. ∀ u. (u ε z ⟷  u ε x ∧ P (Ξ(n:= u)))"
  using sep[OF swap_variables, OF assms, of "Ξ(n:= Ξ 0)" n 0]
  by (cases "n = 0", simp) (simp del: neq0_conv add: fun_upd_twist[of n 0])

lemma sep_SP: assumes "SetProperty P" shows "∀x. ∃ z. ∀ u. (u ε z ⟷  u ε x ∧ P u)" 
  using sep[OF assms[unfolded SetProperty_def]] by simp

lemma sep_SR: assumes "SetRelation P" shows "∀x. ∃ z. ∀ u. (u ε z ⟷  u ε x ∧ P u r)" 
  using sep[OF assms[unfolded SetRelation_def]] by simp

lemma singleton_sep: assumes "z ε x"
  shows "∃ y. ∀ u. u ε y ⟷ u = z"
  using sep[rule_format, of "λΞ. Ξ 0 = Ξ 1" x "undefined(1:=z)", OF SFP_eq, unfolded fun_upd_apply] assms by auto

lemma pair_sep: assumes "z⇩1 ε x" "z⇩2 ε x"
  shows "∃ y. ∀ u. u ε y ⟷ u = z⇩1 ∨ u = z⇩2"
proof-
  have "SetFormulaPredicate (λΞ. Ξ 0 = Ξ 1 ∨ Ξ 0 = Ξ 2)"
    by (rule SFP_rules)+
  from sep[rule_format, OF this, of x "undefined(1:=z⇩1,2:=z⇩2)", simplified]
  show "∃y. ∀u. (u ε y) = (u = z⇩1 ∨ u = z⇩2)"
    using assms by blast
qed

lemma triple_sep: assumes "z⇩1 ε x" "z⇩2 ε x" "z⇩3 ε x"
  shows "∃ y. ∀ u. u ε y ⟷ u = z⇩1 ∨ u = z⇩2 ∨ u = z⇩3"
proof-
  have "SetFormulaPredicate (λΞ. Ξ 0 = Ξ (Suc 0) ∨ Ξ 0 = Ξ 2 ∨ Ξ 0 = Ξ 3)"
    by (rule SFP_rules)+
  from sep[rule_format, OF this, of x "undefined(1:=z⇩1,2:=z⇩2,3:=z⇩3)", simplified] 
  show "∃ y. ∀ u. u ε y ⟷ u = z⇩1 ∨ u = z⇩2 ∨ u = z⇩3" 
    using assms by blast    
qed

lemma regular_not_self_mem_sep: assumes "regular x" shows "¬ x ε x"
proof
  assume "x ε x"
  then obtain t where t: "∀ u. u ε t ⟷ u = x"
    using singleton_sep by blast 
  from assms[unfolded regular_def, rule_format, of t]
  show False
    unfolding subsetM_def t[rule_format] using ‹x ε x› by blast 
qed

lemma regular_antisym_mem_sep: assumes "regular x" "y⇩1 ε x" "y⇩2 ε x" shows "¬ (y⇩1 ε y⇩2 ∧ y⇩2 ε y⇩1)"
proof
  obtain t where t: "∀ u. u ε t ⟷ u = y⇩1 ∨ u = y⇩2"
    using pair_sep[OF assms(2-)] by blast
  assume "y⇩1 ε y⇩2 ∧ y⇩2 ε y⇩1"
  with ‹regular x›[unfolded regular_def, rule_format, of t]
  show False
     unfolding subsetM_def t[rule_format] using assms regular_def by blast 
qed

lemma regular_antisym2_mem_sep: assumes "regular x" "y⇩1 ε x" "y⇩2 ε x" "y⇩3 ε x" shows "¬ (y⇩1 ε y⇩2 ∧ y⇩2 ε y⇩3 ∧ y⇩3 ε y⇩1)"
proof
  obtain t where t: "∀ u. u ε t ⟷ u = y⇩1 ∨ u = y⇩2 ∨ u = y⇩3"
    using triple_sep[OF assms(2-)] by blast
  assume "y⇩1 ε y⇩2 ∧ y⇩2 ε y⇩3 ∧ y⇩3 ε y⇩1"
  with ‹regular x›[unfolded regular_def, rule_format, of t]
  show False
    unfolding set_defs t[rule_format] using assms regular_def by blast
qed

lemma ord_mem_ord_sep: assumes  "ordM v" "u ε v" shows "ordM u"
  unfolding ordM_def epschain_def conj_assoc[symmetric]
proof (rule conjI)+
  have "regular v" "u ⊆⇩M v"
    using ‹ordM v› ordM_D1 ‹u ε v› ordM_def by blast+
  then show "regular u"
    unfolding regular_def using subsetM_trans[OF _ ‹u ⊆⇩M v›] by blast
  have "u ⊆⇩M v" "epschain v" "regular v" "transM v"
    using assms unfolding natM_def ordM_def transM_def epschain_def by blast+
  thus "∀y z. y ε u ∧ z ε u ⟶ y ε z ∨ y = z ∨ z ε y"
    using ‹ordM v› unfolding ordM_def subsetM_def epschain_def by blast
  show "transM u"
    unfolding transM_def set_defs
  proof (rule allI, rule impI)+
    fix z y
    assume "y ε u" "z ε y"
    hence "z ε v" "y ε v" 
      using ‹u ε v› ‹transM v› unfolding transM_def set_defs by blast+
    have "u ≠ z"
      using regular_antisym_mem_sep[OF ‹regular v› ‹y ε v› ‹z ε v›] ‹y ε u› ‹z ε y› by blast
    have "¬ u ε z"
      using regular_antisym2_mem_sep[OF ‹regular v› ‹u ε v› ‹z ε v› ‹y ε v›] ‹y ε u› ‹z ε y› by blast
    show "z ε u"
      using ordM_D2[OF ‹ordM v› ‹u ε v› ‹z ε v›] ‹u ≠ z› ‹¬ u ε z› by blast
  qed
qed   

end

text ‹The interest of this locale is to investigate intersections of various kinds.›

locale L_setext_sep = L_setext + L_sep

begin

sublocale L_setext_empty
  by unfold_locales

lemma separ_def_SFP: assumes "SetFormulaPredicate P"
  shows "u ε separationM y (λ x. P(Ξ(n:=x))) ⟷ (u ε y ∧ (P (Ξ(n:= u))))"
  using  collect_def_ex[OF sep_var[rule_format], OF assms] separationM_def by simp

lemma separ_def_SP: assumes "SetProperty P"
  shows "u ε separationM y (λ x. P x) ⟷ (u ε y ∧ P u)"
  using separ_def_SFP[OF assms[unfolded SetProperty_def], of _ _ _ 0] by simp

lemma separ_def_SR: assumes "SetRelation P"
  shows "u ε separationM y (λ x. P x r) ⟷ (u ε y ∧ P u r)"
  using separ_def_SFP[OF assms[unfolded SetRelation_def], of _ _ _ 0] by simp

lemma least_def':
  assumes "Q (Ξ(n:=w))" and "SetFormulaPredicate Q"
  shows "u ε ⋂⇩M (λ x. Q (Ξ(n:=x))) ⟷ (∀ y. Q (Ξ(n:=y)) ⟶ u ε y)"
proof-
  from bounded_free[OF assms(2)]
  obtain m where m: "Q Ξ = Q Ξ'" if "∀i. i < m ⟶ Ξ i = Ξ' i" for Ξ Ξ'
    by blast
  have k: "Q (Ξ(m+n+1 := x, n := y)) ⟷ Q (Ξ(n := y))" for x y
    by (rule m) force+
  have aux: "(Ξ(n := a)) n = a" for Ξ and a::'a
    by simp
  have sfp: "SetFormulaPredicate (λ Ξ. (∀ y. Q (Ξ(n:=y)) ⟶ ((Ξ(n:=y)) (m+n+1)) ε y))"
    by (rule SFP_all[of "λ Ξ.  Q (Ξ) ⟶ (Ξ) (m+n+1) ε (Ξ n)", of n, unfolded aux], unfold logsimps) (rule | fact)+
  have iff: "(v ε w ∧ (∀y. Q (Ξ(n := y)) ⟶ v ε y)) ⟷ (∀y. Q (Ξ(n := y)) ⟶ v ε y)" for v
    using assms(1) by blast
  have sep: "(v ε separationM w (λx. ∀y. Q (Ξ(n := y)) ⟶ x ε y)) = (∀y. Q (Ξ(n := y)) ⟶ v ε y)" for v
    using separ_def_SFP[of _  v, OF sfp, of w Ξ "m+n+1"] iff[of v] 
     unfolding k by force 
  show ?thesis
    unfolding leastM_def using collect_def'
    using collect_def'[of "separationM w (λx. ∀y. Q (Ξ(0 := y)) ⟶ u ε y)"] sep by force
qed

lemma least_def_ex:
   "∃ w. Q (Ξ(n := w)) ⟹ SetFormulaPredicate Q ⟹ 
   u ε ⋂⇩M (λ x. Q (Ξ(n:=x))) ⟷ (∀ y. Q (Ξ(n:=y)) ⟶ u ε y)"
  using least_def' by force

lemma intersection_def'[set_defs]: "z ε x ∩⇩M y ⟷ z ε x ∧ z ε y"
proof-
  have "SetFormulaPredicate (λΞ. Ξ 0 ε Ξ (Suc 0))"
    by (rule SFP_rules)
  from separ_def_SFP[OF this, of z x, rule_format, of "undefined(1:=y)" 0, simplified] 
  show "(z ε x ∩⇩M y) = (z ε x ∧ z ε y)"
    unfolding intersectionM_def separationM_def.
qed

lemma intersect_subset: "x ∩⇩M y ⊆⇩M x" "x ∩⇩M y ⊆⇩M y"
  unfolding set_defs by simp_all 

lemma intersect_regular: assumes "regular x" "regular y"
  shows "regular (x ∩⇩M y)"
  using assms unfolding regular_def intersection_def' subsetM_def by blast

lemma intersect_transM: assumes "transM x" "transM y"
  shows "transM (x ∩⇩M y)"
  using assms unfolding intersection_def' transM_def subsetM_def by blast

lemma intersect_epschain: assumes "epschain x" "epschain y"
  shows "epschain (x ∩⇩M y)"
  using assms intersect_transM unfolding intersection_def' epschain_def subsetM_def by blast

lemma intersect_ordM: assumes "ordM x" "ordM y"
  shows "ordM (x ∩⇩M y)"
  using assms intersect_transM intersect_regular  unfolding ordM_def
  unfolding  intersection_def' epschain_def by simp

lemma ordM_subset_mem: assumes "ordM x" "ordM y" "y ⊂⇩M x"
  shows "y ε x"
proof-
  have SR: "SetRelation (λ v y. ¬ v ε y)" 
    unfolding SetRelation_def by (rule SFP_rules)+
  have "regular x"
    using ‹ordM x› by simp 
  have dif: "u ε separationM x (λ v. ¬ v ε y) ⟷ u ε x ∧ ¬ u ε y" for u
    using separ_def_SR[OF SR].
  hence "separationM  x (λ v. ¬ v ε y) ⊆⇩M x"
    unfolding subsetM_def by blast
  from ‹regular x›[unfolded regular_def, rule_format, OF this, unfolded dif]
  obtain c where "c ε x" "¬ c ε y" and c: "∀v. v ε c ⟶ (v ε y ∨ ¬ v ε x)"
    using  proper_subset_diff[OF ‹y ⊂⇩M x›] by blast 
  have "c ⊆⇩M x"
    using ‹c ε x› assms(1) natM_def ordM_D1 by blast
  hence "c ⊆⇩M y"
    using ‹y ⊂⇩M x› c unfolding subsetM_def proper_subsetM_def by blast 
  have "y = c"
  proof (rule subsetM_antisym[OF ‹c ⊆⇩M y›], unfold subsetM_def, rule allI, rule impI)
    fix z assume "z ε y"   
    hence "z ε x" 
      using ‹y ⊂⇩M x› unfolding proper_subsetM_def by blast
    from ordM_D2[OF ‹ordM x› this ‹c ε x›]
    show "z ε c"
      using ‹¬ c ε y› ‹z ε y› ordM_D1[OF ‹ordM y› ‹z ε y›, unfolded subsetM_def] by blast
  qed
  thus ?thesis  
    using ‹c ε x› by blast
qed

lemma ordM_total: assumes "ordM x" "ordM y"
  shows "x ε y ∨ y ε x ∨ x = y"
  using ordM_def[unfolded epschain_def]
proof-
  have "regular (x ∩⇩M y)"
    using intersect_ordM[OF ‹ordM x› ‹ordM y›] by simp
  from regular_not_self_mem_sep[OF this]
  have "¬ (x ∩⇩M y ⊂⇩M x ∧ x ∩⇩M y ⊂⇩M y)"
    using ordM_subset_mem[OF assms(1) intersect_ordM, OF assms]  
      intersection_def' assms(1,2) ord_mem_ord_sep ordM_subset_mem by blast  
  with sep_SR[rule_format, of "λ v y. v ε y"]
  consider "x ∩⇩M y = x" | "x ∩⇩M y = y" 
    unfolding proper_subsetM_def using intersection_def' by blast  
  then show ?thesis
  proof (cases)
    assume "x ∩⇩M y = x"
    hence "x = y ∨ x ⊂⇩M y"
      unfolding proper_subsetM_def setext using intersection_def' by blast
    with ordM_subset_mem[OF assms(2,1)] 
    show ?thesis
      by blast
  next
    assume "x ∩⇩M y = y"
    hence "x = y ∨ y ⊂⇩M x"
      unfolding proper_subsetM_def setext using intersection_def' by blast
    with ordM_subset_mem[OF assms] 
    show ?thesis
      by blast
  qed
qed

lemma nat_mem_nat: assumes  "natM v" "u ε v" shows "natM u"
  unfolding natM_def 
proof
  show "ordM u"
    using assms ord_mem_ord_sep unfolding natM_def by blast
  show "∀v. v ε u ∨ v = u ⟶ (∃u. u ε v) ⟶ is_sucM v"
    using assms natM_D nat_mem_is_suc  ordM_D1 subsetM_def  by blast  
qed    
      
lemma set_of_ords_regular: assumes "∀ y. y ε s ⟶ ordM y"
  shows "regular s"   
  unfolding regular_def
proof (rule allI, rule impI, rule impI)
  fix y assume "y ⊆⇩M s" "∃z. z ε y"
  then obtain z where "z ε y"
    by blast
  have "ordM z"
    using ‹y ⊆⇩M s› ‹z ε y› assms subsetM_def by blast
  hence "regular z"
    by simp
  show "∃u. u ε y ∧ (∀v. ¬ (v ε u ∧ v ε y))"
  proof (cases "∀v. ¬ (v ε z ∧ v ε y)", use ‹z ε y› in blast)   
    assume a: "¬ (∀v. ¬ (v ε z ∧ v ε y))"
    from sep_SR[of "λ x y. x ε y", rule_format, of z, unfolded SetRelation_def, OF SFP_mem]
    obtain u where u: "∀ v. v ε u ⟷ v ε z ∧ v ε y"
      by auto
    hence "u ⊆⇩M z" "∃ v. v ε u"
      using a unfolding u[rule_format] set_defs by blast+
    from ‹regular z›[unfolded regular_def, rule_format, OF this]
    obtain m where "m ε u" "∀v. ¬ (v ε m ∧ v ε u)" 
      by blast
    hence "m ε y ∧ (∀v. ¬ (v ε m ∧ v ε y))"
      unfolding u[rule_format] using ‹ordM z› ordM_trans by presburger
    thus ?thesis
      by blast
  qed
qed
   
lemma intersect_natM: assumes "natM x" "natM y"
  shows "natM (x ∩⇩M y)"
proof (cases "x = x ∩⇩M y", use assms in argo)
  assume "x ≠ x ∩⇩M y"
  show "natM (x ∩⇩M y)"
  proof (cases "x ∩⇩M y = ∅") 
    assume "x ∩⇩M y ≠ ∅" 
    show "natM (x ∩⇩M y)"
    proof (rule natM_I) 
      show "⋀v. ∃u. u ε v ⟹ v ε x ∩⇩M y ⟹ is_sucM v"
        using ‹natM x›[unfolded natM_def] unfolding intersection_def' by blast
      show "is_sucM (x ∩⇩M y)"
      proof (rule nat_mem_is_suc)
        have "¬ x ε x ∩⇩M y"
          using assms(1) natM_def ordM_def regular_not_self_mem_sep unfolding intersection_def' by fast
        thus "(x ∩⇩M y) ε x"
          using ordM_total[OF _ intersect_ordM, of x x y] ‹¬ x = x ∩⇩M y› natM_D assms by blast
        show "∃u. u ε x ∩⇩M y"
          using ‹x ∩⇩M y ≠ ∅› emptyset_def' by auto 
      qed fact
    qed (simp add: assms  intersect_ordM natM_D)
  qed simp
qed

end

locale L_setext_setsuc_sep = L_setext + L_setsuc + L_sep

begin

text ‹
We want to prove that ordinals are closed under the successor operation. However, regularity is a problem. It is not necessarily preserved by taking successors.

Separation is needed to avoid the following pathological situation:
consider an epschain ‹C = {c⇩z | z ∈ ℤ}› of type ‹ℤ› where moreover ‹∅ ∈ c⇩z› for each ‹z›. That is, ‹u ε c⇩m› iff ‹u = c⇩k› with ‹k < m›, or ‹u = ∅›.  
We postulate that an infinite subclass of ‹C› is a set iff it contains ‹c⇩0›.
Now, ‹c⇩z› are ordinals for all  ‹z ≤ 0›. But ‹c⇩1› is not regular, since it contains an infinite descending chain ‹{c⇩k | k ≤ 0}› as a subset.
›

sublocale L_setext_empty_setsuc
  by unfold_locales

sublocale L_setext_sep
  by unfold_locales

lemma regular_setsuc: assumes "transM x" "regular x" "regular y"
  shows "regular (setsucM x y)"
proof (cases "y ε x")
  assume "y ε x"
  hence "setsucM x y = x"
    unfolding setext[of _ x] set_defs by blast
  thus "regular (setsucM x y)"
    using ‹regular x› by simp
next
  assume "¬ y ε x" 
  show "regular (setsucM x y)"
    unfolding regular_def 
  proof (rule allI, rule impI, rule impI)
    fix w 
    assume "w ⊆⇩M setsucM x y" "∃ z. z ε w"
    have "SetFormulaPredicate (λΞ. Ξ 0 ≠ Ξ 1)"
      by (rule SFP_rules)+
    from sep_SR[of "λ x y. x ≠ y", unfolded SetRelation_def, OF this]
    obtain w' where w': "⋀ z. z ε w' ⟷ z ε w ∧ z ≠ y"
      by presburger
    have  "w' ⊆⇩M x"
      using ‹w ⊆⇩M setsucM x y› w' subsetM_def setsuc_def' by auto 
    show "∃z. z ε w ∧ (∀v. ¬ (v ε z ∧ v ε w))"
    proof (cases "y ε w")
      assume "y ε w"
      show ?thesis
      proof (cases "w' = ∅")
        assume "w' = ∅"
        have "w = {y}⇩M"
          using w' empty_is_empty ‹y ε w› unfolding setext[of w] set_defs ‹w' = ∅› singleton_def' by metis 
        hence "y ε w ∧ (∀v. ¬ (v ε y ∧ v ε w))"
          unfolding ‹w = {y}⇩M› set_defs  using regular_not_self_mem[OF ‹regular y›] singleton_def'
          by auto
        then show ?thesis
          by blast
      next
        assume "¬ w' = ∅"
        hence "∃ z. z ε w'"
          by (simp add: emptyset_def')
        from ‹regular x›[unfolded regular_def, rule_format, OF ‹w' ⊆⇩M x› this]
        obtain m where "m ε w'" and m: "∀v. ¬ (v ε m ∧ v ε w')"
          by blast
        hence "m ε w"
          using w' by blast
        have "¬ y ε m"
          using ‹transM x›[unfolded transM_def] ‹m ε w'› ‹w' ⊆⇩M x› ‹¬ y ε x› subsetM_def by blast
        have "∀v. ¬ (v ε m ∧ v ε w)"
          using m unfolding w' using ‹¬ y ε m› by blast 
        then show ?thesis
          using ‹m ε w› by blast
      qed
    next
      assume "¬ y ε w"
      hence "w ⊆⇩M x"
        using ‹w ⊆⇩M setsucM x y› w' subsetM_def
        by (metis ‹w' ⊆⇩M x›)
      from ‹regular x›[unfolded regular_def, rule_format, OF this ‹∃ z. z ε w›]
      show ?thesis.
    qed
  qed
qed

lemma ord_suc_ord: assumes "ordM x" shows "ordM (setsucM x x)"
proof(rule ordM_I)
  show epschain: "epschain (setsucM x x) "
    using assms
    using ordM_def epschain_suc_epschain by blast 
  show "regular (setsucM x x)"
    unfolding regular_def  using assms epschain_def ordM_def regular_def regular_setsuc by blast 
qed  

lemma nat_suc_nat: assumes "natM x" shows "natM (setsucM x x)"
proof-
  have "(∀v. v ε x ∨ v = x ⟶ (∃u. u ε v) ⟶ (∃y. ∀z. (z ε v) = (z ε y ∨ z = y))) ⟹
    (∀v. v ε setsucM x x ∨ v = setsucM x x ⟶ (∃u. u ε v) ⟶ (∃y. ∀z. (z ε v) = (z ε y ∨ z = y)))"
    using setsuc_def' by auto
  thus  "natM (setsucM x x)"
    using assms ord_suc_ord unfolding natM_def is_sucM_def by fast
qed

lemma one_natM[simp]: "natM ({∅}⇩M)"
  using nat_suc_nat[OF emp_natM] unfolding setsuc_empty_sing.

lemma ord_mem_suc: assumes "ordM x" and "y ε x" 
  shows  "setsucM y y ε x ∨ setsucM y y = x"
proof-
  have "ordM y"
    using ord_mem_ord[OF ‹ordM x› ‹y ε x›].
  have "ordM(setsucM y y)"
    by (simp add: ‹ordM y› ord_suc_ord)
  have "¬ x ε setsucM y y"
  proof
    assume "x ε setsucM y y"
    then consider "x ε y" | "x = y"
      unfolding setsuc_def' by blast
    then show False
      by (cases) (use  ‹y ε x› ‹ordM x› ordM_def ordM_trans regular_not_self_mem in blast)+
  qed
  with ordM_total[OF  ‹ordM x› ‹ordM(setsucM y y)›]    
  show ?thesis
    by blast
qed

lemma ord_limit_or_suc: assumes "ordM x" 
  shows "is_sucM x ∨ (∀ u. u ε x ⟶ setsucM u u ε x)"
  using assms is_suc_def' ord_mem_suc by auto

lemma assumes "regular x" "regular y" 
  shows "regular (setsucM x y)"
  unfolding regular_def setsuc_def' 
  oops
― ‹not true, consider ‹{x} ε x›. Then ‹x ∪ {x}› contains a subset ‹{x,{x}}› which is a cycle›

end 


subsection ‹Transitive superset›

text ‹The existence of transitive supersets needs to be assumed explicitly if the axiom of infinity is absent (or negated). It is related to regularity, since it enables obtaining an infinite set from infinite descending epsilon chains.›

locale L_ts = set_signature +
  assumes ts: "∀ x. ∃ z. (transM z ∧ (x ⊆⇩M z))" 

locale L_setext_sep_ts = L_setext + L_sep + L_ts

begin

sublocale L_setext_sep
  by unfold_locales

lemma least_ts_def' : "u ε least_tsM x ⟷ (∀ v. transM v ∧ x ⊆⇩M v ⟶ u ε v)" 
   (is "u ε least_tsM x ⟷ (∀ v. ?Q v ⟶ u ε v)")
  by (rule least_def_ex[of "λ Ξ. transM (Ξ 0) ∧ Ξ 1 ⊆⇩M Ξ 0" "undefined(1:=x)" 0, 
  simplified, OF ts[rule_format], folded least_tsM_def], unfold logsimps set_defs)
  (rule SFP_rules)+

lemma least_ts_is_transitive: "transM (least_tsM x)"
  using least_ts_def' unfolding transM_def subsetM_def by blast

end

locale L_setext_sep_reg = L_setext + L_sep + L_reg

locale L_setext_sep_reg_ts = L_setext + L_sep + L_reg + L_ts

begin

sublocale L_setext_sep_ts
  by unfold_locales

text ‹The schema of regularity follows from regularity and transitive superset.›

sublocale L_regsch
proof (unfold_locales, rule impI)
  fix P Ξ
  assume "SetFormulaPredicate P"
  assume "∃ x. P (Ξ(0:=x))"
  then obtain x where "P (Ξ(0:=x))" 
    by blast
  have "x ⊆⇩M (least_tsM x)"  
    using least_ts_def' subsetM_def by blast
  define w where "w = separationM (least_tsM x) (λ x. P (Ξ(0:=x)))"
  then have w: "u ε w ⟷ u ε least_tsM x ∧ P (Ξ(0:=u))" for u 
    using separ_def_SFP[OF ‹SetFormulaPredicate P›] by blast
  show "∃x. P (Ξ(0 := x)) ∧ (∀y. y ε x ⟶ ¬ P (Ξ(0 := y)))"
  proof(cases)
    assume "∃ v. v ε w"
    have "(∃ v. v ε w)⟶(∃ v. (v ε w ∧ ( ∀ t. (t ε v  ⟶ ¬ t ε w ) ) ) )" 
      using reg by blast    
    then have "(∃ v. (v ε w ∧ ( ∀ t. (t ε v  ⟶ ¬ t ε w ) ) ) )" using ‹∃ v. v ε w› by blast
    then obtain v where "v ε w" and v: "t ε v  ⟶ ¬ t ε w" for t by blast  
    have "P (Ξ(0 := v))" 
      using w ‹v ε w› by blast
    have "v ε least_tsM x" 
      using w ‹v ε w› by blast
    have "v ⊆⇩M least_tsM x"
      using least_ts_is_transitive ‹v ε least_tsM x› transM_def by blast
    have "t ε v ⟶ ¬ P (Ξ(0 := t))" for t 
      using ‹v ⊆⇩M least_tsM x› w v unfolding subsetM_def by blast 
    then have "∀ t. (t ε v ⟶ ¬ P (Ξ(0 := t)))" by blast
    then have "∃x. P (Ξ(0 := x))∧ (∀y. y ε x ⟶ ¬ P (Ξ(0 := y)))"
      using ‹P (Ξ(0 := v))› by blast
    then show ?thesis by blast
  next
    assume  "¬ (∃ v. v ε w)"
    then have "∀ v. (v ε least_tsM x ⟶ ¬ P (Ξ(0 := v)) )" 
      using w  by blast
    then have  "∀ v. (v ε x ⟶ ¬ P (Ξ(0 := v)) )" 
       using subsetM_def ‹x ⊆⇩M least_tsM x› by blast
     then show ?thesis 
       using ‹P (Ξ(0 := x))› by blast 
  qed
qed

end

subsection Replacement

locale L_repl = set_signature + 
  assumes replf:  "SetFormulaPredicate P ⟹ (∀ u. ∃! v. P (Ξ(0:=u, 1:= v))) ⟶ (∀ x. ∃ z. ∀ v. v ε z ⟷ (∃ u. u ε x ∧ P (Ξ(0:=u, 1:= v))))"
― ‹We can replace ‹x⇩0› by the unique ‹x⇩1› satisfying ‹P(x⇩0,x⇩1)›. Note the presence of parameters ‹x⇩i, i ≥ 2››

locale L_setext_empty_repl = L_setext + L_empty + L_repl

begin

text ‹Replacing using total functions is equivalent to replacing using partial functions.›

lemma replp: assumes "SetFormulaPredicate P" and func: "∀ u v w. P (Ξ(0:=u, 1:= v)) ∧ P (Ξ(0:=u, 1:= w)) ⟶ v = w"
  shows "∀ x. ∃ z. (∀ v. v ε z ⟷ (∃ u. u ε x ∧ P (Ξ(0:=u, 1:= v))))"
proof
  fix x
  show "∃z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0:=u, 1:= v)))"
  proof (cases "∃ u v. u ε x ∧ P (Ξ(0:=u, 1:= v))")
    assume "∄u v. u ε x ∧ P (Ξ(0:=u, 1:= v))"
    then show "∃z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0:=u, 1:= v)))"
      using exI[of "λ z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0:=u, 1:= v)))" ∅] empty by blast 
  next    
    assume ex: "∃ u v. u ε x ∧ P (Ξ(0:=u, 1:= v))"
    then obtain v where ex: "∃u. u ε x ∧ P (Ξ(0:=u, 1:= v))"  
      by blast
    from bounded_free[OF assms(1)]
    obtain k where k0: "∀Ξ Ξ'. (∀i<k. Ξ i = Ξ' i) ⟶ P Ξ = P Ξ'"
      by blast
    let ?k = "Suc (max k 1)"
    have k: "P(Ξ) ⟷ P(Ξ(?k:= a))" "1 < ?k" for Ξ a
      by (rule k0[rule_format, of Ξ "Ξ(?k:= a)"], force) simp   
    have twist: "Ξ(Suc (max k 1) := a, 0 := b, 1 := c) = Ξ(0 := b, 1 := c, Suc (max k 1) := a)" for a b c
      by auto
    have canc: "P(Ξ(?k:=a,0:=b,1:=c)) = P(Ξ(0:=b,1:=c))" "Ξ(?k:=a,0:=b,1:=c,1:=d) = Ξ(?k:=a,0:=b,1:=d)"
     "(Ξ(?k := a, 0 := b, 1 := c)) 1 = c" "(Ξ(?k := a, 0 := b, 1 := c)) ?k = a" for a b c d
      unfolding twist using k(1) by auto
    define Q :: "(nat ⇒ 'a) ⇒ bool" where 
    "Q = (λ Ξ. (if ∃ c. P (Ξ(1:= c)) then P Ξ  else Ξ 1 = Ξ ?k))"
    have "∃! v'. Q (Ξ(?k:=v,0:=u,1:=v'))" for u
      unfolding Q_def canc using ex func by metis
    hence ex1: "∀ u. ∃! w. Q (Ξ(?k:=v,0:=u,1:=w))"
      by simp 
    have "SetFormulaPredicate Q"
      unfolding Q_def by (simp, unfold logsimps) (rule SFP_rules | fact)+
    from replf[rule_format, OF this ex1[rule_format], of x] 
    have  Qset: "∃z. ∀w. (w ε z) = (∃u. u ε x ∧ Q(Ξ(?k:=v,0:=u,1:=w)))".
    have P_iff_Q: "(∃u. u ε x ∧ P (Ξ(0 := u, 1 := w))) ⟷ (∃u. u ε x ∧ Q (Ξ(?k:=v, 0 := u, 1 := w)))" for w
      unfolding Q_def canc  using ex by auto 
    show ?thesis
      using Qset unfolding P_iff_Q.
  qed
qed

lemma replp_vars: assumes "SetFormulaPredicate P" and func: "∀ u v w. P (Ξ(k:=u, l:= v)) ∧ P (Ξ(k:=u, l:= w)) ⟶ v = w"
  shows "∀ x. ∃ z. (∀ v. v ε z ⟷ (∃ u. u ε x ∧ P (Ξ(k:=u, l:= v))))"
proof-
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where m: "P Ξ = P Ξ'" if "∀i<m. Ξ i = Ξ' i" for Ξ Ξ'
    by blast
  let ?m = "Suc (k + l + m)"  
  let ?f = "id(0 := ?m, 1 := Suc ?m, k:= 0,l := 1)"
  let ?Q = "λ X. (P (λ b. X (?f  b)))"
  let ?X = "Ξ(?m:= Ξ 0,(Suc ?m):= Ξ 1)" 
  have sfpq:  "SetFormulaPredicate ?Q"
    using transform_variables[OF ‹SetFormulaPredicate P›] by simp
  have small: "∀ i < m. (Ξ(k := u, l := v)) i = (?X (0 := u, 1 := v)) (?f i)" for u v
    by auto
  have equiv: "(P (Ξ(k := u, l := v))) ⟷ (?Q (?X (0 := u, 1 := v)))" for u v
    by (rule m[of "Ξ(k := u, l := v)" "λ b. (?X (0 := u, 1 := v))(?f b)"]) fact
  then have funcq: "(∀u v w. ?Q (?X(0 := u, 1 := v)) ∧ ?Q (?X(0 := u, 1 := w)) ⟶ v = w)"
    using func by blast 
  show ?thesis
    using replp[OF sfpq funcq] unfolding equiv.    
qed

lemma repl_SR: assumes "SetRelation P" "∀ u v w. P u v ∧ P u w ⟶ v = w"
  shows "∀ x. ∃ z. (∀ v. v ε z ⟷ (∃ u. u ε x ∧ P u v))"
  using assms unfolding SetRelation_def using replp[of "λΞ. P (Ξ 0) (Ξ 1)"] by fastforce    

lemma replace_def':  
  assumes "SetFormulaPredicate P" "∀ u v w. P(Ξ(k:=u, l:= v)) ∧ P(Ξ(k:=u, l:= w)) ⟶ v = w"
  shows "∀ v. v ε replaceM (λ u v. P(Ξ(k:=u, l:= v))) x ⟷ (∃ u. u ε x ∧ (P(Ξ(k:=u, l:= v))))"
  using collect_def_ex[of  "λ v. (∃u. u ε x ∧ P(Ξ(k:=u, l:= v)))", OF replp_vars[OF assms, rule_format], folded replaceM_def] by blast

text ‹Separation can be obtained from replacement.›

sublocale L_setext_sep
proof (unfold_locales, rule allI)
  fix P Ξ x
  assume sfp: "SetFormulaPredicate P"
  ― ‹The idea is clear: we replace ‹x⇩0› with itself, that is, with ‹x⇩1 = x⇩0›. A technical complication is that we have to rename parameters ‹x⇩i› which for separation include ‹x⇩1› while for replacement they have to start with ‹x⇩2››
  have t: "(λn. if n = 0 then v else ((λi. Ξ (i - 1))(0 := v)) (n+1)) = Ξ(0 := v)" for v and Ξ :: "nat ⇒ 'a"
    by auto
  have "SetFormulaPredicate (λ Ξ. (Ξ 0) = (Ξ 1) ∧ P (λ n. Ξ (n+1)))"
    unfolding logsimps by (rule SFP_rules)+ (rule transform_variables[OF sfp])
  from replp[rule_format, OF this, of "λ i. Ξ (i - 1)" x]
  show "∃z. ∀u. (u ε z) = (u ε x ∧ P (Ξ(0 := u)))"
    by (simp del: One_nat_def add: t)  
qed

end

text ‹Separation does not follow from replacement without the empty set axiom. We show it by constructing a counter-model.›

theorem not_repl_ext_implies_separ: "¬ (∀ mem. L_repl mem ∧ L_setext mem ⟶ L_sep mem)"
proof-
  define loop :: "'a ⇒ 'a ⇒ bool" where  "loop ≡ λ x y. x = y"
  interpret eq_mem : set_signature loop.
  have loop_ext: "L_setext loop"
    by (unfold_locales, unfold loop_def) force
  have loop_repl: "L_repl loop"
  proof (unfold_locales, rule impI)
    fix P :: "(nat ⇒ 'a) ⇒ bool" and Ξ
    assume "∀u. ∃!v. P (Ξ(0 := u, 1 := v))"
    then show "∀x. ∃z. ∀v. loop v z = (∃u. loop u x ∧ P (Ξ(0 := u, 1 := v)))"
      unfolding loop_def by metis 
  qed
  have SP: "eq_mem.SetFormulaPredicate (λ Ξ. False)"
    by simp
  have "¬ L_sep loop"
    unfolding L_sep_def using loop_def  SP by blast 
  show ?thesis
    using ‹¬ L_sep loop› loop_ext loop_repl by auto
qed
 

locale L_setext_empty_setsuc_repl = L_setext + L_empty + L_setsuc + L_repl

begin

sublocale L_setext_empty_setsuc
  by unfold_locales

sublocale L_setext_empty_repl
  by unfold_locales

lemma tarski_setsuc_tarski: assumes "tarski_fin x" shows "tarski_fin (setsucM x y)"
  unfolding tarski_fin_def
proof (rule, rule, rule)
  ― ‹fix a system ‹w› for which we want to find the maximum›
  fix w assume w: "∀z. z ε w ⟶ z ⊆⇩M setsucM x y" and "∃ z. z ε w"
    ― ‹remove ‹y› from each element of ‹w›, call the result ‹w'››  
  let ?P = "λ Ξ. ∀ a. a ε Ξ 1 ⟷ a ε Ξ 0 ∧ a ≠ Ξ 2"
  have sfp: "SetFormulaPredicate (λΞ. ∀v. (v ε Ξ 1) = (v ε Ξ 0 ∧ v ≠ Ξ 2))"
    unfolding logsimps by (rule SFP_rules)+
  have sfp': "SetFormulaPredicate (λΞ. Ξ 0 ≠ Ξ 1)"
        by (rule SFP_rules)+
  have aux:  "(Ξ(2::nat := y, 0 := u, 1 := v)) 0 = u"
             "(Ξ(2 := y, 0 := u, 1 := v)) 1 = v"
             "(Ξ(2 := y, 0 := u, 1 := v)) 2 = y" for u v Ξ
    by simp_all
  have "∃ w'. ∀ z. z ε w' ⟷ (∃ u. u ε w ∧ (∀ v. v ε z ⟷ v ε u ∧ v ≠ y))"
       
   by (rule replp[rule_format, of ?P "undefined(2:= y)" w, unfolded aux], fact)
    (unfold setext, simp)
  then obtain w' where w': "∀ z. z ε w' ⟷ (∃ u. u ε w ∧ (∀ v. v ε z ⟷ v ε u ∧ v ≠ y))"  
    by blast
   ― ‹get the maximum of ‹w'››
  obtain wmax' where wmax': "wmax' ε w' ∧ (∄w. w ε w' ∧ wmax' ⊂⇩M w)"
  proof (rule exE[OF assms[unfolded tarski_fin_def, rule_format, of w'], of thesis])   
    show "z ⊆⇩M x" if "z ε w'" for z
      using ‹z ε w'›[unfolded w'[rule_format, of z]] w unfolding subsetM_def setsuc_def' by auto
    show "∃x. x ε w'"
    proof-
      obtain u where "u ε w"
        using ‹∃ z. z ε w› by blast 
      from sep[rule_format, OF sfp', of u "undefined(1:=y)"]
      obtain u' where u': "∀ v. v ε u' ⟷ v ε u ∧ v ≠ y"
         by auto 
      show "∃x. x ε w'"
        unfolding w'[rule_format] using ‹u ε w› u' by blast
    qed
  qed
  have "¬ y ε wmax'" "wmax' ε w'" "∄w. w ε w' ∧ wmax' ⊂⇩M w"
    using w' wmax' by blast+
  ― ‹Either ‹wmax'› or ‹setsucM wmax' y› is the desired maximum of ‹w››
  show "∃z. z ε w ∧ (∄v. v ε w ∧ z ⊂⇩M v)"
  proof(cases) 
    assume "setsucM wmax' y ε w"
    have "(∄v. v ε w ∧ setsucM wmax' y ⊂⇩M v)"
    proof
      assume "∃v. v ε w ∧ setsucM wmax' y ⊂⇩M v"
      then obtain v where "v ε w" and "setsucM wmax' y ⊂⇩M v"
        by blast
      from sep[rule_format, OF sfp', of v "undefined(1:=y)"]  
      obtain v' where v': "⋀ t. t ε v' ⟷ t ε v ∧ t ≠ y"
        by auto
      have "v' ε w'"
        using ‹v ε w› v' w' by auto
      have "wmax' ⊂⇩M v'"
        using ‹setsucM wmax' y ⊂⇩M v› ‹¬ y ε wmax'› unfolding set_defs setext[of wmax'] setext[of _ v] v' by blast 
      show False
        using wmax' ‹v' ε w'› ‹wmax' ⊂⇩M v'› by blast
    qed 
    thus ?thesis
      using ‹setsucM wmax' y ε w› by blast
  next
    assume "¬ setsucM wmax' y ε w" 
    hence "wmax' ε w" 
    proof-
      obtain wmax where "wmax ε w" and wmax: "∀ v. (v ε wmax') = (v ε wmax ∧ v ≠ y)"
        using ‹wmax' ε w'›[unfolded w'[rule_format, of wmax']] ‹¬ y ε wmax'› by blast
      have "¬ y ε wmax"
      proof
        assume "y ε wmax"
        hence "wmax = setsucM wmax' y"
          unfolding setext[of wmax] set_defs wmax[rule_format] by blast
        then show False
          using ‹¬ setsucM wmax' y ε w› ‹wmax ε w› by blast 
      qed
      hence "wmax = wmax'"
        using setext wmax by blast
      then show "wmax' ε w"
        using ‹wmax ε w› by blast
    qed
    have "(∄v. v ε w ∧ wmax' ⊂⇩M v)"
    proof
      assume "∃v. v ε w ∧ wmax' ⊂⇩M v"
      then obtain v where "v ε w" and "wmax' ⊆⇩M v" and "wmax' ≠ v"
        unfolding proper_subset_def' by blast
      obtain v' where v': "⋀ t. t ε v' ⟷ t ε v ∧ t ≠ y"
      using sep[rule_format, OF sfp', of  v "undefined(1:=y)"] by auto 
      have "v' ε w'"
        using ‹v ε w› v' w' by auto
      have "wmax' ⊆⇩M v'"
        using ‹wmax' ⊆⇩M v› ‹¬ y ε wmax'› unfolding setext[of _ v] v' set_defs by blast
      hence "wmax' = v'"
        using wmax' ‹v' ε w'› unfolding  proper_subset_def' by blast
      have "v = setsucM wmax' y"
        using ‹wmax' ≠ v› unfolding ‹wmax' = v'› setext[of v] setext[of _ v] set_defs v' by blast 
      then show False
        using ‹¬ setsucM wmax' y ε w› ‹v ε w› by blast
      qed
    thus ?thesis
      using ‹wmax' ε w› by blast
  qed
qed

end

subsection Powerset

locale L_power = set_signature +
  assumes 
          power: "∀ x. ∃ y. (∀ u. u ε y ⟷ u ⊆⇩M x)"

locale L_setext_empty_power = L_setext + L_empty + L_power

begin

sublocale L_setext_empty
  by unfold_locales

lemma powerset_def'[set_defs]: "u ε (𝔓 x) ⟷ u ⊆⇩M x"
  using collect_def_ex[OF power[rule_format], folded powersetM_def].

lemma "∅ ε 𝔓 ∅"
  using empty_is_subset powerset_def' by blast

lemma set_one_mem [simp]: "u ε 𝔓 ∅ ⟷ u = ∅"
  unfolding powerset_def' subsetM_def emptyset_def' by force 

lemma set_one_def: "𝔓 ∅ = {∅}⇩M"
  unfolding singletonM_def using collect_def'[of "𝔓 ∅"] unfolding set_one_mem by force 

lemma set_two_mem: "u ε 𝔓 (𝔓 ∅) ⟷ u = ∅ ∨ u = {∅}⇩M"
  unfolding powerset_def' set_one_def 
proof
  show "u = ∅ ∨ u = {∅}⇩M" if "u ⊆⇩M {∅}⇩M" 
    using  that[unfolded subsetM_def] emptyset_def'
    unfolding setext[of _ "{∅}⇩M"]  set_one_mem[unfolded set_one_def] by blast 
  show "u = ∅ ∨ u = {∅}⇩M ⟹ u ⊆⇩M {∅}⇩M"
    using empty_is_subset subsetM_refl by blast
qed

end

locale L_setext_empty_power_repl = L_setext + L_empty + L_power + L_repl

― ‹Subsumes many already existing locales. In particular, we obtain set successor from powerset and replacement›

begin

sublocale L_setext_empty_repl
  by unfold_locales

sublocale L_setext_empty_power
  by unfold_locales

sublocale L_setext_empty_setsuc
proof (unfold_locales, rule allI, rule allI)
  fix x y 
  let ?P = "(λ Ξ. ((∃ q. q ε (Ξ (0::nat))) ∧ (∀ q. (q ε (Ξ 0) ⟷ q = (Ξ 1))) ∨ (Ξ 1 = Ξ 2 ∧ ¬(∃ z. ∀ q. (q ε (Ξ 0) ⟷ q = z)))))"
  have sfp: "SetFormulaPredicate ?P"
    unfolding logsimps set_defs by (rule SFP_rules)+
  have func: "∀u v w.
   ((∃q. q ε u) ∧ (∀q. (q ε u) ⟷ (q = v)) ∨ v = y ∧ (∄z. ∀q. (q ε u) ⟷ (q = z))) ∧
   ((∃q. q ε u) ∧ (∀q. (q ε u) ⟷ (q = w)) ∨ w = y ∧ (∄z. ∀q. (q ε u) ⟷ (q = z))) ⟶
   v = w"
    by blast   
  have aux: "(undefined(2 :: nat := y, 0 := u, 1 := v)) 0 = u" "(undefined(2 :: nat := y, 0 := u, 1 := v)) 1 = v" "(undefined(2 :: nat := y, 0 := u, 1 := v)) 2 = y" for u v 
    by simp_all
  have "∃z. ∀v. (v ε z) =
        (∃u. u ε 𝔓 x ∧ ((∃q. q ε u) ∧ (∀q. (q ε u) = (q = v)) ∨ v = y ∧ (∀z. ∃q. (q ε u) = (q ≠ z))))"
    using  replp[OF sfp, simplified, of "undefined(2:=y)", unfolded fun_upd_same, OF func[simplified]]  by simp   
  ― ‹singletons from ‹𝔓 x› are replaced by their elements, other sets by ‹y›› 
  then obtain s where s: "∀v. (v ε s) =
  (∃u. u ε 𝔓 x ∧ ((∃q. q ε u) ∧ (∀q. (q ε u) = (q = v)) ∨ v = y ∧ (∀z. ∃q. (q ε u) = (q ≠ z))))"
    by auto
  have "v ε s ⟷ (v ε x ∨ v = y)" for v
  proof
    show "v ε s ⟹ v ε x ∨ v = y"
      unfolding s[rule_format] powerset_def'[unfolded subsetM_def]  by blast 
    show "v ε x ∨ v = y ⟹ v ε s"
    proof (erule disjE)
      assume "v ε x"
      obtain singv where singv: "singv ε 𝔓 x" "∀a. (a ε singv) ⟷ a = v"
      proof-
        have sfp: "SetFormulaPredicate (λ Ξ. Ξ 0 = ∅ ∧ Ξ 1 = Ξ 2)" 
          unfolding logsimps set_defs by (rule SFP_rules)+
        then obtain singv where "∀a. (a ε singv) ⟷ a = v" 
          using replp[OF sfp, rule_format, of "undefined(2 := v)"  "𝔓 ∅", simplified] by blast
        then have "singv ε 𝔓 x"
          using ‹v ε x› by (simp add: powerset_def' subsetM_def) 
        from that[OF this ‹∀a. (a ε singv) ⟷ a = v›]
        show thesis.
      qed
      then show "v ε s"
           unfolding s[rule_format] by blast
       next
      assume "v = y"
      hence "∅ ε 𝔓 x ∧ ∅ ⊆⇩M x ∧ (v = y ∧ (∄z. ∀q. (q ε ∅) = (q = z)))"  
        unfolding set_defs by force
      then show "v ε s"
        unfolding s[rule_format] by blast
    qed
  qed
  then show "∃z. ∀u. (u ε z) = (u ε x ∨ u = y)"
    by blast
qed

sublocale L_setext_empty_setsuc_repl
  by unfold_locales

end

subsection ‹Union›

locale L_union = set_signature + 
  assumes union: "∀ x. ∃ y.∀ v. v ε y ⟷ (∃ u. u ε x ∧ v ε u)"

locale L_setext_union = L_setext + L_union 

begin

lemma union_def'[set_defs]: "u ε ⋃⇩M x ⟷ (∃ v. v ε x ∧ u ε v)"
  using collect_def_ex[OF union[rule_format, of x], folded unionM_def[of x]].

lemma union_trans_trans: assumes "∀ v. v ε x ⟶ transM v"
  shows "transM (⋃⇩M x)"
  using assms unfolding transM_def union_def' subsetM_def by blast

end

locale L_setext_sep_binunion_ts = L_setext + L_sep +  L_binunion + L_ts

begin

sublocale L_setext_binunion
  by unfold_locales

sublocale L_setext_sep_ts
  by unfold_locales

lemma trans_union: "transM u ⟹ transM v ⟹ transM (u ∪⇩M v)"
  by (simp add: binunion_def' subsetM_def transM_def)

lemma leastTS_union: "least_tsM (u ∪⇩M v) = least_tsM u ∪⇩M least_tsM v"
  unfolding setext least_ts_def' binunion_def'
proof (rule allI, rule iffI)
  fix z
  assume trans: "∀x. transM x ∧ u ∪⇩M v ⊆⇩M x ⟶ z ε x"
  show "(∀x. transM x ∧ u ⊆⇩M x ⟶ z ε x) ∨ (∀x. transM x ∧ v ⊆⇩M x ⟶ z ε x)"
  proof (rule disjCI)
    assume "¬ (∀x. transM x ∧ v ⊆⇩M x ⟶ z ε x)"
    then obtain x where "transM x" "v ⊆⇩M x" "¬ z ε x"
      by blast
    show "∀x. transM x ∧ u ⊆⇩M x ⟶ z ε x"
    proof (rule allI, rule impI)
      fix y
      assume "transM y ∧ u ⊆⇩M y"
      with trans_union[OF ‹transM x›, of y]  
      have "transM (x ∪⇩M y) ∧ u ∪⇩M v ⊆⇩M x ∪⇩M y"
        using ‹v ⊆⇩M x›  binunion_def' subsetM_def by auto
      from trans[rule_format, OF this]
      show "z ε y"
        using ‹¬ z ε x› unfolding binunion_def' by blast
    qed
  qed
next
  fix z
  assume or: "(∀x. transM x ∧ u ⊆⇩M x ⟶ z ε x) ∨ (∀x. transM x ∧ v ⊆⇩M x ⟶ z ε x)"
  show "∀y. transM y ∧ u ∪⇩M v ⊆⇩M y ⟶ z ε y"
  proof (rule allI, rule impI)  
    fix y
    assume "transM y ∧ u ∪⇩M v ⊆⇩M y"
    hence ins: "transM y ∧ u ⊆⇩M y" "transM y ∧ v ⊆⇩M y"
      unfolding subsetM_def binunion_def' by auto 
    show "z ε y"
      by (rule disjE[OF or, rule_format]) (use ins in blast)+
  qed
qed

end

text ‹The following locale is called Elementary Set Theory (EST) in Baratella and Ferro, "A theory of Sets with the Negation of the Axiom of Infinity", 1993.›

locale L_setext_empty_union_repl_pair = L_setext + L_empty + L_union + L_repl + L_pair

begin

― ‹binunion is the union of a pair›
sublocale L_setext_pair_binunion
proof (unfold_locales, rule allI, rule allI) 
  fix x y
  from pair[rule_format, of x y] 
  obtain pair where pair: "∀v. (v ε pair) = (v = x ∨ v = y)"
    by blast
  show "∃z. ∀v. (v ε z) = (v ε x ∨ v ε y)"
    using union[rule_format, of pair] unfolding pair[rule_format] by simp
qed

end

text ‹The locale  ‹L_setext_empty_union_repl_pair› (i.e., the fragment EST also used by Baratella and Ferro \<^cite>‹BaratellaFerro1993›) is the right context in which to show that the schema of regularity yields existence of transitive closures (least transitive supersets)›

locale L_setext_empty_union_repl_pair_regsch = L_setext + L_empty + L_union + L_repl + L_pair + L_regsch

begin

sublocale L_setext_empty_union_repl_pair
  by unfold_locales

sublocale L_setext_empty_repl
  by unfold_locales

sublocale L_setext_union
  by unfold_locales

lemma transitive_closure_ex:
  shows "∀ x. ∃ z. x ⊆⇩M z ∧ transM z ∧ (∀ u. u ε z ⟷ (∀ t. x ⊆⇩M t ∧ transM t ⟶ u ε t))"
    (is "∀ x. ∃ z. ?TC x z" is "∀ x. ?hasTC x") 
proof
  fix x' :: 'a
  have ind_rule: "SetFormulaPredicate (λΞ. ?hasTC(Ξ 0)) ⟹ (⋀x. (⋀y. y ε x ⟹ ?hasTC y) ⟹ ?hasTC x) ⟹ ?hasTC x'"
    using  regsch_epsind[rule_format, of "λ Ξ. ?hasTC(Ξ 0)" "undefined" x', unfolded fun_upd_same] by argo
  show "∃z. x' ⊆⇩M z ∧ transM z ∧ (∀u. (u ε z) = (∀t. x' ⊆⇩M t ∧ transM t ⟶ u ε t))"
  proof (rule ind_rule)
    fix x
    define TC where "TC = ?TC" ― ‹‹TC x z› ›
    have sfp_tc: "SetFormulaPredicate (λΞ. TC (Ξ 0) (Ξ 1))"
      unfolding TC_def set_defs logsimps by (rule SFP_rules)+
    have tc_fun: "∀u v w. TC u v ∧ TC u w ⟶ v = w"
      unfolding TC_def setext by blast
    show "SetFormulaPredicate (λΞ. ?hasTC(Ξ 0))"
      unfolding TC_def set_defs logsimps by (rule SFP_rules)+
    assume IP: "?hasTC y" if "y ε x" for y
    define tcs where "tcs = ⋃⇩M (replaceM TC x)"
    have repl_x: "∀v. (v ε replaceM TC x) ⟷ (∃u. u ε x ∧ TC u v)" 
      by (rule replace_def'[OF sfp_tc, of _ 0 1 x, simplified fun_upd_same fun_upd_other]) fact   
    hence "transM tcs"
      unfolding TC_def tcs_def union_def' transM_def subsetM_def by blast
    hence tcs_mem: "w ε tcs ⟷ (∃ y. y ε x ∧ (∃ v. TC y v ∧ w ε v))" for w
      unfolding tcs_def using union_def' repl_x by auto 
    show "?hasTC x"
    proof (rule exI[of _ "tcs ∪⇩M x"], fold conj_assoc, rule conjI, rule conjI)
      show "x ⊆⇩M tcs ∪⇩M x"
        unfolding tcs_def set_defs by blast
      show trans: "transM (tcs ∪⇩M x)" 
        unfolding transM_def binunion_def'
      proof (rule allI, rule impI, erule disjE)
        show "y ⊆⇩M tcs ∪⇩M x" if "y ε tcs" for y
          using ‹transM tcs› that unfolding transM_def binunion_def' subsetM_def by blast 
        show "y ⊆⇩M tcs ∪⇩M x" if "y ε x" for y
          unfolding subsetM_def tcs_def binunion_def' union_def' repl_x[rule_format] 
        proof (rule allI, rule impI, rule disjI1)
          fix z
          assume "z ε y" 
          obtain w where  "TC y w"
            unfolding TC_def using IP[OF ‹y ε x›] by blast
          hence "z ε w"
            using ‹z ε y› unfolding TC_def subsetM_def by blast
          hence "(y ε x ∧ TC y w) ∧ z ε w"
            using ‹y ε x› ‹TC y w› by blast
          then show "∃v. (∃u. u ε x ∧ TC u v) ∧ z ε v"
            by blast
        qed
      qed
      show "∀u. (u ε tcs ∪⇩M x) ⟷ (∀t. x ⊆⇩M t ∧ transM t ⟶ u ε t)"
      proof (rule, rule, rule, rule)
        ― ‹ ‹tcs ∪⇩M x› is the least transitive superset›
        fix u t
        assume "u ε tcs ∪⇩M x" "x ⊆⇩M t ∧ transM t"
        consider "∃ y. y ε x ∧ (∃ w. TC y w ∧ u ε w)" | "u ε x"
          using ‹u ε tcs ∪⇩M x› unfolding set_defs tcs_def repl_x[rule_format] by blast
        then show "u ε t"
        proof (cases)
          assume "∃ y. y ε x ∧ (∃ w. TC y w ∧ u ε w)"
          then obtain y w where y_w: "y ε x" "TC y w" "u ε w"
            by blast
          have "y ⊆⇩M t"
            using ‹y ε x› ‹x ⊆⇩M t ∧ transM t› unfolding transM_def subsetM_def by blast
          then show "u ε t"
            using ‹x ⊆⇩M t ∧ transM t› y_w unfolding TC_def by blast
        qed (use ‹x ⊆⇩M t ∧ transM t› subsetM_def in blast) ― ‹the trivial case ‹u ε x››
      qed (use ‹x ⊆⇩M tcs ∪⇩M x› local.trans in blast)  ― ‹the trivial implication: ‹tcs ∪⇩M x› is a transitive  superset›
    qed
  qed
qed

sublocale L_setext_sep_reg_ts
    using transitive_closure_ex by unfold_locales blast   

end

locale L_setext_empty_power_union_repl  = L_setext + L_empty + L_power + L_union + L_repl

― ‹ZF without infinity and regularity.
Axioms enabling reasoning about functions, cardinality, and therefore about Dedekind finiteness.›

begin

sublocale L_setext_empty_power_repl
  by unfold_locales

sublocale L_setext_setsuc_sep
  by unfold_locales

sublocale L_setext_union
  by unfold_locales

sublocale L_setext_empty_union_repl_pair
  by unfold_locales

lemma ordered_pair_mem: assumes "v ε x" "v' ε y" shows "⟨v,v'⟩ ε 𝔓 (𝔓 (x ∪⇩M y))"
proof-
  have "{v}⇩M ε 𝔓 (x ∪⇩M y)" "{v,v'}⇩M ε 𝔓 (x ∪⇩M y)"
    using ‹v ε x› ‹v' ε y› unfolding set_defs by blast+
  thus ?thesis
    unfolding setext[of _ "𝔓 _"] powerset_def'[of _ "𝔓 _"]
      pair_def' subsetM_def ordered_pairM_def  by blast
qed

lemma ordered_pair_mem_union: assumes "⟨u,v⟩ ε r" shows "u ε ⋃⇩M (⋃⇩M r)" "v ε ⋃⇩M (⋃⇩M r)"
proof-
  have "(⟨u,v⟩ ε r ∧ {u,v}⇩M ε ⟨u,v⟩) ∧ u ε {u,v}⇩M" "(⟨u,v⟩ ε r ∧ {u,v}⇩M ε ⟨u,v⟩) ∧ v ε {u,v}⇩M"
    using assms unfolding pair_def' ordered_pairM_def by blast+
  then show "u ε ⋃⇩M (⋃⇩M r)" "v ε ⋃⇩M (⋃⇩M r)" 
    unfolding union_def' by blast+
qed

lemma car_prod_ex: "∃ z. ∀ u. u ε z ⟷ (∃ v v'. v ε x ∧ v' ε y ∧ u = ⟨v,v'⟩)"
proof-
  have "SetFormulaPredicate (λΞ. ∃v v'. v ε Ξ 1 ∧ v' ε Ξ 2 ∧ Ξ 0 = ⟨v,v'⟩)"
    unfolding set_defs logsimps by (rule SFP_rules)+
  from sep[rule_format, of _ "𝔓 (𝔓 (x ∪⇩M y))" "undefined(1:=x,2:=y)", OF this, simplified]
  show ?thesis
    using ordered_pair_mem by metis
qed

lemma car_prod_def': "u ε x ×⇩M y ⟷ (∃ v v'.  v ε x ∧ v' ε y ∧  u = ⟨v,v'⟩)"
  unfolding cartesian_productM_def[rule_format] 
  using collect_def_ex[OF car_prod_ex, of _ x y] ordered_pair_mem by blast

lemma rel_inv_def': "u ε rel_inverseM r ⟷ (∃ a b. ⟨a,b⟩ ε r ∧ u = ⟨b,a⟩)"
proof-
  have SR: "SetRelation (λu r. ∃a b. ⟨a,b⟩ ε r ∧ u = ⟨b,a⟩)"
    unfolding SetRelation_def logsimps by (rule SFP_rules)+ 
  have eq: "(u ε ⋃⇩M (⋃⇩M r) ×⇩M ⋃⇩M (⋃⇩M r) ∧ (∃a b. ⟨a,b⟩ ε r ∧ u = ⟨b,a⟩))
            ⟷ (∃a b. ⟨a,b⟩ ε r ∧ u = ⟨b,a⟩)" for u
    unfolding car_prod_def'[rule_format] using ordered_pair_mem_union by blast 
    show ?thesis
      unfolding rel_inverseM_def 
      using collect_def_ex[of "λ v. (∃ a b. ⟨a,b⟩ ε r ∧ v = ⟨b,a⟩)"]
      sep_SR[rule_format,OF SR, of "⋃⇩M (⋃⇩M r) ×⇩M ⋃⇩M (⋃⇩M r)" r, unfolded eq] by simp
qed

lemma dom_def': "u ε domM r ⟷ (∃v. ⟨u,v⟩ ε r)"
  unfolding domM_def 
proof (rule collect_def_ex)
  have aux: "(∃v. ⟨u,v⟩ ε r) ⟷ (∃ x. x ε r ∧ (∃ w. x = ⟨u,w⟩))" for u
    by blast
  show "∃w. ∀u. (u ε w) = (∃v. ⟨u,v⟩ ε r)"
    unfolding aux
    by (rule repl_SR[rule_format, of "λ x u. ∃ w. x = ⟨u,w⟩" r]) force+
qed

lemma rng_def': "u ε rngM r ⟷ (∃v. ⟨v,u⟩ ε r)" 
  unfolding rngM_def 
proof (rule collect_def_ex)
  have aux: "(∃v. ⟨v,u⟩ ε r) ⟷ (∃ x. x ε r ∧ (∃ w. x = ⟨w,u⟩))" for u
    by blast
  show "∃w. ∀u. (u ε w) = (∃v. ⟨v,u⟩ ε r)"
    unfolding aux
    by (rule repl_SR[rule_format, of "λ x u. ∃ w. x = ⟨w,u⟩" r]) force+
qed

lemma SFP_dom[simp, intro]: "SetFormulaPredicate (λ Ξ. Ξ k = domM (Ξ l))"
  unfolding setext dom_def' logsimps by (rule SFP_rules)+ 

lemma SFP_rng[simp, intro]: "SetFormulaPredicate (λ Ξ. Ξ k = rngM (Ξ l))"
  unfolding setext rng_def' logsimps by (rule SFP_rules)+ 

lemmas[SFP_rules] = SFP_rng[unfolded set_defs logsimps] SFP_dom[unfolded set_defs logsimps]

lemma "SetRelation (λx y. ∃f. one_oneM f ∧ x = domM f ∧ y = rngM f)"
    (is "SetRelation (λ x y. (∃ f. ?P x y f))")
    unfolding set_defs logsimps SetRelation_def by (rule SFP_rules)+

lemma SR_equiv[simp]: "SetRelation (λ x y. x ≈⇩M y)"
  unfolding SetRelation_def  set_defs logsimps by (rule SFP_rules)+

lemma SP_dedekind[simp]: "SetProperty dedekind_fin"
  unfolding SetProperty_def dedekind_fin_def one_oneM_def set_equivalent_def set_defs logsimps by (rule SFP_rules)+

lemma SR_card: "SetRelation cardinality"
  unfolding set_defs logsimps SetRelation_def by (rule SFP_rules)+

lemma rel_inv_dom_rng: "domM (rel_inverseM r) = rngM r" "rngM (rel_inverseM r) = domM r"
  unfolding setext[of _ "rngM _"] setext[of _ "domM _"] dom_def' rng_def' rel_inv_def' ordered_pair_unique by blast+

lemma rel_inv_rel: "relationM f ⟹ relationM (rel_inverseM f)"
  unfolding relationM_def rel_inv_def' by blast  

lemma one_one_inv: "one_oneM f ⟹ one_oneM (rel_inverseM f)"
  unfolding one_oneM_def rel_inv_def' functionM_def ordered_pair_unique using rel_inv_rel by auto

lemma dedekind_setsuc_dedekind: assumes "dedekind_fin x" shows "dedekind_fin (setsucM x t)"
proof (cases "t ε x") 
  assume "¬ t ε x"
  show ?thesis
    unfolding dedekind_fin_def  
  proof (rule allI, rule impI)
    have IH: "u ⊂⇩M x ⟹ x ≈⇩M u ⟹ False" for u
      using assms unfolding dedekind_fin_def  by blast
    show "¬ setsucM x t ≈⇩M y" if "y ⊂⇩M setsucM x t" for y
    proof
      assume "setsucM x t ≈⇩M y"
      then obtain f where f_bij: "one_oneM f" and f_dom: "domM f = setsucM x t" and f_rng: "rngM f = y" 
        unfolding set_equivalent_def by force
      obtain ft where "⟨t,ft⟩ ε f"
        using f_dom[unfolded setext dom_def', rule_format, of t] unfolding setsuc_def' by force          
          ― ‹From this we construct a bijection ‹g› between  strict subset ‹y'› of ‹x› and ‹x›
       There are two different constructions. Depending on whether removing the pair ‹fx,x› from ‹f› 
       yields directly a bijection of ‹x› on its subset, or whether a modification is needed. 
       ›
      have "ft ε y"
        using ‹rngM f = y› ‹⟨t,ft⟩ ε f› unfolding setext rng_def' by blast
      consider "t ε y ∧ ft ≠ t" | "y ⊆⇩M x ∨ ft = t" 
        using ‹y ⊂⇩M setsucM x t› unfolding subsetM_def proper_subsetM_def setsuc_def' by blast
      then show False
      proof (cases) 
        assume "y ⊆⇩M x ∨ ft = t" 
          ― ‹First construction just removes ‹⟨t,ft⟩››
        from sep_SR[rule_format, OF SR_neq]  
        obtain y' where y': "∀ u. u ε y' ⟷ u ε y ∧ u ≠ ft"
          by presburger
        from sep_SR[rule_format, OF SR_neq]  
        obtain g where g: "∀ u. u ε g ⟷ u ε f ∧ u ≠ ⟨t,ft⟩" 
          by presburger
        show False
        proof (rule IH)
          show "y' ⊂⇩M x"
            using y' ‹y ⊆⇩M x ∨ ft = t›[unfolded subsetM_def] ‹ft ε y› proper_subsetM_def ‹y ⊂⇩M setsucM x t›[unfolded proper_subsetM_def setsuc_def' setext[of y]] by metis 
          show "x ≈⇩M y'"
          proof-  
            have "one_oneM g"
              using ‹one_oneM f› g unfolding one_oneM_def functionM_def relationM_def by blast
            have "domM g = x"
              using funD[OF conjunct1[OF f_bij[unfolded one_oneM_def]] ‹⟨t,ft⟩ ε f›] f_dom  ‹¬ t ε x›  
              unfolding setext[of "domM _"] dom_def' y'[rule_format] g[rule_format] one_oneM_def functionM_def setsuc_def' ordered_pair_unique 
              by auto
            have "rngM g = y'"
              using one_one_inj[OF f_bij ‹⟨t,ft⟩ ε f›] f_rng 
              unfolding setext[of "rngM _"] rng_def' y'[rule_format] g[rule_format] ordered_pair_unique
              by blast
            show "x ≈⇩M y'"
              unfolding set_equivalent_def using ‹rngM g = y'› ‹domM g = x› ‹one_oneM g›  by blast 
          qed
        qed
      next
        assume "t ε y ∧ ft ≠ t"
        then obtain pt where "⟨pt,t⟩ ε f"
          using f_rng[unfolded setext rng_def', rule_format, of t] by blast
        hence "pt ε x"
          using f_dom[unfolded setext[of "domM _"] dom_def' setsuc_def']
            one_oneD3[OF f_bij, rule_format, of t ft t] ‹⟨pt,t⟩ ε f› ‹⟨t,ft⟩ ε f› ‹t ε y ∧ ft ≠ t› by blast  
        then show False
        proof- 
          ― ‹the second construction requires to modify the mapping ‹f› by adding ‹⟨fx,px⟩›, not just to restrict ‹f››
          from sep_SR[rule_format, OF SR_neq]
          obtain y' where y': "∀ u. u ε y' ⟷ u ε y ∧ u ≠ t"
            by force
          have sfp: "SetFormulaPredicate (λ Ξ. Ξ 0 = ⟨Ξ 1,Ξ 2⟩ ∨ (Ξ 0 ε Ξ 4 ∧ Ξ 0 ≠ ⟨Ξ 3,Ξ 2⟩ ∧ Ξ 0 ≠ ⟨Ξ 1,Ξ 3⟩))"
            unfolding logsimps by (rule SFP_rules)+
          obtain g where g: "∀ u. u ε g ⟷ (u = ⟨pt,ft⟩ ∨ (u ε f ∧ u ≠ ⟨t,ft⟩ ∧ u ≠ ⟨pt,t⟩))"
            using sep[rule_format, OF sfp, of "setsucM f (⟨pt,ft⟩)" "undefined(1:=pt, 2:=ft, 3:= t ,4:=f)", simplified] by auto
          show False
          proof (rule IH)
            show "y' ⊂⇩M x"
              using ‹y ⊂⇩M setsucM x t› ‹t ε y ∧ ft ≠ t› unfolding proper_subsetM_def y'[rule_format] setsuc_def' setext[of y] setext[of y'] by blast
            show "x ≈⇩M y'"
            proof-  
              have "one_oneM g"
                by (rule one_oneI, unfold g[rule_format] ordered_pair_unique) 
                (use one_oneD1[OF f_bij] in blast, 
                use one_oneD2[OF f_bij] ‹⟨t,ft⟩ ε f› in blast,
                use one_oneD3[OF f_bij] ‹⟨pt,t⟩ ε f› in blast) 
              have "domM g = x"
                unfolding setext[of "domM _"] dom_def' 
              proof (rule allI, rule iffI)
                fix z assume "∃v. ⟨z,v⟩ ε g" 
                show "z ε x"
                  using ‹∃v. ⟨z,v⟩ ε g› ‹pt ε x›  one_oneD3[OF f_bij, rule_format, of t ft _] ‹⟨t,ft⟩ ε f› f_dom[unfolded setext[of "domM _"] setsuc_def' dom_def'] unfolding ordered_pair_unique 
                    g[rule_format] by blast
              next
                fix z assume " z ε x" 
                then show "∃v. ⟨z,v⟩ ε g"
                  unfolding g[rule_format] using f_dom[unfolded setext[of "domM _"] setsuc_def' dom_def'] by (cases "z = pt") (use ‹¬ t ε x› in auto) 
              qed
              have "rngM g = y'"
                unfolding setext[of "rngM _"] rng_def'
              proof (rule allI, rule iffI)
                fix z assume "∃v. ⟨v,z⟩ ε g"
                show "z ε y'"
                  using 
                    one_oneD2[OF f_bij]
                   ‹∃v. ⟨v,z⟩ ε g› ‹ft ε y› ‹t ε y ∧ ft ≠ t›  ‹⟨pt,t⟩ ε f› ‹⟨t,ft⟩ ε f›
                  unfolding f_rng[unfolded setext[of "rngM _"]  rng_def', rule_format, symmetric, of z]  y'[rule_format] ordered_pair_unique g[rule_format] by blast
              next
                fix z assume "z ε y'"
                show "∃v. ⟨v,z⟩ ε g"
                  using ‹z ε y'›[unfolded y'[rule_format]]
                  unfolding f_rng[unfolded setext[of "rngM _"]  rng_def', rule_format, symmetric, of z] g[rule_format] ordered_pair_unique by blast
              qed
              show "x ≈⇩M y'"
                unfolding set_equivalent_def using ‹rngM g = y'› ‹domM g = x› ‹one_oneM g›  by blast 
            qed
          qed
        qed
      qed
    qed
  qed
qed (simp add: assms)    

lemma set_equivalent_sym: "x ≈⇩M y ⟷ y ≈⇩M x"
proof-
  have "x ≈⇩M y ⟹  y ≈⇩M x" for x y
  proof-
    assume "x ≈⇩M y"
    then obtain f where f : "one_oneM f" "x = domM f" "y = rngM f"     
      unfolding set_equivalent_def by blast
    show "y ≈⇩M x"
      unfolding set_equivalent_def 
      by (rule exI[of _ "rel_inverseM f"]) (simp add: one_one_inv[OF ‹one_oneM f›] f(2,3) rel_inv_dom_rng) 
  qed
  thus ?thesis 
    by blast
qed

lemma compose_def': "u ε f ∘⇩M g ⟷ (∃a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩)"
proof-
  have ex: "∃w. ∀u. (u ε w) = (u ε domM g ×⇩M rngM f  ∧ (∃a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩))"
    using sep[rule_format, OF SFP_compose[of 1 2 0], of "domM g ×⇩M rngM f" "undefined(1:=g, 2:= f)"] 
    by simp
  have aux: "u ε domM g ×⇩M rngM f  ∧ (∃a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩) ⟷ (∃a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩)" for u
    using dom_def' rng_def' car_prod_def' by auto
  have "u ε f ∘⇩M g ⟷ (∃a b c. ⟨a,b⟩ ε g ∧ ⟨b,c⟩ ε f ∧ u = ⟨a,c⟩)" (is "u ε f ∘⇩M g ⟷ ?Q u")
    unfolding composeM_def  
    using collect_def_ex[of "λ u. ?Q u", OF ex[unfolded aux]].  
  then show ?thesis
    unfolding car_prod_def' dom_def'[of _ g] rng_def'[of _ f]  by blast 
qed  

lemma rel_comp: assumes "relationM f" "relationM g" shows "relationM (f ∘⇩M g)"
  using assms unfolding relationM_def compose_def' by blast

lemma fun_comp: assumes "functionM f" "functionM g" shows "functionM (f ∘⇩M g)"
  using assms rel_comp unfolding functionM_def  compose_def' ordered_pair_unique by blast 

lemma one_one_comp: assumes "one_oneM f" "one_oneM g" shows "one_oneM (f ∘⇩M g)"
  using assms fun_comp unfolding one_oneM_def  compose_def' ordered_pair_unique by blast  

lemma set_equivalent_trans: assumes "x ≈⇩M y" "y ≈⇩M z" shows "x ≈⇩M z"
proof-
  obtain f1 where f1: "one_oneM f1" and  "x = domM f1" "y = rngM f1"
    using ‹x ≈⇩M y› unfolding set_equivalent_def by blast
  obtain f2 where f2: "one_oneM f2" and "y = domM f2" "z = rngM f2"
    using ‹y ≈⇩M z› unfolding set_equivalent_def by blast
  have "one_oneM (f2 ∘⇩M f1)"
    using f1 f2 one_one_comp by blast
  have "x = domM (f2 ∘⇩M f1)"
     unfolding dom_def'  setext unfolding compose_def' ordered_pair_unique
   proof (rule allI, rule iffI)
     fix u assume "∃v a b c. ⟨a,b⟩ ε f1 ∧ ⟨b,c⟩ ε f2 ∧ u = a ∧ v = c"
     then show "u ε x"
       unfolding ‹x = domM f1›[unfolded setext dom_def', rule_format] by blast
   next
     fix u assume "u ε x"
     then obtain b where ‹⟨u,b⟩ ε f1› "b ε y"
       unfolding ‹x = domM f1›[unfolded setext dom_def', rule_format]
                 ‹y = rngM f1›[unfolded setext rng_def', rule_format] by blast
     then obtain c where ‹⟨b,c⟩ ε f2› "c ε z"
       unfolding ‹y = domM f2›[unfolded setext dom_def', rule_format]
                 ‹z = rngM f2›[unfolded setext rng_def', rule_format] by blast
     show "∃v a b c. ⟨a,b⟩ ε f1 ∧ ⟨b,c⟩ ε f2 ∧ u = a ∧ v = c"
       using ‹⟨u,b⟩ ε f1› ‹⟨b,c⟩ ε f2› by auto
   qed
  have "z = rngM (f2 ∘⇩M f1)"
     unfolding rng_def'  setext unfolding compose_def' ordered_pair_unique
   proof (rule allI, rule iffI)
     fix u assume "∃v a b c. ⟨a,b⟩ ε f1 ∧ ⟨b,c⟩ ε f2 ∧ v = a ∧ u = c"
     then show "u ε z"
       unfolding ‹z = rngM f2›[unfolded setext rng_def', rule_format] by blast
   next
     fix u assume "u ε z"
     then obtain b where ‹⟨b,u⟩ ε f2› "b ε y"
       unfolding ‹y = domM f2›[unfolded setext dom_def', rule_format]
                 ‹z = rngM f2›[unfolded setext rng_def', rule_format] by blast
     then obtain c where ‹⟨c,b⟩ ε f1› "c ε x"
       unfolding ‹x = domM f1›[unfolded setext dom_def', rule_format]
                 ‹y = rngM f1›[unfolded setext rng_def', rule_format] by blast
     show "∃v a b c. ⟨a,b⟩ ε f1 ∧ ⟨b,c⟩ ε f2 ∧ v = a ∧ u = c"
       using ‹⟨b,u⟩ ε f2› ‹⟨c,b⟩ ε f1› by auto
   qed
  show ?thesis
      unfolding set_equivalent_def
      using ‹one_oneM (f2 ∘⇩M f1)› ‹x = domM (f2 ∘⇩M f1)› ‹z = rngM (f2 ∘⇩M f1)› by blast 
qed

lemma union_of_ords_regular: assumes "∀ y. y ε s ⟶ ordM y"
  shows "regular (⋃⇩M s)"
  using assms ord_mem_ord set_of_ords_regular union_def' by blast

lemma union_of_ords_ord: assumes "∀ y. y ε s ⟶ ordM y"
  shows "ordM (⋃⇩M s)"   
proof-
  have t: "transM (⋃⇩M s)"
    using assms epschain_def ordM_def union_trans_trans by blast 
  have r: "regular (⋃⇩M s)"
    by (simp add: assms union_of_ords_regular)
  have o: "ordM v" if "v ε (⋃⇩M s)" for v
    using assms(1) ord_mem_ord that union_def' by blast
  show "ordM (⋃⇩M s)"
    unfolding ordM_def epschain_def using t r o ordM_total by blast
qed

lemma union_ord: assumes "ordM x" shows "ordM (⋃⇩M x)"
  using assms ord_mem_ord union_of_ords_ord by blast

lemma non_limit_union_ord_mem: assumes "∀ u. u ε s ⟶ ordM u" "is_sucM (⋃⇩M s)"
  shows "⋃⇩M s ε s"
proof-
  obtain m where m: "∀ z. z ε ⋃⇩M s ⟷ z ε m ∨ z = m"
    using ‹is_sucM (⋃⇩M s)› is_sucM_def by blast
  then obtain ymax where "ymax ε s" "m ε ymax" 
    unfolding union_def' by blast
  from assms(1)[rule_format, OF ‹ymax ε s›]
  have "⋃⇩M s ⊆⇩M ymax"
    unfolding subsetM_def m[rule_format] using ‹m ε ymax› using ordM_trans[of ymax _ m] by blast 
  then have "ymax = ⋃⇩M s"
    using ‹ymax ε s› unfolding setext subsetM_def subsetM_def union_def' by blast
  then show "⋃⇩M s ε s"
    using ‹ymax ε s› by blast 
qed

lemma limit_ord: assumes "∀ u. u ε s ⟶ ordM u ∧ setsucM u u ε s"
  shows "¬ is_sucM (⋃⇩M s)"
  by (metis assms non_limit_union_ord_mem ordM_regular regular_not_self_mem_sep setsuc_def'
      union_def') 

lemma not_limit_ord: assumes "ordM x" "is_sucM x" 
  shows "x = setsucM (⋃⇩M x) (⋃⇩M x)"
proof-
  obtain m where m: "x = setsucM m m"
    using ‹is_sucM x› unfolding setext is_sucM_def setsuc_def' by blast
  hence "ordM m"
    using ‹ordM x› ord_mem_ord setsuc_def' by presburger
  have "m = ⋃⇩M x"
    unfolding m setext[of m] union_def' setsuc_def'  
    using ordM_trans[OF ‹ordM m›] by blast  
  then show ?thesis
    using m by force
qed

lemma natM_fin: assumes "s ⊆⇩M x" "s ≠ ∅" "∀ u. u ε s ⟶ setsucM u u ε s" 
  shows "¬ natM x"
proof
  have "∃ u. u ε ⋃⇩M s"
    using assms union_def'[of _ s] setsuc_def' emptyset_def' by metis
  assume "natM x"
  from natM_D[OF this]
  have "⋃⇩M s ⊆⇩M x"
    unfolding subsetM_def union_def' using ordM_trans ‹s ⊆⇩M x›[unfolded  subsetM_def] by blast 
  have "ordM (⋃⇩M s)"
    using ‹ordM x› union_of_ords_ord ord_mem_ord ‹s ⊆⇩M x›[unfolded subsetM_def] by blast
  have "natM (⋃⇩M s)"
    using ordM_subset_mem[OF ‹ordM x› ‹ordM (⋃⇩M s)›, unfolded proper_subset_def'] ‹natM x›
     nat_mem_nat ‹⋃⇩M s ⊆⇩M x› by blast
  from nat_is_suc[OF this ‹∃ u. u ε ⋃⇩M s›]
  show False
    using assms limit_ord natM_D[OF nat_mem_nat[OF ‹natM x›]] unfolding subsetM_def by force
qed

lemma nat_induction_sfp: assumes "SetFormulaPredicate P" and  "P (Ξ(0:=∅))"  and
  step: "⋀ x. natM x ⟹ P (Ξ(0:=x)) ⟹ P (Ξ(0:=setsucM x x))" and "natM x"
  shows "P (Ξ(0:=x))"
proof (rule ccontr)
  assume "¬ P (Ξ(0:=x))"
  define v where "v = separationM x (λ x. P(Ξ(0:=x)))"
  from separ_def_SFP[OF ‹SetFormulaPredicate P›]
  have v: "u ε v ⟷ u ε x ∧ P(Ξ(0:=u))" for u
    unfolding v_def by simp 
  hence "∅ ε v"
    using ‹P (Ξ(0:=∅))› ‹¬ P (Ξ(0:=x))› ‹natM x› emp_natM empty_is_empty ordM_total unfolding natM_def by fast
  have "(setsucM y y) ε v" if "y ε v" for y
    unfolding v[of "setsucM y y"] using ‹¬ P (Ξ(0:=x))› ‹natM x› that[unfolded v[of y]] step[of y] ord_mem_suc[of x y] nat_mem_nat[of x y] natM_D[OF ‹natM x›]
    by fast
  thus False
    using ‹∅ ε v› notE[OF natM_fin[of v x], OF _ _ _ ‹natM x›] v
    by (metis emptyset_def' subsetM_def) 
qed

― ‹Schema of induction for natural numbers›
lemma nat_induction_sp: assumes "SetProperty P" and  "P ∅" and "natM x" and
  step: "⋀ x. natM x ⟹ P x ⟹ P (setsucM x x)"
shows "P x"
  using assms unfolding SetProperty_def using nat_induction_sfp by force  

theorem nat_tarski_fin: assumes "natM x" shows "tarski_fin x"
  using nat_induction_sp[OF SP_tarski empty_tarski ‹natM x›] tarski_setsuc_tarski by blast

lemma nat_dedekind_finite: assumes "natM x"  shows "dedekind_fin x"
  using nat_induction_sp[OF SP_dedekind empty_dedekind ‹natM x›] dedekind_setsuc_dedekind by blast

lemma card_emp: "cardinality ∅ ∅" 
proof-
  have "natM ∅"
    by simp
  moreover have "one_oneM ∅" 
    unfolding one_oneM_def functionM_def relationM_def by simp
  moreover have "∅ = domM ∅" "∅ = rngM ∅"                          
    unfolding setext dom_def' rng_def' by simp_all 
  ultimately show ?thesis
    unfolding cardinality_def set_equivalent_def 
    using exI[of "λ f.  one_oneM f ∧ ∅ = domM f ∧ ∅ = rngM f" ∅] by blast
qed

lemma nat_equiv_unique: assumes "natM x" "natM y" "x ≈⇩M y"
  shows "x = y"
proof (rule ccontr)
  assume "x ≠ y"
  have "¬ y ε x"  
    using ‹x ≠ y› assms nat_dedekind_finite[unfolded dedekind_fin_def, rule_format, OF ‹natM x›] ordM_D1[OF natM_D[OF ‹natM x›]] subsetM_def proper_subset_def' by blast 
  have "¬ x ε y"  
    using ‹x ≠ y› assms nat_dedekind_finite[unfolded dedekind_fin_def, rule_format, OF ‹natM y›] ordM_D1[OF natM_D[OF ‹natM y›]] 
     subsetM_def proper_subset_def' set_equivalent_sym[of x y] by blast
  show False
    using ‹¬ x ε y› ‹¬ y ε x› ‹x ≠ y›  ordM_total[OF natM_D natM_D, OF assms(1,2)] by blast
qed     

lemma card_fun: assumes "cardinality x n" "cardinality x m" shows "n = m"
  using assms unfolding cardinality_def  using nat_equiv_unique set_equivalent_sym set_equivalent_trans  by blast

end

locale L_setext_empty_power_union_repl_reg  = L_setext + L_empty + L_power + L_union + L_repl 
+ L_reg

begin
text ‹Some consequences of the axiom of regularity›

sublocale L_setext_empty_power_union_repl
  by unfold_locales

lemma mem_not_refl: "¬ x ε x"
 by (simp add: regular_not_self_mem)    

lemma mem_antisym: "¬ (u ε v ∧ v ε u)"
  by (meson any_reg regular_antisym_mem setsuc)   

lemma  suc_unique:  assumes "setsucM c c = setsucM d d" 
  shows "c = d"
proof (rule ccontr)
  assume "c ≠ d"
  from assms[unfolded setext setsuc_def'[of "_ ∪⇩M _"], unfolded setsuc_def']
  have "c ε d" "d ε c"
    using ‹c ≠ d› by blast+
  thus False
    using mem_antisym by blast
qed

lemma mem_neq_singleton: "x ≠ {x}⇩M"
  by (metis reg singleton_def')
   
lemma suc_subset[simp]: "z ⊂⇩M setsucM z z"
  unfolding proper_subsetM_def  setext setsuc_def'
  singleton_def' using mem_not_refl[of z] by blast

lemma card_setsuc: assumes "¬ y ε x" "cardinality x m" shows "cardinality (setsucM x y)  (setsucM m m)"
proof-
  obtain f where "one_oneM f" "x = domM f" "m = rngM f" "natM m"
    using ‹cardinality x m› unfolding cardinality_def set_equivalent_def by blast
  let ?f = "setsucM f (⟨y,m⟩)"
  have "natM (setsucM m m)"
    by (simp add: ‹natM m› nat_suc_nat)
  have "setsucM x y = domM ?f"
    using ‹x = domM f› unfolding setext dom_def' by auto
  have "setsucM m m = rngM ?f"
    using ‹m = rngM f› unfolding setext rng_def' by auto
  have "relationM ?f"
    unfolding relationM_def
    using ‹one_oneM f› functionM_def one_oneM_def relationM_def by auto 
  then have "functionM ?f"
    unfolding functionM_def
    using ‹one_oneM f› ‹x = domM f› ‹¬ y ε x› dom_def' funD one_oneD3 by auto 
  then have "one_oneM ?f"
    unfolding one_oneM_def 
    using   ‹¬ y ε x› one_one_inj[OF ‹one_oneM f›] ‹m = rngM f› mem_not_refl[of m] 
    rng_def'  by auto 
  show ?thesis
    unfolding cardinality_def set_equivalent_def 
    using ‹setsucM m m = rngM ?f› ‹natM (setsucM m m)› ‹one_oneM ?f› ‹setsucM x y = domM ?f› by blast
qed                                    

end

subsection ‹Successor induction› 

text ‹An important fragment of the theory of hereditarily finite sets. The finiteness principle used is the induction schema for set formulas.
 This route to axiomatizating ZFfin is developed in Vopěnka: Mathematics in the alternative set theory \<^cite>‹Vopenka1979›.
Notice that no regularity principles are used in this fragment.›

locale L_setext_empty_setsuc_setind = L_setext + L_empty + L_setsuc + L_setind 

begin

sublocale L_setext_empty_setsuc
  by unfold_locales

lemma binunion_ex:
  shows "∃ z. (∀ u. u ε z ⟷ u ε x ∨ u ε x')" (is "?P x x'")
proof-
  have SR: "SetRelation ?P"
    unfolding SetRelation_def logsimps by (rule SFP_rules)+ 
  show ?thesis
  proof (rule  setind[rule_format, OF  SR[unfolded SetRelation_def], of "undefined(0:=x,1:=x')", simplified], force)
    fix x y :: 'a
    assume ex: "∃z. ∀u. (u ε z) ⟷ (u ε x ∨ u ε x')"
    then show "∃z. ∀u. (u ε z) ⟷ (u ε x ∨ u = y ∨ u ε x')"
      unfolding setsuc_def' using setsuc[rule_format, of _ y]  by metis
  qed  
qed

sublocale L_union
proof (unfold_locales, rule allI, rule setind_SP[rule_format])
  show "∃z. ∀u. (u ε z) ⟷ (∃v. v ε ∅ ∧ u ε v)"
    by (meson empty_is_empty)
next 
  fix x y
  have aux: "(∀u. (u ε z) ⟷ (∃v. (v ε x ∨ v = y) ∧ u ε v)) ⟷ (∀u. (u ε z) ⟷ (∃ v. v ε x ∧ u ε v) ∨ u ε y)" for z
    by blast
  let ?Q = "λ z. ∀u. (u ε z) = (∃v. (v ε x ∨ v = y) ∧ u ε v)"
  assume "∃z. ∀u. (u ε z) ⟷ (∃v. v ε x ∧ u ε v)"
  thus "∃z. ∀u. (u ε z) ⟷ (∃v. v ε (setsucM x y) ∧ u ε v)"
    unfolding setsuc_def' aux using binunion_ex[rule_format, of _ y] by metis
next
  show "SetProperty (λa. ∃z. ∀u. (u ε z) = (∃v. v ε a ∧ u ε v))"
    unfolding SetProperty_def logsimps by (rule SFP_rules)+
qed

sublocale L_repl
proof (unfold_locales, rule impI, rule allI)
  fix P x Ξ 
  assume "SetFormulaPredicate P" and func: "∀u. ∃!v. P (Ξ(0 := u, 1 := v))"
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where m: "∀ Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶  P Ξ = P Ξ'"
    by blast
  hence small: "P (Ξ(m := x, 0 := u, 1 := v)) = P (Ξ(0 := u, 1 := v))" for u v x
    by simp
  let ?P = "λΞ. ∃z. ∀v. (v ε z) = (∃u. u ε Ξ m ∧ P (Ξ (0:=u,1:=v)))"
  have sfp: "SetFormulaPredicate ?P"
    by (rule SFP_replace) fact+  
  note aux_rule = setind_var[rule_format, of ?P Ξ m x, OF sfp, unfolded small, simplified, unfolded One_nat_def[symmetric]] 
  show "∃z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0 := u, 1 := v)))"
  proof (rule aux_rule)
    fix x y
    assume "∃z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0 := u, 1 := v)))"
    then obtain z where z: "∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0 := u, 1 := v)))"
      by blast
    obtain y' where y': "P (Ξ(0 := y, 1 := y'))"
      using func by blast
    show "∃z. ∀v. (v ε z) = (∃u. (u ε x ∨ u = y) ∧ P (Ξ(0 := u, 1 := v)))"
      by (rule exI[of "λ z. ∀v. (v ε z) = (∃u. (u ε x ∨ u = y) ∧ P (Ξ(0 := u, 1 := v)))" "setsucM z y'"])
       (unfold setsuc_def', use y' z func in blast)
  qed (simp only: empty)
qed

sublocale L_setext_empty_repl
  by unfold_locales

lemma setsuc_separ: assumes "y ε u" 
  shows "u = setsucM (separationM u (λ x. x ≠ y)) y"
proof-
  have sfp: "SetFormulaPredicate (λΞ. Ξ 0 ≠ Ξ 1)"
    by (rule SFP_rules)+
  show ?thesis 
    unfolding setext[of u] setsuc_def' separ_def_SR[of "(≠)" _ u y, unfolded SetRelation_def, OF sfp] using ‹y ε u› by blast
qed

lemma setsuc_subset_setind: "u ⊆⇩M setsucM x y ⟷ u ⊆⇩M x ∨ (∃ u'. u' ⊆⇩M x ∧ u = setsucM u' y)"
proof
  assume "u ⊆⇩M setsucM x y"
  show "u ⊆⇩M x ∨ (∃u'. u' ⊆⇩M x ∧ u = setsucM u' y)"
  proof (unfold disj_imp, rule impI)   
    assume "¬ u ⊆⇩M x"
    hence "y ε u"
      using ‹u ⊆⇩M setsucM x y› subsetM_def setsuc_def' by auto 
    have "separationM u (λ x. x ≠ y)  ⊆⇩M x"
      using ‹u ⊆⇩M setsucM x y› unfolding subsetM_def
      separ_def_SR[of "(≠)", unfolded SetRelation_def, OF SFP_neg[OF SFP_eq]] setsuc_def' by blast
    with setsuc_separ[OF ‹y ε u›]
    show "∃u'. u' ⊆⇩M x ∧ u = setsucM u' y"
      by blast
  qed
next
  assume "u ⊆⇩M x ∨ (∃u'. u' ⊆⇩M x ∧ u = setsucM u' y)"
  then show "u ⊆⇩M setsucM x y "
  proof
    show "u ⊆⇩M x ⟹ u ⊆⇩M setsucM x y"
      unfolding subsetM_def setsuc_def' by blast
    assume "∃u'. u' ⊆⇩M x ∧ u = setsucM u' y"
    then show "u ⊆⇩M setsucM x y"
      unfolding subsetM_def setext[of u] setsuc_def' by blast
  qed
qed
        
sublocale L_power
proof (unfold_locales, rule allI)
  fix x
  show "∃y. ∀u. (u ε y) = u ⊆⇩M x"
proof (rule setind_SP[rule_format])
  show "SetProperty (λa. ∃y. ∀u. (u ε y) = u ⊆⇩M a)"
    unfolding SetProperty_def logsimps set_defs by (rule SFP_rules)+
  show "∃y. ∀u. (u ε y) = u ⊆⇩M ∅"
    using singleton_def'[of _ "∅"]  by auto   
    fix x y 
    let ?P = "λ Ξ. Ξ 1 = setsucM (Ξ 0) (Ξ 2)"
    have sfp: "SetFormulaPredicate ?P"
      unfolding setext logsimps set_defs by (rule SFP_rules)+
    have ex1: "∃! v. v = u ∪⇩M {y}⇩M" for u
      by blast 
    have binunion_def': "u ε x ∪⇩M y ⟷ u ε x ∨ u ε y" for u x y
       using collect_def_ex[OF binunion_ex[rule_format, of x y], folded binunionM_def].
    assume "∃z. ∀u. (u ε z) = u ⊆⇩M x"
    then obtain z where z: "∀u. (u ε z) = u ⊆⇩M x"
      by blast
    obtain z' where z': "∀ v. v ε z' ⟷ (∃ u. u ε z ∧ v = setsucM u y)"
      using replf[OF sfp, of "undefined(2:=y)",  simplified] by blast
    show "∃z. ∀u. (u ε z) = u ⊆⇩M setsucM x y"
      by (rule exI[of "λ z.(∀u. (u ε z) = u ⊆⇩M setsucM x y)" "z ∪⇩M z'"])
        (unfold binunion_def' setsuc_subset_setind, use z z' in simp)
  qed 
qed


― ‹Axioms of ZF without infinity and regularity are theorems›

sublocale L_setext_empty_power_union_repl
  by unfold_locales

lemma min_subset_ex: assumes "u ≠ ∅" shows "∃ z. z ε u ∧ (∄ w. w ε u ∧ w ⊂⇩M z)"
proof (rule mp[OF _ assms], rule setind_SP[rule_format])
  show "SetProperty (λa. a ≠ ∅ ⟶ (∃z. z ε a ∧ (∄w. w ε a ∧ w ⊂⇩M z)))"
    unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+
next
  fix  x y
  assume IH: "x ≠ ∅ ⟶ (∃z. z ε x ∧ (∄w. w ε x ∧ w ⊂⇩M z))"
  show "setsucM x y ≠ ∅ ⟶ (∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ w ⊂⇩M z))" 
  proof (rule impI, cases "x = ∅")
    assume "x = ∅"
    then show "∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ w ⊂⇩M z)"
      using setsuc_def' by force
  next
    assume "x ≠ ∅"
    from IH[rule_format, OF this]
    obtain u where "u ε x" and nex: "∄w. w ε x ∧ w ⊂⇩M u"
      by blast
    show "∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ w ⊂⇩M z)"
    proof (cases "y ⊂⇩M u")
      assume "y ⊂⇩M u"
      have "y ε setsucM x y"
        using setsuc_def' by auto
      show ?thesis
      proof (rule exI[of _ y], rule conjI[OF ‹y ε setsucM x y›], rule notI)
        assume "∃w. w ε setsucM x y ∧ w ⊂⇩M y"
        then show False
          using ‹y ⊂⇩M u› ‹y ε setsucM x y› nex proper_subsetM_trans[OF _ ‹y ⊂⇩M u›]
          by (metis proper_subsetM_def setsuc_def') 
      qed
    next
      assume "¬ y ⊂⇩M u"
      show ?thesis
        by (rule exI[of _ u]) (use setsuc_def' ‹u ε x› nex ‹¬ y ⊂⇩M u› in metis)
    qed
  qed
qed simp

text ‹A general variant of Tarski finiteness axiom (also proved in Vopěnka's book). 
Nonempty sets have maximal (and minimal) elements under inclusion.›

lemma max_subset_ex: assumes "u ≠ ∅" shows "∃ z. z ε u ∧ (∄ w. w ε u ∧ z ⊂⇩M w)"
proof (rule mp[OF _ assms], rule setind_SP[rule_format])
  show "SetProperty (λa. a ≠ ∅ ⟶ (∃z. z ε a ∧ (∄w. w ε a ∧ z ⊂⇩M w)))"
    unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+
next
  fix  x y
  assume IH: "x ≠ ∅ ⟶ (∃z. z ε x ∧ (∄w. w ε x ∧ z ⊂⇩M w))"
  show "setsucM x y ≠ ∅ ⟶ (∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ z ⊂⇩M w))" 
  proof (rule impI, cases "x = ∅")
    assume "x = ∅"
    then show "∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ z ⊂⇩M w)"
      using setsuc_def' by force
  next
    assume "x ≠ ∅"
    from IH[rule_format, OF this]
    obtain u where "u ε x" and nex: "∄w. w ε x ∧ u ⊂⇩M w"
      by blast
    show "∃z. z ε setsucM x y ∧ (∄w. w ε setsucM x y ∧ z ⊂⇩M w)"
    proof (cases "u ⊂⇩M y")
      assume "u ⊂⇩M y"
      have "y ε setsucM x y"
        using setsuc_def' by auto
      show ?thesis
      proof (rule exI[of _ y], rule conjI[OF ‹y ε setsucM x y›], rule notI)
        assume "∃w. w ε setsucM x y ∧ y ⊂⇩M w"
        then show False
          using ‹u ⊂⇩M y› ‹y ε setsucM x y› nex proper_subsetM_trans[OF _ ‹u ⊂⇩M y›]
          by (metis proper_subsetM_def setsuc_def')
      qed
    next
      assume "¬ u ⊂⇩M y"
      show ?thesis
        by (rule exI[of _ u]) (use setsuc_def' ‹u ε x› nex ‹¬ u ⊂⇩M y› in metis)
    qed
  qed
qed simp

lemma max_mem: assumes "P n" "n ε x" "SetProperty P"
  shows "∃ m. m ε x ∧ P m ∧ (∀ k. k ε x ∧ P k ⟶ ¬ m ⊂⇩M k)"
proof (rule ccontr)
  assume contr: "∄m. m ε x ∧ P m ∧ (∀k. k ε x ∧ P k ⟶ ¬ m ⊂⇩M k)"
  hence chain: "∃ k. k ε x ∧ P k ∧  m ⊂⇩M k" if a: "P m" "m ε x" for m
    using that by blast
  define y where "y = separationM x P"    
  from separ_def_SP[OF ‹SetProperty P›, of _ x, folded y_def]
  have y_def: "(u ε y) ⟷ (u ε x ∧ P u)" for u
    by simp
  have "y ≠ ∅"
    using assms y_def by force
  show False
    using max_subset_ex[OF ‹y ≠ ∅›] chain unfolding y_def by blast
qed

sublocale L_tarski
  using max_subset_ex 
  by unfold_locales (simp add: tarski_fin_def, metis empty)  

sublocale L_dedekind
  by unfold_locales
  (use setind_SP[rule_format, OF SP_dedekind empty_dedekind] dedekind_setsuc_dedekind in blast) 
    
lemma fun_images: assumes "SetFormulaPredicate P" and "∀ u. (∃! v. P(Ξ(0:=u,1:=v)))"
  shows "∃ z. (∀ v. v ε z ⟷ (∃ u. u ε x ∧ P(Ξ(0:=u,1:=v))))" 
proof-
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where "∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ P Ξ = P Ξ'" 
    by blast
  hence m: "∀Ξ Ξ'. (∀i<m+2. Ξ i = Ξ' i) ⟶ P Ξ = P Ξ'" 
    by simp
  have small: "P (Ξ(Suc (Suc m) := x, 0 := u, Suc 0 := v)) = P (Ξ(0 := u, Suc 0 := v))" for u v x
    by (rule m[rule_format]) simp 
  let ?P = "λ X. ∃z. ∀v. (v ε z) = (∃u. u ε (X (m+2)) ∧ P (X(0 := u, 1 := v)))"
  have "SetFormulaPredicate ?P"
    using SFP_replace[OF ‹SetFormulaPredicate P› m].
  note aux_rule = setind_var[OF this, of "Ξ((m+2):= x)" "m+2", simplified, unfolded small, folded One_nat_def] 
  show "∃ z. (∀ v. v ε z ⟷ (∃ u. u ε x ∧ P(Ξ(0:=u,1:=v))))"
  proof (rule aux_rule[rule_format]) 
    show "∃z. ∀v. ¬ v ε z"
      using empty by blast
  next
    fix x y
    assume "∃z. ∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0 := u, 1 := v)))"
    then obtain z where z_def: "∀v. (v ε z) = (∃u. u ε x ∧ P (Ξ(0 := u, 1 := v)))" 
      by blast
    obtain y' where "P (Ξ(0 := y, 1 := y'))"
      using assms(2) by blast
    have witness: "∀ v. v ε setsucM z y' ⟷ (∃ u. u ε setsucM x y ∧ P (Ξ(0 := u, 1 := v)))"
      unfolding setsuc_def' using  ‹P (Ξ(0 := y, 1 := y'))› assms(2) z_def by auto
    show "∃z. ∀v. (v ε z) = (∃u. (u ε x ∨ u = y) ∧ P (Ξ(0 := u, 1 := v)))"
      by (rule exI[of _ "setsucM z y'"]) (use witness in force) 
  qed
qed

sublocale L_fin
proof (unfold_locales, rule notI)
  assume "∃x. ∅ ε x ∧ (∀y. y ε x ⟶ setsucM y y ε x)"
  then obtain x where "∅ ε x" and suc: "∀y. y ε x ⟶ setsucM y y ε x" 
    by blast
  have SP: "SetProperty (λ x. regular x ∧ transM x)"
    unfolding SetProperty_def unfolding set_defs logsimps by (rule SFP_rules)+
  from sep_SP[OF this, rule_format, of x]
  obtain x' where x': "∀ u. u ε x' ⟷ u ε x ∧ regular u ∧ transM u"
    by blast
  have "x' ≠ ∅" "∅ ε x'"
    using x' ‹∅ ε x› by force+ 
  have suc': "y ε x' ⟶ setsucM y y ε x'" for y
    unfolding x'[rule_format] using suc by (simp add: regular_setsuc trans_suc_trans) 
  from max_subset_ex[OF ‹x' ≠ ∅›]
  obtain xmax where "xmax ε x'" "∄ w. w ε x' ∧ xmax ⊂⇩M w"
    by blast
  with suc'[rule_format, OF ‹xmax ε x'›]
  have "¬ xmax ⊂⇩M setsucM xmax xmax"
    by blast
  then have "xmax ε xmax"
    unfolding set_defs setext[of xmax] by blast
  then show False
    using ‹xmax ε x'› regular_not_self_mem x' by blast
qed    

theorem ord_is_suc: assumes "ordM x"  shows "x = ∅ ∨ is_sucM x"
  using assms empty_mem_ord fin ord_limit_or_suc by blast

theorem ord_iff_nat: "ordM x ⟷ natM x"
proof (rule iffI)
  assume "ordM x"
  show "natM x"
  proof (cases "x = ∅") 
    assume "x ≠ ∅"
    show "natM x"
    proof (rule natM_I, fact)
      fix v assume "∃ u. u ε v" "v ε x" 
      then show "is_sucM v"
        using ord_mem_ord[OF ‹ordM x› ‹v ε x›] ord_is_suc[of v] by fastforce
    qed (use ord_is_suc[OF ‹ordM x›] ‹x ≠ ∅› in auto)
  qed simp
qed (use natM_def in blast)

lemma ord_iff_empty_or_suc: "ordM x ⟷ x = ∅ ∨ (∃ y. ordM y ∧ x = setsucM y y)"
  by (metis emp_natM not_limit_ord ord_is_suc ord_iff_nat ord_suc_ord union_ord)

lemma union_of_ords_mem:  assumes "∀ y. y ε s ⟶ ordM y" "s ≠ ∅" 
  shows "⋃⇩M s ε s"
  using ‹s ≠ ∅› emptyset_def' non_limit_union_ord_mem[OF assms(1)] ord_is_suc[OF union_of_ords_ord[OF assms(1)]]
    union_def' by metis

end

subsection ‹Negation of inf›

text ‹ZF with inf replaced by fin›

locale L_setext_empty_power_union_repl_reg_fin  = L_setext + L_empty + L_power + L_union + L_repl + L_reg + L_fin

begin

sublocale L_setext_empty_power_union_repl_reg
  by unfold_locales

sublocale L_setind
proof (unfold_locales, (rule impI)+, rule allI, rule ccontr)
  fix P Ξ x
  assume "SetFormulaPredicate P" "P (Ξ (0:= ∅))" and step:  "∀x y. P (Ξ (0:= x)) ⟶ P ((Ξ (0:=setsucM x y)))" and "¬ (P (Ξ (0:=x)))"
  have sfp: "SetFormulaPredicate (λ Ξ. cardinality (Ξ 0) (Ξ 1))"
    unfolding set_defs logsimps by (rule SFP_rules)+
  have cinj: "cardinality u v ∧ cardinality u w ⟹ v = w" for u v w
    using card_fun by auto
  from sep[OF ‹SetFormulaPredicate P›, rule_format, of"𝔓 x" Ξ]
  obtain s where s: "∀u. (u ε s) = (u ε 𝔓 x ∧ P (Ξ(0 := u)))"
    by blast
  from replp_vars[rule_format, OF sfp, of Ξ 0 1 s, simplified] 
  obtain m where m: "∀v. (v ε m) = (∃a. a ε s ∧ cardinality a v) " 
    using cinj by blast
  have "∅ ε m"
    using card_emp exI[of "λ x. x ⊆⇩M x ∧ P (Ξ (0:=x, 1:=∅)) ∧ cardinality x ∅" ∅] ‹P (Ξ (0:=∅))› 
    unfolding m[rule_format] powerset_def' subsetM_def s[rule_format]
    using emptyset_def'  by auto 
  have "setsucM n n ε m" if "n ε m" for n
  proof-                  
    obtain y where "y ε 𝔓 x" "cardinality y n" "P (Ξ (0:=y))"
      using m  ‹n ε m› s by fast
    obtain y' where "y' ε x" "¬ y' ε y" 
      using ‹y ε 𝔓 x› ‹P (Ξ (0:=y))› ‹¬ P (Ξ (0:=x))› subsetM_antisym powerset_def' subsetM_def by blast
    show "setsucM n n ε m"
      unfolding m[rule_format] 
    proof (rule exI[of _ "setsucM y y'"])  
      show "setsucM y y' ε s ∧ cardinality (setsucM y y') (setsucM n n)"
        using card_setsuc[OF ‹¬ y' ε y› ‹cardinality y n›] ‹y ε 𝔓 x› ‹y' ε x›  
          step[rule_format, OF ‹P (Ξ(0:= y))›] unfolding powerset_def' subsetM_def s[rule_format] by simp
    qed 
  qed
  then show False
    using fin ‹∅ ε m› by blast
qed

lemma cardinality_ex: "∃! n. natM n ∧ x ≈⇩M n"
proof (rule ex_ex1I)
  show "∃ n. natM n ∧ x ≈⇩M n"
  proof (rule setind_SP[rule_format])
    show "SetProperty (λa. ∃n. natM n ∧ a ≈⇩M n)"
      unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+
    show "∃n. natM n ∧ ∅ ≈⇩M n"
      using card_emp cardinality_def by blast
    show "∃n. natM n ∧ setsucM x y ≈⇩M n" if "∃n. natM n ∧ x ≈⇩M n" for x y
      using that card_setsuc setsuc_triv unfolding cardinality_def  by metis 
  qed
  show "natM n ∧ x ≈⇩M n ⟹ natM y ∧ x ≈⇩M y ⟹ n = y" for n x y
    using nat_equiv_unique set_equivalent_sym set_equivalent_trans by blast
qed

sublocale L_setext_empty_setsuc_setind
  by unfold_locales

end

subsection ‹Dedekind finite›

locale L_setext_empty_power_union_repl_dedekind = L_setext + L_empty + L_power + L_union + L_repl + L_dedekind

begin

sublocale L_setext_empty_power_union_repl
  by unfold_locales  

sublocale L_fin
proof (unfold_locales, rule notI)
  assume "∃x. ∅ ε x ∧ (∀y. y ε x ⟶ setsucM y y ε x)"
  then obtain x' where x': "∅ ε x'" "∀y. y ε x' ⟶ setsucM y y ε x'"
    by blast
  define x where "x = separationM x' natM"
  from separ_def_SP[OF SP_nat]
  have x: "u ε x ⟷ u ε x' ∧ natM u" for u
    unfolding x_def. 
  have x_setsuc: "u ε x ⟶ setsucM u u ε x" for u
    using x'(2) nat_suc_nat[of u] unfolding x by blast 
  have "SetFormulaPredicate (λ Ξ. ∃ v. Ξ 0 = ⟨v,setsucM v v⟩)"
    unfolding logsimps set_defs by (rule SFP_rules)+ 
  from sep[OF this, rule_format, of "x ×⇩M x", simplified]
  obtain f where "u ε f ⟷ (u ε x ×⇩M x  ∧ (∃v. u = ⟨v,setsucM v v⟩))" for u
    by blast
  hence f: "u ε f ⟷ (∃ v. v ε x ∧ u = ⟨v,setsucM v v⟩)" for u
    using car_prod_def' x_setsuc by auto
  have "one_oneM f"
   by (rule one_oneI, unfold f x, blast, unfold ordered_pair_unique)  
    (use ord_pred_fun[OF natM_D natM_D] in blast)+ 
  have "domM f = x"
    unfolding setext[of _ x] f dom_def' by force 
  have "x ≈⇩M rngM f"
    unfolding set_equivalent_def by (rule exI[of _ f]) (use ‹one_oneM f› ‹domM f = x› in blast)
  have "rngM f ⊂⇩M x"
  proof (rule proper_subsetI)
    show "rngM f ⊆⇩M x"
      unfolding subsetM_def rng_def' f ordered_pair_unique using x_setsuc by blast
    show "rngM f ≠ x"
      unfolding setext[of _ x] rng_def' not_all
    proof (rule exI[of _ ∅])
      have t: "∅ ε x = True"
        by (simp add: x x'(1))
      have f: "(∃ v. ⟨v,∅⟩ ε f) = False"
        unfolding f ordered_pair_unique setext[of ∅] binunion_def' singleton_def' by force
      show "(∃v. ⟨v,∅⟩ ε f) ≠ (∅ ε x)"
        unfolding t f by blast
    qed
  qed
  from dedekind[unfolded dedekind_fin_def, rule_format, OF this] 
  show False
    using ‹x ≈⇩M rngM f› by blast
qed

end
  
subsection ‹Tarski finite›

locale L_setext_empty_power_sep_setsuc_tarski = L_setext + L_empty + L_power + L_sep + L_setsuc + L_tarski

begin

sublocale L_setext_empty_power
  by unfold_locales

sublocale L_setext_empty_setsuc 
  by unfold_locales

text ‹In a suitable context, the axiom of Tarski finitness yields the set induction schema.›

sublocale L_setind
proof (unfold_locales, rule impI, rule impI, rule allI)
  fix P Ξ x
  assume set_p: "SetFormulaPredicate P" and
    step: "(∀x y. P (Ξ(0 := x)) ⟶ P (Ξ(0 := setsucM x y)))" and
    "P (Ξ(0 := ∅))"
  show "P (Ξ(0 := x))"
  proof (rule ccontr)
    assume "¬ P (Ξ(0 := x))"
    obtain z where z_def: "⋀ u. (u ε z) ⟷ (u ε (𝔓 x) ∧ P (Ξ(0 := u)))" 
      using sep[OF set_p, rule_format, of "𝔓 x"] by blast   
    have "z ≠ ∅" 
      using z_def ‹P (Ξ(0 := ∅))› empty_is_empty empty_is_subset subsetM_def powerset_def' by blast
    have "z ⊆⇩M 𝔓 x"
      by (simp add: subsetM_def z_def)
    have neg: "∃ v. v ε z ∧ u ⊂⇩M v" if "u ε z" for u
    proof-
      obtain y where "¬ y ε u" and "y ε x"
        using  ‹¬ P (Ξ(0 := x))› ‹u ε z›[unfolded z_def] setext[of u x] unfolding subsetM_def powerset_def' by blast
      have "(setsucM u y) ε z"
        using ‹y ε x› step[rule_format,of u y] powerset_def' subsetM_def setsuc_def' that z_def by auto
      moreover have "u ⊂⇩M (setsucM u y)" 
        unfolding proper_subsetM_def setext[of u] setsuc_def' 
        using ‹¬ y ε u›  by blast
      ultimately show ?thesis
        by blast
    qed
    show False
      using tarski[rule_format, of x, unfolded tarski_fin_def, rule_format, of z] ‹z ⊆⇩M 𝔓 x› neg ‹z ≠ ∅› 
      unfolding subsetM_def powerset_def' z_def
      using ‹P (Ξ(0 := ∅))› empty_is_empty by blast   
  qed   
qed

sublocale L_setext_empty_setsuc_setind
  by unfold_locales 

text ‹It follows in particular that union and replacement are provable in this context.›

sublocale L_repl
  by unfold_locales

sublocale L_union
  by unfold_locales

end

subsection ‹Set induction and regularity schema›

text ‹An apparently minor variation of the set induction schema, 
which nevertheless yields also the schema of regularity (i.e., epsilon induction). 
It is used in Pudlák and Sochor \<^cite>‹PudlakSochor1984›.›

locale L_setindregsch = set_signature +
  assumes setindregsch: "SetFormulaPredicate P ⟹ 
    P(Ξ(0:= ∅)) ⟶ (∀ x y. P(Ξ(0:= x)) ∧ P(Ξ(0:= y)) ⟶ P(Ξ(0:= setsucM x y))) ⟶ (∀ x. P(Ξ(0:= x)))"

begin

lemma setindregsch_sp: assumes "SetProperty P" "P ∅" "∀ x y. P x ∧ P y ⟶ P (setsucM x y)"
  shows "∀ x. P x"
  using setindregsch[OF ‹SetProperty P›[unfolded SetProperty_def]] assms by force

lemma setindregsch_var: assumes "SetFormulaPredicate P" "P(Ξ(n:= ∅))" "∀ x y. P(Ξ(n:= x)) ∧ P(Ξ(n:= y)) 
  ⟶ P(Ξ(n:= setsucM x y))"
  shows "∀ x. P(Ξ(n:= x))"
proof
  fix x
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where m: "P Ξ = P Ξ'" if "∀i<m. Ξ i = Ξ' i" for Ξ Ξ'
    by blast
  let ?m = "Suc (n + m)"  
  let ?f = "id(0 := ?m, n:= 0)"
  let ?Q = "λ X. (P (λ b. X (?f  b)))"
  let ?X = "Ξ(?m:= Ξ 0)" 
  have sfpq:  "SetFormulaPredicate ?Q"
    using transform_variables[OF ‹SetFormulaPredicate P›] by simp
  have small: "∀ i < m. (Ξ(n := u)) i = (?X (0 := u)) (?f i)" for u
    by auto
  have equiv: "(P (Ξ(n := u))) ⟷ (?Q (?X (0 := u)))" for u
    by (rule m[of "Ξ(n := u)" "λ b. (?X (0 := u))(?f b)"]) fact
  show "P (Ξ(n := x))"
    unfolding equiv
    by (rule setindregsch[rule_format, OF sfpq, of "Ξ(Suc (n + m) := Ξ 0)"], unfold equiv[symmetric])
     (use assms in blast)+    
qed  

― ‹Induction schema for set formulas is a theorem.›

sublocale L_setind
  by unfold_locales (use setindregsch in blast)

end

locale L_setext_empty_setsuc_setindregsch = L_setext + L_empty + L_setsuc + L_setindregsch 

begin
 
sublocale L_setext_empty_setsuc_setind
  by unfold_locales

lemma epsind_from_setindregsch_sp: assumes spp: "SetProperty P" and indp: "(∀ x. (∀y. (y ε x ⟶ P y))  ⟶  P x)"
  shows "∀ x. P x"
proof-
  let ?Q = "λ x. ∀ u. (u ε x ⟶ P u)"
  have "SetFormulaPredicate (λΞ. P (Ξ m))" for m
     using spp[unfolded SetProperty_def] by (rule transform_variables) 
   have "SetProperty ?Q" 
     unfolding SetProperty_def set_defs logsimps by (rule SFP_rules)+ fact
   have "∀ v w. ?Q v ∧ ?Q w ⟶ ?Q  (setsucM v w)"  ―‹use ‹?Q› w and ‹indp› to show P w›
     using indp unfolding setsuc_def' by presburger
   from setindregsch_sp[OF ‹SetProperty ?Q› _ this]
   have " ∀ x. ?Q x " 
     by force
   then show " ∀ x. P x "
     using indp by blast 
 qed

― ‹Epsilon induction (and hence, regularity schema) is a theorem.›

lemma epsind_from_setindregsch: assumes sfp: "SetFormulaPredicate P" and indp: "(∀ x. (∀y. (y ε x ⟶ P(Ξ(0:=y))))  ⟶  P(Ξ(0:=x)))"
  shows "∀ x. P(Ξ(0:=x))"
proof
  fix x
  from bounded_free[OF ‹SetFormulaPredicate P›]
  obtain m where "∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ P Ξ = P Ξ'"
    by blast
  then have small: "P(Ξ(Suc m:=a, 0:= u)) = P(Ξ(0:= u))" for Ξ a u
    by simp
  let ?Q = "λ Ξ. ∀ u. (u ε (Ξ (Suc m)) ⟶ P(Ξ(0:=u)))"
  have sfpQ: "SetFormulaPredicate ?Q"
    by (rule SFP_all[of "λ Ξ. (Ξ 0) ε (Ξ (m+1)) ⟶ P Ξ" 0, simplified])
    (unfold logsimps set_defs, (rule | fact)+)
  thm setindregsch_var[OF ‹SetFormulaPredicate ?Q›, of _ "Suc m", unfolded small, simplified]
  have "?Q (Ξ (0:=v))  ∧ ?Q (Ξ (0:=w)) ⟶ ?Q (Ξ (0:=(v∪⇩M{w}⇩M)))" for v w Ξ 
   ―‹use ?Q w and indp to show P w›
    unfolding setsuc_def' using indp[rule_format] by simp
  from setindregsch_var[OF ‹SetFormulaPredicate ?Q›, of _ "Suc m", unfolded small, simplified]
  have " ?Q (Ξ(Suc m:= x))"
    unfolding small fun_upd_same using indp by metis
  then show "P (Ξ(0 := x))"
     using indp unfolding small fun_upd_same by blast 
 qed

sublocale L_epsind
  by (unfold_locales) (use epsind_from_setindregsch in blast)

sublocale L_setext_empty_union_repl_pair_regsch
  by unfold_locales

end

subsection ‹Summary of dependencies›

theorem epsind_regsch_iff:
  "L_epsind mem ⟷ L_regsch mem"
proof
  assume "L_epsind mem"
  from L_epsind.epsind_regsch[OF this]
  show "L_regsch mem"
    by unfold_locales blast
next
  assume "L_regsch mem"
  from L_regsch.regsch_epsind[OF this]
  show "L_epsind mem"
    by unfold_locales
qed

text ‹We give additional names to some important collections of axioms.
Here is a "canonical" axiomatization of the theory of hereditarily finite sets.›

locale ZFfin =  L_setext + L_empty + L_power + L_union +  L_repl + L_fin + L_epsind

begin
sublocale L_setext_empty_power_union_repl_reg_fin
  by unfold_locales
sublocale L_regsch
  by unfold_locales
sublocale L_reg
  by unfold_locales
sublocale L_setsuc
  by unfold_locales
sublocale L_sep
  by unfold_locales
sublocale L_setind
  by unfold_locales
sublocale L_dedekind
  by unfold_locales
sublocale L_tarski
  by unfold_locales
end

text ‹This is the list of axioms for sets from Vopěnka's book \<^cite>‹Vopenka1979›.›

locale ASTset = L_setext + L_empty + L_setsuc + L_setind + L_regsch

begin

text ‹Vopěnka \<^cite>‹Vopenka1979› shows that all axioms of @{term ZFfin} are provable in @{term ASTset}›

sublocale ZFfin
proof-
  interpret L_setext_empty_setsuc_setind
    by unfold_locales
  interpret L_epsind
    by (simp add: L_regsch_axioms epsind_regsch_iff) 
  show "ZFfin (ε)"
    by unfold_locales
qed

text ‹The variation of set induction which combines it with regularity schema is provable from set induction schema and epsilon induction 
(i.e., regularity schema). Taken for granted in  \<^cite>‹PudlakSochor1984›.›

sublocale L_setindregsch
proof (unfold_locales, rule impI, rule impI, rule allI)
  fix P :: "(nat ⇒ 'a) ⇒ bool" and Ξ and x
  let ?P = "λ y. P (Ξ(0 := y))"
  assume sfp: "SetFormulaPredicate P"
  show "?P x" if "?P ∅" and  step: "(∀x y. ?P x ∧ ?P y ⟶ ?P (setsucM x y))"
  proof-
    ―‹In order to complete the proof by ‹ε›-induction, it is enough to show that all sets inherit the property ‹?P›. 
       Call this inheritance property ‹Q››
    let ?Q = "λ w. (∀ u. u ε w ⟶ ?P u) ⟶ ?P w"
      ―‹We show that all sets satisfy ‹Q› by set-induction.›

― ‹But first some work has to be done. Note that ‹?Q› depends on free variables present in ‹P›.
  We therefore have to reformulate ‹?Q› to reflect this. 
  We formulate ‹Q› as a property of a fresh variable ‹Ξ (m+1)››
    from bounded_free[OF sfp]
    obtain m where m: "∀Ξ Ξ'. (∀i<m. Ξ i = Ξ' i) ⟶ P Ξ = P Ξ'" 
      by blast
    have fresh: " P (Ξ(m + k := a, 0 := b)) =  P (Ξ(0 := b))" for a b k Ξ
      ― ‹Indeed, ‹P› does not depend on any ‹Ξ (m+k)›› 
      using m[rule_format, of "Ξ(m + k := a, 0 := b)" "Ξ(0 := b)"] by simp  

    let ?Q' = "λ Ξ. (∀ u. u ε Ξ (m+1) ⟶ P (Ξ(0 := u))) ⟶ P (Ξ(0 := Ξ (m+1)))"
      ― ‹‹?Q' Ξ› now says: ‹x⇩m⇩+⇩1› inherits ‹P› from its elements›
    have "SetFormulaPredicate ?Q'"
      ― ‹The technical part: showing that ‹?Q'› is set formula predicate›
    proof-
      have "SetFormulaPredicate (λΞ. ∀u. u ε Ξ (Suc m) ⟶ P (Ξ(0 := u)))"
        by (rule SFP_all[of "λΞ. Ξ (m+2) ε Ξ (Suc m) ⟶ P (Ξ(0 := Ξ(m+2)))" "m+2", 
              simplified fun_upd_same fun_upd_other, unfolded fresh])
          (unfold logsimps, rule+, fact) 
      show "SetFormulaPredicate ?Q'"
        unfolding logsimps by (rule SFP_rules)+ 
        (simp, fact, simp add: sfp update_variable)  
    qed
      ―‹This yields the desired form of the induction in terms of ‹?Q››
    have Q_ind_rule: "?Q ∅ ⟹ (∀ x y. ?Q x ⟶ ?Q (setsucM x y)) ⟹ ∀ x. ?Q x"
      using 
         setind_var[rule_format, OF ‹SetFormulaPredicate ?Q'›, of Ξ "m+1"]
      unfolding fresh fun_upd_same by (rule, blast+) 

―‹Back to the main proof.›
    have "∀ w. ?Q w"
    proof (rule Q_ind_rule)
      show "?Q ∅"
        using ‹?P ∅› by blast
          ― ‹the empty set inherits ‹P›, since it satisfies ‹P››
      show "∀ x y. ?Q x ⟶ ?Q (setsucM x y)"
      proof (rule allI, rule allI, rule impI, rule impI)
        fix x y
        assume ‹?Q x› and "∀u. u ε setsucM x y ⟶ ?P u" 
        hence "?P x" "?P y"
          using ‹?Q x› unfolding setsuc_def' by blast+
        thus "?P (setsucM x y)"
          using step by blast
      qed
    qed
    thus "?P x"
      using epsind[OF ‹SetFormulaPredicate P›] unfolding fun_upd_same fresh by metis
  qed
qed

end

text ‹‹ZFfin› and ‹ASTset› are two different axiomatizations of the same theory.›

sublocale ASTset ⊆ ZFfin
  by unfold_locales
sublocale ZFfin ⊆ ASTset
  by (simp add: ASTset_def L_empty_axioms L_regsch_axioms L_setext_axioms L_setind_axioms L_setsuc_axioms)
  
text ‹In the AST, set induction and epsilon induction (i.e., regularity schema) can be replaced by the variant ‹setindregsch››

theorem setindregsch_ast: "L_setext_empty_setsuc_setindregsch mem ⟷ ASTset mem"
proof
  assume "L_setext_empty_setsuc_setindregsch mem"
  then interpret  L_setext_empty_setsuc_setindregsch "mem".
  show "ASTset mem"
    by unfold_locales
next
  assume "ASTset mem"
  then interpret  ASTset "mem".
  show "L_setext_empty_setsuc_setindregsch mem"
    by unfold_locales
qed  

theorem zffin_ast: "ZFfin mem ⟷ ASTset mem"
proof
  assume "ZFfin mem"
  then interpret  ZFfin "mem".
  show "ASTset mem"
    by unfold_locales
next
  assume "ASTset mem"
  then interpret  ASTset "mem".
  show "ZFfin mem"
    by unfold_locales
qed  

text ‹Ambivalence of the separation schema and the replacement schema.›

theorem repl_implies_sep:
  shows "L_setext_empty_repl mem ⟹ L_sep mem"
proof-
  assume "L_setext_empty_repl mem"
  then interpret L_setext_empty_repl "mem".
  show "L_sep mem"
    by unfold_locales
qed

text ‹Under certain finiteness assumptions, separation entails replacement. See \<^cite>‹Behounek1998› for details.›

theorem sep_implies_repl:
  shows "L_setext_empty_power_sep_setsuc_tarski mem ⟹ L_repl mem"
proof-
  assume "L_setext_empty_power_sep_setsuc_tarski mem"
  then interpret L_setext_empty_power_sep_setsuc_tarski "mem".
  show "L_repl mem"
    by unfold_locales
qed

text ‹Entailment between different finiteness principles, in their natural contexts.›

text ‹The following is included in Vopěnka \<^cite>‹Vopenka1979› by exploring the consequences of induction for set formulas.›

theorem (in L_setext_empty_setsuc) 
  shows setind_implies_tarski: "L_setind (ε) ⟹ L_tarski (ε)" and
        setind_implies_fin_by_setsuc: "L_setind (ε) ⟹ L_fin (ε)" and 
      setind_implies_dedekind_by_setsuc: "L_setind (ε) ⟹ L_dedekind (ε)"  
proof-
  assume "L_setind (ε)"
  then interpret L_setind
    by blast
  interpret L_setext_empty_setsuc_setind
    by unfold_locales 
  show "L_tarski (ε)" "L_fin (ε)" "L_dedekind (ε)"
    by unfold_locales
qed    

theorem (in L_setext_empty_power_union_repl)
   dedekind_implies_fin: "L_dedekind (ε) ⟹ L_fin (ε)"
proof-
  assume "L_dedekind (ε)"
  then interpret L_dedekind.
  interpret L_setext_empty_power_union_repl_dedekind
    by unfold_locales
  show "L_fin (ε)"
    by (simp add: L_fin_axioms)
qed

text ‹Equivalence of finiteness principles, in sufficiently strong common context.›

theorem (in L_setext_empty_power_union_repl_reg)
        fin_implies_tarski: "L_fin (ε) ⟹ L_tarski (ε)" and
        tarski_implies_fin: "L_tarski (ε) ⟹ L_fin (ε)" and
        fin_implies_setind: "L_fin (ε) ⟹ L_setind (ε)" and
        setind_implies_fin: "L_setind (ε) ⟹ L_fin (ε)" and
        fin_implies_dedekind: "L_fin (ε) ⟹ L_dedekind (ε)"
proof-
  assume "L_fin (ε)"
  then interpret L_fin "(ε)". 
  interpret L_setext_empty_power_union_repl_reg_fin "(ε)"
     by unfold_locales 
  interpret L_setext_empty_setsuc_setind "(ε)"
     by unfold_locales 
  show "L_tarski (ε)" 
    by unfold_locales 
  show "L_dedekind (ε)" 
    by unfold_locales 
  show "L_setind (ε)" 
    by unfold_locales 
next
  assume "L_tarski (ε)"
  then interpret L_tarski "(ε)". 
  interpret L_setext_empty_power_sep_setsuc_tarski
     by unfold_locales 
  show "L_fin (ε)" 
    by unfold_locales 
next
  assume "L_setind (ε)" 
  then interpret L_setind "(ε)"
    by blast
  interpret L_setsuc "(ε)"
    by unfold_locales 
  interpret L_setext_empty_setsuc "(ε)"
    by unfold_locales
  from setind_implies_tarski[OF ‹L_setind (ε)›]  
  interpret L_tarski "(ε)".
  interpret L_setext_empty_power_sep_setsuc_tarski "(ε)"
     by unfold_locales 
  show "L_fin (ε)"
    by unfold_locales 
qed

text ‹The validity of the regularity schema/epsilon induction is closely related to the existence of a transitive superset
See also Proposition 5.4, Kaye and Wong \<^cite>‹KayeWong2007›.
There, the equivalence of ‹L_epsind› and  ‹L_ts› is shown in the context of EST + regularity. 
Instead, we follow  Sochor  \<^cite>‹Sochor1979› and \<^cite>‹Sochor1982› 
in improving the claim by weakening both implications.  
›

theorem  (in L_setext_sep_reg) ts_implies_epsind: 
  "L_ts (ε) ⟹ L_epsind (ε)"
proof-
  assume "L_ts (ε)"
  then interpret L_ts "(ε)".
  interpret L_setext_sep_reg_ts
    by unfold_locales
  interpret L_regsch
    by unfold_locales
  show "L_epsind (ε)"
    using L_epsind_def regsch_epsind by blast
qed

theorem  (in L_setext_empty_union_repl_pair) epsind_implies_ts: 
  "L_epsind (ε) ⟹ L_ts (ε)"
proof-
  assume "L_epsind (ε)"
  then interpret L_epsind "(ε)".
  interpret L_setext_empty_union_repl_pair_regsch
    by unfold_locales  
  show "L_ts (ε)"
    using L_ts_axioms.   
qed

text ‹Consequently, in a sufficiently strong context we can verify the equivalence of axioms  A81 (regularity) + A82 (transitive superset) and A8 (schema of regularity)
from Sochor \<^cite>‹Sochor1979›, p. 709.
›

theorem  (in L_setext_empty_union_repl_pair) ts_reg_iff_regsch: 
  "L_ts (ε) ∧ L_reg (ε) ⟷ L_regsch (ε)"
proof
  assume "L_regsch (ε)"
  then interpret L_regsch "(ε)".
  have "L_reg (ε)"
    by (simp add: L_reg_axioms) 
  have "L_ts (ε)"
    by (simp add: L_regsch_axioms epsind_regsch_iff epsind_implies_ts)
  then show "L_ts (ε) ∧ L_reg (ε)"
    using ‹L_reg (ε)› by blast   
next
  assume "L_ts (ε) ∧ L_reg (ε)"
  then interpret L_ts "(ε)" 
    by simp   
  interpret L_reg "(ε)"
    using ‹L_ts (ε) ∧ L_reg (ε)› by simp
  interpret "L_setext_empty_repl"
    by unfold_locales
  interpret L_sep "(ε)"
    using repl_implies_sep  by (simp add: L_sep_axioms) 
  interpret L_setext_sep_reg "(ε)"
    by unfold_locales
  show "L_regsch (ε)"
    using ts_implies_epsind L_ts_axioms unfolding epsind_regsch_iff.
qed

end