Theory Simplex.QDelta

(* Authors: F. Maric, M. Spasic, R. Thiemann *)
section ‹Rational Numbers Extended with Infinitesimal Element›
theory QDelta
  imports  
    Abstract_Linear_Poly
    Simplex_Algebra 
begin

datatype QDelta = QDelta rat rat

primrec qdfst :: "QDelta ⇒ rat" where
  "qdfst (QDelta a b) = a"

primrec qdsnd :: "QDelta ⇒ rat" where
  "qdsnd (QDelta a b) = b"

lemma [simp]: "QDelta (qdfst qd) (qdsnd qd) = qd"
  by (cases qd) auto

lemma [simp]: "⟦QDelta.qdsnd x = QDelta.qdsnd y; QDelta.qdfst y = QDelta.qdfst x⟧ ⟹ x = y"
  by (cases x) auto

instantiation QDelta :: rational_vector
begin

definition zero_QDelta :: "QDelta"
  where
    "0 = QDelta 0 0"

definition plus_QDelta :: "QDelta ⇒ QDelta ⇒ QDelta"
  where
    "qd1 + qd2 = QDelta (qdfst qd1 + qdfst qd2) (qdsnd qd1 + qdsnd qd2)"

definition minus_QDelta :: "QDelta ⇒ QDelta ⇒ QDelta"
  where
    "qd1 - qd2 = QDelta (qdfst qd1 - qdfst qd2) (qdsnd qd1 - qdsnd qd2)"

definition uminus_QDelta :: "QDelta ⇒ QDelta"
  where
    "- qd = QDelta (- (qdfst qd)) (- (qdsnd qd))"

definition scaleRat_QDelta :: "rat ⇒ QDelta ⇒ QDelta"
  where
    "r *R qd = QDelta (r*(qdfst qd)) (r*(qdsnd qd))"

instance 
proof 
qed (auto simp add: plus_QDelta_def zero_QDelta_def uminus_QDelta_def minus_QDelta_def scaleRat_QDelta_def field_simps)
end

instantiation QDelta :: linorder
begin
definition less_eq_QDelta :: "QDelta ⇒ QDelta ⇒ bool"
  where
    "qd1 ≤ qd2 ⟷ (qdfst qd1 < qdfst qd2) ∨ (qdfst qd1 = qdfst qd2 ∧ qdsnd qd1 ≤ qdsnd qd2)"

definition less_QDelta :: "QDelta ⇒ QDelta ⇒ bool"
  where
    "qd1 < qd2 ⟷ (qdfst qd1 < qdfst qd2) ∨ (qdfst qd1 = qdfst qd2 ∧ qdsnd qd1 < qdsnd qd2)"

instance proof qed (auto simp add: less_QDelta_def less_eq_QDelta_def)
end

instantiation QDelta:: linordered_rational_vector
begin
instance proof qed (auto simp add: plus_QDelta_def less_QDelta_def scaleRat_QDelta_def mult_strict_left_mono mult_strict_left_mono_neg)
end

instantiation QDelta :: lrv
begin
definition one_QDelta where
  "one_QDelta = QDelta 1 0"
instance proof qed (auto simp add: one_QDelta_def zero_QDelta_def)
end

definition δ0 :: "QDelta ⇒ QDelta ⇒ rat"
  where
    "δ0 qd1 qd2 ==
    let c1 = qdfst qd1; c2 = qdfst qd2; k1 = qdsnd qd1; k2 = qdsnd qd2 in
      (if (c1 < c2 ∧ k1 > k2) then 
              (c2 - c1) / (k1 - k2) 
       else
               1
       )
    "

definition val :: "QDelta ⇒ rat ⇒ rat"
  where "val qd δ = (qdfst qd) + δ * (qdsnd qd)"

lemma val_plus: 
  "val (qd1 + qd2) δ = val qd1 δ + val qd2 δ"
  by (simp add: field_simps val_def plus_QDelta_def)

lemma val_scaleRat:
  "val (c *R qd) δ = c * val qd δ"
  by (simp add: field_simps val_def scaleRat_QDelta_def)

