Theory Energy_Order

section ‹Vectors of (extended) Naturals as Energies›

theory Energy_Order
  imports Main List_Lemmas "HOL-Library.Extended_Nat" Well_Quasi_Orders.Well_Quasi_Orders
begin

text ‹
We consider vectors with entries in the extended naturals as energies and fix a dimension later. 
In this theory we introduce the component-wise order on energies (represented as lists of enats) 
as well as a minimum and supremum.
›

type_synonym energy = "enat list"

definition energy_leq:: "energy ⇒ energy ⇒ bool" (infix "e≤" 80) where 
  "energy_leq e e' = ((length e = length e') 
                      ∧ (∀i < length e. (e ! i) ≤ (e' ! i)))"

abbreviation energy_l:: "energy ⇒ energy ⇒ bool" (infix "e<" 80) where 
  "energy_l e e' ≡  e e≤ e' ∧ e ≠ e'"

text‹We now establish that ‹energy_leg› is a partial order.›

interpretation energy_leq: ordering "energy_leq" "energy_l"
proof
  fix e e' e''
  show "e e≤ e" using energy_leq_def by simp
  show "e e≤ e' ⟹ e' e≤ e'' ⟹ e e≤ e''" using energy_leq_def by fastforce 
  show "e e< e' = e e< e'" by simp
  show "e e≤ e' ⟹ e' e≤ e ⟹ e = e'" using energy_leq_def
    by (metis (no_types, lifting) nth_equalityI order_antisym_conv)
qed

text‹ 
We now show that it is well-founded when considering a fixed dimension ‹n›. 
For the proof we define the subsequence of a given sequence of energies such that the last entry is 
increasing but never equals ‹∞›.›

fun subsequence_index::"(nat ⇒ energy) ⇒ nat ⇒ nat" where
  "subsequence_index f 0 = (SOME x. (last (f x) ≠ ∞))" | 
  "subsequence_index f (Suc n) = (SOME x. (last (f x) ≠ ∞ 
            ∧ (subsequence_index f n) < x 
            ∧ (last (f (subsequence_index f n)) ≤ last (f x))))"

lemma energy_leq_wqo: 
  shows "wqo_on energy_leq {e::energy. length e = n}"
