author  ballarin 
Mon, 08 Mar 2004 12:18:19 +0100  
changeset 14446  0bc2519e9990 
parent 14291  61df18481f53 
child 14508  859b11514537 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

3 
Author: Markus Wenzel, LMU/TU Muenchen 
11896  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5 

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

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

8 

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

9 
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

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

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

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

15 
See also: 

16 

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

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

19 
Workshop, TYPES 2003, Torino, Italy, pages ????, in press. 

11896  20 
*) 
21 

22 
signature LOCALE = 

23 
sig 

12046  24 
type context 
25 
datatype ('typ, 'term, 'fact, 'att) elem = 

12058  26 
Fixes of (string * 'typ option * mixfix option) list  
12046  27 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
28 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  29 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
30 
datatype expr = 

31 
Locale of string  

32 
Rename of expr * string option list  

33 
Merge of expr list 

34 
val empty: expr 

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

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

12046  37 
type 'att element 
38 
type 'att element_i 

39 
type locale 

40 
val intern: Sign.sg > xstring > string 

12014  41 
val cond_extern: Sign.sg > string > xstring 
12502  42 
val the_locale: theory > string > locale 
12273  43 
val attribute: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 
44 
> ('typ, 'term, 'thm, context attribute) elem_expr 

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

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

46 
(string * (string list * string list)) list list > context > 
13415  47 
string option * cterm list * context * context * (term * (term list * term list)) list list 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

49 
(term * (term list * term list)) list list > context > 
13415  50 
string option * cterm list * context * context * (term * (term list * term list)) list list 
12758  51 
val print_locales: theory > unit 
52 
val print_locale: theory > expr > context attribute element list > unit 

13394  53 
val add_locale: bool > bstring > expr > context attribute element list > theory > theory 
54 
val add_locale_i: bool > bstring > expr > context attribute element_i list 

55 
> theory > theory 

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

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

12711  59 
val have_thmss: string > xstring > 
60 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 

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

62 
val have_thmss_i: string > string > 

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

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

12958  65 
val add_thmss: string > ((string * thm list) * context attribute list) list > 
13375  66 
theory * context > (theory * context) * (string * thm list) list 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

67 
val prune_prems: theory > thm > thm 
11896  68 
val setup: (theory > theory) list 
69 
end; 

12839  70 

12289  71 
structure Locale: LOCALE = 
11896  72 
struct 
73 

12273  74 
(** locale elements and expressions **) 
11896  75 

12014  76 
type context = ProofContext.context; 
11896  77 

12046  78 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  79 
Fixes of (string * 'typ option * mixfix option) list  
12046  80 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
81 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  82 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
83 

84 
datatype expr = 

85 
Locale of string  

86 
Rename of expr * string option list  

87 
Merge of expr list; 

11896  88 

12273  89 
val empty = Merge []; 
90 

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

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

93 

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

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

12070  96 

97 
type locale = 

14291  98 
{view: cterm list * thm list, 
14446  99 
(* If locale "loc" contains assumptions, either via import or in the 
100 
locale body, a locale predicate "loc" is defined capturing all the 

101 
assumptions. If both import and body contain assumptions, additionally 

102 
a delta predicate "loc_axioms" is defined that abbreviates the 

103 
assumptions of the body. 

104 
The context generated when entering "loc" contains not (necessarily) a 

105 
single assumption "loc", but a list of assumptions of all locale 

106 
predicates of locales without import and all delta predicates of 

107 
locales with import from the import hierarchy (duplicates removed, 

108 
cf. [1], normalisation of locale expressions). 

109 

110 
The first part of view in the above definition (also called statement) 

111 
represents this list of assumptions. The second part (also called 

112 
axioms) contains projections from the predicate "loc" to these 

113 
assumptions. 

114 
*) 

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

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

117 
params: (string * typ option) list * string list}; (*all/local params*) 
12063  118 

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

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

120 
{view = view, import = import, elems = elems, params = params}: locale; 
12063  121 

11896  122 

123 
(** theory data **) 

124 

125 
structure LocalesArgs = 

126 
struct 

12014  127 
val name = "Isar/locales"; 
12063  128 
type T = NameSpace.T * locale Symtab.table; 
11896  129 

12063  130 
val empty = (NameSpace.empty, Symtab.empty); 
131 
val copy = I; 

12118  132 
val prep_ext = I; 
12289  133 

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

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

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

136 
Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); 
12273  137 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  138 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
139 

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

12014  142 
> Pretty.writeln; 
11896  143 
end; 
144 

145 
structure LocalesData = TheoryDataFun(LocalesArgs); 

146 
val print_locales = LocalesData.print; 

147 

12289  148 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
149 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

150 

12277  151 

152 
(* access locales *) 

153 

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

11896  156 

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

12014  160 
fun the_locale thy name = 
161 
(case get_locale thy name of 

162 
Some loc => loc 

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

11896  164 

12046  165 

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

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

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

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

169 

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

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

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

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

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

174 
(case get_locale thy name of 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

175 
None => false 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

176 
 Some {import, ...} => imps import low) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

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

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

182 

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

183 
(** Name suffix of internal delta predicates. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

184 
These specify additional assumptions in a locale with import. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

185 
Also name of theorem set with destruct rules for locale main 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

186 
predicates. **) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

187 

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

188 
val axiomsN = "axioms"; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

189 

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

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

191 

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

192 
(* A trielike structure is used to compute a cover of a normalised 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

193 
locale specification. Entries of the trie will be identifiers: 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

194 
locale names with parameter lists. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

195 

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

196 
datatype 'a trie = Trie of ('a * 'a trie) list; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

197 

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

198 
(* Subsumption relation on identifiers *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

199 

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

200 
fun subsumes thy ((name1, args1), (name2, args2)) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

201 
(name2 = "" andalso null args2) orelse 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

202 
((name2 = name1 orelse imports thy (name1, name2)) andalso 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

203 
(args2 prefix args1)); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

204 

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

205 
(* Insert into trie, wherever possible but avoiding branching *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

206 

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

207 
fun insert_ident subs id (Trie trie) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

209 
fun insert id [] = [(id, Trie [])] 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

210 
 insert id ((id', Trie t')::ts) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

211 
if subs (id, id') 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

212 
then if null ts 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

213 
then [(id', Trie (insert id t'))] (* avoid new branch *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

214 
else (id', Trie (insert id t'))::insert id ts 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

215 
else (id', Trie t')::insert id ts 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

216 
in Trie (insert id trie) end; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

217 

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

218 
(* List of leaves of a trie, removing duplicates *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

219 

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

220 
fun leaves _ (Trie []) = [] 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

221 
 leaves eq (Trie ((id, Trie [])::ts)) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

222 
gen_ins eq (id, leaves eq (Trie ts)) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

223 
 leaves eq (Trie ((id, ts')::ts)) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

224 
gen_merge_lists eq (leaves eq ts') (leaves eq (Trie ts)); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

225 

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

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

227 

14291  228 
(** Prune premises: 
229 
Remove internal delta predicates (generated by "includes") from the 

230 
premises of a theorem. 

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

231 

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

232 
Assumes no outer quanfifiers and no flexflex pairs. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

233 
May change names of TVars. 
14291  234 
Performs compress and close_derivation on result, if modified. **) 
235 

236 
(* Note: reconstruction of the correct premises fails for subspace_normed_vs 

237 
in HOL/Real/HahnBanach/NormedSpace.thy. This cannot be fixed since in the 

238 
current setup there is no way of distinguishing whether the theorem 

239 
statement involved "includes subspace F E + normed_vectorspace E" or 

240 
"includes subspace F E + vectorspace E + norm E norm". 

241 
*) 

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

242 

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

243 
fun prune_prems thy thm = let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

245 
fun analyse cprem = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

246 
(* Returns None if head of premise is not a predicate defined by a locale, 
14291  247 
returns also None if locale has a view but predicate is not *_axioms 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

248 
since this is a premise that wasn't generated by includes. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

249 
case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

250 
(Const (raw_name, T), args) => let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

251 
val name = unsuffix ("_" ^ axiomsN) raw_name 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

252 
handle LIST _ => raw_name 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

253 
in case get_locale thy name of 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

254 
None => None 
14291  255 
 Some {view = (_, axioms), ...} => 
256 
if name = raw_name andalso not (null axioms) 

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

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

258 
else Some (((name, args), T), name = raw_name) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

260 
 _ => None; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

261 
val TFrees = add_term_tfree_names (prop_of thm, []); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

262 
(* Ignores TFrees in flexflex pairs ! *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

263 
val (frozen, thaw) = Drule.freeze_thaw thm; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

264 
val cprop = cprop_of frozen; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

265 
val cprems = Drule.strip_imp_prems cprop; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

266 
val analysis = map analyse cprems; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

268 
if foldl (fn (b, None) => b  (b, Some (_, b')) => b andalso b') 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

269 
(true, analysis) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

270 
then thm (* No premise contains *_axioms predicate 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

271 
==> no changes necessary. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

273 
val ids = map (apsome fst) analysis; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

274 
(* Analyse dependencies of locale premises: store in trie. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

275 
fun subs ((x, _), (y, _)) = subsumes thy (x, y); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

276 
val Trie depcs = foldl (fn (trie, None) => trie 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

277 
 (trie, Some id) => insert_ident subs id trie) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

278 
(Trie [], ids); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

279 
(* Assemble new theorem; new prems will be hyps. 
14291  280 
Axioms is an intermediate list of locale axioms required to 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

281 
replace old premises by new ones. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

282 
fun scan ((roots, thm, cprems', axioms), (cprem, id)) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

284 
None => (roots, implies_elim thm (assume cprem), 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

285 
cprems' @ [cprem], []) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

286 
(* Normal premise: keep *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

287 
 Some id => (* Locale premise *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

289 
fun elim_ax [] thm = (* locale has no axioms *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

290 
implies_elim thm (assume cprem) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

291 
 elim_ax axs thm = let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

292 
(* Eliminate first premise of thm, which is of the form 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

293 
id. Add hyp of the used axiom to thm. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

294 
val ax = the (assoc (axs, fst (fst id))) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

295 
handle _ => error ("Internal error in Locale.prune_\ 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

296 
\prems: axiom for premise" ^ 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

297 
fst (fst id) ^ " not found."); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

298 
val [ax_cprem] = Drule.strip_imp_prems (cprop_of ax) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

299 
handle _ => error ("Internal error in Locale.prune_\ 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

300 
\prems: exactly one premise in axiom expected."); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

301 
val ax_hyp = implies_elim ax (assume (ax_cprem)) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

302 
in implies_elim thm ax_hyp 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

306 
then (roots, elim_ax axioms thm, cprems', axioms) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

307 
(* Remaining premise: drop *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

309 
fun mk_cprem ((name, args), T) = cterm_of sign 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

310 
(ObjectLogic.assert_propT sign 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

311 
(Term.list_comb (Const (name, T), args))); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

312 
fun get_axs ((name, args), _) = let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

313 
val {view = (_, axioms), ...} = the_locale thy name; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

314 
fun inst ax = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

316 
val std = standard ax; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

317 
val (prem, concl) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

318 
Logic.dest_implies (prop_of std); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

319 
val (Const (name2, _), _) = Term.strip_comb 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

320 
(ObjectLogic.drop_judgment sign concl); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

321 
val (_, vars) = Term.strip_comb 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

322 
(ObjectLogic.drop_judgment sign prem); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

323 
val cert = map (cterm_of sign); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

324 
in (unsuffix ("_" ^ axiomsN) name2 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

325 
handle LIST _ => name2, 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

326 
cterm_instantiate (cert vars ~~ cert args) std) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

328 
in map inst axioms end; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

329 
val (id', trie) = hd roots; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

330 
in if id = id' 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

331 
then (* Initial premise *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

333 
val lvs = leaves eq_fst (Trie [(id', trie)]); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

334 
val axioms' = flat (map get_axs lvs) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

335 
in (tl roots, elim_ax axioms' thm, 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

336 
cprems' @ map (mk_cprem) lvs, axioms') 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

338 
else (roots, elim_ax axioms thm, cprems', axioms) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

339 
(* Remaining premise: drop *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

342 
val (_, thm', cprems', _) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

343 
(foldl scan ((depcs, frozen, [], []), cprems ~~ ids)); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

344 
val thm'' = implies_intr_list cprems' thm'; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

346 
fst (varifyT' TFrees (thaw thm'')) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

347 
> Thm.compress > Drule.close_derivation 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

350 

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

351 
end (* local *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

352 

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

353 

12277  354 
(* diagnostics *) 
12273  355 

12277  356 
fun err_in_locale ctxt msg ids = 
357 
let 

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

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

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

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

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

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

12063  367 

12277  368 

369 

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

370 
(** primitives **) 
12046  371 

12277  372 
(* renaming *) 
12263  373 

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

375 

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

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

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

379 
 rename_term _ a = a; 

380 

381 
fun rename_thm ren th = 

382 
let 

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

384 
val cert = Thm.cterm_of sign; 

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

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

389 
in 

390 
if xs = xs' then th 

391 
else 

392 
th 

393 
> Drule.implies_intr_list (map cert hyps) 

394 
> Drule.forall_intr_list (cert_frees xs) 

395 
> Drule.forall_elim_list (cert_vars xs) 

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

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

398 
end; 

399 

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

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

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

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

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

404 
end)) 
12263  405 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
406 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  409 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  410 

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

411 
fun rename_facts prfx elem = 
12307  412 
let 
12323  413 
fun qualify (arg as ((name, atts), x)) = 
13394  414 
if prfx = "" orelse name = "" then arg 
13375  415 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  416 
in 
417 
(case elem of 

418 
Fixes fixes => Fixes fixes 

419 
 Assumes asms => Assumes (map qualify asms) 

420 
 Defines defs => Defines (map qualify defs) 

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

422 
end; 

423 

12263  424 

12502  425 
(* type instantiation *) 
426 

427 
fun inst_type [] T = T 

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

429 

430 
fun inst_term [] t = t 

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

432 

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

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

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

436 
val sign = ProofContext.sign_of ctxt; 
12575  437 
val cert = Thm.cterm_of sign; 
438 
val certT = Thm.ctyp_of sign; 

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

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

12502  442 
in 
443 
if null env' then th 

444 
else 

445 
th 

446 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

452 
end; 

453 

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

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

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

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

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

461 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  462 

463 

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

464 

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

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

466 

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

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

468 

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

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

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

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

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

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

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

475 

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

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

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

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

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

480 

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

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

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

484 

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

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

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

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

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

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

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

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

493 

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

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

496 

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

497 

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

498 
(* flatten expressions *) 
11896  499 

12510  500 
local 
12502  501 

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

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

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

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

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

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

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

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

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

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

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

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

513 

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

514 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  515 
let 
516 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

517 
val maxidx = length raw_parmss; 

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

519 

520 
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

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

522 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  523 

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

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

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

528 
val (unifier, _) = foldl unify_list 

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

530 

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

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

533 

534 
fun inst_parms (i, ps) = 

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

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

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

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

538 
in if T = TFree (a, S) then None else Some ((a, S), T) end) 
12502  539 
in map inst_parms idx_parmss end; 
540 

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

541 
in 
12502  542 

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

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

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

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

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

12839  550 
in map inst (elemss ~~ envs) end; 
12502  551 

12575  552 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  553 
let 
554 
val thy = ProofContext.theory_of ctxt; 

12263  555 

12289  556 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
557 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

561 

562 
fun rename_parms ren (name, ps) = 

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

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

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

566 
end; 

12263  567 

12273  568 
fun identify ((ids, parms), Locale name) = 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

569 
(* CB: ids is list of pairs: locale name and list of parameter renamings, 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

570 
parms is accumulated list of parameters *) 
12289  571 
let 
572 
val {import, params, ...} = the_locale thy name; 

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

574 
in 

12273  575 
if (name, ps) mem ids then (ids, parms) 
12277  576 
else 
12289  577 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
578 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  579 
end 
580 
 identify ((ids, parms), Rename (e, xs)) = 

581 
let 

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

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

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

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

12273  588 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  589 

12307  590 
fun eval (name, xs) = 
12273  591 
let 
13308  592 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  593 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  594 
val (params', elems') = 
595 
if null ren then ((ps, qs), map #1 elems) 

12502  596 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  597 
map (rename_elem ren o #1) elems); 
13375  598 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  599 
in ((name, params'), elems'') end; 
12307  600 

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

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

603 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  604 
in (prev_idents @ idents, elemss) end; 
12046  605 

12510  606 
end; 
607 

12070  608 

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

609 
(* activate elements *) 
12273  610 

12510  611 
local 
612 

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

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

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

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

616 
> Seq.single; 
12263  617 

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

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

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

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

621 
val ts = flat (map (map #1 o #2) asms); 
13629  622 
val (ps,qs) = splitAt (length ts, axs) 
13420  623 
val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

624 
ctxt > ProofContext.fix_frees ts 
13629  625 
> ProofContext.assume_i (export_axioms ps) asms; 
626 
in ((ctxt', qs), []) end 

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

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

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

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

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

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

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

635 
let val (ctxt', res) = ctxt > ProofContext.have_thmss_i facts 
13420  636 
in ((ctxt', axs), if is_ext then res else []) end; 
12502  637 

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

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

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

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

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

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

643 

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

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

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

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

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

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

649 

12546  650 
in 
651 

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

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

653 
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); 
12546  654 

12510  655 
end; 
656 

12307  657 

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

658 

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

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

660 

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

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

662 

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

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

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

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

666 

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

667 

12546  668 
(* attributes *) 
669 

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

671 

14446  672 
(* Map attrib over 
673 
* A context element: add attrib to attribute lists of assumptions, 

674 
definitions and facts (on both sides for facts). 

675 
* Locale expression: no effect. *) 

676 

677 

12546  678 
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) 
679 
 attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) 

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

681 
 attribute attrib (Elem (Notes facts)) = 

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

683 
 attribute _ (Expr expr) = Expr expr; 

684 

685 
end; 

686 

687 

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

688 
(* parameters *) 
12502  689 

690 
local 

691 

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

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

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

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

695 

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

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

697 

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

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

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

700 

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

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

702 

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

703 

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

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

705 

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

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

707 

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

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

709 

12839  710 
local 
711 

12727  712 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  713 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  714 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
715 
 declare_int_elem (ctxt, _) = (ctxt, []); 

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

716 

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

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

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

720 
 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

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

722 

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

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

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

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

12839  731 
in 
732 

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

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

734 

12727  735 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
736 
let 

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

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

738 
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

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

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

741 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  742 
val int_elemss = 
743 
raw_elemss 

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

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

745 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  746 
val (_, raw_elemss') = 
747 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

748 
(int_elemss, raw_elemss); 

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

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

750 

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

752 

12839  753 
local 
754 

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

756 

13336  757 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  758 
let 
759 
val body = Term.strip_all_body eq; 

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

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

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

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

765 

766 
fun abstract_thm sign eq = 

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

12502  768 

13336  769 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  770 
let 
13336  771 
val ((y, T), b) = abstract_term eq; 
13308  772 
val b' = norm_term env b; 
13336  773 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  774 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  775 
in 
13308  776 
conditional (exists (equal y o #1) xs) (fn () => 
777 
err "Attempt to define previously specified variable"); 

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

779 
err "Attempt to redefine variable"); 

13336  780 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  781 
end; 
12575  782 

13308  783 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  784 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
785 
let 

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

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

788 
val spec' = 

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

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

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

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

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

795 

796 
fun closeup _ false elem = elem 

797 
 closeup ctxt true elem = 

12839  798 
let 
13308  799 
fun close_frees t = 
800 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

803 

804 
fun no_binds [] = [] 

805 
 no_binds _ = 

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

807 
in 

808 
(case elem of 

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

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

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

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

813 
 e => e) 

814 
end; 

12839  815 

12502  816 

12839  817 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  818 
(x, assoc_string (parms, x), mx)) fixes) 
12839  819 
 finish_ext_elem _ close (Assumes asms, propp) = 
820 
close (Assumes (map #1 asms ~~ propp)) 

821 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

827 

13375  828 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  829 
let 
13308  830 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
831 
val text' = foldl (eval_text ctxt id false) (text, es); 

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

13375  833 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  834 
let 
835 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  836 
val text' = eval_text ctxt id true (text, e'); 
13308  837 
in (text', (id, [Ext e'])) end; 
12839  838 

839 
in 

12510  840 

13375  841 
fun finish_elemss ctxt parms do_close = 
842 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  843 

844 
end; 

845 

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

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

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

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

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

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

853 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  854 

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

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

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

858 
val propps = unflat raw_propps propp; 
12839  859 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  860 

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

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

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

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

865 
val parms = param_types (xs ~~ typing); 
12273  866 

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

13308  869 
in ((parms, elemss, concl), text) end; 
12502  870 

871 
in 

872 

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

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

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

875 

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

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

877 

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

878 

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

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

880 

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

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

882 

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

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

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

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

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

887 

13375  888 
fun prep_facts _ _ (Int elem) = elem 
889 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

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

894 

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

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

896 

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

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

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

899 

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

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

901 

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

902 

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

904 

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

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

906 

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

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

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

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

910 
val sign = ProofContext.sign_of context; 
13375  911 

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

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

915 
 flatten (ids, Expr expr) = 

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

917 

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

919 
(* CB: normalise "includes" among elements *) 
12575  920 
val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements)))); 
13375  921 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  922 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
13629  923 
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss) 
13420  924 
val ((import_ctxt, axioms'), (import_elemss, _)) = 
13629  925 
activate_facts prep_facts ((context, axioms), ps); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

926 

13420  927 
val ((ctxt, _), (elemss, _)) = 
13629  928 
activate_facts prep_facts ((import_ctxt, axioms'), qs); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

931 
end; 
12529
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 
val gen_context = prep_context_statement intern_expr read_elemss get_facts; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

935 

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

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

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

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

939 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
13415  940 
val ((view_statement, view_axioms), fixed_params, import) = 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

941 
(* view_axioms are xxx.axioms of locale xxx *) 
13415  942 
(case locale of None => (([], []), [], empty) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

943 
 Some name => 
13420  944 
let val {view, params = (ps, _), ...} = the_locale thy name 
945 
in (view, param_types ps, Locale name) end); 

12730  946 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') = 
13415  947 
prep_ctxt false view_axioms fixed_params import elems concl ctxt; 
948 
in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end; 

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

949 

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

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

951 

14216
a15951091d5d
Removed garbage accidentally left behind in file.
ballarin
parents:
14215
diff
changeset

952 
(* CB: arguments are: x>import, y>body (elements?), z>context *) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

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

955 

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

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

957 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  958 

959 
end; 

11896  960 

961 

962 

13336  963 
(** define locales **) 
964 

965 
(* print locale *) 

12070  966 

12758  967 
fun print_locale thy import body = 
12070  968 
let 
12289  969 
val thy_ctxt = ProofContext.init thy; 
13420  970 
val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt; 
13375  971 
val all_elems = flat (map #2 (import_elemss @ elemss)); 
12070  972 

12307  973 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
974 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  976 

977 
fun prt_syn syn = 

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

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

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

983 

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

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

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

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

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

12070  990 

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

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

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

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

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

12277  997 
in 
13336  998 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
999 
> Pretty.writeln 

12277  1000 
end; 
12070  1001 

1002 

12730  1003 
(* store results *) 
11896  1004 

12706  1005 
local 
1006 

12702  1007 
fun hide_bound_names names thy = 
1008 
thy > PureThy.hide_thms false 

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

1010 

12958  1011 
in 
1012 

13375  1013 
fun have_thmss_qualified kind name args thy = 
12706  1014 
thy 
13375  1015 
> Theory.add_path (Sign.base_name name) 
12711  1016 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  1017 
>> hide_bound_names (map (#1 o #1) args) 
1018 
>> Theory.parent_path; 

1019 

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

1022 

1023 
end; 

1024 

1025 
local 

1026 

1027 
fun put_facts loc args thy = 

1028 
let 

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

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

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

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

12706  1034 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
1035 
let 

1036 
val thy_ctxt = ProofContext.init thy; 

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

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

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

1040 
val export = ProofContext.export_standard view loc_ctxt thy_ctxt; 
12711  1041 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  1042 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
1043 
in 

1044 
thy 

1045 
> put_facts loc args 

1046 
> have_thmss_qualified kind loc args' 

1047 
end; 

1048 

1049 
in 

1050 

12711  1051 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
1052 
val have_thmss_i = gen_have_thmss (K I) (K I); 

1053 

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

13336  1057 
val thy' = put_facts loc args' thy; 
13415  1058 
val {view = (_, view_axioms), ...} = the_locale thy loc; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

1059 
val ((ctxt', _), (_, facts')) = 
13420  1060 
activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]); 
1061 
in ((thy', ctxt'), facts') end; 

12702  1062 

12706  1063 
end; 
12063  1064 

11896  1065 

13336  1066 
(* predicate text *) 
1067 

13375  1068 
local 
1069 

1070 
val introN = "intro"; 

1071 

1072 
fun atomize_spec sign ts = 

1073 
let 

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

1075 
val body = ObjectLogic.atomize_term sign t; 

1076 
val bodyT = Term.fastype_of body; 

1077 
in 

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

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

1080 
end; 

1081 

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

1084 
else raise Match); 

13336  1085 

13420  1086 
fun def_pred bname parms defs ts norm_ts thy = 
13375  1087 
let 
1088 
val sign = Theory.sign_of thy; 

1089 
val name = Sign.full_name sign bname; 

1090 

13420  1091 
val (body, bodyT, body_eq) = atomize_spec sign norm_ts; 
13394  1092 
val env = Term.add_term_free_names (body, []); 
1093 
val xs = filter (fn (x, _) => x mem_string env) parms; 

1094 
val Ts = map #2 xs; 

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

1096 
> Library.sort_wrt #1 > map TFree; 

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

1097 
val predT = map Term.itselfT extraTs > Ts > bodyT; 
13336  1098 

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

13375  1101 
val statement = ObjectLogic.assert_propT sign head; 
1102 

1103 
val (defs_thy, [pred_def]) = 

1104 
thy 

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

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

13394  1109 

13375  1110 
val defs_sign = Theory.sign_of defs_thy; 
1111 
val cert = Thm.cterm_of defs_sign; 

1112 

13420  1113 
val intro = Tactic.prove_standard defs_sign [] norm_ts statement (fn _ => 
13375  1114 
Tactic.rewrite_goals_tac [pred_def] THEN 
1115 
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN 

13420  1116 
Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1); 
13375  1117 

1118 
val conjuncts = 

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

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

1120 
Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] 
13375  1121 
> Drule.conj_elim_precise (length ts); 
13394  1122 
val axioms = (ts ~~ conjuncts) > map (fn (t, ax) => 
13375  1123 
Tactic.prove defs_sign [] [] t (fn _ => 
1124 
Tactic.rewrite_goals_tac defs THEN 

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

13394  1126 
in (defs_thy, (statement, intro, axioms)) end; 
13375  1127 

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

13629  1130 
let val (ps,qs) = splitAt(length spec, axs) 
1131 
in (qs, (a, [(ps, [])])) end)) 

13394  1132 
 change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts)) 
1133 
 change_elem _ e = e; 

1134 

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

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

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

1138 
 x => x) > #2; 

1139 

1140 
in 

13375  1141 

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

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

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

1146 
else 

1147 
let 

13420  1148 
val aname = if Library.null ints then bname else bname ^ "_" ^ axiomsN; 
13394  1149 
val (def_thy, (statement, intro, axioms)) = 
1150 
thy > def_pred aname parms defs exts exts'; 

1151 
val elemss' = change_elemss axioms elemss @ 

13420  1152 
[(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])]; 
13394  1153 
in 
1154 
def_thy > have_thmss_qualified "" aname 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14216
diff
changeset

1155 
[((introN, []), [([intro], [])])] 
13394  1156 
> #1 > rpair (elemss', [statement]) 
1157 
end; 

1158 
val (thy'', view) = 

13420  1159 
if Library.null ints then (thy', ([], [])) 
13394  1160 
else 
1161 
let 

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

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

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

1164 
val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement; 
13394  1165 
in 
1166 
def_thy > have_thmss_qualified "" bname 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14216
diff
changeset

1167 
[((introN, []), [([intro], [])]), 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14216
diff
changeset

1168 
((axiomsN, []), [(map Drule.standard axioms, [])])] 
13415  1169 
> #1 > rpair ([cstatement], axioms) 
13394  1170 
end; 
1171 
in (thy'', (elemss', view)) end; 

13375  1172 

1173 
end; 

13336  1174 

1175 

13297  1176 
(* add_locale(_i) *) 
1177 

1178 
local 

1179 

13394  1180 
fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy = 
13297  1181 
let 
1182 
val sign = Theory.sign_of thy; 

1183 
val name = Sign.full_name sign bname; 

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

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

1186 

1187 
val thy_ctxt = ProofContext.init thy; 

13420  1188 
val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) = 
13375  1189 
prep_ctxt raw_import raw_body thy_ctxt; 
1190 
val elemss = import_elemss @ body_elemss; 

13297  1191 

13415  1192 
val (pred_thy, (elemss', view as (view_statement, view_axioms))) = 
13394  1193 
if do_pred then thy > define_preds bname text elemss 
13415  1194 
else (thy, (elemss, ([], []))); 
13375  1195 
val pred_ctxt = ProofContext.init pred_thy; 
13420  1196 

1197 
val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms), elemss'); 

13415  1198 
val export = ProofContext.export_standard view_statement ctxt pred_ctxt; 
13420  1199 
val facts' = facts > map (fn (a, ths) => ((a, []), [(map export ths, [])])); 
13297  1200 
in 
13375  1201 
pred_thy 
13420  1202 
> have_thmss_qualified "" name facts' > #1 
13297  1203 
> declare_locale name 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

1204 
> put_locale name (make_locale view (prep_expr sign raw_import) 
13394  1205 
(map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) 
13375  1206 
(params_of elemss', map #1 (params_of body_elemss))) 
13297  1207 
end; 
1208 

1209 
in 

1210 

1211 
val add_locale = gen_add_locale read_context intern_expr; 

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

1212 

13297  1213 
val add_locale_i = gen_add_locale cert_context (K I); 
1214 

1215 
end; 

1216 

1217 

12730  1218 

11896  1219 
(** locale theory setup **) 
12063  1220 

11896  1221 
val setup = 
13460
ced7a699282b
predefined locales "var" and "struct" (useful for sharing parameters);
wenzelm
parents:
13442
diff
changeset

1222 
[LocalesData.init, 
ced7a699282b
predefined locales "var" and "struct" (useful for sharing parameters);
wenzelm
parents:
13442
diff
changeset

1223 
add_locale_i true "var" empty [Elem (Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)])], 
ced7a699282b
predefined locales "var" and "struct" (useful for sharing parameters);
wenzelm
parents:
13442
diff
changeset

1224 
add_locale_i true "struct" empty [Elem (Fixes [(Syntax.internal "S", None, None)])]]; 
11896  1225 

1226 
end; 