author  haftmann 
Tue, 20 Jun 2006 10:16:22 +0200  
changeset 19929  5c882c3e610b 
parent 19928  cb8472f4c5fd 
child 19953  2f54a51f1801 
permissions  rwrr 
18168  1 
(* Title: Pure/Tools/class_package.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

19468  5 
Type classes derived from primitive axclasses and locales. 
18168  6 
*) 
7 

8 
signature CLASS_PACKAGE = 

9 
sig 

19150  10 
val class: bstring > class list > Element.context list > theory 
18515  11 
> ProofContext.context * theory 
19150  12 
val class_i: bstring > class list > Element.context_i list > theory 
18515  13 
> ProofContext.context * theory 
19150  14 
val instance_arity: (xstring * string list) * string 
19136  15 
> bstring * Attrib.src list > ((bstring * Attrib.src list) * string) list 
18575  16 
> theory > Proof.state 
19150  17 
val instance_arity_i: (string * sort list) * sort 
19136  18 
> bstring * attribute list > ((bstring * attribute list) * term) list 
18575  19 
> theory > Proof.state 
19150  20 
val prove_instance_arity: tactic > (string * sort list) * sort 
19136  21 
> bstring * attribute list > ((bstring * attribute list) * term) list 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

22 
> theory > theory 
19150  23 
val instance_sort: string * string > theory > Proof.state 
24 
val instance_sort_i: class * sort > theory > Proof.state 

25 
val prove_instance_sort: tactic > class * sort > theory > theory 

18168  26 

19253  27 
val use_cp_instance: bool ref; 
28 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

29 
val intern_class: theory > xstring > class 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

30 
val intern_sort: theory > sort > sort 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

31 
val extern_class: theory > class > xstring 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

32 
val extern_sort: theory > sort > sort 
18755  33 
val certify_class: theory > class > class 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

34 
val certify_sort: theory > sort > sort 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

35 
val read_sort: theory > string > sort 
18884  36 
val operational_sort_of: theory > sort > sort 
18702  37 
val the_superclasses: theory > class > class list 
38 
val the_consts_sign: theory > class > string * (string * typ) list 

18168  39 
val lookup_const_class: theory > string > class option 
19213  40 
val the_instances: theory > class > (string * ((sort list) * string)) list 
18702  41 
val the_inst_sign: theory > class * string > (string * sort) list * (string * typ) list 
19213  42 
val get_classtab: theory > (string * string) list Symtab.table 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

43 

18702  44 
val print_classes: theory > unit 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

45 
val intro_classes_tac: thm list > tactic 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

46 
val default_intro_classes_tac: thm list > tactic 
18168  47 

48 
type sortcontext = (string * sort) list 

18884  49 
datatype classlookup = Instance of (class * string) * classlookup list list 
19253  50 
 Lookup of class list * (string * (int * int)) 
18168  51 
val extract_sortctxt: theory > typ > sortcontext 
18884  52 
val extract_classlookup: theory > string * typ > classlookup list list 
53 
val extract_classlookup_inst: theory > class * string > class > classlookup list list 

19253  54 
val extract_classlookup_member: theory > typ * typ > classlookup list list 
18168  55 
end; 
56 

57 
structure ClassPackage: CLASS_PACKAGE = 

58 
struct 

59 

60 

18708  61 
(* theory data *) 
18168  62 

19456  63 
datatype class_data = ClassData of { 
18575  64 
name_locale: string, 
65 
name_axclass: string, 

66 
var: string, 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

67 
consts: (string * (string * typ)) list 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

68 
(*locale parameter ~> toplevel const*) 
18168  69 
}; 
70 

19456  71 
fun rep_classdata (ClassData c) = c; 
72 

18575  73 
structure ClassData = TheoryDataFun ( 
18168  74 
struct 
75 
val name = "Pure/classes"; 

19213  76 
type T = (class_data Graph.T 
77 
* (string * (sort list * string)) list Symtab.table) 

19456  78 
(*class ~> tyco ~> (arity, thyname)*) 
19213  79 
* class Symtab.table; 
80 
val empty = ((Graph.empty, Symtab.empty), Symtab.empty); 

18168  81 
val copy = I; 
82 
val extend = I; 

19456  83 
fun merge _ (((g1, c1), f1) : T, ((g2, c2), f2)) = 
19648  84 
((Graph.merge (K true) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)), 
19213  85 
Symtab.merge (op =) (f1, f2)); 
86 
fun print thy ((gr, _), _) = 