proof
  show "transp_on {e. length e = n} (e≤)"
    by (metis energy_leq.trans transp_onI)
  show "almost_full_on (e≤) {e::energy. length e = n}" 
  proof(induct n)
    case 0
    then show ?case
      by (smt (verit, del_insts) almost_full_onI energy_leq.refl good_def length_0_conv mem_Collect_eq zero_less_Suc)
  next
    case (Suc n)
    hence allF: "∀f ∈ SEQ {e::energy. length e = n}. (∃i j. i < j ∧ (f i) e≤ (f j))" 
      unfolding almost_full_on_def good_def by simp

    have "{e::energy. length e = Suc n} = {e@[x]|e x::enat. e ∈ {e::energy. length e = n}}"
      using length_Suc_conv_rev by auto
    show ?case 
    proof
      fix f (* f:: nat ⇒ {e. length e = Suc n} ist folge von energies*)
      show "∀i. f i ∈ {e::energy. length e = Suc n} ⟹ good (e≤) f" 
      proof-
        assume "∀i. f i ∈ {e::energy. length e = Suc n}"
        show "good (e≤) f" unfolding good_def proof-
          show "∃i j. i < j ∧ f i e≤ f j" 
          proof(cases "finite {i::nat. (f i) ! n = ∞}")
            case True 
            define upbound where "upbound = Sup {(f i) ! n| i::nat. (f i) ! n ≠ ∞}" (* betrachte teilfolge ohne unendlich *)
            then show ?thesis 
            proof(cases "upbound = ∞")
              case True (* dann existiert eine steigende Teilfolge, wende induktionshyps darauf an *)
              have exist: "⋀i. (f i) ! n ≠ ∞ ⟹ ∃j. i < j ∧ (f j) ! n ≠ ∞ ∧ (f i) ! n ≤ (f j) ! n"
              proof-
                fix i 
                assume "(f i) ! n ≠ ∞"
                have "¬(∃j. i < j ∧ (f j) ! n ≠ ∞ ∧(f i) ! n ≤ (f j) ! n) ⟹ False"
                proof-
                  assume "¬(∃j. i < j ∧ (f j) ! n ≠ ∞ ∧ (f i) ! n ≤ (f j) ! n)"
                  hence A: "⋀j. i < j ⟹ (f j) ! n = ∞ ∨ (f i) ! n > (f j) ! n" by auto

                  define max_value where "max_value = Max {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}"
                  have "⋀k. (f k) ! n ≠ ∞ ⟹(f k) ! n ≤ max_value" 
                  proof-
                    fix k 
                    assume not_inf: "(f k) ! n ≠ ∞"
                    show "(f k) ! n ≤ max_value" 
                    proof(cases "k ≤ i")
                      case True
                      hence "(f k) ! n ∈ {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}" using not_inf  by auto              
                      then show ?thesis using Max_ge ‹(f k) ! n ∈ {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}› max_value_def by auto
                    next
                      case False
                      hence "(f k) ! n < (f i) ! n" using A not_inf
                        by (meson leI)
                      have "(f i) ! n ∈ {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}" using ‹(f i) ! n ≠ ∞› by auto 
                      hence "(f i) ! n ≤ max_value" using Max_ge max_value_def by auto
                      then show ?thesis using ‹(f k) ! n < (f i) ! n› by auto
                    qed
                  qed

                  hence "upbound = max_value" using upbound_def
                    by (smt (verit) Sup_least True antisym enat_ord_code(3) mem_Collect_eq)

                  have " (f i)! n ∈ {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}" using ‹(f i) ! n ≠ ∞› by auto
                  hence notempty: "{(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞} ≠ {}" by auto
                  have "finite {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}" by simp
                  hence "max_value ∈ {(f k) ! n| k. k ≤ i ∧ (f k) ! n ≠ ∞}" unfolding max_value_def using Max_in notempty by blast
                  hence "max_value ≠ ∞" using max_value_def by auto
                  hence "upbound ≠ ∞" using ‹upbound = max_value› by simp
                  thus "False" using True by simp
                qed
                thus "∃j. i < j ∧ (f j) ! n ≠ ∞ ∧(f i) ! n ≤ (f j) ! n"
                  by blast 
              qed

              define f' where "f' ≡ λi. butlast (f (subsequence_index f i))"
              
              have "f' ∈ SEQ {e::energy. length e = n}" 
              proof
                show "∀i. f' i ∈ {e. length e = n}"
                proof
                  fix i 
                  have "(f (subsequence_index f i)) ∈ {e. length e = Suc n}" using ‹∀i. f i ∈ {e::energy. length e = Suc n}›
                    by simp 
                  thus "f' i ∈ {e. length e = n}" 
                    using f'_def by auto
                qed
              qed
              hence "(∃i j. i < j ∧ (f' i) e≤ (f' j))" 
                using allF by simp
              from this obtain i j where ij: "i < j ∧ (f' i) e≤ (f' j)" by auto
              hence le: "butlast (f (subsequence_index f i)) e≤ butlast (f (subsequence_index f j))" using f'_def by simp

              have last: "⋀x. last (f x) = (f x) ! n" using last_len
                using ‹∀i. f i ∈ {e. length e = Suc n}› by auto 
              have "{x. (last (f x) ≠ ∞)} ≠ {}" 
              proof
                assume "{x. last (f x) ≠ ∞} = {}"
                hence "⋀x. last (f x) = ∞" by auto
                hence "⋀x. (f x) ! n = ∞" using ‹⋀x. last (f x) = (f x) ! n› by auto
                thus "False" using ‹finite {i::nat. (f i) ! n = ∞}› by simp
              qed
              hence subsequence_index_0: "(last (f (subsequence_index f 0)) ≠ ∞)" 
                using subsequence_index.simps(1)
                by (metis (mono_tags, lifting) Collect_empty_eq some_eq_imp)

              have subsequence_index_Suc: "⋀m. (last (f (subsequence_index f (Suc m))) ≠ ∞ ∧ (subsequence_index f m) < (subsequence_index f (Suc m)) ∧ (last (f (subsequence_index f m)) ≤ last (f (subsequence_index f (Suc m)))))"
              proof-
                fix m 
                have some: "subsequence_index f (Suc m) = (SOME x. last (f x) ≠ ∞ ∧ subsequence_index f m < x ∧ last (f (subsequence_index f m)) ≤ last (f x))" using subsequence_index.simps(2) by auto
                show "(last (f (subsequence_index f (Suc m))) ≠ ∞ ∧ (subsequence_index f m) < (subsequence_index f (Suc m)) ∧ (last (f (subsequence_index f m)) ≤ last (f (subsequence_index f (Suc m)))))" 
                proof(induct m)
                  case 0
                  have "{x. last (f x) ≠ ∞ ∧ subsequence_index f 0 < x ∧ last (f (subsequence_index f 0)) ≤ last (f x)} ≠ {}"
                    unfolding last using subsequence_index_0 exist
                    by (simp add: last)
                  then show ?case using some some_eq_ex
                    by (smt (z3) empty_Collect_eq subsequence_index.simps(2))
                next
                  case (Suc m)
                  hence "{x. last (f x) ≠ ∞ ∧ subsequence_index f (Suc m) < x ∧ last (f (subsequence_index f (Suc m))) ≤ last (f x)} ≠ {}"
                    unfolding last using exist by simp
                  then show ?case using some some_eq_ex 
                    by (smt (z3) empty_Collect_eq subsequence_index.simps(2))
                qed
              qed
              hence "⋀i j. i < j ⟹ subsequence_index f i < subsequence_index f j"
                by (simp add: lift_Suc_mono_less) 
              hence "subsequence_index f i < subsequence_index f j" using ‹i < j ∧ (f' i) e≤ (f' j)› by simp

              have "⋀i j. i < j ⟹ last (f (subsequence_index f i)) ≤ last (f (subsequence_index f j))"
              proof-
                fix i j
                show "i < j ⟹ last (f (subsequence_index f i)) ≤ last (f (subsequence_index f j))"
                proof-
                  assume "i < j"
                  show "last (f (subsequence_index f i)) ≤ last (f (subsequence_index f j))" using ‹i < j› 
                  proof(induct "j-i" arbitrary: i j)
                    case 0
                    then show ?case by simp
                  next
                    case (Suc x)
                    then show ?case 
                    proof(cases "x = 0")
                      case True
                      hence "j = Suc i" using Suc
                        by (simp add: Nat.lessE Suc_pred diff_diff_cancel) 
                      then show ?thesis using subsequence_index_Suc by simp
                    next
                      case False
                      hence "∃x'. x = Suc x'"
                        by (simp add: not0_implies_Suc) 
                      then show ?thesis using Suc subsequence_index_Suc
                        by (smt (verit, ccfv_SIG) Suc_leD diff_Suc_Suc diff_diff_cancel diff_le_self dual_order.strict_trans2 not_less_eq_eq verit_comp_simplify1(3) zero_less_diff)
                    qed
                  qed
                qed
              qed
              hence "(f (subsequence_index f i))!n ≤ (f (subsequence_index f j))!n" using ‹i < j ∧ (f' i) e≤ (f' j)› last by simp

              have "(f (subsequence_index f i)) e≤ (f (subsequence_index f j))" unfolding energy_leq_def 
              proof
                show "length (f (subsequence_index f i)) = length (f (subsequence_index f j))" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                show "∀ia<length (f (subsequence_index f i)). f (subsequence_index f i) ! ia ≤ f (subsequence_index f j) ! ia "
                proof
                  fix ia
                  show "ia < length (f (subsequence_index f i)) ⟶ f (subsequence_index f i) ! ia ≤ f (subsequence_index f j) ! ia"
                  proof
                    assume "ia < length (f (subsequence_index f i))"
                    hence "ia < Suc n" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                    show "f (subsequence_index f i) ! ia ≤ f (subsequence_index f j) ! ia " 
                    proof(cases "ia < n")
                      case True
                      hence "f (subsequence_index f i) ! ia = (butlast (f (subsequence_index f i))) ! ia" using nth_butlast ‹ia < length (f (subsequence_index f i))› ‹∀i. f i ∈ {e::energy. length e = Suc n}›
                        by (metis (mono_tags, lifting) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› f'_def mem_Collect_eq)
                      also have "... ≤ (butlast (f (subsequence_index f j))) ! ia" using le unfolding energy_leq_def using True ‹f' ∈ SEQ {e. length e = n}› f'_def by simp
                      also have "... = f (subsequence_index f j) ! ia" using True nth_butlast ‹ia < length (f (subsequence_index f i))› ‹∀i. f i ∈ {e::energy. length e = Suc n}›
                        by (metis (mono_tags, lifting) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› f'_def mem_Collect_eq)
                      finally show ?thesis .
                    next
                      case False
                      hence "ia = n" using ‹ia < Suc n› by simp
                      then show ?thesis using ‹(f (subsequence_index f i))!n ≤ (f (subsequence_index f j))!n› by simp
                    qed
                  qed
                qed
              qed
              then show ?thesis using ‹subsequence_index f i < subsequence_index f j› by auto
            next
              case False (* dann existiert ein x, sodass {(f i) ! n = x} unendlich ist ⇒ dann analog zu infinite infinity *)
              hence "∃upbound_nat. upbound = enat upbound_nat" by simp
              from this obtain upbound_nat where "upbound = enat upbound_nat" by auto

              have "¬(∃x. infinite {i::nat. (f i) ! n = x}) ⟹ False " 
              proof- 
                assume "¬(∃x. infinite {i::nat. (f i) ! n = x})"
                hence allfinite: "⋀x. x ≤ upbound ⟹ finite {i::nat. (f i) ! n = x}" by auto

                have "⋀k. k ≠ ∞ ⟹ finite {n::enat. n ≤ k}"
                  by (metis finite_enat_bounded mem_Collect_eq not_enat_eq)
                hence "finite ({x. x ≤ upbound} ∪ {∞}) " using False by simp
                hence "finite {{i::nat. (f i) ! n = x}| x. x ≤ upbound ∨ x = ∞}" by simp
                hence union_finite: "finite (⋃ {{i::nat. (f i) ! n = x}| x. x ≤ upbound ∨ x = ∞})" using finite_Union allfinite True by auto

                have "{i::nat. True} = (⋃ {{i::nat. (f i) ! n = x}| x. x ≤ upbound ∨ x = ∞})" 
                proof
                  show "{i. True} ⊆ ⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞}" 
                  proof
                    fix x 
                    show "x ∈ {i. True} ⟹ x ∈ ⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞}"
                    proof-
                      assume  "x ∈ {i. True}"
                      hence "x ∈ {i. f i ! n = f x ! n}" by simp
                      show "x ∈ ⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞}" 
                      proof(cases "f x ! n = ∞")
                        case True
                        thus "x ∈ ⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞}" using ‹x ∈ {i. f i ! n = f x ! n}›
                          by auto
                      next
                        case False
                        hence "f x ! n ≤ upbound" using upbound_def
                          by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq) 
                        thus "x ∈ ⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞}" using ‹x ∈ {i. f i ! n = f x ! n}›
                          by auto
                      qed
                    qed
                  qed
                  show "⋃ {{i. f i ! n = x} |x. x ≤ upbound ∨ x = ∞} ⊆ {i. True}" by simp
                qed
                thus "False" using union_finite by simp
              qed
              hence "∃x. infinite {i::nat. (f i) ! n = x}" by auto
              from this obtain x where inf_x: "infinite {i::nat. (f i) ! n = x}" by auto

              (* Copy Paste case infinite {i::nat. (f i) ! n = ∞} *)
              define f' where "f' ≡ λi. butlast (f (enumerate {i::nat. (f i) ! n = x} i))" (* unendliche Teilfolge mit letzter Eintrag = x, ohne diesen Eintrag*)
              have "∀i. f' i ∈ {e. length e = n}" 
              proof
                fix i
                have "f (enumerate {i::nat. (f i) ! n = x} i) ∈ {e. length e = Suc n}" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                hence "length (f (enumerate {i::nat. (f i) ! n = x} i)) = Suc n" by simp
                hence "length (butlast (f (enumerate {i::nat. (f i) ! n = x} i))) = n" using length_butlast
                  by simp
                hence "butlast (f (enumerate {i::nat. (f i) ! n = x} i)) ∈ {e. length e = n}" by simp
                thus "f' i ∈ {e. length e = n}" using f'_def by simp
              qed
              hence "f' ∈ SEQ {e::energy. length e = n}"
                unfolding SEQ_def by simp
              hence "(∃i j. i < j ∧ (f' i) e≤ (f' j))" 
                using allF by simp
              from this obtain i j where ij: "i < j ∧ (f' i) e≤ (f' j)" by auto
              hence le: "(enumerate {i::nat. (f i) ! n = x} i) < (enumerate {i::nat. (f i) ! n = x} j)" 
                using enumerate_mono inf_x by simp
              have "(f (enumerate {i::nat. (f i) ! n = x} i)) e≤ (f (enumerate {i::nat. (f i) ! n = x} j))" 
                unfolding energy_leq_def 
              proof
                show " length (f (wellorder_class.enumerate {i. f i ! n = x} i)) =
                     length (f (wellorder_class.enumerate {i. f i ! n = x} j))" 
                  using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                show "∀ia<length (f (wellorder_class.enumerate {i. f i ! n = x} i)).
                      f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia
                      ≤ f (wellorder_class.enumerate {i. f i ! n = x} j) ! ia " 
                proof
                  fix ia 
                  show "ia < length (f (wellorder_class.enumerate {i. f i ! n = x} i)) ⟶
                      f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia
                      ≤ f (wellorder_class.enumerate {i. f i ! n = x} j) ! ia" 
                  proof
                    assume "ia < length (f (wellorder_class.enumerate {i. f i ! n = x} i))"
                    hence "ia < Suc n" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                    show "f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia
                        ≤ f (wellorder_class.enumerate {i. f i ! n = x} j) ! ia" 
                    proof(cases "ia < n")
                      case True
                      hence  "f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia = (f' i) ! ia" using f'_def
                        by (smt (verit) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› mem_Collect_eq nth_butlast) 
                      also have "... ≤ (f' j) ! ia" using ij energy_leq_def True ‹f' ∈ SEQ {e. length e = n}›
                        by simp
                      also have "... = f (wellorder_class.enumerate {i. f i ! n = x} j) ! ia" using f'_def True
                        by (smt (verit) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› mem_Collect_eq nth_butlast)
                      finally show ?thesis .
                    next
                      case False
                      hence "ia = n" using ‹ia < Suc n› by simp
                      hence "f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia = x" 
                        using enumerate_in_set ‹infinite {i::nat. (f i) ! n = x}›
                        by auto  
                      hence "f (wellorder_class.enumerate {i. f i ! n = x} i) ! ia = f (wellorder_class.enumerate {i. f i ! n = x} j) ! ia" 
                        using enumerate_in_set ‹infinite {i::nat. (f i) ! n = x}› ‹ia = n›
                        by force 
                      then show ?thesis by simp
                    qed
                  qed
                qed
              qed
              then show ?thesis using le by auto
            qed
          next
            case False (* betrachte teilfolge mit nur unendlich,  wende induktionshyps darauf an *)
            define f' where "f' ≡ λi. butlast (f (enumerate {i::nat. (f i) ! n = ∞} i))" (* unendliche Teilfolge mit letzter Eintrag = ∞, ohne diesen Eintrag*)
            have "∀i. f' i ∈ {e. length e = n}" 
            proof
              fix i
              have "f (enumerate {i::nat. (f i) ! n = ∞} i) ∈ {e. length e = Suc n}" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
              hence "length (f (enumerate {i::nat. (f i) ! n = ∞} i)) = Suc n" by simp
              hence "length (butlast (f (enumerate {i::nat. (f i) ! n = ∞} i))) = n" using length_butlast
                by simp
              hence "butlast (f (enumerate {i::nat. (f i) ! n = ∞} i)) ∈ {e. length e = n}" by simp
              thus "f' i ∈ {e. length e = n}" using f'_def by simp
            qed
            hence "f' ∈ SEQ {e::energy. length e = n}"
              unfolding SEQ_def by simp
            hence "(∃i j. i < j ∧ (f' i) e≤ (f' j))" 
              using allF by simp
            from this obtain i j where ij: "i < j ∧ (f' i) e≤ (f' j)" by auto
            hence le: "(enumerate {i::nat. (f i) ! n = ∞} i) < (enumerate {i::nat. (f i) ! n = ∞} j)" 
              using enumerate_mono False by simp
            have "(f (enumerate {i::nat. (f i) ! n = ∞} i)) e≤ (f (enumerate {i::nat. (f i) ! n = ∞} j))" 
              unfolding energy_leq_def 
            proof
              show " length (f (wellorder_class.enumerate {i. f i ! n = ∞} i)) =
                     length (f (wellorder_class.enumerate {i. f i ! n = ∞} j))" 
                using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
              show "∀ia<length (f (wellorder_class.enumerate {i. f i ! n = ∞} i)).
                      f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia
                      ≤ f (wellorder_class.enumerate {i. f i ! n = ∞} j) ! ia " 
              proof
                fix ia 
                show "ia < length (f (wellorder_class.enumerate {i. f i ! n = ∞} i)) ⟶
                      f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia
                      ≤ f (wellorder_class.enumerate {i. f i ! n = ∞} j) ! ia" 
                proof
                  assume "ia < length (f (wellorder_class.enumerate {i. f i ! n = ∞} i))"
                  hence "ia < Suc n" using ‹∀i. f i ∈ {e::energy. length e = Suc n}› by simp
                  show "f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia
                        ≤ f (wellorder_class.enumerate {i. f i ! n = ∞} j) ! ia" 
                  proof(cases "ia < n")
                    case True
                    hence  "f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia = (f' i) ! ia" using f'_def
                      by (smt (verit) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› mem_Collect_eq nth_butlast) 
                    also have "... ≤ (f' j) ! ia" using ij energy_leq_def True ‹f' ∈ SEQ {e. length e = n}›
                      by simp
                    also have "... = f (wellorder_class.enumerate {i. f i ! n = ∞} j) ! ia" using f'_def True
                      by (smt (verit) SEQ_iff ‹f' ∈ SEQ {e. length e = n}› mem_Collect_eq nth_butlast)
                    finally show ?thesis .
                  next
                    case False
                    hence "ia = n" using ‹ia < Suc n› by simp
                    hence "f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia = ∞" 
                      using enumerate_in_set ‹infinite {i::nat. (f i) ! n = ∞}›
                      by auto  
                    hence "f (wellorder_class.enumerate {i. f i ! n = ∞} i) ! ia = f (wellorder_class.enumerate {i. f i ! n = ∞} j) ! ia" 
                      using enumerate_in_set ‹infinite {i::nat. (f i) ! n = ∞}› ‹ia = n›
                      by force 
                    then show ?thesis by simp
                  qed
                qed
              qed
            qed
            thus "∃i j. i < j ∧ (f i) e≤ (f j)"using le by auto
          qed
        qed
      qed
    qed
  qed
qed

text‹\subsection*{Minimum}›

definition energy_Min:: "energy set ⇒ energy set" where
  "energy_Min A = {e∈A . ∀e'∈A. e≠e' ⟶ ¬ (e' e≤ e)}"

text‹We now observe that the minimum of a non-empty set is not empty. Further, each element $a \in A$ has a lower bound in ‹energy_Min› $A$.›

lemma energy_Min_not_empty:
  assumes "A ≠ {}" and "⋀e. e∈ A ⟹length e = n"
  shows "energy_Min A ≠ {}"
using assms proof(induction n arbitrary: A)
  case 0
  hence "{[]} = A" using assms by auto
  hence "[] ∈ energy_Min A" using energy_Min_def by auto
  then show ?case by auto
next
  case (Suc n)
  have "{butlast a |a. a ∈ A} ≠ {}" using Suc(2) by simp
  have "⋀a. a ∈ {butlast a |a. a ∈ A} ⟹ length a = n" using Suc(3) by auto
  hence "energy_Min {butlast a |a. a ∈ A} ≠ {}" using ‹{butlast a |a. a ∈ A} ≠ {}› Suc(1)
    by meson
  hence "∃x. x∈ energy_Min {butlast a |a. a ∈ A}" by auto
  from this obtain x where "x∈ energy_Min {butlast a |a. a ∈ A}" by auto
  hence "x∈ {butlast a |a. a ∈ A}" using energy_Min_def by auto
  hence "∃a. a∈ A ∧ x = butlast a" by auto
  from this obtain a where "a∈ A ∧ x = butlast a" by auto

  have "last a ∈ {x. (butlast a)@[x] ∈ A} "
    by (metis Suc.prems(2) Zero_neq_Suc ‹a ∈ A ∧ x = butlast a› append_butlast_last_id list.size(3) mem_Collect_eq) 
  hence "{x. (butlast a)@[x] ∈ A} ≠ {}" by auto
  have "∃B. finite B ∧ B⊆ {x. (butlast a)@[x] ∈ A} ∧ Inf {x. (butlast a)@[x] ∈ A} = Min B"
  proof(cases "Inf {x. butlast a @ [x] ∈ A} = ∞")
    case True
    hence "∞ ∈ {x. (butlast a)@[x] ∈ A}" using ‹{x. (butlast a)@[x] ∈ A} ≠ {}›
      by (metis ‹last a ∈ {x. butlast a @ [x] ∈ A}› wellorder_InfI)
    hence "finite {∞} ∧ {∞} ⊆{x. (butlast a)@[x] ∈ A} ∧Inf {x. (butlast a)@[x] ∈ A} = Min {∞}"
      by (simp add: True) 
    then show ?thesis by blast
  next
    case False
    hence "∃m. (enat m) ∈ {x. butlast a @ [x] ∈ A}"
      by (metis Inf_top_conv(2) Succ_def ‹a ∈ A ∧ x = butlast a› not_infinity_eq top_enat_def) 
    from this obtain m where "(enat m) ∈ {x. butlast a @ [x] ∈ A}" by auto
    hence finite: "finite {x. (butlast a)@[x] ∈ A ∧ x≤ enat m}"
      by (metis (no_types, lifting) finite_enat_bounded mem_Collect_eq) 
    have subset: "{x. (butlast a)@[x] ∈ A ∧ x≤ enat m} ⊆ {x. (butlast a)@[x] ∈ A}" by (simp add: Collect_mono)
    have "Inf {x. (butlast a)@[x] ∈ A} = Inf {x. (butlast a)@[x] ∈ A ∧ x≤ enat m}" using ‹(enat m) ∈ {x. butlast a @ [x] ∈ A}›
      by (smt (verit) Inf_lower mem_Collect_eq nle_le wellorder_InfI)
    hence "Inf {x. (butlast a)@[x] ∈ A} = Min {x. (butlast a)@[x] ∈ A ∧ x≤ enat m}" using ‹(enat m) ∈ {x. butlast a @ [x] ∈ A}›
      using finite
      by (smt (verit, best) False Inf_enat_def Min_Inf) 
    hence "finite {x. (butlast a)@[x] ∈ A ∧ x≤ enat m} ∧ {x. (butlast a)@[x] ∈ A ∧ x≤ enat m} ⊆ {x. (butlast a)@[x] ∈ A} ∧ Inf {x. (butlast a)@[x] ∈ A} = Min {x. (butlast a)@[x] ∈ A ∧ x≤ enat m}"
      using finite subset by simp
    then show ?thesis by blast
  qed
  from this obtain B where B: "finite B ∧ B⊆ {x. (butlast a)@[x] ∈ A} ∧ Inf {x. (butlast a)@[x] ∈ A} = Min B" by auto
  hence "((butlast a)@[Min B])∈ A"
    by (metis ‹last a ∈ {x. butlast a @ [x] ∈ A}› mem_Collect_eq wellorder_InfI) 

  have "∀b ∈ A. ((butlast a)@[Min B])≠b ⟶ ¬ (energy_leq b ((butlast a)@[Min B]))" 
  proof
    fix b 
    assume "b∈ A"
    have "energy_leq b (butlast a @ [Min B]) ⟹ butlast a @ [Min B] = b" 
    proof-
      assume "energy_leq b (butlast a @ [Min B])"
      have "energy_leq (butlast b) (butlast a)" 
        unfolding energy_leq_def proof
        show "length (butlast b) = length (butlast a)"
          using ‹⋀a. a ∈ {butlast a |a. a ∈ A} ⟹ length a = n› ‹a ∈ A ∧ x = butlast a› ‹b ∈ A› mem_Collect_eq by blast
        show "∀i<length (butlast b). butlast b ! i ≤ butlast a ! i" 
        proof
          fix i 
          show "i < length (butlast b) ⟶ butlast b ! i ≤ butlast a ! i "
          proof 
            assume " i < length (butlast b)"
            hence "i <length b"
              by (simp add: Suc.prems(2) ‹b ∈ A›) 
            hence B: "b ! i ≤ (butlast a @ [Min B]) !i" using ‹energy_leq b (butlast a @ [Min B])› energy_leq_def by auto

            have "butlast b ! i = b! i" using ‹i < length (butlast b)› nth_butlast by auto
            have "butlast a ! i = (butlast a @ [Min B]) !i "
              by (metis ‹i < length (butlast b)› ‹length (butlast b) = length (butlast a)› butlast_snoc nth_butlast)
            thus "butlast b ! i ≤ butlast a ! i " using B ‹butlast b ! i = b! i› by auto
          qed
        qed
      qed 
      hence "butlast b = butlast a" using ‹x∈ energy_Min {butlast a |a. a ∈ A}› ‹a∈ A ∧ x = butlast a›  energy_Min_def ‹b∈ A› by auto
      hence "(butlast a)@[last b] ∈ A" using Suc(3)
        by (metis ‹b ∈ A› append_butlast_last_id list.size(3) nat.discI) 
      hence "Min B ≤ last b"
        by (metis (no_types, lifting) B Inf_lower mem_Collect_eq) 

      have "last b ≤  Min B" using ‹energy_leq b (butlast a @ [Min B])› energy_leq_def
        by (metis (no_types, lifting) ‹butlast b = butlast a› append_butlast_last_id butlast.simps(1) dual_order.refl impossible_Cons length_Cons length_append_singleton lessI nth_append_length) 
      hence "last b =  Min B" using ‹Min B ≤ last b› by simp
      thus "butlast a @ [Min B] = b" using ‹butlast b = butlast a› Suc(3)
        by (metis Zero_not_Suc ‹b ∈ A› append_butlast_last_id list.size(3))
    qed
    thus "butlast a @ [Min B] ≠ b ⟶ ¬ energy_leq b (butlast a @ [Min B])"
      by auto
  qed
  hence "((butlast a)@[Min B]) ∈ energy_Min A" using energy_Min_def ‹((butlast a)@[Min B])∈ A›
    by simp
  thus ?case by auto
qed

lemma energy_Min_contains_smaller:
  assumes "a ∈ A"
  shows "∃b ∈ energy_Min A. b e≤ a"
proof-
  define set where "set ≡ {e. e ∈ A ∧ e e≤ a}"
  hence "a ∈ set"
    by (simp add: assms(1) energy_leq.refl) 
  hence "set ≠ {}" by auto
  have "⋀s. s∈ set ⟹length s =  length a" using energy_leq_def set_def
    by simp 
  hence "energy_Min set ≠ {}" using ‹set ≠ {}› energy_Min_not_empty by simp
  hence "∃b. b ∈ energy_Min set" by auto
  from this obtain b where "b ∈ energy_Min set" by auto
  hence "⋀b'. b'∈ A ⟹ b' ≠ b ⟹ ¬ (b' e≤ b)"
  proof-
    fix b'
    assume "b' ∈ A"
    assume "b' ≠ b"
    show "¬ (b' e≤ b)"
    proof
      assume "(b' e≤ b)"
      hence "b' e≤ a" using ‹b ∈ energy_Min set› energy_Min_def
        by (simp add: energy_leq.trans local.set_def) 
      hence "b' ∈ set" using ‹b' ∈ A› set_def by simp
      thus "False" using ‹b ∈ energy_Min set› energy_Min_def ‹b' e≤ b› ‹b' ≠ b› by auto 
    qed
  qed
  hence "b∈ energy_Min A" using energy_Min_def
    using ‹b ∈ energy_Min set› local.set_def by auto 
  thus ?thesis using ‹b ∈ energy_Min set› energy_Min_def set_def by auto
qed

text‹We now establish how the minimum relates to subsets.›

lemma energy_Min_subset:
  assumes "A ⊆ B" 
  shows "A ∩ (energy_Min B) ⊆ energy_Min A" and
        "energy_Min B ⊆ A ⟹ energy_Min B = energy_Min A"
proof-
  show "A ∩ energy_Min B ⊆ energy_Min A"
  proof
    fix e 
    assume "e ∈ A ∩ energy_Min B"
    hence "∃a ∈ energy_Min A. a e≤ e" using assms energy_Min_contains_smaller by blast
    from this obtain a where "a ∈ energy_Min A" and " a e≤ e" by auto
    hence "a = e" using ‹e ∈ A ∩ energy_Min B› unfolding energy_Min_def
      using assms by auto 
    thus "e ∈ energy_Min A" using ‹a ∈ energy_Min A› by simp
  qed
  assume "energy_Min B ⊆ A"
  hence "energy_Min B ⊆ energy_Min A" using ‹A ∩ energy_Min B ⊆ energy_Min A› by auto
  have "energy_Min A ⊆ energy_Min B"
  proof
    fix a
    assume "a ∈ energy_Min A"
    hence "a ∈ B" unfolding energy_Min_def using assms by blast
    hence "∃b ∈ energy_Min B. b e≤ a" using assms energy_Min_contains_smaller by blast
    from this obtain b where "b ∈ energy_Min B" and "b e≤ a" by auto
    hence "a = b" using ‹energy_Min B ⊆ A› energy_Min_def
      using ‹a ∈ energy_Min A› by auto 
    thus "a ∈ energy_Min B"
      using ‹b ∈ energy_Min B› by simp
  qed
  thus "energy_Min B = energy_Min A" using ‹energy_Min B ⊆ energy_Min A› by simp
qed

text‹We now show that by well-foundedness the minimum is a finite set. For the proof we first generalise ‹enumerate›.›

fun enumerate_arbitrary :: "'a set ⇒ nat ⇒ 'a"  where
  "enumerate_arbitrary A 0 = (SOME a. a ∈ A)" |
  "enumerate_arbitrary A (Suc n) 
    = enumerate_arbitrary (A - {enumerate_arbitrary A 0}) n"

lemma enumerate_arbitrary_in: 
  shows "infinite A ⟹ enumerate_arbitrary A i ∈ A"
proof(induct i arbitrary: A)
  case 0
  then show ?case using enumerate_arbitrary.simps finite.simps some_in_eq by auto 
next
  case (Suc i)
  hence "infinite (A - {enumerate_arbitrary A 0})" using infinite_remove by simp
  hence "Energy_Order.enumerate_arbitrary (A - {enumerate_arbitrary A 0}) i ∈ (A - {enumerate_arbitrary A 0})" using Suc.hyps by blast
  hence "enumerate_arbitrary A (Suc i) ∈ (A - {enumerate_arbitrary A 0})" using enumerate_arbitrary.simps by simp
  then show ?case by auto
qed

lemma enumerate_arbitrary_neq:
  shows "infinite A ⟹ i < j 
        ⟹ enumerate_arbitrary A i ≠ enumerate_arbitrary A j"
proof(induct i arbitrary: j A)
  case 0
  then show ?case using enumerate_arbitrary.simps
    by (metis Diff_empty Diff_iff enumerate_arbitrary_in finite_Diff_insert gr0_implies_Suc insert_iff)
next
  case (Suc i)
  hence "∃j'. j = Suc j'"
    by (simp add: not0_implies_Suc) 
  from this obtain j' where "j = Suc j'" by auto
  hence "i < j'" using Suc by simp
  from Suc have "infinite (A - {enumerate_arbitrary A 0})" using infinite_remove by simp
  hence "enumerate_arbitrary (A - {enumerate_arbitrary A 0}) i ≠ enumerate_arbitrary (A - {enumerate_arbitrary A 0}) j'" using Suc ‹i < j'›
    by force
  then show ?case using enumerate_arbitrary.simps
    by (simp add: ‹j = Suc j'›) 
qed

lemma energy_Min_finite:
  assumes "⋀e. e∈ A ⟹ length e = n"
  shows "finite (energy_Min A)"
proof-
  have "wqo_on energy_leq (energy_Min A)" using energy_leq_wqo assms 
    by (smt (verit, del_insts) Collect_mono_iff energy_Min_def wqo_on_subset) 
  hence wqoMin: "(∀f ∈ SEQ (energy_Min A). (∃i j. i < j ∧ energy_leq (f i) (f j)))" unfolding wqo_on_def almost_full_on_def good_def by simp
  have "¬ finite (energy_Min A) ⟹ False" 
  proof-
    assume "¬ finite (energy_Min A)"
    hence "infinite (energy_Min A)"
      by simp

    define f where "f ≡ enumerate_arbitrary (energy_Min A)"
    have fneq: "⋀i j. f i ∈ energy_Min A ∧ (j ≠ i ⟶ f j ≠ f i)"
    proof
      fix i j 
      show "f i ∈ energy_Min A" unfolding f_def using enumerate_arbitrary_in ‹infinite (energy_Min A)› by auto 
      show "j ≠ i ⟶ f j ≠ f i" proof
        assume "j ≠ i"
        show "f j ≠ f i" proof(cases "j < i")
          case True
          then show ?thesis unfolding f_def using enumerate_arbitrary_neq ‹infinite (energy_Min A)› by auto 
        next
          case False
          hence "i < j" using ‹j ≠ i› by auto
          then show ?thesis unfolding f_def using enumerate_arbitrary_neq ‹infinite (energy_Min A)›
            by metis 
        qed
      qed
    qed
    hence "∃i j. i < j ∧ energy_leq (f i) (f j)" using wqoMin SEQ_def by simp
    thus "False" using energy_Min_def fneq by force
  qed
  thus ?thesis by auto
qed

text‹\subsection*{Supremum}›

definition energy_sup :: "nat ⇒ energy set ⇒ energy" where 
"energy_sup n A = map (λi. Sup {(e!i)|e. e ∈ A}) [0..<n]" 

text‹We now show that we indeed defined a supremum, i.e.\ a least upper bound, when considering a fixed dimension ‹n›.›

lemma energy_sup_is_sup: 
  shows energy_sup_in: "⋀a. a ∈ A ⟹ length a = n ⟹ a e≤ (energy_sup n A)" and
        energy_sup_leq: "⋀s. (⋀a. a∈ A ⟹a e≤ s) ⟹ length s = n 
                        ⟹ (energy_sup n A) e≤ s"
proof-
  fix a
  assume A1: "a ∈ A" and A2: "length a = n"
  show "a e≤ (energy_sup n A)"
    unfolding energy_leq_def energy_sup_def 
  proof
    show "length a = length (map (λi. Sup {(v!i)|v. v ∈ A}) [0..<n])" using A2
      by simp 
    show "∀i<length a. a ! i ≤ map (λi. Sup {(v!i)|v. v ∈ A}) [0..<n] ! i " 
    proof 
      fix i 
      show "i < length a ⟶ a ! i ≤ map (λi. Sup {(v!i)|v. v ∈ A}) [0..<n] ! i "
      proof 
        assume "i < length a"
        thus "a ! i ≤ map (λi. Sup {(v!i)|v. v ∈ A}) [0..<n] ! i " using A1 A2
        by (smt (verit, del_insts) Sup_upper diff_add_inverse length_upt mem_Collect_eq minus_nat.diff_0 nth_map nth_upt)
      qed
    qed
  qed
next
  fix x 
  assume A1: "⋀a. a∈ A ⟹a e≤ x" and A2: "length x = n"
  show "(energy_sup n A) e≤ x"
    unfolding energy_leq_def
  proof
    show L: "length (energy_sup n A) = length x" using A2 energy_sup_def by simp
    show "∀i<length (energy_sup n A). energy_sup n A ! i ≤ x ! i " 
    proof
      fix i 
      show "i < length (energy_sup n A) ⟶ energy_sup n A ! i ≤ x ! i "
      proof
        assume "i < length (energy_sup n A)"
        hence "i < length [0..<n]" using L A2 by simp
        from A1 have "⋀a. a∈{v ! i |v. v ∈ A} ⟹ a ≤ x ! i"
        proof-
          fix a 
          assume "a∈{v ! i |v. v ∈ A} "
          hence "∃v∈A. a = v ! i" by auto
          from this obtain v where "v∈ A" and "a=v !i" by auto
          thus " a ≤ x ! i" using A1 energy_leq_def L ‹i < length (energy_sup n A)› by simp
        qed

        have "(energy_sup n A) ! i = (map (λi. Sup {(v!i)|v. v ∈ A}) [0..<n] ! i) " using energy_sup_def by auto
        also have "... = (λi. Sup {(v!i)|v. v ∈ A}) ([0..<n] ! i)" using nth_map ‹i < length [0..<n]›
          by auto
        also have "... = Sup {v ! i |v. v ∈ A}"
          using ‹i < length [0..<n]› by auto 
        also have "...≤ (x ! i) " using ‹⋀a. a∈{v ! i |v. v ∈ A} ⟹ a ≤ x ! i›
          by (meson Sup_least)
        finally show "energy_sup n A ! i ≤ x ! i " .
      qed
    qed
  qed
qed

text‹We now observe a version of monotonicity. Afterwards we show that the supremum of the empty set is the zero-vector.›

lemma energy_sup_leq_energy_sup:
  assumes "A ≠ {}" and "⋀a. a∈ A ⟹ ∃b∈ B. energy_leq a b" and 
          "⋀a. a∈ A ⟹ length a = n"
  shows "energy_leq (energy_sup n A) (energy_sup n B)"
proof-
  have len: "length (energy_sup n B) = n" using energy_sup_def by simp
  have "⋀a. a∈ A ⟹ energy_leq a (energy_sup n B)" 
  proof-
    fix a
    assume "a∈ A"
    hence "∃b∈ B. energy_leq a b" using assms by simp
    from this obtain b where "b ∈ B" and "energy_leq a b" by auto
    hence "energy_leq b (energy_sup n B)" using energy_sup_in energy_leq_def
      by (simp add: ‹a ∈ A› assms(3))
    thus "energy_leq a (energy_sup n B)" using ‹energy_leq a b› energy_leq.trans by blast
  qed
  thus ?thesis using len energy_sup_leq by blast
qed

lemma empty_Sup_is_zero:
  assumes "i < n"
  shows "(energy_sup n {}) ! i = 0"
proof-
  have "(energy_sup n {}) ! i = (map (λi. Sup {(v!i)|v. v ∈ {}}) [0..<n]) ! i"
    using energy_sup_def by auto
  also have "... = (λi. Sup {(v!i)|v. v ∈ {}}) ([0..<n] ! i)" using nth_map assms by simp
  finally show "(energy_sup n {}) ! i = 0"
    by (simp add: bot_enat_def)
qed

end