author  haftmann 
Mon, 23 Jan 2006 14:06:11 +0100  
changeset 18754  4e41252eae57 
parent 18728  6790126ab5f6 
child 18799  f137c5e971f5 
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} 
17339  13 
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

14 
theory > {intro: thm, axioms: thm list} * theory 
18728  15 
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

16 
theory > {intro: thm, axioms: thm list} * 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

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 

17339  23 
val instance_subclass: xstring * xstring > theory > Proof.state 
24 
val instance_subclass_i: class * class > theory > Proof.state 

18754  25 
val instance_arity: (theory > theory) > xstring * string list * string > theory > Proof.state 
26 
val instance_arity_i: (theory > theory) > string * sort list * sort > theory > Proof.state 

18574  27 
val read_arity: theory > xstring * string list * string > arity 
28 
val cert_arity: theory > string * sort list * sort > 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

29 
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

30 
val default_intro_classes_tac: thm list > tactic 
3938  31 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

32 

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

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

35 

4015  36 

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

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

38 

5685  39 
(* messages *) 
40 

41 
val quiet_mode = ref false; 

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

43 

44 

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

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

46 

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

47 
fun 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

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

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

50 

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

51 
val map_term_tfrees = map_term_types o map_typ_frees; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

52 

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

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

54 

3395  55 
fun dest_varT (TFree (x, S)) = ((x, ~1), S) 
56 
 dest_varT (TVar xi_S) = xi_S 

3788  57 
 dest_varT T = raise TYPE ("dest_varT", [T], []); 
3395  58 

404
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 

560  61 
(** abstract syntax operations **) 
423  62 

6379  63 
(* names *) 
64 

65 
val introN = "intro"; 

66 
val axiomsN = "axioms"; 

67 

68 

423  69 
(* subclass relations as terms *) 
70 

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

73 
fun dest_classrel tm = 

74 
let 

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

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

79 
handle TYPE _ => err (); 

6379  80 
in (c1, c2) end; 
423  81 

82 

83 
(* arities as terms *) 

84 

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

85 
fun mk_arity (t, Ss, c) = 
423  86 
let 
14695  87 
val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss); 
6379  88 
in Logic.mk_inclass (Type (t, tfrees), c) end; 
423  89 

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

90 
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

91 

423  92 
fun dest_arity tm = 
93 
let 

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

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

423  98 
(case ty of 
3395  99 
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) 
423  100 
 _ => err ()); 
101 
val ss = 

17496  102 
if null (gen_duplicates (eq_fst (op =)) tvars) 
3395  103 
then map snd tvars else err (); 
6379  104 
in (t, ss, c) end; 
423  105 

106 

107 

6379  108 
(** axclass info **) 
109 

110 
type axclass_info = 

111 
{super_classes: class list, 

112 
intro: thm, 

113 
axioms: thm list}; 

114 

16458  115 
structure AxclassesData = TheoryDataFun 
116 
(struct 

6379  117 
val name = "Pure/axclasses"; 
118 
type T = axclass_info Symtab.table; 

119 

120 
val empty = Symtab.empty; 

6546  121 
val copy = I; 
16458  122 
val extend = I; 
123 
fun merge _ = Symtab.merge (K true); 

6379  124 

16458  125 
fun print thy tab = 
6379  126 
let 
127 
fun pretty_class c cs = Pretty.block 

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

6379  130 

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

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

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

8720  136 
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end; 
16458  137 
end); 
6379  138 

18708  139 
val _ = Context.add_setup AxclassesData.init; 
6379  140 
val print_axclasses = AxclassesData.print; 
141 

142 

17412  143 
val lookup_info = Symtab.lookup o AxclassesData.get; 
6379  144 

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

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

146 
(case lookup_info thy c of 
15531  147 
NONE => error ("Unknown axclass " ^ quote c) 
148 
 SOME info => info); 

6379  149 

423  150 

16458  151 
fun class_axms thy = 
152 
let val classes = Sign.classes thy in 

153 
map (Thm.class_triv thy) classes @ 

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

154 
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

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

156 

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

157 

423  158 

159 
(** add axiomatic type classes **) 

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

160 

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

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

162 

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

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

164 
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

165 

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

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

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

168 

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

170 
let 
16458  171 
val class = Sign.full_name thy bclass; 
172 
val super_classes = map (prep_class thy) raw_super_classes; 

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

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

175 

6379  176 
(*declare class*) 
177 
val class_thy = 

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

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

179 

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

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