18575  87 
let 
19928  88 
fun pretty_class gr (name, ClassData {name_locale, name_axclass, var, consts}) = 
18575  89 
(Pretty.block o Pretty.fbreaks) [ 
90 
Pretty.str ("class " ^ name ^ ":"), 

91 
(Pretty.block o Pretty.fbreaks) ( 

92 
Pretty.str "superclasses: " 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

93 
:: (map Pretty.str o Graph.imm_succs gr) name 
18575  94 
), 
95 
Pretty.str ("locale: " ^ name_locale), 

96 
Pretty.str ("axclass: " ^ name_axclass), 

97 
Pretty.str ("class variable: " ^ var), 

98 
(Pretty.block o Pretty.fbreaks) ( 

99 
Pretty.str "constants: " 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

100 
:: map (fn (_, (c, ty)) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts 
18575  101 
) 
102 
] 

103 
in 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

104 
(Pretty.writeln o Pretty.chunks o map (pretty_class gr) 
19468  105 
o AList.make (Graph.get_node gr) o flat o Graph.strong_conn) gr 
18575  106 
end; 
18168  107 
end 
108 
); 

109 

18708  110 
val _ = Context.add_setup ClassData.init; 
18575  111 
val print_classes = ClassData.print; 
112 

19038  113 

114 
(* queries *) 

115 

19456  116 
val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o fst o ClassData.get; 
19213  117 
val the_instances = these oo Symtab.lookup o snd o fst o ClassData.get; 
118 
val lookup_const_class = Symtab.lookup o snd o ClassData.get; 

18168  119 

19038  120 
fun the_class_data thy class = 
18168  121 
case lookup_class_data thy class 
18755  122 
of NONE => error ("undeclared operational class " ^ quote class) 
18168  123 
 SOME data => data; 
124 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

125 
val is_class = is_some oo lookup_class_data; 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

126 

5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

