author  wenzelm 
Tue, 16 Jul 2002 18:41:00 +0200  
changeset 13375  7cbf2dea46d0 
parent 13336  1bd21b082466 
child 13394  b39347206719 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
12958  3 
Author: Markus Wenzel, LMU/TU München 
11896  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5 

12058  6 
Locales  Isar proof contexts as metalevel predicates, with local 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

7 
syntax and implicit structures. 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

8 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

9 
Draws some basic ideas from Florian Kammüller's original version of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

10 
locales, but uses the richer infrastructure of Isar instead of the raw 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

11 
metalogic. Furthermore, we provide structured import of contexts 
13375  12 
(with merge and rename operations), well as typeinference of the 
13 
signature parts, and predicate definitions of the specification text. 

11896  14 
*) 
15 

16 
signature LOCALE = 

17 
sig 

12046  18 
type context 
19 
datatype ('typ, 'term, 'fact, 'att) elem = 

12058  20 
Fixes of (string * 'typ option * mixfix option) list  
12046  21 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
22 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  23 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
24 
datatype expr = 

25 
Locale of string  

26 
Rename of expr * string option list  

27 
Merge of expr list 

28 
val empty: expr 

29 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

30 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr 

12046  31 
type 'att element 
32 
type 'att element_i 

33 
type locale 

34 
val intern: Sign.sg > xstring > string 

12014  35 
val cond_extern: Sign.sg > string > xstring 
12502  36 
val the_locale: theory > string > locale 
12273  37 
val attribute: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 
38 
> ('typ, 'term, 'thm, context attribute) elem_expr 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

39 
val locale_facts: theory > xstring > thm list 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

40 
val locale_facts_i: theory > string > thm list 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

41 
val read_context_statement: xstring option > context attribute element list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

42 
(string * (string list * string list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

43 
string option * context * context * (term * (term list * term list)) list list 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

44 
val cert_context_statement: string option > context attribute element_i list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

45 
(term * (term list * term list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

46 
string option * context * context * (term * (term list * term list)) list list 
12758  47 
val print_locales: theory > unit 
48 
val print_locale: theory > expr > context attribute element list > unit 

13375  49 
val add_locale: bstring option option > bstring 
50 
> expr > context attribute element list > theory > theory 

51 
val add_locale_i: bstring option option > bstring 

52 
> expr > context attribute element_i list > theory > theory 

12958  53 
val smart_have_thmss: string > (string * 'a) Library.option > 
54 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 

55 
theory > theory * (bstring * thm list) list 

12711  56 
val have_thmss: string > xstring > 
57 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 

58 
theory > theory * (bstring * thm list) list 

59 
val have_thmss_i: string > string > 

60 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 

61 
theory > theory * (bstring * thm list) list 

12958  62 
val add_thmss: string > ((string * thm list) * context attribute list) list > 
13375  63 
theory * context > (theory * context) * (string * thm list) list 
11896  64 
val setup: (theory > theory) list 
65 
end; 

12839  66 

12289  67 
structure Locale: LOCALE = 
11896  68 
struct 
69 

13375  70 

12273  71 
(** locale elements and expressions **) 
11896  72 

12014  73 
type context = ProofContext.context; 
11896  74 

12046  75 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  76 
Fixes of (string * 'typ option * mixfix option) list  
12046  77 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
78 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  79 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
80 

81 
datatype expr = 

82 
Locale of string  

83 
Rename of expr * string option list  

84 
Merge of expr list; 

11896  85 

12273  86 
val empty = Merge []; 
87 

88 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

89 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr; 

90 

91 
type 'att element = (string, string, string, 'att) elem_expr; 

92 
type 'att element_i = (typ, term, thm list, 'att) elem_expr; 

12070  93 

94 
type locale = 

12289  95 
{import: expr, (*dynamic import*) 
96 
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) 

12839  97 
params: (string * typ option) list * string list}; (*all vs. local params*) 
12063  98 

13308  99 
fun make_locale import elems params = 
100 
{import = import, elems = elems, params = params}: locale; 

12063  101 

11896  102 

103 

104 
(** theory data **) 

105 

106 
structure LocalesArgs = 

107 
struct 

12014  108 
val name = "Isar/locales"; 
12063  109 
type T = NameSpace.T * locale Symtab.table; 
11896  110 

12063  111 
val empty = (NameSpace.empty, Symtab.empty); 
112 
val copy = I; 

12118  113 
val prep_ext = I; 
12289  114 

115 
(*joining of locale elements: only facts may be added later!*) 

13308  116 
fun join ({import, elems, params}: locale, {elems = elems', ...}: locale) = 
117 
Some (make_locale import (gen_merge_lists eq_snd elems elems') params); 

12273  118 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  119 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
120 

12273  121 
fun print _ (space, locs) = 
122 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 

12014  123 
> Pretty.writeln; 
11896  124 
end; 
125 

126 
structure LocalesData = TheoryDataFun(LocalesArgs); 

127 
val print_locales = LocalesData.print; 

128 

12289  129 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
130 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

131 

12277  132 

133 
(* access locales *) 

134 

12063  135 
fun declare_locale name = 
136 
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name])))); 

11896  137 

12273  138 
fun put_locale name loc = LocalesData.map (apsnd (fn locs => Symtab.update ((name, loc), locs))); 
12063  139 
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name); 
11896  140 

12014  141 
fun the_locale thy name = 
142 
(case get_locale thy name of 

143 
Some loc => loc 

144 
 None => error ("Unknown locale " ^ quote name)); 

11896  145 

12046  146 

12277  147 
(* diagnostics *) 
12273  148 

12277  149 
fun err_in_locale ctxt msg ids = 
150 
let 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

151 
val sign = ProofContext.sign_of ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

152 
fun prt_id (name, parms) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

153 
[Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; 
12289  154 
val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  155 
val err_msg = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

156 
if forall (equal "" o #1) ids then msg 
12502  157 
else msg ^ "\n" ^ Pretty.string_of (Pretty.block 
158 
(Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); 

159 
in raise ProofContext.CONTEXT (err_msg, ctxt) end; 

12063  160 

12277  161 

162 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

163 
(** primitives **) 
12046  164 

12277  165 
(* renaming *) 
12263  166 

167 
fun rename ren x = if_none (assoc_string (ren, x)) x; 

168 

169 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 

170 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

171 
 rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) 

172 
 rename_term _ a = a; 

173 

174 
fun rename_thm ren th = 

175 
let 

176 
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; 

177 
val cert = Thm.cterm_of sign; 

12502  178 
val (xs, Ts) = Library.split_list (foldl Term.add_frees ([], prop :: hyps)); 
12263  179 
val xs' = map (rename ren) xs; 
180 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

181 
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); 

182 
in 

183 
if xs = xs' then th 

184 
else 

185 
th 

186 
> Drule.implies_intr_list (map cert hyps) 

187 
> Drule.forall_intr_list (cert_frees xs) 

188 
> Drule.forall_elim_list (cert_vars xs) 

189 
> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') 

190 
> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) 

191 
end; 

192 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

193 
fun rename_elem ren (Fixes fixes) = Fixes (fixes > map (fn (x, T, mx) => 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

194 
let val x' = rename ren x in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

195 
if x = x' then (x, T, mx) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

196 
else (x', T, if mx = None then mx else Some Syntax.NoSyn) (*drop syntax*) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

197 
end)) 
12263  198 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
199 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

200 
 rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) => 

201 
(rename_term ren t, map (rename_term ren) ps))) defs) 

