Theory Energy

text ‹\newpage›
section ‹Energy›
theory Energy
  imports Main "HOL-Library.Extended_Nat"
begin
text ‹Following the paper \cite[p. 5]{bisping2023lineartimebranchingtime}, we define energies as
      eight-dimensional vectors of natural numbers extended by @{text ‹∞›}.
      But deviate from \cite{bisping2023lineartimebranchingtime} in also defining
      an energy @{text ‹eneg›} that represents negative energy. This allows us to
      express energy updates (cf. \cite[p. 8]{bisping2023lineartimebranchingtime}) as total functions\label{deviation:eneg}.›
datatype energy = E (modal_depth: ‹enat›) (br_conj_depth: ‹enat›) (conj_depth: ‹enat›) (st_conj_depth: ‹enat›)
                    (imm_conj_depth: ‹enat›) (pos_conjuncts: ‹enat›) (neg_conjuncts: ‹enat›) (neg_depth: ‹enat›)

subsection ‹Ordering Energies›
text ‹In order to define subtraction on energies, we first lift the orderings
      @{text ‹≤›} and @{text ‹<›} from @{type ‹enat›} to @{type ‹energy›}.›
instantiation energy :: order begin

definition ‹e1 ≤ e2 ≡
  (case e1 of E a1 b1 c1 d1 e1 f1 g1 h1 ⇒ (
    case e2 of E a2 b2 c2 d2 e2 f2 g2 h2 ⇒
      (a1 ≤ a2 ∧ b1 ≤ b2 ∧ c1 ≤ c2 ∧ d1 ≤ d2 ∧ e1 ≤ e2 ∧ f1 ≤ f2 ∧ g1 ≤ g2 ∧ h1 ≤ h2)
    ))›

definition ‹(x::energy) < y = (x ≤ y ∧ ¬ y ≤ x)›

text ‹Next, we show that this yields a reflexive transitive antisymmetric order.›

instance proof
  fix e1 e2 e3 :: energy
  show ‹e1 ≤ e1› unfolding less_eq_energy_def by (simp add: energy.case_eq_if)
  show ‹e1 ≤ e2 ⟹ e2 ≤ e3 ⟹ e1 ≤ e3› unfolding less_eq_energy_def
    by (smt (z3) energy.case_eq_if order_trans)
  show ‹e1 < e2 = (e1 ≤ e2 ∧ ¬ e2 ≤ e1)› using less_energy_def .
  show ‹e1 ≤ e2 ⟹ e2 ≤ e1 ⟹ e1 = e2› unfolding less_eq_energy_def
    by (smt (z3) energy.case_eq_if energy.expand nle_le)
qed


lemma leq_components[simp]:
  shows ‹e1 ≤ e2 ≡ (modal_depth e1 ≤ modal_depth e2 ∧ br_conj_depth e1 ≤ br_conj_depth e2 ∧ conj_depth e1 ≤ conj_depth e2 ∧
                     st_conj_depth e1 ≤ st_conj_depth e2 ∧ imm_conj_depth e1 ≤ imm_conj_depth e2 ∧ pos_conjuncts e1 ≤ pos_conjuncts e2 ∧
                     neg_conjuncts e1 ≤ neg_conjuncts e2 ∧ neg_depth e1 ≤ neg_depth e2)›
  unfolding less_eq_energy_def by (simp add: energy.case_eq_if)

lemma energy_leq_cases:
  assumes ‹modal_depth e1 ≤ modal_depth e2› ‹br_conj_depth e1 ≤ br_conj_depth e2› ‹conj_depth e1 ≤ conj_depth e2›
          ‹st_conj_depth e1 ≤ st_conj_depth e2› ‹imm_conj_depth e1 ≤ imm_conj_depth e2› ‹pos_conjuncts e1 ≤ pos_conjuncts e2›
          ‹neg_conjuncts e1 ≤ neg_conjuncts e2› ‹neg_depth e1 ≤ neg_depth e2›
  shows ‹e1 ≤ e2› using assms unfolding leq_components by blast

end

text ‹We then use this order to define a predicate that decides if an @{term ‹e1 :: energy›}
      may be subtracted from another @{term ‹e2 :: energy›} without the result being negative. We encode this by @{term ‹e1›} being @{text ‹somewhere_larger›} than @{term ‹e2›}.›

