author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18742  b38a18c9aed9 
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 

17437  14 
Interpretation enables the reuse of theorems of locales in other 
15 
contexts, namely those defined by theories, structured proofs and 

16 
locales themselves. 

17 

14446  18 
See also: 
19 

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

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

15099  22 
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 3450, 2004. 
11896  23 
*) 
24 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

25 
(* TODO: 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

26 
 betaeta normalisation of interpretation parameters 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

27 
 dangling type frees in locales 
16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

28 
 test subsumption of interpretations when merging theories 
17138  29 
 var vs. fixes in locale to be interpreted (interpretation in locale) 
30 
(implicit locale expressions generated by multiple registrations) 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

31 
*) 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

32 

11896  33 
signature LOCALE = 
34 
sig 

12273  35 
datatype expr = 
36 
Locale of string  

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

37 
Rename of expr * (string * mixfix option) option list  
12273  38 
Merge of expr list 
39 
val empty: expr 

18137  40 
datatype 'a element = Elem of 'a  Expr of expr 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

41 

16458  42 
val intern: theory > xstring > string 
43 
val extern: theory > string > xstring 

18617  44 
val init: string > theory > Proof.context 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

45 

18617  46 
(* Processing of locale statements *) (* FIXME export more abstract version *) 
18137  47 
val read_context_statement: xstring option > Element.context element list > 
18617  48 
(string * (string list * string list)) list list > Proof.context > 
49 
string option * (cterm list * cterm list) * Proof.context * Proof.context * 

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

50 
(term * (term list * term list)) list list 
18137  51 
val cert_context_statement: string option > Element.context_i element list > 
18617  52 
(term * (term list * term list)) list list > Proof.context > 
53 
string option * (cterm list * cterm list) * Proof.context * Proof.context * 

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

54 
(term * (term list * term list)) list list 
15596  55 

56 
(* Diagnostic functions *) 

12758  57 
val print_locales: theory > unit 
18137  58 
val print_locale: theory > bool > expr > Element.context list > unit 
17138  59 
val print_global_registrations: bool > string > theory > unit 
18617  60 
val print_local_registrations': bool > string > Proof.context > unit 
61 
val print_local_registrations: bool > string > Proof.context > unit 

18137  62 

18671  63 
(* FIXME avoid duplicates *) 
18137  64 
val add_locale_context: bool > bstring > expr > Element.context list > theory 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

65 
> ((Element.context_i list list * Element.context_i list list) 
18617  66 
* Proof.context) * theory 
18137  67 
val add_locale_context_i: bool > bstring > expr > Element.context_i list > theory 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

68 
> ((Element.context_i list list * Element.context_i list list) 
18617  69 
* Proof.context) * theory 
18137  70 
val add_locale: bool > bstring > expr > Element.context list > theory > theory 
71 
val add_locale_i: bool > bstring > expr > Element.context_i list > theory > theory 

15596  72 

15696  73 
(* Storing results *) 
15703  74 
val smart_note_thmss: string > string option > 
18728  75 
((bstring * attribute list) * (thm list * attribute list) list) list > 
18421
464c93701351
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

76 
theory > (bstring * thm list) list * theory 
15703  77 
val note_thmss: string > xstring > 
78 
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list > 

18617  79 
theory > (bstring * thm list) list * (theory * Proof.context) 
15703  80 
val note_thmss_i: string > string > 
81 
((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list > 

18617  82 
theory > (bstring * thm list) list * (theory * Proof.context) 
18137  83 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

84 
val theorem: string > Method.text option > (thm list list > theory > theory) > 
18137  85 
string * Attrib.src list > Element.context element list > 
17355  86 
((string * Attrib.src list) * (string * (string list * string list)) list) list > 
87 
theory > Proof.state 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

88 
val theorem_i: string > Method.text option > (thm list list > theory > theory) > 
18728  89 
string * attribute list > Element.context_i element list > 
90 
((string * attribute list) * (term * (term list * term list)) list) list > 

17355  91 
theory > Proof.state 
17856  92 
val theorem_in_locale: string > Method.text option > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

93 
(thm list list > thm list list > theory > theory) > 
18137  94 
xstring > string * Attrib.src list > Element.context element list > 
17355  95 
((string * Attrib.src list) * (string * (string list * string list)) list) list > 
96 
theory > Proof.state 

17856  97 
val theorem_in_locale_i: string > Method.text option > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

98 
(thm list list > thm list list > theory > theory) > 
18137  99 
string > string * Attrib.src list > Element.context_i element list > 
17355  100 
((string * Attrib.src list) * (term * (term list * term list)) list) list > 
101 
theory > Proof.state 

102 
val smart_theorem: string > xstring option > 

18137  103 
string * Attrib.src list > Element.context element list > 
17355  104 
((string * Attrib.src list) * (string * (string list * string list)) list) list > 
105 
theory > Proof.state 

106 
val interpretation: string * Attrib.src list > expr > string option list > 

107 
theory > Proof.state 

108 
val interpretation_in_locale: xstring * expr > theory > Proof.state 

109 
val interpret: string * Attrib.src list > expr > string option list > 

110 
bool > Proof.state > Proof.state 

11896  111 
end; 
12839  112 

12289  113 
structure Locale: LOCALE = 
11896  114 
struct 
115 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

116 

12273  117 
(** locale elements and expressions **) 
11896  118 

18137  119 
datatype ctxt = datatype Element.ctxt; 
17355  120 

12273  121 
datatype expr = 
122 
Locale of string  

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

123 
Rename of expr * (string * mixfix option) option list  
12273  124 
Merge of expr list; 
11896  125 

12273  126 
val empty = Merge []; 
127 

18137  128 
datatype 'a element = 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

129 
Elem of 'a  Expr of expr; 
12273  130 

18137  131 
fun map_elem f (Elem e) = Elem (f e) 
132 
 map_elem _ (Expr e) = Expr e; 

133 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

134 
type witness = term * thm; (*hypothesis as fact*) 
12070  135 
type locale = 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

136 
{predicate: cterm list * witness list, 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

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

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

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

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

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

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

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

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

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

146 
import: expr, (*dynamic import*) 
18137  147 
elems: (Element.context_i * stamp) list, (*static content*) 
18671  148 
params: ((string * typ) * mixfix) list * string list, 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

149 
(*all/local params*) 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

150 
regs: ((string * string list) * (term * thm) list) list} 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

151 
(* Registrations: indentifiers and witness theorems of locales interpreted 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

152 
in the locale. 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

153 
*) 
12063  154 

11896  155 

15703  156 
(* CB: an internal (Int) locale element was either imported or included, 
157 
an external (Ext) element appears directly in the locale text. *) 

158 

159 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 

160 

161 

162 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

163 
(** management of registrations in theories and proof contexts **) 
11896  164 

15837  165 
structure Registrations : 
166 
sig 

167 
type T 

168 
val empty: T 

169 
val join: T * T > T 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

170 
val dest: T > (term list * ((string * Attrib.src list) * witness list)) list 
16458  171 
val lookup: theory > T * term list > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

172 
((string * Attrib.src list) * witness list) option 
16458  173 
val insert: theory > term list * (string * Attrib.src list) > T > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

174 
T * (term list * ((string * Attrib.src list) * witness list)) list 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

175 
val add_witness: term list > witness > T > T 
15837  176 
end = 
177 
struct 

178 
(* a registration consists of theorems instantiating locale assumptions 

179 
and prefix and attributes, indexed by parameter instantiation *) 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

180 
type T = ((string * Attrib.src list) * witness list) Termtab.table; 
15837  181 

182 
val empty = Termtab.empty; 

183 

184 
(* term list represented as single term, for simultaneous matching *) 

185 
fun termify ts = 

18343  186 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  187 
fun untermify t = 
188 
let fun ut (Const _) ts = ts 

189 
 ut (s $ t) ts = ut s (t::ts) 

190 
in ut t [] end; 

191 

16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

192 
(* joining of registrations: prefix and attributes of left theory, 
15837  193 
thms are equal, no attempt to subsumption testing *) 
16458  194 
fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2); 
15837  195 

196 
fun dest regs = map (apfst untermify) (Termtab.dest regs); 

197 

198 
(* registrations that subsume t *) 

17203  199 
fun subsumers thy t regs = 
200 
List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); 

