author  wenzelm 
Sun, 25 Apr 2010 19:09:37 +0200  
changeset 36325  8715343af626 
parent 36106  19deea200358 
child 36326  85d026788fce 
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 
Author: Markus Wenzel, TU Muenchen 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

3 

24964  4 
Type classes defined as predicates, associated with a record of 
5 
parameters. 

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 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

10 
val define_class: binding * class list > string list > 
30211  11 
(Thm.binding * term list) list > theory > class * theory 
24589  12 
val add_classrel: thm > theory > theory 
13 
val add_arity: thm > theory > theory 

14 
val prove_classrel: class * class > tactic > theory > theory 

15 
val prove_arity: string * sort list * sort > tactic > theory > theory 

24964  16 
val get_info: theory > class > 
17 
{def: thm, intro: thm, axioms: thm list, params: (string * typ) list} 

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

18 
val class_intros: theory > thm list 
20107  19 
val class_of_param: theory > string > class option 
19405  20 
val cert_classrel: theory > class * class > class * class 
21 
val read_classrel: theory > xstring * xstring > class * class 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

22 
val axiomatize_class: binding * class list > theory > theory 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

23 
val axiomatize_class_cmd: binding * xstring list > theory > theory 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

24 
val axiomatize_classrel: (class * class) list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

25 
val axiomatize_classrel_cmd: (xstring * xstring) list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

26 
val axiomatize_arity: arity > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

27 
val axiomatize_arity_cmd: xstring * string list * string > theory > theory 
25486  28 
val instance_name: string * class > string 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

29 
val declare_overloaded: string * typ > theory > term * theory 
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30469
diff
changeset

30 
val define_overloaded: binding > string * term > theory > thm * theory 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

31 
val unoverload: theory > thm > thm 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

32 
val overload: theory > thm > thm 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

33 
val unoverload_conv: theory > conv 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

34 
val overload_conv: theory > conv 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

35 
val unoverload_const: theory > string * typ > string 
31249  36 
val lookup_inst_param: Consts.T > ((string * string) * 'a) list > string * typ > 'a option 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

37 
val param_of_inst: theory > string * string > string 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

38 
val inst_of_param: theory > string > (string * string) option 
33172  39 
val thynames_of_arity: theory > class * string > string list 
26246  40 
val introN: string 
25617  41 
val axiomsN: string 
3938  42 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

43 

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

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

46 

19405  47 
(** theory data **) 
423  48 

19405  49 
(* class parameters (canonical order) *) 
423  50 

19405  51 
type param = string * class; 
423  52 

19405  53 
fun add_param pp ((x, c): param) params = 
54 
(case AList.lookup (op =) params x of 

55 
NONE => (x, c) :: params 

56 
 SOME c' => error ("Duplicate class parameter " ^ quote x ^ 

57 
" for " ^ Pretty.string_of_sort pp [c] ^ 

58 
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c']))); 

423  59 

19405  60 
fun merge_params _ ([], qs) = qs 
61 
 merge_params pp (ps, qs) = 

62 
fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; 

423  63 

64 

19511  65 
(* axclasses *) 
6379  66 

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

67 
val introN = "intro"; 
19511  68 
val superN = "super"; 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

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

70 

19392  71 
datatype axclass = AxClass of 
19460  72 
{def: thm, 
19392  73 
intro: thm, 
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
20628
diff
changeset

74 
axioms: thm list, 
21925  75 
params: (string * typ) list}; 
19392  76 

19460  77 
type axclasses = axclass Symtab.table * param list; 
19392  78 

27397  79 
fun make_axclass ((def, intro, axioms), params) = AxClass 
80 
{def = def, intro = intro, axioms = axioms, params = params}; 

19405  81 

82 
fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses = 

83 
(Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2)); 

84 

19392  85 

86 
(* instances *) 

87 

20628  88 
val classrel_prefix = "classrel_"; 
89 
val arity_prefix = "arity_"; 

19511  90 

19574  91 
type instances = 
36325  92 
(thm * proof) Symreltab.table * (*classrel theorems*) 
93 
((class * sort list) * ((thm * string) * proof)) list Symtab.table; (*arity theorems with theory name*) 

6379  94 

36325  95 
(*transitive closure of classrels and arity completion is done in Theory.at_begin hook*) 
19574  96 
fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) = 
36325  97 
(Symreltab.join (K fst) (classrel1, classrel2), 
19574  98 
Symtab.join (K (merge (eq_fst op =))) (arities1, arities2)); 
19392  99 

