Theory HereditarilyFinite.HF

chapter ‹The Hereditarily Finite Sets›

theory HF
imports "HOL-Library.Nat_Bijection"
abbrevs "<:" = "❙∈"
  and "~<:" = "❙∉"
begin

text ‹From "Finite sets and Gödel's Incompleteness Theorems" by S. Swierczkowski.
      Thanks for Brian Huffman for this development, up to the cases and induct rules.›

section ‹Basic Definitions and Lemmas›

typedef hf = "UNIV :: nat set" ..

definition hfset :: "hf ⇒ hf set"
  where "hfset a = Abs_hf ` set_decode (Rep_hf a)"

definition HF :: "hf set ⇒ hf"
  where "HF A = Abs_hf (set_encode (Rep_hf ` A))"

definition hinsert :: "hf ⇒ hf ⇒ hf"
  where "hinsert a b = HF (insert a (hfset b))"

definition hmem :: "hf ⇒ hf ⇒ bool"  (infixl ‹❙∈› 50)
  where "hmem a b ⟷ a ∈ hfset b"
  
abbreviation not_hmem :: "hf ⇒ hf ⇒ bool"  (infixl ‹❙∉› 50)
  where "a ❙∉ b ≡ ¬ a ❙∈ b"

notation (ASCII)
  hmem (infixl ‹<:› 50)

instantiation hf :: zero
begin
  definition Zero_hf_def: "0 = HF {}"
  instance ..
end

lemma Abs_hf_0 [simp]: "Abs_hf 0 = 0"
  by (simp add: HF_def Zero_hf_def)


text ‹HF Set enumerations›

abbreviation inserthf :: "hf ⇒ hf ⇒ hf"  (infixl ‹◃› 60)
  where "y ◃ x ≡ hinsert x y"

syntax (ASCII)
  "_HFinset" :: "args ⇒ hf"      (‹{|(_)|}›)
syntax
  "_HFinset" :: "args ⇒ hf"      (‹⦃_⦄›)
syntax_consts
  "_HFinset" ⇌ inserthf
translations
  "⦃x, y⦄" ⇌ "⦃y⦄ ◃ x"
  "⦃x⦄"    ⇌ "0 ◃ x"

lemma finite_hfset [simp]: "finite (hfset a)"
  unfolding hfset_def by simp

lemma HF_hfset [simp]: "HF (hfset a) = a"
  unfolding HF_def hfset_def
  by (simp add: image_image Abs_hf_inverse Rep_hf_inverse)

lemma hfset_HF [simp]: "finite A ⟹ hfset (HF A) = A"
  unfolding HF_def hfset_def
  by (simp add: image_image Abs_hf_inverse Rep_hf_inverse)

lemma inj_on_HF: "inj_on HF (Collect finite)"
  by (metis hfset_HF inj_onI mem_Collect_eq)

lemma hmem_hempty [simp]: "a ❙∉ 0"
  unfolding hmem_def Zero_hf_def by simp

lemmas hemptyE [elim!] = hmem_hempty [THEN notE]

lemma hmem_hinsert [iff]:
  "hmem a (c ◃ b) ⟷ a = b ∨ a ❙∈ c"
  unfolding hmem_def hinsert_def by simp

lemma hf_ext: "a = b ⟷ (∀x. x ❙∈ a ⟷ x ❙∈ b)"
  unfolding hmem_def set_eq_iff [symmetric]
  by (metis HF_hfset)

lemma finite_cases [consumes 1, case_names empty insert]:
  "⟦finite F; F = {} ⟹ P; ⋀A x. ⟦F = insert x A; x ∉ A; finite A⟧ ⟹ P⟧ ⟹ P"
by (induct F rule: finite_induct, simp_all)

lemma hf_cases [cases type: hf, case_names 0 hinsert]:
  obtains "y = 0" | a b where "y = b ◃ a" and "a ❙∉ b"
proof -
  have "finite (hfset y)" by (rule finite_hfset)
  thus thesis
    by (metis Zero_hf_def finite_cases hf_ext hfset_HF hinsert_def hmem_def that)
qed

lemma Rep_hf_hinsert:
  assumes "a ❙∉ b" shows "Rep_hf (hinsert a b) = 2 ^ (Rep_hf a) + Rep_hf b"
proof -
  have "Rep_hf a ∉ set_decode (Rep_hf b)"
    by (metis Rep_hf_inverse hfset_def hmem_def image_eqI assms)
  then show ?thesis
  by (simp add: hinsert_def HF_def hfset_def image_image Abs_hf_inverse Rep_hf_inverse)
qed


section ‹Verifying the Axioms of HF›

text ‹HF1›
lemma hempty_iff: "z=0 ⟷ (∀x. x ❙∉ z)"
  by (simp add: hf_ext)

text ‹HF2›
lemma hinsert_iff: "z = x ◃ y ⟷ (∀u. u ❙∈ z ⟷ u ❙∈ x ∨ u = y)"
  by (auto simp: hf_ext)

text ‹HF induction›
lemma hf_induct [induct type: hf, case_names 0 hinsert]:
  assumes [simp]: "P 0"
                  "⋀x y. ⟦P x; P y; x ❙∉ y⟧ ⟹ P (y ◃ x)"
  shows "P z"
proof (induct z rule: wf_induct [where r="measure Rep_hf", OF wf_measure])
  case (1 x) show ?case
    proof (cases x rule: hf_cases)
      case 0 thus ?thesis by simp
    next
      case (hinsert a b)
      thus ?thesis using 1
        by (simp add: Rep_hf_hinsert
                      less_le_trans [OF less_exp le_add1])
    qed
qed

text ‹HF3›
lemma hf_induct_ax: "⟦P 0; ∀x. P x ⟶ (∀y. P y ⟶ P (x ◃ y))⟧ ⟹ P x"
  by (induct x, auto)

lemma hf_equalityI [intro]: "(⋀x. x ❙∈ a ⟷ x ❙∈ b) ⟹ a = b"
  by (simp add: hf_ext)

lemma hinsert_nonempty [simp]: "A ◃ a ≠ 0"
  by (auto simp: hf_ext)

lemma hinsert_commute: "(z ◃ y) ◃ x = (z ◃ x) ◃ y"
  by (auto simp: hf_ext)

lemma hmem_HF_iff [simp]: "x ❙∈ HF A ⟷ x ∈ A ∧ finite A"
  by (metis Abs_hf_0 HF_def Rep_hf_inverse finite_imageD hemptyE hfset_HF hmem_def inj_onI set_encode_inf)


section ‹Ordered Pairs, from ZF/ZF.thy›

lemma singleton_eq_iff [iff]: "⦃a⦄ = ⦃b⦄ ⟷ a=b"
  by (metis hmem_hempty hmem_hinsert)