15837  201 

202 
(* look up registration, pick one that subsumes the query *) 

203 
fun lookup sign (regs, ts) = 

204 
let 

205 
val t = termify ts; 

17203  206 
val subs = subsumers sign t regs; 
15837  207 
in (case subs of 
208 
[] => NONE 

209 
 ((t', (attn, thms)) :: _) => let 

18190  210 
val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty); 
15837  211 
(* thms contain Frees, not Vars *) 
212 
val tinst' = tinst > Vartab.dest 

213 
> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) 

214 
> Symtab.make; 

215 
val inst' = inst > Vartab.dest 

216 
> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) 

217 
> Symtab.make; 

218 
in 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

219 
SOME (attn, map (fn (t, th) => 
18137  220 
(Element.inst_term (tinst', inst') t, 
221 
Element.inst_thm sign (tinst', inst') th)) thms) 

15837  222 
end) 
223 
end; 

224 

225 
(* add registration if not subsumed by ones already present, 

226 
additionally returns registrations that are strictly subsumed *) 

227 
fun insert sign (ts, attn) regs = 

228 
let 

229 
val t = termify ts; 

17203  230 
val subs = subsumers sign t regs ; 
15837  231 
in (case subs of 
232 
[] => let 

233 
val sups = 

17203  234 
List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); 
15837  235 
val sups' = map (apfst untermify) sups 
17412  236 
in (Termtab.update (t, (attn, [])) regs, sups') end 
15837  237 
 _ => (regs, [])) 
238 
end; 

239 

240 
(* add witness theorem to registration, 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

241 
only if instantiation is exact, otherwise exception Option raised *) 
15837  242 
fun add_witness ts thm regs = 
243 
let 

244 
val t = termify ts; 

18343  245 
val (x, thms) = the (Termtab.lookup regs t); 
15837  246 
in 
17412  247 
Termtab.update (t, (x, thm::thms)) regs 
15837  248 
end; 
249 
end; 

250 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

251 

15837  252 
(** theory data **) 
15596  253 

16458  254 
structure GlobalLocalesData = TheoryDataFun 
255 
(struct 

12014  256 
val name = "Isar/locales"; 
15837  257 
type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table; 
15596  258 
(* 1st entry: locale namespace, 
259 
2nd entry: locales of the theory, 

15837  260 
3rd entry: registrations, indexed by locale name *) 
11896  261 

15596  262 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  263 
val copy = I; 
16458  264 
val extend = I; 
12289  265 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

266 
fun join_locs _ ({predicate, import, elems, params, regs}: locale, 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

267 
{elems = elems', regs = regs', ...}: locale) = 
15596  268 
SOME {predicate = predicate, import = import, 
17496  269 
elems = gen_merge_lists (eq_snd (op =)) elems elems', 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

270 
params = params, 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

271 
regs = merge_alists regs regs'}; 
16458  272 
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = 
15596  273 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 
16458  274 
Symtab.join (K (SOME o Registrations.join)) (regs1, regs2)); 
12289  275 

15596  276 
fun print _ (space, locs, _) = 
16346  277 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 
12014  278 
> Pretty.writeln; 
16458  279 
end); 
11896  280 

18708  281 
val _ = Context.add_setup GlobalLocalesData.init; 
15801  282 

283 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

284 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

285 
(** context data **) 
11896  286 

16458  287 
structure LocalLocalesData = ProofDataFun 
288 
(struct 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

289 
val name = "Isar/locales"; 
15837  290 
type T = Registrations.T Symtab.table; 
291 
(* registrations, indexed by locale name *) 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

292 
fun init _ = Symtab.empty; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

293 
fun print _ _ = (); 
16458  294 
end); 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