abbreviation somewhere_larger where ‹somewhere_larger e1 e2 ≡ ¬(e1 ≥ e2)›

lemma somewhere_larger_eq:
  assumes ‹somewhere_larger e1 e2›
  shows ‹modal_depth e1 < modal_depth e2 ∨ br_conj_depth e1 < br_conj_depth e2
         ∨ conj_depth e1 < conj_depth e2 ∨ st_conj_depth e1 < st_conj_depth e2 ∨ imm_conj_depth e1 < imm_conj_depth e2
         ∨ pos_conjuncts e1 < pos_conjuncts e2 ∨ neg_conjuncts e1 < neg_conjuncts e2 ∨ neg_depth e1 < neg_depth e2›
  by (smt (z3) assms energy.case_eq_if less_eq_energy_def linorder_le_less_linear)

subsection ‹Subtracting Energies›
text ‹Using ‹somewhere_larger› we define subtraction as
  the @{text ‹minus›} operator on energies.›

instantiation energy :: minus
begin

definition minus_energy_def[simp]: ‹e1 - e2 ≡ E
  ((modal_depth e1) - (modal_depth e2))
  ((br_conj_depth e1) - (br_conj_depth e2))
  ((conj_depth e1) - (conj_depth e2))
  ((st_conj_depth e1) - (st_conj_depth e2))
  ((imm_conj_depth e1) - (imm_conj_depth e2))
  ((pos_conjuncts e1) - (pos_conjuncts e2))
  ((neg_conjuncts e1) - (neg_conjuncts e2))
  ((neg_depth e1) - (neg_depth e2))›

instance ..

end

text ‹Afterwards, we prove some lemmas to ease the manipulation of expressions
  using subtraction on energies.›
lemma energy_minus[simp]:
  shows ‹E a1 b1 c1 d1 e1 f1 g1 h1 - E a2 b2 c2 d2 e2 f2 g2 h2
         = E (a1 - a2) (b1 - b2) (c1 - c2) (d1 - d2)
             (e1 - e2) (f1 - f2) (g1 - g2) (h1 - h2)›
  unfolding minus_energy_def somewhere_larger_eq by simp

lemma minus_component_leq:
  assumes ‹s ≤ x› ‹x ≤ y›
  shows ‹modal_depth (x - s) ≤ modal_depth (y - s)› ‹br_conj_depth (x - s) ≤ br_conj_depth (y - s)›
        ‹conj_depth (x - s) ≤ conj_depth (y - s)› ‹st_conj_depth (x - s) ≤ st_conj_depth (y - s)›
        ‹imm_conj_depth (x - s) ≤ imm_conj_depth (y - s)› ‹pos_conjuncts (x - s) ≤ pos_conjuncts (y -s)›
        ‹neg_conjuncts (x - s) ≤ neg_conjuncts (y - s)› ‹neg_depth (x - s) ≤ neg_depth (y - s)›
proof-
  from assms have ‹s ≤ y› by (simp del: leq_components)
  with assms leq_components have
    ‹modal_depth (x - s) ≤ modal_depth (y - s) ∧ br_conj_depth (x - s) ≤ br_conj_depth (y - s) ∧
    conj_depth (x - s) ≤ conj_depth (y - s) ∧ st_conj_depth (x - s) ≤ st_conj_depth (y - s) ∧
    imm_conj_depth (x - s) ≤ imm_conj_depth (y - s) ∧ pos_conjuncts (x - s) ≤ pos_conjuncts (y -s) ∧
    neg_conjuncts (x - s) ≤ neg_conjuncts (y - s) ∧ neg_depth (x - s) ≤ neg_depth (y - s)›
    by (smt (verit, del_insts) add_diff_cancel_enat enat_add_left_cancel_le energy.sel
        leD le_iff_add le_less minus_energy_def)+
  thus
    ‹modal_depth (x - s) ≤ modal_depth (y - s)› ‹br_conj_depth (x - s) ≤ br_conj_depth (y - s)›
    ‹conj_depth (x - s) ≤ conj_depth (y - s)› ‹st_conj_depth (x - s) ≤ st_conj_depth (y - s)›
    ‹imm_conj_depth (x - s) ≤ imm_conj_depth (y - s)› ‹pos_conjuncts (x - s) ≤ pos_conjuncts (y -s)›
    ‹neg_conjuncts (x - s) ≤ neg_conjuncts (y - s)› ‹neg_depth (x - s) ≤ neg_depth (y - s)› by auto
