39 section {* The Code in a Nutshell\label{sec:nutshell} *} |
39 section {* The Code in a Nutshell\label{sec:nutshell} *} |
40 |
40 |
41 |
41 |
42 text {* |
42 text {* |
43 The inductive package will generate the reasoning infrastructure for |
43 The inductive package will generate the reasoning infrastructure for |
44 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
44 mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
45 follows we will have the convention that various, possibly empty collections |
45 follows we will have the convention that various, possibly empty collections |
46 of ``things'' (lists, nested implications and so on) are indicated either by |
46 of ``things'' (lists, terms, nested implications and so on) are indicated either by |
47 adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] |
47 adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] |
48 "\<^isup>*"}. The shorthand for the predicates will therefore be @{text |
48 "\<^isup>*"}. The shorthand for the predicates will therefore be @{text |
49 "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must |
49 "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must |
50 be, of course, at least a single one in order to obtain a meaningful |
50 be, of course, at least a single one in order to obtain a meaningful |
51 definition. |
51 definition. |
62 \<Longrightarrow> pred ts"} |
62 \<Longrightarrow> pred ts"} |
63 \end{isabelle} |
63 \end{isabelle} |
64 |
64 |
65 For the purposes here, we will assume the @{text rules} have this format and |
65 For the purposes here, we will assume the @{text rules} have this format and |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
67 wrong, if the @{text "rules"} are not of this form.\footnote{FIXME: Exercise |
67 wrong, if the @{text "rules"} are not of this form. The @{text As} and |
68 to test this format.} The @{text As} and @{text Bs} in a @{text "rule"} |
68 @{text Bs} in a @{text "rule"} stand for formulae not involving the |
69 stand for formulae not involving the inductive predicates @{text "preds"}; |
69 inductive predicates @{text "preds"}; the instances @{text "pred ss"} and |
70 the instances @{text "pred ss"} and @{text "pred ts"} can stand for |
70 @{text "pred ts"} can stand for different predicates, like @{text |
71 different predicates, like @{text "pred\<^isub>1 ss"} and @{text |
71 "pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}, in case mutual recursive |
72 "pred\<^isub>2 ts"}, in case mutual recursive predicates are defined; the |
72 predicates are defined; the terms @{text ss} and @{text ts} are the |
73 terms @{text ss} and @{text ts} are the arguments of these predicates. Every |
73 arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred |
74 formula left of @{text [quotes] "\<Longrightarrow> pred ts"} is a premise of the rule. The |
74 ts"} is a premise of the rule. The outermost quantified variables @{text |
75 outermost quantified variables @{text "xs"} are usually omitted in the |
75 "xs"} are usually omitted in the user's input. The quantification for the |
76 user's input. The quantification for the variables @{text "ys"} is local |
76 variables @{text "ys"} is local with respect to one recursive premise and |
77 with respect to one recursive premise and must be given. Some examples of |
77 must be given. Some examples of @{text "rule"}s are |
78 @{text "rule"}s are |
|
79 |
78 |
80 |
79 |
81 @{thm [display] fresh_var[no_vars]} |
80 @{thm [display] fresh_var[no_vars]} |
82 |
81 |
83 which has only a single non-recursive premise, whereas |
82 which has only a single non-recursive premise, whereas |
86 |
85 |
87 has a single recursive premise; the rule |
86 has a single recursive premise; the rule |
88 |
87 |
89 @{thm [display] accpartI[no_vars]} |
88 @{thm [display] accpartI[no_vars]} |
90 |
89 |
91 has a single recursive premise that has a precondition. As usual all |
90 has a single recursive premise that has a precondition. As is custom all |
92 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
91 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
93 |
92 |
94 The output of the inductive package will be definitions for the predicates, |
93 The output of the inductive package will be definitions for the predicates, |
95 induction principles and introduction rules. For the definitions we need to have the |
94 induction principles and introduction rules. For the definitions we need to have the |
96 @{text rules} in a form where the meta-quantifiers and meta-implications are |
95 @{text rules} in a form where the meta-quantifiers and meta-implications are |
106 The induction principles for every predicate @{text "pred"} are of the |
105 The induction principles for every predicate @{text "pred"} are of the |
107 form |
106 form |
108 |
107 |
109 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"} |
108 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"} |
110 |
109 |
111 where in the @{text "rules"} every @{text pred} is replaced by a fresh |
110 where in the @{text "rules"}-part every @{text pred} is replaced by a fresh |
112 meta-variable @{text "?P"}. |
111 meta-variable @{text "?P"}. |
113 |
112 |
114 In order to derive an induction principle for the predicate @{text "pred"}, |
113 In order to derive an induction principle for the predicate @{text "pred"}, |
115 we first transform @{text ind} into the object logic and fix the meta-variables. |
114 we first transform @{text ind} into the object logic and fix the meta-variables. |
116 Hence we have to prove a formula of the form |
115 Hence we have to prove a formula of the form |
209 val eo_orules = |
208 val eo_orules = |
210 [@{prop "even 0"}, |
209 [@{prop "even 0"}, |
211 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
210 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
212 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
211 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
213 |
212 |
214 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
213 val eo_preds = [@{term "even::nat \<Rightarrow> bool"}, @{term "odd::nat \<Rightarrow> bool"}] |
215 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
214 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
216 val eo_mxs = [NoSyn, NoSyn] |
215 val eo_mxs = [NoSyn, NoSyn] |
217 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
216 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
218 val e_pred = @{term "even::nat\<Rightarrow>bool"} |
217 val e_pred = @{term "even::nat \<Rightarrow> bool"} |
219 val e_arg_tys = [@{typ "nat"}] |
218 val e_arg_tys = [@{typ "nat"}] |
220 |
219 |
221 |
220 |
222 |
221 |
223 (* freshness example *) |
222 (* freshness example *) |
231 [@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}, |
230 [@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}, |
232 @{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}, |
231 @{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}, |
233 @{prop "\<forall>a t. fresh a (Lam a t)"}, |
232 @{prop "\<forall>a t. fresh a (Lam a t)"}, |
234 @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}] |
233 @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}] |
235 |
234 |
236 val fresh_pred = @{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"} |
235 val fresh_pred = @{term "fresh::string \<Rightarrow> trm \<Rightarrow> bool"} |
237 val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}] |
236 val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}] |
238 |
237 |
239 |
238 |
240 |
239 |
241 (* accessible-part example *) |
240 (* accessible-part example *) |
242 val acc_rules = |
241 val acc_rules = |
243 [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}] |
242 [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}] |
244 val acc_pred = @{term "accpart::('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*} |
243 val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}*} |
245 text_raw{* |
244 text_raw{* |
246 \end{isabelle} |
245 \end{isabelle} |
247 \end{minipage} |
246 \end{minipage} |
248 \caption{Shorthands for the inductive predicates @{text "even"}-@{text "odd"}, |
247 \caption{Shorthands for the inductive predicates @{text "even"}/@{text "odd"}, |
249 @{text "fresh"} and @{text "accpart"}. The names of these shorthands follow |
248 @{text "fresh"} and @{text "accpart"}. The names of these shorthands follow |
250 the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on. |
249 the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on. |
251 The purpose of these shorthands is to simplify the construction of testcases |
250 The purpose of these shorthands is to simplify the construction of testcases |
252 in Section~\ref{sec:code}.\label{fig:shorthands}} |
251 in Section~\ref{sec:code}.\label{fig:shorthands}} |
253 \end{figure} |
252 \end{figure} |