295 

18708  296 
val _ = Context.add_setup LocalLocalesData.init; 
12289  297 

12277  298 

299 
(* access locales *) 

300 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

301 
val print_locales = GlobalLocalesData.print; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

302 

16458  303 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get; 
304 
val extern = NameSpace.extern o #1 o GlobalLocalesData.get; 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

305 

16144  306 
fun declare_locale name thy = 
307 
thy > GlobalLocalesData.map (fn (space, locs, regs) => 

16458  308 
(Sign.declare_name thy name space, locs, regs)); 
11896  309 

15596  310 
fun put_locale name loc = 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

311 
GlobalLocalesData.map (fn (space, locs, regs) => 
17412  312 
(space, Symtab.update (name, loc) locs, regs)); 
313 

314 
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name; 

11896  315 

12014  316 
fun the_locale thy name = 
317 
(case get_locale thy name of 

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

11896  320 

12046  321 

15596  322 
(* access registrations *) 
323 

15696  324 
(* Ids of global registrations are varified, 
325 
Ids of local registrations are not. 

326 
Thms of registrations are never varified. *) 

327 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

328 
(* retrieve registration from theory or context *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

329 

15696  330 
fun gen_get_registrations get thy_ctxt name = 
17412  331 
case Symtab.lookup (get thy_ctxt) name of 
15696  332 
NONE => [] 
15837  333 
 SOME reg => Registrations.dest reg; 
15696  334 

335 
val get_global_registrations = 

336 
gen_get_registrations (#3 o GlobalLocalesData.get); 

337 
val get_local_registrations = 

338 
gen_get_registrations LocalLocalesData.get; 

339 

16458  340 
fun gen_get_registration get thy_of thy_ctxt (name, ps) = 
17412  341 
case Symtab.lookup (get thy_ctxt) name of 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

342 
NONE => NONE 
16458  343 
 SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

344 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

345 
val get_global_registration = 
16458  346 
gen_get_registration (#3 o GlobalLocalesData.get) I; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

347 
val get_local_registration = 
16458  348 
gen_get_registration LocalLocalesData.get ProofContext.theory_of; 
15596  349 

18343  350 
val test_global_registration = is_some oo get_global_registration; 
351 
val test_local_registration = is_some oo get_local_registration; 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

352 
fun smart_test_registration ctxt id = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

353 
let 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

354 
val thy = ProofContext.theory_of ctxt; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

355 
in 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

356 
test_global_registration thy id orelse test_local_registration ctxt id 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

357 
end; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

358 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

359 

15837  360 
(* add registration to theory or context, ignored if subsumed *) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

361 

16458  362 
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = 
15837  363 
map_data (fn regs => 
364 
let 

16458  365 
val thy = thy_of thy_ctxt; 
18343  366 
val reg = the_default Registrations.empty (Symtab.lookup regs name); 
16458  367 
val (reg', sups) = Registrations.insert thy (ps, attn) reg; 
15837  368 
val _ = if not (null sups) then warning 
369 
("Subsumed interpretation(s) of locale " ^ 

16458  370 
quote (extern thy name) ^ 
15837  371 
"\nby interpretation(s) with the following prefix(es):\n" ^ 
372 
commas_quote (map (fn (_, ((s, _), _)) => s) sups)) 

373 
else (); 

17412  374 
in Symtab.update (name, reg') regs end) thy_ctxt; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

375 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

376 
val put_global_registration = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

377 
gen_put_registration (fn f => 
16458  378 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; 
15837  379 
val put_local_registration = 
16458  380 
gen_put_registration LocalLocalesData.map ProofContext.theory_of; 
15596  381 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

382 
fun put_registration_in_locale name id thy = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

383 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

384 
val {predicate, import, elems, params, regs} = the_locale thy name; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

385 
in 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

386 
put_locale name {predicate = predicate, import = import, 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

387 
elems = elems, params = params, regs = regs @ [(id, [])]} thy 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

388 
end; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

389 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

390 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

391 
(* add witness theorem to registration in theory or context, 
15596  392 
ignored if registration not present *) 
393 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

394 
fun add_witness (name, ps) thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

395 
Symtab.map_entry name (Registrations.add_witness ps thm); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

396 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

397 
fun add_global_witness id thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

398 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs)); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

399 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

400 
val add_local_witness = LocalLocalesData.map oo add_witness; 
15596  401 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

402 
fun add_witness_in_locale name id thm thy = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

403 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

404 
val {predicate, import, elems, params, regs} = the_locale thy name; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

405 
fun add (id', thms) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

406 
if id = id' then (id', thm :: thms) else (id', thms); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

407 
in 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

408 
put_locale name {predicate = predicate, import = import, 
18137  409 
elems = elems, params = params, regs = map add regs} thy 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

410 
end; 
15596  411 

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

412 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

413 
(* printing of registrations *) 
15596  414 

17138  415 
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt = 
15596  416 
let 
15703  417 
val ctxt = mk_ctxt thy_ctxt; 
418 
val thy = ProofContext.theory_of ctxt; 

419 

420 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

421 
fun prt_inst ts = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

422 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

423 
fun prt_attn (prfx, atts) = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

424 
Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts); 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

425 
fun prt_thm (_, th) = Pretty.quote (ProofContext.pretty_thm ctxt th); 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

426 
fun prt_thms thms = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

427 
Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms)); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

428 
fun prt_reg (ts, (("", []), thms)) = 
17138  429 
if show_wits 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

430 
then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms] 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

431 
else prt_inst ts 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

432 
 prt_reg (ts, (attn, thms)) = 
17138  433 
if show_wits 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

434 
then Pretty.block ((prt_attn attn @ 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

435 
[Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk, 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

436 
prt_thms thms])) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

437 
else Pretty.block ((prt_attn attn @ 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

438 
[Pretty.str ":", Pretty.brk 1, prt_inst ts])); 
15703  439 

16458  440 
val loc_int = intern thy loc; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

441 
val regs = get_regs thy_ctxt; 
17412  442 
val loc_regs = Symtab.lookup regs loc_int; 
15596  443 
in 
444 
(case loc_regs of 

17355  445 
NONE => Pretty.str ("no interpretations in " ^ msg) 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

446 
 SOME r => let 
15837  447 
val r' = Registrations.dest r; 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

448 
val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; 
17355  449 
in Pretty.big_list ("interpretations in " ^ msg ^ ":") 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

450 
(map prt_reg r'') 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

451 
end) 
15596  452 
> Pretty.writeln 
453 
end; 

454 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

455 
val print_global_registrations = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

456 
gen_print_registrations (#3 o GlobalLocalesData.get) 
15703  457 
ProofContext.init "theory"; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

458 
val print_local_registrations' = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

459 
gen_print_registrations LocalLocalesData.get 
15703  460 
I "context"; 
17138  461 
fun print_local_registrations show_wits loc ctxt = 
462 
(print_global_registrations show_wits loc (ProofContext.theory_of ctxt); 

463 
print_local_registrations' show_wits loc ctxt); 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

464 

15596  465 

12277  466 
(* diagnostics *) 
12273  467 

12277  468 
fun err_in_locale ctxt msg ids = 
469 
let 

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

471 
fun prt_id (name, parms) = 
16458  472 
[Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; 
15570  473 
val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  474 
val err_msg = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

18678  478 
in error err_msg end; 
12063  479 

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

480 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  481 

482 

12046  483 

18137  484 
(** witnesses  protected facts **) 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

485 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

486 
fun assume_protected thy t = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

487 
(t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

488 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

489 
fun prove_protected thy t tac = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

490 
(t, Goal.prove thy [] [] (Logic.protect t) (fn _ => 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

491 
Tactic.rtac Drule.protectI 1 THEN tac)); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

492 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

493 
val conclude_protected = Goal.conclude #> Goal.norm_hhf; 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

494 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

495 
fun satisfy_protected pths thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

496 
let 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

497 
fun satisfy chyp = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

498 
(case find_first (fn (t, _) => Thm.term_of chyp aconv t) pths of 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

499 
NONE => I 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

500 
 SOME (_, th) => Drule.implies_intr_protected [chyp] #> Goal.comp_hhf th); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

501 
in fold satisfy (#hyps (Thm.crep_thm thm)) thm end; 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

502 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

503 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

504 

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

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

506 

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

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

508 

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

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

510 
let 
16861  511 
val tvars = rev (fold Term.add_tvarsT Ts []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

512 
val tfrees = map TFree 
14695  513 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
18343  514 
in map (fn ((xi, S), T) => (xi, (S, T))) (tvars ~~ tfrees) end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

515 

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

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

517 
let 
18343  518 
fun paramify NONE i = (NONE, i) 
519 
 paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); 

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

520 

18343  521 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
522 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

16947  523 
val thy = ProofContext.theory_of ctxt; 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

524 

18190  525 
fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env 
526 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

527 
 unify _ env = env; 

528 
val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); 

15570  529 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 
530 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs)); 

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

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

532 

17496  533 
fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)); 
534 
fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss)); 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

535 
fun params_syn_of syn elemss = 
17496  536 
gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) > 
18343  537 
map (apfst (fn x => (x, the (Symtab.lookup syn x)))); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

538 

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

539 

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

540 
(* CB: param_types has the following type: 
15531  541 
('a * 'b option) list > ('a * 'b) list *) 
15570  542 
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

543 

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

544 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

545 
fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

546 
handle Symtab.DUPS xs => err_in_locale ctxt 
16105  547 
("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

548 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

549 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

550 
(* Distinction of assumed vs. derived identifiers. 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

551 
The former may have axioms relating assumptions of the context to 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

552 
assumptions of the specification fragment (for locales with 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

553 
predicates). The latter have witness theorems relating assumptions of the 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

554 
specification fragment to assumptions of other (assumed) specification 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

555 
fragments. *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

556 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

557 
datatype 'a mode = Assumed of 'a  Derived of 'a; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

558 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

559 
fun map_mode f (Assumed x) = Assumed (f x) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

560 
 map_mode f (Derived x) = Derived (f x); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

561 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

562 

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

563 
(* flatten expressions *) 
11896  564 

12510  565 
local 
12502  566 

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

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

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

569 
val param_decls = 
15570  570 
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

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

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

573 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
15531  574 
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

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

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

578 

18137  579 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  580 
let 
16458  581 
val thy = ProofContext.theory_of ctxt; 
12502  582 
val maxidx = length raw_parmss; 
583 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

584 

585 
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

586 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  587 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  588 

18137  589 
fun unify T U envir = Sign.typ_unify thy (U, T) envir 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

590 
handle Type.TUNIFY => 
18137  591 
let val prt = Sign.string_of_typ thy in 
592 
raise TYPE ("unify_parms: failed to unify types " ^ 

593 
prt U ^ " and " ^ prt T, [U, T], []) 

594 
end; 

595 
fun unify_list (T :: Us) = fold (unify T) Us 

596 
 unify_list [] = I; 

597 
val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_multi parms))) 

598 
(Vartab.empty, maxidx); 

12502  599 

17496  600 
val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms); 
12502  601 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); 
602 

603 
fun inst_parms (i, ps) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

604 
foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) 
15570  605 
> List.mapPartial (fn (a, S) => 
12502  606 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
18137  607 
in if T = TFree (a, S) then NONE else SOME (a, T) end) 
608 
> Symtab.make; 

609 
in map inst_parms idx_parmss end; 

12502  610 

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

611 
in 
12502  612 

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

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

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

615 
 unify_elemss ctxt fixed_parms elemss = 
12502  616 
let 
18137  617 
val thy = ProofContext.theory_of ctxt; 
17756  618 
val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

619 
fun inst ((((name, ps), mode), elems), env) = 
18137  620 
(((name, map (apsnd (Option.map (Element.instT_type env))) ps), 
621 
map_mode (map (fn (t, th) => 

622 
(Element.instT_term env t, Element.instT_thm thy env th))) mode), 

623 
map (Element.instT_ctxt thy env) elems); 

12839  624 
in map inst (elemss ~~ envs) end; 
12502  625 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

626 
(* like unify_elemss, but does not touch mode, additional 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

627 
parameter c_parms for enforcing further constraints (eg. syntax) *) 
18343  628 
(* FIXME avoid code duplication *) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

