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 
      (iA. X i)  (iA.  i) + (jF. Y j) 
      (iA. X i  Cs)  (jF. Y j  Ps j)"

lemma feasible_private_ownershipD:
  assumes "feasible_private_ownership A F  Cs Ps X Y"
  shows "(iA. X i)  (iA.  i) + (jF. Y j)"
    and "(iA. X i  Cs)" and "(jF. 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