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