# Theory OrdArith

```chapter ‹Addition, Sequences and their Concatenation›

theory OrdArith imports Rank
begin

section ‹Generalised Addition --- Also for Ordinals›
text ‹Source: Laurence Kirby, Addition and multiplication of sets
Math. Log. Quart. 53, No. 1, 52-65 (2007) / DOI 10.1002/malq.200610026
@{url "http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf"}›

definition
hadd      :: "hf ⇒ hf ⇒ hf"           (infixl "@+" 65)  where
"hadd x ≡ hmemrec (λf z. x ⊔ RepFun z f)"

lemma hadd: "x @+ y = x ⊔ RepFun y (λz. x @+ z)"
by (metis def_hmemrec RepFun_ecut hadd_def order_refl)

assumes l: "l ❙∈ x @+ y"
obtains "l ❙∈ x" | z where "z ❙∈ y" "l = x @+ z"
using l by (auto simp: hadd [of x y])

lemma hadd_0_right [simp]: "x @+ 0 = x"

lemma hadd_hinsert_right: "x @+ hinsert y z = hinsert (x @+ y) (x @+ z)"

lemma hadd_succ_right [simp]: "x @+ succ y = succ (x @+ y)"

lemma not_add_less_right: "¬ (x @+ y < x)"
proof (induction y)
case (2 y1 y2)
then show ?case
using hadd less_supI1 order_less_le by blast
qed auto

lemma not_add_mem_right: "¬ (x @+ y ❙∈ x)"

lemma hadd_0_left [simp]: "0 @+ x = x"
by (induct x) (auto simp: hadd_hinsert_right)

lemma hadd_succ_left [simp]: "Ord y ⟹ succ x @+ y = succ (x @+ y)"
by (induct y rule: Ord_induct2) auto

lemma hadd_assoc: "(x @+ y) @+ z = x @+ (y @+ z)"
by (induct z) (auto simp: hadd_hinsert_right)

lemma RepFun_hadd_disjoint: "x ⊓ RepFun y ((@+) x) = 0"
by (metis hf_equalityI RepFun_iff hinter_iff not_add_mem_right hmem_hempty)

lemma Rep_le_Cancel: "x ⊔ RepFun y ((@+) x) ≤ x ⊔ RepFun z ((@+) x)
⟹ RepFun y ((@+) x) ≤ RepFun z ((@+) x)"

lemma hadd_cancel_right [simp]: "x @+ y = x @+ z ⟷ y=z"
proof (induct y arbitrary: z rule: hmem_induct)
case (step y z) show ?case
proof auto
assume eq: "x @+ y = x @+ z"
hence  "RepFun y ((@+) x) = RepFun z ((@+) x)"
by (metis hadd Rep_le_Cancel order_antisym order_refl)
thus  "y = z"
by (metis hf_equalityI RepFun_iff step)
qed
qed

lemma RepFun_hadd_cancel: "RepFun y (λz. x @+ z) = RepFun z (λz. x @+ z) ⟷ y=z"

lemma hadd_hmem_cancel [simp]: "x @+ y ❙∈ x @+ z ⟷ y ❙∈ z"

lemma ord_of_add: "ord_of (i+j) = ord_of i @+ ord_of j"
by (induct j) auto

lemma Ord_hadd: "Ord x ⟹ Ord y ⟹ Ord (x @+ y)"
by (induct x rule: Ord_induct2) auto

lemma hmem_self_hadd [simp]: "k1 ❙∈ k1 @+ k2 ⟷ 0 ❙∈ k2"

lemma hadd_commute: "Ord x ⟹ Ord y ⟹ x @+ y = y @+ x"
by (induct x rule: Ord_induct2) auto

lemma hadd_cancel_left [simp]: "Ord x ⟹ y @+ x = z @+ x ⟷ y=z"
by (induct x rule: Ord_induct2) auto

subsection ‹The predecessor function›

definition pred :: "hf ⇒ hf"
where "pred x ≡ (THE y. succ y = x ∨ x=0 ∧ y=0)"

lemma pred_succ [simp]: "pred (succ x) = x"

lemma pred_0 [simp]: "pred 0 = 0"

lemma succ_pred [simp]: "Ord x ⟹ x ≠ 0 ⟹ succ (pred x) = x"
by (metis Ord_cases pred_succ)

lemma pred_mem [simp]: "Ord x ⟹ x ≠ 0 ⟹ pred x ❙∈ x"
by (metis succ_iff succ_pred)

lemma Ord_pred [simp]: "Ord x ⟹ Ord (pred x)"
by (metis Ord_in_Ord pred_0 pred_mem)

lemma hadd_pred_right: "Ord y ⟹ y ≠ 0 ⟹ x @+ pred y = pred (x @+ y)"

lemma Ord_pred_HUnion: "Ord(k) ⟹ pred k = ⨆k"
by (metis HUnion_hempty Ordinal.Ord_pred pred_0 pred_succ)

section ‹A Concatentation Operation for Sequences›

definition shift :: "hf ⇒ hf ⇒ hf"
where "shift f delta = ⦃v . u ❙∈ f, ∃n y. u = ⟨n, y⟩ ∧ v = ⟨delta @+ n, y⟩⦄"

lemma shiftD: "x ❙∈ shift f delta ⟹ ∃u. u ❙∈ f ∧ x = ⟨delta @+ hfst u, hsnd u⟩"
by (auto simp: shift_def hsplit_def)

lemma hmem_shift_iff: "⟨m, y⟩ ❙∈ shift f delta ⟷ (∃n. m = delta @+ n ∧ ⟨n, y⟩ ❙∈ f)"
by (auto simp: shift_def hrelation_def is_hpair_def)

lemma hmem_shift_add_iff [simp]: "⟨delta @+ n, y⟩ ❙∈ shift f delta ⟷ ⟨n, y⟩ ❙∈ f"

lemma hrelation_shift [simp]: "hrelation (shift f delta)"
by (auto simp: shift_def hrelation_def hsplit_def)

lemma app_shift [simp]: "app (shift f k) (k @+ j) = app f j"

lemma hfunction_shift_iff [simp]: "hfunction (shift f delta) = hfunction f"
by (auto simp: hfunction_def hmem_shift_iff)

lemma hdomain_shift_add: "hdomain (shift f delta) = ⦃delta @+ n . n ❙∈ hdomain f⦄"
by  (rule hf_equalityI) (force simp add: hdomain_def hmem_shift_iff)

lemma hdomain_shift_disjoint: "delta ⊓ hdomain (shift f delta) = 0"

definition seq_append :: "hf ⇒ hf ⇒ hf ⇒ hf"
where "seq_append k f g ≡ hrestrict f k ⊔ shift g k"

lemma hrelation_seq_append [simp]: "hrelation (seq_append k f g)"

lemma Seq_append:
assumes "Seq s1 k1" "Seq s2 k2"
shows "Seq (seq_append k1 s1 s2) (k1 @+ k2)"
proof -
have "hfunction (hrestrict s1 k1 ⊔ shift s2 k1)"
using assms
by (simp add: Ordinal.Seq_def hdomain_shift_disjoint hfunction_hunion hfunction_restr inf.absorb2)
moreover
have "⋀x. ⟦x ❙∈ k1 @+ k2; x ❙∉ hdomain (shift s2 k1)⟧ ⟹ x ❙∈ hdomain s1 ∧ x ❙∈ k1"
ultimately show ?thesis
by (auto simp: Seq_def seq_append_def)
qed

lemma app_hunion1: "x ❙∉ hdomain g ⟹ app (f ⊔ g) x = app f x"
by (auto simp: app_def) (metis hdomainI)

lemma app_hunion2: "x ❙∉ hdomain f ⟹ app (f ⊔ g) x = app g x"
by (auto simp: app_def) (metis hdomainI)

lemma Seq_append_app1: "Seq s k ⟹ l ❙∈ k ⟹ app (seq_append k s s') l = app s l"
by (metis app_hrestrict app_hunion1 hdomain_shift_disjoint hemptyE hinter_iff seq_append_def)

lemma Seq_append_app2: "Seq s1 k1 ⟹ Seq s2 k2 ⟹ l = k1 @+ j ⟹ app (seq_append k1 s1 s2) l = app s2 j"
by (metis seq_append_def app_hunion2 app_shift hdomain_restr hinter_iff not_add_mem_right)

section ‹Nonempty sequences indexed by ordinals›

definition OrdDom where
"OrdDom r ≡ ∀x y. ⟨x,y⟩ ❙∈ r ⟶ Ord x"

lemma OrdDom_insf: "⟦OrdDom s; Ord k⟧ ⟹ OrdDom (insf s (succ k) y)"
by (auto simp: insf_def OrdDom_def)

lemma OrdDom_hunion [simp]: "OrdDom (s1 ⊔ s2) ⟷ OrdDom s1 ∧ OrdDom s2"
by (auto simp: OrdDom_def)

lemma OrdDom_hrestrict: "OrdDom s ⟹ OrdDom (hrestrict s A)"
by (auto simp: OrdDom_def)

lemma OrdDom_shift: "⟦OrdDom s; Ord k⟧ ⟹ OrdDom (shift s k)"
by (auto simp: OrdDom_def shift_def Ord_hadd)

text ‹A sequence of positive length ending with @{term y}›
definition LstSeq :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "LstSeq s k y ≡ Seq s (succ k) ∧ Ord k ∧ ⟨k,y⟩ ❙∈ s ∧ OrdDom s"

lemma LstSeq_imp_Seq_succ: "LstSeq s k y ⟹ Seq s (succ k)"
by (metis LstSeq_def)

lemma LstSeq_imp_Seq_same: "LstSeq s k y ⟹ Seq s k"
by (metis LstSeq_imp_Seq_succ Seq_succ_D)

lemma LstSeq_imp_Ord: "LstSeq s k y ⟹ Ord k"
by (metis LstSeq_def)

lemma LstSeq_trunc: "LstSeq s k y ⟹ l ❙∈ k ⟹ LstSeq s l (app s l)"
by (meson LstSeq_def Ord_in_Ord Seq_Ord_D Seq_iff_app Seq_succ_iff)

lemma LstSeq_insf: "LstSeq s k z ⟹ LstSeq (insf s (succ k) y) (succ k) y"
using LstSeq_def OrdDom_insf Seq_insf insf_def by force

lemma app_insf_LstSeq: "LstSeq s k z ⟹ app (insf s (succ k) y) (succ k) = y"
by (metis LstSeq_imp_Seq_succ app_insf_Seq)

lemma app_insf2_LstSeq: "LstSeq s k z ⟹ k' ≠ succ k ⟹ app (insf s (succ k) y) k' = app s k'"
by (metis LstSeq_imp_Seq_succ app_insf2_Seq)

lemma app_insf_LstSeq_if: "LstSeq s k z ⟹ app (insf s (succ k) y) k' = (if k' = succ k then y else app s k')"
by (metis app_insf2_LstSeq app_insf_LstSeq)

lemma LstSeq_append_app1:
"LstSeq s k y ⟹ l ❙∈ succ k ⟹ app (seq_append (succ k) s s') l = app s l"
by (metis LstSeq_imp_Seq_succ Seq_append_app1)

lemma LstSeq_append_app2:
"⟦LstSeq s1 k1 y1; LstSeq s2 k2 y2; l = succ k1 @+ j⟧
⟹ app (seq_append (succ k1) s1 s2) l = app s2 j"
by (metis LstSeq_imp_Seq_succ Seq_append_app2)

lemma Seq_append_pair:
"⟦Seq s1 k1; Seq s2 (succ n);  ⟨n, y⟩ ❙∈ s2; Ord n⟧ ⟹ ⟨k1 @+ n, y⟩ ❙∈ (seq_append k1 s1 s2)"

lemma Seq_append_OrdDom: "⟦Ord k; OrdDom s1; OrdDom s2⟧ ⟹ OrdDom (seq_append k s1 s2)"
by (auto simp: seq_append_def OrdDom_hrestrict OrdDom_shift)

lemma LstSeq_append:
"⟦LstSeq s1 k1 y1; LstSeq s2 k2 y2⟧ ⟹ LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
using LstSeq_def Ord_hadd Seq_append Seq_append_OrdDom Seq_append_pair by fastforce

lemma LstSeq_app [simp]: "LstSeq s k y ⟹ app s k = y"
by (metis LstSeq_def Seq_imp_eq_app)

subsection ‹Sequence-building operators›

definition Builds :: "(hf ⇒ bool) ⇒ (hf ⇒ hf ⇒ hf ⇒ bool) ⇒ hf ⇒ hf ⇒ bool"
where "Builds B C s l ≡ B (app s l) ∨ (∃m ❙∈ l. ∃n ❙∈ l. C (app s l) (app s m) (app s n))"

definition BuildSeq :: "(hf ⇒ bool) ⇒ (hf ⇒ hf ⇒ hf ⇒ bool) ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "BuildSeq B C s k y ≡ LstSeq s k y ∧ (∀l ❙∈ succ k. Builds B C s l)"

lemma BuildSeqI: "LstSeq s k y ⟹ (⋀l. l ❙∈ succ k ⟹ Builds B C s l) ⟹ BuildSeq B C s k y"

lemma BuildSeq_imp_LstSeq: "BuildSeq B C s k y ⟹ LstSeq s k y"
by (metis BuildSeq_def)

lemma BuildSeq_imp_Seq: "BuildSeq B C s k y ⟹ Seq s (succ k)"
by (metis LstSeq_imp_Seq_succ BuildSeq_imp_LstSeq)

lemma BuildSeq_conj_distrib:
"BuildSeq (λx. B x ∧ P x) (λx y z. C x y z ∧ P x) s k y ⟷
BuildSeq B C s k y ∧ (∀l ❙∈ succ k. P (app s l))"
by (auto simp: BuildSeq_def Builds_def)

lemma BuildSeq_mono:
assumes y: "BuildSeq B C s k y"
and B: "⋀x. B x ⟹ B' x" and C: "⋀x y z. C x y z ⟹ C' x y z"
shows "BuildSeq B' C' s k y"
using y
by (auto simp: BuildSeq_def Builds_def intro!: B C)

lemma BuildSeq_trunc:
assumes b: "BuildSeq B C s k y"
and l: "l ❙∈ k"
shows "BuildSeq B C s l (app s l)"
by (smt (verit) BuildSeqI BuildSeq_def LstSeq_def LstSeq_trunc Ord_trans b hballE l succ_iff)

subsection ‹Showing that Sequences can be Constructed›

lemma Builds_insf: "Builds B C s l ⟹ LstSeq s k z ⟹ l ❙∈ succ k ⟹ Builds B C (insf s (succ k) y) l"
by (auto simp: HBall_def hmem_not_refl Builds_def app_insf_LstSeq_if simp del: succ_iff)
(metis hmem_not_sym)

lemma BuildSeq_insf:
assumes b: "BuildSeq B C s k z"
and m: "m ❙∈ succ k"
and n: "n ❙∈ succ k"
and y: "B y ∨ C y (app s m) (app s n)"
shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
proof (rule BuildSeqI)
show "LstSeq (insf s (succ k) y) (succ k) y"
by (metis BuildSeq_imp_LstSeq LstSeq_insf b)
next
fix l
assume l: "l ❙∈ succ (succ k)"
thus "Builds B C (insf s (succ k) y) l"
proof
assume l: "l = succ k"
have "B (app (insf s l y) l) ∨ C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)"
by (metis BuildSeq_imp_Seq app_insf_Seq_if b hmem_not_refl l m n y)
thus "Builds B C (insf s (succ k) y) l" using m n
by (auto simp: Builds_def l)
next
assume l: "l ❙∈ succ k"
thus "Builds B C (insf s (succ k) y) l" using b l
by (metis hballE Builds_insf BuildSeq_def)
qed
qed

lemma BuildSeq_insf1:
assumes b: "BuildSeq B C s k z"
and y: "B y"
shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
by (metis BuildSeq_insf b succ_iff y)

lemma BuildSeq_insf2:
assumes b: "BuildSeq B C s k z"
and m: "m ❙∈ k"
and n: "n ❙∈ k"
and y: "C y (app s m) (app s n)"
shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
by (metis BuildSeq_insf b m n succ_iff y)

lemma BuildSeq_append:
assumes s1: "BuildSeq B C s1 k1 y1" and s2: "BuildSeq B C s2 k2 y2"
shows "BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
proof (rule BuildSeqI)
show "LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
using assms
by (metis BuildSeq_imp_LstSeq LstSeq_append)
next
fix l
have s1L: "LstSeq s1 k1 y1"
and s1BC: "⋀l. l ❙∈ succ k1 ⟹ Builds B C s1 l"
and s2L: "LstSeq s2 k2 y2"
and s2BC: "⋀l. l ❙∈ succ k2 ⟹ Builds B C s2 l"
using s1 s2 by (auto simp: BuildSeq_def)
assume l: "l ❙∈ succ (succ (k1 @+ k2))"
hence  "l ❙∈ succ k1 @+ succ k2"
thus "Builds B C (seq_append (succ k1) s1 s2) l"
assume l1: "l ❙∈ succ k1"
hence "B (app s1 l) ∨ (∃m❙∈l. ∃n❙∈l. C (app s1 l) (app s1 m) (app s1 n))" using s1BC
thus ?thesis
proof
assume "B (app s1 l)"
thus ?thesis
by (metis Builds_def LstSeq_append_app1 l1 s1L)
next
assume "∃m❙∈l. ∃n❙∈l. C (app s1 l) (app s1 m) (app s1 n)"
then obtain m n where mn: "m ❙∈ l" "n ❙∈ l" and C: "C (app s1 l) (app s1 m) (app s1 n)"
by blast
moreover have "m ❙∈ succ k1" "n ❙∈ succ k1"
by (metis LstSeq_def Ord_trans l1 mn s1L succ_iff)+
ultimately have "C (app (seq_append (succ k1) s1 s2) l)
(app (seq_append (succ k1) s1 s2) m)
(app (seq_append (succ k1) s1 s2) n)"
using s1L l1
thus "Builds B C (seq_append (succ k1) s1 s2) l" using mn
by (auto simp: Builds_def)
qed
next
fix z
assume z: "z ❙∈ succ k2" and l2: "l = succ k1 @+ z"
hence "B (app s2 z) ∨ (∃m❙∈z. ∃n❙∈z. C (app s2 z) (app s2 m) (app s2 n))" using s2BC
thus ?thesis
proof
assume "B (app s2 z)"
thus ?thesis
by (metis Builds_def LstSeq_append_app2 l2 s1L s2L)
next
assume "∃m❙∈z. ∃n❙∈z. C (app s2 z) (app s2 m) (app s2 n)"
then obtain m n where mn: "m ❙∈ z" "n ❙∈ z" and C: "C (app s2 z) (app s2 m) (app s2 n)"
by blast
also have "m ❙∈ succ k2" "n ❙∈ succ k2" using mn
by (metis LstSeq_def Ord_trans z s2L succ_iff)+
ultimately have "C (app (seq_append (succ k1) s1 s2) l)
(app (seq_append (succ k1) s1 s2) (succ k1 @+ m))
(app (seq_append (succ k1) s1 s2) (succ k1 @+ n))"
using s1L s2L l2 z
thus "Builds B C (seq_append (succ k1) s1 s2) l" using mn l2
by (auto simp: Builds_def HBall_def)
qed
qed
qed

lemma BuildSeq_combine:
assumes b1: "BuildSeq B C s1 k1 y1" and b2: "BuildSeq B C s2 k2 y2"
and y: "C y y1 y2"
shows "BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y"
proof -
have k2: "Ord k2"  using b2
by (auto simp: BuildSeq_def LstSeq_def)
show ?thesis
proof (rule BuildSeq_insf [where m=k1 and n="succ(k1@+k2)"])
show "BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
by (rule BuildSeq_append [OF b1 b2])
next
show "k1 ❙∈ succ (succ (k1 @+ k2))" using k2
next
show "succ (k1 @+ k2) ❙∈ succ (succ (k1 @+ k2))"
by (metis succ_iff)
next
have [simp]: "app (seq_append (succ k1) s1 s2) k1 = y1"
by (metis b1 BuildSeq_imp_LstSeq LstSeq_app LstSeq_append_app1 succ_iff)
have [simp]: "app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) = y2"
by (metis b1 b2 k2 BuildSeq_imp_LstSeq LstSeq_app LstSeq_append_app2 hadd_succ_left)
show "B y ∨
C y (app (seq_append (succ k1) s1 s2) k1)
(app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))"
using y by simp
qed
qed

lemma LstSeq_1: "LstSeq ⦃⟨0, y⟩⦄ 0 y"
by (auto simp: LstSeq_def One_hf_eq_succ Seq_ins OrdDom_def)

lemma BuildSeq_1: "B y ⟹ BuildSeq B C ⦃⟨0, y⟩⦄ 0 y"
by (auto simp: BuildSeq_def Builds_def LstSeq_1)

lemma BuildSeq_exI: "B t ⟹ ∃s k. BuildSeq B C s k t"
by (metis BuildSeq_1)

subsection ‹Proving Properties of Given Sequences›

lemma BuildSeq_succ_E:
assumes s: "BuildSeq B C s k y"
obtains "B y" |  m n where "m ❙∈ k" "n ❙∈ k" "C y (app s m) (app s n)"
proof -
have Bs: "Builds B C s k" and apps: "app s k = y" using s
by (auto simp: BuildSeq_def)
hence "B y ∨ (∃m ❙∈ k. ∃n ❙∈ k. C y (app s m) (app s n))"
by (metis Builds_def apps Bs)
thus ?thesis using that
by auto
qed

lemma BuildSeq_induct [consumes 1, case_names B C]:
assumes major: "BuildSeq B C s k a"
and B: "⋀x. B x ⟹ P x"
and C: "⋀x y z. C x y z ⟹ P y ⟹ P z ⟹ P x"
shows "P a"
proof -
have "Ord k" using assms
by (auto simp: BuildSeq_def LstSeq_def)
hence "⋀a s. BuildSeq B C s k a ⟹ P a"
by (induction k rule: Ord_induct) (metis BuildSeq_trunc BuildSeq_succ_E B C)
thus ?thesis
by (metis major)
qed

definition BuildSeq2 :: "[[hf,hf] ⇒ bool, [hf,hf,hf,hf,hf,hf] ⇒ bool, hf, hf, hf, hf] ⇒ bool"
where "BuildSeq2 B C s k y y' ≡
BuildSeq (λp. ∃x x'. p = ⟨x,x'⟩ ∧ B x x')
(λp q r. ∃x x' y y' z z'. p = ⟨x,x'⟩ ∧ q = ⟨y,y'⟩ ∧ r = ⟨z,z'⟩ ∧ C x x' y y' z z')
s k ⟨y,y'⟩"

lemma BuildSeq2_combine:
assumes b1: "BuildSeq2 B C s1 k1 y1 y1'" and b2: "BuildSeq2 B C s2 k2 y2 y2'"
and y: "C y y' y1 y1' y2 y2'"
shows "BuildSeq2 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) ⟨y, y'⟩)
(succ (succ (k1 @+ k2))) y y'"
using BuildSeq2_def BuildSeq_combine b1 b2 y by force

lemma BuildSeq2_1: "B y y' ⟹ BuildSeq2 B C ⦃⟨0, y, y'⟩⦄ 0 y y'"
by (auto simp: BuildSeq2_def BuildSeq_1)

lemma BuildSeq2_exI: "B t t' ⟹ ∃s k. BuildSeq2 B C s k t t'"
by (metis BuildSeq2_1)

lemma BuildSeq2_induct [consumes 1, case_names B C]:
assumes "BuildSeq2 B C s k a a'"
and B: "⋀x x'. B x x' ⟹ P x x'"
and C: "⋀x x' y y' z z'. C x x' y y' z z' ⟹ P y y' ⟹ P z z' ⟹ P x x'"
shows "P a a'"
using assms BuildSeq_induct [where P = "λ⟨x,x'⟩. P x x'"]
by (smt (verit, del_insts) BuildSeq2_def hsplit)

definition BuildSeq3
:: "[[hf,hf,hf] ⇒ bool, [hf,hf,hf,hf,hf,hf,hf,hf,hf] ⇒ bool, hf, hf, hf, hf, hf] ⇒ bool"
where "BuildSeq3 B C s k y y' y'' ≡
BuildSeq (λp. ∃x x' x''. p = ⟨x,x',x''⟩ ∧ B x x' x'')
(λp q r. ∃x x' x'' y y' y'' z z' z''.
p = ⟨x,x',x''⟩ ∧ q = ⟨y,y',y''⟩ ∧ r = ⟨z,z',z''⟩ ∧
C x x' x'' y y' y'' z z' z'')
s k ⟨y,y',y''⟩"

lemma BuildSeq3_combine:
assumes b1: "BuildSeq3 B C s1 k1 y1 y1' y1''" and b2: "BuildSeq3 B C s2 k2 y2 y2' y2''"
and y: "C y y' y'' y1 y1' y1'' y2 y2' y2''"
shows "BuildSeq3 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) ⟨y, y', y''⟩)
(succ (succ (k1 @+ k2))) y y' y''"
using assms
unfolding BuildSeq3_def by (blast intro: BuildSeq_combine)

lemma BuildSeq3_1: "B y y' y'' ⟹ BuildSeq3 B C ⦃⟨0, y, y', y''⟩⦄ 0 y y' y''"
by (auto simp: BuildSeq3_def BuildSeq_1)

lemma BuildSeq3_exI: "B t t' t'' ⟹ ∃s k. BuildSeq3 B C s k t t' t''"
by (metis BuildSeq3_1)

lemma BuildSeq3_induct [consumes 1, case_names B C]:
assumes "BuildSeq3 B C s k a a' a''"
and B: "⋀x x' x''. B x x' x'' ⟹ P x x' x''"
and C: "⋀x x' x'' y y' y'' z z' z''. C x x' x'' y y' y'' z z' z'' ⟹ P y y' y'' ⟹ P z z' z'' ⟹ P x x' x''"
shows "P a a' a''"
using assms BuildSeq_induct [where P = "λ⟨x,x',x''⟩. P x x' x''"]
by (smt (verit, del_insts) BuildSeq3_def hsplit)

section ‹A Unique Predecessor for every non-empty set›

lemma Rep_hf_0 [simp]: "Rep_hf 0 = 0"
by (metis Abs_hf_inverse HF.HF_def UNIV_I Zero_hf_def image_empty set_encode_empty)

lemma hmem_imp_less: "x ❙∈ y ⟹ Rep_hf x < Rep_hf y"
unfolding hmem_def hfset_def image_iff
apply (clarsimp simp: hmem_def hfset_def set_decode_def Abs_hf_inverse)
apply (metis div_less even_zero le_less_trans less_exp not_less)
done

lemma hsubset_imp_le:
assumes "x ≤ y" shows "Rep_hf x ≤ Rep_hf y"
proof -
have "⋀u v. ⟦∀x. x ∈ Abs_hf ` set_decode (Rep_hf (Abs_hf u)) ⟶
x ∈ Abs_hf ` set_decode (Rep_hf (Abs_hf v))⟧
⟹ u ≤ v"
by (metis Abs_hf_inverse UNIV_I imageE image_eqI subsetI subset_decode_imp_le)
then show ?thesis
by (metis Rep_hf_inverse assms hfset_def hmem_def hsubsetCE)
qed

lemma diff_hmem_imp_less: assumes "x ❙∈ y" shows "Rep_hf (y - ⦃x⦄) < Rep_hf y"
proof -
have  "Rep_hf (y - ⦃x⦄) ≤ Rep_hf y"
by (metis hdiff_iff hsubsetI hsubset_imp_le)
moreover
have "Rep_hf (y - ⦃x⦄) ≠ Rep_hf y" using assms
by (metis Rep_hf_inject hdiff_iff hinsert_iff)
ultimately show ?thesis
by (metis le_neq_implies_less)
qed

definition least :: "hf ⇒ hf"
where "least a ≡ (THE x. x ❙∈ a ∧ (∀y. y ❙∈ a ⟶ Rep_hf x ≤ Rep_hf y))"

lemma least_equality:
assumes "x ❙∈ a" and "⋀y. y ❙∈ a ⟹ Rep_hf x ≤ Rep_hf y"
shows "least a = x"
unfolding least_def
using Rep_hf_inject assms order_antisym_conv by blast

lemma leastI2_order:
assumes "x ❙∈ a"
and "⋀y. y ❙∈ a ⟹ Rep_hf x ≤ Rep_hf y"
and "⋀z. z ❙∈ a ⟹ ∀y. y ❙∈ a ⟶ Rep_hf z ≤ Rep_hf y ⟹ Q z"
shows "Q (least a)"
by (metis assms least_equality)

lemma nonempty_imp_ex_least: "a ≠ 0 ⟹ ∃x. x ❙∈ a ∧ (∀y. y ❙∈ a ⟶ Rep_hf x ≤ Rep_hf y)"
proof (induction a rule: hf_induct)
case 0 thus ?case by simp
next
case (hinsert u v)
show ?case
proof (cases "v=0")
case True thus ?thesis
by (rule_tac x=u in exI, simp)
next
case False
thus ?thesis
by (metis order.trans hinsert.IH(2) hmem_hinsert linorder_le_cases)
qed
qed

lemma least_hmem: "a ≠ 0 ⟹ least a ❙∈ a"
by (metis least_equality nonempty_imp_ex_least)

end
```