182 
if null (term_tfrees ax) then 
14854  183 
Logic.mk_implies (Logic.mk_inclass (aT [], class), ax) 
3788  184 
else map_term_tfrees (K (aT [class])) ax; 
17756  185 
val abs_axms = map (abs_axm o snd) axms; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

186 

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

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

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

189 
[] => [] 
16458  190 
 [(_, 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

191 
 _ => err_bad_tfrees name); 
16458  192 
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

193 

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

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

196 

1498  197 
val intro_axm = Logic.list_implies 
6379  198 
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); 
199 

200 
(*declare axioms and rule*) 

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

203 
> Theory.add_path (Sign.const_of_class bclass) 
6379  204 
> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] 
18377  205 
>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; 
6379  206 
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; 
207 

208 
(*store info*) 

18377  209 
val (_, final_thy) = 
6379  210 
axms_thy 
17703  211 
> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT > propT)] 
18377  212 
> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) 
213 
> Theory.restore_naming class_thy 

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

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

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

216 

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

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

218 

18728  219 
val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.attribute; 
6390  220 
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

221 

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

223 

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

224 

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

225 

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

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

227 

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

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

229 

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

230 
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

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

232 
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

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

234 
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

235 
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

236 
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

237 
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

238 
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

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

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

242 
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

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

244 
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

245 
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

246 
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

247 
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

248 
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

249 

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

250 

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

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

252 

16458  253 
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

254 

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

257 
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

258 

16458  259 
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

260 

16458  261 
fun prep_arity prep_tycon prep_sort prep thy (t, Ss, x) = 
262 
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

263 

16364  264 
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

265 
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

266 

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

267 

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

269 

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

270 
local 
423  271 

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

273 
let 
16458  274 
val (c1, c2) = prep_classrel thy raw_cc; 
275 
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

276 
val _ = message ("Proving class inclusion " ^ txt ^ " ..."); 
18678  277 
val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR msg => 
278 
cat_error msg ("The error(s) above occurred while trying to prove " ^ txt); 

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

280 

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

281 
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

282 
let 
16458  283 
val arity = prep_arity thy raw_arity; 
284 
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

285 
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

286 
val props = (mk_arities arity); 
17956  287 
val ths = Goal.prove_multi thy [] [] props 
18678  288 
(fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => 
289 
cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt); 

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

291 

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

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

293 

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

294 
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

295 
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

296 
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

297 
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

298 

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

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

300 

423  301 

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

303 

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

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

305 

18754  306 
fun gen_instance mk_prop add_thms after_qed inst thy = 
307 
thy 

17339  308 
> ProofContext.init 
18754  309 
> Proof.theorem_i Drule.internalK NONE (after_qed oo fold add_thms) NONE ("", []) 
310 
(map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); 

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

311 

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

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

313 

17339  314 
val instance_subclass = 
18754  315 
gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms I; 
17339  316 
val instance_subclass_i = 
18754  317 
gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms I; 
318 
val instance_arity = 

319 
gen_instance (mk_arities oo read_arity) add_arity_thms; 

320 
val instance_arity_i = 

321 
gen_instance (mk_arities oo cert_arity) add_arity_thms; 

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

322 

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

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

324 

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 
(* tactics and methods *) 
6379  327 

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

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

329 
(ALLGOALS (Method.insert_tac facts THEN' 
16458  330 
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

331 
THEN Tactic.distinct_subgoals_tac) st; 
6379  332 

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

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

334 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 
10309  335 

336 
fun default_tac rules ctxt facts = 

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

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

338 
default_intro_classes_tac facts; 
10309  339 

18708  340 
val _ = Context.add_setup (Method.add_methods 
15801  341 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 
18708  342 
"backchain introduction rules of axiomatic type classes"), 
343 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); 

10309  344 

345 

423  346 

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

347 
(** outer syntax **) 
6379  348 

17057  349 
local structure P = OuterParse and K = OuterKeyword in 
3949  350 

6379  351 
val axclassP = 
6719  352 
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

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

354 
P.!!! (P.list1 P.xname)) [])  Scan.repeat P.spec_name 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

355 
>> (Toplevel.theory o (snd oo uncurry add_axclass))); 
6379  356 

357 
val instanceP = 

6719  358 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 
17339  359 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> instance_subclass  
18754  360 
P.xname  (P.$$$ "::"  P.!!! P.arity) >> (instance_arity I o P.triple2)) 
17339  361 
>> (Toplevel.print oo Toplevel.theory_to_proof)); 
6379  362 

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

364 

365 
end; 

3949  366 

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

367 
end; 