Theory Cost

(*
    Authors:    Maximilian Haslbeck
                René Thiemann
    License:    BSD
*)
section ‹Representing Computation Costs as Pairs of Results and Costs›
theory Cost
  imports Main
begin

type_synonym 'a cost = "'a × nat" 

definition cost :: "'a cost ⇒ nat" where "cost = snd" 
definition result :: "'a cost ⇒ 'a" where "result = fst" 

lemma cost_simps: "cost (a,c) = c" "result (a,c) = a" 
  unfolding cost_def result_def by auto

lemma result_costD: assumes "result f_c = f" 
  "cost f_c ≤ b"
  "f_c = (a,c)"
shows "a = f" "c ≤ b" using assms by (auto simp: cost_simps)

lemma result_costD': assumes "result f_c = f ∧ cost f_c ≤ b"
  "f_c = (a,c)"
  shows "a = f" "c ≤ b" using assms by (auto simp: cost_simps)

end