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