author  wenzelm 
Tue, 01 Aug 1995 17:20:21 +0200  
changeset 1217  f96a04c6b352 
parent 1201  de2fc8cf9b6a 
child 1237  45ac644b0052 
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 = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

10 
structure Tactical: TACTICAL 
560  11 
local open Tactical Tactical.Thm in 
423  12 
val add_thms_as_axms: (string * thm) list > theory > theory 
13 
val add_classrel_thms: thm list > theory > theory 

14 
val add_arity_thms: thm list > theory > theory 

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

15 
val add_axclass: class * class list > (string * string) list 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

17 
val add_axclass_i: class * class list > (string * term) list 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

18 
> theory > theory 
449  19 
val add_inst_subclass: class * class > string list > thm list 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

20 
> tactic option > theory > theory 
449  21 
val add_inst_arity: string * sort list * class list > string list 
423  22 
> thm list > tactic option > theory > theory 
474  23 
val axclass_tac: theory > thm list > tactic 
638  24 
val prove_subclass: theory > class * class > thm list 
25 
> tactic option > thm 

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

27 
> tactic option > thm 

474  28 
val goal_subclass: theory > class * class > thm list 
29 
val goal_arity: theory > string * sort list * class > thm list 

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

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

31 
end; 
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 
functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC 
474  34 
sharing Goals.Tactical = Tactic.Tactical): AX_CLASS = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

35 
struct 
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 
structure Tactical = Goals.Tactical; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

38 
structure Thm = Tactical.Thm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

39 
structure Sign = Thm.Sign; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

40 
structure Type = Sign.Type; 
487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

41 
structure Pretty = Sign.Syntax.Pretty; 
404
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 
open Logic Thm Tactical Tactic Goals; 
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 

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

46 
(** utilities **) 
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 
(* 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 

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

58 

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

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

60 

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

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

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

63 

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

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

65 

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

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

67 

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

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

69 
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

70 

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

71 

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

72 

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

75 
(* subclass relations as terms *) 

76 

77 
fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2); 

78 

79 
fun dest_classrel tm = 

80 
let 

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

82 

83 
val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err (); 

84 
val c1 = (case ty of TFree (_, [c]) => c  _ => err ()); 

85 
in 

86 
(c1, c2) 

87 
end; 

88 

89 

90 
(* arities as terms *) 

91 

92 
fun mk_arity (t, ss, c) = 

93 
let 

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

97 
mk_inclass (Type (t, tfrees), c) 

98 
end; 

99 

100 
fun dest_arity tm = 

101 
let 

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

103 

104 
val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err (); 

105 
val (t, tfrees) = 

106 
(case ty of 

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

108 
 _ => err ()); 

109 
val ss = 

110 
if null (gen_duplicates eq_fst tfrees) 

111 
then map snd tfrees else err (); 

112 
in 

113 
(t, ss, c) 

114 
end; 

115 

116 

117 

560  118 
(** add theorems as axioms **) 
423  119 

120 
fun prep_thm_axm thy thm = 

121 
let 

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

123 

1217  124 
val {sign, shyps, hyps, prop, ...} = rep_thm thm; 
423  125 
in 
126 
if not (Sign.subsig (sign, sign_of thy)) then 

127 
err "theorem not of same theory" 

1217  128 
else if not (null shyps) orelse not (null hyps) then 
423  129 
err "theorem may not contain hypotheses" 
130 
else prop 

131 
end; 

132 

133 
(*general theorems*) 

134 
fun add_thms_as_axms thms thy = 

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

136 

137 
(*theorems expressing class relations*) 

138 
fun add_classrel_thms thms thy = 

139 
let 

140 
fun prep_thm thm = 

141 
let 

142 
val prop = prep_thm_axm thy thm; 

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

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

145 
in (c1, c2) end; 

146 
in 

147 
add_classrel (map prep_thm thms) thy 

148 
end; 

149 

150 
(*theorems expressing arities*) 

151 
fun add_arity_thms thms thy = 

152 
let 

153 
fun prep_thm thm = 

154 
let 

155 
val prop = prep_thm_axm thy thm; 

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

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

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

159 
in 

160 
add_arities (map prep_thm thms) thy 

161 
end; 

162 

163 

164 

165 
(** add axiomatic type classes **) 

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

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

171 

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

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

173 
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

174 

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

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

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

177 

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

180 

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

181 
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

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

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

185 
val sign = sign_of thy; 
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 abstract axioms *) 
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 
fun abs_axm ax = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

191 
if null (term_tfrees ax) then 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

192 
mk_implies (mk_inclass (aT logicS, class), ax) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

194 
map_term_tfrees (K (aT [class])) ax; 
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 
val abs_axioms = map (apsnd abs_axm) axioms; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

197 

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

200 

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

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

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

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

204 

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

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

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

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

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

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

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

211 
 _ => err_bad_tfrees name); 
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 
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

214 

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

215 
val int_axm = close_form o map_term_tfrees (K (aT axS)); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

216 
fun inclass c = mk_inclass (aT axS, c); 
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 
val intro_axm = list_implies 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

222 
end; 
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 

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

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

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

229 

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

230 

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

231 

423  232 
(** prove class relations and type arities **) 
233 

234 
(* class_axms *) 

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

235 

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

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

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

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

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

240 
in 
1217  241 
map (class_triv thy) classes @ 
242 
get_axioms thy intros 

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

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

244 

423  245 

246 
(* axclass_tac *) 

247 

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

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

252 

253 
fun axclass_tac thy thms = 

1217  254 
let 
255 
val defs = filter is_def thms; 

256 
val non_defs = filter_out is_def thms; 

257 
in 

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

259 
TRY (rewrite_goals_tac defs) THEN 

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

261 
end; 

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

262 

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

263 

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

265 

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

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

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

271 
in 

272 
prove_goalw_cterm [] goal (K [tac]) 

273 
end 

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

275 
^ quote (str_of sig_prop)); 

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

276 

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

279 

423  280 
val prove_arity = 
281 
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

282 

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

283 

423  284 
(* make goals (for interactive use) *) 
285 

286 
fun mk_goal term_of thy sig_prop = 

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

288 

289 
val goal_subclass = mk_goal mk_classrel; 

290 
val goal_arity = mk_goal mk_arity; 

291 

292 

293 

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

295 

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

298 
[prove_subclass thy (c1, c2) (witnesses thy axms thms) usr_tac] thy; 
423  299 

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

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

304 
prove_arity thy (t, ss, c) wthms usr_tac; 
423  305 
in 
306 
add_arity_thms (map prove cs) thy 

307 
end; 

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

308 

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

309 

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

310 
end; 