author  wenzelm 
Sun, 26 Nov 2006 18:07:31 +0100  
changeset 21533  bada5ac1216a 
parent 21498  6382c3a1e7cf 
child 21570  f20f9304ab48 
permissions  rwrr 
20894  1 
(* Title: Pure/Isar/theory_target.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

5 
Common theory targets. 

6 
*) 

7 

8 
signature THEORY_TARGET = 

9 
sig 

21006  10 
val peek: local_theory > string option 
20962  11 
val begin: bstring > Proof.context > local_theory 
20894  12 
val init: xstring option > theory > local_theory 
13 
val init_i: string option > theory > local_theory 

14 
end; 

15 

16 
structure TheoryTarget: THEORY_TARGET = 

17 
struct 

18 

19 
(** locale targets **) 

20 

21006  21 
(* context data *) 
22 

23 
structure Data = ProofDataFun 

24 
( 

25 
val name = "Isar/theory_target"; 

26 
type T = string option; 

27 
fun init _ = NONE; 

28 
fun print _ _ = (); 

29 
); 

30 

31 
val _ = Context.add_setup Data.init; 

32 
val peek = Data.get; 

33 

34 

20894  35 
(* pretty *) 
36 

37 
fun pretty loc ctxt = 

38 
let 

39 
val thy = ProofContext.theory_of ctxt; 

40 
val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); 

41 
val assumes = map (fn A => (("", []), [(A, [])])) (Assumption.assms_of ctxt); 

42 
val elems = 

43 
(if null fixes then [] else [Element.Fixes fixes]) @ 

44 
(if null assumes then [] else [Element.Assumes assumes]); 

45 
in 

20984  46 
if loc = "" then 
47 
[Pretty.block 

48 
[Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), 

49 
Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] 

50 
else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)] 

51 
else 

52 
[Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =") 

53 
(map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] 

20894  54 
end; 
55 

56 

57 
(* consts *) 

58 

59 
fun consts loc depends decls lthy = 

60 
let 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

61 
val is_loc = loc <> ""; 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

62 
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); 
20894  63 

64 
fun const ((c, T), mx) thy = 

65 
let 

66 
val U = map #2 xs > T; 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

67 
val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

68 
val thy' = Sign.add_consts_authentic [(c, U, Syntax.unlocalize_mixfix is_loc mx)] thy; 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

