author  paulson 
Fri, 16 Feb 1996 11:35:52 +0100  
changeset 1498  7b7d20e89b1b 
parent 1237  45ac644b0052 
child 2266  82aef6857c5b 
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 = 
1498  9 
sig 
10 
val add_thms_as_axms: (string * thm) list > theory > theory 

11 
val add_classrel_thms: thm list > theory > theory 

12 
val add_arity_thms: thm list > theory > theory 

13 
val add_axclass: class * class list > (string * string) list 

14 
> theory > theory 

15 
val add_axclass_i: class * class list > (string * term) list 

16 
> theory > theory 

17 
val add_inst_subclass: class * class > string list > thm list 

18 
> tactic option > theory > theory 

19 
val add_inst_arity: string * sort list * class list > string list 

20 
> thm list > tactic option > theory > theory 

21 
val axclass_tac: theory > thm list > tactic 

22 
val prove_subclass: theory > class * class > thm list 

23 
> tactic option > thm 

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

25 
> tactic option > thm 

26 
val goal_subclass: theory > class * class > thm list 

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

28 
end; 

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

29 

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

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

32 

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

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

34 

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

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

36 

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

37 
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

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

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

40 

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

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

42 

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

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

44 

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

45 

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

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

47 

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

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

49 
Some (get_axiom thy name) handle THEORY _ => None; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

50 

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

51 
val get_axioms = mapfilter o get_ax; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

52 

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

54 

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

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

56 
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

57 

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

58 

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

59 

560  60 
(** abstract syntax operations **) 
423  61 

62 
(* subclass relations as terms *) 

63 

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

66 
fun dest_classrel tm = 

67 
let 

68 
fun err () = raise_term "dest_classrel" [tm]; 

69 

1498  70 
val (ty, c2) = Logic.dest_inclass (Logic.freeze_vars tm) 
71 
handle TERM _ => err (); 

423  72 
val c1 = (case ty of TFree (_, [c]) => c  _ => err ()); 
73 
in 

74 
(c1, c2) 

75 
end; 

76 

77 

78 
(* arities as terms *) 

79 

80 
fun mk_arity (t, ss, c) = 

81 
let 

449  82 
val names = tl (variantlist (replicate (length ss + 1) "'", [])); 
423  83 
val tfrees = map TFree (names ~~ ss); 
84 
in 

1498  85 
Logic.mk_inclass (Type (t, tfrees), c) 
423  86 
end; 
87 

88 
fun dest_arity tm = 

89 
let 

90 
fun err () = raise_term "dest_arity" [tm]; 

91 

1498  92 
val (ty, c) = Logic.dest_inclass (Logic.freeze_vars tm) 
93 
handle TERM _ => err (); 

423  94 
val (t, tfrees) = 
95 
(case ty of 

96 
Type (t, tys) => (t, map (fn TFree x => x  _ => err ()) tys) 

97 
 _ => err ()); 

98 
val ss = 

99 
if null (gen_duplicates eq_fst tfrees) 

100 
then map snd tfrees else err (); 

101 
in 

102 
(t, ss, c) 

103 
end; 

104 

105 

106 

560  107 
(** add theorems as axioms **) 
423  108 

109 
fun prep_thm_axm thy thm = 

110 
let 

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

112 

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

116 
err "theorem not of same theory" 

1237  117 
else if not (null (extra_shyps thm)) orelse not (null hyps) then 
423  118 
err "theorem may not contain hypotheses" 
119 
else prop 

120 
end; 

121 

122 
(*general theorems*) 

123 
fun add_thms_as_axms thms thy = 

124 
add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy; 

125 

126 
(*theorems expressing class relations*) 

127 
fun add_classrel_thms thms thy = 

128 
let 

129 
fun prep_thm thm = 

130 
let 

131 
val prop = prep_thm_axm thy thm; 

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

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

134 
in (c1, c2) end; 

135 
in 

136 
add_classrel (map prep_thm thms) thy 

137 
end; 

138 

139 
(*theorems expressing arities*) 

140 
fun add_arity_thms thms thy = 

141 
let 

142 
fun prep_thm thm = 

143 
let 

144 
val prop = prep_thm_axm thy thm; 

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

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

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

148 
in 

149 
add_arities (map prep_thm thms) thy 

150 
end; 

151 

152 

153 

154 
(** add axiomatic type classes **) 

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

155 

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

156 
(* errors *) 
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 
fun err_not_logic c = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

160 

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

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

162 
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

163 

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

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

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

166 

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

167 

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

168 
(* ext_axclass *) 
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 
fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

172 
val axioms = map (prep_axm (sign_of old_thy)) raw_axioms; 
560  173 
val thy = add_classes [(class, super_classes)] old_thy; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

174 
val sign = sign_of thy; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

175 

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

176 

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

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

178 

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

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

180 
if null (term_tfrees ax) then 
1498  181 
Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

183 
map_term_tfrees (K (aT [class])) ax; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

184 

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

185 
val abs_axioms = map (apsnd abs_axm) axioms; 
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 

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

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

189 

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

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

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

192 
else err_not_logic class; 
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 
fun axm_sort (name, ax) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

195 
(case term_tfrees ax of 
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 
 [(_, S)] => 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

201 

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

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

203 

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

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

206 

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

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

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

210 
add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

212 

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

213 

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

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

217 
val add_axclass_i = ext_axclass cert_axm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

218 

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 

423  221 
(** prove class relations and type arities **) 
222 

223 
(* class_axms *) 

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

224 

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

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

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

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

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

229 
in 
1217  230 
map (class_triv thy) classes @ 
231 
get_axioms thy intros 

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

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

233 

423  234 

235 
(* axclass_tac *) 

236 

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

237 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
1217  238 
try class_trivs first, then "cI" axioms 
423  239 
(2) rewrite goals using user supplied definitions 
240 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

241 

242 
fun axclass_tac thy thms = 

1217  243 
let 
244 
val defs = filter is_def thms; 

245 
val non_defs = filter_out is_def thms; 

246 
in 

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

248 
TRY (rewrite_goals_tac defs) THEN 

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

250 
end; 

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

251 

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

252 

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

254 

423  255 
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

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

257 
val sign = sign_of thy; 
423  258 
val goal = cterm_of sign (term_of sig_prop); 
259 
val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac); 

260 
in 

261 
prove_goalw_cterm [] goal (K [tac]) 

262 
end 

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

264 
^ quote (str_of sig_prop)); 

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

265 

638  266 
val prove_subclass = 
423  267 
prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

268 

423  269 
val prove_arity = 
270 
prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c])); 

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

271 

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

272 

423  273 
(* make goals (for interactive use) *) 
274 

275 
fun mk_goal term_of thy sig_prop = 

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

277 

278 
val goal_subclass = mk_goal mk_classrel; 

279 
val goal_arity = mk_goal mk_arity; 

280 

281 

282 

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

284 

449  285 
fun add_inst_subclass (c1, c2) axms thms usr_tac thy = 
423  286 
add_classrel_thms 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

287 
[prove_subclass thy (c1, c2) (witnesses thy axms thms) usr_tac] thy; 
423  288 

449  289 
fun add_inst_arity (t, ss, cs) axms thms usr_tac thy = 
423  290 
let 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

291 
val wthms = witnesses thy axms thms; 
423  292 
fun prove c = 
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset

293 
prove_arity thy (t, ss, c) wthms usr_tac; 
423  294 
in 
295 
add_arity_thms (map prove cs) thy 

296 
end; 

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

297 

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

298 

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

299 
end; 