Theory Complexity_Carrier

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Complexity Carrier›

text ‹We define which properties a carrier of matrices must exhibit, so that it
  can be used for checking complexity proofs.›

theory Complexity_Carrier
imports
  "Abstract-Rewriting.SN_Order_Carrier"
  Ring_Hom_Matrix
  Derivation_Bound
  HOL.Real
begin

class large_real_ordered_semiring_1 = large_ordered_semiring_1 + real_embedding

instance real :: large_real_ordered_semiring_1 ..
instance int :: large_real_ordered_semiring_1 ..
instance rat :: large_real_ordered_semiring_1 ..

text ‹For complexity analysis, we need a bounding function which tells us how often
  one can strictly decrease a value. To this end, $\delta$-orderings are usually applied
  when working with the reals or rational numbers.›

locale complexity_one_mono_ordered_semiring_1 = one_mono_ordered_semiring_1 default gt 
  for gt :: "'a :: large_ordered_semiring_1 ⇒ 'a ⇒ bool" (infix "≻" 50) and default :: 'a + 
  fixes bound :: "'a ⇒ nat"
  assumes bound_mono: "⋀ a b. a ≥ b ⟹ bound a ≥ bound b"
   and bound_plus: "⋀ a b. bound (a + b) ≤ bound a + bound b" 
   and bound_plus_of_nat: "⋀ a n. a ≥ 0 ⟹ bound (a + of_nat n) = bound a + bound (of_nat n)" 
   and bound_zero[simp]: "bound 0 = 0"
   and bound_one: "bound 1 ≥ 1"
   and bound: "⋀ a. deriv_bound {(a,b). b ≥ 0 ∧ a ≻ b} a (bound a)"
begin


lemma bound_linear: "∃ c. ∀ n. bound (of_nat n) ≤ c * n"
proof (rule exI[of _ "bound 1"], intro allI)
  fix n
  show "bound (of_nat n) ≤ bound 1 * n"
  proof (induct n)
    case (Suc n)
    have "bound (of_nat (Suc n)) = bound (1 + of_nat n)" by simp
    also have "... ≤ bound 1 + bound (of_nat n)"
      by (rule bound_plus)
    also have "... ≤ bound 1 + bound 1 * n"
      using Suc by auto
    finally show ?case by auto
  qed simp
qed

lemma bound_of_nat_times: "bound (of_nat n * v) ≤ n * bound v"
proof (induct n)
  case (Suc n)
  have "bound (of_nat (Suc n) * v) = bound (v + of_nat n * v)" by (simp add: field_simps)
  also have "… ≤ bound v + bound (of_nat n * v)" by (rule bound_plus)
  also have "… ≤ bound v + n * bound v" using Suc by auto
  finally show ?case by simp 
qed simp

lemma bound_mult_of_nat: "bound (a * of_nat n) ≤ bound a * bound (of_nat n)"
proof (induct n)
  case (Suc n)
  have "bound (a * of_nat (Suc n)) = bound (a + a * of_nat n)" by (simp add: field_simps)
  also have "... ≤ bound a + bound (a * of_nat n)"
    by (rule bound_plus)
  also have "... ≤ bound a + bound a * bound (of_nat n)" using Suc by auto
  also have "... = bound a * (1 + bound (of_nat n))" by (simp add: field_simps)
  also have "... ≤ bound a * (bound (1 + of_nat n))"
  proof (rule mult_le_mono2)
    show "1 + bound(of_nat n) ≤ bound (1 + of_nat n)" using bound_one
    using bound_plus
      unfolding bound_plus_of_nat[OF one_ge_zero] by simp
  qed
  finally show ?case by simp
qed simp

lemma bound_pow_of_nat: "bound (a * of_nat n ^ deg) ≤ bound a * of_nat n ^ deg" 
proof (induct deg)
  case (Suc deg)
  have "bound (a * of_nat n ^ Suc deg) =  bound (of_nat n * (a * of_nat n ^ deg))"
    by (simp add: field_simps)
  also have "… ≤ n * bound (a * of_nat n ^ deg)"
    by (rule bound_of_nat_times)
  also have "… ≤ n * (bound a * of_nat n ^ deg)"
    using Suc by auto
  finally show ?case by (simp add: field_simps)
qed simp
end

end