author  wenzelm 
Fri, 19 Jan 2007 22:08:08 +0100  
changeset 22101  6d13239d5f52 
parent 21584  22c9392de970 
child 22568  ed7aa5a350ef 
permissions  rwrr 
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 > 
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 

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 

19849  24 
fun gen_invoke prep_att prep_expr prep_terms add_fixes 
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  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  32 

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 [])); 

19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

36 

19849  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 

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  49 
prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts'); 
50 
val inst_rules = 

51 
replicate (length types') Drule.termI @ 

52 
map (fn t => 

53 
(case AList.lookup (op =) insts t of 

54 
SOME u => Drule.mk_term (Thm.cterm_of thy u) 

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  58 
[(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'), 
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 #> 

20305  63 
Proof.map_context (fn ctxt => 
19849  64 
let 
65 
val ([res_types, res_params, res_prems], ctxt'') = 

20218
be3bfb0699ba
Variable.import(T): result includes fixed types/terms;
wenzelm
parents:
19919
diff
changeset

66 
fold_burrow (apfst snd oo Variable.import false) results ctxt'; 
19849  67 

68 
val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types; 

69 
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

70 
val inst = Element.morph_ctxt (Element.inst_morphism thy 
19849  71 
(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

72 
val elems' = map inst elems; 
19868  73 
val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems; 
20266  74 
val notes = 
75 
maps (Element.facts_of thy) elems' 

76 
> Element.satisfy_facts prems'' 

21584  77 
> Element.generalize_facts ctxt'' ctxt 
19849  78 
> Attrib.map_facts (Attrib.attribute_i thy) 
20266  79 
> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs)); 
19849  80 
in 
81 
ctxt 

82 
> ProofContext.sticky_prefix prfx 

83 
> ProofContext.qualified_names 

21440  84 
> (snd o ProofContext.note_thmss_i "" notes) 
19849  85 
> ProofContext.restore_naming ctxt 
20305  86 
end) #> 
87 
Proof.put_facts NONE #> Seq.single; 

19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

88 
in 
19849  89 
state' 
19868  90 
> 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

91 
"invoke" NONE after_qed propp 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

92 
> Element.refine_witness 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

93 
> Seq.hd 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

94 
> 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

95 
> Seq.hd 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

96 
end; 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

97 

b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

98 
(* FIXME *) 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

99 
fun read_terms ctxt args = 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

100 
#1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args) 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19868
diff
changeset

101 
> Variable.polymorphic ctxt; 
19813
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 cert_terms ctxt args = map fst args; 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

105 

b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

106 
in 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

107 

19849  108 
fun invoke x = gen_invoke Attrib.attribute Locale.read_expr read_terms ProofContext.add_fixes x; 
109 
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

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 

b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

118 
val invokeP = 
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 
19849  123 
>> (fn (((name, expr), insts), fixes) => 
124 
Toplevel.print o Toplevel.proof' (invoke name 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 
val _ = OuterSyntax.add_parsers [invokeP]; 
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; 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

129 

b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

130 
end; 