author  ballarin 
Thu, 12 Aug 2004 10:01:09 +0200  
changeset 15127  2550a5578d39 
parent 15104  f14e0d9587be 
child 15206  09d78ec709c7 
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 

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

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

7 

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

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

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

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

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

14 
See also: 

15 

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

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

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

21 
signature LOCALE = 

22 
sig 

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

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

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

30 
Locale of string  

31 
Rename of expr * string option list  

32 
Merge of expr list 

33 
val empty: expr 

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

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

12046  36 
type 'att element 
37 
type 'att element_i 

15127  38 
type 'att elem_or_expr 
39 
type 'att elem_or_expr_i 

12046  40 
type locale 
41 
val intern: Sign.sg > xstring > string 

12014  42 
val cond_extern: Sign.sg > string > xstring 
12502  43 
val the_locale: theory > string > locale 
15127  44 
val map_attrib_elem: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem 
45 
> ('typ, 'term, 'thm, context attribute) elem 

46 
val map_attrib_elem_expr: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 

12273  47 
> ('typ, 'term, 'thm, context attribute) elem_expr 
15127  48 
val read_context_statement: xstring option > context attribute elem_or_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

49 
(string * (string list * string list)) list list > context > 
13415  50 
string option * cterm list * context * context * (term * (term list * term list)) list list 
15127  51 
val cert_context_statement: string option > context attribute elem_or_expr_i list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

52 
(term * (term list * term list)) list list > context > 
13415  53 
string option * cterm list * context * context * (term * (term list * term list)) list list 
12758  54 
val print_locales: theory > unit 
55 
val print_locale: theory > expr > context attribute element list > unit 

13394  56 
val add_locale: bool > bstring > expr > context attribute element list > theory > theory 
57 
val add_locale_i: bool > bstring > expr > context attribute element_i list 

58 
> theory > theory 

14564  59 
val smart_note_thmss: string > (string * 'a) Library.option > 
12958  60 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 
61 
theory > theory * (bstring * thm list) list 

14564  62 
val note_thmss: string > xstring > 
12711  63 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 
64 
theory > theory * (bstring * thm list) list 

14564  65 
val note_thmss_i: string > string > 
12711  66 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 
67 
theory > theory * (bstring * thm list) list 

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

70 
val prune_prems: theory > thm > thm 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

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

72 
> thm list option > context > context 
11896  73 
val setup: (theory > theory) list 
74 
end; 

12839  75 

12289  76 
structure Locale: LOCALE = 
11896  77 
struct 
78 

12273  79 
(** locale elements and expressions **) 
11896  80 

12014  81 
type context = ProofContext.context; 
11896  82 

12046  83 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  84 
Fixes of (string * 'typ option * mixfix option) list  
12046  85 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
86 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  87 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
88 

89 
datatype expr = 

90 
Locale of string  

91 
Rename of expr * string option list  

92 
Merge of expr list; 

11896  93 

12273  94 
val empty = Merge []; 
95 

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

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

98 

15127  99 
type 'att element = (string, string, string, 'att) elem; 
100 
type 'att element_i = (typ, term, thm list, 'att) elem; 

101 
type 'att elem_or_expr = (string, string, string, 'att) elem_expr; 

102 
type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr; 

12070  103 

104 
type locale = 

14291  105 
{view: cterm list * thm list, 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

106 
(* CB: If locale "loc" contains assumptions, either via import or in the 
14446  107 
locale body, a locale predicate "loc" is defined capturing all the 
108 
assumptions. If both import and body contain assumptions, additionally 

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

110 
assumptions of the body. 

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

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

113 
predicates of locales without import and all delta predicates of 

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

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

116 

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

117 
The record entry view is either ([], []) or ([statement], axioms) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

118 
where statement is the predicate "loc" applied to the parameters, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

119 
and axioms contains projections from "loc" to the list of assumptions 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

120 
generated when entering the locale. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

121 
It appears that an axiom of the form A [A] is never generated. 
14446  122 
*) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

123 
import: expr, (*dynamic import*) 
12289  124 
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) 
15127  125 
params: (string * typ option) list * string list, (*all/local params*) 
126 
typing: (string * typ) list}; (*inferred parameter types, currently unused*) 

12063  127 

11896  128 

129 
(** theory data **) 

130 

131 
structure LocalesArgs = 

132 
struct 

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

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

12118  138 
val prep_ext = I; 
12289  139 

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

15127  141 
fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) = 
142 
Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems', 

143 
params = params, typing = typing}; 

12273  144 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  145 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
146 

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

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

152 
structure LocalesData = TheoryDataFun(LocalesArgs); 

153 
val print_locales = LocalesData.print; 

154 

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

157 

12277  158 

159 
(* access locales *) 

160 

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

11896  163 

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

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

169 
Some loc => loc 

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

11896  171 

12046  172 

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

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

174 
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

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

176 

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

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

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

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

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

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

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

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

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

185 
 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

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

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

188 
end; 
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 
(** Name suffix of internal delta predicates. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

192 
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

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

194 

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

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

196 

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

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

198 

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

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

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

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

202 

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

203 
datatype 'a trie = Trie of ('a * 'a trie) list; 
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 
(* Subsumption relation on identifiers *) 
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 subsumes thy ((name1, args1), (name2, args2)) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

211 

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

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

213 

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

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

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

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

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

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

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

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

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

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

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

224 

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

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

226 

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

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

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

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

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

231 
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

232 

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

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

234 

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

237 
premises of a theorem. 

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

238 

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

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

240 
May change names of TVars. 
14291  241 
Performs compress and close_derivation on result, if modified. **) 
242 

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

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

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

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

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

248 
*) 

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

249 

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

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

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

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

253 
(* Returns None if head of premise is not a predicate defined by a locale, 
14291  254 
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

255 
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

256 
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

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

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

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

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

261 
None => None 
14291  262 
 Some {view = (_, axioms), ...} => 
263 
if name = raw_name andalso not (null axioms) 

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

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

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

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

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

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

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

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

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

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

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

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

275 
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

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

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

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

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

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

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

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

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

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

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

286 
(* Assemble new theorem; new prems will be hyps. 
14291  287 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

305 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

347 
end 
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 
val (_, thm', cprems', _) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

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

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

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

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

357 

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

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

359 

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

360 

12277  361 
(* diagnostics *) 
12273  362 

12277  363 
fun err_in_locale ctxt msg ids = 
364 
let 

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

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

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

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

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

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

12063  374 

12277  375 

376 

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

377 
(** primitives **) 
12046  378 

12277  379 
(* renaming *) 
12263  380 

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

382 

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

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

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

386 
 rename_term _ a = a; 

387 

388 
fun rename_thm ren th = 

389 
let 

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

391 
val cert = Thm.cterm_of sign; 

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

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

396 
in 

397 
if xs = xs' then th 

398 
else 

399 
th 

400 
> Drule.implies_intr_list (map cert hyps) 

401 
> Drule.forall_intr_list (cert_frees xs) 

402 
> Drule.forall_elim_list (cert_vars xs) 

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

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

405 
end; 

406 

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

407 
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

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

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

410 
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

411 
end)) 
12263  412 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
413 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  416 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  417 

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

418 
fun rename_facts prfx elem = 
12307  419 
let 
12323  420 
fun qualify (arg as ((name, atts), x)) = 
13394  421 
if prfx = "" orelse name = "" then arg 
13375  422 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  423 
in 
424 
(case elem of 

425 
Fixes fixes => Fixes fixes 

426 
 Assumes asms => Assumes (map qualify asms) 

427 
 Defines defs => Defines (map qualify defs) 

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

429 
end; 

430 

12263  431 

12502  432 
(* type instantiation *) 
433 

434 
fun inst_type [] T = T 

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

436 

437 
fun inst_term [] t = t 

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

439 

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

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

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

443 
val sign = ProofContext.sign_of ctxt; 
12575  444 
val cert = Thm.cterm_of sign; 
445 
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

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

12502  449 
in 
450 
if null env' then th 

451 
else 

452 
th 

453 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

459 
end; 

460 

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

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

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

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

467 
 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

468 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  469 

470 

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

471 

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

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

473 

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

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

475 

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

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

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

478 

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

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

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

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

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

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

485 

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

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

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

488 
fun paramify (i, None) = (i, None) 
14777  489 
 paramify (i, Some T) = apsnd Some (TypeInfer.paramify_dummies (i, T)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

490 

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

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

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

494 

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

495 
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

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

497 
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

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

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

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

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

503 

12730  504 
fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss)); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

