author  ballarin 
Fri, 02 Apr 2004 14:08:30 +0200  
changeset 14508  859b11514537 
parent 14446  0bc2519e9990 
child 14528  1457584110ac 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

8 

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

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

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

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

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

15 
See also: 

16 

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

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

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

11896  20 
*) 
21 

22 
signature LOCALE = 

23 
sig 

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

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

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

31 
Locale of string  

32 
Rename of expr * string option list  

33 
Merge of expr list 

34 
val empty: expr 

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

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

12046  37 
type 'att element 
38 
type 'att element_i 

39 
type locale 

40 
val intern: Sign.sg > xstring > string 

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

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

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

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

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

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

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

55 
> theory > theory 

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

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

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

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

62 
val have_thmss_i: string > string > 

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

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

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

67 
val prune_prems: theory > thm > thm 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

68 
val instantiate: string > string > thm list option > context > context 
11896  69 
val setup: (theory > theory) list 
70 
end; 

12839  71 

12289  72 
structure Locale: LOCALE = 
11896  73 
struct 
74 

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

12014  77 
type context = ProofContext.context; 
11896  78 

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

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

85 
datatype expr = 

86 
Locale of string  

87 
Rename of expr * string option list  

88 
Merge of expr list; 

11896  89 

12273  90 
val empty = Merge []; 
91 

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

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

94 

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

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

12070  97 

98 
type locale = 

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

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

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

104 
assumptions of the body. 

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

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

107 
predicates of locales without import and all delta predicates of 

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

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

110 

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

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

112 
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

113 
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

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

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

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

119 
params: (string * typ option) list * string list}; (*all/local params*) 
12063  120 

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

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

122 
{view = view, import = import, elems = elems, params = params}: locale; 
12063  123 

11896  124 

125 
(** theory data **) 

126 

127 
structure LocalesArgs = 

128 
struct 

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

12063  132 
val empty = (NameSpace.empty, Symtab.empty); 
133 
val copy = I; 

12118  134 
val prep_ext = I; 
12289  135 

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

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

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

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

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

12014  144 
> Pretty.writeln; 
11896  145 
end; 
146 

147 
structure LocalesData = TheoryDataFun(LocalesArgs); 

148 
val print_locales = LocalesData.print; 

149 

12289  150 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
151 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

152 

12277  153 

154 
(* access locales *) 

155 

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

11896  158 

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

12014  162 
fun the_locale thy name = 
163 
(case get_locale thy name of 

164 
Some loc => loc 

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

11896  166 

12046  167 

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

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

169 
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

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

171 

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

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

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

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

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

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

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

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

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

180 
 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

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

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

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

184 

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

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

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

187 
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

188 
predicates. **) 
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 
val axiomsN = "axioms"; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

191 

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

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

193 

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

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

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

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

197 

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

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

199 

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

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

201 

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

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

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

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

205 
(args2 prefix args1)); 
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 
(* Insert into trie, wherever possible but avoiding branching *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

208 

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

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

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

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

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

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

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

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

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

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

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

219 

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

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

221 

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

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

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

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

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

226 
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

227 

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

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

229 

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

232 
premises of a theorem. 

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

233 

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

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

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

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

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

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

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

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

243 
*) 

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

244 

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

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

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

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

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

250 
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

251 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

270 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

300 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

352 

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

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

354 

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

355 

12277  356 
(* diagnostics *) 
12273  357 

12277  358 
fun err_in_locale ctxt msg ids = 
359 
let 

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

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

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

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

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

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

12063  369 

12277  370 

371 

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

372 
(** primitives **) 
12046  373 

12277  374 
(* renaming *) 
12263  375 

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

377 

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

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

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

381 
 rename_term _ a = a; 

382 

383 
fun rename_thm ren th = 

384 
let 

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

386 
val cert = Thm.cterm_of sign; 

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

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

391 
in 

392 
if xs = xs' then th 

393 
else 

394 
th 

395 
> Drule.implies_intr_list (map cert hyps) 

396 
> Drule.forall_intr_list (cert_frees xs) 

