1279 Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); |
1279 Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); |
1280 |
1280 |
1281 in end\<close> |
1281 in end\<close> |
1282 |
1282 |
1283 |
1283 |
1284 section \<open>Isar attributes\<close> |
|
1285 |
|
1286 attribute_setup tagged = |
|
1287 \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close> |
|
1288 "tagged theorem" |
|
1289 |
|
1290 attribute_setup untagged = |
|
1291 \<open>Scan.lift Args.name >> Thm.untag\<close> |
|
1292 "untagged theorem" |
|
1293 |
|
1294 attribute_setup kind = |
|
1295 \<open>Scan.lift Args.name >> Thm.kind\<close> |
|
1296 "theorem kind" |
|
1297 |
|
1298 attribute_setup THEN = |
|
1299 \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm |
|
1300 >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close> |
|
1301 "resolution with rule" |
|
1302 |
|
1303 attribute_setup OF = |
|
1304 \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close> |
|
1305 "rule resolved with facts" |
|
1306 |
|
1307 attribute_setup rename_abs = |
|
1308 \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => |
|
1309 Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close> |
|
1310 "rename bound variables in abstractions" |
|
1311 |
|
1312 attribute_setup unfolded = |
|
1313 \<open>Attrib.thms >> (fn ths => |
|
1314 Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close> |
|
1315 "unfolded definitions" |
|
1316 |
|
1317 attribute_setup folded = |
|
1318 \<open>Attrib.thms >> (fn ths => |
|
1319 Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close> |
|
1320 "folded definitions" |
|
1321 |
|
1322 attribute_setup consumes = |
|
1323 \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close> |
|
1324 "number of consumed facts" |
|
1325 |
|
1326 attribute_setup constraints = |
|
1327 \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close> |
|
1328 "number of equality constraints" |
|
1329 |
|
1330 attribute_setup case_names = |
|
1331 \<open>Scan.lift (Scan.repeat1 (Args.name -- |
|
1332 Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) [])) |
|
1333 >> (fn cs => |
|
1334 Rule_Cases.cases_hyp_names |
|
1335 (map #1 cs) |
|
1336 (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close> |
|
1337 "named rule cases" |
|
1338 |
|
1339 attribute_setup case_conclusion = |
|
1340 \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close> |
|
1341 "named conclusion of rule cases" |
|
1342 |
|
1343 attribute_setup params = |
|
1344 \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close> |
|
1345 "named rule parameters" |
|
1346 |
|
1347 attribute_setup rule_format = |
|
1348 \<open>Scan.lift (Args.mode "no_asm") |
|
1349 >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close> |
|
1350 "result put into canonical rule format" |
|
1351 |
|
1352 attribute_setup elim_format = |
|
1353 \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close> |
|
1354 "destruct rule turned into elimination rule format" |
|
1355 |
|
1356 attribute_setup no_vars = |
|
1357 \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th => |
|
1358 let |
|
1359 val ctxt = Variable.set_body false (Context.proof_of context); |
|
1360 val ((_, [th']), _) = Variable.import true [th] ctxt; |
|
1361 in th' end))\<close> |
|
1362 "imported schematic variables" |
|
1363 |
|
1364 attribute_setup atomize = |
|
1365 \<open>Scan.succeed Object_Logic.declare_atomize\<close> |
|
1366 "declaration of atomize rule" |
|
1367 |
|
1368 attribute_setup rulify = |
|
1369 \<open>Scan.succeed Object_Logic.declare_rulify\<close> |
|
1370 "declaration of rulify rule" |
|
1371 |
|
1372 attribute_setup rotated = |
|
1373 \<open>Scan.lift (Scan.optional Parse.int 1 |
|
1374 >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close> |
|
1375 "rotated theorem premises" |
|
1376 |
|
1377 attribute_setup defn = |
|
1378 \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close> |
|
1379 "declaration of definitional transformations" |
|
1380 |
|
1381 attribute_setup abs_def = |
|
1382 \<open>Scan.succeed (Thm.rule_attribute [] (fn context => |
|
1383 Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close> |
|
1384 "abstract over free variables of definitional theorem" |
|
1385 |
|
1386 |
|
1387 section \<open>Further content for the Pure theory\<close> |
1284 section \<open>Further content for the Pure theory\<close> |
1388 |
1285 |
1389 subsection \<open>Meta-level connectives in assumptions\<close> |
1286 subsection \<open>Meta-level connectives in assumptions\<close> |
1390 |
1287 |
1391 lemma meta_mp: |
1288 lemma meta_mp: |