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