author  wenzelm 
Fri, 16 Apr 2004 20:59:09 +0200  
changeset 14605  9de4d64eee3b 
parent 12876  a70df1e5bf10 
child 14695  9c78044b99c3 
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 
11539  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

5 

6379  6 
Axiomatic type class package. 
404
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 

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

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

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

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

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

11828  19 
val add_inst_subclass_x: xclass * xclass > string list > thm list 
3788  20 
> tactic option > theory > theory 
11828  21 
val add_inst_subclass: xclass * xclass > tactic > theory > theory 
22 
val add_inst_subclass_i: class * class > tactic > theory > theory 

23 
val add_inst_arity_x: xstring * string list * string > string list 

3938  24 
> thm list > tactic option > theory > theory 
11828  25 
val add_inst_arity: xstring * string list * string > tactic > theory > theory 
26 
val add_inst_arity_i: string * sort list * sort > tactic > theory > theory 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

27 
val default_intro_classes_tac: thm list > tactic 
6379  28 
val axclass_tac: thm list > tactic 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

29 
val instance_subclass_proof: xclass * xclass > bool > theory > ProofHistory.T 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

30 
val instance_subclass_proof_i: class * class > bool > theory > ProofHistory.T 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

31 
val instance_arity_proof: xstring * string list * string > bool > theory > ProofHistory.T 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

32 
val instance_arity_proof_i: string * sort list * sort > bool > theory > ProofHistory.T 
6379  33 
val setup: (theory > theory) list 
3938  34 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

35 

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

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

38 

4015  39 

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

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

41 

5685  42 
(* messages *) 
43 

44 
val quiet_mode = ref false; 

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

46 

47 

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

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

49 

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

50 
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

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

52 
 map_typ_frees _ a = a; 
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 
val map_term_tfrees = map_term_types o map_typ_frees; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

55 

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

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

57 

3395  58 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
59 
 dest_varT (TVar xi_S) = xi_S 

3788  60 
 dest_varT T = raise TYPE ("dest_varT", [T], []); 
3395  61 

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

62 

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

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

64 

1498  65 
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

66 

4934  67 
fun witnesses thy names thms = 
6379  68 
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

69 

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

70 

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

71 

560  72 
(** abstract syntax operations **) 
423  73 

6379  74 
(* names *) 
75 

76 
fun intro_name c = c ^ "I"; 

77 
val introN = "intro"; 

78 
val axiomsN = "axioms"; 

79 

80 

423  81 
(* subclass relations as terms *) 
82 

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

85 
fun dest_classrel tm = 

86 
let 

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

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

91 
handle TYPE _ => err (); 

6379  92 
in (c1, c2) end; 
423  93 

94 

95 
(* arities as terms *) 

96 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

97 
fun mk_arity (t, Ss, c) = 
423  98 
let 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

99 
val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss); 
6379  100 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  101 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

102 
fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S; 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

103 

423  104 
fun dest_arity tm = 
105 
let 

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

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

423  110 
(case ty of 
3395  111 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  112 
 _ => err ()); 
113 
val ss = 

3395  114 
if null (gen_duplicates eq_fst tvars) 
115 
then map snd tvars else err (); 

6379  116 
in (t, ss, c) end; 
423  117 

118 

119 

560  120 
(** add theorems as axioms **) 
423  121 

122 
fun prep_thm_axm thy thm = 

123 
let 

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

125 

1237  126 
val {sign, hyps, prop, ...} = rep_thm thm; 
423  127 
in 
6390  128 
if not (Sign.subsig (sign, Theory.sign_of thy)) then 
423  129 
err "theorem not of same theory" 
1237  130 
else if not (null (extra_shyps thm)) orelse not (null hyps) then 
423  131 
err "theorem may not contain hypotheses" 
132 
else prop 

133 
end; 

134 

135 
(*theorems expressing class relations*) 

136 
fun add_classrel_thms thms thy = 

137 
let 

138 
fun prep_thm thm = 

139 
let 

140 
val prop = prep_thm_axm thy thm; 

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

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

143 
in (c1, c2) end; 

8897  144 
in Theory.add_classrel_i (map prep_thm thms) thy end; 
423  145 

146 
(*theorems expressing arities*) 

147 
fun add_arity_thms thms thy = 

148 
let 

149 
fun prep_thm thm = 

150 
let 

