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