author  wenzelm 
Tue, 28 Oct 1997 17:27:10 +0100  
changeset 4015  92874142156b 
parent 3988  6ff1a1e2bd21 
child 4845  fdc7d8949d82 
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 

4015  36 

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

37 
(** utilities **) 
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 
(* type vars *) 
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 
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

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

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

46 

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

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

48 

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

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

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

53 

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

54 
(* get axioms and theorems *) 
404
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 get_ax thy name = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

60 

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

62 

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

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

64 
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

65 

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

66 

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

67 

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

70 
(* subclass relations as terms *) 

71 

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

74 
fun dest_classrel tm = 

75 
let 

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

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

80 
handle TYPE _ => err (); 

423  81 
in 
82 
(c1, c2) 

83 
end; 

84 

85 

86 
(* arities as terms *) 

87 

88 
fun mk_arity (t, ss, c) = 

89 
let 

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

96 
fun dest_arity tm = 

97 
let 

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

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

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

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

423  108 
in 
109 
(t, ss, c) 

110 
end; 

111 

112 

113 

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

116 
fun prep_thm_axm thy thm = 

117 
let 

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

119 

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

123 
err "theorem not of same theory" 

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

127 
end; 

128 

129 
(*theorems expressing class relations*) 

130 
fun add_classrel_thms thms thy = 

131 
let 

132 
fun prep_thm thm = 

133 
let 

134 
val prop = prep_thm_axm thy thm; 

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

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

137 
in (c1, c2) end; 

138 
in 

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

142 
(*theorems expressing arities*) 

143 
fun add_arity_thms thms thy = 

144 
let 

145 
fun prep_thm thm = 

146 
let 

147 
val prop = prep_thm_axm thy thm; 

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

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

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

151 
in 

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

155 

156 

157 
(** add axiomatic type classes **) 

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

158 

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

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

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

165 
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

166 

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

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

168 
error ("More than one type variable in axiom " ^ quote ax); 
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 

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

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

172 

3788  173 
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

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

177 
val class = Sign.full_name old_sign raw_class; 

178 

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

181 
[(raw_class, raw_super_classes)] old_thy; 

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

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

185 
else raw_super_classes; 

404
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 
1498  192 
Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) 
3788  193 
else map_term_tfrees (K (aT [class])) ax; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

194 

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

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

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

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

199 

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

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

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

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

203 

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

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

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

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

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

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

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

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

211 

3788  212 
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

213 

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

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

216 

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

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

219 
in 
4015  220 
PureThy.add_store_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

225 

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

404
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 

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

230 

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

233 
(* class_axms *) 

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

234 

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

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

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

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

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

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

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

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

243 

423  244 

245 
(* axclass_tac *) 

246 

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

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

251 

252 
fun axclass_tac thy thms = 

1217  253 
let 
254 
val defs = filter is_def thms; 

255 
val non_defs = filter_out is_def thms; 

256 
in 

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

258 
TRY (rewrite_goals_tac defs) THEN 

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

260 
end; 

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

261 

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

262 

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

264 

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

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

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

270 
in 

271 
prove_goalw_cterm [] goal (K [tac]) 

272 
end 

273 
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

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

275 

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

277 
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

278 

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

280 
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

281 

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

282 

423  283 

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

285 

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

288 

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

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

293 
else raw_c1_c2; 

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

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

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

299 
end; 

423  300 

3788  301 

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

304 

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

3949  309 
if int then intrn_arity sign Sign.intern_sort (raw_t, raw_Ss, raw_cs) 
3788  310 
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

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

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

314 
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

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

318 
end; 

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

319 

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

322 
val add_inst_arity = ext_inst_arity true; 

323 
val add_inst_arity_i = ext_inst_arity false; 

324 

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

325 

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

328 
fun mk_goal term_of thy sig_prop = 

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

330 

331 
fun goal_subclass thy = 

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

333 

334 
fun goal_arity thy = 

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

336 

337 

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

338 
end; 