author  wenzelm 
Sun, 25 Apr 2010 22:50:47 +0200  
changeset 36329  85004134055c 
parent 36328  4d9deabf6474 
child 36330  0584e203960e 
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 

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

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

19405  45 
(** theory data **) 
423  46 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

47 
(* axclass info *) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

48 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

49 
type info = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

50 
{def: thm, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

51 
intro: thm, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

52 
axioms: thm list, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

53 
params: (string * typ) list}; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

54 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

55 
fun make_axclass (def, intro, axioms, params): info = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

56 
{def = def, intro = intro, axioms = axioms, params = params}; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

57 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

58 

19405  59 
(* class parameters (canonical order) *) 
423  60 

19405  61 
type param = string * class; 
423  62 

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

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

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

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

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

423  69 

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

70 

19511  71 
(* setup data *) 
19392  72 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

73 
datatype data = Data of 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

74 
{axclasses: info Symtab.table, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

75 
params: param list, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

76 
proven_classrels: (thm * proof) Symreltab.table, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

77 
proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

78 
(*arity theorems with theory name*) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

79 
inst_params: 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

80 
(string * thm) Symtab.table Symtab.table * 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

81 
(*constant name ~> type constructor ~> (constant name, equation)*) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

82 
(string * string) Symtab.table (*constant name ~> (constant name, type constructor)*), 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

83 
diff_merge_classrels: (class * class) list}; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

84 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

85 
fun make_data 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

86 
(axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

87 
Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

88 
proven_arities = proven_arities, inst_params = inst_params, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

89 
diff_merge_classrels = diff_merge_classrels}; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

90 

36327  91 
structure Data = Theory_Data_PP 
22846  92 
( 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

93 
type T = data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

94 
val empty = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

95 
make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []); 
19574  96 
val extend = I; 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

97 
fun merge pp 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

98 
(Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

99 
proven_arities = proven_arities1, inst_params = inst_params1, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

100 
diff_merge_classrels = diff_merge_classrels1}, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

101 
Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

102 
proven_arities = proven_arities2, inst_params = inst_params2, 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

103 
diff_merge_classrels = diff_merge_classrels2}) = 
36325  104 
let 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

105 
val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

106 
val params' = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

107 
if null params1 then params2 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

108 
else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

109 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

110 
(*transitive closure of classrels and arity completion is done in Theory.at_begin hook*) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

111 
val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

112 
val proven_arities' = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

113 
Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

114 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

115 
val classrels1 = Symreltab.keys proven_classrels1; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

116 
val classrels2 = Symreltab.keys proven_classrels2; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

117 
val diff_merge_classrels' = 
36327  118 
subtract (op =) classrels1 classrels2 @ 
119 
subtract (op =) classrels2 classrels1 @ 

120 
diff_merge_classrels1 @ diff_merge_classrels2; 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

121 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

122 
val inst_params' = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

123 
(Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

124 
Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); 
36325  125 
in 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

126 
make_data (axclasses', params', proven_classrels', proven_arities', inst_params', 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

127 
diff_merge_classrels') 
36325  128 
end; 
22846  129 
); 
6379  130 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

131 
fun map_data f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

132 
Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

133 
make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels))); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

134 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

135 
fun map_axclasses f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

136 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

137 
(f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

138 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

139 
fun map_params f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

140 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

141 
(axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

142 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

143 
fun map_proven_classrels f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

144 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

145 
(axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels)); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

146 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

147 
fun map_proven_arities f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

148 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

149 
(axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels)); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

150 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

151 
fun map_inst_params f = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

152 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

153 
(axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels)); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

154 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

155 
val clear_diff_merge_classrels = 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

156 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) => 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

157 
(axclasses, params, proven_classrels, proven_arities, inst_params, [])); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

158 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

159 
val rep_data = Data.get #> (fn Data args => args); 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

160 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

161 
val axclasses_of = #axclasses o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

162 
val params_of = #params o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

163 
val proven_classrels_of = #proven_classrels o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

164 
val proven_arities_of = #proven_arities o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

165 
val inst_params_of = #inst_params o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

166 
val diff_merge_classrels_of = #diff_merge_classrels o rep_data; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

167 

6379  168 

