added lemma antiquotation
authorhaftmann
Tue Apr 29 19:55:02 2008 +0200 (2008-04-29)
changeset 2676278ed28528ca6
parent 26761 190da765a628
child 26763 fba4995cb0f9
added lemma antiquotation
NEWS
src/Pure/Isar/method.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Tue Apr 29 15:25:50 2008 +0200
     1.2 +++ b/NEWS	Tue Apr 29 19:55:02 2008 +0200
     1.3 @@ -98,6 +98,16 @@
     1.4  situations.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* Antiquotation "lemma" takes a proposition and a simple method text as argument
    1.10 +and asserts that the proposition is provable by the corresponding method
    1.11 +invocation.  Prints text of proposition, as does antiquotation "prop".  A simple
    1.12 +method text is either a method name or a method name plus (optional) method
    1.13 +arguments in parentheses, mimicing the conventions known from Isar proof text.
    1.14 +Useful for illustration of presented theorems by particular examples.
    1.15 +
    1.16 +
    1.17  *** HOL ***
    1.18  
    1.19  * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations
     2.1 --- a/src/Pure/Isar/method.ML	Tue Apr 29 15:25:50 2008 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Tue Apr 29 19:55:02 2008 +0200
     2.3 @@ -79,6 +79,7 @@
     2.4    val method_setup: bstring -> string * Position.T -> string -> theory -> theory
     2.5    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     2.6      -> src -> Proof.context -> 'a * Proof.context
     2.7 +  val simple_text: Args.T list -> text * Args.T list
     2.8    val simple_args: (Args.T list -> 'a * Args.T list)
     2.9      -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
    2.10    val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
    2.11 @@ -467,6 +468,11 @@
    2.12  
    2.13  fun syntax scan = Args.context_syntax "method" scan;
    2.14  
    2.15 +val simple_text = (Args.$$$ "(" |-- Args.name
    2.16 +    -- Scan.repeat (Scan.one (fn x => not (Args.string_of x = ")"))) --| Args.$$$ ")"
    2.17 +  || Args.name -- Scan.succeed [])
    2.18 +  >> (fn (name, args) => Source (Args.src ((name, args), Position.none)));
    2.19 +
    2.20  fun simple_args scan f src ctxt : method =
    2.21    fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
    2.22  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Apr 29 15:25:50 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Apr 29 19:55:02 2008 +0200
     3.3 @@ -456,6 +456,13 @@
     3.4      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
     3.5    in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
     3.6  
     3.7 +fun pretty_fact ctxt (prop, method_text) =
     3.8 +  let
     3.9 +    val _ = ctxt
    3.10 +      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
    3.11 +      |> Proof.global_terminal_proof (method_text, NONE);
    3.12 +  in pretty_term ctxt prop end;
    3.13 +
    3.14  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    3.15  
    3.16  fun pretty_term_style ctxt (name, t) =
    3.17 @@ -517,6 +524,7 @@
    3.18   [("thm", args Attrib.thms (output_list pretty_thm)),
    3.19    ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
    3.20    ("prop", args Args.prop (output pretty_term)),
    3.21 +  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact)),
    3.22    ("term", args Args.term (output pretty_term)),
    3.23    ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
    3.24    ("term_type", args Args.term (output pretty_term_typ)),