author  wenzelm 
Wed, 17 Mar 1999 13:44:43 +0100  
changeset 6379  2b17ff28a6cc 
parent 6084  842b059e023f 
child 6390  5d58c100ca3f 
permissions  rwrr 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/axclass.ML 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

4 

6379  5 
Axiomatic type class package. 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

6 
*) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

7 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

8 
signature AX_CLASS = 
3938  9 
sig 
5685  10 
val quiet_mode: bool ref 
6379  11 
val print_axclasses: theory > unit 
1498  12 
val add_classrel_thms: thm list > theory > theory 
13 
val add_arity_thms: thm list > theory > theory 

6379  14 
val add_axclass: bclass * xclass list > ((bstring * string) * Args.src list) list 
15 
> theory > theory * {intro: thm, axioms: thm list} 

16 
val add_axclass_i: bclass * class list > ((bstring * term) * theory attribute list) list 

17 
> theory > theory * {intro: thm, axioms: thm list} 

3938  18 
val add_inst_subclass: xclass * xclass > string list > thm list 
19 
> tactic option > theory > theory 

3788  20 
val add_inst_subclass_i: class * class > string list > thm list 
21 
> tactic option > theory > theory 

3938  22 
val add_inst_arity: xstring * xsort list * xclass list > string list 
23 
> thm list > tactic option > theory > theory 

3788  24 
val add_inst_arity_i: string * sort list * class list > string list 
25 
> thm list > tactic option > theory > theory 

6379  26 
val axclass_tac: thm list > tactic 
1498  27 
val prove_subclass: theory > class * class > thm list 
28 
> tactic option > thm 

29 
val prove_arity: theory > string * sort list * class > thm list 

30 
> tactic option > thm 

3949  31 
val goal_subclass: theory > xclass * xclass > thm list 
32 
val goal_arity: theory > xstring * xsort list * xclass > thm list 

6379  33 
val instance_subclass_proof: xclass * xclass > theory > ProofHistory.T 
34 
val instance_subclass_proof_i: class * class > theory > ProofHistory.T 

35 
val instance_arity_proof: xstring * xsort list * xclass > theory > ProofHistory.T 

36 
val instance_arity_proof_i: string * sort list * class > theory > ProofHistory.T 

37 
val setup: (theory > theory) list 

3938  38 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

39 

1498  40 
structure AxClass : AX_CLASS = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

41 
struct 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

42 

4015  43 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

44 
(** utilities **) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

45 

5685  46 
(* messages *) 
47 

48 
val quiet_mode = ref false; 

49 
fun message s = if ! quiet_mode then () else writeln s; 

50 

51 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

52 
(* type vars *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

53 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

54 
fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

55 
 map_typ_frees f (TFree a) = f a 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

56 
 map_typ_frees _ a = a; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

57 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

58 
val map_term_tfrees = map_term_types o map_typ_frees; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

59 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

60 
fun aT S = TFree ("'a", S); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

61 

3395  62 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
63 
 dest_varT (TVar xi_S) = xi_S 

3788  64 
 dest_varT T = raise TYPE ("dest_varT", [T], []); 
3395  65 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

66 

886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

67 
(* get axioms and theorems *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

68 

1498  69 
val is_def = Logic.is_equals o #prop o rep_thm; 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

70 

4934  71 
fun witnesses thy names thms = 
6379  72 
PureThy.get_thmss thy names @ thms @ filter is_def (map snd (axioms_of thy)); 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

73 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

74 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

75 

560  76 
(** abstract syntax operations **) 
423  77 

6379  78 
(* names *) 
79 

80 
fun intro_name c = c ^ "I"; 

81 
val introN = "intro"; 

82 
val axiomsN = "axioms"; 

83 

84 

423  85 
(* subclass relations as terms *) 
86 

1498  87 
fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2); 
423  88 

89 
fun dest_classrel tm = 

90 
let 

3788  91 
fun err () = raise TERM ("dest_classrel", [tm]); 
423  92 

3395  93 
val (ty, c2) = Logic.dest_inclass tm handle TERM _ => err (); 
94 
val c1 = (case dest_varT ty of (_, [c]) => c  _ => err ()) 

95 
handle TYPE _ => err (); 

6379  96 
in (c1, c2) end; 
423  97 

98 

99 
(* arities as terms *) 

100 

101 
fun mk_arity (t, ss, c) = 

102 
let 

449  103 
val names = tl (variantlist (replicate (length ss + 1) "'", [])); 
2266  104 
val tfrees = ListPair.map TFree (names, ss); 
6379  105 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  106 

107 
fun dest_arity tm = 

108 
let 

3788  109 
fun err () = raise TERM ("dest_arity", [tm]); 
423  110 

3395  111 
val (ty, c) = Logic.dest_inclass tm handle TERM _ => err (); 
112 
val (t, tvars) = 

423  113 
(case ty of 
3395  114 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  115 
 _ => err ()); 
116 
val ss = 

3395  117 
if null (gen_duplicates eq_fst tvars) 
118 
then map snd tvars else err (); 

6379  119 
in (t, ss, c) end; 
423  120 

121 

122 

560  123 
(** add theorems as axioms **) 
423  124 

125 
fun prep_thm_axm thy thm = 

126 
let 

127 
fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); 