19574  169 
(* maintain axclasses *) 
19392  170 

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

171 
fun get_info thy c = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

172 
(case Symtab.lookup (axclasses_of thy) c of 
36327  173 
SOME info => info 
21919  174 
 NONE => error ("No such axclass: " ^ quote c)); 
6379  175 

19123  176 
fun class_intros thy = 
19392  177 
let 
36327  178 
fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro  _ => I); 
21931
314f9e2a442c
replaced Sign.classes by Sign.all_classes (topologically sorted);
wenzelm
parents:
21925
diff
changeset

179 
val classes = Sign.all_classes thy; 
19392  180 
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

181 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

182 

85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

183 
(* maintain params *) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

184 

36327  185 
fun all_params_of thy S = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

186 
let val params = params_of thy; 
36327  187 
in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end; 
19460  188 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

189 
fun class_of_param thy = AList.lookup (op =) (params_of thy); 
19460  190 

21919  191 

19511  192 
(* maintain instances *) 
19503  193 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

194 
val classrel_prefix = "classrel_"; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

195 
val arity_prefix = "arity_"; 
25486  196 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

197 
fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a; 
19528  198 

199 

19574  200 
fun the_classrel thy (c1, c2) = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

201 
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of 
36325  202 
SOME classrel => classrel 
24920  203 
 NONE => error ("Unproven class relation " ^ 
204 
Syntax.string_of_classrel (ProofContext.init thy) [c1, c2])); 

19574  205 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

206 
fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

207 
fun the_classrel_prf thy = #2 o the_classrel thy; 
36325  208 

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

210 
let 

36327  211 
val cert = Thm.cterm_of thy; 
212 
val certT = Thm.ctyp_of thy; 

213 

36328
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
36327
diff
changeset

214 
val classes = Sorts.classes_of (Sign.classes_of thy); 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

215 
val classrels = proven_classrels_of thy; 
36325  216 

217 
fun reflcl_classrel (c1', c2') = 

36327  218 
if c1' = c2' 
219 
then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1'))) 

220 
else the_classrel_thm thy (c1', c2'); 

36325  221 
fun gen_classrel (c1_pred, c2_succ) = 
222 
let 

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

36327  224 
> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] [] 
225 
> Thm.close_derivation; 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

226 
val prf' = Thm.proof_of th'; 
36327  227 
in ((c1_pred, c2_succ), (th', prf')) end; 
36325  228 

36327  229 
val new_classrels = 
230 
Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2) 

36325  231 
> filter_out (Symreltab.defined classrels) 
36327  232 
> map gen_classrel; 
233 
val needed = not (null new_classrels); 

36325  234 
in 
235 
(needed, 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

236 
if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

237 
else thy) 
36325  238 
end; 
239 

240 
fun complete_classrels thy = 

241 
let 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

242 
val classrels = proven_classrels_of thy; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

243 
val diff_merge_classrels = diff_merge_classrels_of thy; 
36325  244 
val (needed, thy') = (false, thy) > 
245 
fold (fn c12 => fn (needed, thy) => 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

246 
put_trancl_classrel (c12, Symreltab.lookup classrels c12 > the > #1) thy 
36325  247 
>> (fn b => needed orelse b)) 
36327  248 
diff_merge_classrels; 
36325  249 
in 
250 
if null diff_merge_classrels then NONE 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

251 
else SOME (clear_diff_merge_classrels thy') 
36325  252 
end; 
19503  253 

254 

19574  255 
fun the_arity thy a (c, Ss) = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

256 
(case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of 
36325  257 
SOME arity => arity 
24920  258 
 NONE => error ("Unproven type arity " ^ 
259 
Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c]))); 

19503  260 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

261 
fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss > #1 > #1 > Thm.transfer thy; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

262 
fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss > #2; 
36325  263 

33172  264 
fun thynames_of_arity thy (c, a) = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

265 
Symtab.lookup_list (proven_arities_of thy) a 
36325  266 
> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE) 
27497  267 
> rev; 
27397  268 

36325  269 
fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities = 
27547  270 
let 
271 
val algebra = Sign.classes_of thy; 

33172  272 
val super_class_completions = 
273 
Sign.super_classes thy c 

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

