Commit 27997821 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

simplify worra operator (disjunction is now done in the backtyping app rule)

parent 9d53d224
......@@ -116,8 +116,8 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
\apply t s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
%\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\[4mm]
\worra t s & = & \left\{\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n'),\ \dom t \wedge\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\ |\ i\in I\right\}
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\[4mm]
%\worra t s & = & \left\{\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n'),\ \dom t \wedge\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\ |\ i\in I\right\}
\end{eqnarray*}
The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
......@@ -212,16 +212,16 @@ The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
{ }
\\
\Infer[AppL*]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: S_i
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{u_i}}{[]} \ct[{x_1}{x_2}]: S_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \textstyle\bigcup_{i\in I}S_i}
{ }
\\
\Infer[AppLDom]
{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: S_1\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: S_2
{\Gamma(x_1) = u\\u\land (\arrow{\Empty}{\Any})\neq\Empty\\u\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: S_1\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: S_2
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: S_1\cup S_2}
{ }
......@@ -343,9 +343,11 @@ rules, because one branch is already unreachable and retyping only occurs with s
{ }
\\
\Infer[App]
{\worra{\Gamma(x_1)}t = \{ (u_i, t_i) \}_{i\in I} \\
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i}
{
\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\\
\forall i\in I.\ \worra{(\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j})}t = s_i' \\
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i'}
}
{
\Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
......@@ -391,9 +393,9 @@ the environment is supposed to already contain a type for $x$.
\begin{mathpar}
\Infer[App]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
\forall i\in I.\ u_i\leq \arrow{\neg s_i}{t_i} \text{ with } t_i\land t = \varnothing \\
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i}
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
}
{
\Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
......@@ -486,16 +488,16 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
{ }
\\
\Infer[AppL*]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{u_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[AppLDom]
{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_2
{\Gamma(x_1) = u\\u\land (\arrow{\Empty}{\Any})\neq\Empty\\u\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_2
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_1,\tree_2\})}
{ }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment