equal
deleted
inserted
replaced
1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package |
2 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
5 section {* Parsing and Typing the Specification *} |
5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 |
6 |
7 text {* |
7 text {* |
8 To be able to write down the specification in Isabelle, we have to introduce |
8 To be able to write down the specification in Isabelle, we have to introduce |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
10 new command we chose \simpleinductive{}. In the package we want to support |
10 new command we chose \simpleinductive{}. In the package we want to support |
446 |
446 |
447 The point of these examples is to get a feeling what the automatic proofs |
447 The point of these examples is to get a feeling what the automatic proofs |
448 should do in order to solve all inductive definitions we throw at them. For this |
448 should do in order to solve all inductive definitions we throw at them. For this |
449 it is instructive to look at the general construction principle |
449 it is instructive to look at the general construction principle |
450 of inductive definitions, which we shall do in the next section. |
450 of inductive definitions, which we shall do in the next section. |
|
451 |
|
452 The code of the inductive package falls roughly in tree parts: the first |
|
453 deals with the definitions, the second with the induction principles and |
|
454 the third with the introduction rules. |
|
455 |
451 *} |
456 *} |
452 |
457 |
453 |
458 |
454 (*<*) |
459 (*<*) |
455 end |
460 end |