lemma doubleton_eq_iff: "⦃a,b⦄ = ⦃c,d⦄ ⟷ (a=c ∧ b=d) ∨ (a=d ∧ b=c)"
  by auto (metis hmem_hempty hmem_hinsert)+

definition hpair :: "hf ⇒ hf ⇒ hf"
  where "hpair a b = ⦃⦃a⦄,⦃a,b⦄⦄"

definition hfst :: "hf ⇒ hf"
  where "hfst p ≡ THE x. ∃y. p = hpair x y"

definition hsnd :: "hf ⇒ hf"
  where "hsnd p ≡ THE y. ∃x. p = hpair x y"

definition hsplit :: "[[hf, hf] ⇒ 'a, hf] ⇒ 'a::{}"  ― ‹for pattern-matching›
  where "hsplit c ≡ λp. c (hfst p) (hsnd p)"

text ‹Ordered Pairs, from ZF/ZF.thy›

nonterminal hfs
syntax (ASCII)
  "_Tuple"    :: "[hf, hfs] ⇒ hf"              (‹<(_,/ _)>›)
  "_hpattern" :: "[pttrn, patterns] ⇒ pttrn"   (‹<_,/ _>›)
syntax
  ""          :: "hf ⇒ hfs"                    (‹_›)
  "_Enum"     :: "[hf, hfs] ⇒ hfs"             (‹_,/ _›)
  "_Tuple"    :: "[hf, hfs] ⇒ hf"              (‹⟨(_,/ _)⟩›)
  "_hpattern" :: "[pttrn, patterns] ⇒ pttrn"   (‹⟨_,/ _⟩›)
syntax_consts
  "_Enum" "_Tuple" ⇌ hpair and
  "_hpattern" ⇌ hsplit
translations
  "<x, y, z>"    ⇌ "<x, <y, z>>"
  "<x, y>"       ⇌ "CONST hpair x y"
  "<x, y, z>"    ⇌ "<x, <y, z>>"
  "λ<x,y,zs>. b" ⇌ "CONST hsplit(λx <y,zs>. b)"
  "λ<x,y>. b"    ⇌ "CONST hsplit(λx y. b)"


lemma hpair_def': "hpair a b = ⦃⦃a,a⦄,⦃a,b⦄⦄"
  by (auto simp: hf_ext hpair_def)

