Theory ZFfin_HF

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


chapter ‹Models and counter-models›
theory ZFfin_HF
imports HereditarilyFinite.Rank ZFfin
begin

section ‹Hereditarily finite sets›

text ‹We show that the hereditarily finite sets as implemented in @{theory HereditarilyFinite.HF} are a model of 
 ZFfin as implemented in @{theory ZF_finite.ZFfin}›

interpretation zfhf: ZFfin "(❙∈)"
  rewrites "zfhf.emptysetM = 0" and
           "zfhf.singletonM y = ⦃y⦄" and
           "zfhf.setsucM x y = x ◃ y"
proof-
  interpret zfhf: L_setsuc  "(❙∈)"
    by unfold_locales blast+ 
  interpret zfhf: L_empty  "(❙∈)"
    by unfold_locales blast
  interpret zfhf: L_setext_empty  "(❙∈)"
    by unfold_locales blast
  show zfhf_emp: "zfhf.emptysetM = 0"
      using zfhf.empty_is_empty by auto
  interpret zfhf: L_setsuc  "(❙∈)"
    by unfold_locales blast+ 
  interpret zfhf: L_empty  "(❙∈)"
    by unfold_locales blast
  interpret zfhf: L_setext_empty_setsuc "(❙∈)"
    by unfold_locales
  show zfhf_sing: "zfhf.singletonM y = ⦃y⦄" for y
    using zfhf.singleton_def' by blast  
  show zfhf_suc:  "zfhf.setsucM x y = x ◃ y" for x y
    unfolding zfhf.setext[of _ "x ◃ y"] zfhf.setsuc_def'  by auto 
  interpret L_setind "(❙∈)"
  proof
    show "zfhf.SetFormulaPredicate P ⟹  P (Ξ(0 := zfhf.emptysetM)) ⟶
        (∀x y. P (Ξ(0 := x)) ⟶ P (Ξ(0 := zfhf.setsucM x y))) ⟶ (∀x. P (Ξ(0 := x)))" for P Ξ
      unfolding zfhf_suc zfhf_emp using hf_induct[of "λ a. P (Ξ(0:=a))"] by blast
  qed
  interpret L_setext_empty_setsuc_setind "(❙∈)"
    by unfold_locales
  interpret L_epsind "(❙∈)"
  proof
    fix Ξ  :: "nat ⇒ hf" and Q
    from Rank.hmem_induct[of "λ x. Q(Ξ(0:=x))"]
    show "(∀x. (∀y. y ❙∈ x ⟶ Q (Ξ(0 := y))) ⟶ Q (Ξ(0 := x))) ⟶ (∀x. Q (Ξ(0 := x)))"
      by blast
  qed
  show "ZFfin (❙∈)"
  proof (unfold_locales, unfold zfhf_emp zfhf_suc) 
    fix Ξ  :: "nat ⇒ hf" and P
    from hf_induct[of "λ x. P(Ξ(0:=x))"]
    show "∄x. 0 ❙∈ x ∧ (∀y. y ❙∈ x ⟶ y ◃ y ❙∈ x)"
      using fin zfhf_emp zfhf_suc by auto
  qed
qed  

end