505 

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

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

507 
('a * 'b Library.option) list > ('a * 'b) list *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

508 
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

509 

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

510 

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

511 
(* flatten expressions *) 
11896  512 

12510  513 
local 
12502  514 

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

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

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

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

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

519 

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

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

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

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

523 
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

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

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

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

527 
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

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

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

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

531 

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

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

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

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

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

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

537 

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

538 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  539 
let 
540 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

541 
val maxidx = length raw_parmss; 

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

543 

544 
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

545 
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

546 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  547 

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

548 
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

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

552 
val (unifier, _) = foldl unify_list 

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

554 

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

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

557 

558 
fun inst_parms (i, ps) = 

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

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

561 
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

562 
in if T = TFree (a, S) then None else Some ((a, S), T) end) 
12502  563 
in map inst_parms idx_parmss end; 
564 

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

565 
in 
12502  566 

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

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

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

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

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

12839  574 
in map inst (elemss ~~ envs) end; 
12502  575 

12575  576 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  577 
let 
578 
val thy = ProofContext.theory_of ctxt; 

12263  579 

12289  580 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
581 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

585 

586 
fun rename_parms ren (name, ps) = 

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

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

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

590 
end; 

12263  591 

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

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

594 
parms is accumulated list of parameters *) 
12289  595 
let 
596 
val {import, params, ...} = the_locale thy name; 

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

598 
in 

12273  599 
if (name, ps) mem ids then (ids, parms) 
12277  600 
else 
12289  601 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
602 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  603 
end 
604 
 identify ((ids, parms), Rename (e, xs)) = 

605 
let 

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

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

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

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

12273  612 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  613 

