author  haftmann 
Mon, 10 Apr 2006 08:30:26 +0200  
changeset 19398  8ad34412ea97 
parent 19392  a631cd2117a8 
child 19405  a551256aba15 
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 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

5 
Axiomatic type classes: pure logical content. 
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 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

10 
val mk_classrel: class * class > term 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

11 
val dest_classrel: term > class * class 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

12 
val mk_arity: string * sort list * class > term 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

13 
val mk_arities: string * sort list * sort > term list 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

14 
val dest_arity: term > string * sort list * class 
6379  15 
val print_axclasses: theory > unit 
19392  16 
val get_info: theory > class > {super_classes: class list, intro: thm, axioms: thm list} 
17 
val get_instances: theory > 

18 
{classrel: unit Graph.T, subsorts: ((sort * sort) * thm) list, arities: (arity * thm) list} 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

19 
val class_intros: theory > thm list 
17339  20 
val add_axclass: bstring * xstring list > ((bstring * string) * Attrib.src list) list > 
19392  21 
theory > class * theory 
18728  22 
val add_axclass_i: bstring * class list > ((bstring * term) * attribute list) list > 
19392  23 
theory > class * theory 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

24 
val add_classrel: thm list > theory > theory 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

25 
val add_arity: thm list > theory > theory 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

26 
val prove_subclass: class * class > tactic > theory > theory 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

27 
val prove_arity: string * sort list * sort > tactic > theory > theory 
3938  28 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

29 

15801  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 

4015  33 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

34 
(** abstract syntax operations **) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

35 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

36 
(* subclass propositions *) 
423  37 

19392  38 
fun mk_classrel (c1, c2) = Logic.mk_inclass (Term.aT [c1], c2); 
423  39 

40 
fun dest_classrel tm = 

41 
let 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

42 
fun err () = raise TERM ("AxClass.dest_classrel", [tm]); 
423  43 

3395  44 
val (ty, c2) = Logic.dest_inclass tm handle TERM _ => err (); 
19392  45 
val c1 = (case dest_TVar ty of (_, [c]) => c  _ => err ()) 
3395  46 
handle TYPE _ => err (); 
6379  47 
in (c1, c2) end; 
423  48 

49 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

50 
(* arity propositions *) 
423  51 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

52 
fun mk_arity (t, Ss, c) = 
423  53 
let 
14695  54 
val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss); 
6379  55 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  56 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

57 
fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S; 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

58 

423  59 
fun dest_arity tm = 
60 
let 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

61 
fun err () = raise TERM ("AxClass.dest_arity", [tm]); 
423  62 

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

423  65 
(case ty of 
19392  66 
Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) 
423  67 
 _ => err ()); 
68 
val ss = 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

69 
if has_duplicates (eq_fst (op =)) tvars then err () 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

70 
else map snd tvars; 
6379  71 
in (t, ss, c) end; 
423  72 

73 

74 

19392  75 
(** theory data **) 
76 

77 
(* axclass *) 

6379  78 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

79 
val introN = "intro"; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

80 
val axiomsN = "axioms"; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

81 

19392  82 
datatype axclass = AxClass of 
83 
{super_classes: class list, 

84 
intro: thm, 

85 
axioms: thm list}; 

86 

87 
fun make_axclass (super_classes, intro, axioms) = 

88 
AxClass {super_classes = super_classes, intro = intro, axioms = axioms}; 

89 

90 

91 
(* instances *) 

92 

93 
datatype instances = Instances of 

94 
{classrel: unit Graph.T, (*raw relation  no closure!*) 

95 
subsorts: ((sort * sort) * thm) list, 

96 
arities: (arity * thm) list}; 

97 

98 
fun make_instances (classrel, subsorts, arities) = 

99 
Instances {classrel = classrel, subsorts = subsorts, arities = arities}; 

6379  100 

19392  101 
fun map_instances f (Instances {classrel, subsorts, arities}) = 
102 
make_instances (f (classrel, subsorts, arities)); 

103 

104 
fun merge_instances 

