author  wenzelm 
Fri, 24 Oct 1997 17:11:48 +0200  
changeset 3988  6ff1a1e2bd21 
parent 3956  d59fe4579004 
child 4015  92874142156b 
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 

560  5 
User interfaces for axiomatic type classes. 
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 
1498  10 
val add_classrel_thms: thm list > theory > theory 
11 
val add_arity_thms: thm list > theory > theory 

3956  12 
val add_axclass: bclass * xclass list > (string * string) list 
1498  13 
> theory > theory 
3956  14 
val add_axclass_i: bclass * class list > (string * term) list 
1498  15 
> theory > theory 
3938  16 
val add_inst_subclass: xclass * xclass > string list > thm list 
17 
> tactic option > theory > theory 

3788  18 
val add_inst_subclass_i: class * class > string list > thm list 
19 
> tactic option > theory > theory 

3938  20 
val add_inst_arity: xstring * xsort list * xclass list > string list 
21 
> thm list > tactic option > theory > theory 

3788  22 
val add_inst_arity_i: string * sort list * class list > string list 
23 
> thm list > tactic option > theory > theory 

1498  24 
val axclass_tac: theory > thm list > tactic 
25 
val prove_subclass: theory > class * class > thm list 

26 
> tactic option > thm 

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

28 
> tactic option > thm 

3949  29 
val goal_subclass: theory > xclass * xclass > thm list 
30 
val goal_arity: theory > xstring * xsort list * xclass > thm list 

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

32 

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

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

35 

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

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

37 

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

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

39 

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

40 
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

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

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

43 

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

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

45 

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

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

47 

3395  48 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
49 
 dest_varT (TVar xi_S) = xi_S 

3788  50 
 dest_varT T = raise TYPE ("dest_varT", [T], []); 
3395  51 

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

52 

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

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

54 

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

55 
fun get_ax thy name = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

56 
Some (get_axiom thy name) handle THEORY _ => None; 
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 get_axioms = mapfilter o get_ax; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

59 

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

61 

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

62 
fun witnesses thy axms thms = 
1201
de2fc8cf9b6a
minor fix: instance now raises error if witness axioms don't exist;
wenzelm
parents:
886
diff
changeset

63 
map (get_axiom thy) axms @ 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

64 

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

65 

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

66 

560  67 
(** abstract syntax operations **) 
423  68 

69 
(* subclass relations as terms *) 

70 

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

73 
fun dest_classrel tm = 

74 
let 

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

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

79 
handle TYPE _ => err (); 

423  80 
in 
81 
(c1, c2) 

82 
end; 

83 

84 

85 
(* arities as terms *) 

86 

87 
fun mk_arity (t, ss, c) = 

88 
let 

449  89 
val names = tl (variantlist (replicate (length ss + 1) "'", [])); 
2266  90 
val tfrees = ListPair.map TFree (names, ss); 
423  91 
in 
1498  92 
Logic.mk_inclass (Type (t, tfrees), c) 
423  93 
end; 
94 

95 
fun dest_arity tm = 

96 
let 

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

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

423  101 
(case ty of 
3395  102 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  103 
 _ => err ()); 
104 
val ss = 

3395  105 
if null (gen_duplicates eq_fst tvars) 
106 
then map snd tvars else err (); 

423  107 
in 
108 
(t, ss, c) 

109 
end; 

110 

111 

112 

560  113 
(** add theorems as axioms **) 
423  114 

115 
fun prep_thm_axm thy thm = 

116 
let 

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

118 

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

122 
err "theorem not of same theory" 

1237  123 
else if not (null (extra_shyps thm)) orelse not (null hyps) then 
423  124 
err "theorem may not contain hypotheses" 
125 
else prop 

126 
end; 

127 

128 
(*theorems expressing class relations*) 

129 
fun add_classrel_thms thms thy = 

130 
let 

131 
fun prep_thm thm = 

132 
let 

133 
val prop = prep_thm_axm thy thm; 

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

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

136 
in (c1, c2) end; 

137 
in 

3764  138 
Theory.add_classrel (map prep_thm thms) thy 
423  139 
end; 
140 

141 
(*theorems expressing arities*) 

142 
fun add_arity_thms thms thy = 

143 
let 

144 
fun prep_thm thm = 

145 
let 

146 
val prop = prep_thm_axm thy thm; 

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

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

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

150 
in 

3764  151 
Theory.add_arities (map prep_thm thms) thy 
423  152 
end; 
153 

154 

155 

156 
(** add axiomatic type classes **) 

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

157 

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

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

159 

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

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

161 
error ("Axiomatic class " ^ quote c ^ " not subclass of \"logic\""); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

162 

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

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

164 
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

165 

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

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

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

168 

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

169 

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

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

171 

3788  172 
fun ext_axclass int prep_axm (raw_class, raw_super_classes) raw_axioms old_thy = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

173 
let 
3938  174 
val old_sign = sign_of old_thy; 
175 
val axioms = map (prep_axm old_sign) raw_axioms; 

176 
val class = Sign.full_name old_sign raw_class; 

177 

3788  178 
val thy = 
179 
(if int then Theory.add_classes else Theory.add_classes_i) 

