Billaude's work to finish

From Event-B
Jump to navigationJump to search

This page is here to describe the work that I started, but which is yet to be finished.

MembershipGoal

Here the rules that could be useful for the reasoner MembershipGoal.

Inference rules for the reasoner MembershipGoal
Inference Rule Side condition Implemented in the new version Implemented in the first version
 x\in A,\;\; A\subseteq B\vdash x\in B \checkmark
 A\subset B\vdash A\subseteq B \checkmark \checkmark
 A=B\vdash A\subseteq B \checkmark \checkmark
 A=B\vdash B\subseteq A \checkmark \checkmark
 A\subseteq B\vdash \dom(A)\subseteq\dom(B) \checkmark \checkmark
 A\subseteq B\vdash \ran(A)\subseteq\ran(B) \checkmark \checkmark
 x\in\dom(A\cprod B)\vdash x\in A \checkmark \checkmark
 y\in\ran(A\cprod B)\vdash y\in B \checkmark \checkmark
 x\mapsto y\in f\vdash x\in\dom(f) \checkmark \checkmark
 x\mapsto y\in f\vdash y\in\ran(f) \checkmark \checkmark
 \left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A \checkmark \checkmark
 f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A \checkmark \checkmark
 f\in A\;op\;B\vdash f\subseteq A\cprod B where \mathit{op} is one of \rel, \trel, \srel, \strel, \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij \checkmark \checkmark
e\subseteq f,\;\; f\setminus g\subseteq h\quad\vdash\quad e\setminus g\subseteq h \checkmark
g\subseteq k,\;\; f\setminus g\subseteq h \quad\vdash\quad f\setminus k\subseteq h \checkmark
e\subseteq f\setminus g,\;\; f\subseteq h\quad\vdash\quad e\subseteq h\setminus g \checkmark
e\subseteq f\setminus g,\;\; k\subseteq g \quad\vdash\quad e\subseteq f\setminus k \checkmark
e\subseteq f,\;\; f\ranres B\subseteq g \quad\vdash\quad e\ranres B\subseteq g \checkmark
A\subseteq B ,\;\; f\ranres B\subseteq g \quad\vdash\quad f\ranres A\subseteq g \checkmark
f\subseteq g\ranres A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ranres A \checkmark
f\subseteq g\ranres A ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ranres B \checkmark
A\subseteq B ,\;\; B\domres f\subseteq g \quad\vdash\quad A\domres f\subseteq g \checkmark
e\subseteq f ,\;\; B\domres f\subseteq g \quad\vdash\quad B\domres e\subseteq g \checkmark
f\subseteq A\domres g ,\;\; A\subseteq B \quad\vdash\quad f\subseteq B\domres g \checkmark
f\subseteq A\domres g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domres h \checkmark
e\subseteq f ,\;\; f\ransub A\subseteq g \quad\vdash\quad e\ransub A\subseteq g \checkmark
f\ransub A\subseteq g ,\;\; A\subseteq B \quad\vdash\quad f\ransub B\subseteq g \checkmark
f\subseteq g\ransub A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ransub A \checkmark
f\subseteq g\ransub B ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ransub A \checkmark
A\domsub f\subseteq g ,\;\; A\subseteq B \quad\vdash\quad B\domsub f\subseteq g \checkmark
e\subseteq f ,\;\; A\domsub f\subseteq g \quad\vdash\quad A\domsub e\subseteq g \checkmark
A\subseteq B ,\;\; f\subseteq B\domsub g \quad\vdash\quad f\subseteq A\domsub g \checkmark
f\subseteq A\domsub g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domsub h \checkmark
e\subseteq f ,\;\; f\ovl g\ovl\cdots\ovl h\subseteq k \quad\vdash\quad e\ovl g\ovl\cdots\ovl h\subseteq k \checkmark
f\subseteq g\ovl h\ovl\cdots\ovl k ,\;\; e\subseteq g \quad\vdash\quad f\subseteq e\ovl h\ovl\cdots\ovl k \checkmark
Z\subseteq B,\;\; A\bunion\cdots\bunion B\bunion\cdots\bunion C\subseteq D\quad\vdash\quad A\bunion\cdots\bunion Z\bunion\cdots\bunion C\subseteq D \checkmark
B\subseteq Z ,\;\; D\subseteq A\bunion\cdots\bunion B\bunion\cdots\bunion C \quad\vdash\quad D\subseteq A\bunion\cdots\bunion Z\bunion\cdots\bunion C \checkmark
Z\subseteq B,\;\; A\binter\cdots\binter B\binter\cdots\binter C\subseteq D\quad\vdash\quad A\binter\cdots\binter Z\binter\cdots\binter C\subseteq D \checkmark
B\subseteq Z ,\;\; D\subseteq A\binter\cdots\binter B\binter\cdots\binter C \quad\vdash\quad D\subseteq A\binter\cdots\binter Z\binter\cdots\binter C \checkmark
A\subseteq B,\;\; B\cprod D\subseteq E \quad\vdash\quad A\cprod D\subseteq E \checkmark
C\subseteq D,\;\; B\cprod D\subseteq E \quad\vdash\quad B\cprod C\subseteq E \checkmark
A\subseteq B\cprod D,\;\; B\subseteq C \quad\vdash\quad A\subseteq C\cprod D \checkmark
A\subseteq B\cprod D,\;\; D\subseteq E\quad\vdash\quad A\subseteq B\cprod E \checkmark
\dom(f\domres\prjone)\defi f \checkmark
\dom(f\domres\prjtwo)\defi f \checkmark
\dom(f\domres\id)\defi f \checkmark
\ran(\prjone\ranres f)\defi f \checkmark
\ran(\prjtwo\ranres f)\defi f \checkmark
\ran(\id\ranres f)\defi f \checkmark
\ran(f\domres\prjone)\defi\dom(f) \checkmark
\ran(f\domres\prjtwo)\defi\ran(f) \checkmark
\ran(f\domres\id)\defi f \checkmark

This describe the rule that I implemented in the first version of MembershipGoal. Others should also be taken into account (they will be written later). Even if those rule have been checked, they may not be implemented in the reasoner since some can explode the time research.

Membership Goal Exhaustive rules

To be completed ...

Autorewriter

In the AutorewriterL3, some re-writing about \usucc and \upred are proceeded. But, more re-writing should be done. Unfortunately, I did not take too much time to analyze all the possibilities about this two functions \left(\finite(\usucc) = \bfalse,\;\cdots\right).

Nevertheless, one trail has been explored : instead of re-writing \usucc(x) = x+1, we may should better re-write : \left(\lambda x\qdot\btrue\mid x+1\right).

Moreover, since \upred\defi\usucc^{-1}, instead of re-writing \usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x+1\right)^{-1}\defi\left\{a\qdot\btrue\mid a-1\mapsto a\right\} (the last re-writing is proceeded by the auto-rewriter, and is not really easy to read), I think that we should re-write \usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x-1\right).

Others Feature Requests

The feature request #2887264 should also be treated.