src/Pure/ML/ml_thms.ML
author wenzelm
Wed, 19 Oct 2011 17:03:07 +0200
changeset 45198 f579dab96734
parent 43560 d1650e3720fd
child 45592 8baa0b7f3f66
permissions -rw-r--r--
proper source positions for @{lemma};
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_thms.ML
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     3
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     4
Isar theorem values within ML.
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     5
*)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     6
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     7
signature ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     8
sig
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     9
  val the_thms: Proof.context -> int -> thm list
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    10
  val the_thm: Proof.context -> int -> thm
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    11
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    12
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    13
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    14
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    15
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    16
(* auxiliary facts table *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    17
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    18
structure Aux_Facts = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    19
(
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    20
  type T = thm list Inttab.table;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    21
  fun init _ = Inttab.empty;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    22
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    23
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    24
val put_thms = Aux_Facts.map o Inttab.update;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    25
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    26
fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    27
fun the_thm ctxt name = the_single (the_thms ctxt name);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    28
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    29
fun thm_bind kind a i =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    30
  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    31
    " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    32
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    33
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    34
(* fact references *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    35
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    36
fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33700
diff changeset
    37
  (fn _ => scan >> (fn ths => fn background =>
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    38
    let
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    39
      val i = serial ();
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    40
      val (a, background') = background
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    41
        |> ML_Antiquote.variant kind ||> put_thms (i, ths);
41486
82c1e348bc18 reverted 08240feb69c7 -- breaks positions of reports;
wenzelm
parents: 41376
diff changeset
    42
      val ml = (thm_bind kind a i, "Isabelle." ^ a);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    43
    in (K ml, background') end));
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    44
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    45
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    46
  Context.>> (Context.map_theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    47
   (thm_antiq "thm" (Attrib.thm >> single) #>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    48
    thm_antiq "thms" Attrib.thms));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    49
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    50
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    51
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    52
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    53
val and_ = Args.$$$ "and";
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27521
diff changeset
    54
val by = Args.$$$ "by";
45198
f579dab96734 proper source positions for @{lemma};
wenzelm
parents: 43560
diff changeset
    55
val goal = Scan.unless (by || and_) Args.name_source;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    56
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    57
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    58
  Context.>> (Context.map_theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    59
   (ML_Context.add_antiq (Binding.name "lemma")
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    60
    (fn _ => Args.context -- Args.mode "open" --
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    61
        Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    62
          (by |-- Method.parse -- Scan.option Method.parse)) >>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    63
      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    64
        let
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    65
          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    66
          val i = serial ();
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    67
          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    68
          fun after_qed res goal_ctxt =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    69
            put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    70
          val ctxt' = ctxt
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    71
            |> Proof.theorem NONE after_qed propss
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    72
            |> Proof.global_terminal_proof methods;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    73
          val (a, background') = background
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    74
            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    75
          val ml =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    76
            (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    77
        in (K ml, background') end))));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    78
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    79
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    80