278 
let 

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

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

36327  281 
> Thm.close_derivation; 
282 
val prf1 = Thm.proof_of th1; 

283 
in (((th1, thy_name), prf1), c1) end); 

36325  284 
val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1))) 
27547  285 
completions arities; 
33172  286 
in (null completions, arities') end; 
19503  287 

27547  288 
fun put_arity ((t, Ss, c), th) thy = 
289 
let 

36325  290 
val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th))); 
27547  291 
in 
292 
thy 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

293 
> map_proven_arities 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

294 
(Symtab.insert_list (eq_fst op =) arity' #> 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

295 
insert_arity_completions thy arity' #> snd) 
27547  296 
end; 
19503  297 

31944  298 
fun complete_arities thy = 
27547  299 
let 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

300 
val arities = proven_arities_of thy; 
33172  301 
val (finished, arities') = arities 
302 
> fold_map (insert_arity_completions thy) (Symtab.dest_list arities); 

303 
in 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

304 
if forall I finished 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

305 
then NONE 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

306 
else SOME (map_proven_arities (K arities') thy) 
27547  307 
end; 
308 

36325  309 
val _ = Context.>> (Context.map_theory 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

310 
(Theory.at_begin complete_classrels #> Theory.at_begin complete_arities)); 
27397  311 

312 

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

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

314 

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

315 
fun get_inst_param thy (c, tyco) = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

316 
(case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of 
36327  317 
SOME c' => c' 
318 
 NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco)); 

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

319 

36327  320 
fun add_inst_param (c, tyco) inst = 
321 
(map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) 

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

322 
#> (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

323 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

324 
val inst_of_param = Symtab.lookup o #2 o inst_params_of; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

325 
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

326 

36327  327 
fun inst_thms thy = 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

328 
Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) []; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

329 

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

331 

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

332 
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

333 
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

334 

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

335 
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

336 
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

337 

36327  338 
fun lookup_inst_param consts params (c, T) = 
339 
(case get_inst_tyco consts (c, T) of 

340 
SOME tyco => AList.lookup (op =) params (c, tyco) 

341 
 NONE => NONE); 

31249  342 

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

343 
fun unoverload_const thy (c_ty as (c, _)) = 
36327  344 
if is_some (class_of_param thy c) then 
345 
(case get_inst_tyco (Sign.consts_of thy) c_ty of 

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

347 
 NONE => c) 

33969  348 
else c; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

349 

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

350 

36327  351 

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

353 

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

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

355 

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

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

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

364 
 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

365 
commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); 
19405  366 
in (c1, c2) end; 
367 

368 
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

369 
cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel) 
19405  370 
handle TYPE (msg, _, _) => error msg; 
371 

372 

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

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

374 

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

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

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

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

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

379 
quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); 
31249  380 

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

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

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

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

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

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

386 
 NONE => error ("Not a class parameter: " ^ quote c)); 
31249  387 
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

388 
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

389 
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

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

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

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

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

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

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

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

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

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

399 
#> (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

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

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

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

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

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

405 

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

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

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

408 
val T = Term.fastype_of t; 
31249  409 
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

410 
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

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

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

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

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

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

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

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

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

419 

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

420 

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

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

422 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

423 
val shyps_topped = forall null o #shyps o Thm.rep_thm; 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

424 

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

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

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

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

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

429 
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

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

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

434 
> Drule.unconstrainTs; 

36327  435 
val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain"; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

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

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

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

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

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

442 

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

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

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

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

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

447 
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

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

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

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

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

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

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

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

458 
> Drule.unconstrainTs; 

36327  459 
val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain"; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

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

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

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

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

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

466 

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

467 

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

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

469 

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

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

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

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

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

474 
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

475 
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

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

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

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

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

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

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

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

483 

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

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

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

486 
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

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

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

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

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

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

492 
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

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

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

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

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

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

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

499 

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

500 

19511  501 

502 
(** class definitions **) 

503 

23421  504 
fun split_defined n eq = 
505 
let 

506 
val intro = 

507 
(eq RS Drule.equal_elim_rule2) 

508 
> Conjunction.curry_balanced n 

509 
> n = 0 ? Thm.eq_assumption 1; 

510 
val dests = 

