author  wenzelm 
Fri, 19 Jul 2002 18:44:07 +0200  
changeset 13399  c136276dc847 
parent 13394  b39347206719 
child 13415  63462ccc6fac 
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 > 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

43 
string option * cterm option * context * context * (term * (term list * term list)) list list 
12529
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 > 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

46 
string option * cterm 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 

13394  49 
val add_locale: bool > bstring > expr > context attribute element list > theory > theory 
50 
val add_locale_i: bool > bstring > expr > context attribute element_i list 

51 
> theory > theory 

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

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

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

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

58 
val have_thmss_i: string > string > 

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

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

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

12839  65 

12289  66 
structure Locale: LOCALE = 
11896  67 
struct 
68 

12273  69 
(** locale elements and expressions **) 
11896  70 

12014  71 
type context = ProofContext.context; 
11896  72 

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

12273  77 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
78 

79 
datatype expr = 

80 
Locale of string  

81 
Rename of expr * string option list  

82 
Merge of expr list; 

11896  83 

12273  84 
val empty = Merge []; 
85 

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

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

88 

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

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

12070  91 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

92 
type view = (cterm * thm list) option; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

93 

c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

94 
fun view_statement (None: view) = None 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

95 
 view_statement (Some (ct, _)) = Some ct; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

96 

c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

97 
fun view_axioms (None: view) = [] 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

98 
 view_axioms (Some (_, axs)) = axs; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

99 

12070  100 
type locale = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

101 
{view: view, (*external view on assumptions*) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

102 
import: expr, (*dynamic import*) 
12289  103 
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

104 
params: (string * typ option) list * string list}; (*all/local params*) 
12063  105 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

106 
fun make_locale view import elems params = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

107 
{view = view, import = import, elems = elems, params = params}: locale; 
12063  108 

11896  109 

110 

111 
(** theory data **) 

112 

113 
structure LocalesArgs = 

114 
struct 

12014  115 
val name = "Isar/locales"; 
12063  116 
type T = NameSpace.T * locale Symtab.table; 
11896  117 

12063  118 
val empty = (NameSpace.empty, Symtab.empty); 
119 
val copy = I; 

12118  120 
val prep_ext = I; 
12289  121 

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

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

123 
fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

124 
Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); 
12273  125 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  126 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
127 

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

12014  130 
> Pretty.writeln; 
11896  131 
end; 
132 

133 
structure LocalesData = TheoryDataFun(LocalesArgs); 

134 
val print_locales = LocalesData.print; 

135 

12289  136 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
137 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

138 

12277  139 

140 
(* access locales *) 

141 

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

11896  144 

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

12014  148 
fun the_locale thy name = 
149 
(case get_locale thy name of 

150 
Some loc => loc 

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

11896  152 

12046  153 

12277  154 
(* diagnostics *) 
12273  155 

12277  156 
fun err_in_locale ctxt msg ids = 
157 
let 

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

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

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

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

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

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

12063  167 

12277  168 

169 

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

170 
(** primitives **) 
12046  171 

12277  172 
(* renaming *) 
12263  173 

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

175 

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

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

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

179 
 rename_term _ a = a; 

180 

181 
fun rename_thm ren th = 

182 
let 

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

184 
val cert = Thm.cterm_of sign; 

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

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

189 
in 

190 
if xs = xs' then th 

191 
else 

192 
th 

193 
> Drule.implies_intr_list (map cert hyps) 

194 
> Drule.forall_intr_list (cert_frees xs) 

195 
> Drule.forall_elim_list (cert_vars xs) 

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

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

198 
end; 

199 

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

200 
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

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

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

203 
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

204 
end)) 
12263  205 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
206 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  209 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  210 

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

