3 begin |
3 begin |
4 |
4 |
5 section{* Preliminaries *} |
5 section{* Preliminaries *} |
6 |
6 |
7 text {* |
7 text {* |
8 On the Isabelle level, the user will just give a specification of an |
8 The user will just give a specification of an inductive predicate and |
9 inductive predicate and expects from the package to produce a convenient |
9 expects from the package to produce a convenient reasoning |
10 reasoning infrastructure. This infrastructure needs to be derived from the |
10 infrastructure. This infrastructure needs to be derived from the definition |
11 definition that correspond to the specified predicate. This will roughly |
11 that correspond to the specified predicate. This will roughly mean that the |
12 mean that the package has three main parts, namely: |
12 package has three main parts, namely: |
13 |
13 |
14 |
14 |
15 \begin{itemize} |
15 \begin{itemize} |
16 \item parsing the specification and typing the parsed input, |
16 \item parsing the specification and typing the parsed input, |
17 \item making the definitions and deriving the reasoning infrastructure, and |
17 \item making the definitions and deriving the reasoning infrastructure, and |
18 \item storing the results in the theory. |
18 \item storing the results in the theory. |
19 \end{itemize} |
19 \end{itemize} |
20 |
20 |
21 Before we start with explaining all parts, |
21 Before we start with explaining all parts, let us first give three examples |
22 let us first give three examples showing how to define inductive predicates |
22 showing how to define inductive predicates by hand and then also how to |
23 by hand and then also how to prove by hand important properties about |
23 prove by hand important properties about them. From these examples, we will |
24 them. From these examples, we will figure out a general method for defining |
24 figure out a general method for defining inductive predicates. The aim in |
25 inductive predicates. The aim in this section is \emph{not} to write proofs |
25 this section is \emph{not} to write proofs that are as beautiful as |
26 that are as beautiful as possible, but as close as possible to the ML-code |
26 possible, but as close as possible to the ML-code we will develop in later |
27 we will develop in later sections. |
27 sections. |
|
28 |
28 |
29 |
29 We first consider the transitive closure of a relation @{text R}. It is |
30 We first consider the transitive closure of a relation @{text R}. It is |
30 an inductive predicate characterised by the two introduction rules: |
31 an inductive predicate characterised by the two introduction rules: |
31 |
32 |
32 \begin{center}\small |
33 \begin{center}\small |
33 @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} |
34 @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} |
34 @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
35 @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
35 \end{center} |
36 \end{center} |
36 |
37 |
37 In Isabelle the user will state for @{term trcl\<iota>} the specification: |
38 In Isabelle, the user will state for @{term trcl\<iota>} the specification: |
38 *} |
39 *} |
39 |
40 |
40 simple_inductive |
41 simple_inductive |
41 trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
42 trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
42 where |
43 where |
63 HOL). However, the introduction rules and induction principles |
64 HOL). However, the introduction rules and induction principles |
64 should use the meta-connectives since they simplify the |
65 should use the meta-connectives since they simplify the |
65 reasoning for the user. |
66 reasoning for the user. |
66 |
67 |
67 With this definition, the proof of the induction principle for @{term trcl} |
68 With this definition, the proof of the induction principle for @{term trcl} |
68 closure is almost immediate. It suffices to convert all the meta-level |
69 is almost immediate. It suffices to convert all the meta-level |
69 connectives in the lemma to object-level connectives using the |
70 connectives in the lemma to object-level connectives using the |
70 proof method @{text atomize} (Line 4), expand the definition of @{term trcl} |
71 proof method @{text atomize} (Line 4), expand the definition of @{term trcl} |
71 (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7), |
72 (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7), |
72 and then solve the goal by assumption (Line 8). |
73 and then solve the goal by assumption (Line 8). |
73 |
74 |
337 qed |
338 qed |
338 |
339 |
339 text {* |
340 text {* |
340 In Line 11, applying the assumption @{text "r1"} generates a goal state with |
341 In Line 11, applying the assumption @{text "r1"} generates a goal state with |
341 the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the |
342 the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the |
342 proof above (Line 14). This local assumption will be used to solve |
343 proof above (Line 14). This local assumption is used to solve |
343 the goal @{term "P y"} using the assumption @{text "p1"}. |
344 the goal @{term "P y"} with the help of assumption @{text "p1"}. |
344 |
345 |
345 The point of these examples is to get a feeling what the automatic proofs |
346 The point of these examples is to get a feeling what the automatic proofs |
346 should do in order to solve all inductive definitions we throw at them. |
347 should do in order to solve all inductive definitions we throw at them. |
347 This is usually the first step in writing a package. |
348 This is usually the first step in writing a package. We next explain |
348 |
349 the parsing and typing part of the package. |
349 *} |
350 |
350 |
351 *} |
351 end |
352 (*<*)end(*>*) |