Commit 511f26a4 authored by Ralf Jung's avatar Ralf Jung
Browse files

Add Dave's proof macros

parent 2c1c1ab8
\ No newline at end of file
......@@ -82,7 +82,7 @@ action on morphisms).
% \protStatus &::=& \enabled \ALT \disabled \\[0.4em]
\textdom{Res} &\eqdef&
\{\, \res = (\pres, \ghostRes) \mid
\{\, \rs = (\pres, \ghostRes) \mid
\pres \in \textdom{State} \uplus \{\munit\} \land \ghostRes \in \mcarp{\monoid} \,\} \\[0.5em]
(\pres, \ghostRes) \rsplit
(\pres', \ghostRes') &\eqdef&
......@@ -92,17 +92,17 @@ action on morphisms).
\res \leq \res' & \eqdef &
\Exists \res''. \res' = \res \rsplit \res''\\[1em]
\rs \leq \rs' & \eqdef &
\Exists \rs''. \rs' = \rs \rsplit \rs''\\[1em]
\UPred(\textdom{Res}) &\eqdef&
\{\, p \subseteq \mathbb{N} \times \textdom{Res} \mid
\All (k,\res) \in p.
\All (k,\rs) \in p.
\All j\leq k.
\All \res' \geq \res.
(j,\res')\in p \,\}\\[0.5em]
\All \rs' \geq \rs.
(j,\rs')\in p \,\}\\[0.5em]
\restr{p}{k} &\eqdef&
\{\, (j, \res) \in p \mid j < k \,\}\\[0.5em]
\{\, (j, \rs) \in p \mid j < k \,\}\\[0.5em]
p \nequiv{n} q & \eqdef & \restr{p}{n} = \restr{q}{n}\\[1em]
\textdom{PreProp} & \cong &
......@@ -187,7 +187,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
%\typedsection{Validity}{valid : \pset{\textdom{Prop}} \in Sets}
%valid(p) &\iff \All n \in \mathbb{N}. \All \res \in \textdom{Res}. \All W \in \textdom{World}. (n, \res) \in p(W)
%valid(p) &\iff \All n \in \mathbb{N}. \All \rs \in \textdom{Res}. \All W \in \textdom{World}. (n, \rs) \in p(W)
\typedsection{Later modality}{\later : \textdom{Prop} \to \textdom{Prop} \in {\cal U}}
......@@ -213,7 +213,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
%&\forall p, q \in \textdom{Prop}.~\\
% (\forall n \in \mathbb{N}.~\forall \res \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \res) \in p(W) \Rightarrow (n, \res) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)})
% (\forall n \in \mathbb{N}.~\forall \rs \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \rs) \in p(W) \Rightarrow (n, \rs) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)})
......@@ -232,11 +232,11 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\textdom{World} \to \psetdown{\mathbb{N}} \in {\cal U}}
\ralf{Make this Dave-compatible: Explicitly compose all the things in $s$}
\fullSat{\state}{\mask}{\res}{W} &=
\fullSat{\state}{\mask}{\rs}{W} &=
\{\, n + 1 \in \mathbb{N} \mid &\Exists \resB:\mathbb{N} \fpfn \textdom{Res}. (\res \rsplit \resB).\pres = \state \land{}\\
&\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\resB) \land {}\\
&\quad\quad \iota \in \mask \ra (n, \resB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \}
\{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rsplit \rsB).\pres = \state \land{}\\
&\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\
&\quad\quad \iota \in \mask \ra (n, \rsB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \}
......@@ -248,9 +248,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\All \state \in \Delta(\textdom{State}).
\All \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}).
\All \res, \resB \in \Delta(\textdom{Res}).
\All \rs, \rsB \in \Delta(\textdom{Res}).
\All W \in \textdom{World}. \\&
\mask_1 \subseteq \mask_2 \implies (\fullSat{\state}{\mask_2}{\res}{W}) \subseteq (\fullSat{\state}{\mask_1}{\res}{W})
\mask_1 \subseteq \mask_2 \implies (\fullSat{\state}{\mask_2}{\rs}{W}) \subseteq (\fullSat{\state}{\mask_1}{\rs}{W})
......@@ -293,11 +293,11 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\mathit{vs}_{\mask_1}^{\mask_2}(q) &= \Lam W.
\{\, (n, \res) &\mid \All W_F \geq W. \All \res_F, \mask_F, \state. \All k \leq n.\\
\{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\
k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\res \rsplit \res_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
\Exists W' \geq W_F. \Exists \res'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k, \res') \in q(W')
\Exists W' \geq W_F. \Exists \rs'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(W')
......@@ -338,10 +338,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
% \All \iota \in \mathbb{N}.
% \All p \in \textdom{Prop}.
% \All W \in \textdom{World}.
% \All \res \in \textdom{Res}.
% \All \rs \in \textdom{Res}.
% \All n \in \mathbb{N}. \\
% (n, \res) \in inv(\iota, p)(W) \implies (n, \res) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W)
% (n, \rs) \in inv(\iota, p)(W) \implies (n, \rs) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W)
......@@ -352,10 +352,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
% \forall \iota \in \mathbb{N}.~
% \forall p \in \textdom{Prop}.~
% \forall W \in \textdom{World}.~
% \forall \res \in \textdom{Res}.~
% \forall \rs \in \textdom{Res}.~
% \forall n \in \mathbb{N}.~\\
% (n, \res) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \res) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W)
% (n, \rs) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \rs) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W)
......@@ -392,22 +392,22 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\mathit{wp}_\mask(\expr, q) &\eqdef \Lam W.
\{\, (n, \res) &\mid \All W_F \geq W; k \leq n; \res_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\res \rsplit \res_F}{W_F}) \implies{}\\
\{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \implies{}\\
(\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \res'. \\
(\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\
k \in (\fullSat{\state}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k, \res') \in q(\expr)(W'))~\land \\
k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
(\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \res'. \\
(\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\
k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k-1, \res') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
(\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \res', \res_1', \res_2'. \\
(\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\
k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land \res' = \res_1' \rsplit \res_2'~\land \\
k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land \rs' = \rs_1' \rsplit \rs_2'~\land \\
(k-1, \res_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
(k-1, \res_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
(k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
(k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
......@@ -491,9 +491,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\semTerm{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &=
inv(\semTerm{\vctx \proves \iname : \textsort{InvName}}_\gamma, \semTerm{\vctx \proves \prop : \Prop}_\gamma) \\
\semTerm{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &=
\Lam W. \{\, (n, \res) \mid \res.\ghostRes \geq \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\
\Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\
\semTerm{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &=
\Lam W. \{\, (n, \res) \mid \res.\pres = \semTerm{\vctx \proves \state : \textsort{State}}_\gamma \,\}
\Lam W. \{\, (n, \rs) \mid \rs.\pres = \semTerm{\vctx \proves \state : \textsort{State}}_\gamma \,\}
......@@ -513,10 +513,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\forall n \in \mathbb{N}.\;
\forall W \in \textdom{World}.\;
\forall \res \in \textdom{Res}.\;
\forall \rs \in \textdom{Res}.\;
\forall \gamma \in \semSort{\vctx},\;
\bigl(\All \propB \in \pfctx. (n, \res) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W)\bigr)
\implies (n, \res) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W)
\bigl(\All \propB \in \pfctx. (n, \rs) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W)\bigr)
\implies (n, \rs) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W)
\ No newline at end of file
\ No newline at end of file
% Locallabel
% Copyright (C) 2001, 2002, 2003 Didier Rmy
% Author : Didier Remy
% Version : 1.1.1
% Bug Reports : to author
% Web Site :
% Locallabel is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
% Locallabel is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% GNU General Public License for more details
% (
% File locallabel.sty (LaTeX macros)
%% Identification
[2001/23/02 v0.92 Locallabel]
%% Preliminary declarations
%% Options
%% More declarations
%% We use two counters: The global counter is incremented at each reset.
%% Its value is the ``group'' of a local.
%% The local counter is the last numeric value of a bound label in the
%% current group. The value of a label #1 is globally set to
%% \csname llb@\the\c@llb@global-#1\endcsname
%% The global command \csname llb@\the\c@llb@global-#1*\endcsname is
%% use to ensure that a label is only bound once. Usually a label is
%% bound and declared at the same time with \llabel. It may also be bound in
%% advance, with \lbind, for instance so as to control the numbering.
%% Then, another \llabel must be used to declare it in the text.
%% If no \lbind has been used before, the \llabel calls \lbind implicitlt.
\newcommand \llb@find [1]
{\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
\message {*** Local label #1 undefined in this context}%
\edef \llb@current {#1??}%
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}%
\newcommand \llb@make [1]
{\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
\stepcounter{llb@local}\relax \expandafter
\xdef \csname llb@\the\c@llb@global-#1\endcsname {\the\c@llb@local}%
\edef \llb@current {\the\c@llb@local}%
\expandafter \ifx \csname llb@\the\c@llb@global-#1*\endcsname \relax
\message {*** Local label #1 already defined in this countext!}%
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname ??}%
\expandafter \global \expandafter \let
\csname llb@\the\c@llb@global-#1*\endcsname \relax
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}
%%% Redefine those macros to change typsetting
\newcommand \thelocallabel {\the \c@llb@local}
\newcommand \LlabelTypeset [1] {(\textrm {\bfseries #1})}
\newcommand \LrefTypeset [1] {(\textrm {#1)}}
\newcommand \glabel [1]{\LlabelTypeset{\softtarget {#1}{#1}}}
\newcommand \gref [1]{\LrefTypeset{\softlink {#1}{#1}}}
%%% To reset all local labels---which just increment a global prefix.
\newcommand \locallabelreset[1][0]%
{\stepcounter {llb@global}\setcounter {llb@local}{#1}}
%%% Make a new local label, typeset it, and bind to the given name
\def \llb@relax {\relax}
\newcommand {\llabel}[2][\relax]%
\def \@test {#1}\ifx \@test\llb@relax\else
\edef \@currentlabel {\the\c@llb@local}%
\def \@test {#1}\ifx \@test\empty \def \@test{#2}\fi
\LlabelTypeset {\softtarget{llb@\the\c@llb@global-#2}{\llb@current}}}
%%% Retreive the local label of given name and type set it.
\newcommand \lref [1]
{\llb@find {#1}%
\LrefTypeset {\softlink {llb@\the\c@llb@global-#1}{\llb@current}}}
%%% Make a new local label and bind it to the given name but do not typeset
%%% it. Typesetting may then be done with \llabel non locally. Useful to
%%% control the order of numberring.
\newcommand \lbind [1]
{\llb@make {#1}%
\expandafter \global \expandafter
\let \csname llb@\the\c@llb@global-#1*\endcsname \empty}
\AtBeginDocument {%
\@ifundefined{softlink}{\let \softlink \@secondoftwo}{}%
\@ifundefined{softtarget}{\let \softtarget \@secondoftwo}{}%
%% This is file `pfsteps.sty',
%% generated with the docstrip utility.
%% The original source files were:
%% pfsteps.dtx (with options: `package')
%% Copyright (C) 2011 by Jesse A. Tov
%% This file may be distributed and/or modified under the conditions of the
%% LaTeX Project Public License, either version 1.2 of this license or (at
%% your option) any later version. The latest version of this license is
%% in:
%% and version 1.2 or later is part of all distributions of LaTeX
%% version 1999/12/01 or later.
[2011/04/04 v0.4 proof tools]
\expandafter\let\csname #1pfsteps@#2\endcsname#3
{\csname\pfsteps@pfc@{\pfsteps@strip#1 \@empty}\endcsname}
{pfsteps@pfc@\pfsteps@strip#1 \@empty @\thepfsectioncounter}
\def\pfsteps@strip#1 #2{%
{Proof step (#1) already defined in this section}%
\csname pfsteps@pfc@#1@#2\endcsname
{Proof step (##1) not yet defined in this section}%
, #1\let\listitem\pfsteps@pfref@listitem@rest
\ifcsname hypertarget\endcsname
{\pfsteps@unmath{\penalty-1 \mbox{~}\hfill%
\raggedright##1 ##2%
\expandafter\gdef\csname pfsteps\atsign setup\atsign atsign\endcsname{
\gdef@##1 {\pflabel{##1}}
\pfstepsSetupUnicode{171}{»}{8226} % « » •
\providecommand{\byCasesCaseTemplate}[1]{\textbf{Case\ \ \fbox{#1}}}
\ifcsname inferrule\endcsname\let\icase\byCases@icase\fi
\list{}{\labelwidth\z@ \itemindent-\leftmargin
{\item[{\let\AND\byCases@and #2}]\strut#1\pfsteps@reallynopagebreak}
\@ifnextchar* \byCases@icase@star \byCases@icase@nostar
\@ifnextchar [{\byCases@icase@opts{#1}}{\byCases@icase@noopts{#1}}
\@ifnextchar [
%% End of file `pfsteps.sty'.
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
%% Biimplication inference rules
% \biimp above below
% The double lines obtained by the simpler
% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
% mask E_M in an atomic triple).
%% inferH is infer with hyperlinked names.
% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
% Think @currentlabel : text ref.
\edef\@currentlabel{#2}% Save text
\phantomsection% Correct hyper reference link