Theory NREST_Type_Classes

✐‹creator "Maximilian P. L. Haslbeck"›
✐‹contributor "Peter Lammich"›
section ‹Type Class needed for currency refine and backwards reasoning gwp›
theory NREST_Type_Classes
imports NREST
begin

paragraph ‹Summary›
text ‹This theory collects the properties a resource type needs to allow for currency refinement
  and backwards reasoning.›

subsection ‹Type class for currency refinement›

text ‹this is needed for monotonicity of Sum_any›

class nonneg = ord + zero +
  assumes needname_nonneg: "0 ≤ x"

subsection ‹Algebraic structure needed for backwards reasoning›



lemma le_None: "t ≤ None ⟷ t = None" apply(cases t) apply auto done


lemma enat_1: "top - a = (top::enat)"
  apply(cases a) by (auto simp: top_enat_def)
lemma enat_2: "a - (b + c) = a - c - (b::enat)" 
  apply(cases a;cases b;cases c) by (auto)  
lemma enat_3: "  ⟦a + b ≤ c;   b ≤ (c::enat) ⟧ ⟹  a ≤ c - b"
  apply(cases a; cases b; cases c) by auto
lemma enat_4: "a + b ≤ c⟹  b ≤ (c::enat)"
  apply(cases a; cases b; cases c) by auto
lemma enat_5: "⟦t1 ≤ b - a; aa ≤ b - a - t1; a ≤ b⟧ ⟹ t1 + a ≤ (b::enat)"
  apply(cases t1; cases b; cases aa; cases a) by auto

lemma nat_2: "a - (b + c) = a - c - (b::nat)" 
  apply(cases a;cases b;cases c) by (auto)  
lemma nat_3: "  ⟦a + b ≤ c;   b ≤ (c::nat) ⟧ ⟹  a ≤ c - b"
  apply(rule linordered_semidom_class.add_le_imp_le_diff) .
lemma nat_4: "a + b ≤ c⟹  b ≤ (c::nat)"
  by(rule Nat.add_leD2)

(* TODO: good name *)
class needname = complete_lattice + minus + plus +
  assumes top_absorb: "⋀a. top - a = top" 
      and minus_plus_assoc2: "⋀a b c. a - (b + c) = a - c - b"
      and le_diff_if_add_le: "⋀a b c. ⟦a + b ≤ c;   b ≤ c ⟧ ⟹  a ≤ c - b"
      and add_leD2: "⋀a b c. a + b ≤ c⟹  b ≤ c"
      and add_le_if_le_diff: "⋀t1 a aa b. ⟦t1 ≤ b - a; aa ≤ b - a - t1; a ≤ b⟧ ⟹ t1 + a ≤ b"
begin 
lemma needname_cancle: "t1 + t2 ≤ t ⟹ t2 ≤ t" 
  apply(rule add_leD2) .

lemma needname_adjoint: "a + b ≤ c ⟹ a ≤ c - b"
  using add_leD2 le_diff_if_add_le by blast

end

(*
class resource = complete_lattice + monoid_add
begin

definition minus :: "'a ⇒ 'a ⇒ 'a" where
  "minus a b = Sup {c. c + b ≤ a  }"

lemma "minus top a = top"
  unfolding minus_def 
  apply(rule antisym)
   apply simp
  apply(rule Sup_upper)
  by simp

lemma "minus a (b + c) = minus (minus a b) c"
  unfolding minus_def
  apply(rule antisym)
  subgoal
   apply (rule Sup_upper)
   apply auto
    apply (rule Sup_upper)
    apply auto
    sorry
  subgoal 
    apply(rule Sup_upper)
    apply auto
    sorry

    oops

lemma "⟦a + b ≤ c;   b ≤ c ⟧ ⟹  a ≤ minus c b"
  unfolding minus_def apply(rule Sup_upper)
  apply simp
  done

lemma " a + b ≤ c⟹  b ≤ c"
  sorry

lemma " ⟦t1 ≤ minus b a; aa ≤ minus (minus b a) t1; a ≤ b⟧ ⟹ t1 + a ≤ b"
  unfolding minus_def
  sorry
    


end
*)


instance enat :: needname
  apply standard
      apply(fact enat_1)
     apply(fact enat_2)
    apply(fact enat_3)
   apply(fact enat_4)
  apply(fact enat_5)
  done

