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