91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory Ind_Code
210
+ − 2
imports "../Base" "../FirstSteps" Ind_General_Scheme
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3
begin
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
210
+ − 5
section {* The Gory Details *}
208
+ − 6
+ − 7
subsection {* Definitions *}
+ − 8
+ − 9
text {*
209
+ − 10
We first have to produce for each predicate the definition, whose general form is
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
@{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 13
208
+ − 14
and then ``register'' the definition inside a local theory.
190
+ − 15
To do the latter, we use the following wrapper for
183
+ − 16
@{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
annotation and a term representing the right-hand side of the definition.
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
210
+ − 20
ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy =
164
+ − 21
let
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
val arg = ((predname, syn), (Attrib.empty_binding, trm))
176
+ − 23
val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
164
+ − 24
in
176
+ − 25
(thm, lthy')
164
+ − 26
end*}
+ − 27
+ − 28
text {*
183
+ − 29
It returns the definition (as a theorem) and the local theory in which this definition has
184
+ − 30
been made. In Line 4, @{ML internalK in Thm} is a flag attached to the
210
+ − 31
theorem (others possibile flags are @{ML definitionK in Thm} and @{ML axiomK in Thm}).
176
+ − 32
These flags just classify theorems and have no significant meaning, except
183
+ − 33
for tools that, for example, find theorems in the theorem database. We also
210
+ − 34
use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates
+ − 35
the definitions do not need to have any theorem attributes. A testcase for this
+ − 36
function is
164
+ − 37
*}
+ − 38
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
local_setup %gray {* fn lthy =>
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
let
209
+ − 41
val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})
210
+ − 42
val (def, lthy') = make_defn arg lthy
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
in
194
+ − 44
warning (str_of_thm_no_vars lthy' def); lthy'
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
end *}
164
+ − 46
+ − 47
text {*
210
+ − 48
which introduces the definition @{prop "MyTrue \<equiv> True"} and then prints it out.
208
+ − 49
Since we are testing the function inside \isacommand{local\_setup}, i.e., make
+ − 50
changes to the ambient theory, we can query the definition with the usual
183
+ − 51
command \isacommand{thm}:
179
+ − 52
+ − 53
\begin{isabelle}
+ − 54
\isacommand{thm}~@{text "MyTrue_def"}\\
+ − 55
@{text "> MyTrue \<equiv> True"}
+ − 56
\end{isabelle}
164
+ − 57
208
+ − 58
The next two functions construct the right-hand sides of the definitions,
+ − 59
which are terms of the form
179
+ − 60
190
+ − 61
@{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
179
+ − 62
208
+ − 63
When constructing them, the variables @{text "zs"} need to be chosen so that
+ − 64
they do not occur in the @{text orules} and also be distinct from the @{text
+ − 65
"preds"}.
+ − 66
183
+ − 67
210
+ − 68
The first function constructs the term for one particular predicate (the
+ − 69
argument @{text "pred"} in the code belo). The number of arguments of this predicate is
190
+ − 70
determined by the number of argument types given in @{text "arg_tys"}.
208
+ − 71
The other arguments are all the @{text "preds"} and the @{text "orules"}.
164
+ − 72
*}
+ − 73
210
+ − 74
ML %linenosgray{*fun defn_aux lthy orules preds (pred, arg_tys) =
164
+ − 75
let
+ − 76
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
+ − 77
+ − 78
val fresh_args =
176
+ − 79
arg_tys
164
+ − 80
|> map (pair "z")
179
+ − 81
|> Variable.variant_frees lthy (preds @ orules)
164
+ − 82
|> map Free
+ − 83
in
+ − 84
list_comb (pred, fresh_args)
+ − 85
|> fold_rev (curry HOLogic.mk_imp) orules
+ − 86
|> fold_rev mk_all preds
+ − 87
|> fold_rev lambda fresh_args
+ − 88
end*}
+ − 89
+ − 90
text {*
184
+ − 91
The function in Line 3 is just a helper function for constructing universal
+ − 92
quantifications. The code in Lines 5 to 9 produces the fresh @{text
190
+ − 93
"zs"}. For this it pairs every argument type with the string
184
+ − 94
@{text [quotes] "z"} (Line 7); then generates variants for all these strings
190
+ − 95
so that they are unique w.r.t.~to the predicates and @{text "orules"} (Line 8);
184
+ − 96
in Line 9 it generates the corresponding variable terms for the unique
+ − 97
strings.
164
+ − 98
183
+ − 99
The unique free variables are applied to the predicate (Line 11) using the
+ − 100
function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
+ − 101
Line 13 we quantify over all predicates; and in line 14 we just abstract
208
+ − 102
over all the @{text "zs"}, i.e., the fresh arguments of the
190
+ − 103
predicate. A testcase for this function is
164
+ − 104
*}
+ − 105
179
+ − 106
local_setup %gray{* fn lthy =>
176
+ − 107
let
+ − 108
val pred = @{term "even::nat\<Rightarrow>bool"}
+ − 109
val arg_tys = [@{typ "nat"}]
210
+ − 110
val def = defn_aux lthy eo_orules eo_preds (pred, arg_tys)
173
+ − 111
in
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
warning (Syntax.string_of_term lthy def); lthy
179
+ − 113
end *}
173
+ − 114
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 115
text {*
210
+ − 116
The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints
208
+ − 117
out the generated definition. So we obtain as printout
179
+ − 118
+ − 119
@{text [display]
+ − 120
"\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+ − 121
\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
+ − 122
210
+ − 123
If we try out the function for the definition of freshness
+ − 124
*}
+ − 125
+ − 126
local_setup %gray{* fn lthy =>
+ − 127
(warning (Syntax.string_of_term lthy
+ − 128
(defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
+ − 129
lthy) *}
+ − 130
+ − 131
text {*
+ − 132
we obtain
+ − 133
+ − 134
@{term [display]
+ − 135
"\<lambda>z za. \<forall>fresh. (\<forall>a b. \<not> a = b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+ − 136
(\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+ − 137
(\<forall>a t. fresh a (Lam a t)) \<longrightarrow>
+ − 138
(\<forall>a b t. \<not> a = b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh z za"}
+ − 139
+ − 140
190
+ − 141
The second function for the definitions has to just iterate the function
210
+ − 142
@{ML defn_aux} over all predicates. The argument @{text "preds"} is again
184
+ − 143
the the list of predicates as @{ML_type term}s; the argument @{text
209
+ − 144
"prednames"} is the list of names of the predicates; @{text syns} are the
+ − 145
syntax annotations for each predicate; @{text "arg_tyss"} is
184
+ − 146
the list of argument-type-lists for each predicate.
164
+ − 147
*}
+ − 148
210
+ − 149
ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy =
164
+ − 150
let
+ − 151
val thy = ProofContext.theory_of lthy
+ − 152
val orules = map (ObjectLogic.atomize_term thy) rules
210
+ − 153
val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss)
164
+ − 154
in
210
+ − 155
fold_map make_defn (prednames ~~ syns ~~ defs) lthy
164
+ − 156
end*}
+ − 157
+ − 158
text {*
184
+ − 159
The user will state the introduction rules using meta-implications and
+ − 160
meta-quanti\-fications. In Line 4, we transform these introduction rules into
+ − 161
the object logic (since definitions cannot be stated with
+ − 162
meta-connectives). To do this transformation we have to obtain the theory
+ − 163
behind the local theory (Line 3); with this theory we can use the function
+ − 164
@{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
210
+ − 165
to @{ML defn_aux} in Line 5 produces all right-hand sides of the
184
+ − 166
definitions. The actual definitions are then made in Line 7. The result
190
+ − 167
of the function is a list of theorems and a local theory. A testcase for
+ − 168
this function is
164
+ − 169
*}
+ − 170
179
+ − 171
local_setup %gray {* fn lthy =>
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
let
208
+ − 173
val (defs, lthy') =
210
+ − 174
defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 175
in
208
+ − 176
warning (str_of_thms_no_vars lthy' defs); lthy
179
+ − 177
end *}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 178
179
+ − 179
text {*
184
+ − 180
where we feed into the functions all parameters corresponding to
+ − 181
the @{text even}-@{text odd} example. The definitions we obtain
+ − 182
are:
179
+ − 183
210
+ − 184
@{text [display, break]
+ − 185
"even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+ − 186
\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
+ − 187
odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+ − 188
\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
208
+ − 190
Note that in the testcase we return the local theory @{text lthy}
+ − 191
(not the modified @{text lthy'}). As a result the test case has no effect
210
+ − 192
on the ambient theory. The reason is that if we introduce the
+ − 193
definition again, we pollute the name space with two versions of @{text "even"}
208
+ − 194
and @{text "odd"}.
164
+ − 195
210
+ − 196
This completes the code for introducing the definitions. Next we deal with
208
+ − 197
the induction principles.
+ − 198
*}
+ − 199
210
+ − 200
subsection {* Induction Principles *}
208
+ − 201
+ − 202
text {*
+ − 203
Recall that the proof of the induction principle
184
+ − 204
for @{text "even"} was:
179
+ − 205
*}
176
+ − 206
210
+ − 207
lemma manual_ind_prin_even:
209
+ − 208
assumes prem: "even z"
+ − 209
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
176
+ − 210
apply(atomize (full))
209
+ − 211
apply(cut_tac prem)
176
+ − 212
apply(unfold even_def)
+ − 213
apply(drule spec[where x=P])
+ − 214
apply(drule spec[where x=Q])
+ − 215
apply(assumption)
+ − 216
done
+ − 217
179
+ − 218
text {*
190
+ − 219
The code for automating such induction principles has to accomplish two tasks:
184
+ − 220
constructing the induction principles from the given introduction
190
+ − 221
rules and then automatically generating proofs for them using a tactic.
183
+ − 222
+ − 223
The tactic will use the following helper function for instantiating universal
184
+ − 224
quantifiers.
179
+ − 225
*}
176
+ − 226
179
+ − 227
ML{*fun inst_spec ctrm =
+ − 228
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
164
+ − 229
+ − 230
text {*
184
+ − 231
This helper function instantiates the @{text "?x"} in the theorem
208
+ − 232
@{thm spec} with a given @{ML_type cterm}. We call this helper function
+ − 233
in the tactic:
164
+ − 234
*}
+ − 235
183
+ − 236
ML{*fun inst_spec_tac ctrms =
+ − 237
EVERY' (map (dtac o inst_spec) ctrms)*}
+ − 238
+ − 239
text {*
208
+ − 240
This tactic allows us to instantiate in the following proof the
184
+ − 241
three quantifiers in the assumption.
+ − 242
*}
183
+ − 243
184
+ − 244
lemma
+ − 245
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ − 246
shows "\<forall>x y z. P x y z \<Longrightarrow> True"
176
+ − 247
apply (tactic {*
184
+ − 248
inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
179
+ − 249
txt {*
183
+ − 250
We obtain the goal state
179
+ − 251
+ − 252
\begin{minipage}{\textwidth}
+ − 253
@{subgoals}
+ − 254
\end{minipage}*}
164
+ − 255
(*<*)oops(*>*)
+ − 256
+ − 257
text {*
183
+ − 258
Now the complete tactic for proving the induction principles can
+ − 259
be implemented as follows:
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
*}
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 261
210
+ − 262
ML %linenosgray{*fun ind_tac defs prem insts =
176
+ − 263
EVERY1 [ObjectLogic.full_atomize_tac,
208
+ − 264
cut_facts_tac prem,
164
+ − 265
K (rewrite_goals_tac defs),
183
+ − 266
inst_spec_tac insts,
164
+ − 267
assume_tac]*}
+ − 268
179
+ − 269
text {*
210
+ − 270
We have to give it as arguments the definitions, the premise (this premise
+ − 271
is @{text "even n"} in lemma @{thm [source] manual_ind_prin_even}) and the
+ − 272
instantiations. Compare this tactic with the manual for the lemma @{thm
+ − 273
[source] manual_ind_prin_even}: as you can see there is almost a one-to-one
+ − 274
correspondence between the \isacommand{apply}-script and the @{ML
+ − 275
ind_tac}. Two testcases for this tactic are:
183
+ − 276
*}
+ − 277
210
+ − 278
lemma automatic_ind_prin_even:
208
+ − 279
assumes prem: "even z"
+ − 280
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
210
+ − 281
by (tactic {* ind_tac eo_defs @{thms prem}
+ − 282
[@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+ − 283
+ − 284
lemma automatic_ind_prin_fresh:
+ − 285
assumes prem: "fresh z za"
+ − 286
shows "(\<And>a b. a \<noteq> b \<Longrightarrow> P a (Var b)) \<Longrightarrow>
+ − 287
(\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>
+ − 288
(\<And>a t. P a (Lam a t)) \<Longrightarrow>
+ − 289
(\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"
+ − 290
by (tactic {* ind_tac @{thms fresh_def} @{thms prem}
+ − 291
[@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})
+ − 292
164
+ − 293
165
+ − 294
text {*
210
+ − 295
Let us have a closer look at the first proved theorem:
209
+ − 296
+ − 297
\begin{isabelle}
210
+ − 298
\isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\
+ − 299
@{text "> "}~@{thm automatic_ind_prin_even}
209
+ − 300
\end{isabelle}
+ − 301
210
+ − 302
The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic
+ − 303
variables (since they are not quantified in the lemma). These schematic
+ − 304
variables are needed so that they can be instantiated by the user later
+ − 305
on. We have to take care to also generate these schematic variables when
+ − 306
generating the goals for the induction principles. While the tactic for
+ − 307
proving the induction principles is relatively simple, it will be a bit
+ − 308
of work to construct the goals from the introduction rules the user
+ − 309
provides. In general we have to construct for each predicate @{text "pred"}
+ − 310
a goal of the form
179
+ − 311
+ − 312
@{text [display]
208
+ − 313
"pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
180
+ − 314
190
+ − 315
where the predicates @{text preds} are replaced in the introduction
208
+ − 316
rules by new distinct variables @{text "?Ps"}.
+ − 317
We also need to generate fresh arguments @{text "?zs"} for the predicate
+ − 318
@{text "pred"} and the @{text "?P"} in the conclusion. Note
190
+ − 319
that the @{text "?Ps"} and @{text "?zs"} need to be
208
+ − 320
schematic variables that can be instantiated by the user.
190
+ − 321
208
+ − 322
We generate these goals in two steps. The first function expects that the
+ − 323
introduction rules are already appropriately substituted. The argument
+ − 324
@{text "srules"} stands for these substituted rules; @{text cnewpreds} are
+ − 325
the certified terms coresponding to the variables @{text "?Ps"}; @{text
210
+ − 326
"pred"} is the predicate for which we prove the induction principle;
208
+ − 327
@{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
+ − 328
types of this predicate.
165
+ − 329
*}
+ − 330
210
+ − 331
ML %linenosgray{*fun prove_ind lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 332
let
190
+ − 333
val zs = replicate (length arg_tys) "z"
179
+ − 334
val (newargnames, lthy') = Variable.variant_fixes zs lthy;
190
+ − 335
val newargs = map Free (newargnames ~~ arg_tys)
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 336
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
val goal = Logic.list_implies
183
+ − 339
(srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
in
179
+ − 341
Goal.prove lthy' [] [prem] goal
210
+ − 342
(fn {prems, ...} => ind_tac defs prems cnewpreds)
179
+ − 343
|> singleton (ProofContext.export lthy' lthy)
+ − 344
end *}
+ − 345
180
+ − 346
text {*
190
+ − 347
In Line 3 we produce names @{text "zs"} for each type in the
183
+ − 348
argument type list. Line 4 makes these names unique and declares them as
210
+ − 349
\emph{free} (but fixed) variables in the local theory @{text "lthy'"}.
+ − 350
That means they are not (yet) schematic variables.
+ − 351
In Line 5 we construct the terms corresponding to these variables.
208
+ − 352
The variables are applied to the predicate in Line 7 (this corresponds
190
+ − 353
to the first premise @{text "pred zs"} of the induction principle).
+ − 354
In Line 8 and 9, we first construct the term @{text "P zs"}
209
+ − 355
and then add the (substituted) introduction rules as premises. In case that
184
+ − 356
no introduction rules are given, the conclusion of this implication needs
183
+ − 357
to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
+ − 358
mechanism will fail.
180
+ − 359
208
+ − 360
In Line 11 we set up the goal to be proved; in the next line we call the
+ − 361
tactic for proving the induction principle. As mentioned before, this tactic
+ − 362
expects the definitions, the premise and the (certified) predicates with
+ − 363
which the introduction rules have been substituted. The code in these two
+ − 364
lines will return a theorem. However, it is a theorem
184
+ − 365
proved inside the local theory @{text "lthy'"}, where the variables @{text
209
+ − 366
"zs"} are fixed, but free (see Line 4). By exporting this theorem from @{text
210
+ − 367
"lthy'"} (which contains the @{text "zs"} as free variables) to @{text
208
+ − 368
"lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
+ − 369
A testcase for this function is
190
+ − 370
*}
180
+ − 371
190
+ − 372
local_setup %gray{* fn lthy =>
+ − 373
let
210
+ − 374
val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
190
+ − 375
val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
210
+ − 376
val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules
190
+ − 377
val newpred = @{term "P::nat\<Rightarrow>bool"}
+ − 378
val intro =
210
+ − 379
prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
190
+ − 380
in
194
+ − 381
warning (str_of_thm lthy intro); lthy
210
+ − 382
end *}
184
+ − 383
190
+ − 384
text {*
210
+ − 385
This prints out the theorem:
190
+ − 386
+ − 387
@{text [display]
+ − 388
" \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"}
+ − 389
210
+ − 390
The export from @{text lthy'} to @{text lthy} in Line 13 above
+ − 391
has correctly turned the free, but fixed, @{text "z"} into a schematic
209
+ − 392
variable @{text "?z"}; the variables @{text "P"} and @{text "Q"} are not yet
208
+ − 393
schematic.
190
+ − 394
+ − 395
We still have to produce the new predicates with which the introduction
210
+ − 396
rules are substituted and iterate @{ML prove_ind} over all
208
+ − 397
predicates. This is what the second function does:
180
+ − 398
*}
165
+ − 399
210
+ − 400
ML %linenosgray{*fun inds rules defs preds arg_tyss lthy =
164
+ − 401
let
+ − 402
val Ps = replicate (length preds) "P"
183
+ − 403
val (newprednames, lthy') = Variable.variant_fixes Ps lthy
164
+ − 404
183
+ − 405
val thy = ProofContext.theory_of lthy'
164
+ − 406
184
+ − 407
val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
165
+ − 408
val newpreds = map Free (newprednames ~~ tyss')
164
+ − 409
val cnewpreds = map (cterm_of thy) newpreds
184
+ − 410
val srules = map (subst_free (preds ~~ newpreds)) rules
164
+ − 411
+ − 412
in
210
+ − 413
map (prove_ind lthy' defs srules cnewpreds)
184
+ − 414
(preds ~~ newpreds ~~ arg_tyss)
183
+ − 415
|> ProofContext.export lthy' lthy
165
+ − 416
end*}
+ − 417
184
+ − 418
text {*
208
+ − 419
In Line 3, we generate a string @{text [quotes] "P"} for each predicate.
184
+ − 420
In Line 4, we use the same trick as in the previous function, that is making the
190
+ − 421
@{text "Ps"} fresh and declaring them as fixed, but free, in
184
+ − 422
the new local theory @{text "lthy'"}. From the local theory we extract
+ − 423
the ambient theory in Line 6. We need this theory in order to certify
208
+ − 424
the new predicates. In Line 8, we construct the types of these new predicates
190
+ − 425
using the given argument types. Next we turn them into terms and subsequently
+ − 426
certify them (Line 9 and 10). We can now produce the substituted introduction rules
+ − 427
(Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate
+ − 428
the proofs for all predicates.
184
+ − 429
From this we obtain a list of theorems. Finally we need to export the
208
+ − 430
fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
184
+ − 431
(Line 16).
+ − 432
+ − 433
A testcase for this function is
+ − 434
*}
+ − 435
+ − 436
local_setup %gray {* fn lthy =>
+ − 437
let
210
+ − 438
val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
184
+ − 439
in
194
+ − 440
warning (str_of_thms lthy ind_thms); lthy
190
+ − 441
end *}
165
+ − 442
176
+ − 443
184
+ − 444
text {*
+ − 445
which prints out
+ − 446
+ − 447
@{text [display]
210
+ − 448
"even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
+ − 449
(\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
+ − 450
odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
+ − 451
(\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
184
+ − 452
208
+ − 453
Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic
210
+ − 454
variables. The numbers attached to these variables have been introduced by
+ − 455
the pretty-printer and are \emph{not} important for the user.
184
+ − 456
210
+ − 457
This completes the code for the induction principles. The final peice
+ − 458
of reasoning infrastructure we need are the introduction rules.
208
+ − 459
*}
+ − 460
+ − 461
subsection {* Introduction Rules *}
+ − 462
+ − 463
text {*
210
+ − 464
The proofs of the introduction rules are quite a bit
+ − 465
more involved than the ones for the induction principles.
+ − 466
To ease somewhat our work here, we use the following two helper
208
+ − 467
functions.
+ − 468
184
+ − 469
*}
+ − 470
165
+ − 471
ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
+ − 472
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
+ − 473
190
+ − 474
text {*
208
+ − 475
To see what these functions do, let us suppose whe have the following three
190
+ − 476
theorems.
+ − 477
*}
+ − 478
+ − 479
lemma all_elims_test:
+ − 480
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ − 481
shows "\<forall>x y z. P x y z" sorry
+ − 482
+ − 483
lemma imp_elims_test:
+ − 484
shows "A \<longrightarrow> B \<longrightarrow> C" sorry
+ − 485
+ − 486
lemma imp_elims_test':
+ − 487
shows "A" "B" sorry
+ − 488
+ − 489
text {*
+ − 490
The function @{ML all_elims} takes a list of (certified) terms and instantiates
+ − 491
theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
210
+ − 492
the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
190
+ − 493
+ − 494
@{ML_response_fake [display, gray]
+ − 495
"let
+ − 496
val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+ − 497
val new_thm = all_elims ctrms @{thm all_elims_test}
+ − 498
in
194
+ − 499
warning (str_of_thm_no_vars @{context} new_thm)
190
+ − 500
end"
+ − 501
"P a b c"}
+ − 502
+ − 503
Similarly, the function @{ML imp_elims} eliminates preconditions from implications.
210
+ − 504
For example we can eliminate the preconditions @{text "A"} and @{text "B"} from
+ − 505
@{thm [source] imp_elims_test}:
190
+ − 506
+ − 507
@{ML_response_fake [display, gray]
194
+ − 508
"warning (str_of_thm_no_vars @{context}
190
+ − 509
(imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+ − 510
"C"}
+ − 511
210
+ − 512
To explain the proof for the introduction rule, our running example will be
+ − 513
the rule:
190
+ − 514
209
+ − 515
\begin{isabelle}
210
+ − 516
@{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
209
+ − 517
\end{isabelle}
+ − 518
210
+ − 519
for freshness of applications. We set up the proof as follows:
190
+ − 520
*}
+ − 521
192
+ − 522
lemma fresh_App:
210
+ − 523
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+ − 524
(*<*)oops(*>*)
+ − 525
+ − 526
text {*
+ − 527
The first step will be to expand the definitions of freshness
+ − 528
and then introduce quantifiers and implications. For this we
+ − 529
will use the tactic
+ − 530
*}
+ − 531
+ − 532
ML{*fun expand_tac defs =
+ − 533
ObjectLogic.rulify_tac 1
+ − 534
THEN rewrite_goals_tac defs
+ − 535
THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
+ − 536
+ − 537
text {*
+ − 538
The first step of ``rulifying'' the lemma will turn out important
+ − 539
later on. Applying this tactic
+ − 540
*}
+ − 541
+ − 542
(*<*)
+ − 543
lemma fresh_App:
+ − 544
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+ − 545
(*>*)
+ − 546
apply(tactic {* expand_tac @{thms fresh_def} *})
209
+ − 547
+ − 548
txt {*
210
+ − 549
we end up in the goal state
+ − 550
209
+ − 551
\begin{isabelle}
210
+ − 552
@{subgoals [display]}
209
+ − 553
\end{isabelle}
210
+ − 554
+ − 555
As you can see, there are parameters (namely @{text "a"}, @{text "b"}
+ − 556
and @{text "t"}) which come from the introduction rule and parameters
+ − 557
(in the case above only @{text "fresh"}) which come from the universal
+ − 558
quantification in the definition @{term "fresh a (App t s)"}.
+ − 559
Similarly, there are preconditions
+ − 560
that come from the premises of the rule and premises from the
+ − 561
definition. We need to treat these
+ − 562
parameters and preconditions differently. In the code below
+ − 563
we will therefore separate them into @{text "params1"} and @{text params2},
+ − 564
respectively @{text "prems1"} and @{text "prems2"}. To do this
+ − 565
separation, it is best to open a subproof with the tactic
+ − 566
@{ML SUBPROOF}, since this tactic provides us
+ − 567
with the parameters (as list of @{ML_type cterm}s) and the premises
+ − 568
(as list of @{ML_type thm}s). The problem we have to overcome
+ − 569
with @{ML SUBPROOF} is that this tactic always expects us to completely
+ − 570
discharge with the goal (see Section ???). This is inconvenient for
+ − 571
our gradual explanation of the proof. To circumvent this inconvenience
+ − 572
we use the following modified tactic:
+ − 573
*}
+ − 574
(*<*)oops(*>*)
+ − 575
ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}
+ − 576
+ − 577
text {*
+ − 578
If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will
+ − 579
still succeed. With this testing tactic, we can gradually implement
+ − 580
all necessary proof steps.
+ − 581
*}
+ − 582
+ − 583
text_raw {*
+ − 584
\begin{figure}[t]
+ − 585
\begin{minipage}{\textwidth}
+ − 586
\begin{isabelle}
+ − 587
*}
+ − 588
ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
+ − 589
let
+ − 590
val s = ["Params1 from the rule:", str_of_cterms ctxt params1]
+ − 591
@ ["Params2 from the predicate:", str_of_cterms ctxt params2]
+ − 592
@ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1)
+ − 593
@ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2)
+ − 594
in
+ − 595
s |> separate "\n"
+ − 596
|> implode
+ − 597
|> warning
+ − 598
end*}
+ − 599
text_raw{*
+ − 600
\end{isabelle}
+ − 601
\end{minipage}
+ − 602
\caption{FIXME\label{fig:chopprint}}
+ − 603
\end{figure}
+ − 604
*}
+ − 605
+ − 606
text {*
+ − 607
First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
+ − 608
from @{text "params"} and @{text "prems"}, respectively. To see what is
+ − 609
going in our example, we will print out the values using the printing
+ − 610
function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
+ − 611
supply us the @{text "params"} and @{text "prems"} as lists, we can
+ − 612
separate them using the function @{ML chop}.
+ − 613
*}
+ − 614
+ − 615
ML{*fun chop_test_tac preds rules =
+ − 616
SUBPROOF_test (fn {params, prems, context, ...} =>
+ − 617
let
+ − 618
val (params1, params2) = chop (length params - length preds) params
+ − 619
val (prems1, prems2) = chop (length prems - length rules) prems
+ − 620
in
+ − 621
chop_print params1 params2 prems1 prems2 context; no_tac
+ − 622
end) *}
+ − 623
+ − 624
text {*
+ − 625
For the separation we can rely on that Isabelle deterministically
+ − 626
produces parameter and premises in a goal state. The last parameters
+ − 627
that were introduced, come from the quantifications in the definitions.
+ − 628
Therefore we only have to subtract the number of predicates (in this
+ − 629
case only @{text "1"} from the lenghts of all parameters. Similarly
+ − 630
with the @{text "prems"}. The last premises in the goal state must
+ − 631
come from unfolding of the conclusion. So we can just subtract
+ − 632
the number of rules from the number of all premises. Applying
+ − 633
this tactic in our example
209
+ − 634
*}
+ − 635
210
+ − 636
(*<*)
+ − 637
lemma fresh_App:
+ − 638
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+ − 639
apply(tactic {* expand_tac @{thms fresh_def} *})
+ − 640
(*>*)
+ − 641
apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})
+ − 642
(*<*)oops(*>*)
+ − 643
+ − 644
text {*
+ − 645
gives
209
+ − 646
210
+ − 647
\begin{isabelle}
+ − 648
@{text "Params1 from the rule:"}\\
+ − 649
@{text "a, b, t"}\\
+ − 650
@{text "Params2 from the predicate:"}\\
+ − 651
@{text "fresh"}\\
+ − 652
@{text "Prems1 from the rule:"}\\
+ − 653
@{term "a \<noteq> b"}\\
+ − 654
@{text [break]
+ − 655
"\<forall>fresh.
+ − 656
(\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+ − 657
(\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+ − 658
(\<forall>a t. fresh a (Lam a t)) \<longrightarrow>
+ − 659
(\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
+ − 660
@{text "Prems2 from the predicate:"}\\
+ − 661
@{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\
+ − 662
@{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\
+ − 663
@{term "\<forall>a t. fresh a (Lam a t)"}\\
+ − 664
@{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}
+ − 665
\end{isabelle}
208
+ − 666
192
+ − 667
210
+ − 668
We now have to select from @{text prems2} the premise
+ − 669
that corresponds to the introduction rule we prove, namely:
+ − 670
+ − 671
@{term [display] "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}
+ − 672
+ − 673
To use this premise with @{ML rtac}, we need to instantiate its
+ − 674
quantifiers (with @{text params1}) and transform it into a
+ − 675
introduction rule (using @{ML "ObjectLogic.rulify"}.
+ − 676
So we can modify the subproof as follows:
+ − 677
*}
+ − 678
+ − 679
ML{*fun apply_prem_tac i preds rules =
+ − 680
SUBPROOF_test (fn {params, prems, context, ...} =>
+ − 681
let
+ − 682
val (params1, params2) = chop (length params - length preds) params
+ − 683
val (prems1, prems2) = chop (length prems - length rules) prems
+ − 684
in
+ − 685
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ − 686
THEN print_tac ""
+ − 687
THEN no_tac
+ − 688
end) *}
+ − 689
+ − 690
text {* and apply it with *}
+ − 691
+ − 692
(*<*)
+ − 693
lemma fresh_App:
+ − 694
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+ − 695
apply(tactic {* expand_tac @{thms fresh_def} *})
+ − 696
(*>*)
+ − 697
apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
+ − 698
(*<*)oops(*>*)
+ − 699
+ − 700
text {*
+ − 701
Since we print out the goal state after the @{ML rtac} we can see
+ − 702
the goal state has the two subgoals
+ − 703
+ − 704
\begin{isabelle}
+ − 705
@{text "1."}~@{prop "a \<noteq> b"}\\
+ − 706
@{text "2."}~@{prop "fresh a t"}
+ − 707
\end{isabelle}
+ − 708
+ − 709
where the first comes from a non-recursive precondition of the rule
+ − 710
and the second comes from a recursive precondition. The first kind
+ − 711
can be solved immediately by @{text "prems1"}. The second kind
+ − 712
needs more work. It can be solved with the other premise in @{text "prems1"},
+ − 713
namely
+ − 714
+ − 715
@{term [break,display]
+ − 716
"\<forall>fresh.
+ − 717
(\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+ − 718
(\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+ − 719
(\<forall>a t. fresh a (Lam a t)) \<longrightarrow>
+ − 720
(\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}
+ − 721
+ − 722
but we have to instantiate it appropriately. These instantiations
+ − 723
come from @{text "params1"} and @{text "prems2"}. We can determine
+ − 724
whether we are in the simple or complicated case by checking whether
+ − 725
the topmost connective is @{text "\<forall>"}. The premises in the simple
+ − 726
case cannot have such a quantification, since in the first step
+ − 727
of @{ML "expand_tac"} was the ``rulification'' of the lemma. So
+ − 728
we can implement the following function
+ − 729
*}
+ − 730
+ − 731
ML{*fun prepare_prem params2 prems2 prem =
+ − 732
rtac (case prop_of prem of
165
+ − 733
_ $ (Const (@{const_name All}, _) $ _) =>
210
+ − 734
prem |> all_elims params2
+ − 735
|> imp_elims prems2
+ − 736
| _ => prem) *}
+ − 737
+ − 738
text {*
+ − 739
which either applies the premise outright or if it had an
+ − 740
outermost universial quantification, instantiates it first with
+ − 741
@{text "params1"} and then @{text "prems1"}. The following tactic
+ − 742
will therefore prove the lemma.
+ − 743
*}
+ − 744
+ − 745
ML{*fun prove_intro_tac i preds rules =
+ − 746
SUBPROOF (fn {params, prems, context, ...} =>
+ − 747
let
+ − 748
val (params1, params2) = chop (length params - length preds) params
+ − 749
val (prems1, prems2) = chop (length prems - length rules) prems
+ − 750
in
+ − 751
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ − 752
THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
+ − 753
end) *}
+ − 754
+ − 755
text {*
+ − 756
We can complete the proof of the introduction rule now as follows:
+ − 757
*}
+ − 758
+ − 759
(*<*)
+ − 760
lemma fresh_App:
+ − 761
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+ − 762
apply(tactic {* expand_tac @{thms fresh_def} *})
+ − 763
(*>*)
+ − 764
apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
+ − 765
done
+ − 766
+ − 767
text {*
+ − 768
Unfortunately, not everything is done yet.
+ − 769
*}
+ − 770
+ − 771
lemma accpartI:
+ − 772
shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+ − 773
apply(tactic {* expand_tac @{thms accpart_def} *})
+ − 774
apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
+ − 775
apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
+ − 776
+ − 777
txt {*
+ − 778
+ − 779
@{subgoals [display]}
+ − 780
+ − 781
\begin{isabelle}
+ − 782
@{text "Params1 from the rule:"}\\
+ − 783
@{text "x"}\\
+ − 784
@{text "Params2 from the predicate:"}\\
+ − 785
@{text "P"}\\
+ − 786
@{text "Prems1 from the rule:"}\\
+ − 787
@{text "R ?y x \<Longrightarrow> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P ?y"}\\
+ − 788
@{text "Prems2 from the predicate:"}\\
+ − 789
@{term "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x"}\\
+ − 790
\end{isabelle}
+ − 791
+ − 792
*}
+ − 793
(*<*)oops(*>*)
+ − 794
+ − 795
+ − 796
ML{*fun prepare_prem params2 prems2 ctxt prem =
+ − 797
SUBPROOF (fn {prems, ...} =>
+ − 798
let
+ − 799
val prem' = prems MRS prem
+ − 800
in
+ − 801
rtac (case prop_of prem' of
+ − 802
_ $ (Const (@{const_name All}, _) $ _) =>
+ − 803
prem' |> all_elims params2
+ − 804
|> imp_elims prems2
+ − 805
| _ => prem') 1
+ − 806
end) ctxt *}
+ − 807
+ − 808
ML{*fun prove_intro_tac i preds rules =
+ − 809
SUBPROOF (fn {params, prems, context, ...} =>
+ − 810
let
+ − 811
val (params1, params2) = chop (length params - length preds) params
+ − 812
val (prems1, prems2) = chop (length prems - length rules) prems
+ − 813
in
+ − 814
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ − 815
THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
+ − 816
end) *}
+ − 817
+ − 818
lemma accpartI:
+ − 819
shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+ − 820
apply(tactic {* expand_tac @{thms accpart_def} *})
+ − 821
apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})
+ − 822
done
+ − 823
+ − 824
165
+ − 825
190
+ − 826
text {*
+ − 827
+ − 828
*}
+ − 829
165
+ − 830
ML{*
190
+ − 831
fun intros_tac defs rules preds i ctxt =
165
+ − 832
EVERY1 [ObjectLogic.rulify_tac,
+ − 833
K (rewrite_goals_tac defs),
184
+ − 834
REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
210
+ − 835
prove_intro_tac i preds rules ctxt]*}
165
+ − 836
190
+ − 837
text {*
+ − 838
A test case
+ − 839
*}
+ − 840
+ − 841
ML{*fun intros_tac_test ctxt i =
208
+ − 842
intros_tac eo_defs eo_rules eo_preds i ctxt *}
190
+ − 843
+ − 844
lemma intro0:
+ − 845
shows "even 0"
+ − 846
apply(tactic {* intros_tac_test @{context} 0 *})
+ − 847
done
+ − 848
+ − 849
lemma intro1:
+ − 850
shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+ − 851
apply(tactic {* intros_tac_test @{context} 1 *})
+ − 852
done
+ − 853
+ − 854
lemma intro2:
+ − 855
shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"
+ − 856
apply(tactic {* intros_tac_test @{context} 2 *})
173
+ − 857
done
+ − 858
210
+ − 859
ML{*fun intros rules preds defs lthy =
165
+ − 860
let
+ − 861
fun prove_intro (i, goal) =
+ − 862
Goal.prove lthy [] [] goal
190
+ − 863
(fn {context, ...} => intros_tac defs rules preds i context)
165
+ − 864
in
+ − 865
map_index prove_intro rules
164
+ − 866
end*}
+ − 867
176
+ − 868
text {* main internal function *}
+ − 869
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 870
ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
165
+ − 871
let
+ − 872
val syns = map snd pred_specs
+ − 873
val pred_specs' = map fst pred_specs
+ − 874
val prednames = map fst pred_specs'
+ − 875
val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 876
165
+ − 877
val tyss = map (binder_types o fastype_of) preds
+ − 878
val (attrs, rules) = split_list rule_specs
+ − 879
210
+ − 880
val (defs, lthy') = defns rules preds prednames syns tyss lthy
+ − 881
val ind_rules = inds rules defs preds tyss lthy'
+ − 882
val intro_rules = intros rules preds defs lthy'
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 883
165
+ − 884
val mut_name = space_implode "_" (map Binding.name_of prednames)
+ − 885
val case_names = map (Binding.name_of o fst) attrs
+ − 886
in
+ − 887
lthy'
+ − 888
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ − 889
((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules))
+ − 890
|-> (fn intross => LocalTheory.note Thm.theoremK
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 891
((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross))
165
+ − 892
|>> snd
+ − 893
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 894
((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),
165
+ − 895
[Attrib.internal (K (RuleCases.case_names case_names)),
+ − 896
Attrib.internal (K (RuleCases.consumes 1)),
+ − 897
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
+ − 898
(pred_specs ~~ ind_rules)) #>> maps snd)
+ − 899
|> snd
+ − 900
end*}
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 901
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 902
ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
165
+ − 903
let
183
+ − 904
val ((pred_specs', rule_specs'), _) =
+ − 905
Specification.read_spec pred_specs rule_specs lthy
165
+ − 906
in
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 907
add_inductive pred_specs' rule_specs' lthy
165
+ − 908
end*}
+ − 909
+ − 910
ML{*val spec_parser =
+ − 911
OuterParse.fixes --
+ − 912
Scan.optional
+ − 913
(OuterParse.$$$ "where" |--
+ − 914
OuterParse.!!!
+ − 915
(OuterParse.enum1 "|"
+ − 916
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+ − 917
+ − 918
ML{*val specification =
+ − 919
spec_parser >>
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 920
(fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
165
+ − 921
185
+ − 922
ML{*val _ = OuterSyntax.local_theory "simple_inductive"
+ − 923
"define inductive predicates"
+ − 924
OuterKeyword.thy_decl specification*}
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 925
124
+ − 926
text {*
+ − 927
Things to include at the end:
+ − 928
+ − 929
\begin{itemize}
+ − 930
\item say something about add-inductive-i to return
+ − 931
the rules
+ − 932
\item say that the induction principle is weaker (weaker than
+ − 933
what the standard inductive package generates)
192
+ − 934
\item say that no conformity test is done
210
+ − 935
\item exercise about strong induction principles
+ − 936
\item exercise about the test for the intro rules
124
+ − 937
\end{itemize}
+ − 938
+ − 939
*}
+ − 940
165
+ − 941
simple_inductive
+ − 942
Even and Odd
+ − 943
where
+ − 944
Even0: "Even 0"
+ − 945
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
+ − 946
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
124
+ − 947
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 948
end