src/Pure/ML/ml_thms.ML
author wenzelm
Fri Apr 27 22:47:30 2012 +0200 (2012-04-27 ago)
changeset 47815 43f677b3ae91
parent 45592 8baa0b7f3f66
child 48776 37cd53e69840
permissions -rw-r--r--
clarified signature;
     1 (*  Title:      Pure/ML/ml_thms.ML
     2     Author:     Makarius
     3 
     4 Attribute source and theorem values within ML.
     5 *)
     6 
     7 signature ML_THMS =
     8 sig
     9   val the_attributes: Proof.context -> int -> Args.src list
    10   val the_thms: Proof.context -> int -> thm list
    11   val the_thm: Proof.context -> int -> thm
    12 end;
    13 
    14 structure ML_Thms: ML_THMS =
    15 struct
    16 
    17 (* auxiliary data *)
    18 
    19 structure Data = Proof_Data
    20 (
    21   type T = Args.src list Inttab.table * thm list Inttab.table;
    22   fun init _ = (Inttab.empty, Inttab.empty);
    23 );
    24 
    25 val put_attributes = Data.map o apfst o Inttab.update;
    26 fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
    27 
    28 val put_thms = Data.map o apsnd o Inttab.update;
    29 
    30 fun the_thms ctxt name = the (Inttab.lookup (snd (Data.get ctxt)) name);
    31 fun the_thm ctxt name = the_single (the_thms ctxt name);
    32 
    33 
    34 (* attribute source *)
    35 
    36 val _ =
    37   Context.>> (Context.map_theory
    38     (ML_Context.add_antiq (Binding.name "attributes")
    39       (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background =>
    40         let
    41           val thy = Proof_Context.theory_of background;
    42 
    43           val i = serial ();
    44           val srcs = map (Attrib.intern_src thy) raw_srcs;
    45           val _ = map (Attrib.attribute background) srcs;
    46           val (a, background') = background
    47             |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
    48           val ml =
    49             ("val " ^ a ^ " = ML_Thms.the_attributes (ML_Context.the_local_context ()) " ^
    50               string_of_int i ^ ";\n", "Isabelle." ^ a);
    51         in (K ml, background') end))));
    52 
    53 
    54 (* fact references *)
    55 
    56 fun thm_bind kind a i =
    57   "val " ^ a ^ " = ML_Thms.the_" ^ kind ^
    58     " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
    59 
    60 fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
    61   (fn _ => scan >> (fn ths => fn background =>
    62     let
    63       val i = serial ();
    64       val (a, background') = background
    65         |> ML_Antiquote.variant kind ||> put_thms (i, ths);
    66       val ml = (thm_bind kind a i, "Isabelle." ^ a);
    67     in (K ml, background') end));
    68 
    69 val _ =
    70   Context.>> (Context.map_theory
    71    (thm_antiq "thm" (Attrib.thm >> single) #>
    72     thm_antiq "thms" Attrib.thms));
    73 
    74 
    75 (* ad-hoc goals *)
    76 
    77 val and_ = Args.$$$ "and";
    78 val by = Args.$$$ "by";
    79 val goal = Scan.unless (by || and_) Args.name_source;
    80 
    81 val _ =
    82   Context.>> (Context.map_theory
    83    (ML_Context.add_antiq (Binding.name "lemma")
    84     (fn _ => Args.context -- Args.mode "open" --
    85         Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
    86           (by |-- Method.parse -- Scan.option Method.parse)) >>
    87       (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
    88         let
    89           val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    90           val i = serial ();
    91           val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    92           fun after_qed res goal_ctxt =
    93             put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
    94           val ctxt' = ctxt
    95             |> Proof.theorem NONE after_qed propss
    96             |> Proof.global_terminal_proof methods;
    97           val (a, background') = background
    98             |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    99           val ml =
   100             (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
   101         in (K ml, background') end))));
   102 
   103 end;
   104