lemma hpair_iff [simp]: "hpair a b = hpair a' b' ⟷ a=a' ∧ b=b'"
  by (auto simp: hpair_def' doubleton_eq_iff)

lemmas hpair_inject = hpair_iff [THEN iffD1, THEN conjE, elim!]

lemma hfst_conv [simp]: "hfst ⟨a,b⟩ = a"
  by (simp add: hfst_def)

lemma hsnd_conv [simp]: "hsnd ⟨a,b⟩ = b"
  by (simp add: hsnd_def)

lemma hsplit [simp]: "hsplit c ⟨a,b⟩ = c a b"
  by (simp add: hsplit_def)


section ‹Unions, Comprehensions, Intersections›

subsection ‹Unions›

text ‹Theorem 1.5 (Existence of the union of two sets).›
lemma binary_union: "∃z. ∀u. u ❙∈ z ⟷ u ❙∈ x ∨ u ❙∈ y"
proof (induct x rule: hf_induct)
  case 0 thus ?case by auto
next
  case (hinsert a b) thus ?case by (metis hmem_hinsert)
qed

text ‹Theorem 1.6 (Existence of the union of a set of sets).›
lemma union_of_set: "∃z. ∀u. u ❙∈ z ⟷ (∃y. y ❙∈ x ∧ u ❙∈ y)"
proof (induct x rule: hf_induct)
  case 0 thus ?case by (metis hmem_hempty)
next
  case (hinsert a b)
  then show ?case
    by (metis hmem_hinsert binary_union [of a])
qed


subsection ‹Set comprehensions›

text ‹Theorem 1.7, comprehension scheme›
lemma comprehension: "∃z. ∀u. u ❙∈ z ⟷ u ❙∈ x ∧ P u"
proof (induct x rule: hf_induct)
  case 0 thus ?case by (metis hmem_hempty)
next
  case (hinsert a b) thus ?case by (metis hmem_hinsert)
qed

definition HCollect :: "(hf ⇒ bool) ⇒ hf ⇒ hf" ― ‹comprehension›
  where "HCollect P A = (THE z. ∀u. u ❙∈ z = (P u ∧ u ❙∈ A))"

syntax (ASCII)
  "_HCollect" :: "idt ⇒ hf ⇒ bool ⇒ hf"    (‹(1⦃_ <:/ _./ _⦄)›)
syntax
  "_HCollect" :: "idt ⇒ hf ⇒ bool ⇒ hf"    (‹(1⦃_ ❙∈/ _./ _⦄)›)
syntax_consts
  "_HCollect" ⇌ HCollect
translations
  "⦃x ❙∈ A. P⦄" ⇌ "CONST HCollect (λx. P) A"

lemma HCollect_iff [iff]: "hmem x (HCollect P A) ⟷ P x ∧ x ❙∈ A"
  using comprehension [of A P]
  apply (clarsimp simp: HCollect_def)
  apply (rule theI2, blast)
   apply (auto simp: hf_ext)
  done

lemma HCollectI: "a ❙∈ A ⟹ P a ⟹ hmem a ⦃x ❙∈ A. P x⦄"
  by simp

lemma HCollectE:
  assumes "a ❙∈ ⦃x ❙∈ A. P x⦄" obtains "a ❙∈ A" "P a"
  using assms by auto

lemma HCollect_hempty [simp]: "HCollect P 0 = 0"
  by (simp add: hf_ext)


subsection ‹Union operators›

instantiation hf :: sup
begin
  definition "sup a b = (THE z. ∀u. u ❙∈ z ⟷ u ❙∈ a ∨ u ❙∈ b)"
  instance ..
end

abbreviation hunion :: "hf ⇒ hf ⇒ hf" (infixl ‹⊔› 65) where
  "hunion ≡ sup"

lemma hunion_iff [iff]: "hmem x (a ⊔ b) ⟷ x ❙∈ a ∨ x ❙∈ b"
  using binary_union [of a b]
  apply (clarsimp simp: sup_hf_def)
  apply (rule theI2, auto simp: hf_ext)
  done

definition HUnion :: "hf ⇒ hf"        (‹⨆_› [900] 900)
  where "HUnion A = (THE z. ∀u. u ❙∈ z ⟷ (∃y. y ❙∈ A ∧ u ❙∈ y))"

lemma HUnion_iff [iff]: "hmem x (⨆ A) ⟷ (∃y. y ❙∈ A ∧ x ❙∈ y)"
  using union_of_set [of A]
  apply (clarsimp simp: HUnion_def)
  apply (rule theI2, auto simp: hf_ext)
  done

lemma HUnion_hempty [simp]: "⨆ 0 = 0"
  by (simp add: hf_ext)

lemma HUnion_hinsert [simp]: "⨆(A ◃ a) = a ⊔ ⨆A"
  by (auto simp: hf_ext)

lemma HUnion_hunion [simp]: "⨆(A ⊔ B) =  ⨆A ⊔ ⨆B"
  by blast


subsection ‹Definition 1.8, Intersections›

instantiation hf :: inf
begin
  definition "inf a b = ⦃x ❙∈ a. x ❙∈ b⦄"
  instance ..
end

abbreviation hinter :: "hf ⇒ hf ⇒ hf" (infixl ‹⊓› 70) where
  "hinter ≡ inf"

lemma hinter_iff [iff]: "hmem u (x ⊓ y) ⟷ u ❙∈ x ∧ u ❙∈ y"
  by (metis HCollect_iff inf_hf_def)

definition HInter :: "hf ⇒ hf"           (‹⨅_› [900] 900)
  where "HInter(A) = ⦃x ❙∈ HUnion(A). ∀y. y ❙∈ A ⟶ x ❙∈ y⦄"

lemma HInter_hempty [iff]: "⨅ 0 = 0"
  by (metis HCollect_hempty HUnion_hempty HInter_def)

lemma HInter_iff [simp]: "A≠0 ⟹ hmem x (⨅ A) ⟷ (∀y. y ❙∈ A ⟶ x ❙∈ y)"
  by (auto simp: HInter_def)

lemma HInter_hinsert [simp]: "A≠0 ⟹ ⨅(A ◃ a) = a ⊓ ⨅A"
  by (auto simp: hf_ext HInter_iff [OF hinsert_nonempty])


subsection ‹Set Difference›

instantiation hf :: minus
begin
  definition "A - B = ⦃x ❙∈ A. x ❙∉ B⦄"
  instance ..
end

lemma hdiff_iff [iff]: "hmem u (x - y) ⟷ u ❙∈ x ∧ u ❙∉ y"
  by (auto simp: minus_hf_def)

lemma hdiff_zero [simp]: fixes x :: hf shows "(x - 0) = x"
  by blast

lemma zero_hdiff [simp]: fixes x :: hf shows "(0 - x) = 0"
  by blast

lemma hdiff_insert: "A - (B ◃ a) = A - B - ⦃a⦄"
  by blast

lemma hinsert_hdiff_if:
  "(A ◃ x) - B = (if x ❙∈ B then A - B else (A - B) ◃ x)"
  by auto


section ‹Replacement›

text ‹Theorem 1.9 (Replacement Scheme).›
lemma replacement:
  "(∀u v v'. u ❙∈ x ⟶ R u v ⟶ R u v' ⟶ v'=v) ⟹ ∃z. ∀v. v ❙∈ z ⟷ (∃u. u ❙∈ x ∧ R u v)"
proof (induct x rule: hf_induct)
  case 0 thus ?case
    by (metis hmem_hempty)
next
  case (hinsert a b) thus ?case
    by simp (metis hmem_hinsert)
qed

lemma replacement_fun: "∃z. ∀v. v ❙∈ z ⟷ (∃u. u ❙∈ x ∧ v = f u)"
  by (rule replacement [where R = "λu v. v = f u"]) auto

definition PrimReplace :: "hf ⇒ (hf ⇒ hf ⇒ bool) ⇒ hf"
  where "PrimReplace A R = (THE z. ∀v. v ❙∈ z ⟷ (∃u. u ❙∈ A ∧ R u v))"

definition Replace :: "hf ⇒ (hf ⇒ hf ⇒ bool) ⇒ hf"
  where "Replace A R = PrimReplace A (λx y. (∃!z. R x z) ∧ R x y)"

definition RepFun :: "hf ⇒ (hf ⇒ hf) ⇒ hf"
  where "RepFun A f = Replace A (λx y. y = f x)"


syntax (ASCII)
  "_HReplace"  :: "[pttrn, pttrn, hf, bool] ⇒ hf" (‹(1{|_ ./ _<: _, _|})›)
  "_HRepFun"   :: "[hf, pttrn, hf] ⇒ hf"          (‹(1{|_ ./ _<: _|})› [51,0,51])
  "_HINTER"    :: "[pttrn, hf, hf] ⇒ hf"          (‹(3INT _<:_./ _)› 10)
  "_HUNION"    :: "[pttrn, hf, hf] ⇒ hf"          (‹(3UN _<:_./ _)› 10)
syntax
  "_HReplace"  :: "[pttrn, pttrn, hf, bool] ⇒ hf" (‹(1⦃_ ./ _ ❙∈ _, _⦄)›)
  "_HRepFun"   :: "[hf, pttrn, hf] ⇒ hf"          (‹(1⦃_ ./ _ ❙∈ _⦄)› [51,0,51])
  "_HINTER"    :: "[pttrn, hf, hf] ⇒ hf"          (‹(3⨅_❙∈_./ _)› 10)
  "_HUNION"    :: "[pttrn, hf, hf] ⇒ hf"          (‹(3⨆_❙∈_./ _)› 10)
syntax_consts
  "_HReplace" ⇌ Replace and
  "_HRepFun" ⇌ RepFun and
  "_HINTER" ⇌ HInter and
  "_HUNION" ⇌ HUnion
translations
  "⦃y. x❙∈A, Q⦄" ⇌ "CONST Replace A (λx y. Q)"
  "⦃b. x❙∈A⦄"    ⇌ "CONST RepFun A (λx. b)"
  "⨅x❙∈A. B"    ⇌ "CONST HInter(CONST RepFun A (λx. B))"
  "⨆x❙∈A. B"    ⇌ "CONST HUnion(CONST RepFun A (λx. B))"

lemma PrimReplace_iff:
  assumes sv: "∀u v v'. u ❙∈ A ⟶ R u v ⟶ R u v' ⟶ v'=v"
  shows "v ❙∈ (PrimReplace A R) ⟷ (∃u. u ❙∈ A ∧ R u v)"
  using replacement [OF sv]
  apply (clarsimp simp: PrimReplace_def)
  apply (rule theI2, auto simp: hf_ext)
  done

lemma Replace_iff [iff]:
  "v ❙∈ Replace A R ⟷ (∃u. u ❙∈ A ∧ R u v ∧ (∀y. R u y ⟶ y=v))"
  unfolding Replace_def
  by (smt (verit, ccfv_threshold) PrimReplace_iff)

lemma Replace_0 [simp]: "Replace 0 R = 0"
  by blast

lemma Replace_hunion [simp]: "Replace (A ⊔ B) R = Replace A R  ⊔  Replace B R"
  by blast

lemma Replace_cong [cong]:
    "⟦ A=B;  ⋀x y. x ❙∈ B ⟹ P x y ⟷ Q x y ⟧  ⟹ Replace A P = Replace B Q"
  by (simp add: hf_ext cong: conj_cong)

lemma RepFun_iff [iff]: "v ❙∈ (RepFun A f) ⟷ (∃u. u ❙∈ A ∧ v = f u)"
  by (auto simp: RepFun_def)

lemma RepFun_cong [cong]:
    "⟦ A=B;  ⋀x. x ❙∈ B ⟹ f(x)=g(x) ⟧  ⟹ RepFun A f = RepFun B g"
by (simp add: RepFun_def)

lemma triv_RepFun [simp]: "RepFun A (λx. x) = A"
  by blast

lemma RepFun_0 [simp]: "RepFun 0 f = 0"
  by blast

lemma RepFun_hinsert [simp]: "RepFun (hinsert a b) f = hinsert (f a) (RepFun b f)"
  by blast

lemma RepFun_hunion [simp]:
  "RepFun (A ⊔ B) f = RepFun A f  ⊔  RepFun B f"
  by blast

lemma HF_HUnion: "⟦finite A; ⋀x. x∈A ⟹ finite (B x)⟧ ⟹ HF (⋃x ∈ A. B x) = (⨆x❙∈HF A. HF (B x))"
  by (rule hf_equalityI) (auto)


section ‹Subset relation and the Lattice Properties›

text ‹Definition 1.10 (Subset relation).›
instantiation hf :: order
begin
  definition less_eq_hf where "A ≤ B ⟷ (∀x. x ❙∈ A ⟶ x ❙∈ B)"

  definition less_hf    where "A < B ⟷ A ≤ B ∧ A ≠ (B::hf)"

  instance by standard (auto simp: less_eq_hf_def less_hf_def)
end


subsection ‹Rules for subsets›

lemma hsubsetI [intro!]:
    "(⋀x. x❙∈A ⟹ x❙∈B) ⟹ A ≤ B"
  by (simp add: less_eq_hf_def)

text ‹Classical elimination rule›
lemma hsubsetCE [elim]: "⟦ A ≤ B;  c❙∉A ⟹ P;  c❙∈B ⟹ P ⟧  ⟹ P"
  by (auto simp: less_eq_hf_def)

text ‹Rule in Modus Ponens style›
lemma hsubsetD [elim]: "⟦ A ≤ B;  c❙∈A ⟧ ⟹ c❙∈B"
  by auto

text ‹Sometimes useful with premises in this order›
lemma rev_hsubsetD: "⟦ c❙∈A; A≤B ⟧ ⟹ c❙∈B"
  by blast

lemma contra_hsubsetD: "⟦ A ≤ B; c ∉ B ⟧  ⟹ c ∉ A"
  by blast

lemma rev_contra_hsubsetD: "⟦ c ∉ B;  A ≤ B ⟧  ⟹ c ∉ A"
  by blast

lemma hf_equalityE:
  fixes A :: hf shows "A = B ⟹ (A ≤ B ⟹ B ≤ A ⟹ P) ⟹ P"
  by (metis order_refl)


subsection ‹Lattice properties›

instantiation hf :: distrib_lattice
begin
  instance by standard (auto simp: less_eq_hf_def less_hf_def inf_hf_def)
end

instantiation hf :: bounded_lattice_bot
begin
  definition "bot = (0::hf)"
  instance by standard (auto simp: less_eq_hf_def bot_hf_def)
end

lemma hinter_hempty_left [simp]: "0 ⊓ A = 0"
  by (metis bot_hf_def inf_bot_left)

lemma hinter_hempty_right [simp]: "A ⊓ 0 = 0"
  by (metis bot_hf_def inf_bot_right)

lemma hunion_hempty_left [simp]: "0 ⊔ A = A"
  by (metis bot_hf_def sup_bot_left)

lemma hunion_hempty_right [simp]: "A ⊔ 0 = A"
  by (metis bot_hf_def sup_bot_right)

lemma less_eq_hempty [simp]: "u ≤ 0 ⟷ u = (0::hf)"
  by (metis hempty_iff less_eq_hf_def)

lemma less_eq_insert1_iff [iff]: "(hinsert x y) ≤ z ⟷ x ❙∈ z ∧ y ≤ z"
  by (auto simp: less_eq_hf_def)

lemma less_eq_insert2_iff:
  "z ≤ (hinsert x y) ⟷ z ≤ y ∨ (∃u. hinsert x u = z ∧ x ❙∉ u ∧ u ≤ y)"
proof (cases "x ❙∈ z")
  case True
  hence u: "hinsert x (z - ⦃x⦄) = z" by auto
  show ?thesis
    proof
      assume "z ≤ (hinsert x y)"
      thus "z ≤ y ∨ (∃u. hinsert x u = z ∧ x ❙∉ u ∧ u ≤ y)"
        by (simp add: less_eq_hf_def) (metis u hdiff_iff hmem_hinsert)
    next
      assume "z ≤ y ∨ (∃u. hinsert x u = z ∧ x ❙∉ u ∧ u ≤ y)"
      thus "z ≤ (hinsert x y)"
        by (auto simp: less_eq_hf_def)
    qed
next
  case False thus ?thesis
    by (metis hmem_hinsert less_eq_hf_def)
qed

lemma zero_le [simp]: "0 ≤ (x::hf)"
  by blast

lemma hinsert_eq_sup: "b ◃ a = b ⊔ ⦃a⦄"
  by blast

lemma hunion_hinsert_left: "hinsert x A ⊔ B = hinsert x (A ⊔ B)"
  by blast

lemma hunion_hinsert_right: "B ⊔ hinsert x A = hinsert x (B ⊔ A)"
  by blast

lemma hinter_hinsert_left: "hinsert x A ⊓ B = (if x ❙∈ B then hinsert x (A ⊓ B) else A ⊓ B)"
  by auto

lemma hinter_hinsert_right: "B ⊓ hinsert x A = (if x ❙∈ B then hinsert x (B ⊓ A) else B ⊓ A)"
  by auto


section ‹Foundation, Cardinality, Powersets›

subsection ‹Foundation›

text ‹Theorem 1.13: Foundation (Regularity) Property.›
lemma foundation:
  assumes z: "z ≠ 0" shows "∃w. w ❙∈ z ∧ w ⊓ z = 0"
proof -
  { fix x
    assume z: "(∀w. w ❙∈ z ⟶ w ⊓ z ≠ 0)"
    have "x ❙∉ z ∧ x ⊓ z = 0"
    proof (induction x rule: hf_induct)
      case 0 thus ?case
        by (metis hinter_hempty_left z)
    next
      case (hinsert x y) thus ?case
        by (metis hinter_hinsert_left z)
    qed
  }
  thus ?thesis using z
    by (metis z hempty_iff)
qed

lemma hmem_not_refl: "x ❙∉ x"
  using foundation [of "⦃x⦄"]
  by (metis hinter_iff hmem_hempty hmem_hinsert)

lemma hmem_not_sym: "¬ (x ❙∈ y ∧ y ❙∈ x)"
  using foundation [of "⦃x,y⦄"]
  by (metis hinter_iff hmem_hempty hmem_hinsert)

lemma hmem_ne: "x ❙∈ y ⟹ x ≠ y"
  by (metis hmem_not_refl)

lemma hmem_Sup_ne: "x ❙∈ y ⟹ ⨆x ≠ y"
  by (metis HUnion_iff hmem_not_sym)

lemma hpair_neq_fst: "⟨a,b⟩ ≠ a"
  by (metis hpair_def hinsert_iff hmem_not_sym)

lemma hpair_neq_snd: "⟨a,b⟩ ≠ b"
  by (metis hpair_def hinsert_iff hmem_not_sym)

lemma hpair_nonzero [simp]: "⟨x,y⟩ ≠ 0"
  by (auto simp: hpair_def)

lemma zero_notin_hpair: "0 ❙∉ ⟨x,y⟩"
  by (auto simp: hpair_def)


subsection ‹Cardinality›

text ‹First we need to hack the underlying representation›
lemma hfset_0 [simp]: "hfset 0 = {}"
  by (metis Zero_hf_def finite.emptyI hfset_HF)

lemma hfset_hinsert: "hfset (b ◃ a) = insert a (hfset b)"
  by (metis finite_insert hinsert_def HF.finite_hfset hfset_HF)

lemma hfset_hdiff: "hfset (x - y) = hfset x - hfset y"
proof (induct x arbitrary: y rule: hf_induct)
  case 0 thus ?case
    by simp
next
  case (hinsert a b) thus ?case
    by (simp add: hfset_hinsert Set.insert_Diff_if hinsert_hdiff_if hmem_def)
qed

definition hcard :: "hf ⇒ nat"
  where "hcard x = card (hfset x)"

lemma hcard_0 [simp]: "hcard 0 = 0"
  by (simp add: hcard_def)

lemma hcard_hinsert_if: "hcard (hinsert x y) = (if x ❙∈ y then hcard y else Suc (hcard y))"
  by (simp add: hcard_def hfset_hinsert card_insert_if hmem_def)

lemma hcard_union_inter: "hcard (x ⊔ y) + hcard (x ⊓ y) = hcard x + hcard y"
proof (induct x arbitrary: y rule: hf_induct)
next
  case (hinsert x y)
  then show ?case
    by (simp add: hcard_hinsert_if hinter_hinsert_left hunion_hinsert_left)
qed auto

lemma hcard_hdiff1_less: "x ❙∈ z ⟹ hcard (z - ⦃x⦄) < hcard z"
  unfolding hmem_def
  by (metis card_Diff1_less finite_hfset hcard_def hfset_0 hfset_hdiff hfset_hinsert)


subsection ‹Powerset Operator›

text ‹Theorem 1.11 (Existence of the power set).›
lemma powerset: "∃z. ∀u. u ❙∈ z ⟷ u ≤ x"
proof (induction x rule: hf_induct)
 case 0 thus ?case
    by (metis hmem_hempty hmem_hinsert less_eq_hempty)
next
  case (hinsert a b)
  then obtain Pb where Pb: "∀u. u ❙∈ Pb ⟷ u ≤ b"
    by auto
  obtain RPb where RPb: "∀v. v ❙∈ RPb ⟷ (∃u. u ❙∈ Pb ∧ v = hinsert a u)"
    using replacement_fun ..
  thus ?case using Pb binary_union [of Pb RPb]
    unfolding less_eq_insert2_iff
    by (smt (verit, ccfv_threshold) hinsert.hyps less_eq_hf_def)
qed

definition HPow :: "hf ⇒ hf"
  where "HPow x = (THE z. ∀u. u ❙∈ z ⟷ u ≤ x)"

lemma HPow_iff [iff]: "u ❙∈ HPow x ⟷ u ≤ x"
  using powerset [of x]
  apply (clarsimp simp: HPow_def)
  apply (rule theI2, auto simp: hf_ext)
  done

lemma HPow_mono: "x ≤ y ⟹ HPow x ≤ HPow y"
  by (metis HPow_iff less_eq_hf_def order_trans)

lemma HPow_mono_strict: "x < y ⟹ HPow x < HPow y"
  by (metis HPow_iff HPow_mono less_le_not_le order_eq_iff)

lemma HPow_mono_iff [simp]: "HPow x ≤ HPow y ⟷ x ≤ y"
  by (metis HPow_iff HPow_mono hsubsetCE order_refl)

lemma HPow_mono_strict_iff [simp]: "HPow x < HPow y ⟷ x < y"
  by (metis HPow_mono_iff less_le_not_le)


section ‹Bounded Quantifiers›

definition HBall :: "hf ⇒ (hf ⇒ bool) ⇒ bool" where
  "HBall A P ⟷ (∀x. x ❙∈ A ⟶ P x)"   ― ‹bounded universal quantifiers›

definition HBex :: "hf ⇒ (hf ⇒ bool) ⇒ bool" where
  "HBex A P ⟷ (∃x. x ❙∈ A ∧ P x)"   ― ‹bounded existential quantifiers›

syntax (ASCII)
  "_HBall"       :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3ALL _<:_./ _)› [0, 0, 10] 10)
  "_HBex"        :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3EX _<:_./ _)›  [0, 0, 10] 10)
  "_HBex1"       :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3EX! _<:_./ _)› [0, 0, 10] 10)
