524 val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma"; |
524 val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma"; |
525 val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary"; |
525 val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary"; |
526 val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition"; |
526 val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition"; |
527 val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal"; |
527 val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal"; |
528 |
528 |
529 in end\<close> |
529 (**)in end(**)\<close> |
530 |
530 |
531 ML \<open> |
531 ML \<open> |
532 local |
532 local |
533 |
533 |
534 val _ = |
534 val _ = |
1415 Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs" |
1415 Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs" |
1416 (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => |
1416 (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => |
1417 Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); |
1417 Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); |
1418 |
1418 |
1419 in end\<close> |
1419 in end\<close> |
|
1420 |
|
1421 ML \<open> (** types of **) |
|
1422 \<close> text \<open> (*prep.for theorem: outcomment (** )local( **) above!*) |
|
1423 long_statement: |
|
1424 Token.T list -> (bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement) * Token.T list |
|
1425 \<close> text \<open> |
|
1426 short_statement: |
|
1427 Token.T list -> (bool * (binding * _d list) * _c list * (string, string, _b) Element.ctxt list * (_a, string) Element.stmt) * Token.T list |
|
1428 \<close> text \<open> |
|
1429 fun theorem spec schematic descr = |
|
1430 Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) |
|
1431 ((long_statement || (*short_statement*)long_statement) >> (fn (long, binding, includes, elems, concl) => |
|
1432 ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) |
|
1433 long Thm.theoremK NONE (K I) binding includes elems concl)) ); |
|
1434 \<close> text \<open> |
|
1435 theorem: Outer_Syntax.command_keyword -> bool -> string -> unit; |
|
1436 val schematic = false; |
|
1437 \<close> ML \<open> |
|
1438 \<close> text \<open> (*Outer_Syntax.local_theory_to_proof' ... :: thy_goal_stmt*) |
|
1439 (fn (long, binding, includes, elems, concl) => |
|
1440 ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) |
|
1441 long Thm.theoremK NONE (K I) binding includes elems concl)) |
|
1442 : |
|
1443 bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement -> bool -> |
|
1444 local_theory(*Proof.context*) -> Proof.state |
|
1445 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^*) |
|
1446 \<close> ML \<open> |
|
1447 \<close> ML \<open> (*Outer_Syntax.command \<^command_keyword>\<open>from\<close> :: prf_chain % "proof" *) |
|
1448 Toplevel.proof o Proof.from_thmss_cmd: |
|
1449 (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition |
|
1450 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) |
|
1451 \<close> ML \<open> |
|
1452 \<close> ML \<open> (**) |
|
1453 \<close> ML \<open> |
|
1454 \<close> ML \<open> (**) |
|
1455 \<close> ML \<open> |
|
1456 \<close> ML \<open> (**) |
|
1457 \<close> ML \<open> |
|
1458 \<close> ML \<open> (**) |
|
1459 \<close> ML \<open> |
|
1460 \<close> ML \<open> (**) |
|
1461 \<close> ML \<open> |
|
1462 \<close> ML \<open> (**) |
|
1463 \<close> ML \<open> |
|
1464 \<close> ML \<open> (**) |
|
1465 \<close> ML \<open> |
|
1466 \<close> ML \<open> (**) |
|
1467 \<close> ML \<open> |
|
1468 \<close> ML \<open> |
|
1469 \<close> |
1420 |
1470 |
1421 |
1471 |
1422 section \<open>Auxiliary lemmas\<close> |
1472 section \<open>Auxiliary lemmas\<close> |
1423 |
1473 |
1424 subsection \<open>Meta-level connectives in assumptions\<close> |
1474 subsection \<open>Meta-level connectives in assumptions\<close> |