imports SN_Order_Carrier Ring_Hom_Matrix Derivation_Bound

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