Theory Preferences

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

section ‹Preference Relations›

text ‹ Preferences modeled as a set of pairs ›

theory Preferences
  imports
    "HOL-Analysis.Multivariate_Analysis"
    Syntax
begin


subsection ‹Basic Preference Relation›

text ‹ Basic preference relation locale with carrier and relation modeled as a set of pairs. ›

locale preference =
  fixes carrier :: "'a set"
  fixes relation :: "'a relation"
  assumes not_outside: "(x,y) ∈ relation ⟹ x ∈ carrier"
    and "(x,y) ∈ relation ⟹ y ∈ carrier"
  assumes trans_refl: "preorder_on  carrier relation"

context preference
begin

no_notation eqpoll (infixl ‹≈› 50)

abbreviation geq (‹_ ≽ _› [51,51] 60)
  where
    "x ≽ y ≡ x ≽[relation] y"

abbreviation str_gr (‹_ ≻ _› [51,51] 60)
  where
    "x ≻ y ≡ x ≽ y ∧ ¬y ≽ x"

abbreviation indiff (‹_ ≈ _› [51,51] 60)
  where
    "x ≈ y ≡ x ≽ y ∧ y ≽ x"

lemma reflexivity: "refl_on carrier relation"
  using preorder_on_def trans_refl by blast

lemma transitivity: "trans relation"
  using preorder_on_def trans_refl by auto

lemma indiff_trans [simp]: "x ≈ y ⟹ y ≈ z ⟹ x ≈ z"
  by (meson transE transitivity)

end


subsubsection ‹ Contour sets ›

definition at_least_as_good :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
  where
    "at_least_as_good x B P = {y ∈ B. y ≽[P] x }"

definition no_better_than :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
  where
    "no_better_than x B P = {y ∈ B. x ≽[P] y}"

definition as_good_as :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
  where
    "as_good_as x B P = {y ∈ B. x ≈[P] y}"

lemma at_lst_asgd_ge:
  assumes "x ∈ at_least_as_good y B Pr"
  shows "x ≽[Pr] y"
  using assms at_least_as_good_def by fastforce

lemma strict_contour_is_diff:
  "{a ∈ B. a ≻[Pr] y} = at_least_as_good y B Pr - as_good_as y B Pr"
  by(auto simp add: at_least_as_good_def as_good_as_def)

lemma strict_countour_def [simp]:
  "(at_least_as_good y B Pr) - as_good_as y B Pr = {x ∈ B. x ≻[Pr] y}"
  by (simp add: as_good_as_def at_least_as_good_def strict_contour_is_diff)

lemma at_least_as_goodD [dest]:
  assumes "z ∈ at_least_as_good y B Pr"
  shows "z ≽[Pr] y"
  using assms at_least_as_good_def by fastforce


subsection ‹Rational Preference Relation›

text ‹ Rational preferences add totality to the basic preferences. ›

locale rational_preference = preference +
  assumes total: "total_on carrier relation"
begin

lemma compl: "∀x ∈ carrier . ∀y∈ carrier . x ≽ y ∨ y ≽ x"
  by (metis refl_onD reflexivity total total_on_def)

lemma strict_not_refl_weak [iff]: "x ∈ carrier ∧ y ∈ carrier ⟹ ¬ (y ≽ x) ⟷ x ≻ y"
  by (metis refl_onD reflexivity total total_on_def)

lemma strict_trans [simp]: "x ≻ y ⟹ y ≻ z ⟹ x ≻ z"
  by (meson transE transitivity)

lemma completeD [dest]: "x ∈ carrier ⟹ y ∈ carrier ⟹ x ≠ y ⟹ x ≽ y ∨ y ≽ x"
  by blast

lemma pref_in_at_least_as:
  assumes "x ≽ y"
  shows "x ∈ at_least_as_good y carrier relation"
  by (metis (no_types, lifting) CollectI assms
      at_least_as_good_def preference.not_outside preference_axioms)

lemma worse_in_no_better:
  assumes "x ≽ y"
  shows "y ∈ no_better_than y carrier relation"
  by (metis (no_types, lifting) CollectI assms no_better_than_def
      preference_axioms preference_def strict_not_refl_weak)

lemma strict_is_neg_transitive :
  assumes "x ∈ carrier ∧ y ∈ carrier ∧ z ∈ carrier"
  shows "x ≻ y ⟹ x ≻ z ∨ z ≻ y"
  by (meson assms compl transE transitivity)

lemma weak_is_transitive:
 assumes "x ∈ carrier ∧ y ∈ carrier ∧ z ∈ carrier"
 shows "x ≽ y ⟹ y ≽ z ⟹ x ≽ z"
  by (meson transD transitivity)

lemma no_better_than_nonepty:
  assumes "carrier ≠ {}"
  shows "⋀x. x ∈ carrier ⟹ (no_better_than x carrier relation) ≠ {}"
  by (metis (no_types, lifting) empty_iff mem_Collect_eq
      no_better_than_def refl_onD reflexivity)

lemma no_better_subset_pref :
  assumes "x ≽ y"
  shows "no_better_than y carrier relation ⊆ no_better_than x carrier relation"
proof
  fix a
  assume "a ∈ no_better_than y carrier relation"
  then show "a ∈ no_better_than x carrier relation"
    by (metis (no_types, lifting) assms mem_Collect_eq no_better_than_def transE transitivity)
qed

lemma no_better_thansubset_rel :
  assumes "x ∈ carrier" and "y ∈ carrier"
  assumes "no_better_than y carrier relation ⊆ no_better_than x carrier relation"
  shows "x ≽ y"
proof -
  have  "{a ∈ carrier. y ≽ a} ⊆ {a ∈ carrier. x ≽ a}"
    by (metis (no_types) assms(3) no_better_than_def)
  then show ?thesis
    by (metis (mono_tags, lifting) Collect_mono_iff assms(2) compl)
qed

lemma nbt_nest :
  shows "(no_better_than y carrier relation ⊆ no_better_than x carrier relation) ∨
        (no_better_than x carrier relation ⊆ no_better_than y carrier relation)"
  by (metis (no_types, lifting) CollectD compl no_better_subset_pref no_better_than_def not_outside subsetI)

lemma at_lst_asgd_not_ge:
  assumes "carrier ≠ {}"
  assumes "x ∈ carrier" and "y ∈ carrier"
  assumes "x ∉ at_least_as_good y carrier relation"
  shows "¬ x ≽ y"
  by (metis (no_types, lifting) CollectI assms(2) assms(4) at_least_as_good_def)

lemma as_good_as_sameIff[iff]:
  "z ∈ as_good_as y carrier relation ⟷ z ≽ y ∧ y ≽ z"
  by (metis (no_types, lifting) as_good_as_def mem_Collect_eq not_outside)

lemma same_at_least_as_equal:
  assumes "z ≈ y"
  shows "at_least_as_good z carrier relation =
         at_least_as_good y carrier relation" (is "?az = ?ay")
proof
  have "z ∈ carrier ∧ y ∈ carrier"
    by (meson assms refl_onD2 reflexivity)
  moreover have "∀x ∈ carrier. x ≽ z ⟶ x ≽ y"
    by (meson assms transD transitivity)
  ultimately show "?az ⊆ ?ay"
    by (metis at_lst_asgd_ge at_lst_asgd_not_ge
        equals0D not_outside subsetI)
next
   have "z ∈ carrier ∧ y ∈ carrier"
    by (meson assms refl_onD2 reflexivity)
  moreover have "∀x ∈ carrier. x ≽ y ⟶ x ≽ z"
    by (meson assms transD transitivity)
  ultimately show "?ay ⊆ ?az"
    by (metis at_lst_asgd_ge at_lst_asgd_not_ge
        equals0D not_outside subsetI)
qed

lemma as_good_asIff [iff]:
  "x ∈ as_good_as y carrier relation ⟷ x ≈[relation] y"
  by blast

lemma nbt_subset:
  assumes "finite carrier"
  assumes "x ∈ carrier" and "y ∈ carrier"
  shows "no_better_than x carrier relation ⊆ no_better_than x carrier relation ∨
         no_better_than x carrier relation ⊆ no_better_than x carrier relation"
  by auto

lemma fnt_carrier_fnt_rel: "finite carrier ⟹ finite relation"
  by (metis finite_SigmaI refl_on_def reflexivity rev_finite_subset)

lemma nbt_subset_carrier:
  assumes "x ∈ carrier"
  shows "no_better_than x carrier relation ⊆ carrier"
  using no_better_than_def by fastforce

lemma xy_in_eachothers_nbt:
  assumes "x ∈ carrier" "y ∈ carrier"
  shows "x ∈ no_better_than y carrier relation ∨
         y ∈ no_better_than x carrier relation"
  by (meson assms(1) assms(2) contra_subsetD nbt_nest refl_onD reflexivity worse_in_no_better)

lemma same_nbt_same_pref:
  assumes "x ∈ carrier" "y ∈ carrier"
  shows "x ∈ no_better_than y carrier relation ∧
         y ∈ no_better_than x carrier relation ⟷ x ≈ y"
    by (metis (mono_tags, lifting) CollectD contra_subsetD no_better_subset_pref
        no_better_than_def worse_in_no_better)

lemma indifferent_imp_weak_pref: 
  assumes "x ≈ y"
  shows" x ≽ y" "y ≽ x"
  by (simp add: assms)+

subsection ‹ Finite carrier›

context
  assumes "finite carrier"
begin

lemma fnt_carrier_fnt_nbt:
  shows "∀x∈carrier. finite (no_better_than x carrier relation)"
proof
  fix x
  assume "x ∈ carrier"
  then show "finite (no_better_than x carrier relation)"
  using  finite_subset nbt_subset_carrier ‹finite carrier› by blast
qed

lemma nbt_subset_imp_card_leq:
  assumes "x ∈ carrier" and "y ∈ carrier"
  shows "no_better_than x carrier relation ⊆ no_better_than y carrier relation ⟷
  card (no_better_than x carrier relation) ≤ card  (no_better_than y carrier relation)"
  (is "?nbt ⟷ ?card")
proof
  assume "?nbt"
  then show "?card"
    by (simp add: assms(2) card_mono fnt_carrier_fnt_nbt)
next
  assume "?card"
  then show "?nbt"
    by (metis  assms(1) card_seteq fnt_carrier_fnt_nbt nbt_nest)
qed

lemma card_leq_pref:
  assumes "x ∈ carrier" and "y ∈ carrier"
  shows "card (no_better_than x carrier relation) ≤ card (no_better_than y carrier relation)
   ⟷ y ≽ x"
proof (rule iffI, goal_cases)
  case 1
  then show ?case
    using assms(1) assms(2) nbt_subset_imp_card_leq no_better_thansubset_rel by presburger
next
  case 2
  then show ?case
    using assms(1) assms(2) nbt_subset_imp_card_leq no_better_subset_pref by blast
qed

lemma finite_ne_remove_induct:
  assumes "finite B" "B ≠ {}"
    "⋀A. finite A  ⟹ A ⊆ B ⟹ A ≠ {} ⟹
         (⋀x. x ∈ A ⟹ A - {x} ≠ {} ⟹ P (A - {x})) ⟹ P A"
  shows "P B"
  by (metis assms finite_remove_induct[where P = "λF. F = {} ∨ P F" for P])


lemma finite_nempty_preorder_has_max:
  assumes "finite B" "B ≠ {}" "refl_on B R" "trans R" "total_on B R"
  shows "∃x ∈ B. ∀y ∈ B. (x, y) ∈ R"
  using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
  case (insert x F)
  then show ?case using assms(3-)
    by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto

lemma finite_nempty_preorder_has_min:
  assumes "finite B" "B ≠ {}" "refl_on B R" "trans R" "total_on B R"
  shows "∃x ∈ B. ∀y ∈ B. (y, x) ∈ R"
  using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
  case (insert x F)
  then show ?case using assms(3-)
    by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto

lemma finite_nonempty_carrier_has_maximum:
  assumes "carrier ≠ {}"
  shows "∃e ∈ carrier. ∀m ∈ carrier. e ≽[relation] m"
  using finite_nempty_preorder_has_max[of carrier relation] assms
     ‹finite carrier› reflexivity total transitivity by blast

