Theory Update

section ‹Bisping's Updates›

theory Update
  imports Energy_Order 
begin

text ‹
In this theory we define a superset of Bisping's updates and their application. Further, we introduce Bisping's ``inversion''
of updates and relate the two.
›

subsection ‹Bisping's Updates›

text ‹
Bisping allows three ways of updating a component of an energy: ‹zero› does not change the respective entry, 
‹minus_one› subtracts one and ‹min_set› $A$ for some set $A$ replaces the entry by the 
minimum of entries whose index is contained in $A$. We further add ‹plus_one› to add one and omit the assumption that the a minimum has to consider the component it replaces.
Updates are vectors where each entry contains the information, how the update changes the respective 
component of energies. We now introduce a datatype such that updates can be represented as lists of ‹update_component›s.
›

datatype update_component = zero | minus_one | min_set "nat set" | plus_one
type_synonym update = "update_component list" 

abbreviation "valid_update u ≡ (∀i D. u ! i = min_set D 
                                    ⟶ D ≠ {} ∧ D ⊆ {x. x < length u})"

text ‹Now the application of updates ‹apply_update› will be defined.›

fun apply_component::"nat ⇒ update_component ⇒ energy ⇒ enat option" where
  "apply_component i zero e = Some (e ! i)" |
  "apply_component i minus_one e = (if ((e ! i) > 0) then Some ((e ! i) - 1) 
                                    else None)" |
  "apply_component i (min_set A) e = Some (min_list (nths e A))"|
  "apply_component i plus_one e = Some ((e ! i)+1)" 

fun apply_update:: "update ⇒ energy ⇒ energy option"  where 
  "apply_update u e = (if (length u = length e) 
          then (those (map (λi. apply_component i (u ! i) e) [0..<length e])) 
          else  None)"

abbreviation "upd u e ≡ the (apply_update u e)"

text ‹We now observe some properties of updates and their application. 
In particular, the application of an update preserves the dimension and the domain of an update is upward closed.
›

lemma len_appl: 
  assumes "apply_update u e ≠ None"
  shows "length (upd u e) = length e"
proof -  
  from assms have "apply_update u e = those (map (λn. apply_component n (u ! n) e) [0..<length e])" by auto
  thus ?thesis using assms len_those
    using length_map length_upt by force 
qed

lemma apply_to_comp_n:
  assumes "apply_update u e ≠ None" and "i < length e"
  shows  "(upd u e) ! i = the (apply_component i (u ! i) e)" 
proof- 
  have "(the (apply_update u e)) ! i =(the (those (map (λn. apply_component n (u ! n) e) [0..<length e])))!i" using apply_update.simps
    using assms by auto 
  also have "... = the ((map (λn. apply_component n (u ! n) e) [0..<length e])! i)" using the_those_n
    by (metis (no_types, lifting) apply_update.simps assms(1) assms(2) calculation length_map map_nth)
  also have "... = the ( apply_component i (u ! i) e)" using nth_map
    by (simp add: assms(2) calculation linordered_semidom_class.add_diff_inverse not_less_zero nth_map_upt)
  finally show ?thesis.
qed

lemma upd_domain_upward_closed:
  assumes "apply_update u e ≠ None" and "e e≤ e'" 
  shows "apply_update u e' ≠ None"
proof
  assume "apply_update u e' = None"
  from assms have "length u = length e'" unfolding apply_update.simps energy_leq_def by metis 
  hence A: "apply_update u e' = those (map (λn. apply_component n (u ! n) e') [0..<length e'])" using apply_update.simps by simp
  hence "those (map (λn. apply_component n (u ! n) e') [0..<length e']) = None" using ‹apply_update u e' = None› by simp
  hence "¬ (∀n < length e'. (λn. apply_component n (u ! n) e') ([0..<length e'] ! n) ≠ None)" using those_map_not_None
    by (metis (no_types, lifting) length_map map_nth)
  hence "∃n< length e'. (λn. apply_component n (u ! n) e') ([0..<length e'] ! n) = None" by auto
  from this obtain n where "n< length e'" and "(λn. apply_component n (u ! n) e') ([0..<length e'] ! n) = None" by auto
  hence "apply_component n (u ! n) e' = None" by simp
  hence "u ! n = minus_one" using apply_component.elims by blast
  hence  " e' ! n = 0" using ‹apply_component n (u ! n) e' = None› apply_component.elims
    by fastforce
  hence "e ! n = 0" using assms(2) energy_leq_def ‹n < length e'› by auto 
  hence "(λn. apply_component n (u ! n) e) ([0..<length e] ! n) = None" using ‹u ! n = minus_one› apply_component.simps(2)
    using ‹n < length e'› assms(2) energy_leq_def by auto
  hence "those (map (λn. apply_component n (u ! n) e) [0..<length e]) = None" using those.simps option.map_sel  ‹n < length e'›
    by (smt (verit, ccfv_SIG) ‹length u = length e'› apply_update.simps assms(1) length_map map_nth nth_map those_all_Some)
  hence "apply_update u e = None" by simp 
  thus "False" using assms(1) by simp
qed

text ‹Now we show that all valid updates are  monotonic. The proof follows directly 
from the definition of ‹apply_update› and ‹valid_update›.› 

lemma updates_monotonic:
  assumes "apply_update u e ≠ None" and "e e≤ e'" and "valid_update u"
  shows "(upd u e) e≤ (upd u e')" 
  unfolding energy_leq_def proof
  have "apply_update u e' ≠ None" using assms upd_domain_upward_closed by auto
  thus "length (the (apply_update u e)) = length (the (apply_update u e'))" using assms len_appl
    by (metis energy_leq_def)
  show "∀n<length (the (apply_update u e)). the (apply_update u e) ! n ≤ the (apply_update u e') ! n " 
  proof 
    fix n 
    show "n < length (the (apply_update u e)) ⟶ the (apply_update u e) ! n ≤ the (apply_update u e') ! n"
    proof 
      assume "n < length (the (apply_update u e))"
      hence "n < length e" using len_appl assms(1)
        by simp
      hence " e ! n ≤ e' !n " using assms energy_leq_def
        by simp
      consider (zero) "(u ! n) = zero" | (minus_one) "(u ! n) = minus_one" | (min_set) "(∃A. (u ! n) = min_set A)" | (plus_one) "(u ! n) = plus_one"
        using update_component.exhaust by auto 
      thus "the (apply_update u e) ! n ≤ the (apply_update u e') ! n" 
      proof (cases)
        case zero
        then show ?thesis using apply_update.simps apply_component.simps assms ‹e ! n ≤ e' !n› ‹apply_update u e' ≠ None›
          by (metis ‹n < length (the (apply_update u e))› apply_to_comp_n len_appl option.sel)
      next
        case minus_one
        hence "the (apply_update u e) ! n = the (apply_component n (u ! n) e)" using apply_to_comp_n assms(1)
          by (simp add: ‹n < length e›)

        from assms(1) have A: "(map (λn. apply_component n (u ! n) e) [0..<length e]) ! n ≠ None" using  ‹n < length e› those_all_Some apply_update.simps
          by (metis (no_types, lifting) length_map map_nth) 
        hence "(apply_component n (u ! n) e) = (map (λn. apply_component n (u ! n) e) [0..<length e]) ! n " using ‹n < length e›
          by simp
        hence "(apply_component n (u ! n) e) ≠ None" using A by simp
        hence "e ! n >0 " using minus_one apply_component.elims by auto 
        hence  "(e ! n) -1 ≤ (e' ! n) -1" using ‹e ! n ≤ e' ! n› by (metis eSuc_minus_1 iadd_Suc ileI1 le_iff_add)

        from ‹e ! n >0› have "e' ! n > 0" using assms(2) energy_leq_def
          using ‹e ! n ≤ e' ! n› by auto 
        have A: "the (apply_update u e') ! n = the (apply_component n (u ! n) e')" using apply_to_comp_n ‹apply_update u e' ≠ None›
          using ‹n < length e› assms(2) energy_leq_def by auto 
        have "the (apply_component n (u ! n) e' )= (e' ! n) -1" using minus_one ‹e' ! n >0›
          by simp
        hence "the (apply_update u e') ! n  = (e' ! n) -1" using A by simp
        then show ?thesis using ‹(e ! n) -1 ≤ (e' ! n) -1›
          using ‹0 < e ! n› ‹the (apply_update u e) ! n = the (apply_component n (u ! n) e)› minus_one by auto
      next
        case min_set
        from this obtain A where "u ! n = min_set A" by auto
        hence " A ⊆ {x. x < length e}" using assms(3)  by (metis apply_update.elims assms(1))
        hence "∀a ∈ A. e!a ≤ e'!a" using assms(2) energy_leq_def
          by blast
        have "∀a∈ A. (Min (set (nths e A))) ≤ e! a" proof
          fix a
          assume "a ∈ A"
          hence "e!a ∈ set (nths e A)" using set_nths nths_def
            using ‹A ⊆ {x. x < length e}› in_mono by fastforce
          thus "Min (set (nths e A)) ≤ e ! a " using Min_le by simp
        qed
        hence "∀a∈ A. (Min (set (nths e A))) ≤ e'! a" using ‹∀a ∈ A. e!a ≤ e'!a›
          using dual_order.trans by blast 
        hence "∀x ∈ (set (nths e' A)). (Min (set (nths e A))) ≤ x" using set_nths
          by (smt (verit) mem_Collect_eq)        

        from assms(2) have "A≠{}"
          using ‹u ! n = min_set A› assms(3) by auto 
        have "A ⊆ {x. x < length e'}" using ‹A ⊆ {x. x < length e}› assms
          using energy_leq_def by auto 
        hence "set (nths e' A) ≠ {}" using ‹A ≠{}› set_nths
          by (smt (verit, best) Collect_empty_eq Collect_mem_eq Collect_mono_iff) 
        hence "(nths e' A) ≠ []" by simp
        from ‹A≠{}› have "set (nths e A) ≠ {}" using set_nths ‹A ⊆ {x. x < length e}› Collect_empty_eq ‹n < length e› ‹u ! n = min_set A›
          by (smt (verit, best) ‹set (nths e' A) ≠ {}› assms(2) energy_leq_def)
        hence "(nths e A) ≠ []" by simp
        hence "(min_list (nths e A)) = Min (set (nths e A))" using min_list_Min by auto
        also have "... ≤ Min (set (nths e' A))"        
          using ‹∀x ∈ (set (nths e' A)). (Min (set (nths e A))) ≤ x›
          by (simp add: ‹nths e' A ≠ []›) 
        finally have "(min_list (nths e A)) ≤ min_list (nths e' A)" using min_list_Min ‹(nths e' A) ≠ []› by metis
        then show ?thesis using apply_to_comp_n assms(1) ‹apply_update u e' ≠ None› apply_component.simps(3) ‹u ! n = min_set A›
          by (metis ‹length (the (apply_update u e)) = length (the (apply_update u e'))› ‹n < length e› len_appl option.sel)
      next
        case plus_one 
        have "upd u e ! n = the (apply_component n (u ! n) e)" using apply_to_comp_n ‹n < length e› assms(1) by auto 
        also have "... =  (e!n) +1" using apply_component.elims plus_one
          by simp
        also have "... ≤ (e'!n) +1" 
          using ‹e ! n ≤ e' ! n› by auto 
        also have "... = upd u e' ! n" using  apply_to_comp_n ‹n < length e› assms apply_component.elims plus_one
          by (metis ‹apply_update u e' ≠ None› apply_component.simps(4) energy_leq_def option.sel)
        finally show ?thesis by simp
      qed
    qed
  qed
qed

subsection ‹Bisping's Inversion›

text‹The ``inverse'' of an update $u$ is a function mapping energies $e$ to $\min \lbrace e' \ | \ e \leq u(e') \rbrace$ 
w.r.t\ the component-wise order.
We start by giving a calculation and later show that we indeed calculate such minima.  
For an energy $e = (e_0, ..., e_{n-1})$ we calculate this component-wise such that the $i$-th 
component is the maximum of $e_i$ (plus or minus one if applicable) 
and each entry $e_j$ where $i \in u_j \subseteq \lbrace 0, ..., n-1 \rbrace $.
Note that this generalises the inversion proposed by Bisping~\cite{bens-algo}.
›

fun apply_inv_component::"nat ⇒ update ⇒ energy ⇒ enat" where
  "apply_inv_component i u e = Max (set (map (λ(j,up). 
          (case up of zero ⇒ (if i=j then (e ! i) else 0) | 
                minus_one ⇒ (if i=j then (e ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e ! j) else 0) | 
                plus_one ⇒ (if i=j then (e ! i)-1 else 0))) 
          (List.enumerate 0 u)))" 

fun apply_inv_update:: "update ⇒ energy ⇒ energy option" where 
  "apply_inv_update u e = (if (length u = length e) 
                    then Some (map (λi. apply_inv_component i u e) [0..<length e])
                    else None)" 

abbreviation "inv_upd u e ≡ the (apply_inv_update u e)"

text ‹We now observe the following properties, if an update $u$ and an energy $e$ have the same dimension:
\begin{itemize}
  \item ‹apply_inv_update› preserves dimension.
  \item The domain of ‹apply_inv_update u› is $\lbrace ‹e› \ | \ |‹e›| = |‹u›| \rbrace$.
  \item ‹apply_inv_update u e›  is in the domain of the update ‹u›.
\end{itemize}
The first two proofs follow directly from the definition of ‹apply_inv_update›, while the proof
of ‹inv_not_none_then› is done by a case analysis of the possible ‹update_component›s. ›

lemma len_inv_appl: 
  assumes "length u = length e"
  shows "length (inv_upd u e) = length e"
  using assms apply_inv_update.simps length_map option.sel by auto

lemma inv_not_none: 
  assumes "length u = length e"
  shows "apply_inv_update u e ≠ None" 
  using assms apply_inv_update.simps by simp  

lemma inv_not_none_then:
  assumes "apply_inv_update u e ≠ None"
  shows "(apply_update u (inv_upd u e)) ≠ None"
proof - 
  have len: "length u = length (the (apply_inv_update u e))" using assms apply_inv_update.simps len_those
    by auto 
  have "∀n<length u. (apply_component n (u ! n) (the (apply_inv_update u e)))≠None" 
  proof
    fix n
    show "n < length u ⟶ apply_component n (u ! n) (the (apply_inv_update u e)) ≠ None " 
    proof 
      assume "n<length u"
      consider (zero) "(u ! n) = zero" | (minus_one) "(u ! n) = minus_one" | (min_set) "(∃A. (u ! n) = min_set A)" | (plus_one) "(u ! n) = plus_one"
        using update_component.exhaust by auto 
      then show "apply_component n (u ! n) (the (apply_inv_update u e)) ≠ None" 
      proof(cases)
        case zero
        then show ?thesis by simp 
      next
        case minus_one
        have nth: "(the (apply_inv_update u e)) ! n = apply_inv_component n u e" using apply_inv_update.simps
          by (metis ‹n < length u› add_0 assms diff_add_inverse nth_map_upt option.sel)

        have n_minus_one: "List.enumerate 0 u ! n = (n,minus_one) " using minus_one
          by (simp add: ‹n < length u› nth_enumerate_eq) 
        have "(λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)))(n,minus_one) = (e ! n) +1"
          by simp
        hence "(e ! n) +1 ∈ set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒(if n=m then (nth e n)-1 else 0)))(List.enumerate 0 u))" using n_minus_one
          by (metis (no_types, lifting) ‹n < length u› case_prod_conv length_enumerate length_map nth_map nth_mem update_component.simps(15))
        hence "(nth e n)+1 ≤ apply_inv_component n u e" using minus_one nth apply_inv_component.simps Max_ge
          by simp
        hence "(nth (the (apply_inv_update u e)) n >0)" using nth by fastforce
        then show ?thesis by (simp add: minus_one) 
      next
        case min_set
        then show ?thesis by auto 
      next 
        case plus_one
        then show ?thesis by simp
      qed
    qed
  qed
  hence "∀n<length (the (apply_inv_update u e)). apply_component n (u ! n) (the (apply_inv_update u e)) ≠ None" 
    using len by presburger 
  hence "those (map (λn. apply_component n (u ! n) (the (apply_inv_update u e))) [0..<length (the (apply_inv_update u e))]) ≠ None" 
    using those_map_not_None
    by (smt (verit) add_less_cancel_left gen_length_def length_code length_map map_nth nth_upt) 
  thus ?thesis using apply_update.simps len by presburger
qed

text ‹Now we show that ‹apply_inv_update u› is monotonic for all updates ‹u›. The proof follows directly 
from the definition of ‹apply_inv_update› and a case analysis of the possible update components.›

lemma inverse_monotonic:
  assumes "e e≤ e'" and "length u = length e'"
  shows "(inv_upd u e) e≤ (inv_upd u e')"
  unfolding energy_leq_def proof
  show "length (the (apply_inv_update u e)) = length (the (apply_inv_update u e'))" using assms len_inv_appl energy_leq_def
    by simp 
  show "∀i<length (the (apply_inv_update u e)). the (apply_inv_update u e) ! i ≤ the (apply_inv_update u e') ! i " 
  proof
    fix i
    show "i < length (the (apply_inv_update u e)) ⟶ the (apply_inv_update u e) ! i ≤ the (apply_inv_update u e') ! i "
    proof 
      assume "i < length (the (apply_inv_update u e))"
      have "the (apply_inv_update u e) ! i = (map (λi. apply_inv_component i u e) [0..<length e]) ! i" 
        using apply_inv_update.simps assms
        using energy_leq_def by auto
      also have "... =  (λi. apply_inv_component i u e) ([0..<length e] ! i)" using nth_map
        by (metis (full_types) ‹i < length (the (apply_inv_update u e))› add_less_mono assms(1) assms(2) energy_leq_def diff_add_inverse gen_length_def len_inv_appl length_code less_add_same_cancel2 not_less_less_Suc_eq nth_map_upt nth_upt plus_1_eq_Suc)
      also have "... = apply_inv_component i u e"
        using ‹i < length (the (apply_inv_update u e))› assms(1) assms(2) energy_leq_def by auto 
      finally have E: "the (apply_inv_update u e) ! i =
                Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e i) else 0)  | 
                minus_one ⇒ (if i=m then (e ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e ! m) else 0) |
                plus_one ⇒ (if i=m then (nth e i)-1 else 0))) (List.enumerate 0 u)))" using apply_inv_component.simps
        by presburger 


      have "the (apply_inv_update u e') ! i = (map (λi. apply_inv_component i u e') [0..<length e']) ! i" 
        using apply_inv_update.simps assms
        using energy_leq_def by auto
      also have "... =  (λi. apply_inv_component i u e') ([0..<length e'] ! i)" using nth_map
        by (metis (full_types) ‹i < length (the (apply_inv_update u e))› add_less_mono assms(1) assms(2) energy_leq_def diff_add_inverse gen_length_def len_inv_appl length_code less_add_same_cancel2 not_less_less_Suc_eq nth_map_upt nth_upt plus_1_eq_Suc)
      also have "... = apply_inv_component i u e'"
        using ‹i < length (the (apply_inv_update u e))› assms(1) assms(2) energy_leq_def by auto 
      finally have E': "the (apply_inv_update u e') ! i =
                Max (set (map (λ(m,up). (case up of 
                zero ⇒(if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0) |
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u)))" using apply_inv_component.simps
        by presburger 

      have fin': "finite (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0) |
                plus_one ⇒(if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u)))" by simp
      have fin: "finite (set (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0) | minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 |
                            plus_one ⇒ (if i=m then (nth e i)-1 else 0)) 
                   (List.enumerate 0 u)))" by simp

      have "⋀x. x ∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e i) else 0) | 
                minus_one ⇒ (if i=m then (e ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e ! m) else 0) |
                plus_one ⇒ (if i=m then (nth e i)-1 else 0))) (List.enumerate 0 u))) ⟹ (∃y. x≤ y ∧ y∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0)|
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u))))"
      proof-
        fix x
        assume "x ∈ set (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0) | minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 |
                plus_one ⇒ (if i=m then (nth e i)-1 else 0))
                   (List.enumerate 0 u))" 
        hence "∃j < length u. x = (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0) | minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 |
                plus_one ⇒ (if i=m then (nth e i)-1 else 0))
                   (List.enumerate 0 u)) ! j" using in_set_conv_nth
          by (metis (no_types, lifting) length_enumerate length_map)
        from this obtain j where "j < length u" and X: "x = (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0)| minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 |
                plus_one ⇒ (if i=m then (nth e i)-1 else 0))
                   (List.enumerate 0 u)) ! j" by auto
        hence "(List.enumerate 0 u) ! j = (j, (u !j))"
          by (simp add: nth_enumerate_eq) 
        hence X: "x=(case (u !j) of zero ⇒ (if i=j then (nth e i) else 0) | minus_one ⇒ if i = j then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! j else 0 |
                plus_one ⇒ (if i=j then (nth e i)-1 else 0))" using X
          by (simp add: ‹j < length u›) 

        consider (zero) "(u !j) = zero" | (minus_one) "(u !j) = minus_one" | (min_set) "∃ A. (u !j) = min_set A" | (plus_one) "(u!j) = plus_one"
          by (meson update_component.exhaust)

        thus "(∃y. x≤ y ∧ y∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0) |
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u))))" 
        proof(cases)
          case zero
          hence "x= (if i=j then (nth e i) else 0)" using X by simp
          also have "... ≤ (if i=j then (nth e' i) else 0)" using assms
            using ‹i < length (the (apply_inv_update u e))› energy_leq_def
            by force
          also have "... = (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 |
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
            by (simp add: zero)
          finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0|
                            plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
            by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
          then show ?thesis
            using ‹j < length u› by auto 
        next
          case minus_one
          hence X: "x = (if i=j then (e ! i)+1 else 0)" using X by simp
          then show ?thesis proof(cases "i=j")
            case True
            hence "x = (e ! i) +1" using X by simp
            also have "...≤ (e' ! i) +1" using assms
              using True ‹j < length u› energy_leq_def by auto
            also have "... = (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 |
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
            by (simp add: minus_one True)
             finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒(if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0|
                plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
            by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
          then show ?thesis
            using ‹j < length u› by auto
          next
            case False
            hence "x = 0 " using X by simp
            also have "...≤ 0"
              by simp
            also have "... = (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 |
                plus_one ⇒(if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
            by (simp add: minus_one False)
             finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
            by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
          then show ?thesis
            using ‹j < length u› by auto
          qed
        next
          case min_set
          from this obtain A where A: "u ! j = min_set A " by auto
          hence X: "x = (if i ∈ A then e ! j else 0)" using X by auto
          then show ?thesis proof(cases "i ∈ A")
            case True
            hence "x=e ! j" using X by simp
            also have "...≤ e'!j" using assms
              using ‹j < length u› energy_leq_def by auto
            also have "... = (λ(m, up).
                            case up of zero ⇒(if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
              by (simp add: A True)
            finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
              by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
            then show ?thesis
              using ‹j < length u› by auto
          next
            case False
            hence "x=0" using X by simp
            also have "... = (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
              by (simp add: A False)
            finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
              by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
            then show ?thesis
              using ‹j < length u› by auto
          qed
        next 
          case plus_one
          then show ?thesis proof(cases "i=j")
            case True
            hence "x=e!i -1" using X plus_one by simp
            have "x ≤ e' ! i -1"
            proof(cases "e!i =0")
              case True
              then show ?thesis
                by (simp add: ‹x = e ! i - 1›)
            next
              case False
              then show ?thesis
              proof(cases "e!i = ∞")
                case True
                then show ?thesis using assms
                  using ‹i < length (inv_upd u e)› energy_leq_def by fastforce
              next
                case False
                from this obtain b where "e!i = enat (Suc b)" using ‹ e ! i ≠ 0›
                  by (metis list_decode.cases not_enat_eq zero_enat_def)
                then show ?thesis 
                proof(cases "e'!i = ∞")
                  case True
                  then show ?thesis
                    by simp
                next
                  case False
                  from this obtain c where "e'!i = enat (Suc c)" using  ‹e!i = enat (Suc b)› assms
                    by (metis (no_types, lifting) Nat.lessE Suc_ile_eq ‹i < length (inv_upd u e)› enat.exhaust enat_ord_simps(2) energy_leq_def len_inv_appl) 
                  hence "b ≤ c" using assms
                    using ‹e ! i = enat (Suc b)› ‹i < length (inv_upd u e)› energy_leq_def by auto 
                  then show ?thesis using  ‹e!i = enat (Suc b)›  ‹e'!i = enat (Suc c)›
                    by (simp add: ‹x = e ! i - 1› one_enat_def)
                qed
              qed
            qed
            show ?thesis
              using plus_one True ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u› ‹x ≤ e' ! i - 1›
              by (smt (verit, best) nth_map case_prod_conv length_enumerate length_map nth_mem update_component.simps(17))
          next
            case False
            hence "x = 0" using X
              using plus_one by auto
            also have "...≤ 0" by simp
            also have "... = (λ(m, up).
                            case up of zero ⇒(if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 |
                plus_one ⇒(if i=m then (nth e' i)-1 else 0))(j, (u ! j))"
              by (simp add: plus_one False)
            finally have "x ≤ (map (λ(m, up).
                            case up of zero ⇒ (if i=m then (nth e' i) else 0) | minus_one ⇒ if i = m then e' ! i + 1 else 0
                            | min_set A ⇒ if i ∈ A then e' ! m else 0 | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))
                     (List.enumerate 0 u))!j"
              by (simp add: ‹List.enumerate 0 u ! j = (j, u ! j)› ‹j < length u›)
            then show ?thesis
              using ‹j < length u› by auto
          qed
        qed
      qed

      hence "∀x∈ (set (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0) | minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 | plus_one ⇒ (if i=m then (nth e i)-1 else 0))
                   (List.enumerate 0 u))). 
            x≤ Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0) | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u)))"
        using fin'
        by (meson Max.coboundedI dual_order.trans) 
      hence "Max (set (map (λ(m, up).
                          case up of zero ⇒ (if i=m then (nth e i) else 0) | minus_one ⇒ if i = m then e ! i + 1 else 0
                          | min_set A ⇒ if i ∈ A then e ! m else 0 | plus_one ⇒ (if i=m then (nth e i)-1 else 0))
                   (List.enumerate 0 u)))
            ≤ Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if i=m then (nth e' i) else 0) | 
                minus_one ⇒ (if i=m then (e' ! i)+1 else 0) |
                min_set A ⇒ (if i∈A then (e' ! m) else 0) | plus_one ⇒ (if i=m then (nth e' i)-1 else 0))) (List.enumerate 0 u)))"
        using fin assms Max_less_iff
        by (metis (no_types, lifting) Max_in ‹i < length (the (apply_inv_update u e))› ‹length (the (apply_inv_update u e)) = length (the (apply_inv_update u e'))› ex_in_conv len_inv_appl length_enumerate length_map nth_mem)

      thus "the (apply_inv_update u e) ! i ≤ the (apply_inv_update u e') ! i " using E E'
        by presburger 
    qed
  qed
qed

subsection ‹Relating Updates and ``Inverse'' Updates›

text ‹
Since the minimum is not an injective function, for many updates there does not exist an inverse. The 
following $2$-dimensional examples show, that the function ‹apply_inv_update› does not map an update to its inverse.
›

lemma not_right_inverse_example:
  shows "apply_update [minus_one, (min_set {0,1})] [1,2] = Some [0,1]"
        "apply_inv_update [minus_one, (min_set {0,1})] [0,1] = Some [1,1]"  
  by (auto simp add: nths_def)

lemma not_right_inverse:
  shows "∃u. ∃e. apply_inv_update u (upd u e) ≠ Some e" 
  using not_right_inverse_example by force

lemma not_left_inverse_example:
  shows "apply_inv_update [zero, (min_set {0,1})] [0,1] = Some [1,1]"  
        "apply_update [zero, (min_set {0,1})] [1,1] = Some [1,1]"
  by (auto simp add: nths_def)

lemma not_left_inverse: 
  shows "∃u. ∃e. apply_update u (inv_upd u e) ≠ Some e" 
  by (metis option.sel apply_update.simps length_0_conv not_Cons_self2 option.distinct(1))

text ‹
We now show that the given calculation ‹apply_inv_update› indeed calculates $e \mapsto  \min \lbrace e' \ | \ e \leq u(e') \rbrace$
for all valid updates $u$.
For this we first name this set ‹possible_inv u e›. Then we show that ‹inv_upd u e› is an element 
of that set before showing that it is minimal. 
Considering one component at a time, the proofs follow by a case analysis of the possible 
update components from the definition of ‹apply_inv_update›
›

abbreviation "possible_inv u e ≡ {e'. apply_update u e' ≠ None 
                                        ∧ (e e≤ (upd u e'))}"

lemma leq_up_inv:
  assumes "length u = length e" and "valid_update u"
  shows "e e≤ (upd u (inv_upd u e))"
  unfolding energy_leq_def proof
  from assms have notNone: "apply_update u (the (apply_inv_update u e)) ≠ None" using inv_not_none_then inv_not_none by blast
  thus len1: "length e = length (the (apply_update u (the (apply_inv_update u e))))" using assms len_appl len_inv_appl
    by presburger

  show "∀n<length e. e ! n ≤ the (apply_update u (the (apply_inv_update u e))) ! n " 
  proof
    fix n 
    show "n < length e ⟶ e ! n ≤ the (apply_update u (the (apply_inv_update u e))) ! n " 
    proof
      assume "n < length e"

      have notNone_n: "(map (λn. apply_component n (u ! n) (the (apply_inv_update u e))) [0..<length (the (apply_inv_update u e))]) ! n ≠ None" using notNone apply_update.simps
        by (smt (verit) ‹n < length e› assms(1) length_map map_nth nth_map option.distinct(1) those_all_Some)

      have "the (apply_update u (the (apply_inv_update u e))) ! n = the (those (map (λn. apply_component n (u ! n) (the (apply_inv_update u e))) [0..<length (the (apply_inv_update u e))])) ! n" 
        using apply_update.simps assms(1) len1 notNone by presburger 
      also have " ... = the ((map (λn. apply_component n (u ! n) (the (apply_inv_update u e))) [0..<length (the (apply_inv_update u e))]) ! n)" using the_those_n notNone
        by (smt (verit) ‹n < length e› apply_update.elims calculation assms(1) length_map map_nth nth_map) 
      also have "... = the ((λn. apply_component n (u ! n) (the (apply_inv_update u e))) ([0..<length (the (apply_inv_update u e))] ! n))" using nth_map
        using ‹n < length e› assms len_inv_appl minus_nat.diff_0 nth_upt by auto
      also have " ... = the (apply_component n (u ! n) (the (apply_inv_update u e)))" using ‹n < length e› assms len_inv_appl
        by (simp add: plus_nat.add_0) 
      finally have unfolded_apply_update: "the (apply_update u (the (apply_inv_update u e))) ! n = the (apply_component n (u ! n) (the (apply_inv_update u e)))" .

      have "(the (apply_inv_update u e)) ! n = (the (Some (map (λn. apply_inv_component n u e) [0..<length e])))!n " using apply_inv_update.simps assms(1) by auto
      also have "... = (map (λn. apply_inv_component n u e) [0..<length e]) ! n" by auto
      also have "... =  apply_inv_component n u e" using nth_map map_nth
        by (smt (verit) Suc_diff_Suc ‹n < length e› add_diff_inverse_nat diff_add_0 length_map less_diff_conv less_one nat_1 nat_one_as_int nth_upt plus_1_eq_Suc) 
      finally have unfolded_apply_inv: "(the (apply_inv_update u e)) ! n = apply_inv_component n u e". 

      consider (zero) "u ! n = zero" |(minus_one) "u ! n = minus_one" |(min_set) "∃A. min_set A = u ! n" | (plus_one) "u!n = plus_one"
        by (metis update_component.exhaust) 
      thus "e ! n ≤ the (apply_update u (the (apply_inv_update u e))) ! n" 
      proof (cases)
        case zero
        hence "(List.enumerate 0 u) ! n = (n, zero)"
          by (simp add: ‹n < length e› assms(1) nth_enumerate_eq) 
        hence nth_in_set: "e ! n ∈ set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u))" using nth_map
          by (smt (verit) ‹n < length e› assms(1) length_enumerate length_map nth_mem old.prod.case update_component.simps(14))

        from zero have "the (apply_update u (the (apply_inv_update u e))) ! n = the (apply_component n zero (the (apply_inv_update u e)))" using unfolded_apply_update by auto
        also have "... = ((the (apply_inv_update u e)) ! n)" using apply_component.simps(1) by simp
        also have "... = apply_inv_component n u e" using unfolded_apply_inv by auto
        also have "... =  Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using apply_inv_component.simps by auto
        also have "... ≥ e ! n " using nth_in_set by simp
        finally show ?thesis .
      next
        case minus_one

        hence A: "(λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (n,(u!n)) = (e!n) +1"
          by simp 
        have "(List.enumerate 0 u)!n = (n,(u!n))"
          using ‹n < length e› assms(1) nth_enumerate_eq
          by (metis add_0)
        hence "(e!n) +1 ∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using A nth_map
          by (metis (no_types, lifting) ‹n < length e› assms(1) length_enumerate length_map nth_mem) 
        hence leq: "(e!n) +1 ≤ Max (set (map (λ(m,up). (case up of 
                zero ⇒(if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using Max_ge by simp

        have notNone_comp: "apply_component n minus_one (the (apply_inv_update u e)) ≠ None" using notNone
          by (smt (z3) ‹n < length e› add_0 len1 len_appl length_map length_upt map_nth minus_one notNone_n nth_map_upt)

        from minus_one have "the (apply_update u (the (apply_inv_update u e))) ! n = the (apply_component n minus_one (the (apply_inv_update u e)))" using unfolded_apply_update by auto
        also have "... = ((the (apply_inv_update u e)) ! n) -1" using apply_component.simps(2) notNone_comp
          using calculation option.sel by auto 
        also have "... = apply_inv_component n u e -1" using unfolded_apply_inv by auto
        also have "... =  Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u))) -1" using apply_inv_component.simps by auto
        also have "... ≥ e ! n" using leq 
          by (smt (verit) add.assoc add_diff_assoc_enat le_iff_add) 
        finally show ?thesis .
      next
        case min_set
        from this obtain A where "min_set A = u ! n" by auto

        have "upd u (inv_upd u e) ! n = the (apply_component n (min_set A) (inv_upd u e))"
          using ‹min_set A = u ! n› unfolded_apply_update by auto
        also have "... = (min_list (nths (inv_upd u e) A))" 
          using apply_component.elims
          by simp

        have leq: "⋀j. j ∈ A ⟹ e!n ≤ (inv_upd u e)!j"
        proof-
          fix j
          assume "j ∈ A"
          hence "j < length e" using assms
            by (metis ‹min_set A = u ! n› in_mono mem_Collect_eq) 
          hence "j < length [0..<length e]"
            by simp
          have "(inv_upd u e)!j = (map (λi. apply_inv_component i u e) [0..<length e])!j"
            using apply_inv_update.simps assms
            by simp 
          hence "(inv_upd u e)!j = apply_inv_component j u e"
            using nth_map ‹j < length [0..<length e]›
            by (metis ‹j < length e› nth_upt plus_nat.add_0)
          hence "(inv_upd u e)!j =  Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if j=m then (nth e j) else 0) | 
                minus_one ⇒ (if j=m then (nth e j)+1 else 0) |
                min_set A ⇒ (if j∈A then (nth e m) else 0)|
                plus_one ⇒ (if j=m then (nth e j)-1 else 0))) (List.enumerate 0 u)))"
            by auto

          have "(List.enumerate 0 u)! n = (n, u ! n)"
            by (simp add: ‹n < length e› assms(1) nth_enumerate_eq)

          have fin: "finite (set (map (λ(m,up). (case up of 
                zero ⇒ (if j=m then (nth e j) else 0) | 
                minus_one ⇒ (if j=m then (nth e j)+1 else 0) |
                min_set A ⇒ (if j∈A then (nth e m) else 0)|
                plus_one ⇒ (if j=m then (nth e j)-1 else 0))) (List.enumerate 0 u)))" by auto
          have "e!n =  (case (min_set A)  of 
                zero ⇒ (if j=n then (nth e j) else 0) | 
                minus_one ⇒ (if j=n then (nth e j)+1 else 0) |
                min_set A ⇒ (if j∈A then (nth e n) else 0)|
                plus_one ⇒ (if j=n then (nth e j)-1 else 0))"
            by (simp add: ‹j ∈ A›)
          hence "e!n = (λ(m,up). (case up of 
                zero ⇒ (if j=m then (nth e j) else 0) | 
                minus_one ⇒ (if j=m then (nth e j)+1 else 0) |
                min_set A ⇒ (if j∈A then (nth e m) else 0)|
                plus_one ⇒ (if j=m then (nth e j)-1 else 0))) (n, u ! n)"
            using ‹min_set A = u ! n› by simp
          hence "e!n ∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if j=m then (nth e j) else 0) | 
                minus_one ⇒ (if j=m then (nth e j)+1 else 0) |
                min_set A ⇒ (if j∈A then (nth e m) else 0)|
                plus_one ⇒ (if j=m then (nth e j)-1 else 0))) (List.enumerate 0 u)))"
            using ‹(List.enumerate 0 u)! n = (n, u ! n)› nth_map
            by (metis (no_types, lifting) ‹n < length e› assms(1) in_set_conv_nth length_enumerate length_map)

          thus "e!n ≤ (inv_upd u e)!j"
            using fin Max_le_iff
            using ‹inv_upd u e ! j = Max (set (map (λ(k, y). case y of zero ⇒(if j=k then (nth e j) else 0) | minus_one ⇒ if j = k then e ! j + 1 else 0 | min_set A ⇒ if j ∈ A then e ! k else 0 | plus_one ⇒ if j = k then e ! j - 1 else 0) (List.enumerate 0 u)))› by fastforce
        qed

        have "A ≠ {} ∧ A ⊆ {x. x < length u}" using assms
          by (simp add: ‹min_set A = u ! n›)
        hence "A ≠ {} ∧ A ⊆ {x. x < length (inv_upd u e)}" using assms
          by auto

        have "set (nths (inv_upd u e) A) = {(inv_upd u e) ! i |i. i < length (inv_upd u e) ∧ i ∈ A}"
          using set_nths by metis
        hence not_empty: "(set (nths (inv_upd u e) A)) ≠ {}"
          using ‹A ≠ {} ∧ A ⊆ {x. x < length (inv_upd u e)}›
          by (smt (z3) Collect_empty_eq equals0I in_mono mem_Collect_eq)
        hence "(nths (inv_upd u e) A) ≠ []"
          by blast
        hence min_eq_Min: "min_list (nths (inv_upd u e) A) = Min (set (nths (inv_upd u e) A))"
          using min_list_Min by blast

        have "finite (set (nths (inv_upd u e) A))" using assms ‹min_set A = u ! n›
          by simp
        hence "(e!n ≤ Min (set (nths (inv_upd u e) A))) = (∀a∈(set (nths (inv_upd u e) A)). e!n ≤ a)"
          using not_empty Min_ge_iff by auto

        have "e!n ≤ Min (set (nths (inv_upd u e) A))" 
          unfolding ‹(e!n ≤ Min (set (nths (inv_upd u e) A))) = (∀a∈(set (nths (inv_upd u e) A)). e!n ≤ a)›
        proof
          fix x 
          assume "x ∈ set (nths (inv_upd u e) A)"
          hence "x∈ {(inv_upd u e) ! i |i. i < length (inv_upd u e) ∧ i ∈ A}"
            using set_nths
            by metis 
          hence "∃j. j ∈ A ∧ x = (inv_upd u e)!j"
            by blast 
          thus "e ! n ≤ x " using leq
            by auto 
        qed

        hence "e!n ≤ (min_list (nths (inv_upd u e) A))"
          using min_eq_Min
          by metis 
        thus ?thesis
          using calculation by auto 
      next
        case plus_one
        hence A: "(λ(m,up). (case up of 
                zero ⇒(if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (n,(u!n)) = (e!n) -1"
          by simp 
        have "(List.enumerate 0 u)!n = (n,(u!n))"
          using ‹n < length e› assms(1) nth_enumerate_eq
          by (metis add_0)
        hence "(e!n) -1 ∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using plus_one nth_map A
          by (metis (no_types, lifting) ‹n < length e› assms(1) length_enumerate length_map nth_mem)
        hence leq: "(e!n) -1 ≤ Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using Max_ge by simp

        have "e ! n ≤ ((e!n)-1)+1"
          by (metis dual_order.trans eSuc_minus_1 eSuc_plus_1 le_iff_add linorder_le_cases plus_1_eSuc(1))
        also have "... ≤ ( Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0) | 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0)|
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))) +1" using leq
          by simp 
        also have "... = (inv_upd u e) ! n  +1"
          using apply_inv_component.simps unfolded_apply_inv by presburger
        also have "... = upd u (inv_upd u e) ! n"
          using unfolded_apply_update plus_one  by auto 
        finally show ?thesis .
      qed
    qed
  qed 