69 
in (((c, mx), t), thy') end; 
20894  70 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

71 
val (abbrs, lthy') = lthy > LocalTheory.theory_result (fold_map const decls); 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

72 
val defs = abbrs > map (fn (x, t) => (x, (("", []), t))); 
20894  73 
in 
74 
lthy' 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

75 
> K is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

76 
> LocalDefs.add_defs defs >> map (apsnd snd) 
20894  77 
end; 
78 

79 

80 
(* axioms *) 

81 

82 
local 

83 

84 
fun add_axiom hyps (name, prop) thy = 

85 
let 

86 
val name' = if name = "" then "axiom_" ^ serial_string () else name; 

87 
val prop' = Logic.list_implies (hyps, prop); 

88 
val thy' = thy > Theory.add_axioms_i [(name', prop')]; 

89 
val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name')); 

90 
val prems = map (Thm.assume o Thm.cterm_of thy') hyps; 

91 
in (Drule.implies_elim_list axm prems, thy') end; 

92 

93 
in 

94 

21433  95 
fun axioms kind specs lthy = 
20915  96 
let 
97 
val hyps = Assumption.assms_of lthy; 

98 
fun axiom ((name, atts), props) thy = thy 

99 
> fold_map (add_axiom hyps) (PureThy.name_multi name props) 

100 
> (fn ths => pair ((name, atts), [(ths, [])])); 

101 
in 

102 
lthy 

20984  103 
> fold (fold Variable.declare_term o snd) specs 
20915  104 
> LocalTheory.theory_result (fold_map axiom specs) 
21433  105 
> LocalTheory.notes kind 
20915  106 
end; 
20894  107 

108 
end; 

109 

110 

111 
(* defs *) 

112 

113 
local 

114 

115 
fun add_def (name, prop) = 

116 
Theory.add_defs_i false false [(name, prop)] #> 

117 
(fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy)); 

118 

119 
fun expand_defs lthy = 

120 
Drule.term_rule (ProofContext.theory_of lthy) 

121 
(Assumption.export false lthy (LocalTheory.target_of lthy)); 

122 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

123 
infix also; 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

124 
fun eq1 also eq2 = Thm.transitive eq1 eq2; 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

125 

20894  126 
in 
127 

21433  128 
fun defs kind args lthy = 
20894  129 
let 
21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

130 
fun def ((c, mx), ((name, atts), rhs)) lthy1 = 
20894  131 
let 
21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

132 
val name' = Thm.def_name_optional c name; 
20894  133 
val T = Term.fastype_of rhs; 
21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

134 

20894  135 
val rhs' = expand_defs lthy1 rhs; 
136 
val depends = member (op =) (Term.add_frees rhs' []); 

137 
val defined = filter_out depends (Term.add_frees rhs []); 

138 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

139 
val ([(lhs, local_def)], lthy2) = lthy1 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

140 
> LocalTheory.consts depends [((c, T), mx)]; 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

141 
val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def)); 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

142 

20894  143 
val rhs_conv = rhs 
144 
> Thm.cterm_of (ProofContext.theory_of lthy1) 

145 
> Tactic.rewrite true (map_filter (LocalDefs.find_def lthy1 o #1) defined); 

146 

147 
val (global_def, lthy3) = lthy2 

148 
> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs'))); 

149 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

150 
val eq = 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

151 
local_def (*c == loc.c xs*) 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

152 
also global_def (*... == rhs'*) 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

153 
also Thm.symmetric rhs_conv; (*... == rhs*) 
20894  154 
in ((lhs, ((name', atts), [([eq], [])])), lthy3) end; 
155 

156 
val ((lhss, facts), lthy') = lthy > fold_map def args >> split_list; 

21433  157 
val (res, lthy'') = lthy' > LocalTheory.notes kind facts; 
20894  158 
in (lhss ~~ map (apsnd the_single) res, lthy'') end; 
159 

160 
end; 

161 

162 

163 
(* notes *) 

164 

21433  165 
fun context_notes kind facts lthy = 
20894  166 
let 
167 
val facts' = facts 

168 
> Element.export_standard_facts lthy lthy 

169 
> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy)); 

170 
in 

171 
lthy 

21433  172 
> ProofContext.set_stmt true 
20894  173 
> ProofContext.qualified_names 
21433  174 
> ProofContext.note_thmss_i kind facts' 
20894  175 
> ProofContext.restore_naming lthy 
21433  176 
> ProofContext.restore_stmt lthy 
20894  177 
end; 
178 

21433  179 
fun theory_notes keep_atts kind facts lthy = lthy > LocalTheory.theory (fn thy => 
20894  180 
let 
181 
val facts' = facts 

182 
> Element.export_standard_facts lthy (ProofContext.init thy) 

20915  183 
> Attrib.map_facts (if keep_atts then Attrib.attribute_i thy else K I); 
20894  184 
in 
185 
thy 

186 
> Sign.qualified_names 

21433  187 
> PureThy.note_thmss_i kind facts' > #2 
20894  188 
> Sign.restore_naming thy 
189 
end); 

190 

21433  191 
fun locale_notes loc kind facts lthy = lthy > LocalTheory.target (fn ctxt => 
192 
#2 (Locale.add_thmss loc kind (Element.export_standard_facts lthy ctxt facts) ctxt)); 

20894  193 

21433  194 
fun notes "" kind facts = theory_notes true kind facts #> context_notes kind facts 
195 
 notes loc kind facts = theory_notes false kind facts #> 

196 
locale_notes loc kind facts #> context_notes kind facts; 

20894  197 

198 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

199 
(* target declarations *) 
20894  200 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

201 
fun decl _ "" f = 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

202 
LocalTheory.theory (Context.theory_map (f Morphism.identity)) #> 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

203 
LocalTheory.target (Context.proof_map (f Morphism.identity)) 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

204 
 decl add loc f = 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

205 
LocalTheory.target (add loc (Context.proof_map o f)); 
20894  206 

21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21467
diff
changeset

207 
val type_syntax = decl Locale.add_type_syntax; 
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21467
diff
changeset

208 
val term_syntax = decl Locale.add_term_syntax; 
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21467
diff
changeset

209 
val declaration = decl Locale.add_declaration; 
20894  210 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

211 
fun target_morphism loc lthy = 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

212 
ProofContext.export_standard_morphism lthy (LocalTheory.target_of lthy) $> 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

213 
Morphism.name_morphism (NameSpace.qualified loc); 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

214 

bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

215 
fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy) 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

216 
 target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy); 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

217 

20894  218 

219 
(* init and exit *) 

220 

21293  221 
fun begin loc = 
222 
Data.put (if loc = "" then NONE else SOME loc) #> 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

223 
LocalTheory.init (NameSpace.base loc) 
21293  224 
{pretty = pretty loc, 
225 
consts = consts loc, 

226 
axioms = axioms, 

227 
defs = defs, 

228 
notes = notes loc, 

21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21467
diff
changeset

229 
type_syntax = type_syntax loc, 
21293  230 
term_syntax = term_syntax loc, 
231 
declaration = declaration loc, 

21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

232 
target_morphism = target_morphism loc, 
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

233 
target_name = target_name loc, 
21293  234 
reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc), 
21533
bada5ac1216a
simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents:
21498
diff
changeset

235 
exit = LocalTheory.target_of}; 
20894  236 

20962  237 
fun init_i NONE thy = begin "" (ProofContext.init thy) 
238 
 init_i (SOME loc) thy = begin loc (Locale.init loc thy); 

20894  239 

21276  240 
fun init (SOME "") thy = init_i NONE thy 
241 
 init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; 

20894  242 

243 
end; 