12273  202 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  203 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

204 
fun rename_facts prfx elem = 
12307  205 
let 
12323  206 
fun qualify (arg as ((name, atts), x)) = 
13375  207 
if prfx = "" orelse name = "" orelse NameSpace.is_qualified name then arg 
208 
else ((NameSpace.pack [prfx, name], atts), x); 

12307  209 
in 
210 
(case elem of 

211 
Fixes fixes => Fixes fixes 

212 
 Assumes asms => Assumes (map qualify asms) 

213 
 Defines defs => Defines (map qualify defs) 

214 
 Notes facts => Notes (map qualify facts)) 

215 
end; 

216 

12263  217 

12502  218 
(* type instantiation *) 
219 

220 
fun inst_type [] T = T 

221 
 inst_type env T = Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T; 

222 

223 
fun inst_term [] t = t 

224 
 inst_term env t = Term.map_term_types (inst_type env) t; 

225 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

226 
fun inst_thm _ [] th = th 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

227 
 inst_thm ctxt env th = 
12502  228 
let 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

229 
val sign = ProofContext.sign_of ctxt; 
12575  230 
val cert = Thm.cterm_of sign; 
231 
val certT = Thm.ctyp_of sign; 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

232 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
12579  233 
val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []); 
234 
val env' = filter (fn ((a, _), _) => a mem_string tfrees) env; 

12502  235 
in 
236 
if null env' then th 

237 
else 

238 
th 

239 
> Drule.implies_intr_list (map cert hyps) 

