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"      ("⦃_⦄")
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:
  "a ❙∉ b ⟹ Rep_hf (hinsert a b) = 2 ^ (Rep_hf a) + Rep_hf b"
  unfolding hinsert_def HF_def hfset_def
  apply (simp add: image_image Abs_hf_inverse Rep_hf_inverse)
  apply (subst set_encode_insert, simp)
  apply (clarsimp simp add: hmem_def hfset_def image_def
    Rep_hf_inject [symmetric] Abs_hf_inverse, simp)
  done

lemma less_two_power: "n < 2 ^ n"
  by (fact less_exp)


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_two_power 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"
  apply (cases "finite A", auto)
  apply (simp add: hmem_def)
  apply (simp add: hmem_def)
  apply (metis HF_def Rep_hf_inject Abs_hf_0 finite_imageD hempty_iff inj_onI set_encode_inf)
  done


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"   ("⟨_,/ _⟩")
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⦃_ ❙∈/ _./ _⦄)")
translations
  "⦃x ❙∈ A. P⦄" ⇌ "CONST HCollect (λx. P) A"

lemma HCollect_iff [iff]: "hmem x (HCollect P A) ⟷ P x ∧ x ❙∈ A"
apply (insert comprehension [of A P], clarify)
apply (simp add: 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"
apply (insert binary_union [of a b], clarify)
apply (simp add: sup_hf_def)
apply (rule theI2)
apply (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)"
apply (insert union_of_set [of A], clarify)
apply (simp add: HUnion_def)
apply (rule theI2)
apply (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)
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)"
apply (insert replacement [OF sv], clarify)
apply (simp add: PrimReplace_def)
apply (rule theI2)
apply (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))"
apply (simp add: Replace_def)
apply (subst PrimReplace_iff, auto)
done

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 (simp add: less_eq_hf_def)

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"
  apply (induct x arbitrary: y rule: hf_induct)
  apply (auto simp: hcard_hinsert_if hunion_hinsert_left hinter_hinsert_left)
  done

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


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]
    apply (simp add: less_eq_insert2_iff, clarify)
    apply (rule_tac x=z in exI)
    apply (metis hinsert.hyps less_eq_hf_def)
    done
qed

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

lemma HPow_iff [iff]: "u ❙∈ HPow x ⟷ u ≤ x"
apply (insert powerset [of x], clarify)
apply (simp add: HPow_def)
apply (rule theI2)
apply (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)
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 (unfold HBall_def) blast

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"
  by (unfold HBex_def) blast

lemma rev_hbexI [intro?]: "x❙∈A ⟹ P x ⟹ ∃x❙∈A. P x"
  by (unfold HBex_def) blast

lemma bexCI: "(∀x❙∈A. ¬ P x ⟹ P a) ⟹ a❙∈A ⟹ ∃x❙∈A. P x"
  by (unfold HBex_def) blast

lemma hbexE [elim!]: "∃x❙∈A. P x ⟹ (⋀x. x❙∈A ⟹ P x ⟹ Q) ⟹ Q"
  by (unfold HBex_def) blast

lemma hball_triv [simp]: "(∀x❙∈A. P) = ((∃x. x❙∈A) ⟶ P)"
  ― ‹trivial rewrite rule.›
  by (simp add: HBall_def)

lemma hbex_triv [simp]: "(∃x❙∈A. P) = ((∃x. x❙∈A) ∧ P)"
  ― ‹Dual form for existentials.›
  by (simp add: HBex_def)

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)
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