qed


lemma apply_inv_is_min:
  assumes "length u = length e" and "valid_update u"
  shows "energy_Min (possible_inv u e) = {inv_upd u e}"
proof
  have apply_inv_leq_possible_inv: "∀e'∈(possible_inv u e). (inv_upd u e) e≤ e'"
  proof 
    fix e'
    assume "e' ∈ possible_inv u e"
    hence "energy_leq e (the (apply_update u e'))" by auto
    hence B: "∀n < length e. e! n ≤ (the (apply_update u e')) ! n" unfolding energy_leq_def by auto

    from‹e' ∈ possible_inv u e› have "apply_update u e' ≠ None" by simp
    have geq_0:  "⋀i. i < length u ⟹ u!i = minus_one ⟹ e'!i >0"
    proof-
      fix i
      assume "i < length u" and "u!i = minus_one"
      have " e'!i =0 ⟹ False"
      proof-
        assume "e'!i =0"
        hence "apply_component i minus_one e' = None"
          by simp 
        hence "apply_component i (u!i) e' = None"
          using ‹u!i = minus_one› by simp

        from ‹apply_update u e' ≠ None› have "those (map (λi. apply_component i (u ! i) e') [0..<length e'])≠ None" unfolding apply_update.simps
          by meson 
        hence "(map (λi. apply_component i (u ! i) e') [0..<length e']) ! i ≠ None" using those_all_Some
          by (metis ‹apply_update u e' ≠ None› ‹i < length u› apply_update.simps length_map map_nth)
        hence "(λi. apply_component i (u ! i) e') ([0..<length e'] ! i) ≠ None" using nth_map
          by (metis ‹apply_update u e' ≠ None› ‹i < length u› apply_update.simps length_map map_nth) 
        hence "apply_component i (u ! i) e' ≠ None"
          by (metis ‹apply_update u e' ≠ None› ‹i < length u› apply_update.elims nth_upt plus_nat.add_0)
        thus "False"
          using ‹apply_component i (u!i) e' = None› by simp
      qed

      then show " e'!i >0"
        by auto
    qed
      

    show "energy_leq (the (apply_inv_update u e)) e'" unfolding energy_leq_def 
    proof
      show "length (the (apply_inv_update u e)) = length e'" using assms
        by (metis (mono_tags, lifting) ‹e' ∈ possible_inv u e› energy_leq_def len_appl len_inv_appl mem_Collect_eq) 
      show "∀n<length (the (apply_inv_update u e)). the (apply_inv_update u e) ! n ≤ e' ! n" 
      proof
        fix n 
        show " n < length (the (apply_inv_update u e)) ⟶ the (apply_inv_update u e) ! n ≤ e' ! n" 
        proof
          assume "n < length (the (apply_inv_update u e))"
          have "the (apply_inv_update u e) ! n = (map (λn. apply_inv_component n u e) [0..<length e]) ! n" using apply_inv_update.simps
            by (metis assms(1) option.sel)
          also have "... = apply_inv_component n u e"
            by (metis ‹n < length (the (apply_inv_update u e))› assms(1) len_inv_appl minus_nat.diff_0 nth_map_upt plus_nat.add_0)
          also have "... =  Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0)| 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))" using apply_inv_component.simps by auto
          finally have inv_max: "the (apply_inv_update u e) ! n = Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0)| 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u)))".

          from B have "e ! n ≤ (the (apply_update u e')) ! n" using ‹n < length (the (apply_inv_update u e))›
            using assms(1) len_inv_appl by auto 
          hence upd_v: "e ! n ≤ the (apply_component n (u ! n) e')" using apply_to_comp_n
            using ‹length (the (apply_inv_update u e)) = length e'› ‹n < length (the (apply_inv_update u e))› ‹e' ∈ possible_inv u e› by auto 

          have Max_iff: "(Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0)| 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u))) ≤ e' ! n)
                = (∀a∈ (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth e n) else 0)| 
                minus_one ⇒ (if n=m then (nth e n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth e m) else 0) |
                plus_one ⇒ (if n=m then (nth e n)-1 else 0))) (List.enumerate 0 u))). a ≤ e' ! n)"
          proof(rule Max_le_iff)
            show "finite (set (map (λ(m, y). case y of zero ⇒ if n = m then e ! n else 0 | minus_one ⇒ if n = m then e ! n + 1 else 0 | min_set A ⇒ if n ∈ A then e ! m else 0 | plus_one ⇒ if n = m then e ! n - 1 else 0) (List.enumerate 0 u)))"
              by simp
            show "set (map (λ(m, y). case y of zero ⇒ if n = m then e ! n else 0 | minus_one ⇒ if n = m then e ! n + 1 else 0 | min_set A ⇒ if n ∈ A then e ! m else 0 | plus_one ⇒ if n = m then e ! n - 1 else 0) (List.enumerate 0 u)) ≠ {} "
              by (metis (no_types, lifting) ‹n < length (inv_upd u e)› assms(1) empty_iff len_inv_appl length_enumerate length_map nth_mem)
          qed


          show "the (apply_inv_update u e) ! n ≤ e' ! n"
            unfolding inv_max Max_iff
          proof
            fix a 
            assume "a ∈(set (map (λ(m, up). case up of zero ⇒ if n = m then e ! n else 0 | minus_one ⇒ if n = m then e ! n + 1 else 0 | min_set A ⇒ if n ∈ A then e ! m else 0 | plus_one ⇒ if n = m then e ! n - 1 else 0) (List.enumerate 0 u)))"
            hence "∃i. i< length (List.enumerate 0 u) ∧ a = (λ(m, up). case up of zero ⇒ if n = m then e ! n else 0 | minus_one ⇒ if n = m then e ! n + 1 else 0 | min_set A ⇒ if n ∈ A then e ! m else 0 | plus_one ⇒ if n = m then e ! n - 1 else 0) ((List.enumerate 0 u) ! i) " 
              using set_map
              by (metis (no_types, lifting) in_set_conv_nth length_map nth_map)
            from this obtain m where A: "a =  (λ(m, up). case up of zero ⇒ if n = m then e ! n else 0 | minus_one ⇒ if n = m then e ! n + 1 else 0 | min_set A ⇒ if n ∈ A then e ! m else 0 | plus_one ⇒ if n = m then e ! n - 1 else 0) (m, (u!m))"
              and "m < length u"
              using nth_enumerate_eq by fastforce

            consider (zero) "u ! m = zero" | (minus_one) "u ! m = minus_one" | (min) "∃A. u !m = min_set A" | (plus_one) "u!m = plus_one"
              using update_component.exhaust by auto
            then show " a ≤ e' ! n " proof(cases)
              case zero
              hence A: "a= (if n = m then e ! n  else 0)" using A by simp
              then show ?thesis
              proof(cases "n=m")
                case True
                hence "a= e!n" using zero A by simp
                also have "... ≤ the (apply_component n (u ! n) e')" using upd_v by simp
                also have "... = the (apply_component n zero e')" using zero True by simp
                also have  "... = e'!n"
                  by simp
                finally show ?thesis by simp
              next
                case False
                then show ?thesis using zero A by simp
              qed
            next
              case minus_one
              hence A: "a= (if n = m then e ! n + 1 else 0)" using A by simp
              then show ?thesis 
              proof(cases "n=m")
                case True
                hence "a = e!n +1" using minus_one A by simp
                also have "... ≤ (the (apply_component n (u ! n) e')) +1" using upd_v by simp
                also have "... = (the (apply_component n minus_one e')) +1" using minus_one True by simp
                also have "... = (the (if ((e' ! n) > 0) then Some ((e' ! n) - 1) 
                                    else None)) +1" using apply_component.simps
                  by auto
                also have "... = (e'!n -1) +1" using geq_0
                  using True ‹n < length (inv_upd u e)› assms(1) minus_one by fastforce 
                also have "... = e'!n"
                proof(cases "e'!n = ∞")
                  case True
                  then show ?thesis
                    by simp 
                next
                  case False
                  hence "∃b. e' ! n = enat (Suc b)" using geq_0 True ‹n < length (inv_upd u e)› assms(1) minus_one
                    by (metis len_inv_appl not0_implies_Suc not_enat_eq not_iless0 zero_enat_def)
                  from this obtain b where "e' ! n = enat (Suc b)"  by auto 
                  then show ?thesis
                    by (metis eSuc_enat eSuc_minus_1 eSuc_plus_1)
                qed

                finally show ?thesis .
              next
                case False
                then show ?thesis using minus_one A by simp
              qed
            next
              case min
              from this obtain A where "u !m = min_set A" by auto
              hence A: "a = (if n ∈ A then e ! m else 0)" using A by simp
              then show ?thesis 
              proof(cases "n ∈ A")
                case True
                hence "a = e!m" using A min by simp

                have "(set (nths e' A)) ≠ {}" using set_nths True assms
                  by (smt (verit) Collect_empty_eq ‹length (inv_upd u e) = length e'› ‹n < length (inv_upd u e)›) 
                hence "(nths e' A) ≠ []"
                  by auto 

                from B have "e! m ≤ (the (apply_update u e')) ! m"
                  using ‹m < length u› assms(1) len_inv_appl by auto 
                hence upd_v: "e ! m ≤ the (apply_component m (u ! m) e')" using apply_to_comp_n ‹m < length u›
                  by (metis ‹apply_update u e' ≠ None› ‹length (inv_upd u e) = length e'› assms(1) len_inv_appl)
                hence "e ! m ≤ the (apply_component m (min_set A) e')" using ‹u !m = min_set A› by simp
                also have "... = the (Some (min_list (nths e' A)))"
                  by simp
                also have "... = (min_list (nths e' A))"
                  by simp
                also have "... = Min (set (nths e' A))" using min_list_Min ‹(nths e' A) ≠ []›
                  by auto
                also have "... ≤ e'!n" using True Min_le
                  using ‹length (inv_upd u e) = length e'› ‹n < length (inv_upd u e)› set_nths by fastforce 
                finally show ?thesis using ‹a = e!m›
                  by simp
              next
                case False
                then show ?thesis using ‹u !m = min_set A› A by simp
              qed
            next
              case plus_one
              hence A: "a= (if n = m then e ! n - 1 else 0)" using A by simp
              then show ?thesis
              proof(cases "n=m")
                case True

                hence "a =(e!n) -1" using plus_one A by simp
                also have "... ≤ (the (apply_component n (u ! n) e')) -1" 
                proof(cases "(the (apply_component n (u ! n) e')) = 0")
                  case True
                  hence "e!n = 0" using upd_v
                    by simp
                  then show ?thesis using True
                    by auto
                next
                  case False
                  then show ?thesis 
                  proof(cases "e!n = ∞")
                    case True
                    then show ?thesis using upd_v
                      by simp
                  next
                    case False
                    then show ?thesis 
                    proof(cases "e!n =0")
                      case True
                      then show ?thesis
                        by simp
                    next
                      case False
                      hence "∃a. e!n = enat (Suc a)" using ‹ e ! n ≠ ∞›
                        by (metis enat.exhaust old.nat.exhaust zero_enat_def) 
                      then show ?thesis
                      proof(cases "(the (apply_component n (u ! n) e')) = ∞")
                        case True
                        then show ?thesis
                          by simp
                      next
                        case False
                        hence "∃b. (the (apply_component n (u ! n) e')) = enat (Suc b)" using ‹ (the (apply_component n (u ! n) e'))≠ 0›
                          by (metis enat.exhaust old.nat.exhaust zero_enat_def)
                        then show ?thesis using ‹∃a. e!n = enat (Suc a)› upd_v
                          by (metis Suc_le_eq diff_Suc_1 enat_ord_simps(1) idiff_enat_enat less_Suc_eq_le one_enat_def)
                      qed
                    qed
                  qed
                qed
                also have "... = (the (apply_component n plus_one e')) -1" using plus_one True by simp
                also have "... = the (Some ((e'!n)+1)) -1" using apply_component.simps
                  by auto
                also have "... = (e'!n +1) -1"
                  using True ‹n < length (inv_upd u e)› assms(1) plus_one by fastforce 
                also have "... = e'!n"
                proof(cases "e'!n = ∞")
                  case True
                  then show ?thesis
                    by simp
                next
                  case False
                  then show ?thesis
                    by (simp add: add.commute)
                qed

                finally show ?thesis .
              next
                case False
                then show ?thesis using plus_one A by simp
              qed
            qed
          qed        
        qed
      qed
    qed
  qed


  have apply_inv_is_possible_inv: "⋀u v. length u = length v ⟹ valid_update u ⟹ inv_upd u v ∈ possible_inv u v"
  using leq_up_inv inv_not_none_then inv_not_none by blast

  show "energy_Min (possible_inv u e) ⊆ {the (apply_inv_update u e)}" 
    using apply_inv_leq_possible_inv apply_inv_is_possible_inv energy_Min_def assms
    by (smt (verit, ccfv_SIG) Collect_cong insert_iff mem_Collect_eq subsetI) 
  show "{the (apply_inv_update u e)} ⊆ energy_Min (possible_inv u e)"
    using apply_inv_leq_possible_inv apply_inv_is_possible_inv energy_Min_def
    by (smt (verit, ccfv_SIG) ‹energy_Min (possible_inv u e) ⊆ {the (apply_inv_update u e)}› assms(1) assms(2) energy_leq.strict_trans1 insert_absorb mem_Collect_eq subset_iff subset_singletonD) 
qed

text‹
We now show that‹apply_inv_update u› is decreasing. 
›

lemma inv_up_leq: 
  assumes "apply_update u e ≠ None" and "valid_update u" 
  shows "(inv_upd u (upd u e)) e≤ e"
  unfolding energy_leq_def proof
  from assms(1) have "length e = length u"
    by (metis apply_update.simps)
  hence "length (the (apply_update u e)) = length u" using len_appl assms(1)
    by presburger
  hence "(apply_inv_update u (the (apply_update u e))) ≠ None"
    using inv_not_none by presburger 
  thus "length (the (apply_inv_update u (the (apply_update u e)))) = length e" using len_inv_appl ‹length (the (apply_update u e)) = length u› ‹length e = length u›
    by presburger
  show "∀n<length (the (apply_inv_update u (the (apply_update u e)))).
       the (apply_inv_update u (the (apply_update u e))) ! n ≤ e ! n "
  proof
    fix n 
    show "n < length (the (apply_inv_update u (the (apply_update u e)))) ⟶
         the (apply_inv_update u (the (apply_update u e))) ! n ≤ e ! n"
    proof 
      assume "n < length (the (apply_inv_update u (the (apply_update u e))))"
      hence "n < length e"
        using ‹length (the (apply_inv_update u (the (apply_update u e)))) = length e› by auto 
      show "the (apply_inv_update u (the (apply_update u e))) ! n ≤ e ! n"
      proof-
        have "the (apply_inv_update u (the (apply_update u e))) !n = (map (λn. apply_inv_component n u (the (apply_update u e))) [0..<length (the (apply_update u e))]) ! n " using apply_inv_update.simps
          using ‹length (the (apply_update u e)) = length u› ‹length e = length u› option.sel by auto 
        hence A: "the (apply_inv_update u (the (apply_update u e))) !n = apply_inv_component n u (the (apply_update u e))"
          by (metis ‹length (the (apply_inv_update u (the (apply_update u e)))) = length e› ‹length (the (apply_update u e)) = length u› ‹length e = length u› ‹n < length (the (apply_inv_update u (the (apply_update u e))))› diff_diff_left length_upt nth_map nth_upt plus_nat.add_0 zero_less_diff)
        have "apply_inv_component n u (the (apply_update u e)) ≤ e ! n" proof-

          have "∀x ∈ set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0) | 
                minus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth (the (apply_update u e)) m) else 0) |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0)
                )) (List.enumerate 0 u)). x ≤ e ! n" 
          proof
            fix x 
            assume X: "x ∈ set (map (λ(m, up).
                          case up of zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0)
                          | minus_one ⇒ if n = m then the (apply_update u e) ! n + 1 else 0
                          | min_set A ⇒ if n ∈ A then the (apply_update u e) ! m else 0|
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))
                   (List.enumerate 0 u))"
            hence "∃m < length (List.enumerate 0 u). x =  (map (λ(m, up).
                          case up of zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0)
                          | minus_one ⇒ if n = m then the (apply_update u e) ! n + 1 else 0
                          | min_set A ⇒ if n ∈ A then the (apply_update u e) ! m else 0 |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))
                   (List.enumerate 0 u)) ! m" using in_set_conv_nth
              by (metis (no_types, lifting) length_map) 
            from this obtain m where "m < length (List.enumerate 0 u)" and "x =  (map (λ(m, up).
                          case up of zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0)
                          | minus_one ⇒ if n = m then the (apply_update u e) ! n + 1 else 0
                          | min_set A ⇒ if n ∈ A then the (apply_update u e) ! m else 0 |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))
                   (List.enumerate 0 u)) ! m" by auto
            hence "x = (λ(m, up).
                          case up of zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0)
                          | minus_one ⇒ if n = m then the (apply_update u e) ! n + 1 else 0
                          | min_set A ⇒ if n ∈ A then the (apply_update u e) ! m else 0 |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))
                   ((List.enumerate 0 u) ! m)" using nth_map ‹m < length (List.enumerate 0 u)›
              by simp 
            hence X: "x= (λ(m, up).
                          case up of zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0)
                          | minus_one ⇒ if n = m then the (apply_update u e) ! n + 1 else 0
                          | min_set A ⇒ if n ∈ A then the (apply_update u e) ! m else 0 |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))
                   (m, (u ! m))"
              by (metis (no_types, lifting) ‹m < length (List.enumerate 0 u)› add_cancel_left_left length_enumerate nth_enumerate_eq)



            consider (zero) "u ! m = zero" | (minus_one) "u ! m = minus_one" | (min) "∃A. u !m = min_set A" | (plus_one) "u!m = plus_one"
              using update_component.exhaust by auto
            thus "x ≤ e ! n" proof(cases)
              case zero
              hence "x = (if n=m then (nth (the (apply_update u e)) n) else 0)" using X by simp
                then show ?thesis proof(cases "n=m")
                  case True
                  hence "x= upd u e ! n"
                    by (simp add: ‹x = (if n = m then upd u e ! n else 0)›) 
                  also have "... = the (apply_component n (u!n) e)"
                    using ‹n < length e› apply_to_comp_n assms(1) by auto 
                  also have "... = the (apply_component n zero e)" using zero True by simp
                  also have "... = e!n"
                    by simp 
                  finally show ?thesis by auto
                next
                  case False
                  hence "x= 0"
                    by (simp add: ‹x = (if n = m then upd u e ! n else 0)›)
                  then show ?thesis by simp
                qed
              next
                case minus_one
                then show ?thesis proof(cases "m=n")
                  case True
                  hence "u ! n = minus_one" using minus_one by simp
                  have "(apply_component n (u ! n) e) ≠ None"  using assms(1) those_all_Some apply_update.simps apply_component.simps ‹n < length e›
                    by (smt (verit) add_cancel_right_left length_map map_nth nth_map nth_upt)
                  hence "e ! n > 0" using ‹u ! n = minus_one› by auto
                  hence "((e!n) -1 )+1 = e!n" proof(cases "e ! n = ∞")
                    case True
                    then show ?thesis by simp
                  next
                    case False
                    hence "∃b. e ! n = enat b" by simp
                    from this obtain b where "e ! n = enat b" by auto
                    hence "∃b'. b = Suc b'" using ‹e ! n > 0›
                      by (simp add: not0_implies_Suc zero_enat_def)
                    from this obtain b' where "b = Suc b'" by auto
                    hence "e ! n = enat (Suc b')" using ‹e ! n = enat b› by simp
                    hence "(e!n)-1 = enat b'"
                      by (metis eSuc_enat eSuc_minus_1) 
                    hence "((e!n) -1 )+1 = enat (Suc b')"
                      using eSuc_enat plus_1_eSuc(2) by auto 
                    then show ?thesis using ‹e ! n = enat (Suc b')› by simp  
                  qed

                  from True have "x = (the (apply_update u e) ! n) +1" using X minus_one by simp
                  also have "... = (the (apply_component n (u ! n) e)) +1" using apply_to_comp_n assms
                    using ‹length (the (apply_inv_update u (the (apply_update u e)))) = length e› ‹n < length (the (apply_inv_update u (the (apply_update u e))))› by presburger
                  also have "... = ((e !n) -1 ) +1" using ‹u ! n = minus_one› assms those_all_Some apply_update.simps apply_component.simps
                    using ‹0 < e ! n› by auto 
                  finally have "x = e ! n" using ‹((e!n) -1 )+1 = e!n› by simp
                  then show ?thesis by simp
                next
                  case False
                  hence "x = 0" using X minus_one by simp
                  then show ?thesis
                    by simp 
                qed
              next
                case min
                from this obtain A where "u ! m = min_set A" by auto
                hence "A≠{} ∧ A ⊆ {x. x < length e}" using assms
                  by (simp add: ‹length e = length u›) 
                then show ?thesis proof(cases "n ∈ A")
                  case True
                  hence "x = the (apply_update u e) ! m" using X ‹u ! m = min_set A› by simp
                  also have "... = (the (apply_component n (u ! m) e))" using apply_to_comp_n
                    by (metis ‹length e = length u› ‹m < length (List.enumerate 0 u)› ‹u ! m = min_set A› apply_component.simps(3) assms(1) length_enumerate) 
                  also have "... = (min_list (nths e A))" using ‹u ! m = min_set A› apply_component.simps by simp
                  also have "... = Min (set (nths e A))" using ‹A≠{} ∧ A ⊆ {x. x < length e}› min_list_Min
                    by (smt (z3) True ‹n < length e› less_zeroE list.size(3) mem_Collect_eq set_conv_nth set_nths)
                  also have "... ≤ e!n" using True Min_le ‹A≠{} ∧ A ⊆ {x. x < length e}›
                    using List.finite_set ‹n < length e› set_nths by fastforce
                  finally show ?thesis .
                next
                  case False
                  hence "x = 0" using X ‹u ! m = min_set A› by simp
                  then show ?thesis by simp
                qed
              next 
                case plus_one 
                hence X: "x= (if n=m then (nth (the (apply_update u e)) n)-1 else 0)" using X
                  by simp
                then show ?thesis
                proof(cases "n=m")
                  case True
                  hence X: "x=(nth (the (apply_update u e)) n)-1" using X by simp

                  have "nth (the (apply_update u e)) n = the (apply_component n (u!n) e)" using apply_update.simps
                    using ‹n < length e› apply_to_comp_n assms(1) by auto 
                  also have "... = the (apply_component n plus_one e)" using plus_one True by simp
                  also have "... = (e ! n + 1)" unfolding apply_component.simps
                    by simp 
                  finally have "x = (e ! n + 1)-1" using X
                    by simp 
                  then show ?thesis
                    by (simp add: add.commute) 
                next
                  case False
                  hence "x = 0" using X plus_one by simp
                  then show ?thesis by simp
                qed
              qed
            qed

          hence leq: "∀x ∈(set (map (λ(m,up). (case up of 
                zero ⇒(if n=m then (nth (the (apply_update u e)) n) else 0) | 
                minus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth (the (apply_update u e)) m) else 0) |
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))) (List.enumerate 0 u))). x ≤ e ! n" by blast

          have "apply_inv_component n u (the (apply_update u e)) =  Max (set (map (λ(m,up). (case up of 
                zero ⇒ (if n=m then (nth (the (apply_update u e)) n) else 0) | 
                minus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)+1 else 0) |
                min_set A ⇒ (if n∈A then (nth (the (apply_update u e)) m) else 0)|
                plus_one ⇒ (if n=m then (nth (the (apply_update u e)) n)-1 else 0))) (List.enumerate 0 u)))" using apply_inv_component.simps
            by blast 
          also have "... ≤ e! n" using leq Max_le_iff
            by (smt (verit) List.finite_set ‹length e = length u› ‹n < length e› empty_iff length_enumerate length_map nth_mem)
          finally show ?thesis .
        qed
        thus ?thesis using A by presburger 
      qed
    qed
  qed
