src/Pure/Tools/invoke.ML
author wenzelm
Tue Nov 21 18:07:37 2006 +0100 (2006-11-21)
changeset 21440 807a39221a58
parent 20893 c99f79910ae8
child 21483 e4be91feca50
permissions -rw-r--r--
notes: proper kind;
wenzelm@19813
     1
(*  Title:      Pure/Tools/invoke.ML
wenzelm@19813
     2
    ID:         $Id$
wenzelm@19813
     3
    Author:     Makarius
wenzelm@19813
     4
wenzelm@19813
     5
Schematic invocation of locale expression in proof context.
wenzelm@19813
     6
*)
wenzelm@19813
     7
wenzelm@19813
     8
signature INVOKE =
wenzelm@19813
     9
sig
wenzelm@19849
    10
  val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
wenzelm@19849
    11
    (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
wenzelm@19849
    12
  val invoke_i: string * attribute list -> Locale.expr -> term option list ->
wenzelm@19849
    13
    (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
wenzelm@19813
    14
end;
wenzelm@19813
    15
wenzelm@19813
    16
structure Invoke: INVOKE =
wenzelm@19813
    17
struct
wenzelm@19813
    18
wenzelm@19849
    19
wenzelm@19813
    20
(* invoke *)
wenzelm@19813
    21
wenzelm@19813
    22
local
wenzelm@19813
    23
wenzelm@19849
    24
fun gen_invoke prep_att prep_expr prep_terms add_fixes
wenzelm@19849
    25
    (prfx, raw_atts) raw_expr raw_insts fixes int state =
wenzelm@19813
    26
  let
wenzelm@19813
    27
    val _ = Proof.assert_forward_or_chain state;
wenzelm@19813
    28
    val thy = Proof.theory_of state;
wenzelm@19813
    29
wenzelm@19849
    30
    val more_atts = map (prep_att thy) raw_atts;
wenzelm@19813
    31
    val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
wenzelm@19849
    32
wenzelm@19849
    33
    val prems = maps Element.prems_of elems;
wenzelm@19849
    34
    val params = maps Element.params_of elems;
wenzelm@19849
    35
    val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
wenzelm@19813
    36
wenzelm@19849
    37
    val prems' = map Logic.varify prems;
wenzelm@19849
    38
    val params' = map (Logic.varify o Free) params;
wenzelm@19849
    39
    val types' = map (Logic.varifyT o TFree) types;
wenzelm@19849
    40
wenzelm@19849
    41
    val state' = state
wenzelm@19849
    42
      |> Proof.begin_block
wenzelm@19849
    43
      |> Proof.map_context (snd o add_fixes fixes);
wenzelm@19849
    44
    val ctxt' = Proof.context_of state';
wenzelm@19849
    45
wenzelm@19849
    46
    val raw_insts' = zip_options params' raw_insts
wenzelm@19813
    47
      handle Library.UnequalLengths => error "Too many instantiations";
wenzelm@19813
    48
    val insts = map #1 raw_insts' ~~
wenzelm@19849
    49
      prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts');
wenzelm@19849
    50
    val inst_rules =
wenzelm@19849
    51
      replicate (length types') Drule.termI @
wenzelm@19849
    52
      map (fn t =>
wenzelm@19849
    53
        (case AList.lookup (op =) insts t of
wenzelm@19849
    54
          SOME u => Drule.mk_term (Thm.cterm_of thy u)
wenzelm@19849
    55
        | NONE => Drule.termI)) params';
wenzelm@19813
    56
wenzelm@19813
    57
    val propp =
wenzelm@19849
    58
      [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
wenzelm@19849
    59
       (("", []), map (rpair [] o Logic.mk_term) params'),
wenzelm@19849
    60
       (("", []), map (rpair [] o Element.mark_witness) prems')];
wenzelm@19849
    61
    fun after_qed results =
wenzelm@19849
    62
      Proof.end_block #>
wenzelm@20305
    63
      Proof.map_context (fn ctxt =>
wenzelm@19849
    64
        let
wenzelm@19849
    65
          val ([res_types, res_params, res_prems], ctxt'') =
wenzelm@20218
    66
            fold_burrow (apfst snd oo Variable.import false) results ctxt';
wenzelm@19849
    67
wenzelm@19849
    68
          val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
wenzelm@19849
    69
          val params'' = map (Thm.term_of o Drule.dest_term) res_params;
wenzelm@19849
    70
          val elems' = elems |> map (Element.inst_ctxt thy
wenzelm@19849
    71
            (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
wenzelm@19868
    72
          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
wenzelm@20266
    73
          val notes =
wenzelm@20266
    74
            maps (Element.facts_of thy) elems'
wenzelm@20266
    75
            |> Element.satisfy_facts prems''
wenzelm@20893
    76
            |> Element.export_facts ctxt'' ctxt
wenzelm@19849
    77
            |> Attrib.map_facts (Attrib.attribute_i thy)
wenzelm@20266
    78
            |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
wenzelm@19849
    79
        in
wenzelm@19849
    80
          ctxt
wenzelm@19849
    81
          |> ProofContext.sticky_prefix prfx
wenzelm@19849
    82
          |> ProofContext.qualified_names
wenzelm@21440
    83
          |> (snd o ProofContext.note_thmss_i "" notes)
wenzelm@19849
    84
          |> ProofContext.restore_naming ctxt
wenzelm@20305
    85
        end) #>
wenzelm@20305
    86
      Proof.put_facts NONE #> Seq.single;
wenzelm@19813
    87
  in
wenzelm@19849
    88
    state'
wenzelm@19868
    89
    |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
wenzelm@19813
    90
      "invoke" NONE after_qed propp
wenzelm@19813
    91
    |> Element.refine_witness
wenzelm@19813
    92
    |> Seq.hd
wenzelm@19813
    93
    |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules)))))))