100 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

101 
(* instance parameters *) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

102 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

103 
type inst_params = 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

104 
(string * thm) Symtab.table Symtab.table 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

105 
(*constant name ~> type constructor ~> (constant name, equation)*) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

106 
* (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

107 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

108 
fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) = 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

109 
(Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2), 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

110 
Symtab.merge (K true) (param_const1, param_const2)); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

111 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

112 

19511  113 
(* setup data *) 
19392  114 

34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34245
diff
changeset

115 
structure AxClassData = Theory_Data_PP 
22846  116 
( 
36325  117 
type T = axclasses * ((instances * inst_params) * (class * class) list); 
118 
val empty = ((Symtab.empty, []), (((Symreltab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), [])); 

19574  119 
val extend = I; 
36325  120 
fun merge pp ((axclasses1, ((instances1, inst_params1), diff_merge_classrels1)), 
121 
(axclasses2, ((instances2, inst_params2), diff_merge_classrels2))) = 

122 
let 

123 
val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2) 

124 
val diff_merge_classrels = subtract (op =) classrels1 classrels2 

125 
@ subtract (op =) classrels2 classrels1 

126 
@ diff_merge_classrels1 @ diff_merge_classrels2 

127 
in 

128 
(merge_axclasses pp (axclasses1, axclasses2), 

129 
((merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)), 

130 
diff_merge_classrels)) 

131 
end; 

22846  132 
); 
6379  133 

134 

19574  135 
(* maintain axclasses *) 
19392  136 

19574  137 
val get_axclasses = #1 o AxClassData.get; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

138 
val map_axclasses = AxClassData.map o apfst; 
19574  139 

140 
val lookup_def = Symtab.lookup o #1 o get_axclasses; 

6379  141 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

142 
fun get_info thy c = 
19511  143 
(case lookup_def thy c of 
19392  144 
SOME (AxClass info) => info 
21919  145 
 NONE => error ("No such axclass: " ^ quote c)); 
6379  146 

19123  147 
fun class_intros thy = 
19392  148 
let 
149 
fun add_intro c = 

19511  150 
(case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro  _ => I); 
21931
314f9e2a442c
replaced Sign.classes by Sign.all_classes (topologically sorted);
wenzelm
parents:
21925
diff
changeset

151 
val classes = Sign.all_classes thy; 
19392  152 
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

153 

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

154 

19460  155 
fun get_params thy pred = 
19574  156 
let val params = #2 (get_axclasses thy); 
19460  157 
in fold (fn (x, c) => if pred c then cons x else I) params [] end; 
158 

159 
fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); 

160 

24964  161 
fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy)); 
19460  162 

21919  163 

19511  164 
(* maintain instances *) 
19503  165 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

166 
fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a; 
25486  167 

36325  168 
val get_instances = #1 o #1 o #2 o AxClassData.get; 
169 
val map_instances = AxClassData.map o apsnd o apfst o apfst; 

170 

171 
val get_diff_merge_classrels = #2 o #2 o AxClassData.get; 

172 
val clear_diff_merge_classrels = AxClassData.map (apsnd (apsnd (K []))); 

19528  173 

174 

