Theory 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"

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

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

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"   ("⟨_,/ _⟩")
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"

lemma hsnd_conv [simp]: "hsnd ⟨a,b⟩ = b"

lemma hsplit [simp]: "hsplit c ⟨a,b⟩ = c a b"

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

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"

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

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"

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"

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

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

lemma hbspec [dest?]: "∀x❙∈A. P x ⟹ x❙∈A ⟹ P x"

lemma hballE [elim]: "∀x❙∈A. P x ⟹ (P x ⟹ Q) ⟹ (x ❙∉ A ⟹ Q) ⟹ Q"

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"

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"

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

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

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"

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'"

lemma hfunction_0 [simp]: "hfunction 0"

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"

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

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

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"

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"

lemma Inr_iff [iff]: "Inr(a)=Inr(b) ⟷ a=b"

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

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

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"

lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"

lemma sum_case_non [simp]: "¬ is_hsum a ⟹ sum_case f g a = undefined"

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