qed

lemma enat_diff_mono:
  assumes ‹(i::enat) ≤ j›
  shows ‹i - k ≤ j - k›
proof (cases i)
  case (enat iN)
  show ?thesis
  proof (cases j)
    case (enat jN)
    then show ?thesis
      using assms enat_ile by (cases k, fastforce+)
  next
    case infinity
    then show ?thesis using assms by auto
  qed
next
  case infinity
  hence ‹j = ∞›
    using assms by auto
  then show ?thesis by auto
qed

text ‹We further show that the subtraction of energies is decreasing.›
lemma energy_diff_mono:
  fixes s :: energy
  shows ‹mono_on UNIV (λx. x - s)›
  unfolding mono_on_def
  by (auto simp add: enat_diff_mono)

lemma gets_smaller:
  fixes s :: energy
  shows ‹(λx. x - s) x ≤ x›
  by (auto)
     (metis add.commute add_diff_cancel_enat enat_diff_mono idiff_infinity idiff_infinity_right le_iff_add not_infinity_eq zero_le)+

lemma mono_subtract:
  assumes ‹x ≤ x'›
  shows ‹(λx. x - (E a b c d e f g h)) x ≤ (λx. x - (E a b c d e f g h)) x'›
  using assms enat_diff_mono by force

text ‹We also define abbreviations for performing subtraction.›
abbreviation ‹subtract_fn a b c d e f g h ≡
  (λx. if somewhere_larger x (E a b c d e f g h) then None else Some (x - (E a b c d e f g h)))›

abbreviation ‹subtract a b c d e f g h ≡ Some (subtract_fn a b c d e f g h)›

subsection ‹Minimum Updates›
text ‹Next, we define two energy updates that replace the first component with the minimum of two other components.›
definition ‹min1_6 e ≡ case e of E a b c d e f g h ⇒ Some (E (min a f) b c d e f g h)›
definition ‹min1_7 e ≡ case e of E a b c d e f g h ⇒ Some (E (min a g) b c d e f g h)›


text ‹lift order to options›
instantiation option :: (order) order
begin

