Theory Not_ts_model

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

section ‹Independence of transitive superset›
theory Not_ts_model
imports Permutation_models
begin 

text  ‹We explore the model defined by the permutation transposing ‹n› and ‹{n+1}⇩M› for each natural number ‹n›.
The membership in the model is not well-founded since there is an infinite decreasing chain ‹... 2 ε⇧f 1 ε⇧f 0›.

Despite that if the native memebership satisfies regularity and finiteness, the permuted model also satisfies regularity and finiteness.

Consequently, ‹0› (the empty set) has not transitive superset, since it sould be infinite if it existed. 
As a corollary, the permutation model does not satisfy schema of regularity (or, equivalently, epsilon induction) 
since it entails transitive superset axiom.

The construction is given in Rieger in \<^cite>‹Rieger1957› and also in \<^cite>‹ManciniZambella2001› who underscore that the model is recursive. 
The statement that regularity schema does not follow from regularity was also proved in \<^cite>‹VopenkaHajek1963›.
›

context L_setext_empty_power_union_repl_reg

begin

fun regperm :: "'a ⇒ 'a" where
   "regperm a = (if natM a then {setsucM a a}⇩M else 
                   if (∃ b. natM b ∧ a = {setsucM b b}⇩M) then THE b. a = {setsucM b b}⇩M else a)"

lemma two_natM: "natM (setsucM ({∅}⇩M)({∅}⇩M))"
  using nat_suc_nat[OF one_natM]. 

lemma suc_sing_not_nat: "¬ natM ({setsucM b b}⇩M)"
proof
  assume "natM ({setsucM b b}⇩M)"
  hence "ordM ({setsucM b b}⇩M)"
    unfolding natM_def using natM_D  by blast 
  from ordM_D1[OF this, of "setsucM b b"]  
  have "b = setsucM b b"
    unfolding singleton_def' subsetM_def by force
  moreover have "b ε setsucM b b"
    unfolding set_defs by blast
  ultimately show False         
    using mem_not_refl[of b] by simp
qed

lemma regperm_image_nat: assumes "natM a"
  shows "regperm a = {setsucM a a}⇩M"
  using assms by simp

lemma regperm_image_plus: assumes "natM b"
  shows "regperm ({setsucM b b}⇩M) = b"