19574  175 
fun the_classrel thy (c1, c2) = 
36325  176 
(case Symreltab.lookup (#1 (get_instances thy)) (c1, c2) of 
177 
SOME classrel => classrel 

24920  178 
 NONE => error ("Unproven class relation " ^ 
179 
Syntax.string_of_classrel (ProofContext.init thy) [c1, c2])); 

19574  180 

36325  181 
fun the_classrel_thm thy = Thm.transfer thy o fst o the_classrel thy; 
182 
fun the_classrel_prf thy = snd o the_classrel thy; 

183 

184 
fun put_trancl_classrel ((c1, c2), th) thy = 

185 
let 

186 
val classrels = fst (get_instances thy) 

187 
val alg = Sign.classes_of thy 

188 
val {classes, ...} = alg > Sorts.rep_algebra 

189 

190 
fun reflcl_classrel (c1', c2') = 

191 
if c1' = c2' then Thm.trivial (Logic.mk_of_class (TVar(("'a",0),[]), c1') > cterm_of thy) 

192 
else the_classrel_thm thy (c1', c2') 

193 
fun gen_classrel (c1_pred, c2_succ) = 

194 
let 

195 
val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ)) 

196 
> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [] 

197 
> Thm.close_derivation 

198 
val prf' = th' > Thm.proof_of 

199 
in ((c1_pred, c2_succ), (th',prf')) end 

200 

201 
val new_classrels = Library.map_product pair 

202 
(c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2) 

203 
> filter_out (Symreltab.defined classrels) 

204 
> map gen_classrel 

205 
val needed = length new_classrels > 0 

206 
in 

207 
(needed, 

208 
if needed then 

209 
thy > map_instances (fn (classrels, arities) => 

210 
(classrels > fold Symreltab.update new_classrels, arities)) 

211 
else thy) 

212 
end; 

213 

214 
fun complete_classrels thy = 

215 
let 

216 
val diff_merge_classrels = get_diff_merge_classrels thy 

217 
val classrels = fst (get_instances thy) 

218 
val (needed, thy') = (false, thy) > 

219 
fold (fn c12 => fn (needed, thy) => 

220 
put_trancl_classrel (c12, Symreltab.lookup classrels c12 > the > fst) thy 

221 
>> (fn b => needed orelse b)) 

222 
diff_merge_classrels 

223 
in 

224 
if null diff_merge_classrels then NONE 

225 
else thy' > clear_diff_merge_classrels > SOME 

226 
end; 

19503  227 

228 

19574  229 
fun the_arity thy a (c, Ss) = 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

230 
(case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of 
36325  231 
SOME arity => arity 
24920  232 
 NONE => error ("Unproven type arity " ^ 
233 
Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c]))); 

19503  234 

36325  235 
fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss > fst > fst > Thm.transfer thy; 
236 
fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss > snd; 

237 

33172  238 
fun thynames_of_arity thy (c, a) = 
239 
Symtab.lookup_list (#2 (get_instances thy)) a 

36325  240 
> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE) 
27497  241 
> rev; 
27397  242 

36325  243 
fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities = 
27547  244 
let 
245 
val algebra = Sign.classes_of thy; 

33172  246 
val super_class_completions = 
247 
Sign.super_classes thy c 

27547  248 
> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2 
33172  249 
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t)); 
36325  250 
val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss); 
251 
val completions = super_class_completions > map (fn c1 => 

252 
let 

253 
val th1 = (th RS the_classrel_thm thy (c, c1)) 

254 
> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) [] 

255 
> Thm.close_derivation 

256 
val prf1 = Thm.proof_of th1 

257 
in (((th1,thy_name), prf1), c1) end) 

258 
val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1))) 

27547  259 
completions arities; 
33172  260 
in (null completions, arities') end; 
19503  261 

27547  262 
fun put_arity ((t, Ss, c), th) thy = 
263 
let 

36325  264 
val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th))); 
27547  265 
in 
266 
thy 

267 
> map_instances (fn (classrel, arities) => (classrel, 

268 
arities 

269 
> Symtab.insert_list (eq_fst op =) arity' 

270 
> insert_arity_completions thy arity' 

271 
> snd)) 