12307  614 
fun eval (name, xs) = 
12273  615 
let 
13308  616 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  617 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  618 
val (params', elems') = 
619 
if null ren then ((ps, qs), map #1 elems) 

12502  620 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  621 
map (rename_elem ren o #1) elems); 
13375  622 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  623 
in ((name, params'), elems'') end; 
12307  624 

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

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

627 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  628 
in (prev_idents @ idents, elemss) end; 
12046  629 

12510  630 
end; 
631 

12070  632 

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

633 
(* activate elements *) 
12273  634 

12510  635 
local 
636 

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

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

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

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

640 
> Seq.single; 
12263  641 

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

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

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

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

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

649 
ctxt > ProofContext.fix_frees ts 
13629  650 
> ProofContext.assume_i (export_axioms ps) asms; 
651 
in ((ctxt', qs), []) end 

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

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

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

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

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

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

659 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
14564  660 
let val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts 
13420  661 
in ((ctxt', axs), if is_ext then res else []) end; 
12502  662 

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

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

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

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

666 
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

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

668 

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

669 
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

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

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

672 
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

673 
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

674 

12546  675 
in 
676 

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

677 
(* CB: activate_facts prep_facts ((ctxt, axioms), elemss), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

678 
where elemss is a list of pairs consisting of identifiers and context 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

679 
elements, extends ctxt by the context elements yielding ctxt' and returns 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

680 
((ctxt', axioms'), (elemss', facts)). 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

681 
Assumptions use entries from axioms to set up exporters in ctxt'. Unused 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

682 
axioms are returned as axioms'; elemss' is obtained from elemss (without 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

683 
identifier) and the intermediate context with prep_facts. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

686 

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

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

688 
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); 
12546  689 

12510  690 
end; 
691 

12307  692 

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

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

694 

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

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

696 

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

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

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

699 
 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

700 

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

701 

12546  702 
(* attributes *) 
703 

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

705 

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

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

709 
* Locale expression: no effect. *) 

710 

711 

15127  712 
fun map_attrib_elem _ (Fixes fixes) = Fixes fixes 
713 
 map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms) 

714 
 map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs) 

715 
 map_attrib_elem attrib (Notes facts) = 

716 
Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts) 

717 

718 
fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem) 

719 
 map_attrib_elem_expr _ (Expr expr) = Expr expr; 

12546  720 

721 
end; 

722 

723 

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

724 
(* parameters *) 
12502  725 

726 
local 

727 

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

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

729 
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

730 
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

731 

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

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

733 

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

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

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

736 

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

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

738 

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

739 

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

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

741 

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

744 

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

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

746 

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

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

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

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

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

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

752 
context elements generated from expr, decorated with additional 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

753 
information (the identifiers?), including parameter names. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

754 
It appears that the identifier name is empty for external elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

755 
(this is suggested by the implementation of activate_facts). *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

756 

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

757 
fun flatten _ (ids, Elem (Fixes fixes)) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

758 
(ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

762 

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

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

764 

12839  765 
local 
766 

12727  767 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  768 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
14777  769 
(x, apsome (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), []) 
12727  770 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

771 

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

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

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

775 
 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

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

777 

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

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

780 
(case elems of 
13308  781 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  782 
 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

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

12839  786 
in 
787 

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

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

789 

12727  790 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
791 
let 

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

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

793 
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

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

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

796 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  797 
val int_elemss = 
798 
raw_elemss 

799 
> 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

800 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  801 
val (_, raw_elemss') = 
802 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

803 
(int_elemss, raw_elemss); 

804 
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

805 

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

807 

12839  808 
local 
809 

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

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

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

812 

12839  813 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
814 

13336  815 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  816 
let 
817 
val body = Term.strip_all_body eq; 

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

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

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

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

823 

824 
fun abstract_thm sign eq = 

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

12502  826 

13336  827 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  828 
let 
13336  829 
val ((y, T), b) = abstract_term eq; 
13308  830 
val b' = norm_term env b; 
13336  831 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  832 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  833 
in 
13308  834 
conditional (exists (equal y o #1) xs) (fn () => 
835 
err "Attempt to define previously specified variable"); 

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

837 
err "Attempt to redefine variable"); 

13336  838 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  839 
end; 
12575  840 

13308  841 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  842 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
843 
let 

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

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

846 
val spec' = 

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

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

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

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

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

853 

854 
fun closeup _ false elem = elem 

855 
 closeup ctxt true elem = 

12839  856 
let 
13308  857 
fun close_frees t = 
858 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

861 

862 
fun no_binds [] = [] 

863 
 no_binds _ = 

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

865 
in 

866 
(case elem of 

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

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

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

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

871 
 e => e) 

872 
end; 

12839  873 

12502  874 

12839  875 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  876 
(x, assoc_string (parms, x), mx)) fixes) 
12839  877 
 finish_ext_elem _ close (Assumes asms, propp) = 
878 
close (Assumes (map #1 asms ~~ propp)) 

879 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

885 

13375  886 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  887 
let 
13308  888 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
889 
val text' = foldl (eval_text ctxt id false) (text, es); 

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

13375  891 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  892 
let 
893 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  894 
val text' = eval_text ctxt id true (text, e'); 
13308  895 
in (text', (id, [Ext e'])) end; 
12839  896 

897 
in 

12510  898 

13375  899 
fun finish_elemss ctxt parms do_close = 
900 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  901 

902 
end; 

903 

15127  904 
(* CB: type inference and consistency checks for locales *) 
905 

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

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

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

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

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

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

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

915 
raw_proppss contains assumptions and definitions from the 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

916 
(external?) elements in raw_elemss. *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

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

920 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

921 
(* CB: read/cert entire proposition (conclusion and premises from 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

923 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

924 
(* CB: it appears that terms declared in the propositions are added 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

925 
to the context here. *) 
12502  926 

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

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

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

930 
val propps = unflat raw_propps propp; 
12839  931 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  932 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

964 
*) 
13308  965 
in ((parms, elemss, concl), text) end; 
12502  966 

967 
in 

968 

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

969 
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

970 
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

971 

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

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

973 

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

974 

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

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

976 

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

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

978 

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

979 
fun prep_name ctxt (name, atts) = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

984 

13375  985 
fun prep_facts _ _ (Int elem) = elem 
986 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

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

991 

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

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

993 

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

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

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

996 

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

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

998 

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

999 

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

1001 

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

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

1003 

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

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

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

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

1007 
val sign = ProofContext.sign_of context; 
13375  1008 

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

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

1010 
(* CB: normalise "includes" among elements *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1011 
val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign)) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1014 
context elements obtained from import and elements. *) 
13375  1015 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  1016 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
13629  1017 
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss) 
13420  1018 
val ((import_ctxt, axioms'), (import_elemss, _)) = 
13629  1019 
activate_facts prep_facts ((context, axioms), ps); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1020 

13420  1021 
val ((ctxt, _), (elemss, _)) = 
13629  1022 
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

1023 
in 
13420  1024 
((((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

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

1026 

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

1027 
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

1028 
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

1029 

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

1030 
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

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

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

1033 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
13415  1034 
val ((view_statement, view_axioms), fixed_params, import) = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

1043 

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

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

1045 

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

1048 
fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z); 

1049 
fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z); 

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

1050 

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

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

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

1054 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  1055 

1056 
end; 

11896  1057 

1058 

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

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

1060 

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

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

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

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

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

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

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

1067 

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

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

1069 

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

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

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

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

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

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

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

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

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

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

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

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

1081 

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

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

1083 

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

1084 
val inst = case raw_inst of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1085 
None => if null ints 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1087 
else error "Locale has assumptions but no chained fact was found" 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1088 
 Some [] => if null ints 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1090 
else error "Locale has assumptions but no chained fact was found" 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1091 
 Some [thm] => if null ints 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1092 
then (warning "Locale has no assumptions: fact ignored"; None) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1094 
 Some _ => error "Multiple facts are not allowed"; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1095 

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

1096 
val args = case inst of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1097 
None => [] 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1098 
 Some thm => thm > prop_of > ObjectLogic.drop_judgment sign 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

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

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

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

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

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

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

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

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

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

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

1109 

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

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

1111 

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

1112 
val def_names = map (fn (Free (s, _), _) => s) env; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1113 
val (defined, assumed) = partition 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

1117 

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

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

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

1120 
val arg_types = map Term.fastype_of args; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1121 
val Tenv = foldl (Type.typ_match tsig) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1122 
(Vartab.empty, v_param_types ~~ arg_types) 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1123 
handle Library.LIST "~~" => error "Number of parameters does not \ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

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

1125 
(* get their sorts *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1126 
val tfrees = foldr Term.add_typ_tfrees (param_types, []); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1127 
val Tenv' = map 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1128 
(fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T)) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1130 

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

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

1132 

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

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

1134 
 inst_type env T = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1136 

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

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

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

1139 

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

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

1141 

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

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

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

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

1145 

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

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

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

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

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

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

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

1152 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1153 
val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1154 
val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

1162 
Thm.instantiate ((map (fn ((a, _), T) => 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1163 
(the (assoc (al, a)), certT T)) Tenv'), [])) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

1167 

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

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

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

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

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

1172 
val ass = map (fn ax => (prop_of ax, ax)) axioms; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1173 
val axs' = foldl (fn (axs, hyp) => 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1174 
(case gen_assoc (op aconv) (ass, hyp) of None => axs 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1175 
 Some ax => axs @ [ax])) ([], hyps); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

1180 
val thm''' = case inst of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1181 
None => thm'' 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1182 
 Some inst_thm => let 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

1195 

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

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

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

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

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

1200 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1218 

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

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

1220 

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

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

1222 

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

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

1224 

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

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

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

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

1228 

11896  1229 

13336  1230 
(** define locales **) 
1231 

1232 
(* print locale *) 

12070  1233 

12758  1234 
fun print_locale thy import body = 
12070  1235 
let 
12289  1236 
val thy_ctxt = ProofContext.init thy; 
13420  1237 
val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt; 
13375  1238 
val all_elems = flat (map #2 (import_elemss @ elemss)); 
12070  1239 

12307  1240 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
1241 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  1243 

1244 
fun prt_syn syn = 

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

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

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

1250 

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

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

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

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

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

12070  1257 

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

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

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

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

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

12277  1264 
in 
13336  1265 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
1266 
> Pretty.writeln 

12277  1267 
end; 
12070  1268 

1269 

12730  1270 
(* store results *) 
11896  1271 

12706
05fa6a8a6320
removed add_thmss;
wenz 