Theory Not_regular_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 ‹Regularity›
theory Not_regular_model
imports Permutation_models
begin

text ‹
Axioms of extensionality, empty set, powerset, union, replacement and set induction 
are not sufficient to prove regularity, even in the presence of transitive superset axiom.

We prove this using permutation models.
It is enough to transpose ‹0› and ‹1› in order to obtain a model which violates regularity, cf. \<^cite>‹"Theorem 13" in BaratellaFerro1993›
›

context L_setext_empty_power_union_repl

begin

definition swap_zero_one :: "'a ⇒ 'a" where 
  "swap_zero_one x = (if x = ∅ then {∅}⇩M else (if x = {∅}⇩M then ∅ else x))"

lemma swap_zero_one_involution[simp]: "swap_zero_one (swap_zero_one x) = x"
  by (simp add: swap_zero_one_def)

lemma bij_swap_zero_one: "bij swap_zero_one"
  by (simp add: involuntory_imp_bij swap_zero_one_def)
  
lemma swap_zero_one_mem: "a ε swap_zero_one b ⟷ (b ≠ {∅}⇩M ∧ a ε b) ∨ (a = ∅ ∧ b = ∅)"
  unfolding swap_zero_one_def  by (simp add: singleton_def')

lemma swap_zero_one_perm_model: "permutation_model (ε) swap_zero_one"
proof
  show "SetRelation (λx y. x ε swap_zero_one y)"
    unfolding SetRelation_def swap_zero_one_mem logsimps singleton_eq set_defs by (rule SFP_rules)+  
qed (rule bij_swap_zero_one)

interpretation swap: permutation_model "(ε)" swap_zero_one
  using swap_zero_one_perm_model by blast

notation swap.perm_mem (infix ‹ε⇧s› 50)

interpretation swap: L_setext_empty_power_union_repl "(ε⇧s)"
  using swap.perm_model.

notation swap.emptysetM (‹∅⇧s›)

notation swap.setsucM (‹𝔰𝔲𝔠⇧s›)

― ‹‹{∅}› is the empty set in the permuted model›
lemma one_swap: "¬ (a ε⇧s {∅}⇩M)"
  unfolding  swap_zero_one_mem using singleton_def' by force 

lemma swap_empty: "∅⇧s = {∅}⇩M"
  using emptyset_def' swap.emptyset_def' swap_zero_one_mem by blast 

― ‹‹∅› is a singleton loop in the permuted model›
lemma zero_swap_mem_iff: "a ε⇧s ∅ ⟷ a = ∅"
  unfolding  swap_zero_one_mem  by auto

text ‹Since ‹∅ ε⇧s ∅›, the permuted model is not regular.›

theorem not_reg_swap_zero_one: "¬ (L_reg (ε⇧s))" 
  unfolding L_reg_def swap_zero_one_mem by force

text ‹In order to show that the model with memebership ‹ε⇧s› satisfies ‹L_setind› (‹L_ts› resp.) if the original model does, we first show how the modified successor behaves.›

lemma swap_mem_mem: "¬ (x = ∅ ∧ y = ∅) ⟹ x ε⇧s y ⟹ x ε y"
  using swap_zero_one_mem by auto

lemma swap_setsuc_1_y: assumes "y ≠ ∅" shows "𝔰𝔲𝔠⇧s ({∅}⇩M) y = {y}⇩M"
proof-
  have "swap_zero_one ({y}⇩M) = {y}⇩M"
    by (metis assms empty_is_empty singleton_def' swap_zero_one_def)
  have "u ε⇧s 𝔰𝔲𝔠⇧s ({∅}⇩M) y ⟷ u = y" for u
    using one_swap by auto
  hence "swap_zero_one (𝔰𝔲𝔠⇧s ({∅}⇩M) y) = {y}⇩M"
     unfolding setext singleton_def' by fast
  from arg_cong[OF this, of  swap_zero_one]
  show "𝔰𝔲𝔠⇧s ({∅}⇩M) y = {y}⇩M"
    unfolding ‹swap_zero_one ({y}⇩M) = {y}⇩M› by simp
qed     
       
lemma swap_setsuc_0_y: assumes "y ≠ ∅" shows "𝔰𝔲𝔠⇧s ∅ y = {∅,y}⇩M"
proof-
  have "{∅,y}⇩M ≠ ∅ ∧ {∅,y}⇩M ≠ {∅}⇩M"
    unfolding setext unfolding pair_def' singleton_def' using assms by auto   
  hence "swap_zero_one ({∅,y}⇩M) = {∅,y}⇩M"
    by (simp add: swap_zero_one_def)
  have "u ε⇧s 𝔰𝔲𝔠⇧s ∅ y ⟷ u = ∅ ∨ u = y" for u
    by (simp add: zero_swap_mem_iff)
  hence "swap_zero_one (𝔰𝔲𝔠⇧s ∅ y) = {∅,y}⇩M"
     unfolding setext pair_def' by fast
  from arg_cong[OF this, of  swap_zero_one]
  show "𝔰𝔲𝔠⇧s ∅ y = {∅,y}⇩M"
    unfolding ‹swap_zero_one ({∅,y}⇩M) = {∅,y}⇩M› by simp
qed     

lemma swap_setsuc_0_0: "𝔰𝔲𝔠⇧s ∅ ∅ = ∅"
  using zero_swap_mem_iff by auto 

lemma swap_setsuc_1_0: "𝔰𝔲𝔠⇧s ({∅}⇩M) ∅ = ∅"
proof-
  have "u ε⇧s 𝔰𝔲𝔠⇧s ({∅}⇩M) ∅ ⟷ u = ∅" for u
    using one_swap by auto
  hence "swap_zero_one (𝔰𝔲𝔠⇧s ({∅}⇩M) ∅) = {∅}⇩M"
    unfolding setext singleton_def' by blast
  from arg_cong[OF this, of  swap_zero_one]
  show "𝔰𝔲𝔠⇧s ({∅}⇩M) ∅ = ∅"
    by (simp add: emptyset_def' one_swap)
qed

lemma swap_setsuc_1_1: "𝔰𝔲𝔠⇧s ({∅}⇩M) ({∅}⇩M) = {{∅}⇩M}⇩M"
proof-
  have "{{∅}⇩M}⇩M ≠ ∅ ∧ {{∅}⇩M}⇩M ≠ {∅}⇩M"
    unfolding setext[of "{_}⇩M"] by (metis empty_is_empty singleton_def')  
  hence "swap_zero_one ({{∅}⇩M}⇩M) = {{∅}⇩M}⇩M"
    by (simp add: swap_zero_one_def)
  have "u ε⇧s 𝔰𝔲𝔠⇧s ({∅}⇩M) ({∅}⇩M) ⟷ u = {∅}⇩M" for u
    using one_swap by auto
  hence "swap_zero_one (𝔰𝔲𝔠⇧s ({∅}⇩M) ({∅}⇩M)) = {{∅}⇩M}⇩M"
    unfolding setext singleton_def' by blast
  from arg_cong[OF this, of swap_zero_one]
  show "𝔰𝔲𝔠⇧s ({∅}⇩M) ({∅}⇩M) = {{∅}⇩M}⇩M"
    unfolding ‹swap_zero_one ({{∅}⇩M}⇩M) = {{∅}⇩M}⇩M› by simp 
qed

lemma setsuc_setsuc': assumes "x ≠ ∅ ∧ x ≠ {∅}⇩M"
  shows "𝔰𝔲𝔠⇧s x y = 𝔰𝔲𝔠 x y"
proof-
  have "𝔰𝔲𝔠 x y ≠ {∅}⇩M" "𝔰𝔲𝔠 x y ≠ ∅"
    by (metis assms emptyset_def' setsuc_def' setsuc_triv singleton_def') (use emptyset_def' in auto)
  hence aux: "z ε⇧s 𝔰𝔲𝔠 x y ⟷ z ε 𝔰𝔲𝔠 x y" "z ε⇧s x ⟷ z ε x" for z
    by (simp_all add: assms swap_zero_one_mem)
  thus ?thesis
    unfolding swap.setext[of _ "𝔰𝔲𝔠 x y"] unfolding  aux swap.setsuc_def'[rule_format] setsuc_def'[rule_format] 
    by blast
qed

theorem setind_swap_setind: "L_setind (ε) ⟶ L_setind (ε⇧s)"
proof
  assume "L_setind (ε)"
  then interpret L_setind "(ε)".
  show "L_setind (ε⇧s)" 
  proof (unfold_locales, rule impI, rule impI, rule allI)
    fix P :: "(nat ⇒ 'a) ⇒ bool" and w and Ξ
    let ?P = "λ x. P(Ξ(0:= x))"
    assume "?P ∅⇧s" and step: "∀x y. ?P x ⟶ ?P (𝔰𝔲𝔠⇧s x y)" and SFP: "swap.SetFormulaPredicate P"
    hence "?P ({∅}⇩M)"
      using swap_empty by auto
    have aux: "(𝔰𝔲𝔠⇧s ({∅}⇩M) ∅) = ∅ ⟷ (𝔰𝔲𝔠⇧s ({∅}⇩M) ∅) ε⇧s (𝔰𝔲𝔠⇧s ({∅}⇩M) ∅)"
      using swap.setsuc_def' swap_zero_one_mem by blast
    have "𝔰𝔲𝔠⇧s ({∅}⇩M) ∅ = ∅"
      by (metis swap.setsuc_empty_sing swap.singleton_eq swap_empty zero_swap_mem_iff)
    hence "?P ∅"
      using step[rule_format, OF ‹?P ({∅}⇩M)›, of ∅]   by simp
    have "SetFormulaPredicate P"
      by (simp add: SFP swap.permSFP_SFP)
    show "?P w"
    proof (rule setind[OF ‹SetFormulaPredicate P›, of Ξ, rule_format])
      show "?P ∅"
        by fact
    next
      fix x y
      assume "?P x"  
      show "?P (𝔰𝔲𝔠 x y)"
      proof-
        consider "x = ∅ ∧ y = ∅" | "x = ∅ ∧ y ≠ ∅"  | "x = {∅}⇩M ∧ y = ∅"  |  "x = {∅}⇩M ∧ y ≠ ∅" | "x ≠ ∅ ∧ x ≠ {∅}⇩M"
          by blast
        then show ?thesis
        proof (cases) 
          assume "x = ∅ ∧ y = ∅"
          then show "?P (𝔰𝔲𝔠 x y)"
            using ‹P (Ξ(0 := {∅}⇩M))› setsuc_empty_sing by auto
        next
          assume "x = ∅ ∧ y ≠ ∅"
          then show "?P (𝔰𝔲𝔠 x y)"
            using step[rule_format, OF ‹?P ({∅}⇩M)›, of y] setsuc_empty_sing swap_setsuc_1_y by force
        next
          assume "x = {∅}⇩M ∧ y = ∅"
          then show "?P (𝔰𝔲𝔠 x y)"
            using ‹P (Ξ(0 := x))› singleton_def' by auto
        next
          assume "x = {∅}⇩M ∧ y ≠ ∅"
          hence "𝔰𝔲𝔠 x y = {∅,y}⇩M" 
            unfolding setext setsuc_def' singleton_def' pair_def' by force 
          hence "𝔰𝔲𝔠⇧s ∅ y = 𝔰𝔲𝔠 x y" 
            by (simp add: swap_setsuc_0_y ‹x = {∅}⇩M ∧ y ≠ ∅›) 
          then show "?P (𝔰𝔲𝔠 x y)"
            using step[rule_format, OF ‹?P ∅›, of y] by presburger
        next
          assume "x ≠ ∅ ∧ x ≠ {∅}⇩M"
          then show "?P (𝔰𝔲𝔠 x y)"
            using setsuc_setsuc' step[rule_format, OF ‹?P x›] by force
        qed
      qed
    qed
  qed
qed

lemma ts_swap_ts: "L_ts (ε) ⟶ L_ts (ε⇧s)"
proof
  assume "L_ts (ε)"
  then interpret L_setext_sep_binunion_ts "(ε)"
    by (simp add: L_binunion_axioms L_sep_axioms L_setext_axioms L_setext_sep_binunion_ts.intro) 
  have suc: "x ∪⇩M {∅}⇩M = 𝔰𝔲𝔠 x ∅" for x
    unfolding binunion_def' singleton_def' setsuc_def' setext by blast
  have empts: "least_tsM ({∅}⇩M) = {∅}⇩M"
    unfolding setext unfolding least_ts_def' singleton_def'
    by (metis subsetM_def transM_def set_two_mem powerset_def' set_one_mem)
  show "L_ts (ε⇧s)"
  proof (unfold_locales, rule allI, unfold set_signature.transM_def set_signature.subsetM_def)
    fix x :: 'a
    consider "x = ∅" | "x = {∅}⇩M" | "x ≠ ∅ ∧ x ≠ {∅}⇩M"
      by blast
    then show "∃z. (∀y. y ε⇧s z ⟶ (∀za. za ε⇧s y ⟶ za ε⇧s z)) ∧
             (∀za. za ε⇧s x ⟶ za ε⇧s z)"
    proof (cases)
      assume "x = ∅"
      show ?thesis
        by (rule exI[of _ ∅], simp add: ‹x = ∅› swap_zero_one_mem)
    next
      assume "x = {∅}⇩M"
      show ?thesis
        by (rule exI[of _ "{∅}⇩M"], simp add: ‹x = {∅}⇩M› swap_zero_one_mem)  
    next
      assume "x ≠ ∅ ∧ x ≠ {∅}⇩M"
      let ?t = "least_tsM (setsucM x ∅)" 
      have t: "?t = (least_tsM x) ∪⇩M {∅}⇩M"
        by (metis empts leastTS_union suc) 
      have "?t ≠ ∅"
        unfolding t setext binunion_def' singleton_def' by auto
      have esimp: "a ε⇧s ?t ⟷ a ε least_tsM x ∨ a = ∅" for a
      proof  
        assume "a ε⇧s ?t"
        from swap_mem_mem[OF _ this]
        have "a ε ?t"
          using ‹x ≠ ∅ ∧ x ≠ {∅}⇩M› ‹?t ≠ ∅› by blast    
        show "a ε least_tsM x ∨ a = ∅"
        proof (cases "a = ∅")
          assume "a ≠ ∅"
          have "a ε least_tsM x"
            unfolding least_ts_def'
          proof (rule ccontr)
            assume "¬ (∀v. transM v ∧ x ⊆⇩M v ⟶ a ε v)"
            then obtain v where "transM v" "x ⊆⇩M v" "¬ a ε v"
              by blast
            let ?v = "setsucM v ∅" 
            have "transM ?v" "𝔰𝔲𝔠 x ∅ ⊆⇩M ?v"
              using ‹transM v› ‹x ⊆⇩M v› unfolding transM_def subsetM_def setsuc_def' by force+
            hence "a ε ?v"
              using ‹a ε least_tsM (𝔰𝔲𝔠 x ∅)›[unfolded least_ts_def'] by blast
            thus False
              using ‹¬ a ε v› ‹a ≠ ∅› unfolding setsuc_def' by blast
          qed
          thus "a ε least_tsM x ∨ a = ∅"
            by blast
        qed simp
      next
        assume "a ε least_tsM x ∨ a = ∅" 
        hence "a ε least_tsM (𝔰𝔲𝔠 x ∅)"
          by (simp add: binunion_def' singleton_def' t)
        have "least_tsM (𝔰𝔲𝔠 x ∅) ≠ {∅}⇩M"
        proof
          assume "least_tsM (𝔰𝔲𝔠 x ∅) = {∅}⇩M"
          have "x ⊆⇩M least_tsM (𝔰𝔲𝔠 x ∅)"
            by (simp add: least_ts_def' subsetM_def)
          show False  
            using ‹x ≠ ∅ ∧ x ≠ {∅}⇩M›
            by (metis ‹least_tsM (𝔰𝔲𝔠 x ∅) = {∅}⇩M› ‹x ⊆⇩M least_tsM (𝔰𝔲𝔠 x ∅)› powerset_def' set_one_def set_two_mem)
        qed
        then show "a ε⇧sleast_tsM (𝔰𝔲𝔠 x ∅)"
          by (simp add: ‹a ε least_tsM (𝔰𝔲𝔠 x ∅)› swap_zero_one_mem)
      qed
      show  "∃z. (∀y. y ε⇧s z ⟶ (∀za. za ε⇧s y ⟶ za ε⇧s z)) ∧
        (∀za. za ε⇧s x ⟶ za ε⇧s z)"
      proof (rule exI[of _ ?t], rule conjI, rule allI, rule impI)
        fix y assume "y ε⇧s least_tsM (𝔰𝔲𝔠 x ∅)"
        then show "∀za. za ε⇧s y ⟶ za ε⇧s least_tsM (𝔰𝔲𝔠 x ∅)"
          unfolding esimp by (metis  empty_mem_false least_ts_is_transitive set_signature.subsetM_def swap_zero_one_mem transM_def)
      next
        show "∀za. za ε⇧s x ⟶ za ε⇧s least_tsM (𝔰𝔲𝔠 x ∅)"
          unfolding esimp using least_ts_def' subsetM_def swap_mem_mem by blast 
      qed
    qed
  qed
qed

end

theorem not_reg_model: assumes "L_setext_empty_power_union_repl (mem :: 'a ⇒ 'a ⇒ bool)" "L_setind mem" "L_ts mem"
  shows "¬ (∀ (m :: 'a ⇒ 'a ⇒ bool). L_setext_empty_power_union_repl m ∧ L_setind m ∧ L_ts m ⟶ L_reg m)"
proof (rule notI)
  assume contr: "∀(m :: 'a ⇒ 'a ⇒ bool). L_setext_empty_power_union_repl m ∧ L_setind m ∧ L_ts m ⟶ L_reg m"
  interpret L_setext_empty_power_union_repl mem
    using assms by simp
  interpret L_setind mem 
    using assms by simp
  interpret permutation_model mem swap_zero_one
    using swap_zero_one_perm_model.
  have "L_setext_empty_power_union_repl perm_mem ∧ L_setind perm_mem ∧ L_ts perm_mem"
    by (simp add: perm_model setind_swap_setind ts_swap_ts ‹L_setind mem› ‹L_ts mem›)
  from contr[rule_format, OF this]
  show False
    using not_reg_swap_zero_one by blast 
qed

end