author  wenzelm 
Tue, 06 Sep 2005 16:59:56 +0200  
changeset 17281  3b9ff0131ed1 
parent 17221  6cd180204582 
child 17339  ab97ccef124a 
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 

6379  5 
Axiomatic type class package. 
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 
5685  10 
val quiet_mode: bool ref 
6379  11 
val print_axclasses: theory > unit 
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

12 
val get_info: theory > string > {super_classes: class list, intro: thm, axioms: thm list} 
16333  13 
val add_axclass: bstring * xstring list > ((bstring * string) * Attrib.src list) list 
6379  14 
> theory > theory * {intro: thm, axioms: thm list} 
16333  15 
val add_axclass_i: bstring * class list > ((bstring * term) * theory attribute list) list 
6379  16 
> theory > theory * {intro: thm, axioms: thm list} 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

18 
val add_arity_thms: thm list > theory > theory 
16333  19 
val add_inst_subclass: xstring * xstring > tactic > theory > theory 
11828  20 
val add_inst_subclass_i: class * class > tactic > theory > theory 
21 
val add_inst_arity: xstring * string list * string > tactic > theory > theory 

22 
val add_inst_arity_i: string * sort list * sort > tactic > theory > theory 

17041  23 
val instance_subclass_proof: xstring * xstring > (theory > theory) 
24 
> bool > theory > ProofHistory.T 

25 
val instance_subclass_proof_i: class * class > (theory > theory) 

26 
> bool > theory > ProofHistory.T 

27 
val instance_arity_proof: xstring * string list * string > (theory > theory) 

28 
> bool > theory > ProofHistory.T 

29 
val instance_arity_proof_i: string * sort list * sort > (theory > theory) 

30 
> bool > theory > ProofHistory.T 

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

31 
val intro_classes_tac: thm list > tactic 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

32 
val default_intro_classes_tac: thm list > tactic 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

33 

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

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

35 
val axclass_tac: thm list > tactic 
16333  36 
val add_inst_subclass_x: xstring * xstring > string list > thm list 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

38 
val add_inst_arity_x: xstring * string list * string > string list 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

39 
> thm list > tactic option > theory > theory 
3938  40 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

41 

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

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

44 

4015  45 

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

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

47 

5685  48 
(* messages *) 
49 

50 
val quiet_mode = ref false; 

51 
fun message s = if ! quiet_mode then () else writeln s; 

52 

53 

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

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

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

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

63 

3395  64 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
65 
 dest_varT (TVar xi_S) = xi_S 

3788  66 
 dest_varT T = raise TYPE ("dest_varT", [T], []); 
3395  67 

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

68 

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

69 

560  70 
(** abstract syntax operations **) 
423  71 

6379  72 
(* names *) 
73 

74 
val introN = "intro"; 

75 
val axiomsN = "axioms"; 

76 

77 

423  78 
(* subclass relations as terms *) 
79 

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

82 
fun dest_classrel tm = 

83 
let 

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

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

88 
handle TYPE _ => err (); 

6379  89 
in (c1, c2) end; 
423  90 

91 

92 
(* arities as terms *) 

93 

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

94 
fun mk_arity (t, Ss, c) = 
423  95 
let 
14695  96 
val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss); 
6379  97 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  98 

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

99 
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

100 

423  101 
fun dest_arity tm = 
102 
let 

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

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

423  107 
(case ty of 
3395  108 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  109 
 _ => err ()); 
110 
val ss = 

3395  111 
if null (gen_duplicates eq_fst tvars) 
112 
then map snd tvars else err (); 

6379  113 
in (t, ss, c) end; 
423  114 

115 

116 

6379  117 
(** axclass info **) 
118 

119 
(* data kind 'Pure/axclasses' *) 

120 

121 
type axclass_info = 

122 
{super_classes: class list, 

123 
intro: thm, 

124 
axioms: thm list}; 

125 

16458  126 
structure AxclassesData = TheoryDataFun 
127 
(struct 

6379  128 
val name = "Pure/axclasses"; 
129 
type T = axclass_info Symtab.table; 

130 

131 
val empty = Symtab.empty; 

6546  132 
val copy = I; 
16458  133 
val extend = I; 
134 
fun merge _ = Symtab.merge (K true); 

6379  135 

16458  136 
fun print thy tab = 
6379  137 
let 
138 
fun pretty_class c cs = Pretty.block 

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

6379  141 

10008  142 
fun pretty_thms name thms = Pretty.big_list (name ^ ":") 
16458  143 
(map (Display.pretty_thm_sg thy) thms); 
6379  144 

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

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

8720  147 
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end; 
16458  148 
end); 
6379  149 

15801  150 
val _ = Context.add_setup [AxclassesData.init]; 
6379  151 
val print_axclasses = AxclassesData.print; 
152 

