Theory First_Welfare_Theorem.Syntax

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

section ‹ Introducing Syntax ›

text ‹ Syntax, abbreviations and type-synonyms ›

theory Syntax
  imports Main
begin


type_synonym 'a relation = "('a × 'a) set"

abbreviation gen_weak_stx :: "'a ⇒ 'a relation ⇒ 'a ⇒ bool"
  (‹_ ≽[_] _› [51,100,51] 60)
  where
    "x ≽[P] y ≡ (x, y) ∈ P"

abbreviation gen_indif_stx :: "'a ⇒ 'a relation ⇒ 'a ⇒ bool"
  (‹_ ≈[_] _› [51,100,51] 60)
  where
    "x ≈[P] y ≡ x ≽[P] y ∧ y ≽[P] x "

abbreviation gen_strc_stx :: "'a ⇒ 'a relation ⇒ 'a ⇒ bool"
  (‹_ ≻[_] _› [51,100,51] 60)
  where
    "x ≻[P] y ≡  x ≽[P] y ∧ ¬y ≽[P] x "


end