1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports "../Base" "../Parsing" Simple_Inductive_Package |
2 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
5 section {* Parsing the Specification *} |
5 section {* Parsing and Typing the Specification *} |
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 new |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
10 command we chose \simpleinductive{}. We want that the package can cope with |
10 new command we chose \simpleinductive{}. In the package we want to support |
|
11 some ``advanced'' features: First, we want that the package can cope with |
11 specifications inside locales. For example it should be possible to declare |
12 specifications inside locales. For example it should be possible to declare |
12 |
|
13 *} |
13 *} |
14 |
14 |
15 locale rel = |
15 locale rel = |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 |
17 |
18 text {* |
18 text {* |
19 and then define the transitive closure and the accessible part as follows: |
19 and then define the transitive closure and the accessible part as follows: |
20 *} |
20 *} |
21 |
21 |
22 |
22 |
23 simple_inductive (in rel) trcl' |
23 simple_inductive (in rel) |
|
24 trcl' |
24 where |
25 where |
25 base: "trcl' x x" |
26 base: "trcl' x x" |
26 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z" |
27 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z" |
27 |
28 |
28 simple_inductive (in rel) accpart' |
29 simple_inductive (in rel) |
|
30 accpart' |
29 where |
31 where |
30 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
32 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
31 |
33 |
32 |
34 text {* |
33 |
35 Second, we want that the user can specify fixed parameters. |
34 text {* |
36 Remember in the previous section we stated that the user can give the |
35 After the keyword we expect a constant (or constants) with possible typing |
37 specification for the transitive closure of a relation @{text R} as |
36 annotations and a |
38 *} |
37 list of introduction rules. While these specifications are all |
39 |
38 straightforward, there is a technicality we like to deal with to do with |
40 simple_inductive |
39 fixed parameters and locales. Remember we pointed out that the parameter |
41 trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
40 @{text R} is fixed throughout the specifications of @{text trcl} and @{text |
42 where |
41 accpart}. The point is that they might be fixed in a locale and we like to |
43 base: "trcl\<iota>\<iota> R x x" |
42 support this. Accordingly we treat some parameters of the inductive |
44 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z" |
43 definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive |
45 |
44 closure and accessible part are defined with a fixed parameter @{text R} and |
46 text {* |
45 also inside a locale fixing @{text R}. |
47 Note that there is no locale given in this specification---the parameter |
46 *} |
48 @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but |
47 |
49 stays fixed throughout the specification. The problem with this way of |
48 text_raw {* |
50 stating the specification for the transitive closure is that it derives the |
49 \begin{figure}[p] |
51 following induction principle. |
50 \begin{isabelle} |
52 |
51 *} |
53 \begin{center}\small |
|
54 \mprset{flushleft} |
|
55 \mbox{\inferrule{ |
|
56 @{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
|
57 @{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
|
58 @{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}} |
|
59 {@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} |
|
60 \end{center} |
|
61 |
|
62 But this does not correspond to the induction principle we derived by hand, which |
|
63 was |
|
64 |
|
65 \begin{center}\small |
|
66 \mprset{flushleft} |
|
67 \mbox{\inferrule{ |
|
68 @{thm_style prem1 trcl_induct[no_vars]}\\\\ |
|
69 @{thm_style prem2 trcl_induct[no_vars]}\\\\ |
|
70 @{thm_style prem3 trcl_induct[no_vars]}} |
|
71 {@{thm_style concl trcl_induct[no_vars]}}} |
|
72 \end{center} |
|
73 |
|
74 The difference is that in the one derived by hand the relation @{term R} is not |
|
75 a parameter of the proposition @{term P} to be proved and it is also not universally |
|
76 qunatified in the second and third premise. The point is that the parameter @{term R} |
|
77 stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' |
|
78 argument of the transitive closure, but one that can be freely instantiated. |
|
79 In order to recognise such parameters, we have to extend the specification |
|
80 to include a mechanism to state fixed parameters. The user should be able |
|
81 to write |
|
82 |
|
83 *} |
|
84 |
52 simple_inductive |
85 simple_inductive |
53 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
86 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
54 where |
87 where |
55 base: "trcl'' R x x" |
88 base: "trcl'' R x x" |
56 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z" |
89 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z" |
58 simple_inductive |
91 simple_inductive |
59 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
92 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
60 where |
93 where |
61 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
94 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
62 |
95 |
63 text_raw {* |
96 text {* |
64 \end{isabelle} |
97 \begin{figure}[t] |
65 \caption{The first definition is for the transitive closure where the |
|
66 relation @{text R} is explicitly fixed. Simiraly the second definition |
|
67 of the accessible part of the relation @{text R}. The last two definitions |
|
68 specify the same inductive predicates, but this time defined inside |
|
69 a locale.\label{fig:inddefsfixed}} |
|
70 \end{figure} |
|
71 *} |
|
72 |
|
73 text {* |
|
74 \begin{figure}[p] |
|
75 \begin{isabelle} |
98 \begin{isabelle} |
76 \railnontermfont{\rmfamily\itshape} |
99 \railnontermfont{\rmfamily\itshape} |
77 \railterm{simpleinductive,where,for} |
100 \railterm{simpleinductive,where,for} |
78 \railalias{simpleinductive}{\simpleinductive{}} |
101 \railalias{simpleinductive}{\simpleinductive{}} |
79 \railalias{where}{\isacommand{where}} |
102 \railalias{where}{\isacommand{where}} |