author  wenzelm 
Sat, 11 Mar 2006 16:53:20 +0100  
changeset 19243  5dcb899a8486 
parent 19134  47d337aefc21 
child 19392  a631cd2117a8 
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 
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

16 
val get_info: theory > string > {super_classes: class list, intro: thm, axioms: thm list} 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

17 
val class_intros: theory > thm list 
17339  18 
val add_axclass: bstring * xstring list > ((bstring * string) * Attrib.src list) list > 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

19 
theory > {intro: thm, axioms: thm list} * theory 
18728  20 
val add_axclass_i: bstring * class list > ((bstring * term) * attribute list) list > 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

21 
theory > {intro: thm, axioms: thm list} * theory 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

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

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

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

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

27 

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

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

30 

4015  31 

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

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

33 

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

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

35 

3395  36 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

37 
 dest_varT (TVar a) = a 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

38 
 dest_varT T = raise TYPE ("AxClass.dest_varT", [T], []); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

39 

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

40 

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

41 
(* subclass propositions *) 
423  42 

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

45 
fun dest_classrel tm = 

46 
let 

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

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

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

51 
handle TYPE _ => err (); 

6379  52 
in (c1, c2) end; 
423  53 

54 

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

55 
(* arity propositions *) 
423  56 

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

57 
fun mk_arity (t, Ss, c) = 
423  58 
let 
14695  59 
val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss); 
6379  60 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  61 

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

62 
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

63 

423  64 
fun dest_arity tm = 
65 
let 

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

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

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

423  70 
(case ty of 
3395  71 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  72 
 _ => err ()); 
73 
val ss = 

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

74 
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

75 
else map snd tvars; 
6379  76 
in (t, ss, c) end; 
423  77 

78 

79 

6379  80 
(** axclass info **) 
81 

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

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

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

84 

6379  85 
type axclass_info = 
86 
{super_classes: class list, 

87 
intro: thm, 

88 
axioms: thm list}; 

89 

16458  90 
structure AxclassesData = TheoryDataFun 
91 
(struct 

6379  92 
val name = "Pure/axclasses"; 
93 
type T = axclass_info Symtab.table; 

94 

95 
val empty = Symtab.empty; 

6546  96 
val copy = I; 
16458  97 
val extend = I; 
98 
fun merge _ = Symtab.merge (K true); 

6379  99 

16458  100 
fun print thy tab = 
6379  101 
let 
102 
fun pretty_class c cs = Pretty.block 

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

6379  105 

10008  106 
fun pretty_thms name thms = Pretty.big_list (name ^ ":") 
16458  107 
(map (Display.pretty_thm_sg thy) thms); 
6379  108 

109 
fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks 

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

8720  111 
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end; 
16458  112 
end); 
6379  113 

18708  114 
val _ = Context.add_setup AxclassesData.init; 
6379  115 
val print_axclasses = AxclassesData.print; 
116 

117 

17412  118 
val lookup_info = Symtab.lookup o AxclassesData.get; 
6379  119 

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

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

121 
(case lookup_info thy c of 
15531  122 
NONE => error ("Unknown axclass " ^ quote c) 
123 
 SOME info => info); 

6379  124 

19123  125 
fun class_intros thy = 
16458  126 
let val classes = Sign.classes thy in 
127 
map (Thm.class_triv thy) classes @ 

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

128 
List.mapPartial (Option.map #intro o lookup_info thy) classes 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

130 

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

131 

423  132 

133 
(** add axiomatic type classes **) 

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

134 

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

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

136 

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

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

138 
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

139 

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

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

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

142 

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

143 
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

144 

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

145 
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

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

147 
let 
16458  148 
val class = Sign.full_name thy bclass; 
149 
val super_classes = map (prep_class thy) raw_super_classes; 

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

6379  151 
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

152 

6379  153 
(*declare class*) 
154 
val class_thy = 

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

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

156 

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

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

159 
if null (term_tfrees ax) then 
14854  160 
Logic.mk_implies (Logic.mk_inclass (aT [], class), ax) 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

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

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

166 
[] => [] 
16458  167 
 [(_, 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

168 
 _ => err_bad_tfrees name); 
16458  169 
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

170 

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

171 
val int_axm = Logic.close_form o replace_tfree (aT axS); 
1498  172 
fun inclass c = Logic.mk_inclass (aT axS, c); 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

173 

1498  174 
val intro_axm = Logic.list_implies 
6379  175 
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); 
176 

177 
(*declare axioms and rule*) 

18377  178 
val (([intro], [axioms]), axms_thy) = 
6379  179 
class_thy 
18932  180 
> Theory.add_path (Logic.const_of_class bclass) 
6379  181 
> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] 
18377  182 
>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 
6379  183 
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; 
184 

185 
(*store info*) 

18377  186 
val (_, final_thy) = 
6379  187 
axms_thy 
18932  188 
> Theory.add_finals_i false [Const (Logic.const_of_class class, a_itselfT > propT)] 
18377  189 
> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) 
190 
> Theory.restore_naming class_thy 

191 
> AxclassesData.map (Symtab.update (class, info)); 

18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

192 
in ({intro = intro, axioms = axioms}, final_thy) end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

193 

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

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

195 

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

196 
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

197 
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

198 

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

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

200 

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

201 

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

202 

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

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

204 

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

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

206 

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

207 
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

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

209 
fun prep_thm 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

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

211 
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

212 
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

213 
raise THM ("AxClass.add_classrel: not a class relation", 0, [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

214 
in (c1, c2) end; 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

215 
in Theory.add_classrel_i (map prep_thm 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

216 

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

217 
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

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

219 
fun prep_thm 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

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

221 
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

222 
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

223 
raise THM ("AxClass.add_arity: not a type arity", 0, [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

224 
in (t, ss, [c]) end; 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

225 
in Theory.add_arities_i (map prep_thm ths) thy end; 
404
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 

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

228 
(* 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

229 

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

230 
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

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

232 
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

233 
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

234 
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

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

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

237 

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

238 
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

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

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

241 
val props = mk_arities arity; 
17956  242 
val ths = Goal.prove_multi thy [] [] props 
18678  243 
(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

244 
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

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

246 
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

247 

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

248 
end; 