--- a/src/Pure/Tools/invoke.ML Wed Jan 21 15:26:02 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,127 +0,0 @@
-(* Title: Pure/Tools/invoke.ML
- Author: Makarius
-
-Schematic invocation of locale expression in proof context.
-*)
-
-signature INVOKE =
-sig
- val invoke: string * Attrib.src list -> Old_Locale.expr -> string option list ->
- (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val invoke_i: string * attribute list -> Old_Locale.expr -> term option list ->
- (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
-end;
-
-structure Invoke: INVOKE =
-struct
-
-
-(* invoke *)
-
-local
-
-fun gen_invoke prep_att prep_expr parse_term add_fixes
- (prfx, raw_atts) raw_expr raw_insts fixes int state =
- let
- val thy = Proof.theory_of state;
- val _ = Proof.assert_forward_or_chain state;
- val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
-
- val more_atts = map (prep_att thy) raw_atts;
- val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
-
- val prems = maps Element.prems_of elems;
- val params = maps Element.params_of elems;
- val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
-
- val prems' = map Logic.varify prems;
- val params' = map (Logic.varify o Free) params;
- val types' = map (Logic.varifyT o TFree) types;
-
- val state' = state
- |> Proof.enter_forward
- |> Proof.begin_block
- |> Proof.map_context (snd o add_fixes fixes);
- val ctxt' = Proof.context_of state';
-
- val raw_insts' = zip_options params' raw_insts
- handle Library.UnequalLengths => error "Too many instantiations";
-
- fun prep_inst (t, u) =
- TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);
- val insts = map #1 raw_insts' ~~
- Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));
- val inst_rules =
- replicate (length types') Drule.termI @
- map (fn t =>
- (case AList.lookup (op =) insts t of
- SOME u => Drule.mk_term (Thm.cterm_of thy u)
- | NONE => Drule.termI)) params';
-
- val propp =
- [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
- ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
- ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
- fun after_qed results =
- Proof.end_block #>
- Proof.map_context (fn ctxt =>
- let
- val ([res_types, res_params, res_prems], ctxt'') =
- fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';
-
- val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
- val params'' = map (Thm.term_of o Drule.dest_term) res_params;
- val inst = Element.morph_ctxt (Element.inst_morphism thy
- (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
- val elems' = map inst elems;
- val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
- val notes =
- maps (Element.facts_of thy) elems'
- |> Element.satisfy_facts prems''
- |> Element.generalize_facts ctxt'' ctxt
- |> Attrib.map_facts (Attrib.attribute_i thy)
- |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
- in
- ctxt
- |> ProofContext.sticky_prefix prfx
- |> ProofContext.qualified_names
- |> (snd o ProofContext.note_thmss_i "" notes)
- |> ProofContext.restore_naming ctxt
- end) #>
- Proof.put_facts NONE;
- in
- state'
- |> Proof.chain_facts chain_facts
- |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
- "invoke" NONE after_qed propp
- |> Element.refine_witness
- |> Seq.hd
- |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),
- Position.none))
- |> Seq.hd
- end;
-
-in
-
-fun invoke x =
- gen_invoke Attrib.attribute Old_Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;
-fun invoke_i x = gen_invoke (K I) Old_Locale.cert_expr (K I) ProofContext.add_fixes_i x;
-
-end;
-
-
-(* concrete syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ =
- OuterSyntax.command "invoke"
- "schematic invocation of locale expression in proof context"
- (K.tag_proof K.prf_goal)
- (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
- >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
- Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
-
-end;
-
-end;