Difference between revisions of "Induction proof"

From Event-B
Jump to navigationJump to search
imported>Christophe
imported>Mathieu
m (ortho)
 
(2 intermediate revisions by the same user 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 14: Line 15:
 
----
 
----
  
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 \Rightarrow n+1 \in s)\Rightarrow  \mathbb{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
Line 21: Line 23:
 
----
 
----
  
The proof of the previous theorem is given by instanciate the key theorem with : <math>   \{x|x\in \mathbb{N} \land P(x)\}</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)\}