lemma qdfst_setsum:
  "finite A ⟹ qdfst (∑x∈A. f x) = (∑x∈A. qdfst (f x))"
  by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)

lemma qdsnd_setsum:
  "finite A ⟹ qdsnd (∑x∈A. f x) = (∑x∈A. qdsnd (f x))"
  by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)

lemma valuate_valuate_rat:
  "lp ⦃(λv. (QDelta (vl v) 0))⦄ = QDelta (lp⦃vl⦄) 0"
  using Rep_linear_poly
  by (simp add: valuate_def scaleRat_QDelta_def qdsnd_setsum qdfst_setsum)

lemma valuate_rat_valuate:
  "lp⦃(λv. val (vl v) δ)⦄ = val (lp⦃vl⦄) δ"
  unfolding valuate_def val_def
  using rational_vector.scale_sum_right[of δ "λx. Rep_linear_poly lp x * qdsnd (vl x)" "{v :: nat. Rep_linear_poly lp v ≠ (0 :: rat)}"]
  using Rep_linear_poly
  by (auto simp add: field_simps sum.distrib qdfst_setsum qdsnd_setsum) (auto simp add: scaleRat_QDelta_def)

lemma delta0:
  assumes "qd1 ≤ qd2"
  shows "∀ ε. ε > 0 ∧ ε ≤ (δ0 qd1 qd2) ⟶ val qd1 ε ≤ val qd2 ε"
proof-
  have "⋀ e c1 c2 k1 k2 :: rat. ⟦e ≥ 0; c1 < c2; k1 ≤ k2⟧ ⟹ c1 + e*k1 ≤ c2 + e*k2"
  proof-
    fix e c1 c2 k1 k2 :: rat
    show "⟦e ≥ 0; c1 < c2; k1 ≤ k2⟧ ⟹ c1 + e*k1 ≤ c2 + e*k2"
      using mult_left_mono[of "k1" "k2" "e"]
      using add_less_le_mono[of "c1" "c2" "e*k1" "e*k2"]
      by simp
  qed
  then show ?thesis
    using assms
    by (auto simp add: δ0_def val_def less_eq_QDelta_def Let_def field_simps mult_left_mono)
qed

primrec
  δ_min ::"(QDelta × QDelta) list ⇒ rat" where
  "δ_min [] = 1" |
  "δ_min (h # t) = min (δ_min t) (δ0 (fst h) (snd h))"

lemma delta_gt_zero:
  "δ_min l > 0"
  by (induct l) (auto simp add: Let_def field_simps δ0_def)

lemma delta_le_one: 
  "δ_min l ≤ 1" 
  by (induct l, auto)

lemma delta_min_append:
  "δ_min (as @ bs) = min (δ_min as) (δ_min bs)"
  by (induct as, insert delta_le_one[of bs], auto)

lemma delta_min_mono: "set as ⊆ set bs ⟹ δ_min bs ≤ δ_min as" 
proof (induct as)
  case Nil
  then show ?case using delta_le_one by simp
next
  case (Cons a as)
  from Cons(2) have "a ∈ set bs" by auto
  from split_list[OF this]
  obtain bs1 bs2 where bs: "bs = bs1 @ [a] @ bs2" by auto
  have bs: "δ_min bs = δ_min ([a] @ bs)" unfolding bs delta_min_append by auto
  show ?case unfolding bs using Cons(1-2) by auto
qed


lemma delta_min:
  assumes "∀ qd1 qd2. (qd1, qd2) ∈ set qd ⟶ qd1 ≤ qd2"
  shows "∀ ε. ε > 0 ∧ ε ≤ δ_min qd ⟶ (∀ qd1 qd2. (qd1, qd2) ∈ set qd ⟶ val qd1 ε ≤ val qd2 ε)"
  using assms
  using delta0
  by (induct qd, auto)

lemma QDelta_0_0: "QDelta 0 0 = 0" by code_simp
lemma qdsnd_0: "qdsnd 0 = 0" by code_simp
lemma qdfst_0: "qdfst 0 = 0" by code_simp


end