syntax
  "_HBall"       :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3∀_❙∈_./ _)›  [0, 0, 10] 10)
  "_HBex"        :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3∃_❙∈_./ _)›  [0, 0, 10] 10)
  "_HBex1"       :: "pttrn ⇒ hf ⇒ bool ⇒ bool"      (‹(3∃!_❙∈_./ _)› [0, 0, 10] 10)
syntax_consts
  "_HBall" ⇌ HBall and
  "_HBex" ⇌ HBex and
  "_HBex1" ⇌ Ex1
translations
  "∀x❙∈A. P" ⇌ "CONST HBall A (λx. P)"
  "∃x❙∈A. P" ⇌ "CONST HBex A (λx. P)"
  "∃!x❙∈A. P" ⇀ "∃!x. x∈A ∧ P"

lemma hball_cong [cong]:
    "⟦ A=A';  ⋀x. x ❙∈ A' ⟹ P(x) ⟷ P'(x) ⟧  ⟹ (∀x❙∈A. P(x)) ⟷ (∀x❙∈A'. P'(x))"
  by (simp add: HBall_def)

lemma hballI [intro!]: "(⋀x. x❙∈A ⟹ P x) ⟹ ∀x❙∈A. P x"
  by (simp add: HBall_def)

lemma hbspec [dest?]: "∀x❙∈A. P x ⟹ x❙∈A ⟹ P x"
  by (simp add: HBall_def)

