22 text {* |
22 text {* |
23 Returns the definition and the local theory in which this definition has |
23 Returns the definition and the local theory in which this definition has |
24 been made. What is @{ML Thm.internalK}? |
24 been made. What is @{ML Thm.internalK}? |
25 *} |
25 *} |
26 |
26 |
27 ML {*let |
27 ML{*let |
28 val lthy = TheoryTarget.init NONE @{theory} |
28 val lthy = TheoryTarget.init NONE @{theory} |
29 in |
29 in |
30 make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy |
30 make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy |
31 end*} |
31 end*} |
32 |
32 |
68 the intro rules are attached as preconditions (Line 12); in Line 13 we |
68 the intro rules are attached as preconditions (Line 12); in Line 13 we |
69 quantify over all predicates; and in line 14 we just abstract over all |
69 quantify over all predicates; and in line 14 we just abstract over all |
70 the (fresh) arguments of the predicate. |
70 the (fresh) arguments of the predicate. |
71 *} |
71 *} |
72 |
72 |
|
73 ML{*let |
|
74 val orules = [@{term "even 0"}, |
|
75 @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"}, |
|
76 @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] |
|
77 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
|
78 in |
|
79 warning |
|
80 (Syntax.string_of_term @{context} |
|
81 (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}]))) |
|
82 end*} |
|
83 |
|
84 |
73 text {* |
85 text {* |
74 The arguments of the main function for the definitions are |
86 The arguments of the main function for the definitions are |
75 the intro rules; the predicates and their names, their syntax |
87 the intro rules; the predicates and their names, their syntax |
76 annotations and the argument types of each predicate. It |
88 annotations and the argument types of each predicate. It |
77 returns a theorem list (the definitions) and a local |
89 returns a theorem list (the definitions) and a local |
91 In line 4 we generate the intro rules in the object logic; for this we have to |
103 In line 4 we generate the intro rules in the object logic; for this we have to |
92 obtain the theory behind the local theory (Line 3); with this we can |
104 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. |
105 call @{ML defs_aux} to generate the terms for the left-hand sides. |
94 The actual definitions are made in Line 7. |
106 The actual definitions are made in Line 7. |
95 *} |
107 *} |
96 |
|
97 |
108 |
98 subsection {* Induction Principles *} |
109 subsection {* Induction Principles *} |
99 |
110 |
100 ML{*fun inst_spec ct = |
111 ML{*fun inst_spec ct = |
101 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
112 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
170 val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
181 val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
171 val newpreds = map Free (newprednames ~~ tyss') |
182 val newpreds = map Free (newprednames ~~ tyss') |
172 val cnewpreds = map (cterm_of thy) newpreds |
183 val cnewpreds = map (cterm_of thy) newpreds |
173 val rules' = map (subst_free (preds ~~ newpreds)) rules |
184 val rules' = map (subst_free (preds ~~ newpreds)) rules |
174 |
185 |
|
186 |
175 fun prove_induction ((pred, newpred), tys) = |
187 fun prove_induction ((pred, newpred), tys) = |
176 let |
188 let |
177 val zs = replicate (length tys) "z" |
189 val zs = replicate (length tys) "z" |
178 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
190 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
179 val newargs = map Free (newargnames ~~ tys) |
191 val newargs = map Free (newargnames ~~ tys) |
182 val goal = Logic.list_implies |
194 val goal = Logic.list_implies |
183 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
195 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
184 in |
196 in |
185 Goal.prove lthy3 [] [prem] goal |
197 Goal.prove lthy3 [] [prem] goal |
186 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
198 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
187 |> singleton (ProofContext.export lthy3 lthy1) |
199 |> singleton (ProofContext.export lthy3 lthy1) |
188 end |
200 end |
189 in |
201 in |
190 map prove_induction (preds ~~ newpreds ~~ tyss) |
202 map prove_induction (preds ~~ newpreds ~~ tyss) |
191 end*} |
203 end*} |
192 |
204 |
193 (* |
|
194 ML {* |
205 ML {* |
195 let |
206 let |
196 val rules = [@{term "even 0"}, |
207 val rules = [@{prop "even (0::nat)"}, |
197 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
208 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
198 @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
209 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
199 val defs = [@{thm even_def}, @{thm odd_def}] |
210 val defs = [@{thm even_def}, @{thm odd_def}] |
200 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
211 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
201 val tyss = [[@{typ "nat"}],[@{typ "nat"}]] |
212 val tyss = [[@{typ "nat"}],[@{typ "nat"}]] |
202 in |
213 in |
203 inductions rules defs preds tyss @{context} |
214 inductions rules defs preds tyss @{context} |
204 end |
215 end |
205 *} |
216 *} |
206 *) |
|
207 |
217 |
208 subsection {* Introduction Rules *} |
218 subsection {* Introduction Rules *} |
209 |
219 |
210 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
220 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})*} |
221 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
240 EVERY1 [ObjectLogic.rulify_tac, |
250 EVERY1 [ObjectLogic.rulify_tac, |
241 K (rewrite_goals_tac defs), |
251 K (rewrite_goals_tac defs), |
242 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
252 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
243 subproof1 rules preds i ctxt]*} |
253 subproof1 rules preds i ctxt]*} |
244 |
254 |
|
255 lemma evenS: |
|
256 shows "odd m \<Longrightarrow> even (Suc m)" |
|
257 apply(tactic {* |
|
258 let |
|
259 val rules = [@{prop "even (0::nat)"}, |
|
260 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
|
261 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
|
262 val defs = [@{thm even_def}, @{thm odd_def}] |
|
263 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
|
264 in |
|
265 introductions_tac defs rules preds 1 @{context} |
|
266 end *}) |
|
267 done |
|
268 |
|
269 |
245 ML{*fun introductions rules preds defs lthy = |
270 ML{*fun introductions rules preds defs lthy = |
246 let |
271 let |
247 fun prove_intro (i, goal) = |
272 fun prove_intro (i, goal) = |
248 Goal.prove lthy [] [] goal |
273 Goal.prove lthy [] [] goal |
249 (fn {context, ...} => introductions_tac defs rules preds i context) |
274 (fn {context, ...} => introductions_tac defs rules preds i context) |