12575  240 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  241 
> (fn (th', al) => th' > 
242 
Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), [])) 

243 
> (fn th'' => Drule.implies_elim_list th'' 

244 
(map (Thm.assume o cert o inst_term env') hyps)) 

245 
end; 

246 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

247 
fun inst_elem _ env (Fixes fixes) = 
12502  248 
Fixes (map (fn (x, T, mx) => (x, apsome (inst_type env) T, mx)) fixes) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

249 
 inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
12502  250 
(inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

251 
 inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 
12502  252 
(inst_term env t, map (inst_term env) ps))) defs) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

253 
 inst_elem ctxt env (Notes facts) = 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

254 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  255 

256 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

257 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

258 
(** structured contexts: rename + merge + implicit type instantiation **) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

259 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

260 
(* parameter types *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

261 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

262 
fun frozen_tvars ctxt Ts = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

263 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

264 
val tvars = rev (foldl Term.add_tvarsT ([], Ts)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

265 
val tfrees = map TFree 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

266 
(Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

267 
in map #1 tvars ~~ tfrees end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

268 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

269 
fun unify_frozen ctxt maxidx Ts Us = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

270 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

271 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
12546  272 
fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T) 
273 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

274 
 unify (env, _) = env; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

275 
fun paramify (i, None) = (i, None) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

276 
 paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

277 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

278 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  279 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

280 
val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

281 
val Vs = map (apsome (Envir.norm_type unifier)) Us'; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

282 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs)); 
12532  283 
in map (apsome (Envir.norm_type unifier')) Vs end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

284 

12730  285 
fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

286 
fun param_types ps = mapfilter (fn (_, None) => None  (x, Some T) => Some (x, T)) ps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

287 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

288 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

289 
(* flatten expressions *) 
11896  290 

12510  291 
local 
12502  292 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

293 
fun unique_parms ctxt elemss = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

294 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

295 
val param_decls = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

296 
flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

297 
> Symtab.make_multi > Symtab.dest; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

298 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

299 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

300 
Some (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

301 
(map (apsnd (map fst)) ids) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

302 
 None => map (apfst (apsnd #1)) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

303 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

304 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

305 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  306 
let 
307 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

308 
val maxidx = length raw_parmss; 

309 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

310 

311 
fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

312 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

313 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  314 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

315 
fun unify T ((env, maxidx), U) = Type.unify tsig (env, maxidx) (U, T) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

316 
handle Type.TUNIFY => raise TYPE ("unify_parms: failed to unify types", [U, T], []); 
12502  317 
fun unify_list (envir, T :: Us) = foldl (unify T) (envir, Us) 
318 
 unify_list (envir, []) = envir; 

319 
val (unifier, _) = foldl unify_list 

320 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 

321 

322 
val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms); 

323 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); 

324 

325 
fun inst_parms (i, ps) = 

326 
foldr Term.add_typ_tfrees (mapfilter snd ps, []) 

327 
> mapfilter (fn (a, S) => 

328 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 

329 
in if T = TFree (a, S) then None else Some ((a, S), T) end); 

330 
in map inst_parms idx_parmss end; 

331 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

332 
in 
12502  333 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

334 
fun unify_elemss _ _ [] = [] 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

335 
 unify_elemss _ [] [elems] = [elems] 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

336 
 unify_elemss ctxt fixed_parms elemss = 
12502  337 
let 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

338 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss); 
13308  339 
fun inst (((name, ps), elems), env) = 
340 
((name, map (apsnd (apsome (inst_type env))) ps), (map (inst_elem ctxt env) elems)); 

12839  341 
in map inst (elemss ~~ envs) end; 
12502  342 

12575  343 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  344 
let 
345 
val thy = ProofContext.theory_of ctxt; 

12263  346 

12289  347 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
348 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

12273  349 
 renaming [] _ = [] 
12289  350 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
351 
commas (map (fn None => "_"  Some x => quote x) xs)); 

352 

353 
fun rename_parms ren (name, ps) = 

354 
let val ps' = map (rename ren) ps in 

355 
(case duplicates ps' of [] => (name, ps') 

356 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 

357 
end; 

12263  358 

12273  359 
fun identify ((ids, parms), Locale name) = 
12289  360 
let 
361 
val {import, params, ...} = the_locale thy name; 

362 
val ps = map #1 (#1 params); 

363 
in 

12273  364 
if (name, ps) mem ids then (ids, parms) 
12277  365 
else 
12289  366 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
367 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  368 
end 
369 
 identify ((ids, parms), Rename (e, xs)) = 

370 
let 

371 
val (ids', parms') = identify (([], []), e); 

12839  372 
val ren = renaming xs parms' 
373 
handle ERROR_MESSAGE msg => err_in_locale ctxt msg ids'; 

12289  374 
val ids'' = distinct (map (rename_parms ren) ids'); 
375 
val parms'' = distinct (flat (map #2 ids'')); 

376 
in (merge_lists ids ids'', merge_lists parms parms'') end 

12273  377 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  378 

12307  379 
fun eval (name, xs) = 
12273  380 
let 
13308  381 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  382 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  383 
val (params', elems') = 
384 
if null ren then ((ps, qs), map #1 elems) 

12502  385 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  386 
map (rename_elem ren o #1) elems); 
13375  387 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  388 
in ((name, params'), elems'') end; 
12307  389 

12575  390 
val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents); 
391 
val raw_elemss = unique_parms ctxt (map eval idents); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

392 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  393 
in (prev_idents @ idents, elemss) end; 
12046  394 

12510  395 
end; 
396 

12070  397 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

398 
(* activate elements *) 
12273  399 

12510  400 
local 
401 

13375  402 
fun activate_elem _ (ctxt, Fixes fixes) = (ctxt > ProofContext.add_fixes fixes, []) 
403 
 activate_elem _ (ctxt, Assumes asms) = 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

404 
ctxt > ProofContext.fix_frees (flat (map (map #1 o #2) asms)) 
12839  405 
> ProofContext.assume_i ProofContext.export_assume asms 
13375  406 
> apsnd (map (rpair false)) 
407 
 activate_elem _ (ctxt, Defines defs) = 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

408 
ctxt > ProofContext.assume_i ProofContext.export_def 
13375  409 
(defs > map (fn ((name, atts), (t, ps)) => 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

410 
let val (c, t') = ProofContext.cert_def ctxt t 
13375  411 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) 
412 
> apsnd (map (rpair false)) 

413 
 activate_elem b (ctxt, Notes facts) = 

414 
ctxt > ProofContext.have_thmss_i facts > apsnd (map (rpair b)); 

12263  415 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

416 
fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt => 
13375  417 
foldl_map (activate_elem (name = "")) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) => 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

418 
err_in_locale ctxt msg [(name, map fst ps)]); 
12502  419 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

420 
fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

421 
let 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

422 
val elems = map (prep_facts ctxt) raw_elems; 
13375  423 
val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), elems) ctxt); 
13336  424 
in (ctxt', (((name, ps), elems), facts)) end); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

425 

12546  426 
in 
427 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

428 
fun activate_facts prep_facts ctxt_elemss = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

429 
let val (ctxt', (elemss', factss)) = apsnd split_list (activate_elemss prep_facts ctxt_elemss) 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

430 
in (ctxt', (elemss', flat factss)) end; 
12546  431 

12510  432 
end; 
433 

12307  434 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

435 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

436 
(** prepare context elements **) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

437 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

438 
(* expressions *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

439 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

440 
fun intern_expr sg (Locale xname) = Locale (intern sg xname) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

441 
 intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

442 
 intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

443 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

444 

12546  445 
(* attributes *) 
446 

447 
local fun read_att attrib (x, srcs) = (x, map attrib srcs) in 

448 

449 
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) 

450 
 attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) 

451 
 attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) 

452 
 attribute attrib (Elem (Notes facts)) = 

453 
Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) 

454 
 attribute _ (Expr expr) = Expr expr; 

455 

456 
end; 

457 

458 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

459 
(* parameters *) 
12502  460 

461 
local 

462 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

463 
fun prep_fixes prep_vars ctxt fixes = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

464 
let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

465 
in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

466 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

467 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

468 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

469 
fun read_fixes x = prep_fixes ProofContext.read_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

470 
fun cert_fixes x = prep_fixes ProofContext.cert_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

471 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

472 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

473 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

474 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

475 
(* propositions and bindings *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

476 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

477 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

478 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

479 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

480 

12839  481 
local 
482 

12727  483 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  484 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  485 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
486 
 declare_int_elem (ctxt, _) = (ctxt, []); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

487 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

488 
fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = 
12575  489 
(ctxt > ProofContext.add_fixes (prep_fixes ctxt fixes), []) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

490 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

491 
 declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

492 
 declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

493 

12727  494 
fun declare_elems prep_fixes (ctxt, ((name, ps), elems)) = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

495 
let val (ctxt', propps) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

496 
(case elems of 
13308  497 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  498 
 Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e])) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

499 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
12727  500 
in (ctxt', propps) end; 
501 

12839  502 
in 
503 

12727  504 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
505 
let 

506 
val int_elemss = 

507 
raw_elemss 

508 
> mapfilter (fn (id, Int es) => Some (id, es)  _ => None) 

509 
> unify_elemss ctxt fixed_params; 

510 
val (_, raw_elemss') = 

511 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

512 
(int_elemss, raw_elemss); 

513 
in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end; 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

514 

12839  515 
end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

516 

12839  517 
local 
518 

519 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 

520 

13336  521 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  522 
let 
523 
val body = Term.strip_all_body eq; 

524 
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 

525 
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); 

526 
val (f, xs) = Term.strip_comb lhs; 

13336  527 
val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs); 
528 
in (Term.dest_Free f, eq') end; 

529 

530 
fun abstract_thm sign eq = 

531 
Thm.assume (Thm.cterm_of sign eq) > Drule.gen_all > Drule.abs_def; 

12502  532 

13336  533 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  534 
let 
13336  535 
val ((y, T), b) = abstract_term eq; 
13308  536 
val b' = norm_term env b; 
13336  537 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  538 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  539 
in 
13308  540 
conditional (exists (equal y o #1) xs) (fn () => 
541 
err "Attempt to define previously specified variable"); 

542 
conditional (exists (fn (Free (y', _), _) => y = y'  _ => false) env) (fn () => 

543 
err "Attempt to redefine variable"); 

13336  544 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  545 
end; 
12575  546 

13308  547 
fun eval_text _ _ _ (text, Fixes _) = text 
13336  548 
 eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) = 
13375  549 
let val ts = map (norm_term env) (flat (map (map #1 o #2) asms)) 
550 
in (if do_text then spec @ ts else spec, (foldl Term.add_frees (xs, ts), env, defs)) end 

13308  551 
 eval_text ctxt id _ ((spec, binds), Defines defs) = 
552 
(spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 

553 
 eval_text _ _ _ (text, Notes _) = text; 

554 

555 
fun closeup _ false elem = elem 

556 
 closeup ctxt true elem = 

12839  557 
let 
13308  558 
fun close_frees t = 
559 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

560 
(Term.add_frees ([], t))) 

561 
in Term.list_all_free (frees, t) end; 

562 

563 
fun no_binds [] = [] 

564 
 no_binds _ = 

565 
raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt); 

566 
in 

567 
(case elem of 

568 
Assumes asms => Assumes (asms > map (fn (a, propps) => 

569 
(a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps))) 

570 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 

571 
(a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps)))) 

572 
 e => e) 

573 
end; 

12839  574 

12502  575 

12839  576 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  577 
(x, assoc_string (parms, x), mx)) fixes) 
12839  578 
 finish_ext_elem _ close (Assumes asms, propp) = 
579 
close (Assumes (map #1 asms ~~ propp)) 

580 
 finish_ext_elem _ close (Defines defs, propp) = 

12727  581 
close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp)) 
12839  582 
 finish_ext_elem _ _ (Notes facts, _) = Notes facts; 
583 

584 
fun finish_parms parms ((name, ps), elems) = 

585 
((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems); 

586 

13375  587 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  588 
let 
13308  589 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
590 
val text' = foldl (eval_text ctxt id false) (text, es); 

591 
in (text', (id, map Int es)) end 

13375  592 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  593 
let 
594 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  595 
val text' = eval_text ctxt id true (text, e'); 
13308  596 
in (text', (id, [Ext e'])) end; 
12839  597 

598 
in 

12510  599 

13375  600 
fun finish_elemss ctxt parms do_close = 
601 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  602 

603 
end; 

604 

13375  605 
fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

606 
let 
12727  607 
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

608 
val raw_propps = map flat raw_proppss; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

609 
val raw_propp = flat raw_propps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

610 
val (ctxt, all_propp) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

611 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

612 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  613 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

614 
val all_propp' = map2 (op ~~) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

615 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

616 
val n = length raw_concl; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

617 
val concl = take (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

618 
val propp = drop (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

619 
val propps = unflat raw_propps propp; 
12839  620 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  621 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

622 
val xs = map #1 (params_of raw_elemss); 
12727  623 
val typing = unify_frozen ctxt 0 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

624 
(map (ProofContext.default_type raw_ctxt) xs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

625 
(map (ProofContext.default_type ctxt) xs); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

626 
val parms = param_types (xs ~~ typing); 
12273  627 

13308  628 
val (text, elemss) = 
13375  629 
finish_elemss ctxt parms do_close (([], ([], [], [])), raw_elemss ~~ proppss); 
13308  630 
in ((parms, elemss, concl), text) end; 
12502  631 

632 
in 

633 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

634 
fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

635 
fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

636 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

637 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

638 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

639 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

640 
(* facts *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

641 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

642 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

643 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

644 
fun prep_name ctxt (name, atts) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

645 
if NameSpace.is_qualified name then 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

646 
raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

647 
else (name, atts); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

648 

13375  649 
fun prep_facts _ _ (Int elem) = elem 
650 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

651 
 prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms) 

652 
 prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs) 

653 
 prep_facts get ctxt (Ext (Notes facts)) = Notes (facts > map (fn (a, bs) => 

654 
(prep_name ctxt a, map (apfst (get ctxt)) bs))); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

655 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

656 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

657 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

658 
fun get_facts x = prep_facts ProofContext.get_thms x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

659 
fun get_facts_i x = prep_facts (K I) x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

660 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

661 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

662 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

663 

12546  664 
(* full context statements: import + elements + conclusion *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

665 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

666 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

667 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

668 
fun prep_context_statement prep_expr prep_elemss prep_facts 
13375  669 
do_close fixed_params import elements raw_concl context = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

670 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

671 
val sign = ProofContext.sign_of context; 
13375  672 

12575  673 
fun flatten (ids, Elem (Fixes fixes)) = 
674 
(ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]) 

675 
 flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)]) 

676 
 flatten (ids, Expr expr) = 

13308  677 
apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

678 

12575  679 
val (import_ids, raw_import_elemss) = flatten ([], Expr import); 
680 
val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements)))); 