397 
> Drule.forall_elim_list (cert_vars xs) 

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

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

400 
end; 

401 

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

402 
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

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

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

405 
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

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

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

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

12273  411 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  412 

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

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

420 
Fixes fixes => Fixes fixes 

421 
 Assumes asms => Assumes (map qualify asms) 

422 
 Defines defs => Defines (map qualify defs) 

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

424 
end; 

425 

12263  426 

12502  427 
(* type instantiation *) 
428 

429 
fun inst_type [] T = T 

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

431 

432 
fun inst_term [] t = t 

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

434 

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

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

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

438 
val sign = ProofContext.sign_of ctxt; 
12575  439 
val cert = Thm.cterm_of sign; 
440 
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

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

12502  444 
in 
445 
if null env' then th 

446 
else 

447 
th 

448 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

454 
end; 

455 

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

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

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

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

462 
 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

463 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  464 

465 

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

466 

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

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

468 

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

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

470 

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

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

472 
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

473 

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

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

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

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

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

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

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

480 

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

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

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

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

484 
 paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T)); 
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 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  487 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

489 

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

490 
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

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

492 
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

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

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

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

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

498 

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

500 

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

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

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

503 
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

504 

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

505 

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

506 
(* flatten expressions *) 
11896  507 

12510  508 
local 
12502  509 

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

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

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

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

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

514 

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

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

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

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

518 
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

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

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

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

522 
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

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

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

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

526 

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

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

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

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

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

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

532 

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

533 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  534 
let 
535 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

536 
val maxidx = length raw_parmss; 

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

538 

539 
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

540 
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

541 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  542 

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

543 
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

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

547 
val (unifier, _) = foldl unify_list 

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

549 

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

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

552 

553 
fun inst_parms (i, ps) = 

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

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

556 
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

557 
in if T = TFree (a, S) then None else Some ((a, S), T) end) 
12502  558 
in map inst_parms idx_parmss end; 
559 

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

560 
in 
12502  561 

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

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

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

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

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

12839  569 
in map inst (elemss ~~ envs) end; 
12502  570 

12575  571 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  572 
let 
573 
val thy = ProofContext.theory_of ctxt; 

12263  574 

12289  575 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
576 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

580 

581 
fun rename_parms ren (name, ps) = 

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

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

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

585 
end; 

12263  586 

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

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

589 
parms is accumulated list of parameters *) 
12289  590 
let 
591 
val {import, params, ...} = the_locale thy name; 

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

593 
in 

12273  594 
if (name, ps) mem ids then (ids, parms) 
12277  595 
else 
12289  596 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
597 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  598 
end 
599 
 identify ((ids, parms), Rename (e, xs)) = 

600 
let 

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

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

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

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

12273  607 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  608 

