1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports "../Base" "../Parsing" Simple_Inductive_Package |
2 imports "../Base" "../Parsing" Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
5 section {* The Interface \label{sec:ind-interface} *} |
5 section {* Parsing the Specification *} |
6 |
|
7 text {* |
|
8 The purpose of the package we show next is that the user just specifies the |
|
9 inductive predicate by stating some introduction rules and then the packages |
|
10 makes the equivalent definition and derives from it the needed properties. |
|
11 *} |
|
12 |
|
13 text {* |
|
14 From a high-level perspective the package consists of 6 subtasks: |
|
15 |
|
16 \begin{itemize} |
|
17 \item reading the various parts of specification (i.e.~parser), |
|
18 \item transforming the parser outut into an internal |
|
19 (typed) datastructure, |
|
20 \item making the definitions, |
|
21 \item deriving the induction principles, |
|
22 \item deriving the introduction rules, and |
|
23 \item storing the results in the given theory. |
|
24 to the user. |
|
25 \end{itemize} |
|
26 |
|
27 *} |
|
28 |
6 |
29 text {* |
7 text {* |
30 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 |
31 a new command (see Section~\ref{sec:newcommand}). As the keyword for the new |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the new |
32 command we chose \simpleinductive{}. The specifications corresponding to our |
10 command we chose \simpleinductive{}. We want that the package can cope with |
33 examples described earlier are: |
11 specifications inside locales. For example it should be possible to declare |
34 *} |
12 |
35 |
13 *} |
36 simple_inductive |
14 |
37 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
15 locale rel = |
|
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
17 |
|
18 text {* |
|
19 and then define the transitive closure and the accessible part as follows: |
|
20 *} |
|
21 |
|
22 |
|
23 simple_inductive (in rel) trcl' |
38 where |
24 where |
39 base: "trcl R x x" |
25 base: "trcl' x x" |
40 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z" |
26 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z" |
41 |
27 |
42 simple_inductive |
28 simple_inductive (in rel) accpart' |
43 even and odd |
|
44 where |
29 where |
45 even0: "even 0" |
30 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
46 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
31 |
47 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
32 |
48 |
|
49 simple_inductive |
|
50 accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
51 where |
|
52 accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
|
53 |
33 |
54 text {* |
34 text {* |
55 After the keyword we expect a constant (or constants) with possible typing |
35 After the keyword we expect a constant (or constants) with possible typing |
56 annotations and a |
36 annotations and a |
57 list of introduction rules. While these specifications are all |
37 list of introduction rules. While these specifications are all |
68 text_raw {* |
48 text_raw {* |
69 \begin{figure}[p] |
49 \begin{figure}[p] |
70 \begin{isabelle} |
50 \begin{isabelle} |
71 *} |
51 *} |
72 simple_inductive |
52 simple_inductive |
73 trcl' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
53 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
74 where |
54 where |
75 base: "trcl' R x x" |
55 base: "trcl'' R x x" |
76 | step: "trcl' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl' R x z" |
56 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z" |
77 |
57 |
78 simple_inductive |
58 simple_inductive |
79 accpart' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
59 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
80 where |
60 where |
81 accpartI: "(\<forall>y. R y x \<longrightarrow> accpart' R y) \<Longrightarrow> accpart' R x" |
61 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
82 |
62 |
83 locale rel = |
|
84 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
85 |
|
86 simple_inductive (in rel) trcl'' |
|
87 where |
|
88 base: "trcl'' x x" |
|
89 | step: "trcl'' x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' x z" |
|
90 |
|
91 simple_inductive (in rel) accpart'' |
|
92 where |
|
93 accpartI: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x" |
|
94 text_raw {* |
63 text_raw {* |
95 \end{isabelle} |
64 \end{isabelle} |
96 \caption{The first definition is for the transitive closure where the |
65 \caption{The first definition is for the transitive closure where the |
97 relation @{text R} is explicitly fixed. Simiraly the second definition |
66 relation @{text R} is explicitly fixed. Simiraly the second definition |
98 of the accessible part of the relation @{text R}. The last two definitions |
67 of the accessible part of the relation @{text R}. The last two definitions |
433 to prove that a given set of equations is non-overlapping and covers all cases. The kind |
402 to prove that a given set of equations is non-overlapping and covers all cases. The kind |
434 of the command should be chosen with care, since selecting the wrong one can cause strange |
403 of the command should be chosen with care, since selecting the wrong one can cause strange |
435 behaviour of the user interface, such as failure of the undo mechanism. |
404 behaviour of the user interface, such as failure of the undo mechanism. |
436 *} |
405 *} |
437 |
406 |
|
407 text {* |
|
408 Note that the @{text trcl} predicate has two different kinds of parameters: the |
|
409 first parameter @{text R} stays \emph{fixed} throughout the definition, whereas |
|
410 the second and third parameter changes in the ``recursive call''. This will |
|
411 become important later on when we deal with fixed parameters and locales. |
|
412 |
|
413 |
|
414 |
|
415 The purpose of the package we show next is that the user just specifies the |
|
416 inductive predicate by stating some introduction rules and then the packages |
|
417 makes the equivalent definition and derives from it the needed properties. |
|
418 *} |
|
419 |
|
420 text {* |
|
421 From a high-level perspective the package consists of 6 subtasks: |
|
422 |
|
423 |
|
424 |
|
425 *} |
|
426 |
|
427 |
438 (*<*) |
428 (*<*) |
439 end |
429 end |
440 (*>*) |
430 (*>*) |