127 
fun is_operational_class thy cls = 
18702  128 
lookup_class_data thy cls 
129 
> Option.map (not o null o #consts) 

130 
> the_default false; 

18168  131 

18884  132 
fun operational_sort_of thy sort = 
18360  133 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

134 
fun get_sort class = 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

135 
if is_operational_class thy class 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

136 
then [class] 
19412  137 
else operational_sort_of thy (Sign.super_classes thy class); 
18360  138 
in 
139 
map get_sort sort 

19468  140 
> flat 
19412  141 
> Sign.certify_sort thy 
18360  142 
end; 
18168  143 

18702  144 
fun the_superclasses thy class = 
18515  145 
if is_class thy class 
146 
then 

19412  147 
Sign.super_classes thy class 
18884  148 
> operational_sort_of thy 
18515  149 
else 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

150 
error ("no class: " ^ class); 
18168  151 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

152 
fun get_superclass_derivation thy (subclass, superclass) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

153 
if subclass = superclass 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

154 
then SOME [subclass] 
19575
2d9940cd52d3
replaced Graph.find_paths by Graph.irreducible_paths;
wenzelm
parents:
19518
diff
changeset

155 
else case Graph.irreducible_paths ((fst o fst o ClassData.get) thy) (subclass, superclass) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

156 
of [] => NONE 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

157 
 (p::_) => (SOME o filter (is_operational_class thy)) p; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

158 

19038  159 
fun the_ancestry thy classes = 
160 
let 

161 
fun ancestry class anc = 

162 
anc 

163 
> cons class 

164 
> fold ancestry (the_superclasses thy class); 

165 
in fold ancestry classes [] end; 

166 

167 
fun subst_clsvar v ty_subst = 

168 
map_type_tfree (fn u as (w, _) => 

169 
if w = v then ty_subst else TFree u); 

170 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

171 
fun the_parm_map thy class = 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

172 
let 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

173 
val data = the_class_data thy class 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

174 
in (#consts data) end; 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

175 

18702  176 
fun the_consts_sign thy class = 
18168  177 
let 
19038  178 
val data = the_class_data thy class 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

179 
in (#var data, (map snd o #consts) data) end; 
18702  180 

181 
fun the_inst_sign thy (class, tyco) = 

18168  182 
let 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

183 
val _ = if is_operational_class thy class then () else error ("no operational class: " ^ class); 
19468  184 
val arity = Sign.arity_sorts thy tyco [class]; 
19038  185 
val clsvar = (#var o the_class_data thy) class; 
18702  186 
val const_sign = (snd o the_consts_sign thy) class; 
187 
fun add_var sort used = 

188 
let 

189 
val v = hd (Term.invent_names used "'a" 1) 

190 
in ((v, sort), v::used) end; 

191 
val (vsorts, _) = 

19213  192 
[clsvar] 
18702  193 
> fold (fn (_, ty) => curry (gen_union (op =)) 
194 
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign 

195 
> fold_map add_var arity; 

196 
val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts); 

197 
val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign; 

198 
in (vsorts, inst_signs) end; 

18168  199 

200 
fun get_classtab thy = 

19213  201 
(Symtab.map o map) 
202 
(fn (tyco, (_, thyname)) => (tyco, thyname)) ((snd o fst o ClassData.get) thy); 

18168  203 

204 

19038  205 
(* updaters *) 
206 

19928  207 
fun add_class_data (class, (superclasses, name_locale, name_axclass, var, consts)) = 
19213  208 
ClassData.map (fn ((gr, tab), consttab) => (( 
209 
gr 

19456  210 
> Graph.new_node (class, ClassData { 
19038  211 
name_locale = name_locale, 
212 
name_axclass = name_axclass, 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

213 
var = var, 
19213  214 
consts = consts 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

215 
}) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

216 
> fold (curry Graph.add_edge_acyclic class) superclasses, 
19213  217 
tab 
218 
> Symtab.update (class, [])), 

219 
consttab 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

220 
> fold (fn (_, (c, _)) => Symtab.update (c, class)) consts 
19038  221 
)); 
222 

223 
fun add_inst_data (class, inst) = 

19213  224 
ClassData.map (fn ((gr, tab), consttab) => 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

225 
let 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

226 
val undef_supclasses = class :: (filter (Symtab.defined tab) (Graph.all_succs gr [class])); 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

227 
in 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

228 
((gr, tab > fold (fn class => Symtab.map_entry class (AList.update (op =) inst)) undef_supclasses), consttab) 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

229 
end); 
19038  230 

231 

232 
(* name handling *) 

233 

234 
fun certify_class thy class = 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

235 
(fn class => (the_class_data thy class; class)) (Sign.certify_class thy class); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

236 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

237 
fun certify_sort thy sort = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

238 
map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

239 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

240 
fun intern_class thy = 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

241 
certify_class thy o Sign.intern_class thy; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

242 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

243 
fun intern_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

244 
certify_sort thy o Sign.intern_sort thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

245 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

246 
fun extern_class thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

247 
Sign.extern_class thy o certify_class thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

248 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

249 
fun extern_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

250 
Sign.extern_sort thy o certify_sort thy; 
19038  251 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

252 
fun read_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

253 
certify_sort thy o Sign.read_sort thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

254 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

255 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

256 
(* tactics and methods *) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

257 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

258 
fun intro_classes_tac facts st = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

259 
(ALLGOALS (Method.insert_tac facts THEN' 
19928  260 
REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st)))) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

261 
THEN Tactic.distinct_subgoals_tac) st; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

262 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

263 
fun default_intro_classes_tac [] = intro_classes_tac [] 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

264 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

265 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

266 
fun default_tac rules ctxt facts = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

267 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

268 
default_intro_classes_tac facts; 
19038  269 

19468  270 
val _ = Context.add_setup (Method.add_methods 
271 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

272 
"backchain introduction rules of classes"), 

273 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), 

274 
"apply some intro/elim rule")]); 

275 

19038  276 

