%note : include the file AFTER changing math fonts (e.g. \usepackage{mathpazo})
%       otherwise, \renewcommand{\phi}{\varphi} will produce an error

    \usepackage{stmaryrd}
	\usepackage{amsmath}
	\usepackage{amsthm}
	\usepackage{amssymb}
	\usepackage{amsfonts}
	\usepackage{xspace}

%a faire au début, car sinon renew fait chier 
        \renewcommand{\phi}{\varphi}
        \renewcommand{\equiv}{\Leftrightarrow}

        \newcommand{\anote}[1]{\marginpar[\raggedleft\footnotesize\itshape#1\par]{\raggedright\footnotesize\itshape#1\par}}% %
        \newcommand{\removenotes}{\renewcommand{\anote}[1]{}}
        \newcommand{\achtung}[1]{\anote{\textcolor{red}{#1}}}


%dummy variable (anonyme), cf syntaxe prolog
        \newcommand{\dummy}{\ensuremath{\_}\xspace}

%environnement de citation perso
\newenvironment{itquote}
{	\begin{quote}
        \itshape
}
{
        \end{quote}
}


%logiques
\newcommand{\LTL}{\textsc{ltl}\xspace}      % linear temporal logic
\newcommand{\SDL}{\textsc{sdl}\xspace}      % standard deontic logic
\newcommand{\CTL}{\textsc{ctl}\xspace}      % computational tree logic
\newcommand{\CTLS}{\textsc{ctl$^\star$}\xspace}
\newcommand{\HML}{\textsc{hml}\xspace}      % Henessy-Milner Logic
\newcommand{\FOL}{\textsc{fol}\xspace}      % first-order logic
\newcommand{\MSO}{\textsc{mso}\xspace}      % monadic second order
\newcommand{\IL}{\textsc{il}\xspace}        % intuituionistic
\newcommand{\CL}{\textsc{cl}\xspace}        % classical logic

%fun programming et langages
\newcommand{\GADT}{\textsc{gadt}\xspace}        % Generalized Algebraic DataType
\newcommand{\DSL}{\textsc{dsl}\xspace}          % Domain Specific Langage
\newcommand{\EDSL}{\textsc{edsl}\xspace}        % Embedded Domain Specific Langage
\newcommand{\BNF}{\textsc{bnf}\xspace}          % Backus-Naur Form
\newcommand{\STL}{\textsc{stl}\xspace}          % Standard Template Library
\newcommand{\HASKELL}{\textsc{Haskell}\xspace}  % Haksell programming language

%bases de données
\newcommand{\SGBDR}{\textsc{Sgbdr}\xspace}
\newcommand{\SQL}{\textsc{sql}\xspace}          % Structured Query Language
\newcommand{\DATALOG}{\textsc{Datalog}\xspace}  % Datalog
\newcommand{\SPJU}{\textsc{spju}\xspace}        % Select-Project-Join-Union query language
\newcommand{\SPJRU}{\textsc{spjru}\xspace}      % Select-Project-Join-Renaming-Union query language
\newcommand{\RDF}{\textsc{rdf}\xspace}          % Resource Description Framework
\newcommand{\XML}{\textsc{xml}\xspace}          % eXtensible Markup Language



%misc
\newcommand{\REF}{~[référence]\xspace}      % référence à citer
\newcommand{\AOC}{~[Choix?!]\xspace}        % axiom of choice
\newcommand{\ie}{\emph{id est}\xspace}      % id est
\newcommand{\st}{\emph{such that}\xspace}   % such that

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




% shortcuts pour les catégorie :
%   - s'assurer de l'homogénéité de la notation
%   - de la faisabilité : on postpone tous les symboles jusqu'à la réduction finale

%catégorie
    %un categorie
    \newcommand{\cat}[1]{\ensuremath{\mathbf{#1}}\xspace}

    % objets
    \newcommand{\ob}[1]{\ensuremath{#1}\xspace}
    \newcommand{\finalob}{\cat{1}\xspace}
    \newcommand{\initialob}{\cat{0}\xspace}


    % morphismes
    \newcommand{\mo}{\ensuremath{\rightarrow}\xspace}
    \newcommand{\xmo}[1]{\ensuremath{\xrightarrow{#1}}\xspace}
    % composition
    \newcommand{\co}{\ensuremath{\circ}\xspace}

    % morphismes identité
    \newcommand{\id}[1][]{\ensuremath{id_{#1}}\xspace}

    %isomorphisms
    \newcommand{\iso}{\ensuremath{\cong}}
    \newcommand{\isomto}{\overset{\sim}{\mo}}

    %ensemble de morphismes
    \DeclareMathOperator{\Hom}{Hom}

    % deux catégories ``anonymes''
    \newcommand{\C}{\cat{C}}
    \newcommand{\D}{\cat{D}}

    % catégories ``supposées''
    \newcommand{\Calc}{\cat{Calc}}
    \newcommand{\Jur}{\cat{Jur}}
    \newcommand{\Hask}{\cat{Hask}}

    %des catégories classiques
    \newcommand{\CCC}{\cat{CCC}}
    \newcommand{\CPO}{\cat{CPO}}
    \newcommand{\SET}{\cat{Set}}
    \newcommand{\REL}{\cat{Rel}}

% foncteurs
    %un foncteur
    \newcommand{\func}[1]{\ensuremath{\MakeUppercase{#1}}}
    % foncteur identité dans une catégorie C
    \newcommand{\idF}[1]{\ensuremath{\func{I}_\cat{#1}}}
    % trois foncteurs anonymes
    \newcommand{\F}{\func{F}\xspace}
    \newcommand{\G}{\func{G}\xspace}
    \renewcommand{\H}{\func{H}\xspace}

%transformations naturelles
    %une transformation nat.
    \newcommand{\nat}{\ensuremath{\dot\rightarrow}\xspace}
    % adjonction à droite
    \newcommand{\ladj}{\ensuremath{\dashv}\xspace}


%produit
    \newcommand{\fst}{\ensuremath{\pi_1}\xspace} %premier composant
    \newcommand{\snd}{\ensuremath{\pi_2}\xspace} %second composant

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%algèbre (functorielle)
    %tiret mode math
    \mathchardef\mhyphen="2D
    %categories des algebres d'un foncteur
    \newcommand{\alg}[1]{\ensuremath{\cat{#1 \mhyphen Alg}}}
    % support
    \newcommand{\carrier}[1]{\ensuremath{\lvert #1 \rvert}}
    %point fixe d'un foncteur
    \newcommand{\fix}[1]{\ensuremath{\mu #1}}
    %catamorphism
    \newcommand{\cata}[1]{\ensuremath{\llparenthesis #1 \rrparenthesis}}
    %catamorphism
    \newcommand{\ana}[1]{\ensuremath{[\!(#1)\!]}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %structures de Kripke
    \newcommand{\Worlds}{\ensuremath{W}\xspace}
    \newcommand{\Rel}{\ensuremath{W}\xspace}
    \newcommand{\KF}{\ensuremath{\langle \Worlds, R\subseteq S\times S\rangle}\xspace}
    \newcommand{\KFS}{\ensuremath{\langle \Worlds, R\subseteq S\times S, \Sigma, L:S \rightarrow 2^{\Sigma} \rangle}\xspace}
    \newcommand{\LKF}{\ensuremath{\langle \Worlds, A, R\subseteq S\times A \times S\rangle}\xspace}
    \newcommand{\LKFS}{\ensuremath{\langle \Worlds, A, R\subseteq S\times A \times S, \Sigma, L:S \rightarrow 2^{\Sigma} \rangle}\xspace}

    %modele
    \newcommand{\Mod}{\ensuremath{\mathcal{M}}\xspace}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %généralités
    
    %égalité par définition
    \DeclareMathOperator{\eqdef}{\stackrel{def}{=}} 
    %tel que
    \newcommand{\tq}{\ensuremath{\text{\: t.q.\: }}}
    %cardinalité
    \newcommand{\card}[1]{\ensuremath{\lvert #1 \rvert}}
    %powerset
    \newcommand{\Pow}{\ensuremath{\wp}\xspace}
    %type(set) ensembles
    \newcommand{\setft}[1]{\mathcal{#1}}
    %flèche de l'implication
    \DeclareMathOperator{\imp}{\Rightarrow} 

    %ensembles rigolos
    \newcommand{\bbfont}[1]{\mathbb{#1}} % typo blackboard
    \newcommand{\CC}{\ensuremath{\bbfont{C}}\xspace} %	nombres complexes
    \newcommand{\GG}{\ensuremath{\bbfont{G}}\xspace} %	pour groupe multiplicatif/additif
    \newcommand{\NN}{\ensuremath{\bbfont{N}}\xspace} %	nombres naturels
    \newcommand{\QQ}{\ensuremath{\bbfont{Q}}\xspace} %	nombres rationnels
    \newcommand{\RR}{\ensuremath{\bbfont{R}}\xspace} %	nombres réels
    \newcommand{\ZZ}{\ensuremath{\bbfont{Z}}\xspace} %	entiers

    %classifiers, small finite sets
    \newcommand{\BB}{\ensuremath{\bbfont{B}}\xspace} %	booléens
    \newcommand{\Tri}{\ensuremath{\BB_{3}}\xspace} %	tri-valués

    \newcommand{\true}{\ensuremath{\mathbf{tt}}\xspace} %	booléens
    \newcommand{\false}{\ensuremath{\mathbf{ff}}\xspace} %	booléens
    %\newcommand{\true}{\ensuremath{\mathbf{1}}\xspace} %	booléens
    %\newcommand{\false}{\ensuremath{\mathbf{0}}\xspace} %	booléens
    \newcommand{\und}{\ensuremath{\bot}\xspace} %	booléens
%     \newcommand{\true}{\ensuremath{\top}\xspace} %	booléens
%     \newcommand{\false}{\ensuremath{\bot}\xspace} %	booléens
%     \newcommand{\und}{\ensuremath{\mathbf{u}}\xspace} %	booléens


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % Structure d'interprétation

    \newcommand{\myset}[1]{\mathsf{#1}}

    %traces
    \newcommand{\Ind}{\ensuremath{\myset{I}}\xspace} %indices de traces
    \newcommand{\Tra}{\ensuremath{\Evt^\star}\xspace} %traces d'événements
    \newcommand{\emptyl}{\ensuremath{\varepsilon}\xspace} %traces d'événements
    \newcommand{\len}{\ensuremath{length}} %longueur
    \newcommand{\sig}[1]{\ensuremath{\sigma^{#1}}\xspace}     %point / suffixe de traces

    %pour les événements
    \newcommand{\Evt}{\ensuremath{\myset{E}}\xspace} %événements
    \newcommand{\Name}{\ensuremath{\myset{N}}\xspace} %noms des événements
    \newcommand{\Agt}{\ensuremath{\myset{A}}\xspace} %agents/acteurs
    \newcommand{\Time}{\ensuremath{\myset{T}}\xspace} %domaine des dates
    \newcommand{\Key}{\ensuremath{\myset{K}}\xspace} %clefs
    \newcommand{\Val}{\ensuremath{\myset{V}}\xspace} %clefs

    %fonction associées ?
    \newcommand{\name}{\ensuremath{\pi_{Name}}\xspace}
    \newcommand{\src}{\ensuremath{\pi_{Src}}\xspace}
    \newcommand{\dst}{\ensuremath{\pi_{Dst}}\xspace}
    \newcommand{\content}{\ensuremath{\pi_{Content}}\xspace}
    \renewcommand{\time}{\ensuremath{\pi_{Time}}\xspace}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %evaluation et sémantique

    \newcommand{\val}{\ensuremath{val}\xspace}


    \DeclareMathOperator{\leqtime}{\leqslant_\Time} 

    %Langage formel
    \newcommand{\Cond}{\ensuremath{\myset{C}}\xspace} %couche ``conditionnelle'' des règles de droit
    \newcommand{\Rule}{\ensuremath{\myset{R}}\xspace} %règle de droit
    \newcommand{\oaux}[1]{\ensuremath{\mathcal{O}_{#1}}\xspace} %un O rond pour une obligation


    %evaluation et règles
    \newcommand{\eval}{\ensuremath{\mathsf{eval}}\xspace}
    \newcommand{\full}{\ensuremath{Full}\xspace} %reussi
    \newcommand{\viol}{\ensuremath{Viol}\xspace} %raté
    \newcommand{\unkn}{\ensuremath{Unkn}\xspace} %raté



    %fonction de résiduation
     \newcommand{\step}{\ensuremath{\mathsf{step}}\xspace}

    %preuve formelle d'un matching
    \DeclareMathOperator{\fpof}{\mathbf{P}}
    \newcommand{\bag}{\ensuremath{\Delta}\xspace}
    \newcommand{\newbag}{\ensuremath{\Delta'}\xspace}

    %réécriture des règles
    \newcommand{\rw}{\rwf}
    \newcommand{\rwf}{\ensuremath{\mathsf{rw}^{+}}\xspace}
    \newcommand{\rwv}{\ensuremath{\mathsf{rw}^{-}}\xspace}
    \newcommand{\rwu}{\ensuremath{\mathsf{rw}^{u}}\xspace}

%     \newcommand{\rwf}{\ensuremath{\mathsf{rw}^{f}}\xspace}
%     \newcommand{\rwv}{\ensuremath{\mathsf{rw}^{v}}\xspace}
%     \newcommand{\rwu}{\ensuremath{\mathsf{rw}^{u}}\xspace}





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%langages formels d'intérêt : SYNTAXE

    %opérateurs du langage des règles
    \DeclareMathOperator{\conj}{\wedge}
    \DeclareMathOperator{\dead}{\lhd}               %deadline, séquencement
    \DeclareMathOperator{\ctd}{\gtrdot}               %CTD: sanction, negative trigger
    \DeclareMathOperator{\sanc}{\sanc}              %older operator for CTD, for non regression
    \DeclareMathOperator{\trig}{\rightsquigarrow}   %déclenchement, hypothèse, conséquence
    \DeclareMathOperator{\trug}{\dot{\rightsquigarrow}}   %UNIQUE déclenchement, hypothèse, conséquence
    \DeclareMathOperator{\obl}{{\oplus}}            %obligation
    \DeclareMathOperator{\for}{{\ominus}}           %interdiction
    \DeclareMathOperator{\mode}{{\odot}}            %préfixe quelconque entre \obl et \for
    \newcommand{\dual}[1]{\ensuremath{{#1}^{\dagger}}\xspace} %pour opérateurs \obl et \for



    \newcommand{\Lang}{\ensuremath{\mathcal{L}}\xspace}
    \newcommand{\Pattern}{\ensuremath{\mathcal{P}}\xspace}
    \newcommand{\evaluates}[1][{\_}]{\ensuremath{\llbracket #1\rrbracket}}
    \newcommand{\Domain}{\ensuremath{\mathbb{D}}\xspace}




    %langage connus
    \newcommand{\LCalc}{\ensuremath{\lambda}-calcul\xspace} %lambda calcul

    %opérateurs LTL
    \newcommand{\LLTL}{\ensuremath{\mathcal{L}_{\LTL}}\xspace}
    \DeclareMathOperator{\until}{\mathcal{U}} 
    \DeclareMathOperator{\weak}{\mathcal{W}} 
    \DeclareMathOperator{\since}{\mathcal{S}} 
    \DeclareMathOperator{\nex}{\circ}
    \DeclareMathOperator{\always}{\square}
    \DeclareMathOperator{\hence}{\lozenge}  

    %opérateurs déontique
    \newcommand{\LSDL}{\ensuremath{\mathcal{L}_{\SDL}}\xspace}
    \DeclareMathOperator{\dobl}{\mathcal{O}}
    \DeclareMathOperator{\dfor}{\mathcal{I}}  
    \DeclareMathOperator{\dper}{\mathcal{P}}  
    \DeclareMathOperator{\dfac}{\mathcal{F}}  

    %logiques ``qui disent''
    \DeclareMathOperator{\says}{\text{says}}
