author  skalberg 
Thu, 03 Mar 2005 12:43:01 +0100  
changeset 15570  8d8c70b41bab 
parent 15531  08c8dad8e399 
child 15574  b1d1b5bfc464 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

3 
Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen 
11896  4 

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

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

7 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

8 
Draws some basic ideas from Florian Kammueller's original version of 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

9 
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

10 
metalogic. Furthermore, we provide structured import of contexts 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

11 
(with merge and rename operations), as well as typeinference of the 
13375  12 
signature parts, and predicate definitions of the specification text. 
14446  13 

14 
See also: 

15 

16 
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. 

17 
In Stefano Berardi et al., Types for Proofs and Programs: International 

15099  18 
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 3450, 2004. 
11896  19 
*) 
20 

21 
signature LOCALE = 

22 
sig 

12046  23 
type context 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

24 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

25 
(* Constructors for elem, expr and elem_expr are 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

26 
currently only used for inputting locales (outer_parse.ML). *) 
12046  27 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  28 
Fixes of (string * 'typ option * mixfix option) list  
12046  29 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
30 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  31 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
32 
datatype expr = 

33 
Locale of string  

34 
Rename of expr * string option list  

35 
Merge of expr list 

36 
val empty: expr 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

37 
datatype 'a elem_expr = Elem of 'a  Expr of expr 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

38 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

39 
(* Abstract interface to locales *) 
12046  40 
type 'att element 
41 
type 'att element_i 

42 
type locale 

43 
val intern: Sign.sg > xstring > string 

12014  44 
val cond_extern: Sign.sg > string > xstring 
12502  45 
val the_locale: theory > string > locale 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

46 
val map_attrib_element: ('att > context attribute) > 'att element > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

47 
context attribute element 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

48 
val map_attrib_element_i: ('att > context attribute) > 'att element_i > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

49 
context attribute element_i 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

50 
val map_attrib_elem_or_expr: ('att > context attribute) > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

51 
'att element elem_expr > context attribute element elem_expr 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

52 
val map_attrib_elem_or_expr_i: ('att > context attribute) > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

53 
'att element_i elem_expr > context attribute element_i elem_expr 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

54 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

55 
val read_context_statement: xstring option > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

56 
context attribute element elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

57 
(string * (string list * string list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

58 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

59 
(term * (term list * term list)) list list 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

60 
val cert_context_statement: string option > 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

61 
context attribute element_i elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

62 
(term * (term list * term list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

63 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

64 
(term * (term list * term list)) list list 
12758  65 
val print_locales: theory > unit 
66 
val print_locale: theory > expr > context attribute element list > unit 

13394  67 
val add_locale: bool > bstring > expr > context attribute element list > theory > theory 
68 
val add_locale_i: bool > bstring > expr > context attribute element_i list 

69 
> theory > theory 

15531  70 
val smart_note_thmss: string > (string * 'a) option > 
12958  71 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 
72 
theory > theory * (bstring * thm list) list 

14564  73 
val note_thmss: string > xstring > 
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15212
diff
changeset

74 
((bstring * context attribute list) * (thmref * context attribute list) list) list > 
12711  75 
theory > theory * (bstring * thm list) list 
14564  76 
val note_thmss_i: string > string > 
12711  77 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 
78 
theory > theory * (bstring * thm list) list 

12958  79 
val add_thmss: string > ((string * thm list) * context attribute list) list > 
13375  80 
theory * context > (theory * context) * (string * thm list) list 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

81 
val instantiate: string > string * context attribute list 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

82 
> thm list option > context > context 
11896  83 
val setup: (theory > theory) list 
84 
end; 

12839  85 

12289  86 
structure Locale: LOCALE = 
11896  87 
struct 
88 

12273  89 
(** locale elements and expressions **) 
11896  90 

12014  91 
type context = ProofContext.context; 
11896  92 

12046  93 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  94 
Fixes of (string * 'typ option * mixfix option) list  
12046  95 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
96 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  97 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
98 

99 
datatype expr = 

100 
Locale of string  

101 
Rename of expr * string option list  

102 
Merge of expr list; 

11896  103 

12273  104 
val empty = Merge []; 
105 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

106 
datatype 'a elem_expr = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

107 
Elem of 'a  Expr of expr; 
12273  108 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15212
diff
changeset

109 
type 'att element = (string, string, thmref, 'att) elem; 
15127  110 
type 'att element_i = (typ, term, thm list, 'att) elem; 
12070  111 

112 
type locale = 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

113 
{predicate: cterm list * thm list, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

114 
(* CB: For oldstyle locales with "(open)" this entry is ([], []). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

115 
For newstyle locales, which declare predicates, if the locale declares 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

116 
no predicates, this is also ([], []). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

117 
If the locale declares predicates, the record field is 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

118 
([statement], axioms), where statement is the locale predicate applied 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

119 
to the (assumed) locale parameters. Axioms contains the projections 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

120 
from the locale predicate to the normalised assumptions of the locale 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

121 
(cf. [1], normalisation of locale expressions.) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

122 
*) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

123 
import: expr, (*dynamic import*) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

124 
elems: (context attribute element_i * stamp) list, (*static content*) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

125 
params: (string * typ option) list * string list} (*all/local params*) 
12063  126 

11896  127 

128 
(** theory data **) 

129 

130 
structure LocalesArgs = 

131 
struct 

12014  132 
val name = "Isar/locales"; 
12063  133 
type T = NameSpace.T * locale Symtab.table; 
11896  134 

12063  135 
val empty = (NameSpace.empty, Symtab.empty); 
136 
val copy = I; 

12118  137 
val prep_ext = I; 
12289  138 

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

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

140 
fun join ({predicate, import, elems, params}: locale, {elems = elems', ...}: locale) = 
15531  141 
SOME {predicate = predicate, import = import, elems = gen_merge_lists eq_snd elems elems', 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

142 
params = params}; 
12273  143 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  144 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
145 

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

12014  148 
> Pretty.writeln; 
11896  149 
end; 
150 

151 
structure LocalesData = TheoryDataFun(LocalesArgs); 

152 
val print_locales = LocalesData.print; 

153 

12289  154 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
155 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

156 

12277  157 

158 
(* access locales *) 

159 

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

11896  162 

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

12014  166 
fun the_locale thy name = 
167 
(case get_locale thy name of 

15531  168 
SOME loc => loc 
169 
 NONE => error ("Unknown locale " ^ quote name)); 

11896  170 

12046  171 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

172 
(* import hierarchy 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

173 
implementation could be more efficient, eg. by maintaining a database 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

174 
of dependencies *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

175 

ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

176 
fun imports thy (upper, lower) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

177 
let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

178 
val sign = sign_of thy; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

179 
fun imps (Locale name) low = (name = low) orelse 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

180 
(case get_locale thy name of 
15531  181 
NONE => false 
182 
 SOME {import, ...} => imps import low) 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

183 
 imps (Rename (expr, _)) low = imps expr low 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

184 
 imps (Merge es) low = exists (fn e => imps e low) es; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

185 
in 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

186 
imps (Locale (intern sign upper)) (intern sign lower) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

187 
end; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

188 

ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

189 

12277  190 
(* diagnostics *) 
12273  191 

12277  192 
fun err_in_locale ctxt msg ids = 
193 
let 

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

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

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

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

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

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

12063  203 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

204 
(* Version for identifiers with axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

205 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

206 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  207 

208 

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

209 
(** primitives **) 
12046  210 

12277  211 
(* renaming *) 
12263  212 

15570  213 
fun rename ren x = getOpt (assoc_string (ren, x), x); 
12263  214 

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

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

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

218 
 rename_term _ a = a; 

219 

220 
fun rename_thm ren th = 

221 
let 

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

223 
val cert = Thm.cterm_of sign; 

15570  224 
val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps)); 
12263  225 
val xs' = map (rename ren) xs; 
226 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

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

228 
in 

229 
if xs = xs' then th 

230 
else 

231 
th 

232 
> Drule.implies_intr_list (map cert hyps) 

233 
> Drule.forall_intr_list (cert_frees xs) 

234 
> Drule.forall_elim_list (cert_vars xs) 

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

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

237 
end; 

238 

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

239 
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

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

241 
if x = x' then (x, T, mx) 
15531  242 
else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

243 
end)) 
12263  244 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
245 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  248 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  249 

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

250 
fun rename_facts prfx elem = 
12307  251 
let 
12323  252 
fun qualify (arg as ((name, atts), x)) = 
13394  253 
if prfx = "" orelse name = "" then arg 
13375  254 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  255 
in 
256 
(case elem of 

257 
Fixes fixes => Fixes fixes 

258 
 Assumes asms => Assumes (map qualify asms) 

259 
 Defines defs => Defines (map qualify defs) 

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

261 
end; 

262 

12263  263 

12502  264 
(* type instantiation *) 
265 

266 
fun inst_type [] T = T 

15570  267 
 inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; 
12502  268 

269 
fun inst_term [] t = t 

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

271 

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

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

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

275 
val sign = ProofContext.sign_of ctxt; 
12575  276 
val cert = Thm.cterm_of sign; 
277 
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

278 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
15570  279 
val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []); 
280 
val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; 

12502  281 
in 
282 
if null env' then th 

283 
else 

284 
th 

285 
> Drule.implies_intr_list (map cert hyps) 

12575  286 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  287 
> (fn (th', al) => th' > 
15570  288 
Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), [])) 
12502  289 
> (fn th'' => Drule.implies_elim_list th'' 
290 
(map (Thm.assume o cert o inst_term env') hyps)) 

291 
end; 

292 

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

293 
fun inst_elem _ env (Fixes fixes) = 
15570  294 
Fixes (map (fn (x, T, mx) => (x, Option.map (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

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

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

299 
 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

300 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  301 

302 

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

303 

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

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

305 

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

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

307 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

308 
(* CB: frozen_tvars has the following type: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

309 
ProofContext.context > Term.typ list > (Term.indexname * Term.typ) list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

310 

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

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

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

314 
val tfrees = map TFree 
14695  315 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

317 

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

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

319 
let 
15531  320 
fun paramify (i, NONE) = (i, NONE) 
321 
 paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T)); 

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

322 

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

323 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  324 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

325 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

326 

15531  327 
fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

328 
handle Type.TUNIFY => 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

329 
raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

330 
 unify (env, _) = env; 
15570  331 
val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
332 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 

333 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs)); 

334 
in map (Option.map (Envir.norm_type unifier')) Vs end; 

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

335 

15570  336 
fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)); 
337 
fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

338 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

339 
(* CB: param_types has the following type: 
15531  340 
('a * 'b option) list > ('a * 'b) list *) 
15570  341 
fun param_types ps = List.mapPartial (fn (_, NONE) => NONE  (x, SOME T) => SOME (x, T)) ps; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

342 

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

343 

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

344 
(* flatten expressions *) 
11896  345 

12510  346 
local 
12502  347 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

348 
(* CB: OUTDATED unique_parms has the following type: 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

349 
'a > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

350 
(('b * (('c * 'd) list * Symtab.key list)) * 'e) list > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

351 
(('b * ('c * 'd) list) * 'e) list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

352 

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

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

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

355 
val param_decls = 
15570  356 
List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

359 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
15531  360 
SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

361 
(map (apsnd (map fst)) ids) 
15531  362 
 NONE => map (apfst (apfst (apsnd #1))) elemss) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

364 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

365 
(* CB: unify_parms has the following type: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

366 
ProofContext.context > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

367 
(string * Term.typ) list > 
15531  368 
(string * Term.typ option) list list > 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

369 
((string * Term.sort) * Term.typ) list list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

370 

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

371 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  372 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

373 
val sign = ProofContext.sign_of ctxt; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

374 
val tsig = Sign.tsig_of sign; 
12502  375 
val maxidx = length raw_parmss; 
376 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

377 

378 
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

379 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  380 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  381 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

382 
fun unify T ((env, maxidx), U) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

383 
Type.unify tsig (env, maxidx) (U, T) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

384 
handle Type.TUNIFY => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

385 
let val prt = Sign.string_of_typ sign 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

386 
in raise TYPE ("unify_parms: failed to unify types " ^ 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

387 
prt U ^ " and " ^ prt T, [U, T], []) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

388 
end 
15570  389 
fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) 
12502  390 
 unify_list (envir, []) = envir; 
15570  391 
val (unifier, _) = Library.foldl unify_list 
12502  392 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 
393 

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

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

396 

397 
fun inst_parms (i, ps) = 

15570  398 
Library.foldr Term.add_typ_tfrees (List.mapPartial snd ps, []) 
399 
> List.mapPartial (fn (a, S) => 

12502  400 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
15531  401 
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) 
12502  402 
in map inst_parms idx_parmss end; 
403 

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

404 
in 
12502  405 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

406 
(* like unify_elemss, but does not touch axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

407 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

408 
fun unify_elemss' _ _ [] = [] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

409 
 unify_elemss' _ [] [elems] = [elems] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

410 
 unify_elemss' ctxt fixed_parms elemss = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

411 
let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

412 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

413 
fun inst ((((name, ps), axs), elems), env) = 
15570  414 
(((name, map (apsnd (Option.map (inst_type env))) ps), axs), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

415 
map (inst_elem ctxt env) elems); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

416 
in map inst (elemss ~~ envs) end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

417 

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

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

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

420 
 unify_elemss ctxt fixed_parms elemss = 
12502  421 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

422 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

423 
fun inst ((((name, ps), axs), elems), env) = 
15570  424 
(((name, map (apsnd (Option.map (inst_type env))) ps), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

425 
map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); 
12839  426 
in map inst (elemss ~~ envs) end; 
12502  427 

12575  428 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  429 
let 
430 
val thy = ProofContext.theory_of ctxt; 

12263  431 

15531  432 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
433 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  434 
 renaming [] _ = [] 
12289  435 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
15531  436 
commas (map (fn NONE => "_"  SOME x => quote x) xs)); 
12289  437 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

438 
fun rename_parms top ren ((name, ps), (parms, axs)) = 
12289  439 
let val ps' = map (rename ren) ps in 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

440 
(case duplicates ps' of [] => ((name, ps'), 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

441 
if top then (map (rename ren) parms, map (rename_thm ren) axs) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

442 
else (parms, axs)) 
12289  443 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 
444 
end; 

12263  445 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

446 
fun identify top (Locale name) = 
15212  447 
(* CB: ids is a list of tuples of the form ((name, ps) axs), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

448 
where name is a locale name, ps a list of parameter names and axs 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

449 
a list of axioms relating to the identifier, axs is empty unless 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

450 
identify at top level (top = true); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

451 
parms is accumulated list of parameters *) 
12289  452 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

453 
val {predicate = (_, axioms), import, params, ...} = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

454 
the_locale thy name; 
12289  455 
val ps = map #1 (#1 params); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

456 
val (ids', parms') = identify false import; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

457 
(* acyclic import dependencies *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

458 
val ids'' = ids' @ [((name, ps), ([], []))]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

459 
val ids_ax = if top then snd 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

460 
(foldl_map (fn (axs, ((name, parms), _)) => let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

461 
val {elems, ...} = the_locale thy name; 
15570  462 
val ts = List.concat (List.mapPartial (fn (Assumes asms, _) => 
463 
SOME (List.concat (map (map #1 o #2) asms))  _ => NONE) elems); 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

464 
val (axs1, axs2) = splitAt (length ts, axs); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

465 
in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids'')) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

466 
else ids''; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

467 
in (ids_ax, merge_lists parms' ps) end 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

468 
 identify top (Rename (e, xs)) = 
12273  469 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

470 
val (ids', parms') = identify top e; 
12839  471 
val ren = renaming xs parms' 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

472 
handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

473 
val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids'); 
15570  474 
val parms'' = distinct (List.concat (map (#2 o #1) ids'')); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

475 
in (ids'', parms'') end 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

476 
 identify top (Merge es) = 
15570  477 
Library.foldl (fn ((ids, parms), e) => let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

478 
val (ids', parms') = identify top e 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

479 
in (gen_merge_lists eq_fst ids ids', 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

480 
merge_lists parms parms') end) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

481 
(([], []), es); 
12014  482 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

483 
(* CB: enrich identifiers by parameter types and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

484 
the corresponding elements (with renamed parameters) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

485 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

486 
fun eval ((name, xs), axs) = 
12273  487 
let 
13308  488 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  489 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  490 
val (params', elems') = 
491 
if null ren then ((ps, qs), map #1 elems) 

12502  492 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  493 
map (rename_elem ren o #1) elems); 
13375  494 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

495 
in (((name, params'), axs), elems'') end; 
12307  496 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

497 
(* compute identifiers, merge with previous ones *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

498 
val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

499 
(* add types to params, check for unique params and unify them *) 
12575  500 
val raw_elemss = unique_parms ctxt (map eval idents); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

501 
val elemss = unify_elemss' ctxt [] raw_elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

502 
(* replace params in ids by params from axioms, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

503 
adjust types in axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

504 
val all_params' = params_of' elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

505 
val all_params = param_types all_params'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

506 
val elemss' = map (fn (((name, _), (ps, axs)), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

507 
(((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems)) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

508 
elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

509 
fun inst_ax th = let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

510 
val {hyps, prop, ...} = Thm.rep_thm th; 
15570  511 
val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps)); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

512 
val [env] = unify_parms ctxt all_params [ps]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

513 
val th' = inst_thm ctxt env th; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

514 
in th' end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

515 
val final_elemss = map (fn ((id, axs), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

516 
((id, map inst_ax axs), elems)) elemss'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

517 
in (prev_idents @ idents, final_elemss) end; 
12046  518 

12510  519 
end; 
520 

12070  521 

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

522 
(* activate elements *) 
12273  523 

12510  524 
local 
525 

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

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

527 
th > Drule.satisfy_hyps axs 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

528 
(* CB: replace metahyps, using axs, by a single metahyp. *) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

529 
> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

530 
(* CB: turn remaining hyps into assumptions. *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

531 
> Seq.single 
12263  532 

14643  533 
fun activate_elem _ ((ctxt, axs), Fixes fixes) = 
534 
((ctxt > ProofContext.add_fixes fixes, axs), []) 

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

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

536 
let 
15570  537 
val ts = List.concat (map (map #1 o #2) asms); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

538 
val (ps,qs) = splitAt (length ts, axs); 
13420  539 
val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

540 
ctxt > ProofContext.fix_frees ts 
13629  541 
> ProofContext.assume_i (export_axioms ps) asms; 
542 
in ((ctxt', qs), []) end 

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

543 
 activate_elem _ ((ctxt, axs), Defines defs) = 
13420  544 
let val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

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

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

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

550 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
14564  551 
let val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts 
13420  552 
in ((ctxt', axs), if is_ext then res else []) end; 
12502  553 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

554 
fun activate_elems (((name, ps), axs), elems) ctxt = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

557 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

559 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

562 
val elems = map (prep_facts ctxt) raw_elems; 
15570  563 
val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

565 

12546  566 
in 
567 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

568 
(* CB: activate_facts prep_facts (ctxt, elemss), 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

569 
where elemss is a list of pairs consisting of identifiers and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

570 
context elements, extends ctxt by the context elements yielding 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

571 
ctxt' and returns (ctxt', (elemss', facts)). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

572 
Identifiers in the argument are of the form ((name, ps), axs) and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

573 
assumptions use the axioms in the identifiers to set up exporters 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

574 
in ctxt'. elemss' does not contain identifiers and is obtained 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

575 
from elemss and the intermediate context with prep_facts. 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

576 
If get_facts or get_facts_i is used for prep_facts, these also remove 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

577 
the internal/external markers from elemss. *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

578 

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

579 
fun activate_facts prep_facts arg = 
15570  580 
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg); 
12546  581 

12510  582 
end; 
583 

12307  584 

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

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

586 

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

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

588 

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

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

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

591 
 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

592 

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

593 

12546  594 
(* attributes *) 
595 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

596 
local 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

597 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

598 
fun read_att attrib (x, srcs) = (x, map attrib srcs) 
12546  599 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

600 
(* CB: Map attrib over 
14446  601 
* A context element: add attrib to attribute lists of assumptions, 
602 
definitions and facts (on both sides for facts). 

603 
* Locale expression: no effect. *) 

604 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

605 
fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

606 
 gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

607 
 gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

608 
 gen_map_attrib_elem attrib (Notes facts) = 
15127  609 
Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts) 
610 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

611 
fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

612 
 gen_map_attrib_elem_expr _ (Expr expr) = Expr expr; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

613 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

614 
in 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

615 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

616 
val map_attrib_element = gen_map_attrib_elem; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

617 
val map_attrib_element_i = gen_map_attrib_elem; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

618 
val map_attrib_elem_or_expr = gen_map_attrib_elem_expr; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

619 
val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr; 
12546  620 

621 
end; 

622 

623 

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

624 
(* parameters *) 
12502  625 

626 
local 

627 

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

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

629 
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

630 
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

631 

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

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

633 

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

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

635 
fun cert_fixes x = prep_fixes ProofContext.cert_vars 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 
(* propositions and bindings *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

641 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

642 
(* CB: an internal (Int) locale element was either imported or included, 
15104  643 
an external (Ext) element appears directly in the locale. *) 
644 

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

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

646 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

647 
(* CB: flatten (ids, expr) normalises expr (which is either a locale 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

648 
expression or a single context element) wrt. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

649 
to the list ids of already accumulated identifiers. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

650 
It returns (ids', elemss) where ids' is an extension of ids 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

651 
with identifiers generated for expr, and elemss is the list of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

652 
context elements generated from expr, decorated with additional 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

653 
information (for expr it is the identifier, where parameters additionially 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

654 
contain type information (extracted from the locale record), for a Fixes 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

655 
element, it is an identifier with name = "" and parameters with type 
15531  656 
information NONE, for other elements it is simply ("", [])). 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

657 
The implementation of activate_facts relies on identifier names being 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

658 
empty strings for external elements. 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

659 
TODO: correct this comment wrt axioms. *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

660 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

661 
fun flatten _ (ids, Elem (Fixes fixes)) = 
15531  662 
(ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))]) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

663 
 flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)]) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

664 
 flatten (ctxt, prep_expr) (ids, Expr expr) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

665 
apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr)); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

666 

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

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

668 

12839  669 
local 
670 

12727  671 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  672 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
15570  673 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), []) 
12727  674 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

675 

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

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

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

679 
 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

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

681 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

684 
(case elems of 
13308  685 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  686 
 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

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

12839  690 
in 
691 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

692 
(* CB: only called by prep_elemss. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

693 

12727  694 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
695 
let 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

696 
(* CB: fix of type bug of goal in target with context elements. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

697 
Parameters new in context elements must receive types that are 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

698 
distinct from types of parameters in target (fixed_params). *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

699 
val ctxt_with_fixed = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

700 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  701 
val int_elemss = 
702 
raw_elemss 

15570  703 
> List.mapPartial (fn (id, Int es) => SOME (id, es)  _ => NONE) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

704 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  705 
val (_, raw_elemss') = 
706 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

707 
(int_elemss, raw_elemss); 

708 
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

709 

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

711 

12839  712 
local 
713 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

714 
(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

715 
used in eval_text for defines elements. *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

716 

12839  717 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
718 

13336  719 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  720 
let 
721 
val body = Term.strip_all_body eq; 

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

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

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

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

727 

728 
fun abstract_thm sign eq = 

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

12502  730 

13336  731 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  732 
let 
13336  733 
val ((y, T), b) = abstract_term eq; 
13308  734 
val b' = norm_term env b; 
13336  735 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  736 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  737 
in 
13308  738 
conditional (exists (equal y o #1) xs) (fn () => 
739 
err "Attempt to define previously specified variable"); 

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

741 
err "Attempt to redefine variable"); 

13336  742 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  743 
end; 
12575  744 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

745 
(* CB: for finish_elems (Int and Ext) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

746 

13308  747 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  748 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
749 
let 

15570  750 
val ts = List.concat (map (map #1 o #2) asms); 
13394  751 
val ts' = map (norm_term env) ts; 
752 
val spec' = 

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

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

15570  755 
in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

756 
 eval_text ctxt (id, _) _ ((spec, binds), Defines defs) = 
15570  757 
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 
13308  758 
 eval_text _ _ _ (text, Notes _) = text; 
759 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

760 
(* CB: for finish_elems (Ext) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

761 

13308  762 
fun closeup _ false elem = elem 
763 
 closeup ctxt true elem = 

12839  764 
let 
13308  765 
fun close_frees t = 
766 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

769 

770 
fun no_binds [] = [] 

771 
 no_binds _ = 

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

773 
in 

774 
(case elem of 

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

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

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

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

779 
 e => e) 

780 
end; 

12839  781 

12502  782 

12839  783 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  784 
(x, assoc_string (parms, x), mx)) fixes) 
12839  785 
 finish_ext_elem _ close (Assumes asms, propp) = 
786 
close (Assumes (map #1 asms ~~ propp)) 

787 
 finish_ext_elem _ close (Defines defs, propp) = 

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

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

791 
(* CB: finish_parms introduces type info from parms to identifiers *) 
15531  792 
(* CB: only needed for types that have been NONE so far??? 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

793 
If so, which are these??? *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

794 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

795 
fun finish_parms parms (((name, ps), axs), elems) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

796 
(((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems); 
12839  797 

13375  798 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  799 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

800 
val [(id', es)] = unify_elemss ctxt parms [(id, e)]; 
15570  801 
val text' = Library.foldl (eval_text ctxt id' false) (text, es); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

802 
in (text', (id', map Int es)) end 
13375  803 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  804 
let 
805 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  806 
val text' = eval_text ctxt id true (text, e'); 
13308  807 
in (text', (id, [Ext e'])) end; 
12839  808 

809 
in 

12510  810 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

811 
(* CB: only called by prep_elemss *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

812 

13375  813 
fun finish_elemss ctxt parms do_close = 
814 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  815 

816 
end; 

817 

15127  818 
(* CB: type inference and consistency checks for locales *) 
819 

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

821 
let 
15127  822 
(* CB: contexts computed in the course of this function are discarded. 
823 
They are used for type inference and consistency checks only. *) 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

824 
(* CB: fixed_params are the parameters (with types) of the target locale, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

825 
empty list if there is no target. *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

826 
(* CB: raw_elemss are list of pairs consisting of identifiers and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

827 
context elements, the latter marked as internal or external. *) 
12727  828 
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

829 
(* CB: raw_ctxt is context with additional fixed variables derived from 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

830 
the fixes elements in raw_elemss, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

831 
raw_proppss contains assumptions and definitions from the 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

832 
external elements in raw_elemss. *) 
15570  833 
val raw_propps = map List.concat raw_proppss; 
834 
val raw_propp = List.concat raw_propps; 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

835 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

836 
(* CB: add type information from fixed_params to context (declare_terms) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

837 
(* CB: process patterns (conclusion and external elements only) *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

839 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

840 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

841 
(* CB: add type information from conclusion and external elements 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

842 
to context *) 
15570  843 
val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt; 
12502  844 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

845 
(* CB: resolve schematic variables (patterns) in conclusion and external 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

846 
elements. *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

848 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
13629  849 
val (concl, propp) = splitAt(length raw_concl, all_propp'); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

850 
val propps = unflat raw_propps propp; 
12839  851 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  852 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

853 
(* CB: obtain all parameters from identifier part of raw_elemss *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

858 
val parms = param_types (xs ~~ typing); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

859 
(* CB: parms are the parameters from raw_elemss, with correct typing. *) 
12273  860 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

861 
(* CB: extract information from assumes and defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

862 
(fixes and notes in raw_elemss don't have an effect on text and elemss), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

863 
compute final form of context elements. *) 
13394  864 
val (text, elemss) = finish_elemss ctxt parms do_close 
865 
(((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss); 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

866 
(* CB: text has the following structure: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

867 
(((exts, exts'), (ints, ints')), (xs, env, defs)) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

868 
where 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

869 
exts: external assumptions (terms in external assumes elements) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

870 
exts': dito, normalised wrt. env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

871 
ints: internal assumptions (terms in internal assumes elements) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

872 
ints': dito, normalised wrt. env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

873 
xs: the free variables in exts' and ints' and rhss of definitions, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

874 
this includes parameters except defined parameters 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

875 
env: list of term pairs encoding substitutions, where the first term 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

876 
is a free variable; substitutions represent defines elements and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

877 
the rhs is normalised wrt. the previous env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

878 
defs: theorems representing the substitutions from defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

879 
(thms are normalised wrt. env). 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

880 
elemss is an updated version of raw_elemss: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

881 
 type info added to Fixes 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

882 
 axiom and definition statement replaced by corresponding one 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

883 
from proppss in Assumes and Defines 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

884 
 Facts unchanged 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

885 
*) 
13308  886 
in ((parms, elemss, concl), text) end; 
12502  887 

888 
in 

889 

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

890 
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

891 
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

892 

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

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

894 

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

895 

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

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

897 

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

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

899 

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

900 
fun prep_name ctxt (name, atts) = 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

901 
(* CB: reject qualified theorem names in locale declarations *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

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

905 

13375  906 
fun prep_facts _ _ (Int elem) = elem 
907 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

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

912 

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

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

914 

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

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

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

917 

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

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

919 

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

920 

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

922 

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

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

924 

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

925 
fun prep_context_statement prep_expr prep_elemss prep_facts 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

928 
val sign = ProofContext.sign_of context; 
13375  929 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

930 
val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

931 
(* CB: normalise "includes" among elements *) 
15570  932 
val raw_elemss = List.concat (#2 ((foldl_map (flatten (context, prep_expr sign)) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

933 
(import_ids, elements)))); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

934 
(* CB: raw_import_elemss @ raw_elemss is the normalised list of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

935 
context elements obtained from import and elements. *) 
13375  936 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  937 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

938 
(* CB: all_elemss and parms contain the correct parameter types *) 
13629  939 
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

940 
val (import_ctxt, (import_elemss, _)) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

941 
activate_facts prep_facts (context, ps); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

942 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

943 
val (ctxt, (elemss, _)) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

944 
activate_facts prep_facts (import_ctxt, qs); 
15212  945 
val stmt = gen_distinct Term.aconv 
15570  946 
(List.concat (map (fn ((_, axs), _) => 
947 
List.concat (map (#hyps o Thm.rep_thm) axs)) qs)); 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

948 
val cstmt = map (cterm_of sign) stmt; 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

949 
in 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

952 

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

953 
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

954 
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

955 

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

956 
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

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

958 
val thy = ProofContext.theory_of ctxt; 
15570  959 
val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

960 
val (target_stmt, fixed_params, import) = 
15531  961 
(case locale of NONE => ([], [], empty) 
962 
 SOME name => 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

963 
let val {predicate = (stmt, _), params = (ps, _), ...} = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

964 
the_locale thy name 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

965 
in (stmt, param_types ps, Locale name) end); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

966 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

967 
prep_ctxt false fixed_params import elems concl ctxt; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

968 
in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

969 

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

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

971 

15127  972 
(* CB: processing of locales for add_locale(_i) and print_locale *) 
973 
(* CB: arguments are: x>import, y>body (elements), z>context *) 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

974 
fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

975 
fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

976 

15127  977 
(* CB: processing of locales for note_thmss(_i), 
978 
Proof.multi_theorem(_i) and antiquotations with option "locale" *) 

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

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

980 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  981 

982 
end; 

11896  983 

984 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

985 
(** CB: experimental instantiation mechanism **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

986 

14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

987 
fun instantiate loc_name (prfx, attribs) raw_inst ctxt = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

988 
let 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

989 
val thy = ProofContext.theory_of ctxt; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

990 
val sign = Theory.sign_of thy; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

991 
val tsig = Sign.tsig_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

992 
val cert = cterm_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

993 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

994 
(** process the locale **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

995 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

996 
val {predicate = (_, axioms), params = (ps, _), ...} = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

997 
the_locale thy (intern sign loc_name); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

998 
val fixed_params = param_types ps; 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

999 
val init = ProofContext.init thy; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1000 
val (ids, raw_elemss) = 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1001 
flatten (init, intern_expr sign) ([], Expr (Locale loc_name)); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1002 
val ((parms, all_elemss, concl), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1003 
(spec as (_, (ints, _)), (xs, env, defs))) = 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1004 
read_elemss false (* do_close *) init 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1005 
fixed_params (* could also put [] here??? *) raw_elemss 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1006 
[] (* concl *); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1007 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1008 
(** analyse the instantiation theorem inst **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1009 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1010 
val inst = case raw_inst of 
15531  1011 
NONE => if null ints 
1012 
then NONE 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1013 
else error "Locale has assumptions but no chained fact was found" 
15531  1014 
 SOME [] => if null ints 
1015 
then NONE 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1016 
else error "Locale has assumptions but no chained fact was found" 
15531  1017 
 SOME [thm] => if null ints 
1018 
then (warning "Locale has no assumptions: fact ignored"; NONE) 

1019 
else SOME thm 

1020 
 SOME _ => error "Multiple facts are not allowed"; 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1021 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1022 
val args = case inst of 
15531  1023 
NONE => [] 
1024 
 SOME thm => thm > prop_of > ObjectLogic.drop_judgment sign 

14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1025 
> Term.strip_comb 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1026 
>> (fn t as (Const (s, _)) => if (intern sign loc_name = s) 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1027 
then t 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1028 
else error ("Constant " ^ quote loc_name ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1029 
" expected but constant " ^ quote s ^ " was found") 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1030 
 t => error ("Constant " ^ quote loc_name ^ " expected \ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1031 
\but term " ^ quote (Sign.string_of_term sign t) ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1032 
" was found")) 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1033 
> snd; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1034 
val cargs = map cert args; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1035 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1036 
(* process parameters: match their types with those of arguments *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1037 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1038 
val def_names = map (fn (Free (s, _), _) => s) env; 
15570  1039 
val (defined, assumed) = List.partition 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1040 
(fn (s, _) => s mem def_names) fixed_params; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1041 
val cassumed = map (cert o Free) assumed; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1042 
val cdefined = map (cert o Free) defined; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1043 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1044 
val param_types = map snd assumed; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1045 
val v_param_types = map Type.varifyT param_types; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1046 
val arg_types = map Term.fastype_of args; 
15570  1047 
val Tenv = Library.foldl (Type.typ_match tsig) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1048 
(Vartab.empty, v_param_types ~~ arg_types) 
15570  1049 
handle UnequalLengths => error "Number of parameters does not \ 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1050 
\match number of arguments of chained fact"; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1051 
(* get their sorts *) 
15570  1052 
val tfrees = Library.foldr Term.add_typ_tfrees (param_types, []); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1053 
val Tenv' = map 
15570  1054 
(fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T)) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1055 
(Vartab.dest Tenv); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1056 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1057 
(* process (internal) elements *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1058 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1059 
fun inst_type [] T = T 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1060 
 inst_type env T = 
15570  1061 
Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1062 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1063 
fun inst_term [] t = t 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1064 
 inst_term env t = Term.map_term_types (inst_type env) t; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1065 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1066 
(* parameters with argument types *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1067 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1068 
val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1069 
val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1070 
val cdefining = map (cert o inst_term Tenv' o snd) env; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1071 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1072 
fun inst_thm _ [] th = th 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1073 
 inst_thm ctxt Tenv th = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1074 
let 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1075 
val sign = ProofContext.sign_of ctxt; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1076 
val cert = Thm.cterm_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1077 
val certT = Thm.ctyp_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1078 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
15570  1079 
val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []); 
1080 
val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv; 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1081 
in 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1082 
if null Tenv' then th 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1083 
else 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1084 
th 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1085 
> Drule.implies_intr_list (map cert hyps) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1086 
> Drule.tvars_intr_list (map (#1 o #1) Tenv') 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1087 
> (fn (th', al) => th' > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1088 
Thm.instantiate ((map (fn ((a, _), T) => 
15570  1089 
(valOf (assoc (al, a)), certT T)) Tenv'), [])) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1090 
> (fn th'' => Drule.implies_elim_list th'' 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1091 
(map (Thm.assume o cert o inst_term Tenv') hyps)) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1092 
end; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1093 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1094 
fun inst_thm' thm = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1095 
let 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1096 
(* not all axs are normally applicable *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1097 
val hyps = #hyps (rep_thm thm); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1098 
val ass = map (fn ax => (prop_of ax, ax)) axioms; 
15570  1099 
val axs' = Library.foldl (fn (axs, hyp) => 
15531  1100 
(case gen_assoc (op aconv) (ass, hyp) of NONE => axs 
1101 
 SOME ax => axs @ [ax])) ([], hyps); 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1102 
val thm' = Drule.satisfy_hyps axs' thm; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1103 
(* instantiate types *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1104 
val thm'' = inst_thm ctxt Tenv' thm'; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1105 
(* substitute arguments and discharge hypotheses *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1106 
val thm''' = case inst of 
15531  1107 
NONE => thm'' 
1108 
 SOME inst_thm => let 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1109 
val hyps = #hyps (rep_thm thm''); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1110 
val th = thm'' > implies_intr_hyps 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1111 
> forall_intr_list (cparams' @ cdefined') 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1112 
> forall_elim_list (cargs @ cdefining) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1113 
(* th has premises of the form either inst_thm or x==x *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1114 
fun mk hyp = if Logic.is_equals hyp 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1115 
then hyp > Logic.dest_equals > snd > cert 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1116 
> reflexive 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1117 
else inst_thm 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1118 
in implies_elim_list th (map mk hyps) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1119 
end; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1120 
in thm''' end; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1121 

14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1122 
val prefix_fact = 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1123 
if prfx = "" then I 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1124 
else (fn "" => "" 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1125 
 s => NameSpace.append prfx s); 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1126 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1127 
fun inst_elem (ctxt, (Ext _)) = ctxt 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1128 
 inst_elem (ctxt, (Int (Notes facts))) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1129 
(* instantiate fact *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1130 
let val facts' = 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1131 
map (apsnd (map (apfst (map inst_thm')))) facts 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1132 
handle THM (msg, n, thms) => error ("Exception THM " ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1133 
string_of_int n ^ " raised\n" ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1134 
"Note: instantiate does not support oldstyle locales \ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1135 
\declared with (open)\n" ^ msg ^ "\n" ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1136 
cat_lines (map string_of_thm thms)) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1137 
(* rename fact *) 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1138 
val facts'' = map (apfst (apfst prefix_fact)) facts' 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1139 
(* add attributes *) 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1140 
val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts'' 
14564  1141 
in fst (ProofContext.note_thmss_i facts''' ctxt) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1142 
end 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1143 
 inst_elem (ctxt, (Int _)) = ctxt; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1144 

15570  1145 
fun inst_elems (ctxt, (id, elems)) = Library.foldl inst_elem (ctxt, elems); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1146 

15570  1147 
fun inst_elemss ctxt elemss = Library.foldl inst_elems (ctxt, elemss); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1148 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1149 
(* main part *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1150 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1151 
val ctxt' = ProofContext.qualified true ctxt; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1152 
in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1153 
end; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1154 

11896  1155 

13336  1156 
(** define locales **) 
1157 

1158 
(* print locale *) 

12070  1159 

12758  1160 
fun print_locale thy import body = 
12070  1161 
let 
12289  1162 
val thy_ctxt = ProofContext.init thy; 
13420  1163 
val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt; 
15570  1164 
val all_elems = List.concat (map #2 (import_elemss @ elemss)); 
12070  1165 

12307  1166 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
1167 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  1169 

1170 
fun prt_syn syn = 

15531  1171 
let val s = (case syn of NONE => "(structure)"  SOME mx => Syntax.string_of_mixfix mx) 
12575  1172 
in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; 
15531  1173 
fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: 
12070  1174 
prt_typ T :: Pretty.brk 1 :: prt_syn syn) 
15531  1175 
 prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); 
12070  1176 

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

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

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

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

15570  1182 
(prt_name a @ Pretty.breaks (map prt_thm (List.concat (map fst ths)))); 
12070  1183 

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

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

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

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

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

12277  1190 
in 
13336  1191 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
1192 
> Pretty.writeln 

12277  1193 
end; 
12070  1194 

1195 

12730  1196 
(* store results *) 
11896  1197 

12706  1198 
local 
1199 

12702  1200 
fun hide_bound_names names thy = 
1201 
thy > PureThy.hide_thms false 

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

1203 

12958  1204 
in 
1205 

14564  1206 
fun note_thmss_qualified kind name args thy = 
12706  1207 
thy 
13375  1208 
> Theory.add_path (Sign.base_name name) 
14564  1209 
> PureThy.note_thmss_i (Drule.kind kind) args 
12706  1210 
>> hide_bound_names (map (#1 o #1) args) 
1211 
>> Theory.parent_path; 

1212 

15531  1213 
fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind) 
1214 
 smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc; 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1215 
(* CB: only used in Proof.finish_global. *) 
12958  1216 

1217 
end; 

1218 

1219 
local 

1220 

1221 
fun put_facts loc args thy = 

1222 
let 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1223 
val {predicate, import, elems, params} = the_locale thy loc; 
12958  1224 
val note = Notes (map (fn ((a, more_atts), th_atts) => 
1225 
((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1226 
in thy > put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())], 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1227 
params = params} end; 
12958  1228 

14564  1229 
fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy = 
12706  1230 
let 
1231 
val thy_ctxt = ProofContext.init thy; 

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

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1233 
val (_, (stmt, _), loc_ctxt, _, _) = 
15531  1234 
cert_context_statement (SOME loc) [] [] thy_ctxt; 
12706  1235 
val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1236 
val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt; 
14564  1237 
val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt)); 
12706  1238 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
1239 
in 

1240 
thy 

1241 
> put_facts loc args 

14564  1242 
> note_thmss_qualified kind loc args' 
12706  1243 
end; 
1244 

1245 
in 

1246 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1247 
(* CB: note_thmss(_i) is the base for the Isar commands 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1248 
"theorems (in loc)" and "declare (in loc)". *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1249 

14564  1250 
val note_thmss = gen_note_thmss intern ProofContext.get_thms; 
1251 
val note_thmss_i = gen_note_thmss (K I) (K I); 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1252 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1253 
(* CB: only used in Proof.finish_global. *) 
12711  1254 

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

13336  1258 
val thy' = put_facts loc args' thy; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1259 
val (ctxt', (_, facts')) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
