Theory RPRs
theory RPRs
imports FSext
begin
section‹Preliminaries›
text‹
The auxiliary concepts defined here are standard \<^cite>‹"Routley:79" and "Sen:70a" and "Taylor:2005"›. Throughout we make use of a fixed set @{term "A"} of
alternatives, drawn from some arbitrary type @{typ "'a"} of suitable
size. Taylor \<^cite>‹"Taylor:2005"› terms this set an \emph{agenda}. Similarly
we have a type @{typ "'i"} of individuals and a population @{term "Is"}.
›
subsection‹Rational Preference Relations (RPRs)›
text‹
Definitions for rational preference relations (RPRs), which represent
indifference or strict preference amongst some set of alternatives. These
are also called \emph{weak orders} or (ambiguously) \emph{ballots}.
Unfortunately Isabelle's standard ordering operators and lemmas are
typeclass-based, and as introducing new types is painful and we need several
orders per type, we need to repeat some things.
›
type_synonym 'a RPR = "('a * 'a) set"
abbreviation rpr_eq_syntax :: "'a ⇒ 'a RPR ⇒ 'a ⇒ bool" (‹_ ⇘_⇙≼ _› [50, 1000, 51] 50) where
"x ⇘r⇙≼ y == (x, y) ∈ r"
definition indifferent_pref :: "'a ⇒ 'a RPR ⇒ 'a ⇒ bool" (‹_ ⇘_⇙≈ _› [50, 1000, 51] 50) where
"x ⇘r⇙≈ y ≡ (x ⇘r⇙≼ y ∧ y ⇘r⇙≼ x)"
lemma indifferent_prefI[intro]: "⟦ x ⇘r⇙≼ y; y ⇘r⇙≼ x ⟧ ⟹ x ⇘r⇙≈ y"
unfolding indifferent_pref_def by simp
lemma indifferent_prefD[dest]: "x ⇘r⇙≈ y ⟹ x ⇘r⇙≼ y ∧ y ⇘r⇙≼ x"
unfolding indifferent_pref_def by simp
definition strict_pref :: "'a ⇒ 'a RPR ⇒ 'a ⇒ bool" (‹_ ⇘_⇙≺ _› [50, 1000, 51] 50) where
"x ⇘r⇙≺ y ≡ (x ⇘r⇙≼ y ∧ ¬(y ⇘r⇙≼ x))"
lemma strict_pref_def_irrefl[simp]: "¬ (x ⇘r⇙≺ x)" unfolding strict_pref_def by blast
lemma strict_prefI[intro]: "⟦ x ⇘r⇙≼ y; ¬(y ⇘r⇙≼ x) ⟧ ⟹ x ⇘r⇙≺ y"
unfolding strict_pref_def by simp
text‹
Traditionally, @{term "x ⇘r⇙≼ y"} would be written $x\ R\ y$,
@{term "x ⇘r⇙≈ y"} as $x\ I\ y$ and @{term "x
⇘r⇙≺ y"} as $x\ P\ y$, where the relation $r$ is implicit, and
profiles are indexed by subscripting.
›
text‹
\emph{Complete} means that every pair of distinct alternatives is
ranked. The "distinct" part is a matter of taste, as it makes sense to
regard an alternative as as good as itself. Here I take reflexivity
separately.
›
definition complete :: "'a set ⇒ 'a RPR ⇒ bool" where
"complete A r ≡ (∀x ∈ A. ∀y ∈ A - {x}. x ⇘r⇙≼ y ∨ y ⇘r⇙≼ x)"
lemma completeI[intro]:
"(⋀x y. ⟦ x ∈ A; y ∈ A; x ≠ y ⟧ ⟹ x ⇘r⇙≼ y ∨ y ⇘r⇙≼ x) ⟹ complete A r"
unfolding complete_def by auto
lemma completeD[dest]:
"⟦ complete A r; x ∈ A; y ∈ A; x ≠ y ⟧ ⟹ x ⇘r⇙≼ y ∨ y ⇘r⇙≼ x"
unfolding complete_def by auto
lemma complete_less_not: "⟦ complete A r; hasw [x,y] A; ¬ x ⇘r⇙≺ y ⟧ ⟹ y ⇘r⇙≼ x"
unfolding complete_def strict_pref_def by auto
lemma complete_indiff_not: "⟦ complete A r; hasw [x,y] A; ¬ x ⇘r⇙≈ y ⟧ ⟹ x ⇘r⇙≺ y ∨ y ⇘r⇙≺ x"
unfolding complete_def indifferent_pref_def strict_pref_def by auto
lemma complete_exh:
assumes "complete A r"
and "hasw [x,y] A"
obtains (xPy) "x ⇘r⇙≺ y"
| (yPx) "y ⇘r⇙≺ x"
| (xIy) "x ⇘r⇙≈ y"
using assms unfolding complete_def strict_pref_def indifferent_pref_def by auto
text‹
Use the standard @{term "refl"}. Also define \emph{irreflexivity}
analogously to how @{term "refl"} is defined in the standard library.
›
declare refl_onI[intro] refl_onD[dest]
lemma complete_refl_on:
"⟦ complete A r; refl_on A r; x ∈ A; y ∈ A ⟧ ⟹ x ⇘r⇙≼ y ∨ y ⇘r⇙≼ x"
unfolding complete_def by auto
definition irrefl :: "'a set ⇒ 'a RPR ⇒ bool" where
"irrefl A r ≡ r ⊆ A × A ∧ (∀x ∈ A. ¬ x ⇘r⇙≼ x)"
lemma irreflI[intro]: "⟦ r ⊆ A × A; ⋀x. x ∈ A ⟹ ¬ x ⇘r⇙≼ x ⟧ ⟹ irrefl A r"
unfolding irrefl_def by simp
lemma irreflD[dest]: "⟦ irrefl A r; (x, y) ∈ r ⟧ ⟹ hasw [x,y] A"
unfolding irrefl_def by auto
lemma irreflD'[dest]:
"⟦ irrefl A r; r ≠ {} ⟧ ⟹ ∃x y. hasw [x,y] A ∧ (x, y) ∈ r"
unfolding irrefl_def by auto
text‹Rational preference relations, also known as weak orders and (I
guess) complete pre-orders.›
definition rpr :: "'a set ⇒ 'a RPR ⇒ bool" where
"rpr A r ≡ complete A r ∧ r ⊆ A × A ∧ refl_on A r ∧ trans r"
lemma rprI[intro]: "⟦ complete A r; r ⊆ A × A; refl_on A r; trans r ⟧ ⟹ rpr A r"
unfolding rpr_def by simp
lemma rprD: "rpr A r ⟹ complete A r ∧ refl_on A r ∧ trans r"
unfolding rpr_def by simp
lemma rpr_in_set[dest]: "⟦ rpr A r; x ⇘r⇙≼ y ⟧ ⟹ {x,y} ⊆ A"
unfolding rpr_def refl_on_def by auto
lemma rpr_refl[dest]: "⟦ rpr A r; x ∈ A ⟧ ⟹ x ⇘r⇙≼ x"
unfolding rpr_def by blast
lemma rpr_less_not: "⟦ rpr A r; hasw [x,y] A; ¬ x ⇘r⇙≺ y ⟧ ⟹ y ⇘r⇙≼ x"
unfolding rpr_def by (auto simp add: complete_less_not)
lemma rpr_less_imp_le[simp]: "⟦ x ⇘r⇙≺ y ⟧ ⟹ x ⇘r⇙≼ y"
unfolding strict_pref_def by simp
lemma rpr_less_imp_neq[simp]: "⟦ x ⇘r⇙≺ y ⟧ ⟹ x ≠ y"
unfolding strict_pref_def by blast
lemma rpr_less_trans[trans]: "⟦ x ⇘r⇙≺ y; y ⇘r⇙≺ z; rpr A r ⟧ ⟹ x ⇘r⇙≺ z"
unfolding rpr_def strict_pref_def trans_def by blast
lemma rpr_le_trans[trans]: "⟦ x ⇘r⇙≼ y; y ⇘r⇙≼ z; rpr A r ⟧ ⟹ x ⇘r⇙≼ z"
unfolding rpr_def trans_def by blast
lemma rpr_le_less_trans[trans]: "⟦ x ⇘r⇙≼ y; y ⇘r⇙≺ z; rpr A r ⟧ ⟹ x ⇘r⇙≺ z"
unfolding rpr_def strict_pref_def trans_def by blast
lemma rpr_less_le_trans[trans]: "⟦ x ⇘r⇙≺ y; y ⇘r⇙≼ z; rpr A r ⟧ ⟹ x ⇘r⇙≺ z"
unfolding rpr_def strict_pref_def trans_def by blast
lemma rpr_complete: "⟦ rpr A r; x ∈ A; y ∈ A ⟧ ⟹ x ⇘r⇙≼ y ∨ y ⇘r⇙≼ x"
unfolding rpr_def by (blast dest: complete_refl_on)
subsection‹Profiles›
text ‹A \emph{profile} (also termed a collection of \emph{ballots}) maps
each individual to an RPR for that individual.›
type_synonym ('a, 'i) Profile = "'i ⇒ 'a RPR"
definition profile :: "'a set ⇒ 'i set ⇒ ('a, 'i) Profile ⇒ bool" where
"profile A Is P ≡ Is ≠ {} ∧ (∀i ∈ Is. rpr A (P i))"
lemma profileI[intro]: "⟦ ⋀i. i ∈ Is ⟹ rpr A (P i); Is ≠ {} ⟧ ⟹ profile A Is P"
unfolding profile_def by simp
lemma profile_rprD[dest]: "⟦ profile A Is P; i ∈ Is ⟧ ⟹ rpr A (P i)"
unfolding profile_def by simp
lemma profile_non_empty: "profile A Is P ⟹ Is ≠ {}"
unfolding profile_def by simp
end