author  haftmann 
Mon, 12 Jun 2006 09:14:41 +0200  
changeset 19852  b06db8e4476b 
parent 19849  d96a15bb2d88 
child 19868  e93ffc043dfd 
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 #> 

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'; 

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; 

70 
val elems' = elems > map (Element.inst_ctxt thy 

71 
(Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params''))); 

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

72 

19849  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 

19852  80 
val _ = print notes; 
19849  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); 

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

93 
in 
19849  94 
state' 
19813
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

95 
> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_schematic_i 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

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

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

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

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

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

101 
end; 
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 read_terms ctxt args = 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

105 
#1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args) 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

106 
> ProofContext.polymorphic ctxt; 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

107 

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

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

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

112 

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

115 

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

116 
end; 
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 

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

119 
(* concrete syntax *) 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

120 

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

121 
local structure P = OuterParse and K = OuterKeyword in 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

122 

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

123 
val invokeP = 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

124 
OuterSyntax.command "invoke" 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

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

126 
(K.tag_proof K.prf_goal) 
19849  127 
(P.opt_thm_name ":"  P.locale_expr  P.locale_insts  P.for_fixes 
128 
>> (fn (((name, expr), insts), fixes) => 

129 
Toplevel.print o Toplevel.proof' (invoke name expr insts fixes))); 

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

130 

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

131 
val _ = OuterSyntax.add_parsers [invokeP]; 
b051be997d50
Schematic invocation of locale expression in proof context.
wenzelm
parents:
diff
changeset

132 

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

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

134 

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

135 
end; 