91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory Ind_Code
176
+ − 2
imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
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
192
+ − 5
datatype trm =
+ − 6
Var "string"
+ − 7
| App "trm" "trm"
+ − 8
| Lam "string" "trm"
+ − 9
+ − 10
simple_inductive
+ − 11
fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)
+ − 12
where
+ − 13
"a\<noteq>b \<Longrightarrow> a\<sharp>Var b"
+ − 14
| "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+ − 15
| "a\<sharp>Lam a t"
+ − 16
| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
+ − 17
+ − 18
164
+ − 19
section {* Code *}
+ − 20
+ − 21
text {*
192
+ − 22
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
@{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
@{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
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
@{text [display] "def ::= 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
+ − 28
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
@{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
@{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}
189
+ − 32
+ − 33
\underline{Induction proof}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
189
+ − 35
After ``objectivication'' we have
+ − 36
@{text "pred zs"} and @{text "orules[preds::=Ps]"}; and have to show
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
@{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<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
+ − 38
Instantiating the @{text "preds"} with @{text "Ps"} gives
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
@{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
189
+ − 41
\underline{Intro proof}
+ − 42
+ − 43
Assume we want to prove the $i$th intro rule.
+ − 44
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};
189
+ − 46
expanding the defs, gives
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
@{text [display]
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
"\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ts"}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
190
+ − 51
By applying as many allI and impI as possible, we have
189
+ − 52
190
+ − 53
@{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
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
@{text "orules"}; and have to show @{text "pred ts"}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
189
+ − 56
the $i$th @{text "orule"} is of the
+ − 57
form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
190
+ − 59
So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)
+ − 60
and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions
+ − 61
@{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.
+ − 62
164
+ − 63
*}
+ − 64
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
text {*
190
+ − 67
First we have to produce for each predicate the definition of the form
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 68
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
@{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
+ − 70
190
+ − 71
and then ``register'' the definitions with Isabelle.
+ − 72
To do the latter, we use the following wrapper for
183
+ − 73
@{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
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
+ − 75
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
164
+ − 78
let
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
val arg = ((predname, syn), (Attrib.empty_binding, trm))
176
+ − 80
val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
164
+ − 81
in
176
+ − 82
(thm, lthy')
164
+ − 83
end*}
+ − 84
+ − 85
text {*
183
+ − 86
It returns the definition (as a theorem) and the local theory in which this definition has
184
+ − 87
been made. In Line 4, @{ML internalK in Thm} is a flag attached to the
183
+ − 88
theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}).
176
+ − 89
These flags just classify theorems and have no significant meaning, except
183
+ − 90
for tools that, for example, find theorems in the theorem database. We also
179
+ − 91
use @{ML empty_binding in Attrib} in Line 3, since the definition does
183
+ − 92
not need to have any theorem attributes. A testcase for this function is
164
+ − 93
*}
+ − 94
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
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
+ − 96
let
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
val (def, lthy') = make_defs arg lthy
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 99
in
179
+ − 100
warning (str_of_thm 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
+ − 101
end *}
164
+ − 102
+ − 103
text {*
184
+ − 104
which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out.
183
+ − 105
Since we are testing the function inside \isacommand{local\_setup}, i.e.~make
+ − 106
changes to the ambient theory, we can query the definition using the usual
+ − 107
command \isacommand{thm}:
179
+ − 108
+ − 109
\begin{isabelle}
+ − 110
\isacommand{thm}~@{text "MyTrue_def"}\\
+ − 111
@{text "> MyTrue \<equiv> True"}
+ − 112
\end{isabelle}
164
+ − 113
190
+ − 114
The next two functions construct the right-hand sides of the definitions, which
+ − 115
are of the form
179
+ − 116
190
+ − 117
@{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
179
+ − 118
190
+ − 119
The variables @{text "zs"} need to be chosen so that they do not occur
184
+ − 120
in the @{text orules} and also be distinct from the @{text "preds"}.
183
+ − 121
184
+ − 122
The first function constructs the term for one particular predicate, say
+ − 123
@{text "pred"}; the number of arguments of this predicate is
190
+ − 124
determined by the number of argument types given in @{text "arg_tys"}.
+ − 125
The other arguments are all @{text "preds"} and the @{text "orules"}.
164
+ − 126
*}
+ − 127
176
+ − 128
ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
164
+ − 129
let
+ − 130
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
+ − 131
+ − 132
val fresh_args =
176
+ − 133
arg_tys
164
+ − 134
|> map (pair "z")
179
+ − 135
|> Variable.variant_frees lthy (preds @ orules)
164
+ − 136
|> map Free
+ − 137
in
+ − 138
list_comb (pred, fresh_args)
+ − 139
|> fold_rev (curry HOLogic.mk_imp) orules
+ − 140
|> fold_rev mk_all preds
+ − 141
|> fold_rev lambda fresh_args
+ − 142
end*}
+ − 143
+ − 144
text {*
184
+ − 145
The function in Line 3 is just a helper function for constructing universal
+ − 146
quantifications. The code in Lines 5 to 9 produces the fresh @{text
190
+ − 147
"zs"}. For this it pairs every argument type with the string
184
+ − 148
@{text [quotes] "z"} (Line 7); then generates variants for all these strings
190
+ − 149
so that they are unique w.r.t.~to the predicates and @{text "orules"} (Line 8);
184
+ − 150
in Line 9 it generates the corresponding variable terms for the unique
+ − 151
strings.
164
+ − 152
183
+ − 153
The unique free variables are applied to the predicate (Line 11) using the
+ − 154
function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
+ − 155
Line 13 we quantify over all predicates; and in line 14 we just abstract
190
+ − 156
over all the @{text "zs"}, i.e.~the fresh arguments of the
+ − 157
predicate. A testcase for this function is
164
+ − 158
*}
+ − 159
179
+ − 160
local_setup %gray{* fn lthy =>
176
+ − 161
let
+ − 162
val orules = [@{prop "even 0"},
+ − 163
@{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
+ − 164
@{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
190
+ − 165
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
176
+ − 166
val pred = @{term "even::nat\<Rightarrow>bool"}
+ − 167
val arg_tys = [@{typ "nat"}]
+ − 168
val def = defs_aux lthy orules preds (pred, arg_tys)
173
+ − 169
in
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 170
warning (Syntax.string_of_term lthy def); lthy
179
+ − 171
end *}
173
+ − 172
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 173
text {*
190
+ − 174
It calls @{ML defs_aux} for the definition of @{text "even"} and prints
+ − 175
out the definition. So we obtain as printout
179
+ − 176
+ − 177
@{text [display]
+ − 178
"\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+ − 179
\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
+ − 180
190
+ − 181
The second function for the definitions has to just iterate the function
184
+ − 182
@{ML defs_aux} over all predicates. The argument @{text "preds"} is again
+ − 183
the the list of predicates as @{ML_type term}s; the argument @{text
+ − 184
"prednames"} is the list of names of the predicates; @{text "arg_tyss"} is
+ − 185
the list of argument-type-lists for each predicate.
164
+ − 186
*}
+ − 187
+ − 188
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
+ − 189
let
+ − 190
val thy = ProofContext.theory_of lthy
+ − 191
val orules = map (ObjectLogic.atomize_term thy) rules
+ − 192
val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss)
+ − 193
in
+ − 194
fold_map make_defs (prednames ~~ syns ~~ defs) lthy
+ − 195
end*}
+ − 196
+ − 197
text {*
184
+ − 198
The user will state the introduction rules using meta-implications and
+ − 199
meta-quanti\-fications. In Line 4, we transform these introduction rules into
+ − 200
the object logic (since definitions cannot be stated with
+ − 201
meta-connectives). To do this transformation we have to obtain the theory
+ − 202
behind the local theory (Line 3); with this theory we can use the function
+ − 203
@{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
+ − 204
to @{ML defs_aux} in Line 5 produces all left-hand sides of the
+ − 205
definitions. The actual definitions are then made in Line 7. The result
190
+ − 206
of the function is a list of theorems and a local theory. A testcase for
+ − 207
this function is
164
+ − 208
*}
+ − 209
179
+ − 210
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
+ − 211
let
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 212
val rules = [@{prop "even 0"},
179
+ − 213
@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ − 214
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 215
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 216
val prednames = [@{binding "even"}, @{binding "odd"}]
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 217
val syns = [NoSyn, NoSyn]
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 218
val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 219
val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 220
in
183
+ − 221
warning (str_of_thms lthy' defs); lthy'
179
+ − 222
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
+ − 223
179
+ − 224
text {*
184
+ − 225
where we feed into the functions all parameters corresponding to
+ − 226
the @{text even}-@{text odd} example. The definitions we obtain
+ − 227
are:
179
+ − 228
183
+ − 229
\begin{isabelle}
+ − 230
\isacommand{thm}~@{text "even_def odd_def"}\\
+ − 231
@{text [break]
+ − 232
"> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+ − 233
> \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
+ − 234
> odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
184
+ − 235
> \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
183
+ − 236
\end{isabelle}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 237
164
+ − 238
184
+ − 239
This completes the code for making the definitions. Next we deal with
+ − 240
the induction principles. Recall that the proof of the induction principle
+ − 241
for @{text "even"} was:
179
+ − 242
*}
176
+ − 243
184
+ − 244
lemma man_ind_principle:
183
+ − 245
assumes prems: "even n"
+ − 246
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
176
+ − 247
apply(atomize (full))
+ − 248
apply(cut_tac prems)
+ − 249
apply(unfold even_def)
+ − 250
apply(drule spec[where x=P])
+ − 251
apply(drule spec[where x=Q])
+ − 252
apply(assumption)
+ − 253
done
+ − 254
179
+ − 255
text {*
190
+ − 256
The code for automating such induction principles has to accomplish two tasks:
184
+ − 257
constructing the induction principles from the given introduction
190
+ − 258
rules and then automatically generating proofs for them using a tactic.
183
+ − 259
+ − 260
The tactic will use the following helper function for instantiating universal
184
+ − 261
quantifiers.
179
+ − 262
*}
176
+ − 263
179
+ − 264
ML{*fun inst_spec ctrm =
+ − 265
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
164
+ − 266
+ − 267
text {*
184
+ − 268
This helper function instantiates the @{text "?x"} in the theorem
+ − 269
@{thm spec} with a given @{ML_type cterm}. Together with the tactic
164
+ − 270
*}
+ − 271
183
+ − 272
ML{*fun inst_spec_tac ctrms =
+ − 273
EVERY' (map (dtac o inst_spec) ctrms)*}
+ − 274
+ − 275
text {*
190
+ − 276
we can use @{ML inst_spec_tac} in the following proof to instantiate the
184
+ − 277
three quantifiers in the assumption.
+ − 278
*}
183
+ − 279
184
+ − 280
lemma
+ − 281
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ − 282
shows "\<forall>x y z. P x y z \<Longrightarrow> True"
176
+ − 283
apply (tactic {*
184
+ − 284
inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
179
+ − 285
txt {*
183
+ − 286
We obtain the goal state
179
+ − 287
+ − 288
\begin{minipage}{\textwidth}
+ − 289
@{subgoals}
+ − 290
\end{minipage}*}
164
+ − 291
(*<*)oops(*>*)
+ − 292
+ − 293
text {*
183
+ − 294
Now the complete tactic for proving the induction principles can
+ − 295
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
+ − 296
*}
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
180
+ − 298
ML %linenosgray{*fun induction_tac defs prems insts =
176
+ − 299
EVERY1 [ObjectLogic.full_atomize_tac,
164
+ − 300
cut_facts_tac prems,
+ − 301
K (rewrite_goals_tac defs),
183
+ − 302
inst_spec_tac insts,
164
+ − 303
assume_tac]*}
+ − 304
179
+ − 305
text {*
190
+ − 306
We only have to give it the definitions, the premise (like @{text "even n"})
+ − 307
and the instantiations as arguments. Compare this with the manual proof
+ − 308
given for the lemma @{thm [source] man_ind_principle}: there is almos a
+ − 309
one-to-one correspondence between the \isacommand{apply}-script and the
+ − 310
@{ML induction_tac}. A testcase for this tactic is the function
179
+ − 311
*}
+ − 312
183
+ − 313
ML{*fun test_tac prems =
+ − 314
let
+ − 315
val defs = [@{thm even_def}, @{thm odd_def}]
+ − 316
val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+ − 317
in
+ − 318
induction_tac defs prems insts
+ − 319
end*}
+ − 320
+ − 321
text {*
184
+ − 322
which indeed proves the induction principle:
183
+ − 323
*}
+ − 324
190
+ − 325
lemma auto_ind_principle:
183
+ − 326
assumes prems: "even n"
+ − 327
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+ − 328
apply(tactic {* test_tac @{thms prems} *})
164
+ − 329
done
+ − 330
165
+ − 331
text {*
184
+ − 332
While the tactic for the induction principle is relatively simple,
+ − 333
it is a bit harder to construct the goals from the introduction
+ − 334
rules the user provides. In general we have to construct for each predicate
183
+ − 335
@{text "pred"} a goal of the form
179
+ − 336
+ − 337
@{text [display]
190
+ − 338
"pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P$ ?zs"}
180
+ − 339
190
+ − 340
where the predicates @{text preds} are replaced in the introduction
+ − 341
rules by new distinct variables written @{text "Ps"}.
184
+ − 342
We also need to generate fresh arguments for the predicate @{text "pred"} in
190
+ − 343
the premise and the @{text "?P"} in the conclusion. Note
+ − 344
that the @{text "?Ps"} and @{text "?zs"} need to be
+ − 345
schematic variables that can be instantiated. This corresponds to what the
+ − 346
@{thm [source] auto_ind_principle} looks like:
+ − 347
+ − 348
\begin{isabelle}
+ − 349
\isacommand{thm}~@{thm [source] auto_ind_principle}\\
+ − 350
@{text "> \<lbrakk>even ?n; ?P 0; \<And>m. ?Q m \<Longrightarrow> ?P (Suc m); \<And>m. ?P m \<Longrightarrow> ?Q (Suc m)\<rbrakk> \<Longrightarrow> ?P ?n"}
+ − 351
\end{isabelle}
+ − 352
+ − 353
We achieve
184
+ − 354
that in two steps.
179
+ − 355
184
+ − 356
The function below expects that the introduction rules are already appropriately
+ − 357
substituted. The argument @{text "srules"} stands for these substituted
+ − 358
rules; @{text cnewpreds} are the certified terms coresponding
190
+ − 359
to the variables @{text "Ps"}; @{text "pred"} is the predicate for
180
+ − 360
which we prove the introduction principle; @{text "newpred"} is its
183
+ − 361
replacement and @{text "tys"} are the argument types of this predicate.
165
+ − 362
*}
+ − 363
190
+ − 364
ML %linenosgray{*fun prove_induction 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
+ − 365
let
190
+ − 366
val zs = replicate (length arg_tys) "z"
179
+ − 367
val (newargnames, lthy') = Variable.variant_fixes zs lthy;
190
+ − 368
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
+ − 369
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 370
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
+ − 371
val goal = Logic.list_implies
183
+ − 372
(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
+ − 373
in
179
+ − 374
Goal.prove lthy' [] [prem] goal
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 375
(fn {prems, ...} => induction_tac defs prems cnewpreds)
179
+ − 376
|> singleton (ProofContext.export lthy' lthy)
+ − 377
end *}
+ − 378
180
+ − 379
text {*
190
+ − 380
In Line 3 we produce names @{text "zs"} for each type in the
183
+ − 381
argument type list. Line 4 makes these names unique and declares them as
+ − 382
\emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In
+ − 383
Line 5 we just construct the terms corresponding to these variables.
+ − 384
The term variables are applied to the predicate in Line 7 (this corresponds
190
+ − 385
to the first premise @{text "pred zs"} of the induction principle).
+ − 386
In Line 8 and 9, we first construct the term @{text "P zs"}
184
+ − 387
and then add the (substituded) introduction rules as premises. In case that
+ − 388
no introduction rules are given, the conclusion of this implication needs
183
+ − 389
to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
+ − 390
mechanism will fail.
180
+ − 391
190
+ − 392
In Line 11 we set up the goal to be proved; in the next line we call the tactic
+ − 393
for proving the induction principle. This tactic expects the definitions, the
184
+ − 394
premise and the (certified) predicates with which the introduction rules
190
+ − 395
have been substituted. The code in these two lines will return a theorem.
+ − 396
However, it is a theorem
184
+ − 397
proved inside the local theory @{text "lthy'"}, where the variables @{text
190
+ − 398
"zs"} are fixed, but free. By exporting this theorem from @{text
+ − 399
"lthy'"} (which contains the @{text "zs"} as free) to @{text
+ − 400
"lthy"} (which does not), we obtain the desired schematic variables.
+ − 401
*}
180
+ − 402
190
+ − 403
local_setup %gray{* fn lthy =>
+ − 404
let
+ − 405
val defs = [@{thm even_def}, @{thm odd_def}]
+ − 406
val srules = [@{prop "P (0::nat)"},
+ − 407
@{prop "\<And>n::nat. Q n \<Longrightarrow> P (Suc n)"},
+ − 408
@{prop "\<And>n::nat. P n \<Longrightarrow> Q (Suc n)"}]
+ − 409
val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+ − 410
val pred = @{term "even::nat\<Rightarrow>bool"}
+ − 411
val newpred = @{term "P::nat\<Rightarrow>bool"}
+ − 412
val arg_tys = [@{typ "nat"}]
+ − 413
val intro =
+ − 414
prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
+ − 415
in
+ − 416
warning (str_of_thm_raw lthy intro); lthy
+ − 417
end *}
184
+ − 418
190
+ − 419
text {*
+ − 420
This prints out:
+ − 421
+ − 422
@{text [display]
+ − 423
" \<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"}
+ − 424
+ − 425
Note that the export from @{text lthy'} to @{text lthy} in Line 13 above
+ − 426
has turned the free, but fixed, @{text "z"} into a schematic
+ − 427
variable @{text "?z"}.
+ − 428
+ − 429
We still have to produce the new predicates with which the introduction
+ − 430
rules are substituted and iterate @{ML prove_induction} over all
+ − 431
predicates. This is what the next function does.
180
+ − 432
*}
165
+ − 433
184
+ − 434
ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy =
164
+ − 435
let
+ − 436
val Ps = replicate (length preds) "P"
183
+ − 437
val (newprednames, lthy') = Variable.variant_fixes Ps lthy
164
+ − 438
183
+ − 439
val thy = ProofContext.theory_of lthy'
164
+ − 440
184
+ − 441
val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
165
+ − 442
val newpreds = map Free (newprednames ~~ tyss')
164
+ − 443
val cnewpreds = map (cterm_of thy) newpreds
184
+ − 444
val srules = map (subst_free (preds ~~ newpreds)) rules
164
+ − 445
+ − 446
in
184
+ − 447
map (prove_induction lthy' defs srules cnewpreds)
+ − 448
(preds ~~ newpreds ~~ arg_tyss)
183
+ − 449
|> ProofContext.export lthy' lthy
165
+ − 450
end*}
+ − 451
184
+ − 452
text {*
+ − 453
In Line 3 we generate a string @{text [quotes] "P"} for each predicate.
+ − 454
In Line 4, we use the same trick as in the previous function, that is making the
190
+ − 455
@{text "Ps"} fresh and declaring them as fixed, but free, in
184
+ − 456
the new local theory @{text "lthy'"}. From the local theory we extract
+ − 457
the ambient theory in Line 6. We need this theory in order to certify
+ − 458
the new predicates. In Line 8 we calculate the types of these new predicates
190
+ − 459
using the given argument types. Next we turn them into terms and subsequently
+ − 460
certify them (Line 9 and 10). We can now produce the substituted introduction rules
+ − 461
(Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate
+ − 462
the proofs for all predicates.
184
+ − 463
From this we obtain a list of theorems. Finally we need to export the
190
+ − 464
fixed variables @{text "Ps"} to obtain the schematic variables
184
+ − 465
(Line 16).
+ − 466
+ − 467
A testcase for this function is
+ − 468
*}
+ − 469
+ − 470
local_setup %gray {* fn lthy =>
+ − 471
let
+ − 472
val rules = [@{prop "even (0::nat)"},
+ − 473
@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ − 474
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+ − 475
val defs = [@{thm even_def}, @{thm odd_def}]
+ − 476
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+ − 477
val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
+ − 478
val ind_thms = inductions rules defs preds tyss lthy
+ − 479
in
190
+ − 480
warning (str_of_thms_raw lthy ind_thms); lthy
+ − 481
end *}
165
+ − 482
176
+ − 483
184
+ − 484
text {*
+ − 485
which prints out
+ − 486
+ − 487
@{text [display]
190
+ − 488
"> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
+ − 489
> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
+ − 490
> odd ?z \<Longrightarrow> ?P1 0
+ − 491
> \<Longrightarrow> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
184
+ − 492
+ − 493
190
+ − 494
Note that now both, the @{text "Ps"} and the @{text "zs"}, are schematic
+ − 495
variables. The numbers have been introduced by the pretty-printer and are
+ − 496
not significant.
184
+ − 497
190
+ − 498
This completes the code for the induction principles. Finally we can prove the
+ − 499
introduction rules. Their proofs are quite a bit more involved. To ease them
+ − 500
somewhat we use the following two helper function.
184
+ − 501
*}
+ − 502
165
+ − 503
ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
+ − 504
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
+ − 505
190
+ − 506
text {*
+ − 507
To see what they do, let us suppose whe have the follwoing three
+ − 508
theorems.
+ − 509
*}
+ − 510
+ − 511
lemma all_elims_test:
+ − 512
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ − 513
shows "\<forall>x y z. P x y z" sorry
+ − 514
+ − 515
lemma imp_elims_test:
+ − 516
fixes A B C::"bool"
+ − 517
shows "A \<longrightarrow> B \<longrightarrow> C" sorry
+ − 518
+ − 519
lemma imp_elims_test':
+ − 520
fixes A::"bool"
+ − 521
shows "A" "B" sorry
+ − 522
+ − 523
text {*
+ − 524
The function @{ML all_elims} takes a list of (certified) terms and instantiates
+ − 525
theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
+ − 526
the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows
+ − 527
+ − 528
@{ML_response_fake [display, gray]
+ − 529
"let
+ − 530
val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+ − 531
val new_thm = all_elims ctrms @{thm all_elims_test}
+ − 532
in
+ − 533
warning (str_of_thm @{context} new_thm)
+ − 534
end"
+ − 535
"P a b c"}
+ − 536
+ − 537
Similarly, the function @{ML imp_elims} eliminates preconditions from implications.
+ − 538
For example
+ − 539
+ − 540
@{ML_response_fake [display, gray]
+ − 541
"warning (str_of_thm @{context}
+ − 542
(imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+ − 543
"C"}
+ − 544
*}
+ − 545
+ − 546
ML {* prems_of *}
+ − 547
ML {* Logic.strip_params *}
+ − 548
ML {* Logic.strip_assums_hyp *}
+ − 549
+ − 550
ML {*
192
+ − 551
fun chop_print_tac m n ctxt thm =
190
+ − 552
let
+ − 553
val [trm] = prems_of thm
+ − 554
val params = map fst (Logic.strip_params trm)
+ − 555
val prems = Logic.strip_assums_hyp trm
192
+ − 556
val (prems1, prems2) = chop (length prems - m) prems;
+ − 557
val (params1, params2) = chop (length params - n) params;
190
+ − 558
val _ = warning (Syntax.string_of_term ctxt trm)
+ − 559
val _ = warning (commas params)
+ − 560
val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
+ − 561
val _ = warning ((commas params1) ^ " | " ^ (commas params2))
+ − 562
val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
+ − 563
(commas (map (Syntax.string_of_term ctxt) prems2)))
+ − 564
in
+ − 565
Seq.single thm
+ − 566
end
+ − 567
*}
+ − 568
192
+ − 569
ML {* METAHYPS *}
+ − 570
+ − 571
ML {*
+ − 572
fun chop_print_tac2 ctxt prems =
+ − 573
let
+ − 574
val _ = warning (commas (map (str_of_thm ctxt) prems))
+ − 575
in
+ − 576
all_tac
+ − 577
end
+ − 578
*}
190
+ − 579
+ − 580
lemma intro1:
+ − 581
shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+ − 582
apply(tactic {* ObjectLogic.rulify_tac 1 *})
+ − 583
apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
+ − 584
apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
192
+ − 585
apply(tactic {* chop_print_tac 3 2 @{context} *})
190
+ − 586
oops
+ − 587
192
+ − 588
ML {*
+ − 589
fun SUBPROOF_test tac ctxt =
+ − 590
SUBPROOF (fn {params, prems, context,...} =>
+ − 591
let
+ − 592
val thy = ProofContext.theory_of context
+ − 593
in
+ − 594
tac (params, prems, context)
+ − 595
THEN Method.insert_tac prems 1
+ − 596
THEN print_tac "SUBPROOF Test"
+ − 597
THEN SkipProof.cheat_tac thy
+ − 598
end) ctxt 1
+ − 599
*}
+ − 600
+ − 601
+ − 602
+ − 603
+ − 604
lemma fresh_App:
+ − 605
shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+ − 606
apply(tactic {* ObjectLogic.rulify_tac 1 *})
+ − 607
apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
+ − 608
apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
+ − 609
oops
+ − 610
(*
+ − 611
apply(tactic {* SUBPROOF_test
+ − 612
(fn (params, prems, ctxt) =>
+ − 613
let
+ − 614
val (prems1, prems2) = chop (length prems - 4) prems;
+ − 615
val (params1, params2) = chop (length params - 1) params;
+ − 616
in
+ − 617
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1
+ − 618
end) @{context} *})
+ − 619
*)
+ − 620
165
+ − 621
ML{*fun subproof2 prem params2 prems2 =
+ − 622
SUBPROOF (fn {prems, ...} =>
+ − 623
let
+ − 624
val prem' = prems MRS prem;
+ − 625
val prem'' =
+ − 626
case prop_of prem' of
+ − 627
_ $ (Const (@{const_name All}, _) $ _) =>
+ − 628
prem' |> all_elims params2
+ − 629
|> imp_elims prems2
+ − 630
| _ => prem';
+ − 631
in
+ − 632
rtac prem'' 1
+ − 633
end)*}
+ − 634
190
+ − 635
text {*
+ − 636
+ − 637
*}
+ − 638
+ − 639
+ − 640
ML %linenosgray{*fun subproof1 rules preds i =
165
+ − 641
SUBPROOF (fn {params, prems, context = ctxt', ...} =>
+ − 642
let
+ − 643
val (prems1, prems2) = chop (length prems - length rules) prems;
+ − 644
val (params1, params2) = chop (length params - length preds) params;
+ − 645
in
+ − 646
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
190
+ − 647
(* applicateion of the i-ith intro rule *)
165
+ − 648
THEN
+ − 649
EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
+ − 650
end)*}
+ − 651
190
+ − 652
text {*
+ − 653
@{text "params1"} are the variables of the rules; @{text "params2"} is
+ − 654
the variables corresponding to the @{text "preds"}.
+ − 655
+ − 656
@{text "prems1"} are the assumption corresponding to the rules;
+ − 657
@{text "prems2"} are the assumptions coming from the allIs/impIs
+ − 658
+ − 659
you instantiate the parameters i-th introduction rule with the parameters
+ − 660
that come from the rule; and you apply it to the goal
+ − 661
+ − 662
this now generates subgoals corresponding to the premisses of this
+ − 663
intro rule
+ − 664
*}
+ − 665
165
+ − 666
ML{*
190
+ − 667
fun intros_tac defs rules preds i ctxt =
165
+ − 668
EVERY1 [ObjectLogic.rulify_tac,
+ − 669
K (rewrite_goals_tac defs),
184
+ − 670
REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
165
+ − 671
subproof1 rules preds i ctxt]*}
+ − 672
190
+ − 673
text {*
+ − 674
A test case
+ − 675
*}
+ − 676
+ − 677
ML{*fun intros_tac_test ctxt i =
173
+ − 678
let
+ − 679
val rules = [@{prop "even (0::nat)"},
190
+ − 680
@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ − 681
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
173
+ − 682
val defs = [@{thm even_def}, @{thm odd_def}]
+ − 683
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+ − 684
in
190
+ − 685
intros_tac defs rules preds i ctxt
+ − 686
end*}
+ − 687
+ − 688
lemma intro0:
+ − 689
shows "even 0"
+ − 690
apply(tactic {* intros_tac_test @{context} 0 *})
+ − 691
done
+ − 692
+ − 693
lemma intro1:
+ − 694
shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+ − 695
apply(tactic {* intros_tac_test @{context} 1 *})
+ − 696
done
+ − 697
+ − 698
lemma intro2:
+ − 699
shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"
+ − 700
apply(tactic {* intros_tac_test @{context} 2 *})
173
+ − 701
done
+ − 702
165
+ − 703
ML{*fun introductions rules preds defs lthy =
+ − 704
let
+ − 705
fun prove_intro (i, goal) =
+ − 706
Goal.prove lthy [] [] goal
190
+ − 707
(fn {context, ...} => intros_tac defs rules preds i context)
165
+ − 708
in
+ − 709
map_index prove_intro rules
164
+ − 710
end*}
+ − 711
176
+ − 712
text {* main internal function *}
+ − 713
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 714
ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
165
+ − 715
let
+ − 716
val syns = map snd pred_specs
+ − 717
val pred_specs' = map fst pred_specs
+ − 718
val prednames = map fst pred_specs'
+ − 719
val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 720
165
+ − 721
val tyss = map (binder_types o fastype_of) preds
+ − 722
val (attrs, rules) = split_list rule_specs
+ − 723
+ − 724
val (defs, lthy') = definitions rules preds prednames syns tyss lthy
+ − 725
val ind_rules = inductions rules defs preds tyss lthy'
+ − 726
val intro_rules = introductions rules preds defs lthy'
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 727
165
+ − 728
val mut_name = space_implode "_" (map Binding.name_of prednames)
+ − 729
val case_names = map (Binding.name_of o fst) attrs
+ − 730
in
+ − 731
lthy'
+ − 732
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ − 733
((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules))
+ − 734
|-> (fn intross => LocalTheory.note Thm.theoremK
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 735
((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross))
165
+ − 736
|>> snd
+ − 737
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),
165
+ − 739
[Attrib.internal (K (RuleCases.case_names case_names)),
+ − 740
Attrib.internal (K (RuleCases.consumes 1)),
+ − 741
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
+ − 742
(pred_specs ~~ ind_rules)) #>> maps snd)
+ − 743
|> snd
+ − 744
end*}
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 745
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 746
ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
165
+ − 747
let
183
+ − 748
val ((pred_specs', rule_specs'), _) =
+ − 749
Specification.read_spec pred_specs rule_specs lthy
165
+ − 750
in
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 751
add_inductive pred_specs' rule_specs' lthy
165
+ − 752
end*}
+ − 753
+ − 754
ML{*val spec_parser =
+ − 755
OuterParse.fixes --
+ − 756
Scan.optional
+ − 757
(OuterParse.$$$ "where" |--
+ − 758
OuterParse.!!!
+ − 759
(OuterParse.enum1 "|"
+ − 760
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+ − 761
+ − 762
ML{*val specification =
+ − 763
spec_parser >>
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 764
(fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
165
+ − 765
185
+ − 766
ML{*val _ = OuterSyntax.local_theory "simple_inductive"
+ − 767
"define inductive predicates"
+ − 768
OuterKeyword.thy_decl specification*}
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 769
124
+ − 770
text {*
+ − 771
Things to include at the end:
+ − 772
+ − 773
\begin{itemize}
+ − 774
\item say something about add-inductive-i to return
+ − 775
the rules
+ − 776
\item say that the induction principle is weaker (weaker than
+ − 777
what the standard inductive package generates)
192
+ − 778
\item say that no conformity test is done
124
+ − 779
\end{itemize}
+ − 780
+ − 781
*}
+ − 782
165
+ − 783
simple_inductive
+ − 784
Even and Odd
+ − 785
where
+ − 786
Even0: "Even 0"
+ − 787
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
+ − 788
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
124
+ − 789
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 790
end