92 obtain the theory behind the local theory (Line 3); with this we can |
92 obtain the theory behind the local theory (Line 3); with this we can |
93 call @{ML defs_aux} to generate the terms for the left-hand sides. |
93 call @{ML defs_aux} to generate the terms for the left-hand sides. |
94 The actual definitions are made in Line 7. |
94 The actual definitions are made in Line 7. |
95 *} |
95 *} |
96 |
96 |
97 subsection {* Introduction Rules *} |
97 |
|
98 subsection {* Induction Principles *} |
98 |
99 |
99 ML{*fun inst_spec ct = |
100 ML{*fun inst_spec ct = |
100 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
101 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
101 |
102 |
102 text {* |
103 text {* |
103 Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}. |
104 Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. |
104 *} |
105 *} |
105 |
106 |
106 text {* |
107 text {* |
107 Instantiates universal qantifications in the premises |
108 Instantiates universal qantifications in the premises |
108 *} |
109 *} |
109 |
110 |
110 lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True" |
111 lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True" |
111 apply (tactic {* EVERY' (map (dtac o inst_spec) |
112 apply (tactic {* EVERY' (map (dtac o inst_spec) |
112 [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) |
113 [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) |
|
114 txt {* \begin{minipage}{\textwidth} |
|
115 @{subgoals} |
|
116 \end{minipage}*} |
113 (*<*)oops(*>*) |
117 (*<*)oops(*>*) |
114 |
118 |
|
119 |
|
120 lemma |
|
121 assumes "even n" |
|
122 shows "P 0 \<Longrightarrow> |
|
123 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
|
124 apply(atomize (full)) |
|
125 apply(cut_tac prems) |
|
126 apply(unfold even_def) |
|
127 apply(drule spec[where x=P]) |
|
128 apply(drule spec[where x=Q]) |
|
129 apply(assumption) |
|
130 done |
|
131 |
115 text {* |
132 text {* |
116 The tactic for proving the induction rules: |
133 The tactic for proving the induction rules: |
117 *} |
134 *} |
118 |
135 |
119 ML{*fun induction_tac defs prems insts = |
136 ML{*fun induction_tac defs prems insts = |
120 EVERY1 [ObjectLogic.full_atomize_tac, |
137 EVERY1 [K (print_tac "start"), |
|
138 ObjectLogic.full_atomize_tac, |
121 cut_facts_tac prems, |
139 cut_facts_tac prems, |
122 K (rewrite_goals_tac defs), |
140 K (rewrite_goals_tac defs), |
123 EVERY' (map (dtac o inst_spec) insts), |
141 EVERY' (map (dtac o inst_spec) insts), |
124 assume_tac]*} |
142 assume_tac]*} |
125 |
143 |
126 lemma |
144 lemma |
127 assumes asm: "even n" |
145 assumes "even n" |
128 shows "P 0 \<Longrightarrow> |
146 shows "P 0 \<Longrightarrow> |
129 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
147 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
130 apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] |
148 apply(tactic {* |
131 [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *}) |
149 let |
|
150 val defs = [@{thm even_def}, @{thm odd_def}] |
|
151 val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] |
|
152 in |
|
153 induction_tac defs @{thms prems} insts |
|
154 end *}) |
132 done |
155 done |
133 |
156 |
134 ML %linenosgray{*fun inductions rules defs preds Tss lthy1 = |
157 text {* |
|
158 While the generic proof is relatively simple, it is a bit harder to |
|
159 set up the goals for the induction principles. |
|
160 *} |
|
161 |
|
162 |
|
163 ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = |
135 let |
164 let |
136 val Ps = replicate (length preds) "P" |
165 val Ps = replicate (length preds) "P" |
137 val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 |
166 val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 |
138 |
167 |
139 val thy = ProofContext.theory_of lthy2 |
168 val thy = ProofContext.theory_of lthy2 |
140 |
169 |
141 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
170 val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
142 val newpreds = map Free (newprednames ~~ Tss') |
171 val newpreds = map Free (newprednames ~~ tyss') |
143 val cnewpreds = map (cterm_of thy) newpreds |
172 val cnewpreds = map (cterm_of thy) newpreds |
144 val rules' = map (subst_free (preds ~~ newpreds)) rules |
173 val rules' = map (subst_free (preds ~~ newpreds)) rules |
145 |
174 |
146 fun prove_induction ((pred, newpred), Ts) = |
175 fun prove_induction ((pred, newpred), tys) = |
147 let |
176 let |
148 val zs = replicate (length Ts) "z" |
177 val zs = replicate (length tys) "z" |
149 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
178 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
150 val newargs = map Free (newargnames ~~ Ts) |
179 val newargs = map Free (newargnames ~~ tys) |
151 |
180 |
152 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
181 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
153 val goal = Logic.list_implies |
182 val goal = Logic.list_implies |
154 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
183 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
155 in |
184 in |
156 Goal.prove lthy3 [] [prem] goal |
185 Goal.prove lthy3 [] [prem] goal |
157 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
186 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
158 |> singleton (ProofContext.export lthy3 lthy1) |
187 |> singleton (ProofContext.export lthy3 lthy1) |
159 end |
188 end |
160 in |
189 in |
161 map prove_induction (preds ~~ newpreds ~~ Tss) |
190 map prove_induction (preds ~~ newpreds ~~ tyss) |
162 end*} |
191 end*} |
163 |
192 |
164 ML {* Goal.prove *} |
193 (* |
165 ML {* singleton *} |
194 ML {* |
166 ML {* ProofContext.export *} |
195 let |
167 |
196 val rules = [@{term "even 0"}, |
168 text {* |
197 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
169 |
198 @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
170 *} |
199 val defs = [@{thm even_def}, @{thm odd_def}] |
171 |
200 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
172 text {* |
201 val tyss = [[@{typ "nat"}],[@{typ "nat"}]] |
173 @{ML_chunk [display,gray] subproof1} |
202 in |
174 |
203 inductions rules defs preds tyss @{context} |
175 @{ML_chunk [display,gray] subproof2} |
204 end |
176 |
205 *} |
177 @{ML_chunk [display,gray] intro_rules} |
206 *) |
178 |
207 |
179 |
208 subsection {* Introduction Rules *} |
180 *} |
209 |
|
210 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
|
211 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
|
212 |
|
213 ML{*fun subproof2 prem params2 prems2 = |
|
214 SUBPROOF (fn {prems, ...} => |
|
215 let |
|
216 val prem' = prems MRS prem; |
|
217 val prem'' = |
|
218 case prop_of prem' of |
|
219 _ $ (Const (@{const_name All}, _) $ _) => |
|
220 prem' |> all_elims params2 |
|
221 |> imp_elims prems2 |
|
222 | _ => prem'; |
|
223 in |
|
224 rtac prem'' 1 |
|
225 end)*} |
|
226 |
|
227 ML{*fun subproof1 rules preds i = |
|
228 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
|
229 let |
|
230 val (prems1, prems2) = chop (length prems - length rules) prems; |
|
231 val (params1, params2) = chop (length params - length preds) params; |
|
232 in |
|
233 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
|
234 THEN |
|
235 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
|
236 end)*} |
|
237 |
|
238 ML{* |
|
239 fun introductions_tac defs rules preds i ctxt = |
|
240 EVERY1 [ObjectLogic.rulify_tac, |
|
241 K (rewrite_goals_tac defs), |
|
242 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
|
243 subproof1 rules preds i ctxt]*} |
|
244 |
|
245 ML{*fun introductions rules preds defs lthy = |
|
246 let |
|
247 fun prove_intro (i, goal) = |
|
248 Goal.prove lthy [] [] goal |
|
249 (fn {context, ...} => introductions_tac defs rules preds i context) |
|
250 in |
|
251 map_index prove_intro rules |
|
252 end*} |
|
253 |
|
254 ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = |
|
255 let |
|
256 val syns = map snd pred_specs |
|
257 val pred_specs' = map fst pred_specs |
|
258 val prednames = map fst pred_specs' |
|
259 val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' |
|
260 |
|
261 val tyss = map (binder_types o fastype_of) preds |
|
262 val (attrs, rules) = split_list rule_specs |
|
263 |
|
264 val (defs, lthy') = definitions rules preds prednames syns tyss lthy |
|
265 val ind_rules = inductions rules defs preds tyss lthy' |
|
266 val intro_rules = introductions rules preds defs lthy' |
|
267 |
|
268 val mut_name = space_implode "_" (map Binding.name_of prednames) |
|
269 val case_names = map (Binding.name_of o fst) attrs |
|
270 in |
|
271 lthy' |
|
272 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
|
273 ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) |
|
274 |-> (fn intross => LocalTheory.note Thm.theoremK |
|
275 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
|
276 |>> snd |
|
277 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
|
278 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
|
279 [Attrib.internal (K (RuleCases.case_names case_names)), |
|
280 Attrib.internal (K (RuleCases.consumes 1)), |
|
281 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
|
282 (pred_specs ~~ ind_rules)) #>> maps snd) |
|
283 |> snd |
|
284 end*} |
|
285 |
|
286 |
|
287 ML{*fun read_specification' vars specs lthy = |
|
288 let |
|
289 val specs' = map (fn (a, s) => [(a, [s])]) specs |
|
290 val ((varst, specst), _) = |
|
291 Specification.read_specification vars specs' lthy |
|
292 val specst' = map (apsnd the_single) specst |
|
293 in |
|
294 (varst, specst') |
|
295 end*} |
|
296 |
|
297 ML{*fun add_inductive pred_specs rule_specs lthy = |
|
298 let |
|
299 val (pred_specs', rule_specs') = |
|
300 read_specification' pred_specs rule_specs lthy |
|
301 in |
|
302 add_inductive_i pred_specs' rule_specs' lthy |
|
303 end*} |
|
304 |
|
305 ML{*val spec_parser = |
|
306 OuterParse.opt_target -- |
|
307 OuterParse.fixes -- |
|
308 Scan.optional |
|
309 (OuterParse.$$$ "where" |-- |
|
310 OuterParse.!!! |
|
311 (OuterParse.enum1 "|" |
|
312 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
|
313 |
|
314 ML{*val specification = |
|
315 spec_parser >> |
|
316 (fn ((loc, pred_specs), rule_specs) => |
|
317 Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*} |
|
318 |
|
319 ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
|
320 OuterKeyword.thy_decl specification*} |
181 |
321 |
182 text {* |
322 text {* |
183 Things to include at the end: |
323 Things to include at the end: |
184 |
324 |
185 \begin{itemize} |
325 \begin{itemize} |