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