153 

154 
(* get and put data *) 

155 

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

156 
val lookup_info = Symtab.curried_lookup o AxclassesData.get; 
6379  157 

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

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

159 
(case lookup_info thy c of 
15531  160 
NONE => error ("Unknown axclass " ^ quote c) 
161 
 SOME info => info); 

6379  162 

423  163 

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

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

165 

16458  166 
fun class_axms thy = 
167 
let val classes = Sign.classes thy in 

168 
map (Thm.class_triv thy) classes @ 

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

169 
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

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

171 

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

172 

423  173 

174 
(** add axiomatic type classes **) 

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

175 

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

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

177 

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

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

179 
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

180 

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

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

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

183 

6379  184 
fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

185 
let 
16458  186 
val class = Sign.full_name thy bclass; 
187 
val super_classes = map (prep_class thy) raw_super_classes; 

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

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

190 

6379  191 
(*declare class*) 
192 
val class_thy = 

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

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

194 

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

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

197 
if null (term_tfrees ax) then 
14854  198 
Logic.mk_implies (Logic.mk_inclass (aT [], class), ax) 
3788  199 
else map_term_tfrees (K (aT [class])) ax; 
6379  200 
val abs_axms = map (abs_axm o #2) axms; 
404
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 
fun axm_sort (name, ax) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

204 
[] => [] 
16458  205 
 [(_, 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

206 
 _ => err_bad_tfrees name); 
16458  207 
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

208 

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

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

211 

1498  212 
val intro_axm = Logic.list_implies 
6379  213 
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); 
214 

215 
(*declare axioms and rule*) 

8420  216 
val (axms_thy, ([intro], [axioms])) = 
6379  217 
class_thy 
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

218 
> Theory.add_path (Sign.const_of_class bclass) 
6379  219 
> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] 
8420  220 
>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 
6379  221 
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; 
222 

223 
(*store info*) 

224 
val final_thy = 

225 
axms_thy 

8420  226 
> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) 
16180  227 
> Theory.restore_naming class_thy 
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

228 
> AxclassesData.map (Symtab.curried_update (class, info)); 
6379  229 
in (final_thy, {intro = intro, axioms = axioms}) end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

230 

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

232 

6390  233 
val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute; 
234 
val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I); 

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

235 

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

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

237 

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

238 

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

239 

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

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

241 

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

242 
(* add thms to type signature *) 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

243 

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

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

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

246 
fun prep_thm thm = 
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 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

248 
val prop = Drule.plain_prop_of (Thm.transfer thy thm); 
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 _ => 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

250 
raise THM ("add_classrel_thms: not a class relation", 0, [thm]); 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

252 
in Theory.add_classrel_i (map prep_thm thms) thy end; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

253 

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

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

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

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

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

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

259 
val (t, ss, c) = dest_arity prop handle TERM _ => 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

260 
raise THM ("add_arity_thms: not an arity", 0, [thm]); 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

261 
in (t, ss, [c]) end; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

262 
in Theory.add_arities_i (map prep_thm thms) thy end; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

263 

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

264 

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

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

266 

16458  267 
fun read_class thy c = Sign.certify_class thy (Sign.intern_class thy c); 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

268 

16458  269 
fun test_classrel thy cc = (Type.add_classrel (Sign.pp thy) [cc] (Sign.tsig_of thy); cc); 
270 
fun cert_classrel thy = test_classrel thy o Library.pairself (Sign.certify_class thy); 

271 
fun read_classrel thy = test_classrel thy o Library.pairself (read_class 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

272 

16458  273 
fun test_arity thy ar = (Type.add_arities (Sign.pp thy) [ar] (Sign.tsig_of thy); ar); 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

274 

16458  275 
fun prep_arity prep_tycon prep_sort prep thy (t, Ss, x) = 
276 
test_arity thy (prep_tycon thy t, map (prep_sort thy) Ss, prep thy x); 

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

277 

16364  278 
val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

279 
val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

280 

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

281 

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

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

283 

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

284 
local 
423  285 

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 
fun ext_inst_subclass prep_classrel raw_cc tac thy = 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

287 
let 
16458  288 
val (c1, c2) = prep_classrel thy raw_cc; 
289 
val txt = quote (Sign.string_of_classrel thy [c1, c2]); 

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

290 
val _ = message ("Proving class inclusion " ^ txt ^ " ..."); 
16458  291 
val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR => 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

292 
error ("The error(s) above occurred while trying to prove " ^ txt); 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

294 

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

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

296 
let 
16458  297 
val arity = prep_arity thy raw_arity; 
298 
val txt = quote (Sign.string_of_arity thy arity); 

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

299 
val _ = message ("Proving type arity " ^ txt ^ " ..."); 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

300 
val props = (mk_arities arity); 
16458  301 
val ths = Tactic.prove_multi thy [] [] props 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

302 
(fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

303 
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt); 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

305 

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

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

307 

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

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

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

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

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

312 

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

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

314 

423  315 

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

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

317 

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

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

319 

17041  320 
fun inst_proof mk_prop add_thms inst after_qed int theory = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

321 
theory 
17041  322 
> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

323 
("", [fn (thy, th) => (add_thms [th] thy, th)]) [] 
16458  324 
(map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

325 

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

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

327 

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

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

329 
inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

331 
inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

332 
val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

333 
val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

334 

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

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

336 

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

337 

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

338 
(* tactics and methods *) 
6379  339 

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

340 
fun intro_classes_tac facts st = 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

341 
(ALLGOALS (Method.insert_tac facts THEN' 
16458  342 
REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.theory_of_thm st)))) 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