13375  681 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  682 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
13375  683 

684 
val xs = foldl Term.add_frees ([], spec); 

685 
val xs' = parms > mapfilter (fn (x, _) => 

686 
(case assoc_string (xs, x) of None => None  Some T => Some (x, T))); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

687 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

688 
val n = length raw_import_elemss; 
12839  689 
val (import_ctxt, (import_elemss, import_facts)) = 
690 
activate_facts prep_facts (context, take (n, all_elemss)); 

691 
val (ctxt, (elemss, facts)) = 

692 
activate_facts prep_facts (import_ctxt, drop (n, all_elemss)); 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

693 
in 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

694 
((((import_ctxt, (import_elemss, import_facts)), 
13336  695 
(ctxt, (elemss, facts))), (xs', spec, defs)), concl) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

696 
end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

697 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

698 
val gen_context = prep_context_statement intern_expr read_elemss get_facts; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

699 
val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

700 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

701 
fun gen_facts prep_locale thy name = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

702 
let val ((((_, (_, facts)), _), _), _) = thy > ProofContext.init 
13375  703 
> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; 
704 
in flat (map (#2 o #1) facts) end; 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

705 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

706 
fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

707 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

708 
val thy = ProofContext.theory_of ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

709 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

710 
val (fixed_params, import) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

711 
(case locale of None => ([], empty) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

712 
 Some name => (param_types (#1 (#params (the_locale thy name))), Locale name)); 
12730  713 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') = 
13375  714 
prep_ctxt false fixed_params import elems concl ctxt; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

715 
in (locale, locale_ctxt, elems_ctxt, concl') end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

716 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

717 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

718 

13375  719 
fun read_context x y z = #1 (gen_context true [] x y [] z); 
720 
fun cert_context x y z = #1 (gen_context_i true [] x y [] z); 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

721 
val locale_facts = gen_facts intern; 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

722 
val locale_facts_i = gen_facts (K I); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

723 
val read_context_statement = gen_statement intern gen_context; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

724 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  725 

726 
end; 

11896  727 

728 

729 

13336  730 
(** define locales **) 
731 

732 
(* print locale *) 

12070  733 

12758  734 
fun print_locale thy import body = 
12070  735 
let 
736 
val sg = Theory.sign_of thy; 

12289  737 
val thy_ctxt = ProofContext.init thy; 
13375  738 
val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = read_context import body thy_ctxt; 
739 
val all_elems = flat (map #2 (import_elemss @ elemss)); 

12070  740 

12307  741 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
742 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

743 
val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; 

12070  744 

745 
fun prt_syn syn = 

746 
let val s = (case syn of None => "(structure)"  Some mx => Syntax.string_of_mixfix mx) 

12575  747 
in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; 
12070  748 
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: 
749 
prt_typ T :: Pretty.brk 1 :: prt_syn syn) 

750 
 prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); 

751 

12307  752 
fun prt_name "" = [Pretty.brk 1] 
753 
 prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1]; 

754 
fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts)); 

755 
fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]); 

756 
fun prt_fact ((a, _), ths) = Pretty.block 

757 
(prt_name a @ Pretty.breaks (map prt_thm (flat (map fst ths)))); 

12070  758 

12289  759 
fun items _ [] = [] 
760 
 items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; 

761 
fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes) 

762 
 prt_elem (Assumes asms) = items "assumes" (map prt_asm asms) 

763 
 prt_elem (Defines defs) = items "defines" (map prt_def defs) 

764 
 prt_elem (Notes facts) = items "notes" (map prt_fact facts); 

12277  765 
in 
13336  766 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
767 
> Pretty.writeln 

12277  768 
end; 
12070  769 

770 

12730  771 
(* store results *) 
11896  772 

12706  773 
local 
774 

12702  775 
fun hide_bound_names names thy = 
776 
thy > PureThy.hide_thms false 

777 
(map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names)); 

778 

12958  779 
in 
780 

13375  781 
fun have_thmss_qualified kind name args thy = 
12706  782 
thy 
13375  783 
> Theory.add_path (Sign.base_name name) 
12711  784 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  785 
>> hide_bound_names (map (#1 o #1) args) 
786 
>> Theory.parent_path; 

787 

12958  788 
fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind) 
789 
 smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc; 

790 

791 
end; 

792 

793 
local 

794 

795 
fun put_facts loc args thy = 

796 
let 

13308  797 
val {import, elems, params} = the_locale thy loc; 
12958  798 
val note = Notes (map (fn ((a, more_atts), th_atts) => 
799 
((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); 

13308  800 
in thy > put_locale loc (make_locale import (elems @ [(note, stamp ())]) params) end; 
12958  801 

12706  802 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
803 
let 

804 
val thy_ctxt = ProofContext.init thy; 

805 
val loc = prep_locale (Theory.sign_of thy) raw_loc; 

13375  806 
val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt))); 
12706  807 
val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; 
13375  808 
val export = ProofContext.export_standard loc_ctxt thy_ctxt; 
12711  809 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  810 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
811 
in 

812 
thy 

813 
> put_facts loc args 

814 
> have_thmss_qualified kind loc args' 

815 
end; 

816 

817 
in 

818 

12711  819 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
820 
val have_thmss_i = gen_have_thmss (K I) (K I); 

821 

13336  822 
fun add_thmss loc args (thy, ctxt) = 
12958  823 
let 
824 
val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args; 

13336  825 
val thy' = put_facts loc args' thy; 
13375  826 
val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [Notes args'])]); 
827 
in ((thy', ctxt'), map #1 facts') end; 

12702  828 

12706  829 
end; 
12063  830 

11896  831 

13336  832 
(* predicate text *) 
833 

13375  834 
local 
835 

836 
val introN = "intro"; 

837 
val axiomsN = "axioms"; 

838 

839 
fun atomize_spec sign ts = 

840 
let 

841 
val t = Library.foldr1 Logic.mk_conjunction ts; 

842 
val body = ObjectLogic.atomize_term sign t; 

843 
val bodyT = Term.fastype_of body; 

844 
in 

845 
if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t)) 

846 
else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t)) 

