Theory NREST_Auxiliaries

theory 
  NREST_Auxiliaries
imports
  "HOL-Library.Extended_Nat" "Automatic_Refinement.Automatic_Refinement"
begin

unbundle lattice_syntax

section "Auxiliaries"

subsection "Auxiliaries for option"

lemma less_eq_option_None_is_None': "x ≤ None ⟷ x = None"
  by(auto simp: less_eq_option_None_is_None)

lemma everywhereNone: "(∀x∈X. x = None) ⟷ X = {} ∨ X = {None}"
  by auto

subsection "Auxiliaries for enat"

lemma enat_minus_mono: "a' ≥ b ⟹ a' ≥ a ⟹ a' - b ≥ (a::enat) - b"
  by (cases a; cases b; cases a') auto

lemma enat_plus_minus_aux1: "a + b ≤ a' ⟹ ¬ a' < a ⟹ b ≤ a' - (a::enat)"
  by (cases a; cases b; cases a') auto

lemma enat_plus_minus_aux2: "¬ a < a' ⟹ b ≤ a - a' ⟹ a' + b ≤ (a::enat)"
  by (cases a; cases b; cases a') auto

lemma enat_minus_inf_conv[simp]: "a - enat n = ∞ ⟷ a=∞" by (cases a) auto
lemma enat_minus_fin_conv[simp]: "a - enat n = enat m ⟷ (∃k. a=enat k ∧ m = k - n)"
  by (cases a) auto

lemma helper: "x2 ≤ x2a ⟹ ¬ x2 < a ⟹ ¬ x2a < a ⟹  x2 - (a::enat) ≤ x2a - a"
  by (cases x2; cases x2a; cases a) auto

lemma helper2: "x2b ≤ x2 ⟹ ¬ x2a < x2  ⟹ ¬ x2a < x2b ⟹ x2a - (x2::enat) ≤ x2a - x2b"
  by (cases x2; cases x2a; cases x2b) auto

lemma Sup_finite_enat: "Sup X = Some (enat a) ⟹ Some (enat a) ∈ X"
  by (auto simp: Sup_option_def Sup_enat_def these_empty_eq Max_eq_iff in_these_eq split: if_splits)

lemma Sup_enat_less2: "Sup X = ∞ ⟹ ∃x∈X. enat t < x"
  by (subst less_Sup_iff[symmetric]) simp

lemma enat_upper[simp]: "t ≤ Some (∞::enat)"
  by (cases t, auto)

subsection "Auxiliary (for Sup and Inf)"

lemma aux11: "f`X={y} ⟷ (X≠{} ∧ (∀x∈X. f x = y))" by auto
 
lemma aux2: "(λf. f x) ` {[x ↦ t1] |x t1. M x = Some t1} = {None} ⟷ (M x = None ∧ M≠Map.empty)"
  by (cases "M x"; force simp: aux11)

lemma aux3: "(λf. f x) ` {[x ↦ t1] |x t1. M x = Some t1}
  = {Some t1 | t1. M x = Some t1} ∪ ({None | y. y≠x ∧ M y ≠ None })"
  by (fastforce split: if_splits simp: image_iff) 

lemma Sup_pointwise_eq_fun: "(⨆f ∈ {[x ↦ t1] |x t1. M x = Some t1}. f x) = M x"
proof(cases "M x")
  case None
  then show ?thesis 
    by (auto simp add: Sup_option_def aux2 split: if_splits)
next
  case (Some a)
  have s: "Option.these {u. u = None ∧ (∃y. y ≠ x ∧ (∃ya. M y = Some ya))} = {}"
    by (auto simp add: in_these_eq)
  from Some show ?thesis
    by (auto simp add: Sup_option_def s aux3 split: if_splits)
qed

lemma SUP_eq_None_iff: "(⨆f ∈ X. f x) = None ⟷ X={} ∨ (∀f∈X. f x = None)"
  by (smt SUP_bot_conv(2) SUP_empty Sup_empty empty_Sup)

lemma SUP_eq_Some_iff:
  "(⨆f ∈ X. f x) = Some t ⟷ (∃f∈X. f x ≠ None) ∧ (t=Sup {t' | f t'. f∈X ∧ f x = Some t' })"
proof safe 
  show "(⨆f∈X. f x) = Some t ⟹ ∃f∈X. f x ≠ None"
    by (metis SUP_eq_None_iff option.distinct(1))
qed (fastforce intro!: arg_cong[where f=Sup] simp: image_iff Option.these_def Sup_option_def split: option.splits if_splits)+



lemma Sup_enat_less: "X ≠ {} ⟹ enat t ≤ Sup X ⟷ (∃x∈X. enat t ≤ x)"
  using finite_enat_bounded by (simp add: Max_ge_iff Sup_upper2 Sup_enat_def) (meson nle_le)

(* 
  This is how implication can be phrased with an Inf operation.
  Generalization from boolean to enat can be explained this way.
 *)

lemma fixes Q P  shows
    "Inf { P x ≤ Q x |x. True}  ⟷ P ≤ Q" 
  unfolding le_fun_def by simp

end