128 

1237  129 
val {sign, hyps, prop, ...} = rep_thm thm; 
423  130 
in 
131 
if not (Sign.subsig (sign, sign_of thy)) then 

132 
err "theorem not of same theory" 

1237  133 
else if not (null (extra_shyps thm)) orelse not (null hyps) then 
423  134 
err "theorem may not contain hypotheses" 
135 
else prop 

136 
end; 

137 

138 
(*theorems expressing class relations*) 

139 
fun add_classrel_thms thms thy = 

140 
let 

141 
fun prep_thm thm = 

142 
let 

143 
val prop = prep_thm_axm thy thm; 

144 
val (c1, c2) = dest_classrel prop handle TERM _ => 

145 
raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]); 

146 
in (c1, c2) end; 

6379  147 
in Theory.add_classrel (map prep_thm thms) thy end; 
423  148 

149 
(*theorems expressing arities*) 

150 
fun add_arity_thms thms thy = 

151 
let 

152 
fun prep_thm thm = 

153 
let 

154 
val prop = prep_thm_axm thy thm; 

155 
val (t, ss, c) = dest_arity prop handle TERM _ => 

156 
raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]); 

157 
in (t, ss, [c]) end; 

6379  158 
in Theory.add_arities (map prep_thm thms) thy end; 
159 

160 

161 

162 
(** axclass info **) 

163 

164 
(* data kind 'Pure/axclasses' *) 

165 

166 
type axclass_info = 

167 
{super_classes: class list, 

168 
intro: thm, 

169 
axioms: thm list}; 

170 

171 
structure AxclassesArgs = 

172 
struct 

173 
val name = "Pure/axclasses"; 

174 
type T = axclass_info Symtab.table; 

175 

176 
val empty = Symtab.empty; 

177 
val prep_ext = I; 

178 
fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); 

179 

180 
fun print sg tab = 

181 
let 

182 
val ext_class = Sign.cond_extern sg Sign.classK; 

183 
val ext_thm = PureThy.cond_extern_thm_sg sg; 

184 

185 
fun pretty_class c cs = Pretty.block 

186 
(Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 :: 

187 
Pretty.breaks (map (Pretty.str o ext_class) cs)); 

188 

189 
fun pretty_thms name thms = Pretty.big_list (name ^ ":") (map Display.pretty_thm thms); 

190 

191 
fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks 

192 
[pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]); 

193 
in seq (Pretty.writeln o pretty_axclass) (Symtab.dest tab) end; 

194 
end; 

195 

196 
structure AxclassesData = TheoryDataFun(AxclassesArgs); 

197 
val print_axclasses = AxclassesData.print; 

198 

199 

200 
(* get and put data *) 

201 

202 
fun lookup_axclass_info_sg sg c = Symtab.lookup (AxclassesData.get_sg sg, c); 

203 

204 
fun get_axclass_info thy c = 

205 
(case lookup_axclass_info_sg (Theory.sign_of thy) c of 

206 
None => error ("Unknown axclass " ^ quote c) 

207 
 Some info => info); 

208 

209 
fun put_axclass_info c info thy = 

210 
thy > AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy)); 

423  211 

212 

213 

214 
(** add axiomatic type classes **) 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

215 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

216 
(* errors *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

217 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

218 
fun err_not_logic c = 
4917  219 
error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

220 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

221 
fun err_bad_axsort ax c = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

222 
error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

223 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

224 
fun err_bad_tfrees ax = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

225 
error ("More than one type variable in axiom " ^ quote ax); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

226 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

227 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

228 
(* ext_axclass *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

229 

6379  230 
fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

231 
let 
6379  232 
val sign = Theory.sign_of thy; 
3938  233 

6379  234 
val class = Sign.full_name sign bclass; 
235 
val super_classes = map (prep_class sign) raw_super_classes; 

236 
val axms = map (prep_axm sign o fst) raw_axioms_atts; 

237 
val atts = map (map (prep_att thy) o snd) raw_axioms_atts; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

238 

6379  239 
(*declare class*) 
240 
val class_thy = 

241 
thy > Theory.add_classes_i [(bclass, super_classes)]; 

242 
val class_sign = Theory.sign_of class_thy; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

243 

6379  244 
(*prepare abstract axioms*) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

245 
fun abs_axm ax = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

246 
if null (term_tfrees ax) then 
1498  247 
Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) 
3788  248 
else map_term_tfrees (K (aT [class])) ax; 
6379  249 
val abs_axms = map (abs_axm o #2) axms; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

250 

6379  251 
(*prepare introduction rule*) 
252 
val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

253 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

254 
fun axm_sort (name, ax) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

255 
(case term_tfrees ax of 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

256 
[] => [] 
6379  257 
 [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

258 
 _ => err_bad_tfrees name); 
6379  259 
val axS = Sign.norm_sort class_sign (logicC :: flat (map axm_sort axms)); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

260 

1498  261 
val int_axm = Logic.close_form o map_term_tfrees (K (aT axS)); 
262 
fun inclass c = Logic.mk_inclass (aT axS, c); 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

263 

1498  264 
val intro_axm = Logic.list_implies 
6379  265 
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); 
266 

267 
(*declare axioms and rule*) 

268 
val axms_thy = 

269 
class_thy 

270 
> Theory.add_path bclass 

271 
> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] 

272 
> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 

273 

274 
val intro = PureThy.get_thm axms_thy introN; 

275 
val axioms = PureThy.get_thms axms_thy axiomsN; 

276 
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; 

277 

278 
(*store info*) 

279 
val final_thy = 

280 
axms_thy 

281 
> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) 

282 
> Theory.parent_path 

283 
> PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)] 

284 
> put_axclass_info class info; 

285 
in (final_thy, {intro = intro, axioms = axioms}) end; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

286 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

287 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

288 
(* external interfaces *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

289 

6379  290 
val add_axclass = ext_axclass Sign.intern_class read_axm Attrib.global_attribute; 
291 
val add_axclass_i = ext_axclass (K I) cert_axm (K I); 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

292 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

293 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

294 

423  295 
(** prove class relations and type arities **) 
296 

297 
(* class_axms *) 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

298 

6379  299 
fun class_axms sign = 
300 
let val classes = Sign.classes sign in 

301 
map (Thm.class_triv sign) classes @ 

302 
mapfilter (apsome #intro o lookup_axclass_info_sg sign) classes 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

303 
end; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

304 

423  305 

6379  306 
(* expand classes *) 
307 

308 
fun expand_classes_tac st = 

309 
TRY (REPEAT_FIRST (resolve_tac (class_axms (Thm.sign_of_thm st)))) st; 

310 

311 
val expand_classes_method = 

312 
("expand_classes", Method.no_args (Method.METHOD0 expand_classes_tac), 

313 
"expand axiomatic type classes"); 

314 

315 

423  316 
(* axclass_tac *) 
317 

487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

318 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
1217  319 
try class_trivs first, then "cI" axioms 
423  320 
(2) rewrite goals using user supplied definitions 
321 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

322 

6379  323 
fun axclass_tac thms = 
1217  324 
let 
325 
val defs = filter is_def thms; 

326 
val non_defs = filter_out is_def thms; 

327 
in 

6379  328 
expand_classes_tac THEN 
1217  329 
TRY (rewrite_goals_tac defs) THEN 
330 
TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) 

331 
end; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

332 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

333 

423  334 
(* provers *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

335 

6379  336 
fun prove mk_prop str_of thy sig_prop thms usr_tac = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

337 
let 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

338 
val sign = sign_of thy; 
6379  339 
val goal = Thm.cterm_of sign (mk_prop sig_prop); 
340 
val tac = axclass_tac thms THEN (if_none usr_tac all_tac); 

423  341 
in 
342 
prove_goalw_cterm [] goal (K [tac]) 

343 
end 

344 
handle ERROR => error ("The error(s) above occurred while trying to prove " 

3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

345 
^ quote (str_of (sign_of thy, sig_prop))); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

346 

638  347 
val prove_subclass = 
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

348 
prove mk_classrel (fn (sg, c1_c2) => Sign.str_of_classrel sg c1_c2); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

349 

423  350 
val prove_arity = 
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

351 
prove mk_arity (fn (sg, (t, Ss, c)) => Sign.str_of_arity sg (t, Ss, [c])); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

352 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

353 

423  354 

449  355 
(** add proved subclass relations and arities **) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

356 

3949  357 
fun intrn_classrel sg c1_c2 = 
358 
pairself (Sign.intern_class sg) c1_c2; 

359 

6379  360 
fun intrn_arity intrn sg (t, Ss, x) = 
361 
(Sign.intern_tycon sg t, map (Sign.intern_sort sg) Ss, intrn sg x); 

362 

363 

364 
fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy = 

365 
let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in 

5685  366 
message ("Proving class inclusion " ^ 
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

367 
quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ..."); 
6379  368 
thy > add_classrel_thms [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac] 
3788  369 
end; 
423  370 

6379  371 
fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy = 
423  372 
let 
6379  373 
val sign = Theory.sign_of thy; 
374 
val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs); 

4934  375 
val wthms = witnesses thy names thms; 
423  376 
fun prove c = 
5685  377 
(message ("Proving type arity " ^ 
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

378 
quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ..."); 
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

379 
prove_arity thy (t, Ss, c) wthms usr_tac); 
6379  380 
in add_arity_thms (map prove cs) thy end; 
381 

382 

383 
val add_inst_subclass = ext_inst_subclass intrn_classrel; 

384 
val add_inst_subclass_i = ext_inst_subclass (K I); 

385 
val add_inst_arity = ext_inst_arity (intrn_arity Sign.intern_sort); 

386 
val add_inst_arity_i = ext_inst_arity (K I); 

387 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

388 

6379  389 
(* make oldstyle interactive goals *) 
390 

391 
fun mk_goal mk_prop thy sig_prop = 

392 
Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop)); 

393 

394 
val goal_subclass = mk_goal (mk_classrel oo intrn_classrel); 

395 
val goal_arity = mk_goal (mk_arity oo intrn_arity Sign.intern_class); 

396 

3788  397 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

398 

6379  399 
(** instance proof interfaces **) 
400 

401 
fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm); 

402 

403 
fun inst_proof mk_prop add_thms sig_prop thy = 

404 
thy 

405 
> IsarThy.theorem_i "" [inst_attribute add_thms] 

406 
(mk_prop (Theory.sign_of thy) sig_prop, []); 

3949  407 

6379  408 
val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms; 
409 
val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms; 

410 
val instance_arity_proof = inst_proof (mk_arity oo intrn_arity Sign.intern_class) add_arity_thms; 

411 
val instance_arity_proof_i = inst_proof (K mk_arity) add_arity_thms; 

412 

413 

414 

415 
(** package setup **) 

416 

417 
(* setup theory *) 

3949  418 

6379  419 
val setup = 
420 
[AxclassesData.init, 

421 
Method.add_methods [expand_classes_method]]; 

422 

423 

424 
(* outer syntax *) 

425 

426 
local open OuterParse in 

3949  427 

6379  428 
val axclassP = 
429 
OuterSyntax.command "axclass" "define axiomatic type class" 

430 
(name  Scan.optional ($$$ "<"  !!! (list1 xname)) []  Scan.repeat spec_name 

431 
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); 

432 

433 
val instanceP = 

434 
OuterSyntax.command "instance" "prove type arity or subclass relation" 

435 
((xname  ($$$ "<"  xname) >> instance_subclass_proof  

436 
xname  ($$$ "::"  simple_arity) >> (instance_arity_proof o triple2)) 

437 
>> (Toplevel.print oo Toplevel.theory_to_proof)); 

438 

439 
val _ = OuterSyntax.add_parsers [axclassP, instanceP]; 

440 

441 
end; 

3949  442 

443 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

444 
end; 