847 
end; 

848 

849 
fun print_translation name xs thy = 

850 
let 

851 
val n = length xs; 

852 
fun aprop_tr' c = (c, fn args => 

853 
if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) 

854 
else raise Match); 

855 
in thy > Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' name), []) end; 

13336  856 

13375  857 
in 
858 

859 
fun define_pred bname loc (xs, ts, defs) elemss thy = 

860 
let 

861 
val sign = Theory.sign_of thy; 

862 
val name = Sign.full_name sign bname; 

863 

864 

865 
(* predicate definition and syntax *) 

13336  866 

13375  867 
val (body, bodyT, body_eq) = atomize_spec sign ts; 
868 
val predT = map #2 xs > bodyT; 

869 
val head = Term.list_comb (Const (name, predT), map Free xs); 

870 
val statement = ObjectLogic.assert_propT sign head; 

871 

872 
val (defs_thy, [pred_def]) = 

873 
thy 

874 
> (if bodyT = propT then print_translation name xs else I) 

875 
> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)] 

876 
> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])]; 

877 
val defs_sign = Theory.sign_of defs_thy; 

878 
val cert = Thm.cterm_of defs_sign; 

879 

13336  880 

13375  881 
(* introduction rule *) 
882 

883 
val intro = Tactic.prove_standard defs_sign (map #1 xs) ts statement (fn _ => 

884 
Tactic.rewrite_goals_tac [pred_def] THEN 

885 
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN 

886 
Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts), 0) 1); 