180 
[(raw_class, raw_super_classes)] old_thy; 

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

181 
val sign = sign_of thy; 
3938  182 
val super_classes = 
183 
if int then map (Sign.intern_class sign) raw_super_classes 

184 
else raw_super_classes; 

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

185 

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

186 

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

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

188 

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

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

190 
if null (term_tfrees ax) then 
1498  191 
Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) 
3788  192 
else map_term_tfrees (K (aT [class])) ax; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

193 

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

194 
val abs_axioms = map (apsnd abs_axm) axioms; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

195 

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

196 

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

197 
(* prepare introduction orule *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

198 

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

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

200 
if Sign.subsort sign ([class], logicS) then () 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

202 

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

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

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

205 
[] => [] 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

206 
 [(_, S)] => 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

207 
if Sign.subsort sign ([class], S) then S 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

209 
 _ => err_bad_tfrees name); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

210 

3788  211 
val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms)) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

212 

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

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

215 

1498  216 
val intro_axm = Logic.list_implies 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

217 
(map inclass super_classes @ map (int_axm o snd) axioms, inclass class); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

218 
in 
3809  219 
Theory.add_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

221 

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

224 

3788  225 
val add_axclass = ext_axclass true read_axm; 
226 
val add_axclass_i = ext_axclass false cert_axm; 

404
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 

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

229 

423  230 
(** prove class relations and type arities **) 
231 

232 
(* class_axms *) 

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

233 

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

234 
fun class_axms thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

236 
val classes = Sign.classes (sign_of thy); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

237 
val intros = map (fn c => c ^ "I") classes; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

238 
in 
1217  239 
map (class_triv thy) classes @ 
240 
get_axioms thy intros 

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

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

242 

423  243 

244 
(* axclass_tac *) 

245 

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

246 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
1217  247 
try class_trivs first, then "cI" axioms 
423  248 
(2) rewrite goals using user supplied definitions 
249 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

250 

251 
fun axclass_tac thy thms = 

1217  252 
let 
253 
val defs = filter is_def thms; 

254 
val non_defs = filter_out is_def thms; 

255 
in 

256 
TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN 

257 
TRY (rewrite_goals_tac defs) THEN 

258 
TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) 

259 
end; 

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

260 

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

261 

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

263 

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

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

266 
val sign = sign_of thy; 
423  267 
val goal = cterm_of sign (term_of sig_prop); 
268 
val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac); 

269 
in 

270 
prove_goalw_cterm [] goal (K [tac]) 

271 
end 

272 
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

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

274 

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

276 
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

277 

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

279 
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

280 

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

281 

423  282 

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

284 

3949  285 
fun intrn_classrel sg c1_c2 = 
286 
pairself (Sign.intern_class sg) c1_c2; 

287 

3788  288 
fun ext_inst_subclass int raw_c1_c2 axms thms usr_tac thy = 
289 
let 

3949  290 
val c1_c2 = 
291 
if int then intrn_classrel (sign_of thy) raw_c1_c2 

292 
else raw_c1_c2; 

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

294 
writeln ("Proving class inclusion " ^ 
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

295 
quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ..."); 
3788  296 
add_classrel_thms 
297 
[prove_subclass thy c1_c2 (witnesses thy axms thms) usr_tac] thy 

298 
end; 

423  299 

3788  300 

3949  301 
fun intrn_arity sg intrn (t, Ss, x) = 
302 
(Sign.intern_tycon sg t, map (Sign.intern_sort sg) Ss, intrn sg x); 

303 

3788  304 
fun ext_inst_arity int (raw_t, raw_Ss, raw_cs) axms thms usr_tac thy = 
423  305 
let 
3788  306 
val sign = sign_of thy; 
307 
val (t, Ss, cs) = 

3949  308 
if int then intrn_arity sign Sign.intern_sort (raw_t, raw_Ss, raw_cs) 
3788  309 
else (raw_t, raw_Ss, raw_cs); 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

310 
val wthms = witnesses thy axms thms; 
423  311 
fun prove c = 
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

312 
(writeln ("Proving type arity " ^ 
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset

313 
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

314 
prove_arity thy (t, Ss, c) wthms usr_tac); 
423  315 
in 
316 
add_arity_thms (map prove cs) thy 

317 
end; 

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

318 

3788  319 
val add_inst_subclass = ext_inst_subclass true; 
320 
val add_inst_subclass_i = ext_inst_subclass false; 

321 
val add_inst_arity = ext_inst_arity true; 

322 
val add_inst_arity_i = ext_inst_arity false; 

323 

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

324 

3949  325 
(* make goals (for interactive use) *) 
326 

327 
fun mk_goal term_of thy sig_prop = 

328 
goalw_cterm [] (cterm_of (sign_of thy) (term_of sig_prop)); 

329 

330 
fun goal_subclass thy = 

331 
mk_goal (mk_classrel o intrn_classrel (sign_of thy)) thy; 

332 

333 
fun goal_arity thy = 

334 
mk_goal (mk_arity o intrn_arity (sign_of thy) Sign.intern_class) thy; 

335 

336 

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

337 
end; 