lemma hballE [elim]: "∀x❙∈A. P x ⟹ (P x ⟹ Q) ⟹ (x ❙∉ A ⟹ Q) ⟹ Q"
  by (force simp add: HBall_def)

lemma hbex_cong [cong]:
    "⟦ A=A';  ⋀x. x ❙∈ A' ⟹ P(x) ⟷ P'(x) ⟧  ⟹ (∃x❙∈A. P(x)) ⟷ (∃x❙∈A'. P'(x))"
  by (simp add: HBex_def cong: conj_cong)

lemma hbexI [intro]: "P x ⟹ x❙∈A ⟹ ∃x❙∈A. P x" 
  and rev_hbexI [intro?]: "x❙∈A ⟹ P x ⟹ ∃x❙∈A. P x"
  and bexCI: "(∀x❙∈A. ¬ P x ⟹ P a) ⟹ a❙∈A ⟹ ∃x❙∈A. P x"
  and hbexE [elim!]: "∃x❙∈A. P x ⟹ (⋀x. x❙∈A ⟹ P x ⟹ Q) ⟹ Q"
  using HBex_def by auto

lemma hball_triv [simp]: "(∀x❙∈A. P) = ((∃x. x❙∈A) ⟶ P)" 
  and hbex_triv [simp]: "(∃x❙∈A. P) = ((∃x. x❙∈A) ∧ P)"
  ― ‹Dual form for existentials.›
  by blast+