887 

888 

889 
(* derived axioms *) 

890 

891 
val conjuncts = 

892 
Thm.assume (cert statement) 

893 
> Tactic.rewrite_rule [pred_def] 

894 
> Thm.equal_elim (Thm.symmetric body_eq) 

895 
> Drule.conj_elim_precise (length ts); 

896 

897 
val assumes = elemss > map (fn (("", _), es) => 

898 
flat (es > map (fn Assumes asms => flat (map (map #1 o #2) asms)  _ => [])) 

899 
 _ => []) > flat; 

900 

901 
val axioms = (assumes ~~ conjuncts) > map (fn (t, ax) => 

902 
Tactic.prove defs_sign [] [] t (fn _ => 

903 
Tactic.rewrite_goals_tac defs THEN 

904 
Tactic.compose_tac (false, ax, 0) 1)); 

905 

906 
val implies_intr_assumes = Drule.implies_intr_list (map cert assumes); 

907 
fun implies_elim_axioms th = Drule.implies_elim_list (implies_intr_assumes th) axioms; 

908 

909 
fun change_elem (axms, Assumes asms) = 

910 
apsnd Notes ((axms, asms) > foldl_map (fn (axs, (a, spec)) => 

911 
let val n = length spec 

912 
in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end)) 

913 
 change_elem (axms, Notes facts) = 

914 
(axms, Notes (facts > map (apsnd (map (apfst (map implies_elim_axioms)))))) 

915 
 change_elem e = e; 

916 

917 
val elemss' = ((axioms, elemss) > foldl_map 

918 
(fn (axms, (id as ("", _), es)) => foldl_map change_elem (axms, es) > apsnd (pair id) 

919 
 x => x) > #2) @ 

920 
[(("", []), [Assumes [((NameSpace.pack [loc, axiomsN], []), [(statement, ([], []))])]])]; 

921 
in 

922 
defs_thy 

923 
> have_thmss_qualified "" bname 

924 
[((introN, [ContextRules.intro_query_global None]), [([intro], [])])] 

925 
> #1 > rpair elemss' 

926 
end; 

927 

928 
end; 

13336  929 

930 

13297  931 
(* add_locale(_i) *) 
932 

933 
local 

934 

13375  935 
fun gen_add_locale prep_ctxt prep_expr pname bname raw_import raw_body thy = 
13297  936 
let 
937 
val sign = Theory.sign_of thy; 

938 
val name = Sign.full_name sign bname; 

939 
val _ = conditional (is_some (get_locale thy name)) (fn () => 

940 
error ("Duplicate definition of locale " ^ quote name)); 

941 

942 
val thy_ctxt = ProofContext.init thy; 

13375  943 
val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), text) = 
944 
prep_ctxt raw_import raw_body thy_ctxt; 

945 
val elemss = import_elemss @ body_elemss; 

13297  946 

13375  947 
val (pred_thy, elemss') = 
948 
if pname = Some None orelse Library.null (#1 text) then (thy, elemss) 

949 
else if pname = None then thy > define_pred (bname ^ "_axioms") bname text elemss 

950 
else thy > define_pred (the (the pname)) bname text elemss; 

951 
val elems' = elemss' > filter (equal "" o #1 o #1) > map #2 > flat; 

13297  952 

13375  953 
val pred_ctxt = ProofContext.init pred_thy; 
954 
val (ctxt, (_, facts)) = activate_facts (K I) (pred_ctxt, elemss') 

955 
val export = ProofContext.export_standard ctxt pred_ctxt; 

13297  956 
in 
13375  957 
pred_thy 
958 
> have_thmss_qualified "" name (facts > filter #2 > map (fn ((a, ths), _) => 

959 
((a, []), [(map export ths, [])]))) > #1 

13297  960 
> declare_locale name 
13375  961 
> put_locale name (make_locale (prep_expr sign raw_import) 
962 
(map (fn e => (e, stamp ())) elems') 

963 
(params_of elemss', map #1 (params_of body_elemss))) 

13297  964 
end; 
965 

966 
in 

967 

968 
val add_locale = gen_add_locale read_context intern_expr; 

969 
val add_locale_i = gen_add_locale cert_context (K I); 

970 

971 
end; 

972 

973 

12730  974 

11896  975 
(** locale theory setup **) 
12063  976 

11896  977 
val setup = 
978 
[LocalesData.init]; 

979 

980 
end; 