Difference between revisions of "Datatype Rules"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m
imported>Nicolas
Line 75: Line 75:
 
Starting from goal
 
Starting from goal
  
<math>\forall l,v,r,t. t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>
+
<math>\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>
  
 
we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:
 
we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:
  
 
  <math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty})  \qquad  t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>
 
  <math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty})  \qquad  t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>
 +
 +
the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.
  
 
== Induction ==
 
== Induction ==
  
 
{{TODO}}
 
{{TODO}}

Revision as of 17:43, 6 September 2010

Datatype rules may seem a bit difficult to understand at first sight. Here are a few examples intended to make them clearer.

Datatypes used

The rules will be applied to the following datatypes:

Directions:

direction ::=
    north
  | east
  | south
  | west

Let us have a function

\operatorname{move} \in \Z \cprod \Z \cprod \operatorname{direction} \tfun \Z \cprod \Z 

first two arguments are a start position, third is a direction, result is the end position.


Lists:

list(T) ::=
    nil
  | cons( head : T, tail : list(T) )

Let us have a predicate

\operatorname{member}(T, list(T))

meaning that the first argument is a member of the list.


Trees:

tree(T) ::=
  empty
| node( left : tree(T), value : T, right : tree(T) )


Let us have a function

\operatorname{height} \in \operatorname{Tree} \tfun \N defining the height of a tree

Distinct Case

The rule states

\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }


Application to directions

Starting from goal

\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y

we can free variables x,y,d then apply Distinct Case on d:

The resulting proof step is

\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y  \qquad  d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad  d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad  d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{  \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }

further simplifications depend on the existence of rules about move and the various directions.

Application to lists

Starting from goal

\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)

we can free variable l then apply Distinct Case on it:

\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{nil}) \land (\forall y \qdot \operatorname{member}(y,\operatorname{nil}) \limp y \leq x)  \qquad  l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{cons}(head0, tail1)) \land (\forall y \qdot \operatorname{member}(y,\operatorname{cons}(head0, tail1)) \limp y \leq x) }{  \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }

The left antecedent shows that the case of the nil list has been forgotten when writing the theorem.

Application to trees

Starting from goal

\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)

we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty})  \qquad  t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }

the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.

Induction

TODO