151 
val prop = prep_thm_axm thy thm; 

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

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

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

8897  155 
in Theory.add_arities_i (map prep_thm thms) thy end; 
6379  156 

157 

158 

159 
(** axclass info **) 

160 

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

162 

163 
type axclass_info = 

164 
{super_classes: class list, 

165 
intro: thm, 

166 
axioms: thm list}; 

167 

168 
structure AxclassesArgs = 

169 
struct 

170 
val name = "Pure/axclasses"; 

171 
type T = axclass_info Symtab.table; 

172 

173 
val empty = Symtab.empty; 

6546  174 
val copy = I; 
6379  175 
val prep_ext = I; 
176 
fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); 

177 

178 
fun print sg tab = 

179 
let 

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

181 
val ext_thm = PureThy.cond_extern_thm_sg sg; 

182 

183 
fun pretty_class c cs = Pretty.block 

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

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

186 

10008  187 
fun pretty_thms name thms = Pretty.big_list (name ^ ":") 
188 
(map (Display.pretty_thm_sg sg) thms); 

6379  189 

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

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

8720  192 
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end; 
6379  193 
end; 
194 

195 
structure AxclassesData = TheoryDataFun(AxclassesArgs); 

196 
val print_axclasses = AxclassesData.print; 

197 

198 

199 
(* get and put data *) 

200 

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

202 

203 
fun get_axclass_info thy c = 

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

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

206 
 Some info => info); 

207 

208 
fun put_axclass_info c info thy = 

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

423  210 

211 

212 

213 
(** add axiomatic type classes **) 

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

214 

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

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

216 

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

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

219 

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

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

221 
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

222 

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

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

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

225 

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 
(* ext_axclass *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

228 

6379  229 
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

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

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

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

236 
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

237 

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

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

241 
val class_sign = Theory.sign_of class_thy; 

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

242 

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

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

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

249 

6379  250 
(*prepare introduction rule*) 
251 
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

252 

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

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

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

255 
[] => [] 
6379  256 
 [(_, 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

257 
 _ => err_bad_tfrees name); 
6379  258 
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

259 

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

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

262 

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

266 
(*declare axioms and rule*) 

8420  267 
val (axms_thy, ([intro], [axioms])) = 
6379  268 
class_thy 
269 
> Theory.add_path bclass 

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

8420  271 
>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 
6379  272 
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; 
273 

274 
(*store info*) 

275 
val final_thy = 

276 
axms_thy 

8420  277 
> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) 
6379  278 
> Theory.parent_path 
8420  279 
> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]) 
6379  280 
> put_axclass_info class info; 
281 
in (final_thy, {intro = intro, axioms = axioms}) end; 

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

282 

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

283 

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

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

285 

6390  286 
val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute; 
287 
val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I); 

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

288 

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

289 

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

290 

423  291 
(** prove class relations and type arities **) 
292 

293 
(* class_axms *) 

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

294 

6379  295 
fun class_axms sign = 
296 
let val classes = Sign.classes sign in 

297 
map (Thm.class_triv sign) classes @ 

298 
mapfilter (apsome #intro o lookup_axclass_info_sg sign) classes 

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

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

300 

423  301 

7351  302 
(* intro_classes *) 
6379  303 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

304 
fun intro_classes_tac facts st = 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

305 
(ALLGOALS (Method.insert_tac facts THEN' 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

306 
REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

307 
THEN Tactic.distinct_subgoals_tac) st; 
6379  308 

7351  309 
val intro_classes_method = 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

310 
("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 
7351  311 
"backchain introduction rules of axiomatic type classes"); 
6379  312 

313 

10309  314 
(* default method *) 
315 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

316 
fun default_intro_classes_tac [] = intro_classes_tac [] 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

317 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 
10309  318 

319 
fun default_tac rules ctxt facts = 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

320 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

321 
default_intro_classes_tac facts; 
10309  322 

323 
val default_method = 

12371  324 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule"); 
10309  325 

326 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

327 
(* oldstyle axclass_tac *) 
423  328 

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

329 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
1217  330 
try class_trivs first, then "cI" axioms 
423  331 
(2) rewrite goals using user supplied definitions 
332 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

333 

6379  334 
fun axclass_tac thms = 
1217  335 
let 
336 
val defs = filter is_def thms; 

337 
val non_defs = filter_out is_def thms; 

338 
in 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

339 
intro_classes_tac [] THEN 
1217  340 
TRY (rewrite_goals_tac defs) THEN 
341 
TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) 

342 
end; 

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

343 

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

344 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

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

346 

11969  347 
fun prove mk_prop str_of sign prop thms usr_tac = 
348 
(Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac))) 

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

350 
quote (str_of sign prop))) > Drule.standard; 

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

351 

638  352 
val prove_subclass = 
11969  353 
prove mk_classrel (fn sg => fn c1_c2 => Sign.str_of_classrel sg c1_c2); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

354 

423  355 
val prove_arity = 
11969  356 
prove mk_arity (fn sg => fn (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

357 

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

358 

423  359 

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

361 

8897  362 
(* prepare classes and arities *) 
363 

364 
fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c); 

365 

366 
fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc; 

367 
fun read_classrel sg cc = Library.pairself (read_class sg) cc; 

3949  368 

8897  369 
fun check_tycon sg t = 
370 
let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in 

371 
if is_some (Symtab.lookup (abbrs, t)) then 

372 
error ("Illegal type abbreviation: " ^ quote t) 

373 
else if is_none (Symtab.lookup (tycons, t)) then 

374 
error ("Undeclared type constructor: " ^ quote t) 

375 
else t 

8716  376 
end; 
6379  377 

8897  378 
fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) = 
379 
(check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x); 

380 

381 
val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort; 

382 
val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort; 

383 

384 

385 
(* oldstyle instance declarations *) 

6379  386 

387 
fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy = 

11969  388 
let 
389 
val sign = Theory.sign_of thy; 

390 
val c1_c2 = prep_classrel sign raw_c1_c2; 

391 
in 

392 
message ("Proving class inclusion " ^ quote (Sign.str_of_classrel sign c1_c2) ^ " ..."); 

393 
thy > add_classrel_thms [prove_subclass sign c1_c2 (witnesses thy names thms) usr_tac] 

3788  394 
end; 
423  395 

6379  396 
fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy = 
423  397 
let 
6379  398 
val sign = Theory.sign_of thy; 
399 
val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs); 

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

403 
quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ..."); 
11969  404 
prove_arity sign (t, Ss, c) wthms usr_tac); 
6379  405 
in add_arity_thms (map prove cs) thy end; 
406 

11828  407 
fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac); 
408 
fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (Some tac); 

6379  409 

11828  410 
val add_inst_subclass_x = ext_inst_subclass read_classrel; 
411 
val add_inst_subclass = sane_inst_subclass read_classrel; 

412 
val add_inst_subclass_i = sane_inst_subclass cert_classrel; 

413 
val add_inst_arity_x = ext_inst_arity read_arity; 

414 
val add_inst_arity = sane_inst_arity read_arity; 

415 
val add_inst_arity_i = sane_inst_arity cert_arity; 

6379  416 

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

417 

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

418 

6379  419 
(** instance proof interfaces **) 
420 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

421 
fun inst_proof mk_prop add_thms inst int theory = 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

422 
theory 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

423 
> IsarThy.multi_theorem_i Drule.internalK 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

424 
("", [fn (thy, th) => (add_thms [th] thy, th)]) [] 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

425 
(map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int; 
6379  426 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

427 
val instance_subclass_proof = 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

428 
inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

429 
val instance_subclass_proof_i = 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

430 
inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

431 
val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

432 
val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; 
6379  433 

434 

435 

436 
(** package setup **) 

437 

438 
(* setup theory *) 

3949  439 

6379  440 
val setup = 
441 
[AxclassesData.init, 

10309  442 
Method.add_methods [intro_classes_method, default_method]]; 
6379  443 

444 

445 
(* outer syntax *) 

446 

6719  447 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
3949  448 

6379  449 
val axclassP = 
6719  450 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

451 
((P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

452 
P.!!! (P.list1 P.xname)) [])  Scan.repeat P.spec_name 
6379  453 
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); 
454 

455 
val instanceP = 

6719  456 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

457 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.xname) >> instance_subclass_proof  
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

458 
(P.xname  (P.$$$ "::"  P.arity) >> P.triple2) >> instance_arity_proof) 
6379  459 
>> (Toplevel.print oo Toplevel.theory_to_proof)); 
460 

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

462 

463 
end; 

3949  464 

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

465 
end; 