1 theory Ind_Extensions |
1 theory Ind_Extensions |
2 imports Simple_Inductive_Package Ind_Intro |
2 imports Simple_Inductive_Package Ind_Intro |
3 begin |
3 begin |
4 |
4 |
5 section {* Extensions of the Package (TBD) *} |
5 section \<open>Extensions of the Package (TBD)\<close> |
6 |
6 |
7 (* |
7 (* |
8 text {* |
8 text {* |
9 In order to add a new inductive predicate to a theory with the help of our |
9 In order to add a new inductive predicate to a theory with the help of our |
10 package, the user must \emph{invoke} it. For every package, there are |
10 package, the user must \emph{invoke} it. For every package, there are |
27 terms. These two ways of invoking the package are reflected in its ML |
27 terms. These two ways of invoking the package are reflected in its ML |
28 programming interface, which consists of two functions: |
28 programming interface, which consists of two functions: |
29 *} |
29 *} |
30 *) |
30 *) |
31 |
31 |
32 text {* |
32 text \<open> |
33 Things to include at the end: |
33 Things to include at the end: |
34 |
34 |
35 \begin{itemize} |
35 \begin{itemize} |
36 \item include the code for the parameters |
36 \item include the code for the parameters |
37 \item say something about add-inductive to return |
37 \item say something about add-inductive to return |
38 the rules |
38 the rules |
39 \item say something about the two interfaces for calling packages |
39 \item say something about the two interfaces for calling packages |
40 \end{itemize} |
40 \end{itemize} |
41 |
41 |
42 *} |
42 \<close> |
43 |
43 |
44 (* |
44 (* |
45 simple_inductive |
45 simple_inductive |
46 Even and Odd |
46 Even and Odd |
47 where |
47 where |
127 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
127 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
128 where |
128 where |
129 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
129 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
130 *) |
130 *) |
131 |
131 |
132 text {* |
132 text \<open> |
133 \begin{exercise} |
133 \begin{exercise} |
134 In Section~\ref{sec:nutshell} we required that introduction rules must be of the |
134 In Section~\ref{sec:nutshell} we required that introduction rules must be of the |
135 form |
135 form |
136 |
136 |
137 \begin{isabelle} |
137 \begin{isabelle} |
138 @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"} |
138 \<open>rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts\<close> |
139 \end{isabelle} |
139 \end{isabelle} |
140 |
140 |
141 where the @{text "As"} and @{text "Bs"} can be any collection of formulae |
141 where the \<open>As\<close> and \<open>Bs\<close> can be any collection of formulae |
142 not containing the @{text "preds"}. This requirement is important, |
142 not containing the \<open>preds\<close>. This requirement is important, |
143 because if violated, the theory behind the inductive package does not work |
143 because if violated, the theory behind the inductive package does not work |
144 and also the proofs break. Write code that tests whether the introduction |
144 and also the proofs break. Write code that tests whether the introduction |
145 rules given by the user fit into the scheme described above. Hint: It |
145 rules given by the user fit into the scheme described above. Hint: It |
146 is not important in which order the premises ar given; the |
146 is not important in which order the premises ar given; the |
147 @{text "As"} and @{text "(\<And>ys. Bs \<Longrightarrow> pred ss)"} premises can occur |
147 \<open>As\<close> and \<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<close> premises can occur |
148 in any order. |
148 in any order. |
149 \end{exercise} |
149 \end{exercise} |
150 *} |
150 \<close> |
151 |
151 |
152 text_raw {* |
152 text_raw \<open> |
153 \begin{exercise} |
153 \begin{exercise} |
154 If you define @{text even} and @{text odd} with the standard inductive |
154 If you define \<open>even\<close> and \<open>odd\<close> with the standard inductive |
155 package |
155 package |
156 \begin{isabelle} |
156 \begin{isabelle} |
157 *} |
157 \<close> |
158 inductive |
158 inductive |
159 even_2 and odd_2 |
159 even_2 and odd_2 |
160 where |
160 where |
161 even0_2: "even_2 0" |
161 even0_2: "even_2 0" |
162 | evenS_2: "odd_2 m \<Longrightarrow> even_2 (Suc m)" |
162 | evenS_2: "odd_2 m \<Longrightarrow> even_2 (Suc m)" |
163 | oddS_2: "even_2 m \<Longrightarrow> odd_2 (Suc m)" |
163 | oddS_2: "even_2 m \<Longrightarrow> odd_2 (Suc m)" |
164 |
164 |
165 text_raw{* |
165 text_raw\<open> |
166 \end{isabelle} |
166 \end{isabelle} |
167 |
167 |
168 you will see that the generated induction principle for @{text "even'"} (namely |
168 you will see that the generated induction principle for \<open>even'\<close> (namely |
169 @{text "even_2_odd_2.inducts"} has the additional assumptions |
169 \<open>even_2_odd_2.inducts\<close> has the additional assumptions |
170 @{prop "odd_2 m"} and @{prop "even_2 m"} in the recursive cases. These additional |
170 @{prop "odd_2 m"} and @{prop "even_2 m"} in the recursive cases. These additional |
171 assumptions can sometimes make ``life easier'' in proofs. Since |
171 assumptions can sometimes make ``life easier'' in proofs. Since |
172 more assumptions can be made when proving properties, these induction principles |
172 more assumptions can be made when proving properties, these induction principles |
173 are called strong inductions principles. However, it is the case that the |
173 are called strong inductions principles. However, it is the case that the |
174 ``weak'' induction principles imply the ``strong'' ones. Hint: Prove a property |
174 ``weak'' induction principles imply the ``strong'' ones. Hint: Prove a property |
184 The standard inductive package is based on least fix-points. It allows more |
184 The standard inductive package is based on least fix-points. It allows more |
185 general introduction rules that can include any monotone operators and also |
185 general introduction rules that can include any monotone operators and also |
186 provides a richer reasoning infrastructure. The code of this package can be found in |
186 provides a richer reasoning infrastructure. The code of this package can be found in |
187 @{ML_file "HOL/Tools/inductive.ML"}. |
187 @{ML_file "HOL/Tools/inductive.ML"}. |
188 \end{readmore} |
188 \end{readmore} |
189 *} |
189 \<close> |
190 |
190 |
191 section {* Definitional Packages *} |
191 section \<open>Definitional Packages\<close> |
192 |
192 |
193 text {* Type declarations *} |
193 text \<open>Type declarations\<close> |
194 |
194 |
195 (* |
195 (* |
196 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn) |
196 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn) |
197 @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *} |
197 @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *} |
198 *) |
198 *) |
199 |
199 |
200 ML %grayML{*fun pat_completeness_auto ctxt = |
200 ML %grayML\<open>fun pat_completeness_auto ctxt = |
201 Pat_Completeness.pat_completeness_tac ctxt 1 |
201 Pat_Completeness.pat_completeness_tac ctxt 1 |
202 THEN auto_tac ctxt*} |
202 THEN auto_tac ctxt\<close> |
203 |
203 |
204 ML {* |
204 ML \<open> |
205 val conf = Function_Common.default_config |
205 val conf = Function_Common.default_config |
206 *} |
206 \<close> |
207 |
207 |
208 datatype foo = Foo nat |
208 datatype foo = Foo nat |
209 |
209 |
210 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
210 local_setup\<open>Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
211 [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])] |
211 [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])] |
212 conf pat_completeness_auto #> snd*} |
212 conf pat_completeness_auto #> snd\<close> |
213 |
213 |
214 (*<*)end(*>*) |
214 (*<*)end(*>*) |