162 |
162 |
163 val global_transfer = gen_transfer I; |
163 val global_transfer = gen_transfer I; |
164 val local_transfer = gen_transfer ProofContext.theory_of; |
164 val local_transfer = gen_transfer ProofContext.theory_of; |
165 |
165 |
166 |
166 |
|
167 (* COMP *) |
|
168 |
|
169 fun comp B (x, A) = (x, A COMP B); |
|
170 |
|
171 fun gen_COMP thm = syntax (thm >> comp); |
|
172 val global_COMP = gen_COMP global_thm; |
|
173 val local_COMP = gen_COMP local_thm; |
|
174 |
|
175 |
167 (* RS *) |
176 (* RS *) |
168 |
177 |
169 fun resolve (i, B) (x, A) = (x, A RSN (i, B)); |
178 fun resolve (i, B) (x, A) = (x, A RSN (i, B)); |
170 |
179 |
171 fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve); |
180 fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve); |
248 (* pure_attributes *) |
257 (* pure_attributes *) |
249 |
258 |
250 val pure_attributes = |
259 val pure_attributes = |
251 [("tag", (gen_tag, gen_tag), "tag theorem"), |
260 [("tag", (gen_tag, gen_tag), "tag theorem"), |
252 ("untag", (gen_untag, gen_untag), "untag theorem"), |
261 ("untag", (gen_untag, gen_untag), "untag theorem"), |
|
262 ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"), |
253 ("RS", (global_RS, local_RS), "resolve with rule"), |
263 ("RS", (global_RS, local_RS), "resolve with rule"), |
254 ("APP", (global_APP, local_APP), "resolve rule with"), |
264 ("APP", (global_APP, local_APP), "resolve rule with"), |
255 ("where", (global_where, local_where), "named instantiation of theorem"), |
265 ("where", (global_where, local_where), "named instantiation of theorem"), |
256 ("with", (global_with, local_with), "positional instantiation of theorem"), |
266 ("with", (global_with, local_with), "positional instantiation of theorem"), |
257 ("standard", (standard, standard), "put theorem into standard form"), |
267 ("standard", (standard, standard), "put theorem into standard form"), |