author  wenzelm 
Wed, 06 Jul 1994 12:49:56 +0200  
changeset 449  75ac32497f09 
parent 423  a42892e72854 
child 474  ac1d1988d528 
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 

423  5 
Higher level user interfaces for axiomatic type classes. 
449  6 

7 
TODO: 

8 
remove add_sigclass (?) 

9 
remove goal_... (?) 

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

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

11 

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

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

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

14 
structure Tactical: TACTICAL 
423  15 
local open Tactical Tactical.Thm Tactical.Thm.Sign.Syntax.Mixfix in 
16 
val add_thms_as_axms: (string * thm) list > theory > theory 

17 
val add_classrel_thms: thm list > theory > theory 

18 
val add_arity_thms: thm list > theory > theory 

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

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

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

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

22 
> theory > theory 
423  23 
val add_sigclass: class * class list > (string * string * mixfix) list 
24 
> theory > theory 

25 
val add_sigclass_i: class * class list > (string * typ * mixfix) list 

26 
> theory > theory 

27 
val axclass_tac: theory > thm list > tactic 

28 
val prove_classrel: theory > class * class > thm list 

29 
> tactic option > thm 

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

31 
> tactic option > thm 

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

33 
> tactic option > theory > theory 
449  34 
val add_inst_arity: string * sort list * class list > string list 
423  35 
> thm list > tactic option > theory > theory 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

38 

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

39 
functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

40 
sharing Goals.Tactical = Tactic.Tactical)(*: AX_CLASS *) = (* FIXME *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

42 

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

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

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

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

46 
structure Type = Sign.Type; 
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 
open Logic Thm Tactical Tactic Goals; 
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 

423  51 
(* FIXME fake!  remove *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

52 

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

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

54 
val add_defns_i = add_axioms_i; 
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 

423  57 

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

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

59 

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

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

61 

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

62 
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

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

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

67 

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

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

69 

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

72 

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

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

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

75 

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

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

77 

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

78 

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

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

80 

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

81 
fun is_defn thm = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

82 
(case #prop (rep_thm thm) of 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

83 
Const ("==", _) $ _ $ _ => true 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

85 

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

86 

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

87 

423  88 
(** abstract syntax operations **) (* FIXME > logic.ML (?) *) 
89 

90 
(* subclass relations as terms *) 

91 

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

93 

94 
fun dest_classrel tm = 

95 
let 

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

97 

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

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

100 
in 

101 
(c1, c2) 

102 
end; 

103 

104 

105 
(* arities as terms *) 

106 

107 
fun mk_arity (t, ss, c) = 

108 
let 

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

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

113 
end; 

114 

115 
fun dest_arity tm = 

116 
let 

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

118 

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

120 
val (t, tfrees) = 

121 
(case ty of 

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

123 
 _ => err ()); 

124 
val ss = 

125 
if null (gen_duplicates eq_fst tfrees) 

126 
then map snd tfrees else err (); 

127 
in 

128 
(t, ss, c) 

129 
end; 

130 

131 

132 

133 
(** add theorems as axioms **) (* FIXME > drule.ML (?) *) 

134 

135 
fun prep_thm_axm thy thm = 

136 
let 

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

138 

139 
val {sign, hyps, prop, ...} = rep_thm thm; 

140 
in 

141 
if not (Sign.subsig (sign, sign_of thy)) then 

142 
err "theorem not of same theory" 

143 
else if not (null hyps) then 

144 
err "theorem may not contain hypotheses" 

145 
else prop 

146 
end; 

147 

148 
(*general theorems*) 

149 
fun add_thms_as_axms thms thy = 

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

151 

152 
(*theorems expressing class relations*) 

153 
fun add_classrel_thms thms thy = 

154 
let 

155 
fun prep_thm thm = 

156 
let 

157 
val prop = prep_thm_axm thy thm; 

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

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

160 
in (c1, c2) end; 

161 
in 

162 
add_classrel (map prep_thm thms) thy 

163 
end; 

164 

165 
(*theorems expressing arities*) 

166 
fun add_arity_thms thms thy = 

167 
let 

168 
fun prep_thm thm = 

169 
let 

170 
val prop = prep_thm_axm thy thm; 

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

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

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

174 
in 

175 
add_arities (map prep_thm thms) thy 

176 
end; 

177 

178 

179 

180 
(** add axiomatic type classes **) 

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

181 

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

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

183 

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

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

185 
error ("Axiomatic class " ^ quote c ^ " not subclass of \"logic\""); 
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 
fun err_bad_axsort ax c = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

188 
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

189 

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

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

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

192 

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 
(* ext_axclass *) 
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 
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

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

198 
val axioms = map (prep_axm (sign_of old_thy)) raw_axioms; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

199 
val thy = add_classes [([], class, super_classes)] old_thy; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

200 
val sign = sign_of thy; 
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 

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

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

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

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

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

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

210 

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

211 
val abs_axioms = map (apsnd abs_axm) axioms; 
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 
(* prepare introduction orule *) 
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 _ = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

229 

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

230 
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

231 
fun inclass c = mk_inclass (aT axS, c); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

232 

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

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

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

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

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

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

238 

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

239 

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

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

241 

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

242 
val add_axclass = ext_axclass read_axm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

244 

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

245 

423  246 
(* add signature classes *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

247 

423  248 
fun ext_sigclass add_cnsts (class, super_classes) consts old_thy = 
249 
old_thy 

250 
> add_axclass (class, super_classes) [] 

251 
> add_defsort [class] 

252 
> add_cnsts consts 

253 
> add_defsort (Type.defaultS (#tsig (Sign.rep_sg (sign_of old_thy)))); 

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

254 

423  255 
val add_sigclass = ext_sigclass add_consts; 
256 
val add_sigclass_i = ext_sigclass add_consts_i; 

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

257 

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

258 

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

259 

423  260 
(** prove class relations and type arities **) 
261 

262 
(* class_axms *) 

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

263 

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

264 
fun class_axms thy = 
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 classes = Sign.classes (sign_of thy); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

269 
get_axioms thy intros @ 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

270 
map (class_triv thy) classes 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

272 

423  273 

274 
(* axclass_tac *) 

275 

276 
(*(1) repeatedly resolve goals of form "( ty : c_class )", 

277 
try "cI" axioms first and use class_triv as last resort 

278 
(2) rewrite goals using user supplied definitions 

279 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

280 

281 
fun axclass_tac thy thms = 

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

283 
TRY (rewrite_goals_tac (filter is_defn thms)) THEN 

284 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))); 

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

285 

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

286 

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

288 

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

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

291 
val sign = sign_of thy; 
423  292 
val goal = cterm_of sign (term_of sig_prop); 
293 
val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac); 

294 
in 

295 
prove_goalw_cterm [] goal (K [tac]) 

296 
end 

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

298 
^ quote (str_of sig_prop)); 

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

299 

423  300 
val prove_classrel = 
301 
prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2); 

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

302 

423  303 
val prove_arity = 
304 
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

305 

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

306 

423  307 
(* make goals (for interactive use) *) 
308 

309 
fun mk_goal term_of thy sig_prop = 

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

311 

312 
val goal_subclass = mk_goal mk_classrel; 

313 
val goal_arity = mk_goal mk_arity; 

314 

315 

316 

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

318 

449  319 
fun add_inst_subclass (c1, c2) axms thms usr_tac thy = 
423  320 
add_classrel_thms 
321 
[prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy; 

322 

449  323 
fun add_inst_arity (t, ss, cs) axms thms usr_tac thy = 
423  324 
let 
325 
val usr_thms = get_axioms thy axms @ thms; 

326 
fun prove c = 

327 
prove_arity thy (t, ss, c) usr_thms usr_tac; 

328 
in 

329 
add_arity_thms (map prove cs) thy 

330 
end; 

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

331 

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

332 

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

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

334 