Theory Percentage

theory Percentage
  imports HOL.Real
begin

section‹Implementation Detail: Percentage Type›

(*thx pruvisto!*)
typedef percentage = ‹{0..(1::real)}›
  morphisms real_of_percentage Abs_percentage
  by auto

setup_lifting type_definition_percentage

instantiation percentage :: ‹zero›
begin
  lift_definition zero_percentage :: ‹percentage› is ‹0 :: real›
    by auto
  instance ..
end

instantiation percentage :: ‹monoid_mult›
begin
  lift_definition one_percentage :: ‹percentage› is ‹1 :: real›
    by auto

  lift_definition times_percentage :: ‹percentage ⇒ percentage ⇒ percentage› is ‹(*) :: real ⇒ _›
    by (auto simp: mult_le_one)

  instance
    by standard (transfer; simp; fail)+
end


text‹A \<^term>‹Abs_percentage 0.1› would give a "Abstraction violation" in a value command.
So here is some magic to make code work.›
definition percentage :: ‹real ⇒ percentage› where
  ‹percentage p ≡ if p ≤ 0 then 0 else if p ≥ 1 then 1 else Abs_percentage p›

lemma percentage_code [code abstract]:
  ‹real_of_percentage (percentage p) = (if p ≤ 0 then 0 else if p ≥ 1 then 1 else p)›
  unfolding percentage_def
  by (simp add: Abs_percentage_inverse one_percentage.rep_eq zero_percentage.rep_eq)

value[code] ‹percentage 0.1› (*no longer an error*)
lemma ‹real_of_percentage (percentage 0.1) * (25::real) = 2.5› by eval
lemma ‹(25::real) * real_of_percentage (percentage 0.1) = 2.5› by eval

text‹And now we get rid of explicit calls to \<^const>‹real_of_percentage››
declare [[coercion ‹real_of_percentage :: percentage ⇒ real›]]

lemma ‹(percentage 0.1) * (25::real) = 2.5› by eval
lemma ‹(25::real) * (percentage 0.1) = 2.5› by eval
lemma ‹(percentage 0.1) * (25::nat) = 2.5› by eval
lemma ‹(25::nat) * (percentage 0.1) = 2.5› by eval


lemma percentage_range:
  fixes p :: ‹percentage›
  shows ‹0 ≤ p ∧ p ≤ 1›
  using real_of_percentage by auto

lemma real_of_percentage_range:
  ‹0 ≤ real_of_percentage p›
  ‹real_of_percentage p ≤ 1›
  by(simp add: percentage_range)+

(*will cause simplifier looping*)
lemma percentage_min_max_simps:
    ‹real_of_percentage p = min 1 p›
    ‹real_of_percentage p = max 0 p›
  by (simp add: percentage_range)+

lemma real_of_percentage_mult:
  ‹real a * real_of_percentage p ≤ a›
  ‹real_of_percentage p * real a ≤ a›
  by (simp add: mult.commute mult_left_le percentage_range)+

lemma percentage_percentage_mult_right:
  fixes a p ::‹percentage›
  shows ‹a * p ≤ a›
  by (simp add: mult_right_le_one_le real_of_percentage_range times_percentage.rep_eq)
lemma percentage_percentage_mult_left:
  fixes a p ::‹percentage›
  shows ‹p * a ≤ a›
  by (simp add: mult.commute percentage_percentage_mult_right mult_right_le_one_le percentage_range times_percentage.rep_eq)

lemma percentage_real_pos_mult_right:
  ‹a ≥ 0 ⟹ a * real_of_percentage p ≤ a›
  by (simp add: mult_left_le percentage_range)

lemma percentage_real_pos_mult_left:
  ‹a ≥ 0 ⟹ real_of_percentage p * a ≤ a›
  by (simp add: mult_left_le_one_le percentage_range)

lemma percentage_mult_right_mono:
  fixes a b p :: ‹percentage›
  shows ‹a ≤ b ⟹ a * p ≤ b * p›
  by transfer (simp add: mult_right_mono)

lemma percentage_real_mult_right_mono:
  fixes p :: ‹percentage› and a b :: ‹real›
  shows ‹a ≤ b ⟹ a * p ≤ b * p›
  by transfer (simp add: mult_right_mono)

lemma percentage_real_diff_mult_right_mono:
  ‹a ≤ b ⟹ a - a * (real_of_percentage p) ≤ b - b * (real_of_percentage p)›
proof -
  assume a: ‹a ≤ b›
  have ‹0 ≤ b - a› by (simp add: a)
  hence ‹(b - a) * real_of_percentage p ≤ b - a›
    by (simp add: percentage_real_pos_mult_right)
  with a show ‹?thesis›
    by (simp add: a left_diff_distrib')
qed

lemma percentage_nat_diff_mult_right_mono: (*warning: coertion*)
  fixes p :: ‹percentage› and a b :: ‹nat›
  shows ‹(a :: nat) ≤ b ⟹ a - a * p ≤ b - b * p›
  by (simp add: percentage_real_diff_mult_right_mono)

  
lemma percentage_add_limit_helper:
  ‹a ≥ 0 ⟹ b ≤ c - a ⟹ a * real_of_percentage prozent + b ≤ c›
by (metis add.commute le_diff_eq order_trans percentage_real_pos_mult_right) 
end