lemma hbex_triv_one_point1 [simp]: "(∃x❙∈A. x = a) = (a❙∈A)"
  by blast

lemma hbex_triv_one_point2 [simp]: "(∃x❙∈A. a = x) = (a❙∈A)"
  by blast

lemma hbex_one_point1 [simp]: "(∃x❙∈A. x = a ∧ P x) = (a❙∈A ∧ P a)"
  by blast

lemma hbex_one_point2 [simp]: "(∃x❙∈A. a = x ∧ P x) = (a❙∈A ∧ P a)"
  by blast

lemma hball_one_point1 [simp]: "(∀x❙∈A. x = a ⟶ P x) = (a❙∈A ⟶ P a)"
  by blast

lemma hball_one_point2 [simp]: "(∀x❙∈A. a = x ⟶ P x) = (a❙∈A ⟶ P a)"
  by blast

lemma hball_conj_distrib:
  "(∀x❙∈A. P x ∧ Q x) ⟷ ((∀x❙∈A. P x) ∧ (∀x❙∈A. Q x))"
  by blast

lemma hbex_disj_distrib:
  "(∃x❙∈A. P x ∨ Q x) ⟷ ((∃x❙∈A. P x) ∨ (∃x❙∈A. Q x))"
  by blast

lemma hb_all_simps [simp, no_atp]:
  "⋀A P Q. (∀x ❙∈ A. P x ∨ Q) ⟷ ((∀x ❙∈ A. P x) ∨ Q)"
  "⋀A P Q. (∀x ❙∈ A. P ∨ Q x) ⟷ (P ∨ (∀x ❙∈ A. Q x))"
  "⋀A P Q. (∀x ❙∈ A. P ⟶ Q x) ⟷ (P ⟶ (∀x ❙∈ A. Q x))"
  "⋀A P Q. (∀x ❙∈ A. P x ⟶ Q) ⟷ ((∃x ❙∈ A. P x) ⟶ Q)"
  "⋀P. (∀x ❙∈ 0. P x) ⟷ True"
  "⋀a B P. (∀x ❙∈ B ◃ a. P x) ⟷ (P a ∧ (∀x ❙∈ B. P x))"
  "⋀P Q. (∀x ❙∈ HCollect Q A. P x) ⟷ (∀x ❙∈ A. Q x ⟶ P x)"
  "⋀A P. (¬ (∀x ❙∈ A. P x)) ⟷ (∃x ❙∈ A. ¬ P x)"
  by auto

lemma hb_ex_simps [simp, no_atp]:
  "⋀A P Q. (∃x ❙∈ A. P x ∧ Q) ⟷ ((∃x ❙∈ A. P x) ∧ Q)"
  "⋀A P Q. (∃x ❙∈ A. P ∧ Q x) ⟷ (P ∧ (∃x ❙∈ A. Q x))"
  "⋀P. (∃x ❙∈ 0. P x) ⟷ False"
  "⋀a B P. (∃x ❙∈ B ◃ a. P x) ⟷ (P a ∨ (∃x ❙∈ B. P x))"
  "⋀P Q. (∃x ❙∈ HCollect Q A. P x) ⟷ (∃x ❙∈ A. Q x ∧ P x)"
  "⋀A P. (¬(∃x ❙∈ A. P x)) ⟷ (∀x ❙∈ A. ¬ P x)"
  by auto

lemma le_HCollect_iff: "A ≤ ⦃x ❙∈ B. P x⦄ ⟷ A ≤ B ∧ (∀x ❙∈ A. P x)"
  by blast


section ‹Relations and Functions›

definition is_hpair :: "hf ⇒ bool"
  where "is_hpair z = (∃x y. z = ⟨x,y⟩)"

definition hconverse :: "hf ⇒ hf"
  where "hconverse(r) = ⦃z. w ❙∈ r, ∃x y. w = ⟨x,y⟩ ∧ z = ⟨y,x⟩⦄"

definition hdomain :: "hf ⇒ hf"
  where "hdomain(r) = ⦃x. w ❙∈ r, ∃y. w = ⟨x,y⟩⦄"

definition hrange :: "hf ⇒ hf"
  where "hrange(r) = hdomain(hconverse(r))"

definition hrelation :: "hf ⇒ bool"
  where "hrelation(r) = (∀z. z ❙∈ r ⟶ is_hpair z)"

definition hrestrict :: "hf ⇒ hf ⇒ hf"
  ― ‹Restrict the relation r to the domain A›
  where "hrestrict r A = ⦃z ❙∈ r. ∃x ❙∈ A. ∃y. z = ⟨x,y⟩⦄"

definition nonrestrict :: "hf ⇒ hf ⇒ hf"
  where "nonrestrict r A = ⦃z ❙∈ r. ∀x ❙∈ A. ∀y. z ≠ ⟨x,y⟩⦄"

definition hfunction :: "hf ⇒ bool"
  where "hfunction(r) = (∀x y. ⟨x,y⟩ ❙∈ r ⟶ (∀y'. ⟨x,y'⟩ ❙∈ r ⟶ y=y'))"

