Theory Common

(* License: LGPL *)
(*
Author: Julian Parsert <julian.parsert@gmail.com>
Author: Cezary Kaliszyk
*)


theory Common
  imports
    "../Preferences"
    "../Utility_Functions"
    "../Argmax"
begin


section ‹ Pareto Ordering ›

text ‹ Allows us to define a Pareto Ordering. ›

locale pareto_ordering =
  fixes agents :: "'i set"
  fixes U :: "'i ⇒ 'a ⇒ real"
begin
notation U (‹U[_]›)

definition pareto_dominating (infix ‹≻Pareto›  60)
  where
    "X ≻Pareto Y ⟷
      (∀i ∈ agents. U[i] (X i) ≥ U[i] (Y i)) ∧
      (∃i ∈ agents. U[i] (X i) > U[i] (Y i))"

lemma trans_strict_pareto: "X ≻Pareto Y ⟹ Y ≻Pareto Z ⟹ X ≻Pareto Z"
proof -
  assume a1: "X ≻Pareto Y"
  assume "Y ≻Pareto Z"
  then have f3: "∀i ∈ agents. U[i] (Z i) ≤ U[i] (X i)"
    by (meson a1 order_trans pareto_dominating_def)
  moreover have "∃i ∈ agents. ¬ U[i] (X i) ≤ U[i] (Y i)"
    using a1 pareto_dominating_def by fastforce
  ultimately show ?thesis
    by (metis ‹Y ≻Pareto Z› less_eq_real_def pareto_dominating_def)
qed

lemma anti_sym_strict_pareto: "X ≻Pareto Y ⟹ ¬Y ≻Pareto X"
  using pareto_dominating_def by auto

end

subsection ‹ Budget constraint›

text ‹ Definition returns all afforedable bundles given wealth W ›
text ‹ f is a function that computes the value given a bundle›
definition budget_constraint
  where
    "budget_constraint f S W = {x ∈ S. f x ≤ W}"


subsection ‹ Feasiblity ›

definition feasible_private_ownership
  where
    "feasible_private_ownership A F ℰ Cs Ps X Y ⟷
      (∑i∈A. X i) ≤ (∑i∈A. ℰ i) + (∑j∈F. Y j) ∧
      (∀i∈A. X i ∈ Cs) ∧ (∀j∈F. Y j ∈ Ps j)"

lemma feasible_private_ownershipD:
  assumes "feasible_private_ownership A F ℰ Cs Ps X Y"
  shows "(∑i∈A. X i) ≤ (∑i∈A. ℰ i) + (∑j∈F. Y j)"
    and "(∀i∈A. X i ∈ Cs)" and "(∀j∈F. Y j ∈ Ps j)"
  using assms feasible_private_ownership_def apply blast
  by (meson assms feasible_private_ownership_def)
    (meson assms feasible_private_ownership_def)

end