proof-
  have  aux: "(THE c. ({setsucM b b}⇩M) = ({setsucM c c}⇩M)) = regperm ({setsucM b b}⇩M)"
    using ‹natM b› suc_sing_not_nat by fastforce
  have aux': "{setsucM b b}⇩M = {setsucM x x}⇩M ⟹ x = b" for x
    using suc_unique[of x b] unfolding setext singleton_def' by blast
  show ?thesis
    using  the_equality[of "λ c. {setsucM b b}⇩M = {setsucM c c}⇩M", OF refl aux']
    unfolding aux by blast    
qed 

lemma regperm_image_else: assumes "¬ natM a" "∄ b. natM b ∧ a = {setsucM b b}⇩M"
  shows "regperm a = a"
  using assms by force

lemma regperm_bij: "bij regperm"
proof (rule involuntory_imp_bij)
  fix a
  show "regperm (regperm a) = a"
    by  (cases "natM a", use regperm_image_nat regperm_image_plus in force)
    (cases "∃ b. natM b ∧ a = {setsucM b b}⇩M", use regperm_image_nat regperm_image_plus in metis, auto)
qed

lemma SR_regperm_eq: "SetRelation (λ x y. regperm x = y)"
proof-
  let ?Def = "λ x y. (natM x ∧ y = {setsucM x x}⇩M) ∨ (¬ natM x ∧ (∃ b. natM b ∧ x = {setsucM b b}⇩M ∧ y = b))
       ∨ (¬ natM x ∧ (∄b. natM b ∧ x = {setsucM b b}⇩M) ∧ y = x)"
  have iff: "?Def x y ⟷ regperm x = y" for x y
  proof-
    consider "natM x" | "¬ natM x ∧ (∃ b. natM b ∧ x = {setsucM b b}⇩M)" | 
              "¬ natM x ∧ (∄ b. natM b ∧ x = {setsucM b b}⇩M)" by blast
    then show ?thesis
      by (cases, force) (use regperm_image_plus in blast, use regperm_image_else in auto)
  qed
  have "SetRelation ?Def"
    unfolding SetRelation_def logsimps set_defs by (rule SFP_rules)+
  thus ?thesis 
    unfolding iff.
qed

lemma SR_regperm_mem: "SetRelation (λ x y. x ε regperm y)"
proof-
  have "SetRelation (λ x y. ∃ z. x ε z ∧ regperm y = z)"
    unfolding SetRelation_def logsimps 
    by (rule SFP_rules)+
    (use transform_variables[OF SR_regperm_eq[unfolded SetRelation_def], of "id(0:=1, 1:=_)"] in simp)
  thus ?thesis
    by metis
qed

end

context  L_setext_empty_power_union_repl_reg_fin

begin  

interpretation perm: permutation_model "(ε)" regperm
  by unfold_locales (use regperm_bij SR_regperm_mem in blast)+  

― ‹membership in the model›
abbreviation fmem (infix "ε⇧f" 51)  where 
  "fmem x y ≡  perm.perm_mem x y"

interpretation fm: L_setext_empty_power_union_repl fmem
    using perm.perm_model. 

lemma regperm_mem_nat: assumes "natM a"
  shows "u ε⇧f a ⟷ u = (setsucM a a)"
  unfolding regperm_image_nat[OF assms] singleton_def'..

― ‹First meta-theorem : not used in the main meta-theorem below.›
lemma fmem_not_wf: "¬ (wfp (ε⇧f))"
proof-
  let ?B = "{x . natM x}"
  have "?B ≠ {}"
    using Collect_empty_eq one_natM by metis
  moreover have "z ∈ ?B ⟹ (setsucM z z) ε⇧f z"  for z
    unfolding mem_Collect_eq using regperm_image_nat unfolding setext singleton_def' by blast
  moreover have "z ∈ ?B ⟹ (setsucM z z) ∈ ?B"  for z
    unfolding mem_Collect_eq using nat_suc_nat.
  ultimately show ?thesis
    unfolding wfp_iff_ex_minimal by metis
qed

text ‹The main meta-theorem. The axiom of the transitive superset does not hold in the model 
since the transitive closure of ‹∅› would be an infinite set.›

theorem regperm_not_ts: "¬ L_ts (ε⇧f)" 
proof
  assume "L_ts (ε⇧f)"
  then interpret L_ts "(ε⇧f)".
      ― ‹take the transitive closure of ‹∅››
  interpret L_setext_sep_ts "(ε⇧f)"
    by unfold_locales
  obtain t where "fm.subsetM ∅ t" "fm.transM t" and least: "∀u. u ε⇧f t ⟷ (∀s. fm.transM s ∧  fm.subsetM ∅ s ⟶ u ε⇧f s)"
    using least_ts_is_transitive[of ∅]  least_ts_def'[of _ ∅] fm.subsetM_def by force  
  have trans_t: "z ε⇧f t" if  "y ε⇧f t" "z ε⇧f y" for y z
    using ‹fm.transM t› that unfolding fm.transM_def fm.subsetM_def by blast
      ― ‹‹t› contains an infinite ‹ε⇧f› chain of natural numbers›
  have suc_t: "setsucM u u  ε⇧f t" if "natM u" "u ε⇧f t" for u
    using trans_t[OF ‹u ε⇧f t›] using regperm_mem_nat[OF ‹natM u›] by blast
      ― ‹we show that ‹ε⇧f› coincides with ‹ε› in ‹t››
  have one_in_t: "{∅}⇩M ε⇧f t"
    using ‹fm.subsetM ∅ t›unfolding fm.subsetM_def using regperm_mem_nat[OF emp_natM]
      setsuc_empty_sing by fastforce
  have two_in_t: "setsucM ({∅}⇩M) ({∅}⇩M) ε⇧f t"
    using one_in_t suc_t[OF one_natM] by blast
  have tmem:  "u ε⇧f t ⟷ u ε t" for u
  proof-
    have "¬ natM t"
    proof
      assume "natM t"
      have iff: "u ε⇧f t ⟷ u = setsucM t t" for u
        unfolding regperm_image_nat[OF ‹natM t›] singleton_def'..
      have "¬ {∅}⇩M ε setsucM ({∅}⇩M) ({∅}⇩M)"
        unfolding two_in_t[unfolded iff, folded one_in_t[unfolded iff]]
        by (rule mem_not_refl)
      then show False 
        unfolding setsuc_def' by blast
    qed
    have "∄ b.  natM b ∧ t = {setsucM b b}⇩M"
    proof
      assume "∃b. natM b ∧ t = {setsucM b b}⇩M"
      then obtain b where "natM b" "t = {setsucM b b}⇩M"
        by blast
      hence iff: "u ε⇧f t ⟷ u ε b" for u
        using regperm_image_plus by auto
      have "b ≠ ∅"
        using iff one_in_t by auto
      hence  "∅ ε b"
        using ‹natM b› by (simp add: empty_mem_ord natM_def) 
      have "setsucM y y ε b" if "y ε b" for y
        using suc_t[unfolded iff, OF _ that] nat_mem_nat[OF _ that] ‹natM b› by blast 
      then show False
        using ‹∅ ε b› fin by blast
    qed
    show ?thesis
      by (simp add: ‹∄b. natM b ∧ t = {setsucM b b}⇩M› ‹¬ natM t›)
  qed  
  ― ‹We get a contradiction with the finiteness axiom since the subset of ‹t› consisting of natural numbers is an inductive set.› 
  thm notE[OF fin[unfolded not_ex, rule_format]] 
  show False
  proof (rule notE[OF fin[unfolded not_ex, rule_format]], rule conjI)
    define tnatM where "tnatM = separationM t natM"
    have tnat:  "u ε tnatM ⟷ natM u ∧ u ε t" for u
    using separ_def_SP tnatM_def by auto
    show "∅ ε setsucM tnatM ∅"
      unfolding set_defs by simp 
    show "∀y. y ε setsucM tnatM ∅ ⟶ setsucM y y ε setsucM tnatM ∅"
    proof (rule allI, rule impI)
      fix y
      assume "y ε setsucM tnatM ∅"
      then consider "y = ∅" | "y ε tnatM"
        unfolding set_defs by blast 
      then show "setsucM y y ε setsucM tnatM ∅"
      proof (cases) 
        assume "y = ∅"
        then show ?thesis 
          using one_in_t[unfolded tmem] setsuc_empty_sing tnat unfolding binunion_def' by simp 
      next
        assume "y ε tnatM"
        then show ?thesis 
          unfolding tnat  binunion_def' setsuc_def'  using   suc_t[unfolded tmem, of y] nat_suc_nat[of y] by blast
      qed
    qed
  qed
qed

― ‹It follows that the scheme of regularity does not hold in the model, since it entails transitive supersets.›
theorem regperm_not_regsch: "¬ L_regsch (ε⇧f)"
    using regperm_not_ts epsind_regsch_iff fm.epsind_implies_ts by blast 

lemma regperm_reg:
  shows "L_setext_empty_power_union_repl_reg (ε⇧f)"
proof (unfold_locales, rule allI, rule impI) 
  fix a
  assume "∃y. y ε⇧f a"
  show "∃y. y ε⇧f a ∧ (∀v. ¬ (v ε⇧f y ∧ v ε⇧f a))"
  proof-
    consider "∃ n. natM n ∧ n ε⇧f a" | "(∄ n. natM n ∧ n ε⇧f a) ∧ (∃ m. natM m ∧ ({setsucM m m}⇩M) ε⇧f a)" | 
              "(∄ n. natM n ∧ n ε⇧f a) ∧ (∄ m. natM m ∧ ({setsucM m m}⇩M) ε⇧f a)" by blast
    then show ?thesis
    proof (cases)
      assume "∃ n. natM n ∧ n ε⇧f a"
      then obtain k where "natM k" "k ε⇧f a" and "⋀ k'. natM k' ⟹ k' ε⇧f a ⟹ ¬ k ⊂⇩M k'"
        using max_mem[OF _ _ SP_nat, of _ "regperm a"] by fast
      then have max_k: "⋀ k'. natM k' ⟹ k' ε⇧f a ⟹ k' ≠ k ⟹ k' ε k"
        unfolding proper_subset_def' using natM_D ordM_D1 ordM_total natM_def by metis 
      show "∃y. y ε⇧f a ∧ (∀v. ¬ (v ε⇧f y ∧ v ε⇧f a))"
      proof (rule exI[of _ k], rule conjI, fact)
        show "∀v. ¬ (v ε⇧f k ∧ v ε⇧f a)"
        proof (rule allI, rule notI)
          fix v 
          assume "v ε⇧f k ∧ v ε⇧f a"
          hence "v ε⇧f a" "v ε⇧f k" "v = setsucM k k"
            unfolding regperm_image_nat[OF ‹natM k›] singleton_def' by blast+
          show False
            using max_k[of v, OF _ ‹v ε⇧f a›, unfolded ‹v = setsucM k k›]
              ‹natM k› mem_antisym nat_suc_nat setsuc_def' natM_def by blast 
        qed
      qed
    next
      assume "(∄n. natM n ∧ n ε⇧f a) ∧ (∃m. natM m ∧ {setsucM m m}⇩M ε⇧f a)"
      then obtain m where "natM m" "{setsucM m m}⇩M ε⇧f a" "∄n. natM n ∧ n ε⇧f a"
        by blast
      show "∃y. y ε⇧f a ∧ (∀v. ¬ (v ε⇧f y ∧ v ε⇧f a))"
      proof (rule exI[of _ "{setsucM m m}⇩M"], rule conjI, fact)
        show "∀v. ¬ (v ε⇧f {setsucM m m}⇩M ∧ v ε⇧f a)"
          unfolding  regperm_image_plus[OF ‹natM m›]
          using ‹∄n. natM n ∧ n ε⇧f a› ‹natM m› nat_mem_nat by blast
      qed
    next
      assume case3: "(∄n. natM n ∧ n ε⇧f a) ∧ (∄m. natM m ∧ {setsucM m m}⇩M ε⇧f a)"
      hence "¬ natM a"
        using nat_suc_nat[of a]
          singleton_def' by force
      have "∄ b. natM b ∧ a = {setsucM b b}⇩M"
        using case3 ‹∃y. y ε⇧f a› nat_mem_nat regperm_image_plus by metis 
      hence a_mem: "u ε⇧f a ⟷ u ε a" for u
        using ‹¬ natM a› by auto
      have "a ≠ ∅"
        using ‹¬ natM a› emp_natM by blast 
      then obtain b where "b ε a" "∀ v. ¬ (v ε b ∧ v ε a)"
        using reg by (metis min_subset_ex) 
      have "¬ natM b" "∄ m. natM m ∧ b = {setsucM m m}⇩M"
        using ‹b ε a› case3 unfolding a_mem by blast+
      hence b_mem: "u ε⇧f b ⟷ u ε b" for u
        by auto
      show "∃y. y ε⇧f a ∧ (∀v. ¬ (v ε⇧f y ∧ v ε⇧f a))"
        by (rule exI[of _ b], rule conjI, unfold a_mem b_mem) fact+ 
    qed
  qed
qed

lemma perm_empty: "fm.emptysetM = {{∅}⇩M}⇩M"
proof (rule sym, unfold fm.emptyset_def') 
  have "regperm ({{∅}⇩M}⇩M) = ∅"
    using regperm_image_plus[OF emp_natM] unfolding setsuc_empty_sing.
  show "∀u. ¬ u ε (regperm ({{∅}⇩M}⇩M))"
    unfolding ‹regperm ({{∅}⇩M}⇩M) = ∅› by (fact empty_is_empty) 
qed

lemma perm_one: "fm.binunionM fm.emptysetM (fm.singletonM fm.emptysetM) = {{{∅}⇩M}⇩M}⇩M"
proof-
  have L: "z ε⇧f fm.binunionM fm.emptysetM (fm.singletonM fm.emptysetM) ⟷ z = fm.emptysetM" for z
    unfolding fm.setext fm.binunion_def' fm.singleton_def'
    using fm.nemp_setI fm.setsuc_def' by blast 
  have "z ε⇧f {{{∅}⇩M}⇩M}⇩M ⟷ z ε {{{∅}⇩M}⇩M}⇩M" for z
    using singleton_def' binunion_emp nat_mem_nat nat_suc_nat
        regperm_image_else[of "{{{∅}⇩M}⇩M}⇩M"] suc_sing_not_nat[of ∅] unfolding setsuc_empty_sing  by metis 
  hence R: "z ε⇧f {{{∅}⇩M}⇩M}⇩M ⟷ z = fm.emptysetM" for z
    unfolding perm_empty singleton_def'.   
  show ?thesis 
    unfolding fm.setext L R by blast
qed

lemma perm_else_setsuc_else: assumes "¬ natM u" "∄ b. natM b ∧ u = {setsucM b b}⇩M"
  shows "¬ natM (setsucM u u)" "∄ b. natM b ∧ setsucM u u = {setsucM b b}⇩M"
  using assms by (meson nat_mem_nat setsuc_def') (metis mem_not_refl singleton_def' setsuc_def')   

lemma perm_setsuc: assumes "¬ natM u" "∄ b. natM b ∧ u = {setsucM b b}⇩M"
  shows "fm.setsucM u u = setsucM u u"
  unfolding fm.setext unfolding fm.binunion_def' regperm_image_else[OF perm_else_setsuc_else[OF assms]] 
  regperm_image_else[OF assms] binunion_def' singleton_def' fm.singleton_def' setsuc_def'
  using ‹regperm u = u› fm.setsuc_def' by auto 

lemma perm_fin: "L_fin (ε⇧f)"
proof(unfold_locales, rule notI)
  assume "∃x. fm.emptysetM ε⇧f x ∧ (∀y. y ε⇧f x ⟶ fm.setsucM y y ε⇧f x)"
  then obtain x where xf: "fm.emptysetM ε⇧f x" "∀y. y ε⇧f x ⟶ fm.setsucM y y ε⇧f x"
    by blast   
  hence mem0: "{{∅}⇩M}⇩M ε⇧f x" 
    using perm_empty by force
  from xf(2)[rule_format, OF xf(1), unfolded perm_one] 
  have mem1: "{{{∅}⇩M}⇩M}⇩M ε⇧f x"
    using fm.binunion_emp fm.setsuc_empty_sing perm_one by force
  hence not1: "¬ natM x"
    using mem0 by (metis mem_neq_singleton regperm_mem_nat) 
  have not2: "∄b. natM b ∧ x = {setsucM b b}⇩M"
    using mem0 mem1
    using binunion_emp nat_mem_nat regperm_image_plus suc_sing_not_nat setsuc_empty_sing by metis
  from regperm_image_else[OF not1 not2]
  have x: "{{∅}⇩M}⇩M ε x" "∀y. y ε x ⟶ fm.setsucM y y ε x"
    using xf perm_empty by force+
  let ?P = "λ u. (¬ natM u ∧ (∄ b. natM b ∧ (u = {setsucM b b}⇩M)))"
  have sp: "SetProperty ?P"
    unfolding SetProperty_def 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 ∧ ¬ natM u ∧ (∄b. natM b ∧ u = {setsucM b b}⇩M))"
    by blast
  have "{{{∅}⇩M}⇩M}⇩M ε x'"
    using mem1  unfolding x'[rule_format] ‹regperm x = x›
    using binunion_emp nat_mem_nat nat_suc_nat singleton_def' suc_sing_not_nat setsuc_empty_sing by metis 
  hence "x' ≠ ∅"
    by force
  have x'_setsuc: "setsucM u u ε x'" if "u ε x'" for u
    unfolding x'[rule_format]
  proof(unfold conj_assoc[symmetric], rule conjI, rule conjI)  
    note u = ‹u ε x'›[unfolded x'[rule_format]]
    have red: "fm.setsucM u u = setsucM u u"
      by (rule perm_setsuc)
      (use  ‹u ε x'›[unfolded x'[rule_format]] in blast)+
    show "setsucM u u ε x"
      by (rule  x(2)[rule_format, of u, unfolded red]) (simp add: u)
    show "¬ natM (setsucM u u)" "∄b. natM b ∧ setsucM u u = {setsucM b b}⇩M"
      using u perm_else_setsuc_else by blast+
  qed
  with max_subset_ex[OF ‹x' ≠ ∅›]
  show False
    using suc_subset by blast
qed     

interpretation find: L_setind "(ε⇧f)"
  using L_setext_empty_power_union_repl_reg.fin_implies_setind regperm_reg perm_fin by blast

end

text‹Summary of results. 
We have shown that if a type admits a membership relation satisfying certain axioms of finite sets
(namely axioms of ZF where inf is replaced by fin), 
it does not follow that the membership on the type satisfies the existence of transitive supersets or the regularity schema.›

theorem not_reg_setind_implies_regsch_ts: 
  assumes "L_setext_empty_power_union_repl_reg_fin (m :: 'a ⇒ 'a ⇒ bool)"
  shows "¬ (∀ (mem :: 'a ⇒ 'a ⇒ bool). L_setext_empty_power_union_repl_reg mem ∧ L_setind mem ⟶ L_regsch mem ∨ L_ts mem)"
proof (rule notI)
  assume contr: "∀(mem :: 'a ⇒ 'a ⇒ bool). L_setext_empty_power_union_repl_reg mem ∧ L_setind mem ⟶ L_regsch mem ∨ L_ts mem"
  interpret L_setext_empty_power_union_repl_reg_fin m
    using assms.
  have L1: "L_setind fmem"
    using L_setext_empty_power_union_repl_reg.fin_implies_setind regperm_reg perm_fin by blast
  have L2: "L_setext_empty_power_union_repl_reg fmem"
    using L_setext_empty_power_union_repl_def L_setext_empty_power_union_repl_reg_def regperm_reg
    by blast
  have L3: "L_regsch fmem ∨ L_ts fmem"
    using L1 L2 contr by blast
  interpret i2: L_setext_empty_power_union_repl_reg fmem
    using L2.
  show False
    using L3 regperm_not_regsch regperm_not_ts by blast
qed 

end