12307  609 
fun eval (name, xs) = 
12273  610 
let 
13308  611 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  612 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  613 
val (params', elems') = 
614 
if null ren then ((ps, qs), map #1 elems) 

12502  615 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  616 
map (rename_elem ren o #1) elems); 
13375  617 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  618 
in ((name, params'), elems'') end; 
12307  619 

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

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

622 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  623 
in (prev_idents @ idents, elemss) end; 
12046  624 

12510  625 
end; 
626 

12070  627 

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

628 
(* activate elements *) 
12273  629 

12510  630 
local 
631 

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

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

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

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

635 
> Seq.single; 
12263  636 

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

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

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

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

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

643 
ctxt > ProofContext.fix_frees ts 
13629  644 
> ProofContext.assume_i (export_axioms ps) asms; 
645 
in ((ctxt', qs), []) end 

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

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

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

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

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

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

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

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

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

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

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

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

660 
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

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

662 

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

663 
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

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

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

666 
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

667 
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

668 

12546  669 
in 
670 

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

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

672 
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

673 
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

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

675 
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

676 
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

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

678 
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

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

680 

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

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

682 
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); 
12546  683 

12510  684 
end; 
685 

12307  686 

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

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

688 

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

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

690 

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

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

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

693 
 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

694 

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

695 

12546  696 
(* attributes *) 
697 

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

699 

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

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

703 
* Locale expression: no effect. *) 

704 

705 

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

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

709 
 attribute attrib (Elem (Notes facts)) = 

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

711 
 attribute _ (Expr expr) = Expr expr; 

712 

713 
end; 

714 

715 

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

716 
(* parameters *) 
12502  717 

718 
local 

719 

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

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

721 
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

722 
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

723 

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

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

725 

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

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

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

728 

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

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

730 

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 
(* propositions and bindings *) 
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 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

735 

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

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

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

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

739 
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

740 
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

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

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

743 
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

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

745 

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

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

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

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

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

750 
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

751 

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

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

753 

12839  754 
local 
755 

12727  756 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  757 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  758 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
759 
 declare_int_elem (ctxt, _) = (ctxt, []); 

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

760 

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

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

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

764 
 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

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

766 

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

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

769 
(case elems of 
13308  770 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  771 
 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

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

12839  775 
in 
776 

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

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

778 

12727  779 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
780 
let 

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

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

782 
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

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

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

785 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  786 
val int_elemss = 
787 
raw_elemss 

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

789 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  790 
val (_, raw_elemss') = 
791 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

792 
(int_elemss, raw_elemss); 

793 
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

794 

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

796 

12839  797 
local 
798 

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

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

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

801 

12839  802 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
803 

13336  804 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  805 
let 
806 
val body = Term.strip_all_body eq; 

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

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

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

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

812 

813 
fun abstract_thm sign eq = 

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

12502  815 

13336  816 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  817 
let 
13336  818 
val ((y, T), b) = abstract_term eq; 
13308  819 
val b' = norm_term env b; 
13336  820 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  821 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  822 
in 
13308  823 
conditional (exists (equal y o #1) xs) (fn () => 
824 
err "Attempt to define previously specified variable"); 

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

826 
err "Attempt to redefine variable"); 

13336  827 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  828 
end; 
12575  829 

13308  830 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  831 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
832 
let 

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

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

835 
val spec' = 

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

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

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

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

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

842 

843 
fun closeup _ false elem = elem 

844 
 closeup ctxt true elem = 

12839  845 
let 
13308  846 
fun close_frees t = 
847 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

850 

851 
fun no_binds [] = [] 

852 
 no_binds _ = 

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

854 
in 

855 
(case elem of 

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

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

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

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

860 
 e => e) 

861 
end; 

12839  862 

12502  863 

12839  864 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  865 
(x, assoc_string (parms, x), mx)) fixes) 
12839  866 
 finish_ext_elem _ close (Assumes asms, propp) = 
867 
close (Assumes (map #1 asms ~~ propp)) 

868 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

874 

13375  875 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  876 
let 
13308  877 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
878 
val text' = foldl (eval_text ctxt id false) (text, es); 

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

13375  880 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  881 
let 
882 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  883 
val text' = eval_text ctxt id true (text, e'); 
13308  884 
in (text', (id, [Ext e'])) end; 
12839  885 

886 
in 

12510  887 

13375  888 
fun finish_elemss ctxt parms do_close = 
889 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  890 

891 
end; 

892 

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

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

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

896 
context elements, the latter marked as internal or external. *) 
12727  897 
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

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

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

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

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

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

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

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

905 
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

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

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

908 
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

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

910 
to the context here. *) 
12502  911 

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

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

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

915 
val propps = unflat raw_propps propp; 
12839  916 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  917 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

937 
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

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

939 
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

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

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

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

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

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

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

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

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

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

949 
*) 
13308  950 
in ((parms, elemss, concl), text) end; 
12502  951 

952 
in 

953 

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

954 
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

955 
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

956 

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

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

958 

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

959 

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

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

961 

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

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

963 

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

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

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

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

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

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

969 

13375  970 
fun prep_facts _ _ (Int elem) = elem 
971 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

12529
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 
in 
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 get_facts x = prep_facts ProofContext.get_thms x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

981 

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

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

983 

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

984 

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

986 

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

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

988 

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

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

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

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

992 
val sign = ProofContext.sign_of context; 
13375  993 

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

994 
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

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

996 
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

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

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

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

1005 

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

1008 
in 
13420  1009 
((((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

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

1011 

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

1012 
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

1013 
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

1014 

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

1015 
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

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

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

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

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

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

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

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

1028 

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

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

1030 

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

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

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

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

1034 

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

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

1036 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  1037 

1038 
end; 

11896  1039 

1040 

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

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

1042 

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

1043 
fun instantiate loc_name prfx raw_inst ctxt = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

1049 

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

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

1051 

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

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

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

1054 
val fixed_params = param_types ps; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1055 
val (ids, raw_elemss) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1058 
(spec as (_, (ints, _)), (xs, env, defs))) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

1062 

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

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

1064 

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

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

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

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

1068 
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

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

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

1071 
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

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

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

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

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

1076 

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

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

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

1079 
 Some thm => thm > prop_of > ObjectLogic.drop_judgment sign 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1080 
> Term.strip_comb > snd; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1082 

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

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

1084 

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

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

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

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

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

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

1090 

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

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

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

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

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

1095 
(Vartab.empty, v_param_types ~~ arg_types) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1096 
handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact"; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

1102 

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

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

1104 

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

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

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

1107 
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

1108 

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

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

1110 
 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

1111 

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

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

1113 

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

1114 
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

1115 
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

1116 
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

1117 

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

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

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

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

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

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

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

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

1125 
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

1126 
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

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

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

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

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

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

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

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

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

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

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

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

1138 
end; 
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 
fun inst_thm' thm = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

1144 
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

1145 
val axs' = foldl (fn (axs, hyp) => 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1146 
(case assoc (ass, hyp) of None => axs 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1166 
in thm''' 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_elem (ctxt, (Ext _)) = ctxt 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1171 
let val facts' = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1172 
map (apsnd (map (apfst (map inst_thm')))) facts 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1175 
map (apfst (apfst (fn "" => "" 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1176 
 s => NameSpace.append prfx s))) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1178 
in fst (ProofContext.have_thmss_i facts'' ctxt) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1181 

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

1182 
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

1183 

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

1184 
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

1185 

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

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

1187 

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

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

1189 
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

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

1191 

11896  1192 

13336  1193 
(** define locales **) 
1194 

1195 
(* print locale *) 

12070  1196 

12758  1197 
fun print_locale thy import body = 
12070  1198 
let 
12289  1199 
val thy_ctxt = ProofContext.init thy; 
13420  1200 
val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt; 
13375  1201 
val all_elems = flat (map #2 (import_elemss @ elemss)); 
12070  1202 

12307  1203 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
1204 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  1206 

1207 
fun prt_syn syn = 

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

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

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

1213 

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

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

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

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

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

12070  1220 

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

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

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

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

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

12277  1227 
in 
13336  1228 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
1229 
> Pretty.writeln 

12277  1230 
end; 
12070  1231 

1232 

12730  1233 
(* store results *) 
11896  1234 

12706  1235 
local 
1236 

12702  1237 
fun hide_bound_names names thy = 
1238 
thy > PureThy.hide_thms false 

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

1240 

12958  1241 
in 
1242 

13375  1243 
fun have_thmss_qualified kind name args thy = 
12706  1244 
thy 
13375  1245 
> Theory.add_path (Sign.base_name name) 
12711  1246 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  1247 
>> hide_bound_names (map (#1 o #1) args) 
1248 
>> Theory.parent_path; 

1249 

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

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

1252 
(* CB: only used in Proof.finish_global. *) 
12958  1253 

1254 
end; 

1255 

1256 
local 

1257 

1258 
fun put_facts loc args thy = 

1259 
let 

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

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

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

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

12706  1265 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
1266 
let 

1267 
val thy_ctxt = ProofContext.init thy; 

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

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

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

1271 
val export = ProofContext.export_standard view loc_ctxt thy_ctxt; 
12711  1272 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  1273 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
1274 
in 

05fa6a8a6320
removed add_thmss;
