src/Pure/Tools/invoke.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24743 cfcdb9817c49
child 28083 103d9282a946
permissions -rw-r--r--
simplified interfaces for outer syntax;
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@24693
    24
fun gen_invoke prep_att prep_expr parse_term add_fixes
wenzelm@19849
    25
    (prfx, raw_atts) raw_expr raw_insts fixes int state =
wenzelm@19813
    26
  let
wenzelm@24743
    27
    val thy = Proof.theory_of state;
wenzelm@19813
    28
    val _ = Proof.assert_forward_or_chain state;
wenzelm@24743
    29
    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
wenzelm@19813
    30
wenzelm@19849
    31
    val more_atts = map (prep_att thy) raw_atts;
wenzelm@19813
    32
    val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
wenzelm@19849
    33
wenzelm@19849
    34
    val prems = maps Element.prems_of elems;
wenzelm@19849
    35
    val params = maps Element.params_of elems;
wenzelm@19849
    36
    val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
wenzelm@19813
    37
wenzelm@19849
    38
    val prems' = map Logic.varify prems;
wenzelm@19849
    39
    val params' = map (Logic.varify o Free) params;
wenzelm@19849
    40
    val types' = map (Logic.varifyT o TFree) types;
wenzelm@19849
    41
wenzelm@19849
    42
    val state' = state
wenzelm@24743
    43
      |> Proof.enter_forward
wenzelm@19849
    44
      |> Proof.begin_block
wenzelm@19849
    45
      |> Proof.map_context (snd o add_fixes fixes);
wenzelm@19849
    46
    val ctxt' = Proof.context_of state';
wenzelm@19849
    47
wenzelm@19849
    48
    val raw_insts' = zip_options params' raw_insts
wenzelm@19813
    49
      handle Library.UnequalLengths => error "Too many instantiations";
wenzelm@24693
    50
wenzelm@24693
    51
    fun prep_inst (t, u) =
wenzelm@24693
    52
      TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);
wenzelm@19813
    53
    val insts = map #1 raw_insts' ~~
wenzelm@24693
    54
      Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));
wenzelm@19849
    55
    val inst_rules =
wenzelm@19849
    56
      replicate (length types') Drule.termI @
wenzelm@19849
    57
      map (fn t =>
wenzelm@19849
    58
        (case AList.lookup (op =) insts t of
wenzelm@19849
    59
          SOME u => Drule.mk_term (Thm.cterm_of thy u)
wenzelm@19849
    60
        | NONE => Drule.termI)) params';
wenzelm@19813
    61
wenzelm@19813
    62
    val propp =
wenzelm@19849
    63
      [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
wenzelm@19849
    64
       (("", []), map (rpair [] o Logic.mk_term) params'),
wenzelm@19849
    65
       (("", []), map (rpair [] o Element.mark_witness) prems')];
wenzelm@19849
    66
    fun after_qed results =
wenzelm@19849
    67
      Proof.end_block #>
wenzelm@20305
    68
      Proof.map_context (fn ctxt =>
wenzelm@19849
    69
        let
wenzelm@19849
    70
          val ([res_types, res_params, res_prems], ctxt'') =
wenzelm@22568
    71
            fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';
wenzelm@19849
    72
wenzelm@19849
    73
          val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
wenzelm@19849
    74
          val params'' = map (Thm.term_of o Drule.dest_term) res_params;
wenzelm@21483
    75
          val inst = Element.morph_ctxt (Element.inst_morphism thy
wenzelm@19849
    76
            (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
wenzelm@21483
    77
          val elems' = map inst elems;
wenzelm@19868
    78
          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
wenzelm@20266
    79
          val notes =
wenzelm@20266
    80
            maps (Element.facts_of thy) elems'
wenzelm@20266
    81
            |> Element.satisfy_facts prems''
wenzelm@21584
    82
            |> Element.generalize_facts ctxt'' ctxt
wenzelm@19849
    83
            |> Attrib.map_facts (Attrib.attribute_i thy)
wenzelm@20266
    84
            |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
wenzelm@19849
    85
        in
wenzelm@19849
    86
          ctxt
wenzelm@19849
    87
          |> ProofContext.sticky_prefix prfx
wenzelm@19849
    88
          |> ProofContext.qualified_names
wenzelm@21440
    89
          |> (snd o ProofContext.note_thmss_i "" notes)
wenzelm@19849
    90
          |> ProofContext.restore_naming ctxt
wenzelm@20305
    91
        end) #>
wenzelm@20305
    92
      Proof.put_facts NONE #> Seq.single;
wenzelm@19813
    93
  in
wenzelm@19849
    94
    state'
wenzelm@24743
    95
    |> Proof.chain_facts chain_facts
wenzelm@19868
    96
    |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
wenzelm@19813
    97
      "invoke" NONE after_qed propp
wenzelm@19813
    98
    |> Element.refine_witness
wenzelm@19813
    99
    |> Seq.hd
wenzelm@23351
   100
    |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),
wenzelm@23351
   101
      Position.none))
wenzelm@19813
   102
    |> Seq.hd
wenzelm@19813
   103
  end;
wenzelm@19813
   104
wenzelm@19813
   105
in
wenzelm@19813
   106
wenzelm@22769
   107
fun invoke x =
wenzelm@24693
   108
  gen_invoke Attrib.attribute Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;
wenzelm@24693
   109
fun invoke_i x = gen_invoke (K I) Locale.cert_expr (K I) ProofContext.add_fixes_i x;
wenzelm@19813
   110
wenzelm@19813
   111
end;
wenzelm@19813
   112
wenzelm@19813
   113
wenzelm@19813
   114
(* concrete syntax *)
wenzelm@19813
   115
wenzelm@19813
   116
local structure P = OuterParse and K = OuterKeyword in
wenzelm@19813
   117
wenzelm@24867
   118
val _ =
wenzelm@19813
   119
  OuterSyntax.command "invoke"
wenzelm@19813
   120
    "schematic invocation of locale expression in proof context"
wenzelm@19813
   121
    (K.tag_proof K.prf_goal)
wenzelm@22101
   122
    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
ballarin@22658
   123
      >> (fn (((name, expr), (insts, _)), fixes) =>
wenzelm@19849
   124
          Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
wenzelm@19813
   125
wenzelm@19813
   126
end;
wenzelm@19813
   127
wenzelm@19813
   128
end;