qed



text‹We now conclude that for any valid update the functions $e \mapsto  \min \lbrace e' \ | \ e \leq u(e') \rbrace$ and $u$ form a 
Galois connection between the domain of $u$ and the set of energies of the same length as $u$ w.r.t 
to the component-wise order.›

lemma galois_connection:
  assumes "apply_update u e' ≠ None" and "length e = length e'" and 
          "valid_update u"
  shows "(inv_upd u e) e≤ e' = e e≤ (upd u e')"
proof
  show "energy_leq (the (apply_inv_update u e)) e' ⟹ energy_leq e (upd u e')" 
  proof- 
    assume A: "energy_leq (the (apply_inv_update u e)) e'" 
    from assms(1) have "length u = length e" using apply_update.simps assms(2) by metis
    hence leq: "energy_leq e (the (apply_update u (the (apply_inv_update u e))))" using leq_up_inv assms(3) inv_not_none
      by presburger
    have "(apply_update u (the (apply_inv_update u e))) ≠ None" using ‹length u = length e›
      using inv_not_none inv_not_none_then by blast
    hence "energy_leq (the (apply_update u (the (apply_inv_update u e)))) (the (apply_update u e'))" using A updates_monotonic
      using ‹length u = length e› assms(3) inv_not_none len_inv_appl by presburger  
    thus "energy_leq e (the (apply_update u e'))" using leq
      using energy_leq.trans by blast 
  qed
  show "energy_leq e (the (apply_update u e')) ⟹ energy_leq (the (apply_inv_update u e)) e' " 
  proof-
    assume A: "energy_leq e (the (apply_update u e'))"
    have "apply_inv_update u e ≠ None" using assms
      by (metis apply_update.simps inv_not_none) 
    have "length u = length e" using assms
      by (metis apply_update.elims) 
    from A have "e' ∈ possible_inv u e"
      using assms(1) mem_Collect_eq by auto
    thus "energy_leq (the (apply_inv_update u e)) e'" using apply_inv_is_min assms ‹length u = length e› energy_Min_def
      by (smt (verit) A Collect_cong energy_leq.strict_trans1 inv_up_leq inverse_monotonic len_appl) 
  qed
qed

end