105 
(Instances {classrel = classrel1, subsorts = subsorts1, arities = arities1}, 

106 
Instances {classrel = classrel2, subsorts = subsorts2, arities = arities2}) = 

107 
make_instances 

108 
(Graph.merge (K true) (classrel1, classrel2), 

109 
merge (eq_fst op =) (subsorts1, subsorts2), 

110 
merge (eq_fst op =) (arities1, arities2)); 

111 

112 

113 
(* setup data *) 

114 

115 
structure AxClassData = TheoryDataFun 

16458  116 
(struct 
19392  117 
val name = "Pure/axclass"; 
118 
type T = axclass Symtab.table * instances; 

6379  119 

19398  120 
val empty = (Symtab.empty, make_instances (Graph.empty, [], [])) : T; 
6546  121 
val copy = I; 
16458  122 
val extend = I; 
6379  123 

19392  124 
fun merge _ ((axclasses1, instances1), (axclasses2, instances2)) = 
125 
(Symtab.merge (K true) (axclasses1, axclasses2), merge_instances (instances1, instances2)); 

126 

127 
fun print thy (axclasses, _) = 

6379  128 
let 
129 
fun pretty_class c cs = Pretty.block 

16458  130 
(Pretty.str (Sign.extern_class thy c) :: Pretty.str " <" :: Pretty.brk 1 :: 
131 
Pretty.breaks (map (Pretty.str o Sign.extern_class thy) cs)); 

6379  132 

10008  133 
fun pretty_thms name thms = Pretty.big_list (name ^ ":") 
16458  134 
(map (Display.pretty_thm_sg thy) thms); 
6379  135 

19392  136 
fun pretty_axclass (name, AxClass {super_classes, intro, axioms}) = 
137 
Pretty.block (Pretty.fbreaks 

138 
[pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]); 

139 
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end; 

16458  140 
end); 
6379  141 

19392  142 
val _ = Context.add_setup AxClassData.init; 
143 
val print_axclasses = AxClassData.print; 

144 

145 
val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts); 

6379  146 

147 

19392  148 

149 
(** axclass definitions **) 

150 

151 
(* lookup *) 

152 

153 
val lookup_info = Symtab.lookup o #1 o AxClassData.get; 

6379  154 

17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

155 
fun get_info thy c = 
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

156 
(case lookup_info thy c of 
19392  157 
SOME (AxClass info) => info 
158 
 NONE => error ("Unknown axclass " ^ quote c)); 

6379  159 

19123  160 
fun class_intros thy = 
19392  161 
let 
162 
fun add_intro c = 

163 
(case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro  _ => I); 

164 
val classes = Sign.classes thy; 

165 
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

166 

a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

167 

19392  168 
(* add_axclass(_i) *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

169 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

170 
local 
404
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 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

178 
fun replace_tfree T = map_term_types (Term.map_atyps (fn TFree _ => T  U => U)); 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

179 

5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

180 
fun gen_axclass prep_class prep_axm prep_att 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

181 
(bclass, raw_super_classes) raw_axioms_atts thy = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

182 
let 
16458  183 
val class = Sign.full_name thy bclass; 
184 
val super_classes = map (prep_class thy) raw_super_classes; 

185 
val axms = map (prep_axm thy o fst) raw_axioms_atts; 

6379  186 
val atts = map (map (prep_att thy) o snd) raw_axioms_atts; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

187 

6379  188 
(*declare class*) 
189 
val class_thy = 

190 
thy > Theory.add_classes_i [(bclass, super_classes)]; 

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

191 

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

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

194 
if null (term_tfrees ax) then 
19392  195 
Logic.mk_implies (Logic.mk_inclass (Term.aT [], class), ax) 
196 
else replace_tfree (Term.aT [class]) ax; 

17756  197 
val abs_axms = map (abs_axm o snd) axms; 
404
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 
fun axm_sort (name, ax) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

201 
[] => [] 
16458  202 
 [(_, S)] => if Sign.subsort class_thy ([class], S) then S else err_bad_axsort name class 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

203 
 _ => err_bad_tfrees name); 
