Difference between revisions of "Induction proof"

From Event-B
Jump to navigationJump to search
imported>Christophe
imported>Mathieu
m (ortho)
 
(7 intermediate revisions by 2 users not shown)
Line 1: Line 1:
This page explains how to proove with induction method on the natural number with Rodin tools.
+
This page explains how to prove with [[wikipedia:Mathematical induction|induction]] method on the natural number with Rodin tools.
In other words, how to proove :<br/>
+
In other words, how to prove :
 +
 
 
<math>
 
<math>
 
P(0)
 
P(0)
Line 10: Line 11:
 
\vdash
 
\vdash
 
</math><br/>
 
</math><br/>
<math>\forall i. i \in \mathbb{N}  \Rightarrow P(i+1)</math>
+
<math>\forall i. i \in \mathbb{N}  \Rightarrow P(i)</math>
  
 
----
 
----
  
The proof key is the following theorem:<br/>
+
The proof key is the following theorem:
 +
 
 
<math>
 
<math>
\forall s.s \subseteq \mathbb{N} \land 0 \in s \land  (\forall n.n \in s => n+1 \in s)\Rightarrow  N \subseteq s
+
\forall s.s \subseteq \mathbb{N} \land 0 \in s \land  (\forall n.n \in s \Rightarrow n+1 \in s)\Rightarrow  \mathbb{N} \subseteq s
 +
</math>
 +
 
 +
----
 +
 
 +
The proof of the previous theorem is given by instantiating the key theorem with : <math>   \{x|x\in \mathbb{N} \land P(x)\}</math>
 +
 
 +
[[Category:Proof patterns]]

Latest revision as of 14:11, 30 October 2008

This page explains how to prove with induction method on the natural number with Rodin tools. In other words, how to prove :


P(0)

\forall i.i \in \mathbb{N}\land P(i) \Rightarrow P(i+1)

\vdash
\forall i. i \in \mathbb{N}  \Rightarrow P(i)


The proof key is the following theorem:


\forall s.s \subseteq \mathbb{N} \land 0 \in s \land  (\forall n.n \in s \Rightarrow n+1 \in s)\Rightarrow  \mathbb{N} \subseteq s


The proof of the previous theorem is given by instantiating the key theorem with : 	  \{x|x\in \mathbb{N} \land P(x)\}