511 
if n = 0 then [] 

512 
else 

513 
(eq RS Drule.equal_elim_rule1) 

32765  514 
> Balanced_Tree.dest (fn th => 
23421  515 
(th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; 
516 
in (intro, dests) end; 

517 

24964  518 
fun define_class (bclass, raw_super) raw_params raw_specs thy = 
19511  519 
let 
520 
val ctxt = ProofContext.init thy; 

24964  521 
val pp = Syntax.pp ctxt; 
19511  522 

523 

24964  524 
(* class *) 
19511  525 

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

526 
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

527 
val class = Sign.full_name thy bclass; 
24731  528 
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); 
19511  529 

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

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

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

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

536 

537 
(* params *) 

538 

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

540 
let 

541 
val T = Sign.the_const_type thy p; 

542 
val _ = 

543 
(case Term.add_tvarsT T [] of 

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

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

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

547 
in (p, T') end); 

548 

549 

550 
(* axioms *) 

551 

19511  552 
fun prep_axiom t = 
553 
(case Term.add_tfrees t [] of 

24964  554 
[(a, S)] => check_constraint (a, S) 
555 
 [] => () 

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

557 
t 

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

559 
> Logic.close_form); 

19511  560 

24681  561 
val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; 
22745  562 
val name_atts = map fst raw_specs; 
19511  563 

564 

565 
(* definition *) 

566 

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

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

571 
val ([def], def_thy) = 

572 
thy 

573 
> Sign.primitive_class (bclass, super) 

35238  574 
> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])]; 
19511  575 
val (raw_intro, (raw_classrel, raw_axioms)) = 
23421  576 
split_defined (length conjs) def > chop (length super); 
19392  577 

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

578 

19511  579 
(* facts *) 
580 

581 
val class_triv = Thm.class_triv def_thy class; 

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

583 
def_thy 

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

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

585 
> PureThy.note_thmss "" 
36326  586 
[((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]), 
587 
((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]), 

588 
((Binding.name "axioms", []), 

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

589 
[(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

590 
> Sign.restore_naming def_thy; 
19511  591 

24847  592 

19511  593 
(* result *) 
594 

36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

595 
val axclass = make_axclass (def, intro, axioms, params); 
19511  596 
val result_thy = 
597 
facts_thy 

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

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

600 
> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) > snd 
19511  601 
> Sign.restore_naming facts_thy 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

602 
> map_axclasses (Symtab.update (class, axclass)) 
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

603 
> map_params (fold (fn (x, _) => add_param pp (x, class)) params); 
19511  604 

605 
in (class, result_thy) end; 

606 

607 

19531  608 

19511  609 
(** axiomatizations **) 
610 

611 
local 

612 

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

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

614 

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

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

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

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

618 

20628  619 
fun axiomatize prep mk name add raw_args thy = 
620 
let 

621 
val args = prep thy raw_args; 

622 
val specs = mk args; 

623 
val names = name args; 

29579  624 
in 
625 
thy 

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

626 
> fold_map add_axiom (map Binding.name names ~~ specs) 
29579  627 
> fold add 
628 
end; 

19511  629 

630 
fun ax_classrel prep = 

20628  631 
axiomatize (map o prep) (map Logic.mk_classrel) 
632 
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; 

19511  633 

634 
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

635 
axiomatize (prep o ProofContext.init) Logic.mk_arities 
20628  636 
(map (prefix arity_prefix) o Logic.name_arities) add_arity; 
19511  637 

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

640 

19511  641 
fun ax_class prep_class prep_classrel (bclass, raw_super) thy = 
642 
let 

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

643 
val class = Sign.full_name thy bclass; 
24731  644 
val super = map (prep_class thy) raw_super > Sign.minimize_sort thy; 
19511  645 
in 
646 
thy 

647 
> Sign.primitive_class (bclass, super) 

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

19706  649 
> Theory.add_deps "" (class_const class) (map class_const super) 
19511  650 
end; 
651 

652 
in 

653 

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

654 
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

655 
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

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

657 
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

658 
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

659 
val axiomatize_arity_cmd = ax_arity ProofContext.read_arity; 
19511  660 

661 
end; 

662 

663 
end; 