12 *} |
12 *} |
13 |
13 |
14 ML{*fun make_defs ((binding, syn), trm) lthy = |
14 ML{*fun make_defs ((binding, syn), trm) lthy = |
15 let |
15 let |
16 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
16 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
17 val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy |
17 val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy |
18 in |
18 in |
19 (thm, lthy) |
19 (thm, lthy') |
20 end*} |
20 end*} |
21 |
21 |
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. The @{ML internalK in Thm} is just a flag attached to the |
25 *} |
25 theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). |
26 |
26 These flags just classify theorems and have no significant meaning, except |
27 ML{*let |
27 for tools such as finding theorems in the theorem database. |
28 val lthy = TheoryTarget.init NONE @{theory} |
28 *} |
29 in |
29 |
30 make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy |
30 local_setup {* |
31 end*} |
31 fn lthy => |
32 |
32 let |
33 text {* |
33 val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy |
34 Why is the output of MyTrue blue? |
34 val _ = warning (str_of_thm lthy' def) |
|
35 in |
|
36 lthy' |
|
37 end |
|
38 *} |
|
39 |
|
40 text {* |
|
41 Prints out the theorem @{prop "MyTrue \<equiv> True"}. |
35 *} |
42 *} |
36 |
43 |
37 text {* |
44 text {* |
38 Constructs the term for the definition: the main arguments are a predicate |
45 Constructs the term for the definition: the main arguments are a predicate |
39 and the types of the arguments, it also expects orules which are the |
46 and the types of the arguments, it also expects orules which are the |
40 intro rules in the object logic; preds which are all predicates. returns the |
47 intro rules in the object logic; preds which are all predicates. returns the |
41 term. |
48 term. |
42 *} |
49 *} |
43 |
50 |
44 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) = |
51 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = |
45 let |
52 let |
46 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
53 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
47 |
54 |
48 val fresh_args = |
55 val fresh_args = |
49 arg_types |
56 arg_tys |
50 |> map (pair "z") |
57 |> map (pair "z") |
51 |> Variable.variant_frees lthy orules |
58 |> Variable.variant_frees lthy orules |
52 |> map Free |
59 |> map Free |
53 in |
60 in |
54 list_comb (pred, fresh_args) |
61 list_comb (pred, fresh_args) |
68 the intro rules are attached as preconditions (Line 12); in Line 13 we |
75 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 |
76 quantify over all predicates; and in line 14 we just abstract over all |
70 the (fresh) arguments of the predicate. |
77 the (fresh) arguments of the predicate. |
71 *} |
78 *} |
72 |
79 |
73 ML{*let |
80 |
74 val orules = [@{term "even 0"}, |
81 local_setup {* |
75 @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"}, |
82 fn lthy => |
76 @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] |
83 let |
|
84 val orules = [@{prop "even 0"}, |
|
85 @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"}, |
|
86 @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] |
77 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
87 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
78 in |
88 val pred = @{term "even::nat\<Rightarrow>bool"} |
79 warning |
89 val arg_tys = [@{typ "nat"}] |
80 (Syntax.string_of_term @{context} |
90 val def = defs_aux lthy orules preds (pred, arg_tys) |
81 (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}]))) |
91 in |
82 end*} |
92 warning (Syntax.string_of_term lthy def); |
83 |
93 lthy |
|
94 end*} |
84 |
95 |
85 text {* |
96 text {* |
86 The arguments of the main function for the definitions are |
97 The arguments of the main function for the definitions are |
87 the intro rules; the predicates and their names, their syntax |
98 the intro rules; the predicates and their names, their syntax |
88 annotations and the argument types of each predicate. It |
99 annotations and the argument types of each predicate. It |
106 The actual definitions are made in Line 7. |
117 The actual definitions are made in Line 7. |
107 *} |
118 *} |
108 |
119 |
109 subsection {* Induction Principles *} |
120 subsection {* Induction Principles *} |
110 |
121 |
111 ML{*fun inst_spec ct = |
122 text {* Recall the proof for the induction principle for @{term "even"}: *} |
112 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
|
113 |
|
114 text {* |
|
115 Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. |
|
116 *} |
|
117 |
|
118 text {* |
|
119 Instantiates universal qantifications in the premises |
|
120 *} |
|
121 |
|
122 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" |
|
123 apply (tactic {* EVERY' (map (dtac o inst_spec) |
|
124 [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) |
|
125 txt {* \begin{minipage}{\textwidth} |
|
126 @{subgoals} |
|
127 \end{minipage}*} |
|
128 (*<*)oops(*>*) |
|
129 |
|
130 |
123 |
131 lemma |
124 lemma |
132 assumes "even n" |
125 assumes prems: "even n" |
133 shows "P 0 \<Longrightarrow> |
126 shows "P 0 \<Longrightarrow> |
134 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
127 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
135 apply(atomize (full)) |
128 apply(atomize (full)) |
136 apply(cut_tac prems) |
129 apply(cut_tac prems) |
137 apply(unfold even_def) |
130 apply(unfold even_def) |
138 apply(drule spec[where x=P]) |
131 apply(drule spec[where x=P]) |
139 apply(drule spec[where x=Q]) |
132 apply(drule spec[where x=Q]) |
140 apply(assumption) |
133 apply(assumption) |
141 done |
134 done |
142 |
135 |
143 text {* |
136 |
144 The tactic for proving the induction rules: |
137 text {* We need to be able to instantiate universal quantifiers. *} |
|
138 |
|
139 ML{*fun inst_spec ct = |
|
140 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
|
141 |
|
142 text {* |
|
143 Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. |
|
144 *} |
|
145 |
|
146 text {* |
|
147 Instantiates universal qantifications in the premises |
|
148 *} |
|
149 |
|
150 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" |
|
151 apply (tactic {* |
|
152 let |
|
153 val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}] |
|
154 in |
|
155 EVERY1 (map (dtac o inst_spec) ctrms) |
|
156 end *}) |
|
157 txt {* \begin{minipage}{\textwidth} |
|
158 @{subgoals} |
|
159 \end{minipage}*} |
|
160 (*<*)oops(*>*) |
|
161 |
|
162 text {* |
|
163 Now the tactic for proving the induction rules: |
145 *} |
164 *} |
146 |
165 |
147 ML{*fun induction_tac defs prems insts = |
166 ML{*fun induction_tac defs prems insts = |
148 EVERY1 [K (print_tac "start"), |
167 EVERY1 [ObjectLogic.full_atomize_tac, |
149 ObjectLogic.full_atomize_tac, |
|
150 cut_facts_tac prems, |
168 cut_facts_tac prems, |
151 K (rewrite_goals_tac defs), |
169 K (rewrite_goals_tac defs), |
152 EVERY' (map (dtac o inst_spec) insts), |
170 EVERY' (map (dtac o inst_spec) insts), |
153 assume_tac]*} |
171 assume_tac]*} |
154 |
172 |
155 lemma |
173 lemma |
156 assumes "even n" |
174 assumes prems: "even n" |
157 shows "P 0 \<Longrightarrow> |
175 shows "P 0 \<Longrightarrow> |
158 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
176 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
159 apply(tactic {* |
177 apply(tactic {* |
160 let |
178 let |
161 val defs = [@{thm even_def}, @{thm odd_def}] |
179 val defs = [@{thm even_def}, @{thm odd_def}] |
207 val rules = [@{prop "even (0::nat)"}, |
226 val rules = [@{prop "even (0::nat)"}, |
208 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
227 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
209 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
228 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
210 val defs = [@{thm even_def}, @{thm odd_def}] |
229 val defs = [@{thm even_def}, @{thm odd_def}] |
211 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
230 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
212 val tyss = [[@{typ "nat"}],[@{typ "nat"}]] |
231 val tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
213 in |
232 in |
214 inductions rules defs preds tyss @{context} |
233 inductions rules defs preds tyss @{context} |
215 end |
234 end |
216 *} |
235 *} |
|
236 |
217 |
237 |
218 subsection {* Introduction Rules *} |
238 subsection {* Introduction Rules *} |
219 |
239 |
220 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
240 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
221 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
241 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
264 in |
284 in |
265 introductions_tac defs rules preds 1 @{context} |
285 introductions_tac defs rules preds 1 @{context} |
266 end *}) |
286 end *}) |
267 done |
287 done |
268 |
288 |
269 |
|
270 ML{*fun introductions rules preds defs lthy = |
289 ML{*fun introductions rules preds defs lthy = |
271 let |
290 let |
272 fun prove_intro (i, goal) = |
291 fun prove_intro (i, goal) = |
273 Goal.prove lthy [] [] goal |
292 Goal.prove lthy [] [] goal |
274 (fn {context, ...} => introductions_tac defs rules preds i context) |
293 (fn {context, ...} => introductions_tac defs rules preds i context) |
275 in |
294 in |
276 map_index prove_intro rules |
295 map_index prove_intro rules |
277 end*} |
296 end*} |
|
297 |
|
298 text {* main internal function *} |
278 |
299 |
279 ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = |
300 ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = |
280 let |
301 let |
281 val syns = map snd pred_specs |
302 val syns = map snd pred_specs |
282 val pred_specs' = map fst pred_specs |
303 val pred_specs' = map fst pred_specs |
306 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
327 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
307 (pred_specs ~~ ind_rules)) #>> maps snd) |
328 (pred_specs ~~ ind_rules)) #>> maps snd) |
308 |> snd |
329 |> snd |
309 end*} |
330 end*} |
310 |
331 |
311 |
|
312 ML{*fun read_specification' vars specs lthy = |
332 ML{*fun read_specification' vars specs lthy = |
313 let |
333 let |
314 val specs' = map (fn (a, s) => [(a, [s])]) specs |
334 val specs' = map (fn (a, s) => (a, [s])) specs |
315 val ((varst, specst), _) = |
335 val ((varst, specst), _) = |
316 Specification.read_specification vars specs' lthy |
336 Specification.read_specification vars specs' lthy |
317 val specst' = map (apsnd the_single) specst |
337 val specst' = map (apsnd the_single) specst |
318 in |
338 in |
319 (varst, specst') |
339 (varst, specst') |