author | haftmann |
Wed, 17 Sep 2008 07:32:04 +0200 | |
changeset 28256 | 4e7f7d52f855 |
parent 28083 | 103d9282a946 |
child 28965 | 1de908189869 |
permissions | -rw-r--r-- |
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 | 10 |
val invoke: string * Attrib.src list -> Locale.expr -> string option list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
11 |
(Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
19849 | 12 |
val invoke_i: string * attribute list -> Locale.expr -> term option list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
13 |
(Name.binding * 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 | 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 |
|
24693 | 24 |
fun gen_invoke prep_att prep_expr parse_term add_fixes |
19849 | 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 |
24743 | 27 |
val thy = Proof.theory_of state; |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
28 |
val _ = Proof.assert_forward_or_chain state; |
24743 | 29 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
30 |
|
19849 | 31 |
val more_atts = map (prep_att thy) raw_atts; |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
32 |
val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy); |
19849 | 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 [])); |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
37 |
|
19849 | 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 |
|
24743 | 43 |
|> Proof.enter_forward |
19849 | 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 |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
49 |
handle Library.UnequalLengths => error "Too many instantiations"; |
24693 | 50 |
|
51 |
fun prep_inst (t, u) = |
|
52 |
TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u); |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
53 |
val insts = map #1 raw_insts' ~~ |
24693 | 54 |
Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts')); |
19849 | 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'; |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
61 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
62 |
val propp = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
63 |
[((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'), |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
64 |
((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'), |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
65 |
((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')]; |
19849 | 66 |
fun after_qed results = |
67 |
Proof.end_block #> |
|
20305 | 68 |
Proof.map_context (fn ctxt => |
19849 | 69 |
let |
70 |
val ([res_types, res_params, res_prems], ctxt'') = |
|
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
22101
diff
changeset
|
71 |
fold_burrow (apfst snd oo Variable.import_thms false) results ctxt'; |
19849 | 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; |
|
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21440
diff
changeset
|
75 |
val inst = Element.morph_ctxt (Element.inst_morphism thy |
19849 | 76 |
(Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params''))); |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21440
diff
changeset
|
77 |
val elems' = map inst elems; |
19868 | 78 |
val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems; |
20266 | 79 |
val notes = |
80 |
maps (Element.facts_of thy) elems' |
|
81 |
|> Element.satisfy_facts prems'' |
|
21584 | 82 |
|> Element.generalize_facts ctxt'' ctxt |
19849 | 83 |
|> Attrib.map_facts (Attrib.attribute_i thy) |
20266 | 84 |
|> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs)); |
19849 | 85 |
in |
86 |
ctxt |
|
87 |
|> ProofContext.sticky_prefix prfx |
|
88 |
|> ProofContext.qualified_names |
|
21440 | 89 |
|> (snd o ProofContext.note_thmss_i "" notes) |
19849 | 90 |
|> ProofContext.restore_naming ctxt |
20305 | 91 |
end) #> |
92 |
Proof.put_facts NONE #> Seq.single; |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
93 |
in |
19849 | 94 |
state' |
24743 | 95 |
|> Proof.chain_facts chain_facts |
19868 | 96 |
|> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
97 |
"invoke" NONE after_qed propp |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
98 |
|> Element.refine_witness |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
99 |
|> Seq.hd |
23351 | 100 |
|> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))), |
101 |
Position.none)) |
|
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
102 |
|> Seq.hd |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
103 |
end; |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
104 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
105 |
in |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
106 |
|
22769 | 107 |
fun invoke x = |
24693 | 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; |
|
19813
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 |
end; |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
112 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
113 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
114 |
(* concrete syntax *) |
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 |
local structure P = OuterParse and K = OuterKeyword in |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
117 |
|
24867 | 118 |
val _ = |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
119 |
OuterSyntax.command "invoke" |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
120 |
"schematic invocation of locale expression in proof context" |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
121 |
(K.tag_proof K.prf_goal) |
22101 | 122 |
(SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
123 |
>> (fn ((((name, atts), expr), (insts, _)), fixes) => |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24867
diff
changeset
|
124 |
Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes))); |
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
125 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
126 |
end; |
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
127 |
|
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset
|
128 |
end; |