instantiation acost :: (type, needname) needname
begin
instance
  apply standard
  subgoal for a apply(cases a) by (auto simp: top_acost_def top_absorb fun_eq_iff)
  subgoal for a b c apply(cases a;cases b;cases c) by (auto simp:  minus_plus_assoc2 less_eq_acost_def)
  subgoal for a b c apply(cases a;cases b;cases c) by (auto simp:  le_diff_if_add_le less_eq_acost_def)
  subgoal for a b c apply(cases a;cases b;cases c) by (auto intro: add_leD2 simp: less_eq_acost_def)
  subgoal for a b c d apply(cases a;cases b;cases c;cases d) by (auto intro: add_le_if_le_diff simp: less_eq_acost_def)
  done
end


lemma diff_left_mono_enat:
   "b ≤ (c::enat)   ⟹ a - c ≤ a - b"  
  apply(cases a; cases b; cases c) by(auto simp: minus_acost_alt less_eq_acost_def diff_left_mono )


class drm = minus + plus + ord + Inf + Sup +
  assumes diff_right_mono: "a ≤ b ⟹ a - c ≤ b - c"
  and diff_left_mono: "⋀a b c. b ≤ c   ⟹ a - c ≤ a - b"  
    (* TODO: investigate what those mean *)
  and minus_continuousInf: "R≠{} ⟹ (INF r∈R. r - mt) ≤ Inf R - mt"
  and minus_continuousSup: "⋀X t q. X≠{} ⟹ ∀x∈X. t ≤ q - (x::'a) ⟹ t ≤ q - (Sup X)" 
  and plus_left_mono: "a ≤ b ⟹ c + a ≤ c + b"







lemma ASSN_enat:
  shows "X≠{} ⟹ ∀x∈X. t ≤ q - (x::enat) ⟹ t ≤ q - (Sup X)"  
  unfolding Sup_enat_def apply auto
  apply(cases q) apply auto
  by (metis antisym cancel_comm_monoid_add_class.diff_cancel diff_left_mono_enat
          finite_enat_bounded idiff_enat_enat linear zero_enat_def zero_le)

instance enat :: drm
  apply standard
  subgoal for a b c apply(cases a; cases b; cases c) by auto
  subgoal for a b c apply(cases a; cases b; cases c) by auto
  subgoal for R mt
    unfolding Inf_enat_def apply auto  
    by (metis (full_types) INF_lower Inf_enat_def LeastI_ex equals0D imageI) 
  subgoal apply(rule ASSN_enat) by auto
  subgoal for a b c apply(cases a; cases b; cases c) by auto
  done



class needname_zero = needname + nonneg + drm + ordered_comm_monoid_add + mult_zero +
  assumes needname_minus_absorb: "x - 0 = x"                                 
   and needname_plus_absorb: "0 + x = x"

instance enat :: needname_zero 
  apply standard
  by auto
lemma ll: "(case acostC x of acostC b ⇒ f b) = f x" by auto

instantiation acost :: (type, needname_zero) needname_zero
begin
  definition "a*b = acostC (λx. the_acost a x * the_acost b x)"

instance
  apply standard
  subgoal for a b c apply(cases a; cases b; cases c) by(auto simp: minus_acost_alt less_eq_acost_def plus_left_mono )  subgoal for a b c apply(cases a; cases b; cases c) by(auto simp: minus_acost_alt less_eq_acost_def diff_right_mono )
  subgoal for a b c apply(cases a; cases b; cases c) by(auto simp: minus_acost_alt less_eq_acost_def diff_left_mono )
  subgoal premises prems for R mt apply(cases mt) unfolding Inf_acost_def less_eq_acost_def minus_acost_alt  apply simp
    apply (subst image_image) apply (auto ) apply(subst ll) 
    apply(rule order.trans)
     defer apply(rule minus_continuousInf) subgoal using prems by auto 
    apply (rule Inf_mono) apply auto
    by (metis acost.case_eq_if acost.sel order_mono_setup.refl)
  subgoal for X t q
    unfolding less_eq_acost_def minus_acost_alt Sup_acost_def
    apply(cases t) apply(cases q)
    apply simp
    apply clarsimp
    apply(rule minus_continuousSup)
    subgoal by blast
    subgoal by (simp add: acost.case_eq_if)
    done
  subgoal for x apply(cases x) by (auto simp: less_eq_acost_def zero_acost_def needname_nonneg)
  subgoal for x apply(cases x) by (auto simp: less_eq_acost_def times_acost_def zero_acost_def)
  subgoal for x apply(cases x) by (auto simp: less_eq_acost_def times_acost_def zero_acost_def)
  subgoal for x apply(cases x) by (auto simp: zero_acost_def needname_minus_absorb)
  subgoal for x apply(cases x) by (auto simp: zero_acost_def needname_plus_absorb)
  done
end



end