272 
end; 

19503  273 

31944  274 
fun complete_arities thy = 
27547  275 
let 
276 
val arities = snd (get_instances thy); 

33172  277 
val (finished, arities') = arities 
278 
> fold_map (insert_arity_completions thy) (Symtab.dest_list arities); 

279 
in 

280 
if forall I finished then NONE 

27547  281 
else SOME (thy > map_instances (fn (classrel, _) => (classrel, arities'))) 
282 
end; 

283 

36325  284 
val _ = Context.>> (Context.map_theory 
285 
(Theory.at_begin complete_classrels #> Theory.at_begin complete_arities)) 

27397  286 

287 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

288 
(* maintain instance parameters *) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

289 

36325  290 
val get_inst_params = #2 o #1 o #2 o AxClassData.get; 
291 
val map_inst_params = AxClassData.map o apsnd o apfst o apsnd; 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

292 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

293 
fun get_inst_param thy (c, tyco) = 
30243
09d5944e224e
explicit error message for `improper` instances lacking explicit instance parameter constants
haftmann
parents:
29579
diff
changeset

294 
case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco 
09d5944e224e
explicit error message for `improper` instances lacking explicit instance parameter constants
haftmann
parents:
29579
diff
changeset

295 
of SOME c' => c' 
09d5944e224e
explicit error message for `improper` instances lacking explicit instance parameter constants
haftmann
parents:
29579
diff
changeset

296 
 NONE => error ("No instance parameter for constant " ^ quote c 
09d5944e224e
explicit error message for `improper` instances lacking explicit instance parameter constants
haftmann
parents:
29579
diff
changeset

297 
^ " on type constructor " ^ quote tyco); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

298 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

299 
fun add_inst_param (c, tyco) inst = (map_inst_params o apfst 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

300 
o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

301 
#> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco))); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

302 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

303 
val inst_of_param = Symtab.lookup o snd o get_inst_params; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

304 
val param_of_inst = fst oo get_inst_param; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

305 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

306 
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

307 
(get_inst_params thy) []; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

308 

31249  309 
fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

310 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

311 
fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

312 
fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy)); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

313 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

314 
fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

315 
fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

316 

31249  317 
fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T) 
318 
of SOME tyco => AList.lookup (op =) params (c, tyco) 

319 
 NONE => NONE; 

320 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

321 
fun unoverload_const thy (c_ty as (c, _)) = 
33969  322 
if is_some (class_of_param thy c) 
323 
then case get_inst_tyco (Sign.consts_of thy) c_ty 

324 
of SOME tyco => try (param_of_inst thy) (c, tyco) > the_default c 

325 
 NONE => c 

326 
else c; 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

327 

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

328 

19511  329 
(** instances **) 
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

330 

03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

331 
(* class relations *) 
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

332 

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

334 
let 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26516
diff
changeset

335 
val string_of_sort = Syntax.string_of_sort_global thy; 
19405  336 
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; 
24271  337 
val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy); 
19405  338 
val _ = 
19460  339 
(case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of 
19405  340 
[] => () 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26516
diff
changeset

341 
 xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26516
diff
changeset

342 
commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); 
19405  343 
in (c1, c2) end; 
344 

345 
fun read_classrel thy raw_rel = 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

346 
cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel) 
19405  347 
handle TYPE (msg, _, _) => error msg; 
348 

36325  349 
fun check_shyps_topped th errmsg = 
350 
let val {shyps, ...} = Thm.rep_thm th 

351 
in 

352 
forall null shyps orelse raise Fail errmsg 

353 
end; 

19405  354 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

355 
(* declaration and definition of instances of overloaded constants *) 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

356 

35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

357 
fun inst_tyco_of thy (c, T) = 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

358 
(case get_inst_tyco (Sign.consts_of thy) (c, T) of 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

359 
SOME tyco => tyco 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

360 
 NONE => error ("Illegal type for instantiation of class parameter: " ^ 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

361 
quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); 
31249  362 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

363 
fun declare_overloaded (c, T) thy = 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

364 
let 
35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

365 
val class = 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

366 
(case class_of_param thy c of 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

367 
SOME class => class 
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

368 
 NONE => error ("Not a class parameter: " ^ quote c)); 
31249  369 
val tyco = inst_tyco_of thy (c, T); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

370 
val name_inst = instance_name (tyco, class) ^ "_inst"; 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

371 
val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

372 
val T' = Type.strip_sorts T; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

373 
in 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

374 
thy 
35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

375 
> Sign.qualified_path true (Binding.name name_inst) 
33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33172
diff
changeset

376 
> Sign.declare_const ((Binding.name c', T'), NoSyn) 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

377 
> (fn const' as Const (c'', _) => 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

378 
Thm.add_def false true 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

379 
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

380 
#>> apsnd Thm.varifyT_global 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

381 
#> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm) 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

382 
#> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

383 
#> snd 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

384 
#> pair (Const (c, T)))) 
35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

385 
> Sign.restore_naming thy 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

386 
end; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

387 

30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30469
diff
changeset

388 
fun define_overloaded b (c, t) thy = 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

389 
let 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

390 
val T = Term.fastype_of t; 
31249  391 
val tyco = inst_tyco_of thy (c, T); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

392 
val (c', eq) = get_inst_param thy (c, tyco); 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

393 
val prop = Logic.mk_equals (Const (c', T), t); 
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30469
diff
changeset

394 
val b' = Thm.def_binding_optional 
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30469
diff
changeset

395 
(Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

396 
in 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

397 
thy 
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30469
diff
changeset

398 
> Thm.add_def false false (b', prop) 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

399 
>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm]) 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

400 
end; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

401 

34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

402 

30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

403 
(* primitive rules *) 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

404 

31948
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

405 
fun add_classrel raw_th thy = 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

406 
let 
31948
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

407 
val th = Thm.strip_shyps (Thm.transfer thy raw_th); 
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

408 
val prop = Thm.plain_prop_of th; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

409 
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

410 
val rel = Logic.dest_classrel prop handle TERM _ => err (); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

411 
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); 
36325  412 
val th' = th 
413 
> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] [] 

414 
> Drule.unconstrainTs; 

415 
val _ = check_shyps_topped th' "add_classrel: nontop shyps after unconstrain" 

30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

416 
in 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

417 
thy 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

418 
> Sign.primitive_classrel (c1, c2) 
36325  419 
> (snd oo put_trancl_classrel) ((c1, c2), th') 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

420 
> perhaps complete_arities 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

421 
end; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

422 

31948
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

423 
fun add_arity raw_th thy = 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

424 
let 
31948
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

425 
val th = Thm.strip_shyps (Thm.transfer thy raw_th); 
ea8c8bf47ce3
add_classrel/arity: strip_shyps of stored result;
wenzelm
parents:
31944
diff
changeset

426 
val prop = Thm.plain_prop_of th; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

427 
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

428 
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); 
36325  429 
val names = Name.names Name.context Name.aT Ss; 
430 
val T = Type (t, map TFree names); 

30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

431 
val missing_params = Sign.complete_sort thy [c] 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

432 
> maps (these o Option.map #params o try (get_info thy)) 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

433 
> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

434 
> (map o apsnd o map_atyps) (K T); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

435 
val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); 
36325  436 
val th' = th 
437 
> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) [] 

438 
> Drule.unconstrainTs; 

439 
val _ = check_shyps_topped th' "add_arity: nontop shyps after unconstrain" 

30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

440 
in 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

441 
thy 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

442 
> fold (snd oo declare_overloaded) missing_params 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

443 
> Sign.primitive_arity (t, Ss, [c]) 
36325  444 
> put_arity ((t, Ss, c), th') 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

445 
end; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

446 

a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

447 

a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

448 
(* tactical proofs *) 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

449 

a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

450 
fun prove_classrel raw_rel tac thy = 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

451 
let 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

452 
val ctxt = ProofContext.init thy; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

453 
val (c1, c2) = cert_classrel thy raw_rel; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

454 
val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

455 
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

456 
quote (Syntax.string_of_classrel ctxt [c1, c2])); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

457 
in 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

458 
thy 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

459 
> PureThy.add_thms [((Binding.name 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

460 
(prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

461 
> (fn [th'] => add_classrel th') 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

462 
end; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

463 

a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

464 
fun prove_arity raw_arity tac thy = 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

465 
let 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

466 
val ctxt = ProofContext.init thy; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

467 
val arity = ProofContext.cert_arity ctxt raw_arity; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

468 
val names = map (prefix arity_prefix) (Logic.name_arities arity); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

469 
val props = Logic.mk_arities arity; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

470 
val ths = Goal.prove_multi ctxt [] [] props 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

471 
(fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

472 
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

473 
quote (Syntax.string_of_arity ctxt arity)); 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

474 
in 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

475 
thy 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

476 
> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

477 
> fold add_arity 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

478 
end; 
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

479 

a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

480 

19511  481 

482 
(** class definitions **) 

483 

23421  484 
fun split_defined n eq = 
485 
let 

486 
val intro = 

487 
(eq RS Drule.equal_elim_rule2) 

488 
> Conjunction.curry_balanced n 

489 
> n = 0 ? Thm.eq_assumption 1; 

490 
val dests = 

491 
if n = 0 then [] 

492 
else 

493 
(eq RS Drule.equal_elim_rule1) 

32765  494 
> Balanced_Tree.dest (fn th => 
23421  495 
(th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; 
496 
in (intro, dests) end; 

497 

24964  498 
fun define_class (bclass, raw_super) raw_params raw_specs thy = 
19511  499 
let 
500 
val ctxt = ProofContext.init thy; 

24964  501 
val pp = Syntax.pp ctxt; 
19511  502 

503 

24964  504 
(* class *) 
19511  505 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

506 
val bconst = Binding.map_name Logic.const_of_class bclass; 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

507 
val class = Sign.full_name thy bclass; 
24731  508 
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); 
19511  509 

24964  510 
fun check_constraint (a, S) = 
511 
if Sign.subsort thy (super, S) then () 

512 
else error ("Sort constraint of type variable " ^ 

32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32791
diff
changeset

513 
setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ 
24964  514 
" needs to be weaker than " ^ Pretty.string_of_sort pp super); 
515 

516 

517 
(* params *) 

518 

519 
val params = raw_params > map (fn p => 

520 
let 

521 
val T = Sign.the_const_type thy p; 

522 
val _ = 

523 
(case Term.add_tvarsT T [] of 

524 
[((a, _), S)] => check_constraint (a, S) 

525 
 _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); 

526 
val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T; 

527 
in (p, T') end); 

528 

529 

530 
(* axioms *) 

531 

19511  532 
fun prep_axiom t = 
533 
(case Term.add_tfrees t [] of 

24964  534 
[(a, S)] => check_constraint (a, S) 
535 
 [] => () 

536 
 _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t); 

537 
t 

538 
> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT []  U => U)) 

539 
> Logic.close_form); 

19511  540 

24681  541 
val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; 
22745  542 
val name_atts = map fst raw_specs; 
19511  543 

544 

545 
(* definition *) 

546 

35854  547 
val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss; 
19511  548 
val class_eq = 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31904
diff
changeset

549 
Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs); 
19511  550 

551 
val ([def], def_thy) = 

552 
thy 

553 
> Sign.primitive_class (bclass, super) 

35238  554 
> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])]; 
19511  555 
val (raw_intro, (raw_classrel, raw_axioms)) = 
23421  556 
split_defined (length conjs) def > chop (length super); 
19392  557 

19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

558 

19511  559 
(* facts *) 
560 

561 
val class_triv = Thm.class_triv def_thy class; 

562 
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = 

563 
def_thy 

35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

564 
> Sign.qualified_path true bconst 
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27683
diff
changeset

565 
> PureThy.note_thmss "" 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34259
diff
changeset

566 
[((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]), 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34259
diff
changeset

567 
((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]), 
28965  568 
((Binding.name axiomsN, []), 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34259
diff
changeset

569 
[(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])] 
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27683
diff
changeset

570 
> Sign.restore_naming def_thy; 
19511  571 

24847  572 

19511  573 
(* result *) 
574 

24964  575 
val axclass = make_axclass ((def, intro, axioms), params); 
19511  576 
val result_thy = 
577 
facts_thy 

36325  578 
> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel) 
35201
c2ddb9395436
axclass: more precise treatment of naming vs. binding;
wenzelm
parents:
35021
diff
changeset

579 
> Sign.qualified_path false bconst 
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27683
diff
changeset

580 
> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) > snd 
19511  581 
> Sign.restore_naming facts_thy 
19574  582 
> map_axclasses (fn (axclasses, parameters) => 
21919  583 
(Symtab.update (class, axclass) axclasses, 
24964  584 
fold (fn (x, _) => add_param pp (x, class)) params parameters)); 
19511  585 

586 
in (class, result_thy) end; 

587 

588 

19531  589 

19511  590 
(** axiomatizations **) 
591 

592 
local 

593 

35896
487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

594 
(* oldstyle axioms *) 
487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

595 

487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

596 
fun add_axiom (b, prop) = 
487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

597 
Thm.add_axiom (b, prop) #> 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35961
diff
changeset

598 
(fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), [])); 
35896
487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

599 

20628  600 
fun axiomatize prep mk name add raw_args thy = 
601 
let 

602 
val args = prep thy raw_args; 

603 
val specs = mk args; 

604 
val names = name args; 

29579  605 
in 
606 
thy 

35896
487b267433b1
inlined version of oldstyle Drule.add_axioms  Specification.axiom is not bootstrapped yet;
wenzelm
parents:
35856
diff
changeset

607 
> fold_map add_axiom (map Binding.name names ~~ specs) 
29579  608 
> fold add 
609 
end; 

19511  610 

611 
fun ax_classrel prep = 

20628  612 
axiomatize (map o prep) (map Logic.mk_classrel) 
613 
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; 

19511  614 

615 
fun ax_arity prep = 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

616 
axiomatize (prep o ProofContext.init) Logic.mk_arities 
20628  617 
(map (prefix arity_prefix) o Logic.name_arities) add_arity; 
19511  618 

19706  619 
fun class_const c = 
620 
(Logic.const_of_class c, Term.itselfT (Term.aT []) > propT); 

621 

19511  622 
fun ax_class prep_class prep_classrel (bclass, raw_super) thy = 
623 
let 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

624 
val class = Sign.full_name thy bclass; 
24731  625 
val super = map (prep_class thy) raw_super > Sign.minimize_sort thy; 
19511  626 
in 
627 
thy 

628 
> Sign.primitive_class (bclass, super) 

629 
> ax_classrel prep_classrel (map (fn c => (class, c)) super) 

19706  630 
> Theory.add_deps "" (class_const class) (map class_const super) 
19511  631 
end; 
632 

633 
in 

634 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

635 
val axiomatize_class = ax_class Sign.certify_class cert_classrel; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

636 
val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel; 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

637 
val axiomatize_classrel = ax_classrel cert_classrel; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

638 
val axiomatize_classrel_cmd = ax_classrel read_classrel; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

639 
val axiomatize_arity = ax_arity ProofContext.cert_arity; 
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35238
diff
changeset

640 
val axiomatize_arity_cmd = ax_arity ProofContext.read_arity; 
19511  641 

642 
end; 

643 

644 
end; 