Theory HereditarilyFinite.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)

lemma hmem_hadd_E:
  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"
  by (subst hadd) simp

lemma hadd_hinsert_right: "x @+ hinsert y z = hinsert (x @+ y) (x @+ z)"
  by (metis hadd hunion_hinsert_right RepFun_hinsert)

lemma hadd_succ_right [simp]: "x @+ succ y = succ (x @+ y)"
  by (metis hadd_hinsert_right succ_def)

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)"
  by (metis hadd hmem_not_refl hunion_iff)

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)


subsection ‹Cancellation laws for addition›

lemma Rep_le_Cancel: "x ⊔ RepFun y ((@+) x) ≤ x ⊔ RepFun z ((@+) x)
                      ⟹ RepFun y ((@+) x) ≤ RepFun z ((@+) x)"
  by (auto simp add: not_add_mem_right)

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"
  by (metis hadd hadd_cancel_right)

lemma hadd_hmem_cancel [simp]: "x @+ y ❙∈ x @+ z ⟷ y ❙∈ z"
  by (metis RepFun_iff hadd hadd_cancel_right hunion_iff not_add_mem_right)

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"
  by (metis hadd_0_right hadd_hmem_cancel)

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"
  by (simp add: pred_def)

lemma pred_0 [simp]: "pred 0 = 0"
  by (simp add: pred_def)

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)"
  by (metis hadd_succ_right pred_succ succ_pred)

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"
  by (metis hadd_cancel_right hmem_shift_iff)

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"
  by (simp add: app_def)

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"
  by (simp add: RepFun_hadd_disjoint hdomain_shift_add)

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)"
  by (simp add: seq_append_def)

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"
    by (metis Ordinal.Seq_def RepFun_iff assms hdomain_shift_add hmem_hadd_E hsubsetCE)
  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)"
  by (metis hmem_shift_add_iff hunion_iff seq_append_def)

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"
  by (simp add: BuildSeq_def)

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"
    by (metis LstSeq_imp_Ord hadd_succ_left hadd_succ_right s2L)
  thus "Builds B C (seq_append (succ k1) s1 s2) l"
  proof (rule hmem_hadd_E)
    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
      by (simp add: Builds_def)
    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
        by (simp add: LstSeq_append_app1)
      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
      by (simp add: Builds_def)
    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
        by (simp add: LstSeq_append_app2)
      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
      by (metis hadd_0_right hmem_0_Ord hmem_self_hadd succ_iff)
  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