211 
fun rename_facts prfx elem = 
12307  212 
let 
12323  213 
fun qualify (arg as ((name, atts), x)) = 
13394  214 
if prfx = "" orelse name = "" then arg 
13375  215 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  216 
in 
217 
(case elem of 

218 
Fixes fixes => Fixes fixes 

219 
 Assumes asms => Assumes (map qualify asms) 

220 
 Defines defs => Defines (map qualify defs) 

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

222 
end; 

223 

12263  224 

12502  225 
(* type instantiation *) 
226 

227 
fun inst_type [] T = T 

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

229 

230 
fun inst_term [] t = t 

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

232 

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

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

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

236 
val sign = ProofContext.sign_of ctxt; 
12575  237 
val cert = Thm.cterm_of sign; 
238 
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

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

12502  242 
in 
243 
if null env' then th 

244 
else 

245 
th 

246 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

252 
end; 

253 

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

254 
fun inst_elem _ env (Fixes fixes) = 
12502  255 
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

256 
 inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
12502  257 
(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

258 
 inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 
12502  259 
(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

260 
 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

261 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  262 

263 

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

264 

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

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

266 

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

267 
(* parameter types *) 
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 frozen_tvars ctxt Ts = 
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 tvars = rev (foldl Term.add_tvarsT ([], Ts)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

273 
(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

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

275 

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

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

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

278 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
12546  279 
fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T) 
280 
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

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

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

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

284 

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

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

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

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

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

291 

12730  292 
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

293 
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

294 

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

295 

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

296 
(* flatten expressions *) 
11896  297 

12510  298 
local 
12502  299 

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

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

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

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

303 
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

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

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

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

307 
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

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

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

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

311 

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

312 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  313 
let 
314 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

315 
val maxidx = length raw_parmss; 

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

317 

318 
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

319 
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

320 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  321 

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

322 
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

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

326 
val (unifier, _) = foldl unify_list 

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

328 

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

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

331 

332 
fun inst_parms (i, ps) = 

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

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

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

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

337 
in map inst_parms idx_parmss end; 

338 

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

339 
in 
12502  340 

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

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

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

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

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

12839  348 
in map inst (elemss ~~ envs) end; 
12502  349 

12575  350 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  351 
let 
352 
val thy = ProofContext.theory_of ctxt; 

12263  353 

12289  354 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
355 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

359 

360 
fun rename_parms ren (name, ps) = 

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

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

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

364 
end; 

12263  365 

12273  366 
fun identify ((ids, parms), Locale name) = 
12289  367 
let 
368 
val {import, params, ...} = the_locale thy name; 

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

370 
in 

12273  371 
if (name, ps) mem ids then (ids, parms) 
12277  372 
else 
12289  373 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
374 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  375 
end 
376 
 identify ((ids, parms), Rename (e, xs)) = 

377 
let 

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

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

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

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

12273  384 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  385 

12307  386 
fun eval (name, xs) = 
12273  387 
let 
13308  388 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  389 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  390 
val (params', elems') = 
391 
if null ren then ((ps, qs), map #1 elems) 

12502  392 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  393 
map (rename_elem ren o #1) elems); 
13375  394 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  395 
in ((name, params'), elems'') end; 
12307  396 

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

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

399 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  400 
in (prev_idents @ idents, elemss) end; 
12046  401 

12510  402 
end; 
403 

12070  404 

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

405 
(* activate elements *) 
12273  406 

12510  407 
local 
408 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

409 
fun export_axioms axs _ hyps th = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

410 
th > Drule.satisfy_hyps axs 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

411 
> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

412 
> Seq.single; 
12263  413 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

414 
fun activate_elem _ ((ctxt, axs), Fixes fixes) = ((ctxt > ProofContext.add_fixes fixes, axs), []) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

415 
 activate_elem _ ((ctxt, axs), Assumes asms) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

416 
let 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

417 
val ts = flat (map (map #1 o #2) asms); 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

418 
val n = length ts; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

419 
val (ctxt', res) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

420 
ctxt > ProofContext.fix_frees ts 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

421 
> ProofContext.assume_i (export_axioms (Library.take (n, axs))) asms; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

422 
in ((ctxt', Library.drop (n, axs)), map (rpair false) res) end 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

423 
 activate_elem _ ((ctxt, axs), Defines defs) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

424 
let val (ctxt', res) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

425 
ctxt > ProofContext.assume_i ProofContext.export_def 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

426 
(defs > map (fn ((name, atts), (t, ps)) => 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

427 
let val (c, t') = ProofContext.cert_def ctxt t 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

428 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

429 
in ((ctxt', axs), map (rpair false) res) end 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

430 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

431 
let val (ctxt', res) = ctxt > ProofContext.have_thmss_i facts 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

432 
in ((ctxt', axs), map (rpair is_ext) res) end; 
12502  433 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

434 
fun activate_elems ((name, ps), elems) (ctxt, axs) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

435 
let val ((ctxt', axs'), res) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

436 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

437 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

438 
in ((ProofContext.restore_qualified ctxt ctxt', axs'), res) end; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

439 

c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

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

442 
val elems = map (prep_facts ctxt) raw_elems; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

443 
val ((ctxt', axs'), res) = apsnd flat (activate_elems ((name, ps), elems) (ctxt, axs)); 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

444 
in ((ctxt', axs'), (((name, ps), elems), res)) end); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

445 

12546  446 
in 
447 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

448 
fun activate_facts prep_facts arg = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

449 
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); 
12546  450 

12510  451 
end; 
452 

12307  453 

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

454 

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

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

456 

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

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

458 

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

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

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

461 
 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

462 

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

463 

12546  464 
(* attributes *) 
465 

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

467 

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

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

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

471 
 attribute attrib (Elem (Notes facts)) = 

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

473 
 attribute _ (Expr expr) = Expr expr; 

474 

475 
end; 

476 

477 

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

478 
(* parameters *) 
12502  479 

480 
local 

481 

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

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

483 
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

484 
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

485 

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

486 
in 
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 read_fixes x = prep_fixes ProofContext.read_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

490 

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

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

492 

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

493 

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

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

495 

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

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

497 

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

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

499 

12839  500 
local 
501 

12727  502 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  503 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  504 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
505 
 declare_int_elem (ctxt, _) = (ctxt, []); 

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

506 

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

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

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

510 
 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

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

512 

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

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

515 
(case elems of 
13308  516 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  517 
 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

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

12839  521 
in 
522 

12727  523 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
524 
let 

525 
val int_elemss = 

526 
raw_elemss 

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

528 
> unify_elemss ctxt fixed_params; 

529 
val (_, raw_elemss') = 

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

531 
(int_elemss, raw_elemss); 

532 
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

533 

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

535 

12839  536 
local 
537 

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

539 

13336  540 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  541 
let 
542 
val body = Term.strip_all_body eq; 

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

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

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

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

548 

549 
fun abstract_thm sign eq = 

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

12502  551 

13336  552 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  553 
let 
13336  554 
val ((y, T), b) = abstract_term eq; 
13308  555 
val b' = norm_term env b; 
13336  556 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  557 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  558 
in 
13308  559 
conditional (exists (equal y o #1) xs) (fn () => 
560 
err "Attempt to define previously specified variable"); 

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

562 
err "Attempt to redefine variable"); 

13336  563 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  564 
end; 
12575  565 

13308  566 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  567 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
568 
let 

569 
val ts = flat (map (map #1 o #2) asms); 

570 
val ts' = map (norm_term env) ts; 

571 
val spec' = 

572 
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) 

573 
else ((exts, exts'), (ints @ ts, ints' @ ts')); 

574 
in (spec', (foldl Term.add_frees (xs, ts'), env, defs)) end 

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

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

578 

579 
fun closeup _ false elem = elem 

580 
 closeup ctxt true elem = 

12839  581 
let 
13308  582 
fun close_frees t = 
583 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

586 

587 
fun no_binds [] = [] 

588 
 no_binds _ = 

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

590 
in 

591 
(case elem of 

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

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

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

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

596 
 e => e) 

597 
end; 

12839  598 

12502  599 

12839  600 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  601 
(x, assoc_string (parms, x), mx)) fixes) 
12839  602 
 finish_ext_elem _ close (Assumes asms, propp) = 
603 
close (Assumes (map #1 asms ~~ propp)) 

604 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

610 

13375  611 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  612 
let 
13308  613 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
614 
val text' = foldl (eval_text ctxt id false) (text, es); 

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

13375  616 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  617 
let 
618 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  619 
val text' = eval_text ctxt id true (text, e'); 
13308  620 
in (text', (id, [Ext e'])) end; 
12839  621 

622 
in 

12510  623 

13375  624 
fun finish_elemss ctxt parms do_close = 
625 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  626 

627 
end; 

628 

13375  629 
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

630 
let 
12727  631 
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

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

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

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

635 
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

636 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  637 

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

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

639 
(#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

640 
val n = length raw_concl; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

641 
val concl = Library.take (n, all_propp'); 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

643 
val propps = unflat raw_propps propp; 
12839  644 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  645 

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

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

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

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

650 
val parms = param_types (xs ~~ typing); 
12273  651 

13394  652 
val (text, elemss) = finish_elemss ctxt parms do_close 
653 
(((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss); 

13308  654 
in ((parms, elemss, concl), text) end; 
12502  655 

656 
in 

657 

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

658 
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

659 
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

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 

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

664 
(* facts *) 
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_name ctxt (name, atts) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

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

672 

13375  673 
fun prep_facts _ _ (Int elem) = elem 
674 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

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

679 

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

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

681 

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

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

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

684 

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

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

686 

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

687 

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

689 

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

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

691 

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

692 
fun prep_context_statement prep_expr prep_elemss prep_facts 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

693 
do_close axioms fixed_params import elements raw_concl context = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

695 
val sign = ProofContext.sign_of context; 
13375  696 

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

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

700 
 flatten (ids, Expr expr) = 

13308  701 
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

702 

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

13375  705 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  706 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
13375  707 

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

708 
val n = length raw_import_elemss; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

709 
val ((import_ctxt, axioms'), (import_elemss, import_facts)) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

710 
activate_facts prep_facts ((context, axioms), Library.take (n, all_elemss)); 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

711 
val ((ctxt, _), (elemss, facts)) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

712 
activate_facts prep_facts ((import_ctxt, axioms'), Library.drop (n, all_elemss)); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

714 
((((import_ctxt, (import_elemss, import_facts)), 
13394  715 
(ctxt, (elemss, facts))), (parms, spec, defs)), concl) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

717 

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

718 
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

719 
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

720 

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

721 
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

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

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

724 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

725 
val (view, fixed_params, import) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

726 
(case locale of None => (None, [], empty) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

727 
 Some name => 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

728 
let val {view, params = (ps, _), ...} = the_locale thy name 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

729 
in (view, param_types ps, Locale name) end); 
12730  730 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

731 
prep_ctxt false (view_axioms view) fixed_params import elems concl ctxt; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

732 
in (locale, view_statement view, locale_ctxt, elems_ctxt, concl') end; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

733 

c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

734 
fun gen_facts prep_locale thy name = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

735 
let val ((((_, (_, facts)), _), _), _) = thy > ProofContext.init 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

736 
> gen_context_i false [] [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

737 
in flat (map (#2 o #1) facts) end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

738 

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

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

740 

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

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

742 
val locale_facts_i = gen_facts (K I); 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

743 

c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

744 
fun read_context x y z = #1 (gen_context true [] [] x y [] z); 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

745 
fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

747 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  748 

749 
end; 

11896  750 

751 

752 

13336  753 
(** define locales **) 
754 

755 
(* print locale *) 

12070  756 

12758  757 
fun print_locale thy import body = 
12070  758 
let 
12289  759 
val thy_ctxt = ProofContext.init thy; 
13375  760 
val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = read_context import body thy_ctxt; 
761 
val all_elems = flat (map #2 (import_elemss @ elemss)); 

12070  762 

12307  763 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
764 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  766 

767 
fun prt_syn syn = 

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

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

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

773 

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

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

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

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

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

12070  780 

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

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

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

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

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

12277  787 
in 
13336  788 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
789 
> Pretty.writeln 

12277  790 
end; 
12070  791 

792 

12730  793 
(* store results *) 
11896  794 

12706  795 
local 
796 

12702  797 
fun hide_bound_names names thy = 
798 
thy > PureThy.hide_thms false 

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

800 

12958  801 
in 
802 

13375  803 
fun have_thmss_qualified kind name args thy = 
12706  804 
thy 
13375  805 
> Theory.add_path (Sign.base_name name) 
12711  806 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  807 
>> hide_bound_names (map (#1 o #1) args) 
808 
>> Theory.parent_path; 

809 

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

812 

813 
end; 

814 

815 
local 

816 

817 
fun put_facts loc args thy = 

818 
let 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

819 
val {view, import, elems, params} = the_locale thy loc; 
12958  820 
val note = Notes (map (fn ((a, more_atts), th_atts) => 
821 
((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

822 
in thy > put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end; 
12958  823 

12706  824 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
825 
let 

826 
val thy_ctxt = ProofContext.init thy; 

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

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

828 
val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt; 
12706  829 
val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

830 
val export = ProofContext.export_standard view loc_ctxt thy_ctxt; 
12711  831 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  832 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
833 
in 

834 
thy 

835 
> put_facts loc args 

836 
> have_thmss_qualified kind loc args' 

837 
end; 

838 

839 
in 

840 

12711  841 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
842 
val have_thmss_i = gen_have_thmss (K I) (K I); 

843 

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

13336  847 
val thy' = put_facts loc args' thy; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

848 
val {view, ...} = the_locale thy loc; 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

849 
val ((ctxt', _), (_, facts')) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

850 
activate_facts (K I) ((ctxt, view_axioms view), [((loc, []), [Notes args'])]); 
13375  851 
in ((thy', ctxt'), map #1 facts') end; 
12702  852 

12706  853 
end; 
12063  854 

11896  855 

13336  856 
(* predicate text *) 
857 

13375  858 
local 
859 

860 
val introN = "intro"; 

13394  861 
val axiomsN = "_axioms"; 
13375  862 

863 
fun atomize_spec sign ts = 

864 
let 

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

866 
val body = ObjectLogic.atomize_term sign t; 

867 
val bodyT = Term.fastype_of body; 

868 
in 

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

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

871 
end; 

872 

13394  873 
fun aprop_tr' n c = (c, fn args => 
874 
if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) 

875 
else raise Match); 

13336  876 

13394  877 
fun def_pred bname parms defs ts ts' thy = 
13375  878 
let 
879 
val sign = Theory.sign_of thy; 

880 
val name = Sign.full_name sign bname; 

881 

13394  882 
val (body, bodyT, body_eq) = atomize_spec sign ts'; 
883 
val env = Term.add_term_free_names (body, []); 

884 
val xs = filter (fn (x, _) => x mem_string env) parms; 

885 
val Ts = map #2 xs; 

886 
val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees (Ts, [])) 

887 
> Library.sort_wrt #1 > map TFree; 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

888 
val predT = map Term.itselfT extraTs > Ts > bodyT; 
13336  889 

13394  890 
val args = map Logic.mk_type extraTs @ map Free xs; 
891 
val head = Term.list_comb (Const (name, predT), args); 

13375  892 
val statement = ObjectLogic.assert_propT sign head; 
893 

894 
val (defs_thy, [pred_def]) = 

895 
thy 

13394  896 
> (if bodyT <> propT then I else 
897 
Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), [])) 

13375  898 
> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)] 
899 
> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])]; 

13394  900 

13375  901 
val defs_sign = Theory.sign_of defs_thy; 
902 
val cert = Thm.cterm_of defs_sign; 

903 

13394  904 
val intro = Tactic.prove_standard defs_sign [] [] statement (fn _ => 
13375  905 
Tactic.rewrite_goals_tac [pred_def] THEN 
906 
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN 

13394  907 
Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts'), 0) 1); 
13375  908 

909 
val conjuncts = 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

910 
Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

911 
Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] 
13375  912 
> Drule.conj_elim_precise (length ts); 
13394  913 
val axioms = (ts ~~ conjuncts) > map (fn (t, ax) => 
13375  914 
Tactic.prove defs_sign [] [] t (fn _ => 
915 
Tactic.rewrite_goals_tac defs THEN 

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

13394  917 
in (defs_thy, (statement, intro, axioms)) end; 
13375  918 

13394  919 
fun change_elem _ (axms, Assumes asms) = 
920 
apsnd Notes ((axms, asms) > foldl_map (fn (axs, (a, spec)) => 

921 
let val n = length spec 

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

923 
 change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts)) 

924 
 change_elem _ e = e; 

925 

926 
fun change_elemss axioms elemss = (axioms, elemss) > foldl_map 

927 
(fn (axms, (id as ("", _), es)) => 

928 
foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) > apsnd (pair id) 

929 
 x => x) > #2; 

930 

931 
in 

13375  932 

13394  933 
fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = 
934 
let 

935 
val (thy', (elemss', more_ts)) = 

936 
if Library.null exts then (thy, (elemss, [])) 

937 
else 

938 
let 

939 
val aname = bname ^ axiomsN; 

940 
val (def_thy, (statement, intro, axioms)) = 

941 
thy > def_pred aname parms defs exts exts'; 

942 
val elemss' = change_elemss axioms elemss @ 

943 
[(("", []), [Assumes [((aname, []), [(statement, ([], []))])]])]; 

944 
in 

945 
def_thy > have_thmss_qualified "" aname 

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

947 
> #1 > rpair (elemss', [statement]) 

948 
end; 

949 
val (thy'', view) = 

950 
if Library.null more_ts andalso Library.null ints then (thy', None) 

951 
else 

952 
let 

953 
val (def_thy, (statement, intro, axioms)) = 

954 
thy' > def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts); 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

955 
val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement; 
13394  956 
in 
957 
def_thy > have_thmss_qualified "" bname 

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

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

959 
> #1 > rpair (Some (cstatement, axioms)) 
13394  960 
end; 
961 
in (thy'', (elemss', view)) end; 

13375  962 

963 
end; 

13336  964 

965 

13297  966 
(* add_locale(_i) *) 
967 

968 
local 

969 

13394  970 
fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy = 
13297  971 
let 
972 
val sign = Theory.sign_of thy; 

973 
val name = Sign.full_name sign bname; 

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

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

976 

977 
val thy_ctxt = ProofContext.init thy; 

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

980 
val elemss = import_elemss @ body_elemss; 

13297  981 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

982 
val (pred_thy, (elemss', view)) = 
13394  983 
if do_pred then thy > define_preds bname text elemss 
984 
else (thy, (elemss, None)); 

13375  985 
val pred_ctxt = ProofContext.init pred_thy; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

986 
val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms view), elemss') 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

987 
val export = ProofContext.export_standard (view_statement view) ctxt pred_ctxt; 
13297  988 
in 
13375  989 
pred_thy 
990 
> have_thmss_qualified "" name (facts > filter #2 > map (fn ((a, ths), _) => 

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

13297  992 
> declare_locale name 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

993 
> put_locale name (make_locale view (prep_expr sign raw_import) 
13394  994 
(map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) 
13375  995 
(params_of elemss', map #1 (params_of body_elemss))) 
13297  996 
end; 
997 

998 
in 

999 

1000 
val add_locale = gen_add_locale read_context intern_expr; 

1001 
val add_locale_i = gen_add_locale cert_context (K I); 

1002 

1003 
end; 

1004 

1005 

12730  1006 

11896  1007 
(** locale theory setup **) 
12063  1008 

11896  1009 
val setup = 
1010 
[LocalesData.init]; 

1011 

1012 
end; 