definition less_eq_option_def[simp]:
  ‹less_eq_option (optA :: 'a option) optB ≡
    case optA of
      (Some a) ⇒
        (case optB of
          (Some b) ⇒ a ≤ b |
          None ⇒ False) |
      None ⇒ True›

definition less_option_def[simp]:
  ‹less_option (optA :: 'a option) optB ≡ (optA ≤ optB ∧ ¬ optB ≤ optA)›

instance proof standard
  fix x y::‹'a option›
  show ‹(x < y) = (x ≤ y ∧ ¬ y ≤ x)› by simp
next
  fix x::‹'a option›
  show ‹x ≤ x›
    by (simp add: option.case_eq_if)
next
  fix x y z::‹'a option›
  assume ‹x ≤ y› ‹y ≤ z›
  thus ‹x ≤ z›
    unfolding less_eq_option_def
    by (metis option.case_eq_if order_trans)
next
  fix x y::‹'a option›
  assume ‹ x ≤ y› ‹y ≤ x›
  thus ‹x = y›
    unfolding less_eq_option_def
    by (smt (z3) inf.absorb_iff2 le_boolD option.case_eq_if option.split_sel order_antisym)
qed

end

text ‹Again, we prove that these updates only decrease energies.›

lemma min_1_6_simps[simp]:
  shows ‹modal_depth (the (min1_6 e)) = min (modal_depth e) (pos_conjuncts e)›
        ‹br_conj_depth (the (min1_6 e)) = br_conj_depth e›
        ‹conj_depth (the (min1_6 e)) = conj_depth e›
        ‹st_conj_depth (the (min1_6 e)) = st_conj_depth e›
        ‹imm_conj_depth (the (min1_6 e)) = imm_conj_depth e›
        ‹pos_conjuncts (the (min1_6 e)) = pos_conjuncts e›
        ‹neg_conjuncts (the (min1_6 e)) = neg_conjuncts e›
        ‹neg_depth (the (min1_6 e)) = neg_depth e›
  unfolding min1_6_def by (simp_all add: energy.case_eq_if)

lemma min_1_7_simps[simp]:
  shows ‹modal_depth (the (min1_7 e)) = min (modal_depth e) (neg_conjuncts e)›
        ‹br_conj_depth (the (min1_7 e)) = br_conj_depth e›
        ‹conj_depth (the (min1_7 e)) = conj_depth e›
        ‹st_conj_depth (the (min1_7 e)) = st_conj_depth e›
        ‹imm_conj_depth (the (min1_7 e)) = imm_conj_depth e›
        ‹pos_conjuncts (the (min1_7 e)) = pos_conjuncts e›
        ‹neg_conjuncts (the (min1_7 e)) = neg_conjuncts e›
        ‹neg_depth (the (min1_7 e)) = neg_depth e›
  unfolding min1_7_def by (simp_all add: energy.case_eq_if)

lemma min_1_6_some:
  shows ‹min1_6 e ≠ None›
  unfolding min1_6_def
  using energy.case_eq_if by blast

lemma min_1_7_some:
  shows ‹min1_7 e ≠ None›
  unfolding min1_7_def
  using energy.case_eq_if by blast

lemma mono_min_1_6:
  shows ‹mono (the ∘ min1_6)›
proof
  fix x y :: energy
  assume ‹x ≤ y›
  thus ‹(the ∘ min1_6) x ≤ (the ∘ min1_6) y› unfolding leq_components
    using min.mono min_1_6_simps min1_6_def by auto
qed

lemma mono_min_1_7:
  shows ‹mono (the ∘ min1_7)›
proof
  fix x y :: energy
  assume ‹x ≤ y›
  thus ‹(the ∘ min1_7) x ≤ (the ∘ min1_7) y› unfolding leq_components
    using min.mono min_1_7_simps min1_7_def by auto
qed

lemma gets_smaller_min_1_6:
  shows ‹the (min1_6 x) ≤ x›
  using min_1_6_simps min_less_iff_conj somewhere_larger_eq by fastforce


lemma gets_smaller_min_1_7:
  shows ‹the (min1_7 x) ≤ x›
  using min_1_7_simps min_less_iff_conj somewhere_larger_eq by fastforce

lemma min_1_7_lower_end:
  assumes ‹(Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) = None›
  shows ‹neg_depth e = 0›
  using assms
  by (smt (verit) bind.bind_lunit energy.sel ileI1 leq_components min_1_7_some not_gr_zero one_eSuc zero_le)

lemma min_1_7_subtr_simp:
  shows ‹(Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)
    = (if neg_depth e = 0 then None
        else Some (E (min (modal_depth e) (neg_conjuncts e)) (br_conj_depth e) (conj_depth e) (st_conj_depth e) (imm_conj_depth e) (pos_conjuncts e) (neg_conjuncts e) (neg_depth e - 1)))›
  using min_1_7_lower_end
  by (auto simp add: min1_7_def)

lemma min_1_7_subtr_mono:
  shows ‹mono (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)›
proof
  fix e1 e2 :: energy
  assume ‹e1 ≤ e2›
  thus ‹(λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) e1
    ≤  (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) e2›
    unfolding min_1_7_subtr_simp
    by (auto simp add: min.coboundedI1  min.coboundedI2 enat_diff_mono)
qed

lemma min_1_6_subtr_simp:
  shows ‹(Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)
    = (if br_conj_depth e = 0 ∨ conj_depth e = 0 then None
        else Some (E (min (modal_depth e) (pos_conjuncts e)) (br_conj_depth e - 1) (conj_depth e - 1) (st_conj_depth e) (imm_conj_depth e) (pos_conjuncts e) (neg_conjuncts e) (neg_depth e)))›
  by (auto simp add: min1_6_def ileI1 one_eSuc)

instantiation energy :: Sup
begin

definition ‹Sup ee ≡ E (Sup (modal_depth ` ee)) (Sup (br_conj_depth ` ee )) (Sup (conj_depth ` ee)) (Sup (st_conj_depth ` ee))
  (Sup (imm_conj_depth ` ee)) (Sup (pos_conjuncts ` ee)) (Sup (neg_conjuncts ` ee)) (Sup (neg_depth ` ee))›

instance ..
end


end