629 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

630 
fun unify_elemss' _ _ [] [] = [] 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

631 
 unify_elemss' _ [] [elems] [] = [elems] 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

632 
 unify_elemss' ctxt fixed_parms elemss c_parms = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

633 
let 
18137  634 
val thy = ProofContext.theory_of ctxt; 
635 
val envs = 

636 
unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms); 

17033  637 
fun inst ((((name, ps), (ps', mode)), elems), env) = 
18137  638 
(((name, map (apsnd (Option.map (Element.instT_type env))) ps), (ps', mode)), 
639 
map (Element.instT_ctxt thy env) elems); 

18343  640 
in map inst (elemss ~~ Library.take (length elemss, envs)) end; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

641 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

642 

15596  643 
(* flatten_expr: 
644 
Extend list of identifiers by those new in locale expression expr. 

645 
Compute corresponding list of lists of locale elements (one entry per 

646 
identifier). 

647 

648 
Identifiers represent locale fragments and are in an extended form: 

649 
((name, ps), (ax_ps, axs)) 

650 
(name, ps) is the locale name with all its parameters. 

651 
(ax_ps, axs) is the locale axioms with its parameters; 

652 
axs are always taken from the top level of the locale hierarchy, 

653 
hence axioms may contain additional parameters from later fragments: 

654 
ps subset of ax_ps. axs is either singleton or empty. 

655 

656 
Elements are enriched by identifierlike information: 

657 
(((name, ax_ps), axs), elems) 

658 
The parameters in ax_ps are the axiom parameters, but enriched by type 

659 
info: now each entry is a pair of string and typ option. Axioms are 

660 
typeinstantiated. 

661 

662 
*) 

663 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

664 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  665 
let 
666 
val thy = ProofContext.theory_of ctxt; 

12263  667 

15531  668 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
669 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  670 
 renaming [] _ = [] 
18678  671 
 renaming xs [] = error ("Too many arguments in renaming: " ^ 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

672 
commas (map (fn NONE => "_"  SOME x => quote (fst x)) xs)); 
12289  673 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

674 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
18137  675 
let val ps' = map (Element.rename ren) ps in 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

676 
(case duplicates ps' of 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

677 
[] => ((name, ps'), 
18137  678 
if top then (map (Element.rename ren) parms, 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

679 
map_mode (map (fn (t, th) => 
18137  680 
(Element.rename_term ren t, Element.rename_thm ren th))) mode) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

681 
else (parms, mode)) 
12289  682 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 
683 
end; 

12263  684 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

685 
(* add registrations of (name, ps), recursively; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

686 
adjust hyps of witness theorems *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

687 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

688 
fun add_regs (name, ps) (ths, ids) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

689 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

690 
val {params, regs, ...} = the_locale thy name; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

691 
val ps' = map #1 (#1 params); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

692 
val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

693 
(* dummy syntax, since required by rename *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

694 
val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps'); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

695 
val [env] = unify_parms ctxt ps [map (apsnd SOME) ps'']; 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

696 
(* propagate parameter types, to keep them consistent *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

697 
val regs' = map (fn ((name, ps), ths) => 
18137  698 
((name, map (Element.rename ren) ps), ths)) regs; 
17496  699 
val new_regs = gen_rems (eq_fst (op =)) (regs', ids); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

700 
val new_ids = map fst new_regs; 
17485  701 
val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

702 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

703 
val new_ths = new_regs > map (fn (_, ths') => ths' > map (fn (t, th) => 
18137  704 
(t > Element.instT_term env > Element.rename_term ren, 
705 
th > Element.instT_thm thy env > Element.rename_thm ren > satisfy_protected ths))); 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

706 
val new_ids' = map (fn (id, ths) => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

707 
(id, ([], Derived ths))) (new_ids ~~ new_ths); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

708 
in 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

709 
fold add_regs new_idTs (ths @ List.concat new_ths, ids @ new_ids') 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

710 
end; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

711 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

712 
(* distribute toplevel axioms over assumed ids *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

713 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

714 
fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

715 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

716 
val {elems, ...} = the_locale thy name; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

717 
val ts = List.concat (map 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

718 
(fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

719 
 _ => []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

720 
elems); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

721 
val (axs1, axs2) = splitAt (length ts, axioms); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

722 
in (((name, parms), (all_ps, Assumed axs1)), axs2) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

723 
 axiomify all_ps (id, (_, Derived ths)) axioms = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

724 
((id, (all_ps, Derived ths)), axioms); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

725 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

726 
(* identifiers of an expression *) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

727 

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

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

730 
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

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

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

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

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

736 
the_locale thy name; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

737 
val ps = map (#1 o #1) (#1 params); 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

739 
(* acyclic import dependencies *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

740 
val ids'' = ids' @ [((name, ps), ([], Assumed []))]; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

741 
val (_, ids''') = add_regs (name, map #1 (#1 params)) ([], ids''); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

742 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

743 
val ids_ax = if top then fst 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

744 
(fold_map (axiomify ps) ids''' axioms) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

745 
else ids'''; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

746 
val syn = Symtab.make (map (apfst fst) (#1 params)); 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

748 
 identify top (Rename (e, xs)) = 
12273  749 
let 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

750 
val (ids', parms', syn') = identify top e; 
12839  751 
val ren = renaming xs parms' 
18678  752 
handle ERROR msg => err_in_locale' ctxt msg ids'; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

753 

17496  754 
val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); 
15570  755 
val parms'' = distinct (List.concat (map (#2 o #1) ids'')); 
18137  756 
val syn'' = syn' > Symtab.dest > map (Element.rename_var ren) > Symtab.make; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

757 
(* check for conflicting syntax? *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

759 
 identify top (Merge es) = 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

760 
fold (fn e => fn (ids, parms, syn) => 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

761 
let 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

762 
val (ids', parms', syn') = identify top e 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

763 
in 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

764 
(merge_alists ids ids', 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

765 
merge_lists parms parms', 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

766 
merge_syntax ctxt ids' (syn, syn')) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

767 
end) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

768 
es ([], [], Symtab.empty); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

769 

12014  770 

18137  771 
(* CB: enrich identifiers by parameter types and 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

772 
the corresponding elements (with renamed parameters), 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

773 
also takes care of parameter syntax *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

774 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

775 
fun eval syn ((name, xs), axs) = 
12273  776 
let 
13308  777 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

778 
val ps' = map (apsnd SOME o #1) ps; 
18671  779 
fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE  opt => opt); 
780 
val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs; 

13308  781 
val (params', elems') = 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

782 
if null ren then ((ps', qs), map #1 elems) 
18137  783 
else ((map (apfst (Element.rename ren)) ps', map (Element.rename ren) qs), 
784 
map (Element.rename_ctxt ren o #1) elems); 

785 
val elems'' = elems' > map (Element.map_ctxt 

786 
{var = I, typ = I, term = I, fact = I, attrib = I, 

787 
name = NameSpace.qualified (space_implode "_" xs)}); 

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

788 
in (((name, params'), axs), elems'') end; 
12307  789 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

790 
(* type constraint for renamed parameter with syntax *) 
18343  791 
fun mixfix_type mx = 
18671  792 
SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

793 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

794 
(* compute identifiers and syntax, merge with previous ones *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

795 
val (ids, _, syn) = identify true expr; 
17496  796 
val idents = gen_rems (eq_fst (op =)) (ids, prev_idents); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

797 
val syntax = merge_syntax ctxt ids (syn, prev_syntax); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

798 
(* add types to params, check for unique params and unify them *) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

799 
val raw_elemss = unique_parms ctxt (map (eval syntax) idents); 
18671  800 
val elemss = unify_elemss' ctxt [] raw_elemss (map (apsnd mixfix_type) (Symtab.dest syntax)); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

801 
(* replace params in ids by params from axioms, 
17033  802 
adjust types in mode *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

804 
val all_params = param_types all_params'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

805 
val elemss' = map (fn (((name, _), (ps, mode)), elems) => 
17485  806 
(((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems)) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

807 
elemss; 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

808 
fun inst_th (t, th) = let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

811 
val [env] = unify_parms ctxt all_params [ps]; 
18137  812 
val t' = Element.instT_term env t; 
813 
val th' = Element.instT_thm thy env th; 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

814 
in (t', th') end; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

815 
val final_elemss = map (fn ((id, mode), elems) => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

816 
((id, map_mode (map inst_th) mode), elems)) elemss'; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

817 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

818 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  819 

12510  820 
end; 
821 

12070  822 

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

823 
(* activate elements *) 
12273  824 

12510  825 
local 
826 

18671  827 
fun axioms_export axs _ hyps = 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

828 
satisfy_protected axs 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

829 
#> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

830 
#> Seq.single; 
12263  831 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

832 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

833 
(* NB: derived ids contain only facts at this stage *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

834 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

835 
fun activate_elem _ ((ctxt, mode), Fixes fixes) = 
18671  836 
((ctxt > ProofContext.add_fixes_i fixes > snd, mode), []) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

837 
 activate_elem _ ((ctxt, mode), Constrains _) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

838 
((ctxt, mode), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

840 
let 
18728  841 
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; 
15703  842 
val ts = List.concat (map (map #1 o #2) asms'); 
843 
val (ps, qs) = splitAt (length ts, axs); 

17856  844 
val (_, ctxt') = 
18671  845 
ctxt > fold ProofContext.fix_frees ts 
846 
> ProofContext.add_assms_i (axioms_export ps) asms'; 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

847 
in ((ctxt', Assumed qs), []) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

848 
 activate_elem _ ((ctxt, Derived ths), Assumes asms) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

849 
((ctxt, Derived ths), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

850 
 activate_elem _ ((ctxt, Assumed axs), Defines defs) = 
15596  851 
let 
18728  852 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
17856  853 
val (_, ctxt') = 
18671  854 
ctxt > ProofContext.add_assms_i ProofContext.def_export 
15703  855 
(defs' > map (fn ((name, atts), (t, ps)) => 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

857 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

858 
in ((ctxt', Assumed axs), []) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

859 
 activate_elem _ ((ctxt, Derived ths), Defines defs) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

860 
((ctxt, Derived ths), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

861 
 activate_elem is_ext ((ctxt, mode), Notes facts) = 
15596  862 
let 
18728  863 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
17856  864 
val (res, ctxt') = ctxt > ProofContext.note_thmss_i facts'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

865 
in ((ctxt', mode), if is_ext then res else []) end; 
12502  866 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

867 
fun activate_elems (((name, ps), mode), elems) ctxt = 
17033  868 
let 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

869 
val thy = ProofContext.theory_of ctxt; 
17033  870 
val ((ctxt', _), res) = 
871 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems) 

18678  872 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 
15696  873 
val ctxt'' = if name = "" then ctxt' 
874 
else let 

875 
val ps' = map (fn (n, SOME T) => Free (n, T)) ps; 

876 
val ctxt'' = put_local_registration (name, ps') ("", []) ctxt' 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

877 
in case mode of 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

878 
Assumed axs => 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

879 
fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt'' 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

880 
 Derived ths => fold (add_local_witness (name, ps')) ths ctxt'' 
15696  881 
end 
16144  882 
in (ProofContext.restore_naming ctxt ctxt'', res) end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

883 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

884 
fun activate_elemss prep_facts = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

885 
fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

886 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

887 
val elems = map (prep_facts ctxt) raw_elems; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

888 
val (ctxt', res) = apsnd List.concat 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

889 
(activate_elems (((name, ps), mode), elems) ctxt); 
18137  890 
val elems' = elems > map (Element.map_ctxt 
891 
{name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure}); 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

893 

12546  894 
in 
895 

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

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

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

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

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

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

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

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

903 
from elemss and the intermediate context with prep_facts. 
15703  904 
If read_facts or cert_facts is used for prep_facts, these also remove 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

906 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

907 
fun activate_facts prep_facts (ctxt, args) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

908 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

909 
val (res, ctxt') = activate_elemss prep_facts args ctxt; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

910 
in 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

911 
(ctxt', apsnd List.concat (split_list res)) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

912 
end; 
12546  913 

15703  914 
fun activate_note prep_facts (ctxt, args) = 
915 
let 

916 
val (ctxt', ([(_, [Notes args'])], facts)) = 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

917 
activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]); 
15703  918 
in (ctxt', (args', facts)) end; 
919 

12510  920 
end; 
921 

12307  922 

15696  923 

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

925 

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

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

927 

16458  928 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
929 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

930 
 intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs); 

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

931 

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

932 

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

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

934 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

935 
(* flatten (ctxt, prep_expr) ((ids, syn), expr) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

936 
normalises expr (which is either a locale 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

938 
to the list ids of already accumulated identifiers. 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

940 
with identifiers generated for expr, and elemss is the list of 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

941 
context elements generated from expr. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

942 
syn and syn' are symtabs mapping parameter names to their syntax. syn' 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

943 
is an extension of syn. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

944 
For details, see flatten_expr. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

945 

15596  946 
Additionally, for a locale expression, the elems are grouped into a single 
947 
Int; individual context elements are marked Ext. In this case, the 

948 
identifierlike information of the element is as follows: 

949 
 for Fixes: (("", ps), []) where the ps have type info NONE 

950 
 for other elements: (("", []), []). 

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

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

952 
empty strings for external elements. 
15596  953 
*) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

954 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

955 
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let 
18137  956 
val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))] 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

957 
in 
18137  958 
((ids', 
959 
merge_syntax ctxt ids' 

960 
(syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) 

961 
handle Symtab.DUPS xs => err_in_locale ctxt 

962 
("Conflicting syntax for parameters: " ^ commas_quote xs) 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

963 
(map #1 ids')), 
18137  964 
[((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

965 
end 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

966 
 flatten _ ((ids, syn), Elem elem) = 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

967 
((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)]) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

968 
 flatten (ctxt, prep_expr) ((ids, syn), Expr expr) = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

970 

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

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

972 

12839  973 
local 
974 

12727  975 
fun declare_int_elem (ctxt, Fixes fixes) = 
18671  976 
(ctxt > ProofContext.add_fixes_i (map (fn (x, T, mx) => 
977 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) > snd, []) 

12727  978 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

979 

18671  980 
fun declare_ext_elem prep_vars (ctxt, Fixes fixes) = 
981 
let val (vars, _) = prep_vars fixes ctxt 

982 
in (ctxt > ProofContext.add_fixes_i vars > snd, []) end 

983 
 declare_ext_elem prep_vars (ctxt, Constrains csts) = 

984 
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt 

985 
in (ctxt', []) end 

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

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

987 
 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

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

989 

18671  990 
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) = 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

991 
let val (ctxt', propps) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

992 
(case elems of 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

993 
Int es => foldl_map declare_int_elem (ctxt, es) 
18671  994 
 Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e])) 
18678  995 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

996 
in (ctxt', propps) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

997 
 declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []); 
12727  998 

12839  999 
in 
1000 

18671  1001 
fun declare_elemss prep_vars fixed_params raw_elemss ctxt = 
12727  1002 
let 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1003 
(* 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

1004 
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

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

1006 
val ctxt_with_fixed = 
16028  1007 
fold ProofContext.declare_term (map Free fixed_params) ctxt; 
12727  1008 
val int_elemss = 
1009 
raw_elemss 

15570  1010 
> 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

1011 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  1012 
val (_, raw_elemss') = 
1013 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

1014 
(int_elemss, raw_elemss); 

18671  1015 
in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1016 

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

1018 

12839  1019 
local 
1020 

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

1022 

13336  1023 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  1024 
let 
1025 
val body = Term.strip_all_body eq; 

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

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

18343  1028 
val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs); 
13336  1029 
val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs); 
1030 
in (Term.dest_Free f, eq') end; 

1031 

16458  1032 
fun abstract_thm thy eq = 
1033 
Thm.assume (Thm.cterm_of thy eq) > Drule.gen_all > Drule.abs_def; 

12502  1034 

18190  1035 
fun bind_def ctxt (name, ps) eq (xs, env, ths) = 
12839  1036 
let 
13336  1037 
val ((y, T), b) = abstract_term eq; 
13308  1038 
val b' = norm_term env b; 
16458  1039 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1040 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1041 
in 
13308  1042 
conditional (exists (equal y o #1) xs) (fn () => 
1043 
err "Attempt to define previously specified variable"); 

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

1045 
err "Attempt to redefine variable"); 

16861  1046 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 
12839  1047 
end; 
12575  1048 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1049 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1050 
(* CB: for finish_elems (Int and Ext), 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1051 
extracts specification, only of assumed elements *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1052 

18190  1053 
fun eval_text _ _ _ (Fixes _) text = text 
1054 
 eval_text _ _ _ (Constrains _) text = text 

1055 
 eval_text _ (_, Assumed _) is_ext (Assumes asms) 

1056 
(((exts, exts'), (ints, ints')), (xs, env, defs)) = 

13394  1057 
let 
15570  1058 
val ts = List.concat (map (map #1 o #2) asms); 
13394  1059 
val ts' = map (norm_term env) ts; 
1060 
val spec' = 

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

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

16861  1063 
in (spec', (fold Term.add_frees ts' xs, env, defs)) end 
18190  1064 
 eval_text _ (_, Derived _) _ (Assumes _) text = text 
1065 
 eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) = 

1066 
(spec, fold (bind_def ctxt id o #1 o #2) defs binds) 

1067 
 eval_text _ (_, Derived _) _ (Defines _) text = text 

1068 
 eval_text _ _ _ (Notes _) text = text; 

13308  1069 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1070 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1071 
(* for finish_elems (Int), 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1072 
remove redundant elements of derived identifiers, 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1073 
turn assumptions and definitions into facts, 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1074 
adjust hypotheses of facts using witness theorems *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1075 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1076 
fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1077 
 finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1078 
 finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1079 
 finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1080 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1081 
 finish_derived _ _ (Derived _) (Fixes _) = NONE 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1082 
 finish_derived _ _ (Derived _) (Constrains _) = NONE 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1083 
 finish_derived sign wits (Derived _) (Assumes asms) = asms 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1084 
> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) 
18137  1085 
> Notes > Element.map_ctxt_values I I (satisfy_protected wits) > SOME 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1086 
 finish_derived sign wits (Derived _) (Defines defs) = defs 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1087 
> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) 
18137  1088 
> Notes > Element.map_ctxt_values I I (satisfy_protected wits) > SOME 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1089 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1090 
 finish_derived _ wits _ (Notes facts) = (Notes facts) 
18137  1091 
> Element.map_ctxt_values I I (satisfy_protected wits) > SOME; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1092 

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

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

1094 

13308  1095 
fun closeup _ false elem = elem 
1096 
 closeup ctxt true elem = 

12839  1097 
let 
13308  1098 
fun close_frees t = 
1099 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

16861  1100 
(Term.add_frees t [])) 
13308  1101 
in Term.list_all_free (frees, t) end; 
1102 

1103 
fun no_binds [] = [] 

18678  1104 
 no_binds _ = error "Illegal term bindings in locale element"; 
13308  1105 
in 
1106 
(case elem of 

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

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

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

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

1111 
 e => e) 

1112 
end; 

12839  1113 

12502  1114 

12839  1115 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
17271  1116 
(x, AList.lookup (op =) parms x, mx)) fixes) 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1117 
 finish_ext_elem parms _ (Constrains csts, _) = 
18671  1118 
(* FIXME fails if x is not a parameter *) 
17271  1119 
Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts) 
12839  1120 
 finish_ext_elem _ close (Assumes asms, propp) = 
1121 
close (Assumes (map #1 asms ~~ propp)) 

1122 
 finish_ext_elem _ close (Defines defs, propp) = 

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

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1126 

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

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

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

1130 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1131 
fun finish_parms parms (((name, ps), mode), elems) = 
17485  1132 
(((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems); 
12839  1133 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1134 
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = 
12839  1135 
let 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1136 
val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1137 
val wits' = case mode of Assumed _ => wits  Derived ths => wits @ ths; 
18190  1138 
val text' = fold (eval_text ctxt id' false) es text; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1139 
val es' = List.mapPartial 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1140 
(finish_derived (ProofContext.theory_of ctxt) wits' mode) es; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1141 
in ((text', wits'), (id', map Int es')) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1142 
 finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = 
13308  1143 
let 
1144 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

18190  1145 
val text' = eval_text ctxt id true e' text; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1146 
in ((text', wits), (id, [Ext e'])) end 
12839  1147 

1148 
in 

12510  1149 

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

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

1151 

13375  1152 
fun finish_elemss ctxt parms do_close = 
1153 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1154 

1155 
end; 

1156 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1157 

1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1158 
(* CB: type inference and consistency checks for locales. 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1159 

1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1160 
Works by building a context (through declare_elemss), extracting the 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1161 
required information and adjusting the context elements (finish_elemss). 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1162 
Can also universally close free vars in assms and defs. This is only 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1163 
needed for Ext elements and controlled by parameter do_close. 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1164 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1165 
Only elements of assumed identifiers are considered. 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1166 
*) 
15127  1167 

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

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

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

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

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

1174 
(* 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

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

1177 
(* 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

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

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

1180 
external elements in raw_elemss. *) 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1181 
fun prep_prop raw_propp (raw_ctxt, raw_concl) = 
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1182 
let 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1183 
(* CB: add type information from fixed_params to context (declare_term) *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1184 
(* CB: process patterns (conclusion and external elements only) *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1185 
val (ctxt, all_propp) = 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1186 
prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1187 
(* CB: add type information from conclusion and external elements to context *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1188 
val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt; 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1189 
(* CB: resolve schematic variables (patterns) in conclusion and external elements. *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1190 
val all_propp' = map2 (curry (op ~~)) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1191 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1192 
val (concl, propp) = splitAt (length raw_concl, all_propp') 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1193 
in (propp, (ctxt, concl)) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1194 

18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1195 
val (proppss, (ctxt, concl)) = 
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1196 
(fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); 
12502  1197 

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

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

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

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

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

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

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

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

1206 
(* CB: extract information from assumes and defines elements 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1207 
(fixes, constrains and notes in raw_elemss don't have an effect on 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1208 
text and elemss), compute final form of context elements. *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1209 
val ((text, _), elemss) = finish_elemss ctxt parms do_close 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1210 
((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

1218 
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

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

1220 
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

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

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

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

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

1225 
elemss is an updated version of raw_elemss: 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1226 
 type info added to Fixes and modified in Constrains 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

1230 
*) 
13308  1231 
in ((parms, elemss, concl), text) end; 
12502  1232 

1233 
in 

1234 

18671  1235 
fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x; 
1236 
fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x; 

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

1237 

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

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

1239 

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

1240 

15703  1241 
(* facts and attributes *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1242 

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

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

1244 

18678  1245 
fun prep_name name = 
1246 
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) 

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

1248 

15703  1249 
fun prep_facts _ _ ctxt (Int elem) = 
18137  1250 
Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem 