author  ballarin 
Tue, 30 Sep 2003 15:13:02 +0200  
changeset 14215  ebf291f3b449 
parent 13629  a46362d2b19b 
child 14216  a15951091d5d 
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. 
11896  14 
*) 
15 

16 
signature LOCALE = 

17 
sig 

12046  18 
type context 
19 
datatype ('typ, 'term, 'fact, 'att) elem = 

12058  20 
Fixes of (string * 'typ option * mixfix option) list  
12046  21 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
22 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  23 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
24 
datatype expr = 

25 
Locale of string  

26 
Rename of expr * string option list  

27 
Merge of expr list 

28 
val empty: expr 

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

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

12046  31 
type 'att element 
32 
type 'att element_i 

33 
type locale 

34 
val intern: Sign.sg > xstring > string 

12014  35 
val cond_extern: Sign.sg > string > xstring 
12502  36 
val the_locale: theory > string > locale 
12273  37 
val attribute: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 
38 
> ('typ, 'term, 'thm, context attribute) elem_expr 

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

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

40 
(string * (string list * string list)) list list > context > 
13415  41 
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

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

43 
(term * (term list * term list)) list list > context > 
13415  44 
string option * cterm list * context * context * (term * (term list * term list)) list list 
12758  45 
val print_locales: theory > unit 
46 
val print_locale: theory > expr > context attribute element list > unit 

13394  47 
val add_locale: bool > bstring > expr > context attribute element list > theory > theory 
48 
val add_locale_i: bool > bstring > expr > context attribute element_i list 

49 
> theory > theory 

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

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

12711  53 
val have_thmss: string > xstring > 
54 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 

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

56 
val have_thmss_i: string > string > 

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

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

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

61 
val prune_prems: theory > thm > thm 
11896  62 
val setup: (theory > theory) list 
63 
end; 

12839  64 

12289  65 
structure Locale: LOCALE = 
11896  66 
struct 
67 

12273  68 
(** locale elements and expressions **) 
11896  69 

12014  70 
type context = ProofContext.context; 
11896  71 

12046  72 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  73 
Fixes of (string * 'typ option * mixfix option) list  
12046  74 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
75 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  76 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
77 

78 
datatype expr = 

79 
Locale of string  

80 
Rename of expr * string option list  

81 
Merge of expr list; 

11896  82 

12273  83 
val empty = Merge []; 
84 

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

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

87 

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

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

12070  90 

91 
type locale = 

13415  92 
{view: cterm list * thm list, (*external view on assumptions*) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

93 
import: expr, (*dynamic import*) 
12289  94 
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

95 
params: (string * typ option) list * string list}; (*all/local params*) 
12063  96 

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

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

98 
{view = view, import = import, elems = elems, params = params}: locale; 
12063  99 

11896  100 

101 
(** theory data **) 

102 

103 
structure LocalesArgs = 

104 
struct 

12014  105 
val name = "Isar/locales"; 
12063  106 
type T = NameSpace.T * locale Symtab.table; 
11896  107 

12063  108 
val empty = (NameSpace.empty, Symtab.empty); 
109 
val copy = I; 

12118  110 
val prep_ext = I; 
12289  111 

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

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

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

114 
Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); 
12273  115 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  116 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
117 

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

12014  120 
> Pretty.writeln; 
11896  121 
end; 
122 

123 
structure LocalesData = TheoryDataFun(LocalesArgs); 

124 
val print_locales = LocalesData.print; 

125 

12289  126 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
127 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

128 

12277  129 

130 
(* access locales *) 

131 

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

11896  134 

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

12014  138 
fun the_locale thy name = 
139 
(case get_locale thy name of 

140 
Some loc => loc 

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

11896  142 

12046  143 

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

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

145 
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

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

147 

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

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

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

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

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

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

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

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

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

156 
 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

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

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

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

160 

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

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

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

163 
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

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

165 

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

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

167 

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

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

169 

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

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

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

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

173 

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

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

175 

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

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

177 

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

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

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

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

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

182 

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

183 
(* Insert into trie, wherever possible but avoiding branching *) 
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 
fun insert_ident subs id (Trie trie) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

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

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

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

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

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

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

195 

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

196 
(* List of leaves of a trie, removing duplicates *) 
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 
fun leaves _ (Trie []) = [] 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

202 
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

203 

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

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

205 

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

206 
(* Prune premises: remove internal delta predicates. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

207 

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

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

209 
May change names of TVars. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

210 
Performs compress and close_derivation on result, if modified. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

211 

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

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

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

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

215 
(* Returns None if head of premise is not a predicate defined by a locale, 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

216 
returns also None if locale has import but predicate is not *_axioms 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

217 
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

218 
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

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

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

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

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

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

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

225 
if name = raw_name andalso import <> empty 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

237 
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

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

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

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

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

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

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

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

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

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

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

248 
(* Assemble new theorem; new prems will be hyps. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

249 
Axioms is an intermeditate list of locale axioms required to 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

267 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

319 

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

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

321 

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

322 

12277  323 
(* diagnostics *) 
12273  324 

12277  325 
fun err_in_locale ctxt msg ids = 
326 
let 

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

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

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

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

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

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

12063  336 

12277  337 

338 

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

339 
(** primitives **) 
12046  340 

12277  341 
(* renaming *) 
12263  342 

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

344 

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

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

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

348 
 rename_term _ a = a; 

349 

350 
fun rename_thm ren th = 

351 
let 

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

353 
val cert = Thm.cterm_of sign; 

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

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

358 
in 

359 
if xs = xs' then th 

360 
else 

361 
th 

362 
> Drule.implies_intr_list (map cert hyps) 

363 
> Drule.forall_intr_list (cert_frees xs) 

364 
> Drule.forall_elim_list (cert_vars xs) 

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

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

367 
end; 

368 

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

369 
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

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

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

372 
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

373 
end)) 
12263  374 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
375 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  378 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  379 

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

380 
fun rename_facts prfx elem = 
12307  381 
let 
12323  382 
fun qualify (arg as ((name, atts), x)) = 
13394  383 
if prfx = "" orelse name = "" then arg 
13375  384 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  385 
in 
386 
(case elem of 

387 
Fixes fixes => Fixes fixes 

388 
 Assumes asms => Assumes (map qualify asms) 

389 
 Defines defs => Defines (map qualify defs) 

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

391 
end; 

392 

12263  393 

12502  394 
(* type instantiation *) 
395 

396 
fun inst_type [] T = T 

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

398 

399 
fun inst_term [] t = t 

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

401 

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

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

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

405 
val sign = ProofContext.sign_of ctxt; 
12575  406 
val cert = Thm.cterm_of sign; 
407 
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

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

12502  411 
in 
412 
if null env' then th 

413 
else 

414 
th 

415 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

421 
end; 

422 

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

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

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

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

429 
 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

430 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  431 

432 

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

433 

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

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

435 

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

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

437 

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

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

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

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

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

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

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

444 

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

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

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

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

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

449 

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

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

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

453 

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

454 
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

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

456 
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

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

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

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

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

462 

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

464 
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

465 

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 
(* flatten expressions *) 
11896  468 

12510  469 
local 
12502  470 

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

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

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

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

474 
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

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

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

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

478 
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

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

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

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

482 

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

483 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  484 
let 
485 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

486 
val maxidx = length raw_parmss; 

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

488 

489 
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

490 
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

491 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  492 

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

493 
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

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

497 
val (unifier, _) = foldl unify_list 

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

499 

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

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

502 

503 
fun inst_parms (i, ps) = 

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

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

506 
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

507 
in if T = TFree (a, S) then None else Some ((a, S), T) end) 
12502  508 
in map inst_parms idx_parmss end; 
509 

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

510 
in 
12502  511 

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

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

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

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

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

12839  519 
in map inst (elemss ~~ envs) end; 
12502  520 

12575  521 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  522 
let 
523 
val thy = ProofContext.theory_of ctxt; 

12263  524 

12289  525 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
526 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

530 

531 
fun rename_parms ren (name, ps) = 

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

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

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

535 
end; 

12263  536 

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

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

539 
parms is accumulated list of parameters *) 
12289  540 
let 
541 
val {import, params, ...} = the_locale thy name; 

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

543 
in 

12273  544 
if (name, ps) mem ids then (ids, parms) 
12277  545 
else 
12289  546 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
547 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  548 
end 
549 
 identify ((ids, parms), Rename (e, xs)) = 

550 
let 

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

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

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

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

12273  557 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  558 

12307  559 
fun eval (name, xs) = 
12273  560 
let 
13308  561 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  562 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  563 
val (params', elems') = 
564 
if null ren then ((ps, qs), map #1 elems) 

12502  565 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  566 
map (rename_elem ren o #1) elems); 
13375  567 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
13308  568 
in ((name, params'), elems'') end; 
12307  569 

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

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

572 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  573 
in (prev_idents @ idents, elemss) end; 
12046  574 

12510  575 
end; 
576 

12070  577 

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

578 
(* activate elements *) 
12273  579 

12510  580 
local 
581 

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

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

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

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

585 
> Seq.single; 
12263  586 

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

587 
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

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

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

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

593 
ctxt > ProofContext.fix_frees ts 
13629  594 
> ProofContext.assume_i (export_axioms ps) asms; 
595 
in ((ctxt', qs), []) end 

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

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

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

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

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

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

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

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

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

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

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

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

610 
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

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

612 

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

613 
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

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

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

616 
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

617 
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

618 

12546  619 
in 
620 

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

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

622 
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); 
12546  623 

12510  624 
end; 
625 

12307  626 

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

627 

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

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

629 

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

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

631 

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

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

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

634 
 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

635 

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

636 

12546  637 
(* attributes *) 
638 

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

640 

641 
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) 

642 
 attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) 

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

644 
 attribute attrib (Elem (Notes facts)) = 

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

646 
 attribute _ (Expr expr) = Expr expr; 

647 

648 
end; 

649 

650 

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

651 
(* parameters *) 
12502  652 

653 
local 

654 

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

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

656 
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

657 
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

658 

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

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

660 

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

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

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

663 

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

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

665 

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

666 

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

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

668 

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

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

670 

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

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

672 

12839  673 
local 
674 

12727  675 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  676 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  677 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
678 
 declare_int_elem (ctxt, _) = (ctxt, []); 

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

679 

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

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

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

683 
 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

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

685 

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

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

688 
(case elems of 
13308  689 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  690 
 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

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

12839  694 
in 
695 

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

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

697 

12727  698 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
699 
let 

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

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

701 
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

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

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

704 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  705 
val int_elemss = 
706 
raw_elemss 

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

708 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  709 
val (_, raw_elemss') = 
710 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

711 
(int_elemss, raw_elemss); 

712 
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

713 

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

715 

12839  716 
local 
717 

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

719 

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

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

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

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

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

728 

729 
fun abstract_thm sign eq = 

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

12502  731 

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

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

742 
err "Attempt to redefine variable"); 

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

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

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

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

751 
val spec' = 

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

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

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

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

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

758 

759 
fun closeup _ false elem = elem 

760 
 closeup ctxt true elem = 

12839  761 
let 
13308  762 
fun close_frees t = 
763 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

766 

767 
fun no_binds [] = [] 

768 
 no_binds _ = 

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

770 
in 

771 
(case elem of 

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

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

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

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

776 
 e => e) 

777 
end; 

12839  778 

12502  779 

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

784 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

790 

13375  791 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  792 
let 
13308  793 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
794 
val text' = foldl (eval_text ctxt id false) (text, es); 

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

13375  796 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  797 
let 
798 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  799 
val text' = eval_text ctxt id true (text, e'); 
13308  800 
in (text', (id, [Ext e'])) end; 
12839  801 

802 
in 

12510  803 

13375  804 
fun finish_elemss ctxt parms do_close = 
805 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  806 

807 
end; 

808 

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

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

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

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

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

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

816 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  817 

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

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

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

821 
val propps = unflat raw_propps propp; 
12839  822 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  823 

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

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

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

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

828 
val parms = param_types (xs ~~ typing); 
12273  829 

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

13308  832 
in ((parms, elemss, concl), text) end; 
12502  833 

834 
in 

835 

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

836 
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

837 
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

838 

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

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

840 

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

841 

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

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

843 

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

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

845 

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

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

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

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

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

850 

13375  851 
fun prep_facts _ _ (Int elem) = elem 
852 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

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

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

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

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

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

857 

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

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

859 

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

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

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

862 

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

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

864 

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

865 

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

867 

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

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

869 

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

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

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

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

873 
val sign = ProofContext.sign_of context; 
13375  874 

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

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

878 
 flatten (ids, Expr expr) = 

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

880 

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

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

889 

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

890 
(* CB: testing *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

891 

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

892 
val axioms' = if true (* null axioms *) then axioms' else 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

893 
let val {view = (ax3_view, ax3_axioms), ...} = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

894 
the_locale (ProofContext.theory_of context) "Type.ax3"; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

895 
val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms)) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

896 
("True <> False", propT)); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

897 
val {view = (ax4_view, ax4_axioms), ...} = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

898 
the_locale (ProofContext.theory_of context) "Type.ax4"; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

899 
in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end; 
13420  900 
val ((ctxt, _), (elemss, _)) = 
13629  901 
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

902 
in 
13420  903 
((((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

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

905 

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

906 
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

907 
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

908 

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

909 
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

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

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

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

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

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

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

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

922 

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

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

924 

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

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

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

927 
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

928 
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

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

930 
fun read_context x y z = (warning "read_context\n"; #1 (gen_context true [] [] x y [] z)); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

932 

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

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

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

935 
val cert_context_statement = gen_statement (K I) gen_context_i; 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

937 

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

938 
fun read_context_statement so cs xss ctxt = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

939 
let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

940 
gen_statement intern gen_context so cs xss ctxt; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

941 
in (locale, view_statement, locale_ctxt, elems_ctxt, concl') 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

943 
fun cert_context_statement so cs xss ctxt = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

944 
let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

945 
gen_statement (K I) gen_context_i so cs xss ctxt; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

946 
in (locale, view_statement, locale_ctxt, elems_ctxt, concl') 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

947 
end; 
12502  948 

949 
end; 

11896  950 

951 

952 

13336  953 
(** define locales **) 
954 

955 
(* print locale *) 

12070  956 

12758  957 
fun print_locale thy import body = 
12070  958 
let 
12289  959 
val thy_ctxt = ProofContext.init thy; 
13420  960 
val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt; 
13375  961 
val all_elems = flat (map #2 (import_elemss @ elemss)); 
12070  962 

12307  963 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
964 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  966 

967 
fun prt_syn syn = 

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

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

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

973 

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

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

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

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

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

12070  980 

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

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

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

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

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

12277  987 
in 
13336  988 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
989 
> Pretty.writeln 

12277  990 
end; 
12070  991 

992 

12730  993 
(* store results *) 
11896  994 

12706  995 
local 
996 

12702  997 
fun hide_bound_names names thy = 
998 
thy > PureThy.hide_thms false 

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

1000 

12958  1001 
in 
1002 

13375  1003 
fun have_thmss_qualified kind name args thy = 
12706  1004 
thy 
13375  1005 
> Theory.add_path (Sign.base_name name) 
12711  1006 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  1007 
>> hide_bound_names (map (#1 o #1) args) 
1008 
>> Theory.parent_path; 

1009 

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

1012 

1013 
end; 

1014 

1015 
local 

1016 

1017 
fun put_facts loc args thy = 

1018 
let 

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

1019 
val {view, import, elems, params} = the_locale thy loc; 
12958  1020 
val note = Notes (map (fn ((a, more_atts), th_atts) => 
1021 
((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

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

12706  1024 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
1025 
let 

1026 
val thy_ctxt = ProofContext.init thy; 

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

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

1028 
val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt; 
12706  1029 
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

1030 
val export = ProofContext.export_standard view loc_ctxt thy_ctxt; 
12711  1031 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  1032 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
1033 
in 

1034 
thy 

1035 
> put_facts loc args 

1036 
> have_thmss_qualified kind loc args' 

1037 
end; 

1038 

1039 
in 

1040 

12711  1041 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
1042 
val have_thmss_i = gen_have_thmss (K I) (K I); 

1043 

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

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

1049 
val ((ctxt', _), (_, facts')) = 
13420  1050 
activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]); 
1051 
in ((thy', ctxt'), facts') end; 

12702  1052 

12706  1053 
end; 
12063  1054 

11896  1055 

13336  1056 
(* predicate text *) 
1057 

13375  1058 
local 
1059 

1060 
val introN = "intro"; 

1061 

1062 
fun atomize_spec sign ts = 

1063 
let 

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

1065 
val body = ObjectLogic.atomize_term sign t; 

1066 
val bodyT = Term.fastype_of body; 

1067 
in 

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

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

1070 
end; 

1071 

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

1074 
else raise Match); 

13336  1075 

13420  1076 
fun def_pred bname parms defs ts norm_ts thy = 
13375  1077 
let 
1078 
val sign = Theory.sign_of thy; 

1079 
val name = Sign.full_name sign bname; 

1080 

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

1084 
val Ts = map #2 xs; 

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

1086 
> Library.sort_wrt #1 > map TFree; 

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

1087 
val predT = map Term.itselfT extraTs > Ts > bodyT; 
13336  1088 

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

13375  1091 
val statement = ObjectLogic.assert_propT sign head; 
1092 

1093 
val (defs_thy, [pred_def]) = 

1094 
thy 

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

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

13394  1099 

13375  1100 
val defs_sign = Theory.sign_of defs_thy; 
1101 
val cert = Thm.cterm_of defs_sign; 

1102 

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

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

1108 
val conjuncts = 

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

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

1110 
Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] 
13375  1111 
> Drule.conj_elim_precise (length ts); 
13394  1112 
val axioms = (ts ~~ conjuncts) > map (fn (t, ax) => 
13375  1113 
Tactic.prove defs_sign [] [] t (fn _ => 
1114 
Tactic.rewrite_goals_tac defs THEN 

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

13394  1116 
in (defs_thy, (statement, intro, axioms)) end; 
13375  1117 

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

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

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

1124 

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

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

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

1128 
 x => x) > #2; 

1129 

1130 
in 

13375  1131 

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

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

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

1136 
else 

1137 
let 

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

1141 
val elemss' = change_elemss axioms elemss @ 

13420  1142 
[(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])]; 
13394  1143 
in 
1144 
def_thy > have_thmss_qualified "" aname 

1145 
[((introN, [ContextRules.intro_query_global None]), [([intro], [])])] 

1146 
> #1 > rpair (elemss', [statement]) 

1147 
end; 

1148 
val (thy'', view) = 

13420  1149 
if Library.null ints then (thy', ([], [])) 
13394  1150 
else 
1151 
let 

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

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

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

1154 
val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement; 
13394  1155 
in 
1156 
def_thy > have_thmss_qualified "" bname 

13420  1157 
[((introN, [ContextRules.intro_query_global None]), [([intro], [])]), 
13442  1158 
((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])] 
13415  1159 
> #1 > rpair ([cstatement], axioms) 
13394  1160 
end; 
1161 
in (thy'', (elemss', view)) end; 

13375  1162 

1163 
end; 

13336  1164 

1165 

13297  1166 
(* add_locale(_i) *) 
1167 

1168 
local 

1169 

13394  1170 
fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy = 
13297  1171 
let 
1172 
val sign = Theory.sign_of thy; 

1173 
val name = Sign.full_name sign bname; 

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

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

1176 

1177 
val thy_ctxt = ProofContext.init thy; 

13420  1178 
val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) = 
13375  1179 
prep_ctxt raw_import raw_body thy_ctxt; 
1180 
val elemss = import_elemss @ body_elemss; 

13297  1181 

13415  1182 
val (pred_thy, (elemss', view as (view_statement, view_axioms))) = 
13394  1183 
if do_pred then thy > define_preds bname text elemss 
13415  1184 
else (thy, (elemss, ([], []))); 
13375  1185 
val pred_ctxt = ProofContext.init pred_thy; 
13420  1186 

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

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

1194 
> put_locale name (make_locale view (prep_expr sign raw_import) 
13394  1195 
(map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) 
13375  1196 
(params_of elemss', map #1 (params_of body_elemss))) 
13297  1197 
end; 
1198 

1199 
in 

1200 

1201 
val add_locale = gen_add_locale read_context intern_expr; 

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

1202 

13297  1203 
val add_locale_i = gen_add_locale cert_context (K I); 
1204 

1205 
end; 

1206 

1207 

12730  1208 

11896  1209 
(** locale theory setup **) 
12063  1210 

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

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

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

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

1216 
end; 