16458  204 
val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms)); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

205 

19392  206 
val int_axm = Logic.close_form o replace_tfree (Term.aT axS); 
207 
fun inclass c = Logic.mk_inclass (Term.aT axS, c); 

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

208 

1498  209 
val intro_axm = Logic.list_implies 
6379  210 
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); 
211 

212 
(*declare axioms and rule*) 

18377  213 
val (([intro], [axioms]), axms_thy) = 
6379  214 
class_thy 
18932  215 
> Theory.add_path (Logic.const_of_class bclass) 
6379  216 
> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] 
18377  217 
>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 
19392  218 
val info = make_axclass (super_classes, intro, axioms); 
6379  219 

220 
(*store info*) 

18377  221 
val (_, final_thy) = 
6379  222 
axms_thy 
19392  223 
> Theory.add_finals_i false [Const (Logic.const_of_class class, Term.a_itselfT > propT)] 
18377  224 
> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) 
225 
> Theory.restore_naming class_thy 

19392  226 
> AxClassData.map (apfst (Symtab.update (class, info))); 
227 
in (class, final_thy) end; 

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

228 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

230 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

231 
val add_axclass = gen_axclass Sign.intern_class Theory.read_axm Attrib.attribute; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

232 
val add_axclass_i = gen_axclass (K I) Theory.cert_axm (K I); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

233 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

234 
end; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

235 

a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

236 

a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

237 

19392  238 
(** instantiation proofs **) 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

239 

19392  240 
(* primitives *) 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

241 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

242 
fun add_classrel ths thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

243 
let 
19392  244 
fun add_rel (c1, c2) = 
245 
Graph.default_node (c1, ()) #> Graph.default_node (c2, ()) #> Graph.add_edge (c1, c2); 

246 
val rels = ths > map (fn th => 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

247 
let 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

248 
val prop = Drule.plain_prop_of (Thm.transfer thy th); 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

249 
val (c1, c2) = dest_classrel prop handle TERM _ => 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

250 
raise THM ("AxClass.add_classrel: not a class relation", 0, [th]); 
19392  251 
in (c1, c2) end); 
252 
in 

253 
thy 

254 
> Theory.add_classrel_i rels 

255 
> AxClassData.map (apsnd (map_instances (fn (classrel, subsorts, arities) => 

256 
(classrel > fold add_rel rels, (map (pairself single) rels ~~ ths) @ subsorts, arities)))) 

257 
end; 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

258 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

259 
fun add_arity ths thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

260 
let 
19392  261 
val ars = ths > map (fn th => 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

262 
let 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

263 
val prop = Drule.plain_prop_of (Thm.transfer thy th); 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

264 
val (t, ss, c) = dest_arity prop handle TERM _ => 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

265 
raise THM ("AxClass.add_arity: not a type arity", 0, [th]); 
19392  266 
in (t, ss, [c]) end); 
267 
in 

268 
thy 

269 
> Theory.add_arities_i ars 

270 
> AxClassData.map (apsnd (map_instances (fn (classrel, subsorts, arities) => 

271 
(classrel, subsorts, (ars ~~ ths) @ arities)))) 

272 
end; 

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

273 

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

274 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

275 
(* tactical proofs *) 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

276 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

277 
fun prove_subclass raw_rel tac thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

278 
let 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

279 
val (c1, c2) = Sign.cert_classrel thy raw_rel; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

280 
val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

281 
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

282 
quote (Sign.string_of_classrel thy [c1, c2])); 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

283 
in add_classrel [th] thy end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

284 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

285 
fun prove_arity raw_arity tac thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

286 
let 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

287 
val arity = Sign.cert_arity thy raw_arity; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

288 
val props = mk_arities arity; 
17956  289 
val ths = Goal.prove_multi thy [] [] props 
18678  290 
(fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

291 
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

292 
quote (Sign.string_of_arity thy arity)); 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

293 
in add_arity ths thy end; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

294 

19392  295 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

296 
end; 