definition app :: "hf ⇒ hf ⇒ hf"
  where "app f x = (THE y. ⟨x, y⟩ ❙∈ f)"

lemma hrestrict_iff [iff]:
    "z ❙∈ hrestrict r A ⟷ z ❙∈ r ∧ (∃ x y. z = ⟨x, y⟩ ∧ x ❙∈ A)"
  by (auto simp: hrestrict_def)

lemma hrelation_0 [simp]: "hrelation 0"
  by (force simp add: hrelation_def)

lemma hrelation_restr [iff]: "hrelation (hrestrict r x)"
  by (metis hrelation_def hrestrict_iff is_hpair_def)

lemma hrelation_hunion [simp]: "hrelation (f ⊔ g) ⟷ hrelation f ∧ hrelation g"
  by (auto simp: hrelation_def)

lemma hfunction_restr: "hfunction r ⟹ hfunction (hrestrict r x)"
  by (auto simp: hfunction_def hrestrict_def)

lemma hdomain_restr [simp]: "hdomain (hrestrict r x) = hdomain r ⊓ x"
  by (force simp add: hdomain_def hrestrict_def)

lemma hdomain_0 [simp]: "hdomain 0 = 0"
  by (force simp add: hdomain_def)

lemma hdomain_ins [simp]: "hdomain (r ◃ ⟨x, y⟩) = hdomain r ◃ x"
  by (force simp add: hdomain_def)

lemma hdomain_hunion [simp]: "hdomain (f ⊔ g) = hdomain f ⊔ hdomain g"
  by (simp add: hdomain_def)

lemma hdomain_not_mem [iff]: "⟨hdomain r, a⟩ ❙∉ r"
  by (metis hdomain_ins hinter_hinsert_right hmem_hinsert hmem_not_refl
            hunion_hinsert_right sup_inf_absorb)

lemma app_singleton [simp]: "app ⦃⟨x, y⟩⦄ x = y"
  by (simp add: app_def)

lemma app_equality: "hfunction f ⟹ ⟨x, y⟩ ❙∈ f ⟹ app f x = y"
  by (auto simp: app_def hfunction_def intro: the1I2)

lemma app_ins2: "x' ≠ x ⟹ app (f ◃ ⟨x, y⟩) x' = app f x'"
  by (simp add: app_def)

lemma hfunction_0 [simp]: "hfunction 0"
  by (force simp add: hfunction_def)

lemma hfunction_ins: "hfunction f ⟹ x ❙∉ hdomain f ⟹ hfunction (f◃ ⟨x, y⟩)"
  by (auto simp: hfunction_def hdomain_def)

lemma hdomainI: "⟨x, y⟩ ❙∈ f ⟹ x ❙∈ hdomain f"
  by (auto simp: hdomain_def)

lemma hfunction_hunion: "hdomain f ⊓ hdomain g = 0
            ⟹ hfunction (f ⊔ g) ⟷ hfunction f ∧ hfunction g"
  by (auto simp: hfunction_def) (metis hdomainI hinter_iff hmem_hempty)+

lemma app_hrestrict [simp]: "x ❙∈ A ⟹ app (hrestrict f A) x = app f x"
  by (simp add: hrestrict_def app_def)


section ‹Operations on families of sets›

definition HLambda :: "hf ⇒ (hf ⇒ hf) ⇒ hf"
  where "HLambda A b = RepFun A (λx. ⟨x, b x⟩)"

definition HSigma :: "hf ⇒ (hf ⇒ hf) ⇒ hf"
  where "HSigma A B = (⨆x❙∈A. ⨆y❙∈B(x). ⦃⟨x,y⟩⦄)"

definition HPi :: "hf ⇒ (hf ⇒ hf) ⇒ hf"
  where "HPi A B = ⦃ f ❙∈ HPow(HSigma A B). A ≤ hdomain(f) ∧ hfunction(f)⦄"


syntax (ASCII)
  "_PROD"     :: "[pttrn, hf, hf] ⇒ hf"        (‹(3PROD _<:_./ _)› 10)
  "_SUM"      :: "[pttrn, hf, hf] ⇒ hf"        (‹(3SUM _<:_./ _)› 10)
  "_lam"      :: "[pttrn, hf, hf] ⇒ hf"        (‹(3lam _<:_./ _)› 10)
syntax
  "_PROD"     :: "[pttrn, hf, hf] ⇒ hf"        (‹(3∏_❙∈_./ _)› 10)
  "_SUM"      :: "[pttrn, hf, hf] ⇒ hf"        (‹(3∑_❙∈_./ _)› 10)
  "_lam"      :: "[pttrn, hf, hf] ⇒ hf"        (‹(3λ_❙∈_./ _)› 10)
syntax_consts
  "_PROD" ⇌ HPi and
  "_SUM" ⇌ HSigma and
  "_lam" ⇌ HLambda
translations
  "∏x❙∈A. B" ⇌ "CONST HPi A (λx. B)"
  "∑x❙∈A. B" ⇌ "CONST HSigma A (λx. B)"
  "λx❙∈A. f"  ⇌ "CONST HLambda A (λx. f)"


subsection ‹Rules for Unions and Intersections of families›

lemma HUN_iff [simp]: "b ❙∈ (⨆x❙∈A. B(x)) ⟷ (∃x❙∈A. b ❙∈ B(x))"
  by auto

(*The order of the premises presupposes that A is rigid; b may be flexible*)
lemma HUN_I: "⟦ a ❙∈ A;  b ❙∈ B(a) ⟧  ⟹ b ❙∈ (⨆x❙∈A. B(x))"
  by auto

lemma HUN_E [elim!]: assumes "b ❙∈ (⨆x❙∈A. B(x))" obtains x where "x ❙∈ A"  "b ❙∈ B(x)"
  using assms  by blast

lemma HINT_iff: "b ❙∈ (⨅x❙∈A. B(x)) ⟷ (∀x❙∈A. b ❙∈ B(x)) ∧ A≠0"
  by (simp add: HInter_def HBall_def) (metis foundation hmem_hempty)

lemma HINT_I: "⟦ ⋀x. x ❙∈ A ⟹ b ❙∈ B(x);  A≠0 ⟧ ⟹ b ❙∈ (⨅x❙∈A. B(x))"
  by (simp add: HINT_iff)

lemma HINT_E: "⟦ b ❙∈ (⨅x❙∈A. B(x));  a ❙∈ A ⟧ ⟹ b ❙∈ B(a)"
  by (auto simp: HINT_iff)


subsection ‹Generalized Cartesian product›

lemma HSigma_iff [simp]: "⟨a,b⟩ ❙∈ HSigma A B ⟷ a ❙∈ A ∧ b ❙∈ B(a)"
  by (force simp add: HSigma_def)

