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