19246  277 
(* axclass instances *) 
278 

279 
local 

280 

19412  281 
fun gen_instance mk_prop add_thm after_qed inst thy = 
19246  282 
thy 
283 
> ProofContext.init 

19412  284 
> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", []) 
19585  285 
(map (fn t => (("", []), [(t, [])])) (mk_prop thy inst)); 
19246  286 

287 
in 

288 

289 
val axclass_instance_subclass = 

19412  290 
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I; 
19246  291 
val axclass_instance_arity = 
19412  292 
gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity; 
19246  293 
val axclass_instance_arity_i = 
19412  294 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 
19246  295 

296 
end; 

297 

298 

19038  299 
(* classes and instances *) 
300 

301 
local 

302 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

303 
fun add_axclass_i (name, supsort) axs thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

304 
let 
19395  305 
val (c, thy') = thy 
19518  306 
> AxClass.define_class_i (name, supsort) [] axs; 
307 
val {intro, axioms, ...} = AxClass.get_definition thy' c; 

19395  308 
in ((c, (intro, axioms)), thy') end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

309 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

310 
fun prove_interpretation_i (prfx, atts) expr insts tac thy = 
19038  311 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

312 
fun ad_hoc_term NONE = NONE 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

313 
 ad_hoc_term (SOME (Const (c, ty))) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

314 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

315 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

316 
val s = c ^ "::" ^ Pretty.output p; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

317 
val _ = writeln s; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

318 
in SOME s end 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

319 
 ad_hoc_term (SOME t) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

320 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

321 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

322 
val s = Pretty.output p; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

323 
val _ = writeln s; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

324 
in SOME s end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

325 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

326 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

327 
> Locale.interpretation (prfx, atts) expr (map ad_hoc_term insts) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

328 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

329 
> (fn _ => I) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

330 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

331 

19150  332 
fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

333 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

334 
val supclasses = map (prep_class thy) raw_supclasses; 
19038  335 
val supsort = 
336 
supclasses 

337 
> map (#name_axclass o the_class_data thy) 

19468  338 
> Sign.certify_sort thy 
19038  339 
> null ? K (Sign.defaultS thy); 
19468  340 
val expr = (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

341 
val mapp_sup = AList.make 
19468  342 
(the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

343 
((map (fst o fst) o Locale.parameters_of_expr thy) expr); 
19038  344 
fun extract_tyvar_consts thy name_locale = 
345 
let 

346 
fun extract_tyvar_name thy tys = 

347 
fold (curry add_typ_tfrees) tys [] 

348 
> (fn [(v, sort)] => 

19468  349 
if Sign.subsort thy (supsort, sort) 
19038  350 
then v 
351 
else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort) 

352 
 [] => error ("no class type variable") 

353 
 vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs)) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

354 
val consts1 = 
19038  355 
Locale.parameters_of thy name_locale 
356 
> map (apsnd Syntax.unlocalize_mixfix) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

357 
val v = (extract_tyvar_name thy o map (snd o fst)) consts1; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

358 
val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

359 
in (v, chop (length mapp_sup) consts2) end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

360 
fun add_consts v raw_cs_sup raw_cs_this thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

361 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

362 
fun add_global_const ((c, ty), syn) thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

363 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

364 
> Sign.add_consts_i [(c, ty > subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)] 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

365 
> `(fn thy => (c, (Sign.intern_const thy c, ty))) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

366 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

367 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

368 
> fold_map add_global_const raw_cs_this 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

369 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

370 
fun extract_assumes thy name_locale cs_mapp = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

371 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

372 
val subst_assume = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

373 
map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

374 
 t => t) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

375 
fun prep_asm ((name, atts), ts) = 
19928  376 
((NameSpace.base name > print, map (Attrib.attribute thy) atts), map subst_assume ts) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

377 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

378 
(map prep_asm o Locale.local_asms_of thy) name_locale 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

379 
end; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

380 
fun add_global_constraint v class (_, (c, ty)) thy = 
19038  381 
thy 
19136  382 
> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty)); 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

383 
fun mk_const thy class v (c, ty) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

384 
Const (c, subst_clsvar v (TFree (v, [class])) ty); 
19038  385 
in 
386 
thy 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

387 
> add_locale bname expr raw_elems 
19928  388 
> (fn (name_locale, ctxt) => 
19038  389 
`(fn thy => extract_tyvar_consts thy name_locale) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

390 
#> (fn (v, (raw_cs_sup, raw_cs_this)) => 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

391 
add_consts v raw_cs_sup raw_cs_this 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

392 
#> (fn mapp_this => 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

393 
`(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this)) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

394 
#> (fn loc_axioms => 
19928  395 
add_axclass_i (bname, supsort) loc_axioms 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

396 
#> (fn (name_axclass, (_, ax_axioms)) => 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

397 
fold (add_global_constraint v name_axclass) mapp_this 
19928  398 
#> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this)) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

399 
#> prove_interpretation_i (NameSpace.base name_locale, []) 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

400 
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) 
19929  401 
((ALLGOALS o ProofContext.fact_tac) ax_axioms) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

402 
#> pair ctxt 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

403 
))))) 
19038  404 
end; 
405 

406 
in 

407 

19928  408 
val class = gen_class (Locale.add_locale false) intern_class; 
409 
val class_i = gen_class (Locale.add_locale_i false) certify_class; 

19038  410 

411 
end; (* local *) 

412 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

413 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

414 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

415 
fun gen_add_defs_overloaded prep_att tap_def add_defs tyco raw_defs thy = 
19038  416 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

417 
fun invent_name raw_t = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

418 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

419 
val t = tap_def thy raw_t; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

420 
val c = (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals) t; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

421 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

422 
Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

423 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

424 
fun prep_def (_, (("", a), t)) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

425 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

426 
val n = invent_name t 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

427 
in ((n, t), map (prep_att thy) a) end 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

428 
 prep_def (_, ((n, a), t)) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

429 
((n, t), map (prep_att thy) a); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

430 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

431 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

432 
> add_defs true (map prep_def raw_defs) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

433 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

434 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

435 
val add_defs_overloaded = gen_add_defs_overloaded Attrib.attribute Sign.read_term PureThy.add_defs; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

436 
val add_defs_overloaded_i = gen_add_defs_overloaded (K I) (K I) PureThy.add_defs_i; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

437 

19136  438 
fun gen_instance_arity prep_arity prep_att add_defs tap_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

439 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

440 
val pp = Sign.pp theory; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

441 
val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity); 
19038  442 
val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts) 
19136  443 
val name = case raw_name 
444 
of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco) 

445 
 _ => raw_name; 

446 
val atts = map (prep_att theory) raw_atts; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

447 
fun get_classes thy tyco sort = 
19038  448 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

449 
fun get class classes = 
19213  450 
if AList.defined (op =) ((the_instances thy) class) tyco 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

451 
then classes 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

452 
else classes 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

453 
> cons class 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

454 
> fold get (the_superclasses thy class) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

455 
in fold get sort [] end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

456 
val classes = get_classes theory tyco sort; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

457 
val _ = if null classes then error ("already instantiated") else (); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

458 
fun get_consts class = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

459 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

460 
val data = the_class_data theory class; 
19038  461 
val subst_ty = map_type_tfree (fn (var as (v, _)) => 
462 
if #var data = v then ty_inst else TFree var) 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

463 
in (map (apsnd subst_ty o snd) o #consts) data end; 
19468  464 
val cs = (flat o map get_consts) classes; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

465 
fun get_remove_contraint c thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

466 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

467 
val ty = Sign.the_const_constraint thy c; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

468 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

469 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

470 
> Sign.add_const_constraint_i (c, NONE) 
19806  471 
> pair (c, Logic.legacy_unvarifyT ty) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

472 
end; 
19253  473 
fun check_defs0 thy raw_defs c_req = 
19038  474 
let 
475 
fun get_c raw_def = 

19253  476 
(fst o Sign.cert_def pp o tap_def thy o snd) raw_def; 
19038  477 
val c_given = map get_c raw_defs; 
19340  478 
fun eq_c ((c1 : string, ty1), (c2, ty2)) = 
19038  479 
let 
19806  480 
val ty1' = Logic.legacy_varifyT ty1; 
481 
val ty2' = Logic.legacy_varifyT ty2; 

19038  482 
in 
483 
c1 = c2 

19253  484 
andalso Sign.typ_instance thy (ty1', ty2') 
485 
andalso Sign.typ_instance thy (ty2', ty1') 

19038  486 
end; 
19300  487 
val _ = case subtract eq_c c_req c_given 
19038  488 
of [] => () 
489 
 cs => error ("superfluous definition(s) given for " 

19253  490 
^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs); 
19340  491 
(*val _ = case subtract eq_c c_given c_req 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

492 
of [] => () 
19038  493 
 cs => error ("no definition(s) given for " 
19340  494 
^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*) 
19253  495 
in () end; 
496 
fun check_defs1 raw_defs c_req thy = 

497 
let 

19518  498 
val thy' = (Sign.primitive_arity (tyco, asorts, sort) o Theory.copy) thy 
19253  499 
in (check_defs0 thy' raw_defs c_req; thy) end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

500 
fun mangle_alldef_name tyco sort = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

501 
Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

502 
fun note_all tyco sort thms thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

503 
thy 
19136  504 
> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])] 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

505 
> snd; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

506 
fun after_qed cs thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

507 
thy 
19253  508 
> fold (fn class => 
509 
add_inst_data (class, (tyco, 

19412  510 
(map (operational_sort_of thy) asorts, Context.theory_name thy)))) sort 
511 
> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); 

19038  512 
in 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

513 
theory 
19253  514 
> check_defs1 raw_defs cs 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

515 
> fold_map get_remove_contraint (map fst cs) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

516 
>> add_defs tyco (map (pair NONE) raw_defs) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

517 
> (fn (cs, defnames) => note_all tyco sort defnames #> pair cs) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

518 
> (fn cs => do_proof (after_qed cs) arity) 
19038  519 
end; 
520 

19246  521 
fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute add_defs_overloaded 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

522 
(fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof; 
19246  523 
fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I) add_defs_overloaded_i 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

524 
(K I) do_proof; 
19246  525 
val setup_proof = axclass_instance_arity_i; 
526 
fun tactic_proof tac after_qed arity = AxClass.prove_arity arity tac #> after_qed; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

527 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

528 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

529 

19150  530 
val instance_arity = instance_arity' setup_proof; 
531 
val instance_arity_i = instance_arity_i' setup_proof; 

532 
val prove_instance_arity = instance_arity_i' o tactic_proof; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

533 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

534 
end; (* local *) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

535 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

536 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

537 

19136  538 
fun fish_thms (name, expr) after_qed thy = 
539 
let 

540 
val _ = writeln ("sub " ^ name) 

541 
val suplocales = (fn Locale.Merge es => map (fn Locale.Locale n => n) es) expr; 

542 
val _ = writeln ("super " ^ commas suplocales) 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

543 
fun get_c name = 
19136  544 
(map (NameSpace.base o fst o fst) o Locale.parameters_of thy) name; 
545 
fun get_a name = 

546 
(map (NameSpace.base o fst o fst) o Locale.local_asms_of thy) name; 

547 
fun get_t supname = 

548 
map (NameSpace.append (NameSpace.append name ((space_implode "_" o get_c) supname)) o NameSpace.base) 

549 
(get_a name); 

550 
val names = map get_t suplocales; 

551 
val _ = writeln ("fishing for " ^ (commas o map commas) names); 

552 
in 

553 
thy 

554 
> after_qed ((map o map) (Drule.standard o get_thm thy o Name) names) 

555 
end; 

556 

557 
fun add_interpretation_in (after_qed : thm list list > theory > theory) (name, expr) thy = 

558 
thy 

559 
> Locale.interpretation_in_locale (name, expr); 

560 

561 
fun prove_interpretation_in tac (after_qed : thm list list > theory > theory) (name, expr) thy = 

562 
thy 

563 
> Locale.interpretation_in_locale (name, expr) 

564 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 

565 
> (fn _ => I); 

19038  566 

19150  567 
fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

568 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

569 
val class = prep_class theory raw_class; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

570 
val sort = prep_sort theory raw_sort; 
19136  571 
val loc_name = (#name_locale o the_class_data theory) class; 
19468  572 
val loc_expr = 
573 
(Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort; 

19136  574 
fun after_qed thmss thy = 
19468  575 
(writeln ""; (Pretty.writeln o Display.pretty_thms o flat) thmss; writeln ""; fold (fn supclass => 
19412  576 
AxClass.prove_classrel (class, supclass) 
19136  577 
(ALLGOALS (K (intro_classes_tac [])) THEN 
19468  578 
(ALLGOALS o resolve_tac o flat) thmss) 
19136  579 
) sort thy) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

580 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

581 
theory 
19136  582 
> do_proof after_qed (loc_name, loc_expr) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

583 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

584 

19150  585 
fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof; 
586 
fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof; 

19136  587 
val setup_proof = add_interpretation_in; 
588 
val tactic_proof = prove_interpretation_in; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

589 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

590 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

591 

19150  592 
val instance_sort = instance_sort' setup_proof; 
593 
val instance_sort_i = instance_sort_i' setup_proof; 

594 
val prove_instance_sort = instance_sort_i' o tactic_proof; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

595 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

596 
end; (* local *) 
19038  597 

18168  598 
(* extracting dictionary obligations from types *) 
599 

600 
type sortcontext = (string * sort) list; 

601 

18335  602 
fun extract_sortctxt thy ty = 
18702  603 
(typ_tfrees o fst o Type.freeze_thaw_type) ty 
18884  604 
> map (apsnd (operational_sort_of thy)) 
18168  605 
> filter (not o null o snd); 
606 

18884  607 
datatype classlookup = Instance of (class * string) * classlookup list list 
19253  608 
 Lookup of class list * (string * (int * int)) 
19213  609 

610 
fun pretty_lookup' (Instance ((class, tyco), lss)) = 

611 
(Pretty.block o Pretty.breaks) ( 

612 
Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco] 

613 
:: map pretty_lookup lss 

614 
) 

19253  615 
 pretty_lookup' (Lookup (classes, (v, (i, j)))) = 
616 
Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)]) 

19213  617 
and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls; 
18168  618 

18864  619 
fun extract_lookup thy sortctxt raw_typ_def raw_typ_use = 
18168  620 
let 
19806  621 
val typ_def = Logic.legacy_varifyT raw_typ_def; 
622 
val typ_use = Logic.legacy_varifyT raw_typ_use; 

18168  623 
val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

624 
fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0); 
18168  625 
fun mk_class_deriv thy subclasses superclass = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

626 
let 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19213
diff
changeset

627 
val (i, (subclass::deriv)) = (the oo get_index) (fn subclass => 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

628 
get_superclass_derivation thy (subclass, superclass) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

629 
) subclasses; 
19253  630 
in (rev deriv, (i, length subclasses)) end; 
19213  631 
fun mk_lookup (sort_def, (Type (tyco, tys))) = 
632 
map (fn class => Instance ((class, tyco), 

633 
map2 (curry mk_lookup) 

19468  634 
(map (operational_sort_of thy) (Sign.arity_sorts thy tyco [class])) 
19213  635 
tys) 
636 
) sort_def 

18168  637 
 mk_lookup (sort_def, TVar ((vname, _), sort_use)) = 
638 
let 

639 
fun mk_look class = 

18884  640 
let val (deriv, classindex) = mk_class_deriv thy (operational_sort_of thy sort_use) class 
18168  641 
in Lookup (deriv, (vname, classindex)) end; 
642 
in map mk_look sort_def end; 

18864  643 
in 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

644 
sortctxt 
18864  645 
> map (tab_lookup o fst) 
18884  646 
> map (apfst (operational_sort_of thy)) 
18864  647 
> filter (not o null o fst) 
648 
> map mk_lookup 

649 
end; 

650 

18884  651 
fun extract_classlookup thy (c, raw_typ_use) = 
18864  652 
let 
653 
val raw_typ_def = Sign.the_const_constraint thy c; 

19806  654 
val typ_def = Logic.legacy_varifyT raw_typ_def; 
18702  655 
fun reorder_sortctxt ctxt = 
656 
case lookup_const_class thy c 

657 
of NONE => ctxt 

658 
 SOME class => 

659 
let 

19038  660 
val data = the_class_data thy class; 
19806  661 
val sign = (Logic.legacy_varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c; 
18702  662 
val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty; 
663 
val v : string = case Vartab.lookup match_tab (#var data, 0) 

664 
of SOME (_, TVar ((v, _), _)) => v; 

665 
in 

666 
(v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt 

667 
end; 

18168  668 
in 
18864  669 
extract_lookup thy 
670 
(reorder_sortctxt (extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def))) 

671 
raw_typ_def raw_typ_use 

18168  672 
end; 
673 

18884  674 
fun extract_classlookup_inst thy (class, tyco) supclass = 
18864  675 
let 
676 
fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco)) 

19136  677 
val typ_def = mk_typ supclass; 
678 
val typ_use = mk_typ class; 

18864  679 
in 
680 
extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use 

681 
end; 

18168  682 

19253  683 
fun extract_classlookup_member thy (ty_decl, ty_use) = 
684 
extract_lookup thy (extract_sortctxt thy ty_decl) ty_decl ty_use; 

18884  685 

18515  686 
(* toplevel interface *) 
687 

688 
local 

689 

690 
structure P = OuterParse 

691 
and K = OuterKeyword 

692 

693 
in 

694 

18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

695 
val (classK, instanceK) = ("class", "instance") 
18515  696 

19253  697 
val use_cp_instance = ref false; 
698 

19136  699 
fun wrap_add_instance_subclass (class, sort) thy = 
700 
case Sign.read_sort thy sort 

701 
of [class'] => 

19253  702 
if ! use_cp_instance 
703 
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class 

19136  704 
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class' 
705 
then 

19150  706 
instance_sort (class, sort) thy 
19136  707 
else 
19246  708 
axclass_instance_subclass (class, sort) thy 
19150  709 
 _ => instance_sort (class, sort) thy; 
19136  710 

18911  711 
val parse_inst = 
19136  712 
(Scan.optional (P.$$$ "("  P.!!! (P.list1 P.sort  P.$$$ ")")) []  P.xname  P.$$$ "::"  P.sort) 
713 
>> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort)) 

714 
 (P.xname  P.$$$ "::"  P.!!! P.arity) 

715 
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); 

18911  716 

19038  717 
val locale_val = 
718 
(P.locale_expr  

719 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 P.context_element)) []  

720 
Scan.repeat1 P.context_element >> pair Locale.empty); 

721 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

722 
val class_subP = P.name  Scan.repeat (P.$$$ "+"  P.name) >> (op ::); 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

723 
val class_bodyP = P.!!! (Scan.repeat1 P.context_element); 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

724 

18515  725 
val classP = 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

726 
OuterSyntax.command classK "operational type classes" K.thy_decl ( 
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

727 
P.name  P.$$$ "=" 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

728 
 ( 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

729 
class_subP  P.$$$ "+"  class_bodyP 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

730 
 class_subP >> rpair [] 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

731 
 class_bodyP >> pair [] 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

732 
) >> (Toplevel.theory_context 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

733 
o (fn (bname, (supclasses, elems)) => class bname supclasses elems))); 
18515  734 

18575  735 
val instanceP = 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

736 
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( 
19136  737 
P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> wrap_add_instance_subclass 
738 
 P.opt_thm_name ":"  (parse_inst  Scan.repeat (P.opt_thm_name ":"  P.prop)) 

19246  739 
>> (fn (("", []), (((tyco, asorts), sort), [])) => axclass_instance_arity I (tyco, asorts, sort) 
19150  740 
 (natts, (inst, defs)) => instance_arity inst natts defs) 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

741 
) >> (Toplevel.print oo Toplevel.theory_to_proof)); 
18575  742 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

743 
val _ = OuterSyntax.add_parsers [classP, instanceP]; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

744 

18515  745 
end; (* local *) 
746 

18168  747 
end; (* struct *) 