343 
THEN Tactic.distinct_subgoals_tac) st; 
6379  344 

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

345 
fun default_intro_classes_tac [] = intro_classes_tac [] 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

346 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 
10309  347 

348 
fun default_tac rules ctxt facts = 

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

349 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
12876
diff
changeset

350 
default_intro_classes_tac facts; 
10309  351 

15801  352 
val _ = Context.add_setup [Method.add_methods 
353 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

354 
"backchain introduction rules of axiomatic type classes"), 

355 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]]; 

10309  356 

357 

423  358 

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

359 
(** outer syntax **) 
6379  360 

17057  361 
local structure P = OuterParse and K = OuterKeyword in 
3949  362 

6379  363 
val axclassP = 
6719  364 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

365 
((P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

366 
P.!!! (P.list1 P.xname)) [])  Scan.repeat P.spec_name 
6379  367 
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); 
368 

369 
val instanceP = 

6719  370 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

371 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.xname) 
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

372 
>> (fn i => instance_subclass_proof i I)  
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

373 
(P.xname  (P.$$$ "::"  P.arity) >> P.triple2) 
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

374 
>> (fn i => instance_arity_proof i I)) 
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset

375 
>> (Toplevel.print oo Toplevel.theory_to_proof)); 
6379  376 

377 
val _ = OuterSyntax.add_parsers [axclassP, instanceP]; 

378 

379 
end; 

3949  380 

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

381 

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

382 

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

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

384 

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

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

386 

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

387 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

388 
try class_trivs first, then "cI" axioms 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

389 
(2) rewrite goals using user supplied definitions 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

390 
(3) repeatedly resolve goals with user supplied nondefinitions*) 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

391 

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

392 
val is_def = Logic.is_equals o #prop o rep_thm; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

393 

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

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

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

396 
val defs = List.filter is_def thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

397 
val non_defs = filter_out is_def thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

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

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

401 
TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

403 

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

404 

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

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

406 

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

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

408 

16458  409 
fun prove mk_prop str_of thy prop thms usr_tac = 
410 
(Tactic.prove thy [] [] (mk_prop prop) 

15973  411 
(K (axclass_tac thms THEN (if_none usr_tac all_tac))) 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

412 
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ 
16458  413 
quote (str_of thy prop))) > Drule.standard; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

414 

16458  415 
val prove_subclass = prove mk_classrel (fn thy => fn (c1, c2) => 
416 
Pretty.string_of_classrel (Sign.pp thy) [c1, c2]); 

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

417 

16458  418 
val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) => 
419 
Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c])); 

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

420 

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

421 
fun witnesses thy names thms = 
16486  422 
PureThy.get_thmss thy (map Name names) @ 
16458  423 
thms @ 
424 
List.filter is_def (map snd (axioms_of 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

425 

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

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

427 

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

428 
fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy = 
16458  429 
let val (c1, c2) = read_classrel thy raw_c1_c2 in 
430 
message ("Proving class inclusion " ^ quote (Sign.string_of_classrel thy [c1, c2]) ^ " ..."); 

431 
thy > add_classrel_thms [prove_subclass thy (c1, c2) (witnesses thy names thms) usr_tac] 

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

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

433 

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

434 
fun add_inst_arity_x raw_arity names thms usr_tac thy = 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

435 
let 
16458  436 
val (t, Ss, cs) = read_arity thy raw_arity; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

437 
val wthms = witnesses thy names thms; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

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

439 
(message ("Proving type arity " ^ 
16458  440 
quote (Sign.string_of_arity thy (t, Ss, [c])) ^ " ..."); 
441 
prove_arity thy (t, Ss, c) wthms usr_tac); 

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

442 
in add_arity_thms (map prove cs) thy end; 
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

443 

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

444 
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

445 

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

446 
end; 