lemma finite_nonempty_carrier_has_minimum:
  assumes "carrier ≠ {}"
  shows "∃e ∈ carrier. ∀m ∈ carrier. m ≽[relation] e"
  using finite_nempty_preorder_has_min[of carrier relation] assms
     ‹finite carrier› reflexivity total transitivity by blast

end (*finite carrier*)


lemma all_carrier_ex_sub_rel: 
  "∀c ⊆ carrier. ∃r ⊆ relation. rational_preference c r"
proof (standard,standard)
  fix c
  assume c_in: "c ⊆ carrier"
  define r' where
    "r' = {(x,y) ∈ relation. x ∈ c ∧ y ∈ c}"
  have r'_sub: "r' ⊆ c × c"
    using r'_def by blast
  have "∀x ∈ c. x ≽[r'] x"
    by (metis (no_types, lifting) CollectI c_in case_prodI compl r'_def subsetCE)
  then have refl: "refl_on c r'"
    by (meson r'_sub refl_onI)
  have trans: "trans r'"
  proof
    fix x y z
    assume a1: "x ≽[r'] y"
    assume a2: "y ≽[r'] z"
    show " x ≽[r'] z"
      by (metis (mono_tags, lifting) CollectD CollectI a1 a2 case_prodD case_prodI r'_def transE transitivity)
  qed
  have total: "total_on c r'"
  proof (standard)
    fix x y
    assume a1:"x ∈ c"
    assume a2: "y ∈ c"
    assume a3: "x ≠ y"
    show "x ≽[r'] y ∨ y ≽[r'] x "
      by (metis (no_types, lifting) CollectI a1 a2 c_in case_prodI compl r'_def subset_iff)
  qed
  have "rational_preference c r'"
    by (meson local.refl local.trans preference.intro preorder_on_def rational_preference.intro 
        rational_preference_axioms.intro refl_on_domain total)
  thus "∃r⊆relation. rational_preference c r"
    by (metis (no_types, lifting) CollectD case_prodD r'_def subrelI)
qed

end (*rational preference*)


subsection ‹ Local Non-Satiation ›

text ‹ Defining local non-satiation. ›

definition local_nonsatiation
  where
  "local_nonsatiation B P ⟷
   (∀x∈B. ∀e>0. ∃y∈B. norm (y - x) ≤ e ∧ y ≻[P] x)"

text ‹ Alternate definitions and intro/dest rules with them ›

lemma lns_alt_def1 [iff] :
  shows "local_nonsatiation B P ⟷ (∀x ∈ B. ∀e>0. (∃y ∈ B. dist y x ≤ e ∧ y ≻[P] x))"
  by(simp add : dist_norm local_nonsatiation_def)

lemma lns_normI [intro]:
  assumes "⋀x e. x ∈ B ⟹ e > 0 ⟹ (∃y∈B. norm (y - x) ≤ e ∧ y ≻[P] x)"
  shows "local_nonsatiation B P"
  by (simp add: assms dist_norm)

lemma lns_distI [intro]:
  assumes "⋀x e. x ∈ B ⟹ e > 0 ⟹ (∃y∈B. (dist y x) ≤ e ∧ y ≻[P] x)"
  shows "local_nonsatiation B P"
  by (meson lns_alt_def1 assms)

lemma lns_alt_def2 [iff]:
  "local_nonsatiation B P ⟷ (∀x∈B. ∀e>0. (∃y.  y ∈ (ball x e) ∧ y ∈ B ∧ y ≻[P] x))"
proof
  assume "local_nonsatiation B P"
  then show "∀x∈B. ∀e>0. ∃x'. x' ∈ ball x e ∧ x' ∈ B ∧ x' ≻[P] x"
    by (auto simp add : ball_def) (metis dense le_less_trans dist_commute)
next
  assume "∀x∈B. ∀e>0. ∃y. y ∈ ball x e ∧ y ∈ B ∧ y ≻[P] x"
  then show "local_nonsatiation B P"
    by (metis (no_types, lifting) ball_def dist_commute
        less_le_not_le lns_alt_def1 mem_Collect_eq)
qed

lemma lns_normD [dest]:
  assumes "local_nonsatiation B P"
  shows "∀x ∈ B. ∀e>0. ∃y ∈ B. (norm (y - x) ≤ e ∧ y ≻[P] x)"
  by (meson assms local_nonsatiation_def)


subsection ‹ Convex preferences ›

definition weak_convex_pref :: "('a::real_vector) relation ⇒ bool"
  where
    "weak_convex_pref Pr ⟷ (∀x y. x ≽[Pr] y ⟶
      (∀α β. α + β = 1 ∧ α > 0 ∧ β > 0 ⟶ α *⇩R x + β *⇩R y ≽[Pr] y))"

definition convex_pref :: "('a::real_vector) relation ⇒ bool"
  where
    "convex_pref Pr ⟷ (∀x y. x ≻[Pr] y ⟶
      (∀α. 1 > α ∧ α > 0 ⟶ α *⇩R x + (1-α) *⇩R y ≻[Pr] y))"

definition strict_convex_pref :: "('a::real_vector) relation ⇒ bool"
  where
    "strict_convex_pref Pr ⟷ (∀x y. x ≽[Pr] y ∧ x ≠ y ⟶
      (∀α. 1 > α ∧ α > 0 ⟶ α *⇩R x + (1-α) *⇩R y ≻[Pr] y))"

lemma convex_ge_imp_conved:
  assumes "∀x y. x ≽[Pr] y ⟶ (∀α β. α + β = 1 ∧ α ≥ 0 ∧ β ≥ 0 ⟶ α *⇩R x + β *⇩R y ≽[Pr] y)"
  shows "weak_convex_pref Pr"
  by (simp add: assms weak_convex_pref_def)

lemma weak_convexI [intro]:
  assumes "⋀x y α β. x ≽[Pr] y ⟹ α + β = 1 ⟹ 0 < α ⟹ 0 < β ⟹ α *⇩R x + β *⇩R y ≽[Pr] y"
  shows "weak_convex_pref Pr"
  by (simp add: assms weak_convex_pref_def)

lemma weak_convexD [dest]:
  assumes "weak_convex_pref Pr" and "x ≽[Pr] y" and "0 < u" and "0 < v" and "u + v = 1"
  shows "u *⇩R x + v *⇩R y ≽[Pr] y"
    using assms weak_convex_pref_def by blast


subsection ‹ Real Vector Preferences ›

text ‹ Preference relations on real vector type class. ›

locale real_vector_rpr = rational_preference carrier relation
for carrier :: "'a::real_vector set"
and relation :: "'a relation"

sublocale  real_vector_rpr ⊆ rational_preference carrier relation
  by (simp add: rational_preference_axioms)

context real_vector_rpr
begin

lemma have_rpr: "rational_preference carrier relation"
  by (simp add: rational_preference_axioms)

text ‹ Multiple convexity alternate definitions intro/dest rules. ›

lemma weak_convex1D [dest]:
  assumes "weak_convex_pref relation" and "x ≽[relation] y" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
  shows "u *⇩R x + v *⇩R y ≽[relation] y"
proof-
  have u_0: "u = 0 ⟶ u *⇩R x + v *⇩R y ≽[relation] y"
  proof
    assume u_0: "u = 0"
    have "v = 1"
      using assms(5) u_0 by auto
    then have "?thesis"
      by (metis add.left_neutral assms(2) preference.reflexivity preference_axioms
          real_vector.scale_zero_left refl_onD2 scaleR_one strict_not_refl_weak)
    thus "u *⇩R x + v *⇩R y ≽[relation] y "
      using u_0 by blast
  qed
  have "u ≠ 0 ∧ u ≠ 1 ⟶ u *⇩R x + v *⇩R y ≽[relation] y"
    by (metis add_cancel_right_right antisym_conv not_le assms weak_convexD )
  then show ?thesis
    by (metis u_0 assms(2,5) add_cancel_right_right real_vector.scale_zero_left scaleR_one)
qed

lemma weak_convex1I [intro] :
  assumes "∀x. convex (at_least_as_good x carrier relation)"
  shows "weak_convex_pref relation"
proof (rule weak_convexI)
  fix x and y and α β :: real
  assume assum : "x ≽[relation] y"
  assume reals: "0 < α" "0 < β" " α + β = 1"
  then have "x ∈ carrier"
    by (meson assum preference.not_outside rational_preference.axioms(1) have_rpr)
  have "y ∈ carrier"
    by (meson assum refl_onD2 reflexivity)
  then have y_in_upper_cont: "y ∈ (at_least_as_good y carrier relation)"
    using assms rational_preference.at_lst_asgd_not_ge
      rational_preference.compl  by (metis empty_iff have_rpr)
  then have "x ∈ (at_least_as_good y carrier relation)"
    using assum pref_in_at_least_as by blast
  moreover have "0 ≤ β" and "0 ≤ α"
    using reals by (auto)
  ultimately show "(α *⇩R x + β *⇩R y) ≽[relation] y"
    by (meson assms(1) at_least_as_goodD convexD reals(3) y_in_upper_cont)
qed

text ‹ Definition of convexity in "Handbook of Social Choice and Welfare"\<^cite>‹"arrow2010handbook"›. ›

lemma convex_def_alt:
  assumes "rational_preference carrier relation"
  assumes "weak_convex_pref relation"
  shows "(∀x ∈ carrier. convex (at_least_as_good x carrier relation))"
proof
  fix x
  assume x_in: "x ∈ carrier"
  show "convex (at_least_as_good x carrier relation)" (is "convex ?x")
  proof (rule convexI)
    fix a b :: "'a" and  α :: "real" and β :: "real"
    assume a_in: "a ∈ ?x"
    assume b_in: "b ∈ ?x"
    assume reals: " 0 ≤ α" "0 ≤ β" "α + β = 1"
    have a_g_x: "a ≽[relation] x"
      using a_in by blast
    have b_g_x: "b ≽[relation] x"
      using b_in by blast
    have "a ≽[relation] b ∨ b ≽[relation] a"
      by (meson a_in at_least_as_goodD b_in preference.not_outside
          rational_preference.compl rational_preference_def assms(1))
    then show "α *⇩R a + β *⇩R b ∈ ?x"
    proof(rule disjE)
      assume "a ≽[relation] b"
      then have "α *⇩R a + β *⇩R b  ≽[relation] b"
        using assms reals by blast
      then have "α *⇩R a + β *⇩R b ≽[relation] x"
        by (meson b_g_x  assms(1) preference.not_outside x_in
            rational_preference.strict_is_neg_transitive
            rational_preference.strict_not_refl_weak rational_preference_def)
      then show ?thesis
        by (metis (no_types, lifting) CollectI  assms(1)
            at_least_as_good_def preference_def rational_preference_def)
    next
      assume as: "b ≽[relation] a"
      then have "α *⇩R a + β *⇩R b ≽[relation] a"
        by (metis add.commute assms(2) reals weak_convex1D)
      have "α *⇩R a + β *⇩R b ≽[relation] a"
        by (metis as add.commute  assms(2)
            reals(1,2,3) weak_convex1D)
      then have "α *⇩R a + β *⇩R b ≽[relation] x"
        by (meson a_g_x assms(1) preference.indiff_trans x_in
            preference.not_outside rational_preference.axioms(1)
            rational_preference.strict_is_neg_transitive )
      then show ?thesis
        using pref_in_at_least_as by blast
    qed
  qed
qed

lemma convex_imp_convex_str_upper_cnt:
  assumes "∀x ∈ carrier. convex (at_least_as_good x carrier relation)"
  shows "convex (at_least_as_good x carrier relation - as_good_as x carrier relation)"
    (is "convex ( ?a - ?b)")
proof (rule convexI)
  fix a y u v
  assume as_a: "a ∈ ?a - ?b"
  assume as_y: "y ∈ ?a - ?b"
  assume reals: "0 ≤ (u::real)" "0 ≤ v" "u + v = 1"
  have cvx: "weak_convex_pref relation "
    by (meson assms at_least_as_goodD convexI have_rpr
        preference_def rational_preference.axioms(1) weak_convex1I)
  then have a_g_x: "a ≻[relation] x"
    using as_a by blast
  then have y_gt_x: "y ≻[relation] x"
    using as_y by blast
  show "u *⇩R a + v *⇩R y ∈ ?a - ?b"
  proof
    show "u *⇩R a + v *⇩R y ∈ ?a"
      by (metis DiffD1 a_g_x as_a as_y assms convexD reals have_rpr
          preference_def rational_preference.axioms(1))
  next
    have "a ≽[relation] y ∨ y ≽[relation] a"
      by (meson a_g_x y_gt_x assms(1) preference.not_outside have_rpr
          rational_preference.axioms(1) rational_preference.strict_not_refl_weak)
    then show "u *⇩R a + v *⇩R y ∉ ?b"
    proof
      assume "a ≽[relation] y"
      then have "u *⇩R a + v *⇩R y ≽[relation] y"
        using cvx assms(1) reals by blast
      then have "u *⇩R a + v *⇩R y ≻[relation] x"
        using y_gt_x by (meson assms(1) rational_preference.axioms(1) have_rpr
            rational_preference.strict_is_neg_transitive preference_def)
      then show "u *⇩R a + v *⇩R y ∉ as_good_as x carrier relation"
        by blast
    next
      assume "y ≽[relation] a"
      then have "u *⇩R a + v *⇩R y ≽[relation] a"
        using cvx assms(1) reals by (metis add.commute weak_convex1D)
      then have "u *⇩R a + v *⇩R y ≻[relation] x"
        by (meson a_g_x assms(1) rational_preference.strict_is_neg_transitive
            rational_preference.axioms(1) preference_def have_rpr)
      then show "u *⇩R a + v *⇩R y ∉ ?b"
        by blast
    qed
  qed
qed

end

subsubsection ‹ Monotone preferences ›

definition weak_monotone_prefs :: "'a set ⇒ ('a::ord) relation ⇒ bool"
  where
    "weak_monotone_prefs B P ⟷ (∀x ∈ B. ∀y ∈ B. x ≥ y ⟶ x ≽[P]y)"

definition monotone_preference :: "'a set ⇒ ('a::ord) relation ⇒ bool"
  where
    "monotone_preference B P ⟷ (∀x ∈ B. ∀y ∈ B. x > y ⟶ x ≻[P] y)"


text ‹ Given a carrier set that is unbounded above (not the "standard" mathematical definition),
       monotonicity implies local non-satiation. ›

lemma unbounded_above_mono_imp_lns:
  assumes "∀M ∈ carrier. (∀x > M. x ∈ carrier)"
  assumes mono: "monotone_preference (carrier:: 'a::ordered_euclidean_space set) relation"
  shows "local_nonsatiation carrier relation"
proof(rule lns_distI)
  fix x and e::"real"
  assume x_in: "x ∈ carrier"
  assume gz : "e > 0"
  show "∃y∈carrier. dist y x ≤ e ∧ y ≽[relation] x ∧ (x, y) ∉ relation"
  proof-
    obtain v :: real where
      v:"v < e" "0 < v" using gz dense by blast
    obtain i where
      i:"(i::'a) ∈ Basis" by fastforce
    define y where
      y_value : "y = x + v *⇩R i"
    have ge:"y ≥ x"
      using y_value i unfolding y_value
      by (simp add: v(2) zero_le_scaleR_iff)
    have "y ≠ x"
      using y_value i unfolding y_value
      using v(2) by auto
    hence y_str_g_x : "y > x"
      using ge by auto
    have y_in: "y ∈ carrier"
      using assms(1) x_in y_str_g_x by blast
    then have y_pref_x : "y ≻[relation] x"
      using y_str_g_x x_in mono monotone_preference_def  by blast
    hence " norm (y - x) ≤ e"
      using ‹0 < v› y_value y_value i v by auto
    hence dist_less_e : "dist y x ≤ e"
      by (simp add: dist_norm)
    thus ?thesis
      using y_pref_x dist_less_e y_in by blast
  qed
qed

end