wenzelm@19813
    94
    |> Seq.hd
wenzelm@19813
    95
  end;
wenzelm@19813
    96
wenzelm@19813
    97
(* FIXME *)
wenzelm@19813
    98
fun read_terms ctxt args =
wenzelm@19813
    99
  #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args)
wenzelm@19897
   100
  |> Variable.polymorphic ctxt;
wenzelm@19813
   101
wenzelm@19813
   102
(* FIXME *)
wenzelm@19813
   103
fun cert_terms ctxt args = map fst args;
wenzelm@19813
   104
wenzelm@19813
   105
in
wenzelm@19813
   106
wenzelm@19849
   107
fun invoke x = gen_invoke Attrib.attribute Locale.read_expr read_terms ProofContext.add_fixes x;
wenzelm@19849
   108
fun invoke_i x = gen_invoke (K I) Locale.cert_expr cert_terms ProofContext.add_fixes_i x;
wenzelm@19813
   109
wenzelm@19813
   110
end;
wenzelm@19813
   111
wenzelm@19813
   112
wenzelm@19813
   113
(* concrete syntax *)
wenzelm@19813
   114
wenzelm@19813
   115
local structure P = OuterParse and K = OuterKeyword in
wenzelm@19813
   116
wenzelm@19813
   117
val invokeP =
wenzelm@19813
   118
  OuterSyntax.command "invoke"
wenzelm@19813
   119
    "schematic invocation of locale expression in proof context"
wenzelm@19813
   120
    (K.tag_proof K.prf_goal)
wenzelm@19849
   121
    (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes
wenzelm@19849
   122
      >> (fn (((name, expr), insts), fixes) =>
wenzelm@19849
   123
          Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
wenzelm@19813
   124
wenzelm@19813
   125
val _ = OuterSyntax.add_parsers [invokeP];
wenzelm@19813
   126
wenzelm@19813
   127
end;
wenzelm@19813
   128
wenzelm@19813
   129
end;