5 section {* Code *} |
5 section {* Code *} |
6 |
6 |
7 subsection {* Definitions *} |
7 subsection {* Definitions *} |
8 |
8 |
9 text {* |
9 text {* |
10 If we give it a term and a constant name, it will define the |
10 @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
11 constant as the term. |
11 |
12 *} |
12 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
13 |
13 |
14 ML{*fun make_defs ((binding, syn), trm) lthy = |
14 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
|
15 |
|
16 @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"} |
|
17 |
|
18 @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"} |
|
19 |
|
20 So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show |
|
21 @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}. |
|
22 Instantiating the @{text "preds"} with @{text "Ps"} gives |
|
23 @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}. |
|
24 |
|
25 We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}; |
|
26 expanding the defs |
|
27 |
|
28 @{text [display] |
|
29 "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ts"} |
|
30 |
|
31 so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"}, |
|
32 @{text "orules"}; and have to show @{text "pred ts"} |
|
33 |
|
34 the @{text "orules"} are of the form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}. |
|
35 |
|
36 using the @{text "As"} we ???? |
|
37 *} |
|
38 |
|
39 |
|
40 text {* |
|
41 First we have to produce for each predicate its definitions of the form |
|
42 |
|
43 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
|
44 |
|
45 We use the following wrapper function to actually make the definition via |
|
46 @{ML LocalTheory.define}. The function takes a predicate name, a syntax |
|
47 annotation and a term representing the right-hand side of the definition. |
|
48 *} |
|
49 |
|
50 ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy = |
15 let |
51 let |
16 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
52 val arg = ((predname, syn), (Attrib.empty_binding, trm)) |
17 val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy |
53 val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy |
18 in |
54 in |
19 (thm, lthy') |
55 (thm, lthy') |
20 end*} |
56 end*} |
21 |
57 |
22 text {* |
58 text {* |
23 Returns the definition and the local theory in which this definition has |
59 Returns the definition (as theorem) and the local theory in which this definition has |
24 been made. The @{ML internalK in Thm} is just a flag attached to the |
60 been made. The @{ML internalK in Thm} in Line 4 is just a flag attached to the |
25 theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). |
61 theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). |
26 These flags just classify theorems and have no significant meaning, except |
62 These flags just classify theorems and have no significant meaning, except |
27 for tools such as finding theorems in the theorem database. |
63 for tools such as finding theorems in the theorem database. We also |
28 *} |
64 use @{ML empty_binding in Attrib} in Line 3, since the definition does not need any |
29 |
65 theorem attributes. |
30 local_setup {* |
66 *} |
31 fn lthy => |
67 |
32 let |
68 local_setup %gray {* fn lthy => |
33 val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy |
69 let |
34 val _ = warning (str_of_thm lthy' def) |
70 val arg = ((Binding.name "MyTrue", NoSyn), @{term True}) |
35 in |
71 val (def, lthy') = make_defs arg lthy |
36 lthy' |
72 val _ = warning (str_of_thm lthy' def) |
37 end |
73 in |
38 *} |
74 lthy' |
|
75 end *} |
39 |
76 |
40 text {* |
77 text {* |
41 Prints out the theorem @{prop "MyTrue \<equiv> True"}. |
78 Prints out the theorem @{prop "MyTrue \<equiv> True"}. |
42 *} |
79 *} |
43 |
80 |
87 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
124 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
88 val pred = @{term "even::nat\<Rightarrow>bool"} |
125 val pred = @{term "even::nat\<Rightarrow>bool"} |
89 val arg_tys = [@{typ "nat"}] |
126 val arg_tys = [@{typ "nat"}] |
90 val def = defs_aux lthy orules preds (pred, arg_tys) |
127 val def = defs_aux lthy orules preds (pred, arg_tys) |
91 in |
128 in |
92 warning (Syntax.string_of_term lthy def); |
129 warning (Syntax.string_of_term lthy def); lthy |
93 lthy |
|
94 end*} |
130 end*} |
95 |
131 |
96 text {* |
132 text {* |
97 The arguments of the main function for the definitions are |
133 The arguments of the main function for the definitions are |
98 the intro rules; the predicates and their names, their syntax |
134 the intro rules; the predicates and their names, their syntax |
114 In line 4 we generate the intro rules in the object logic; for this we have to |
150 In line 4 we generate the intro rules in the object logic; for this we have to |
115 obtain the theory behind the local theory (Line 3); with this we can |
151 obtain the theory behind the local theory (Line 3); with this we can |
116 call @{ML defs_aux} to generate the terms for the left-hand sides. |
152 call @{ML defs_aux} to generate the terms for the left-hand sides. |
117 The actual definitions are made in Line 7. |
153 The actual definitions are made in Line 7. |
118 *} |
154 *} |
|
155 |
|
156 local_setup {* |
|
157 fn lthy => |
|
158 let |
|
159 val rules = [@{prop "even 0"}, |
|
160 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
|
161 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
|
162 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
|
163 val prednames = [Binding.name "even", Binding.name "odd"] |
|
164 val syns = [NoSyn, NoSyn] |
|
165 val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
|
166 val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy |
|
167 in |
|
168 warning (str_of_thms lthy' defs); lthy |
|
169 end*} |
|
170 |
119 |
171 |
120 subsection {* Induction Principles *} |
172 subsection {* Induction Principles *} |
121 |
173 |
122 text {* Recall the proof for the induction principle for @{term "even"}: *} |
174 text {* Recall the proof for the induction principle for @{term "even"}: *} |
123 |
175 |
187 text {* |
239 text {* |
188 While the generic proof is relatively simple, it is a bit harder to |
240 While the generic proof is relatively simple, it is a bit harder to |
189 set up the goals for the induction principles. |
241 set up the goals for the induction principles. |
190 *} |
242 *} |
191 |
243 |
192 ML {* singleton *} |
244 ML {* |
193 ML {* ProofContext.export *} |
245 fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys) = |
|
246 let |
|
247 val zs = replicate (length tys) "z" |
|
248 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
|
249 val newargs = map Free (newargnames ~~ tys) |
|
250 |
|
251 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
|
252 val goal = Logic.list_implies |
|
253 (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
|
254 in |
|
255 Goal.prove lthy3 [] [prem] goal |
|
256 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
|
257 |> singleton (ProofContext.export lthy3 lthy2) |
|
258 end |
|
259 *} |
194 |
260 |
195 ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = |
261 ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = |
196 let |
262 let |
197 val Ps = replicate (length preds) "P" |
263 val Ps = replicate (length preds) "P" |
198 val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 |
264 val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 |
202 val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
268 val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
203 val newpreds = map Free (newprednames ~~ tyss') |
269 val newpreds = map Free (newprednames ~~ tyss') |
204 val cnewpreds = map (cterm_of thy) newpreds |
270 val cnewpreds = map (cterm_of thy) newpreds |
205 val rules' = map (subst_free (preds ~~ newpreds)) rules |
271 val rules' = map (subst_free (preds ~~ newpreds)) rules |
206 |
272 |
207 |
273 in |
208 fun prove_induction ((pred, newpred), tys) = |
274 map (prove_induction lthy2 defs rules' cnewpreds) |
209 let |
275 (preds ~~ newpreds ~~ tyss) |
210 val zs = replicate (length tys) "z" |
276 |> ProofContext.export lthy2 lthy1 |
211 val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
|
212 val newargs = map Free (newargnames ~~ tys) |
|
213 |
|
214 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
|
215 val goal = Logic.list_implies |
|
216 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
|
217 in |
|
218 Goal.prove lthy3 [] [prem] goal |
|
219 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
|
220 |> singleton (ProofContext.export lthy3 lthy1) |
|
221 end |
|
222 in |
|
223 map prove_induction (preds ~~ newpreds ~~ tyss) |
|
224 end*} |
277 end*} |
225 |
278 |
226 ML {* |
279 ML {* |
227 let |
280 let |
228 val rules = [@{prop "even (0::nat)"}, |
281 val rules = [@{prop "even (0::nat)"}, |