Theory Sepreftime_Auxiliaries

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




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"
  apply(cases a; cases b; cases a') by auto

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

lemma enat_plus_minus_aux2: "¬ a < a' ⟹ b ≤ a - a' ⟹ a' + b ≤ (a::enat)"
  apply(cases a; cases b; cases a') by 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"
  apply(cases x2; cases x2a) apply auto apply(cases a) by auto

lemma helper2: "x2b ≤ x2 ⟹ ¬ x2a < x2  ⟹ ¬ x2a < x2b ⟹ x2a - (x2::enat) ≤ x2a - x2b"
  apply(cases x2; cases x2a) apply auto apply(cases x2b) by 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)"
  unfolding  Sup_enat_def using    finite_enat_bounded linear 
  apply(auto split: if_splits)  
   apply (smt Max_in empty_iff enat_ord_code(4))
  by (smt not_less)  


lemma [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)"
  apply (cases "M x"; auto simp: aux11)
  by force

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: "(SUP f:{[x ↦ t1] |x t1. M x = Some t1}. f x) = M x"
  unfolding Sup_option_def  
  apply (simp add: aux2) 
  apply (auto simp: aux3)
  by (metis (mono_tags, lifting) Some_image_these_eq Sup_least in_these_eq mem_Collect_eq sup_absorb1 these_image_Some_eq)


lemma SUP_eq_None_iff: "(SUP 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: "(SUP f:X. f x) = Some t ⟷ (∃f∈X. f x ≠ None) ∧ (t=Sup {t' | f t'. f∈X ∧ f x = Some t' })"
  apply auto
  subgoal 
    by (smt Sup_bot_conv(1) Sup_empty Sup_option_def Sup_pointwise_eq_fun imageE option.distinct(1))
  subgoal 
    unfolding Sup_option_def
    apply (clarsimp split: if_splits)
    apply (fo_rule arg_cong)
    apply (auto simp: Option.these_def)
    apply (metis (mono_tags, lifting) image_iff mem_Collect_eq option.sel)
    apply (metis (mono_tags, lifting) image_iff mem_Collect_eq option.sel)
    done
  subgoal 
    unfolding Sup_option_def
    apply (clarsimp split: if_splits; safe)
    subgoal by (force simp: image_iff)
    apply (fo_rule arg_cong)
    apply (auto simp: Option.these_def)
    apply (metis (mono_tags, lifting) image_iff mem_Collect_eq option.sel)
    done
  done  



lemma Sup_enat_less: "X ≠ {} ⟹ enat t ≤ Sup X ⟷ (∃x∈X. enat t ≤ x)"
  apply rule
  subgoal 
  by (metis Max_in Sup_enat_def finite_enat_bounded linear) 
  subgoal apply auto
    by (simp add: Sup_upper2)
  done


(* 
  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