lemma HSigmaI [intro!]: "⟦ a ❙∈ A;  b ❙∈ B(a) ⟧  ⟹ ⟨a,b⟩ ❙∈ HSigma A B"
  by simp

lemmas HSigmaD1 = HSigma_iff [THEN iffD1, THEN conjunct1]
lemmas HSigmaD2 = HSigma_iff [THEN iffD1, THEN conjunct2]

text ‹The general elimination rule›
lemma HSigmaE [elim!]:
  assumes "c ❙∈ HSigma A B"
  obtains x y where "x ❙∈ A" "y ❙∈ B(x)" "c=⟨x,y⟩"
  using assms  by (force simp add: HSigma_def)

lemma HSigmaE2 [elim!]:
  assumes "⟨a,b⟩ ❙∈ HSigma A B" obtains "a ❙∈ A" and "b ❙∈ B(a)"
  using assms  by auto

lemma HSigma_empty1 [simp]: "HSigma 0 B = 0"
  by blast

instantiation hf :: times
begin
  definition "A * B = HSigma A (λx. B)"
  instance ..
end

lemma times_iff [simp]: "⟨a,b⟩ ❙∈ A * B ⟷ a ❙∈ A ∧ b ❙∈ B"
  by (simp add: times_hf_def)

lemma timesI [intro!]: "⟦ a ❙∈ A;  b ❙∈ B ⟧  ⟹ ⟨a,b⟩ ❙∈ A * B"
  by simp

lemmas timesD1 = times_iff [THEN iffD1, THEN conjunct1]
lemmas timesD2 = times_iff [THEN iffD1, THEN conjunct2]

text ‹The general elimination rule›
lemma timesE [elim!]:
  assumes c: "c ❙∈ A * B"
  obtains x y where "x ❙∈ A" "y ❙∈ B" "c=⟨x,y⟩" using c
  by (auto simp: times_hf_def)

text ‹...and a specific one›
lemma timesE2 [elim!]:
  assumes "⟨a,b⟩ ❙∈ A * B" obtains "a ❙∈ A" and "b ❙∈ B"
using assms
  by auto

lemma times_empty1 [simp]: "0 * B = (0::hf)"
  by auto

lemma times_empty2 [simp]: "A*0 = (0::hf)"
  by blast

lemma times_empty_iff: "A*B=0 ⟷ A=0 ∨ B=(0::hf)"
  by (auto simp: times_hf_def hf_ext)

instantiation hf :: mult_zero
begin
  instance by standard auto
end


section ‹Disjoint Sum›

instantiation hf :: zero_neq_one
begin
  definition One_hf_def: "1 = ⦃0⦄"
  instance by standard (auto simp: One_hf_def)
end

instantiation hf :: plus
begin
  definition "A + B = (⦃0⦄ * A) ⊔ (⦃1⦄ * B)"
  instance ..
end

definition Inl :: "hf⇒hf" where
     "Inl(a) ≡ ⟨0,a⟩"

definition Inr :: "hf⇒hf" where
     "Inr(b) ≡ ⟨1,b⟩"

lemmas sum_defs = plus_hf_def Inl_def Inr_def

lemma Inl_nonzero [simp]:"Inl x ≠ 0"
  by (metis Inl_def hpair_nonzero)

lemma Inr_nonzero [simp]:"Inr x ≠ 0"
  by (metis Inr_def hpair_nonzero)

text‹Introduction rules for the injections (as equivalences)›

lemma Inl_in_sum_iff [iff]: "Inl(a) ❙∈ A+B ⟷ a ❙∈ A"
  by (auto simp: sum_defs)

lemma Inr_in_sum_iff [iff]: "Inr(b) ❙∈ A+B ⟷ b ❙∈ B"
  by (auto simp: sum_defs)

text ‹Elimination rule›

lemma sumE [elim!]:
  assumes u: "u ❙∈ A+B"
  obtains x where "x ❙∈ A" "u=Inl(x)" | y where "y ❙∈ B" "u=Inr(y)" using u
  by (auto simp: sum_defs)

text ‹Injection and freeness equivalences, for rewriting›

lemma Inl_iff [iff]: "Inl(a)=Inl(b) ⟷ a=b"
  by (simp add: sum_defs)

lemma Inr_iff [iff]: "Inr(a)=Inr(b) ⟷ a=b"
  by (simp add: sum_defs)

lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) ⟷ False"
  by (simp add: sum_defs)

lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) ⟷ False"
  by (simp add: sum_defs)

lemma sum_empty [simp]: "0+0 = (0::hf)"
  by (auto simp: sum_defs)

lemma sum_iff: "u ❙∈ A+B ⟷ (∃x. x ❙∈ A ∧ u=Inl(x)) ∨ (∃y. y ❙∈ B ∧ u=Inr(y))"
  by blast

lemma sum_subset_iff:
  fixes A :: hf shows "A+B ≤ C+D ⟷ A≤C ∧ B≤D"
  by blast

lemma sum_equal_iff:
  fixes A :: hf shows "A+B = C+D ⟷ A=C ∧ B=D"
  by (auto simp: hf_ext sum_subset_iff)

definition is_hsum :: "hf ⇒ bool"
  where "is_hsum z = (∃x. z = Inl x ∨ z = Inr x)"

definition sum_case  :: "(hf ⇒ 'a) ⇒ (hf ⇒ 'a) ⇒ hf ⇒ 'a"
  where
  "sum_case f g a ≡
    THE z. (∀x. a = Inl x ⟶ z = f x) ∧ (∀y. a = Inr y ⟶ z = g y) ∧ (¬ is_hsum a ⟶ z = undefined)"

lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x"
  by (simp add: sum_case_def is_hsum_def)

lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"
  by (simp add: sum_case_def is_hsum_def)

lemma sum_case_non [simp]: "¬ is_hsum a ⟹ sum_case f g a = undefined"
  by (simp add: sum_case_def is_hsum_def)

lemma is_hsum_cases: "(∃x. z = Inl x ∨ z = Inr x) ∨ ¬ is_hsum z"
  by (auto simp: is_hsum_def)

lemma sum_case_split:
  "P (sum_case f g a) ⟷ (∀x. a = Inl x ⟶ P(f x)) ∧ (∀y. a = Inr y ⟶ P(g y)) ∧ (¬ is_hsum a ⟶ P undefined)"
  by (cases "is_hsum a") (auto simp: is_hsum_def)

lemma sum_case_split_asm:
  "P (sum_case f g a) ⟷ ¬ ((∃x. a = Inl x ∧ ¬ P(f x)) ∨ (∃y. a = Inr y ∧ ¬ P(g y)) ∨ (¬ is_hsum a ∧ ¬ P undefined))"
  by (auto simp add: sum_case_split)

end