author  wenzelm 
Sat, 14 Dec 2013 17:28:05 +0100  
changeset 54742  7a86358a3c0b 
parent 53171  a5e54d4d9081 
child 54931  88cf06038e37 
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 
36417  5 
parameters. Proven class relations and type arities. 
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 

51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51671
diff
changeset

8 
signature AXCLASS = 
3938  9 
sig 
36427  10 
type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} 
11 
val get_info: theory > class > info 

12 
val class_of_param: theory > string > class option 

13 
val instance_name: string * class > string 

14 
val thynames_of_arity: theory > class * string > string list 

15 
val param_of_inst: theory > string * string > string 

16 
val inst_of_param: theory > string > (string * string) option 

17 
val unoverload: theory > thm > thm 

18 
val overload: theory > thm > thm 

19 
val unoverload_conv: theory > conv 

20 
val overload_conv: theory > conv 

21 
val lookup_inst_param: Consts.T > ((string * string) * 'a) list > string * typ > 'a option 

22 
val unoverload_const: theory > string * typ > string 

23 
val cert_classrel: theory > class * class > class * class 

24 
val read_classrel: theory > xstring * xstring > class * class 

25 
val declare_overloaded: string * typ > theory > term * theory 

26 
val define_overloaded: binding > string * term > theory > thm * theory 

37246  27 
val add_classrel: thm > theory > theory 
28 
val add_arity: thm > theory > theory 

51671  29 
val prove_classrel: class * class > (Proof.context > tactic) > theory > theory 
30 
val prove_arity: string * sort list * sort > (Proof.context > tactic) > theory > theory 

36427  31 
val define_class: binding * class list > string list > 
32 
(Thm.binding * term list) list > theory > class * theory 

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

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

34 
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

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

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

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

38 
val axiomatize_arity_cmd: xstring * string list * string > theory > theory 
3938  39 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

40 

51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51671
diff
changeset

41 
structure Axclass: AXCLASS = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

43 

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

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

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

47 

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

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

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

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

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

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

53 

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

54 
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

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

56 

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

57 

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

19405  60 
type param = string * class; 
423  61 

42389  62 
fun add_param ctxt ((x, c): param) params = 
19405  63 
(case AList.lookup (op =) params x of 
64 
NONE => (x, c) :: params 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42375
diff
changeset

65 
 SOME c' => 
42389  66 
error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^ 
67 
(if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))); 

423  68 

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

69 

19511  70 
(* setup data *) 
19392  71 

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

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

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

74 
params: param list, 
36418
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

75 
proven_classrels: thm Symreltab.table, 
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

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

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

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

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

80 
(*constant name ~> type constructor ~> (constant name, equation)*) 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

82 

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

83 
fun make_data 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

85 
Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels, 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

87 

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

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

91 
val empty = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

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

95 
(Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1, 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

97 
Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2, 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

98 
proven_arities = proven_arities2, inst_params = inst_params2}) = 
36325  99 
let 
42389  100 
val ctxt = Syntax.init_pretty pp; 
101 

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

102 
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

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

104 
if null params1 then params2 
42389  105 
else 
106 
fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p) 

107 
params2 params1; 

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

108 

50760  109 
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*) 
50768
2172f82de515
tuned  prefer highlevel Table.merge with its slightly more conservative update;
wenzelm
parents:
50764
diff
changeset

110 
val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2); 
2172f82de515
tuned  prefer highlevel Table.merge with its slightly more conservative update;
wenzelm
parents:
50764
diff
changeset

111 
val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2); 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

112 

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

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

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

115 
Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); 
36325  116 
in 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

117 
make_data (axclasses', params', proven_classrels', proven_arities', inst_params') 
36325  118 
end; 
22846  119 
); 
6379  120 

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

121 
fun map_data f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

122 
Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params} => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

124 

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

125 
fun map_axclasses f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

126 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

128 

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

129 
fun map_params f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

130 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

132 

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

133 
fun map_proven_classrels f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

134 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

136 

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

137 
fun map_proven_arities f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

138 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

140 

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

141 
fun map_inst_params f = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

142 
map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) => 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

144 

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

145 
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

146 

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

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

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

149 
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

150 
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

151 
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

152 

6379  153 

36346  154 
(* axclasses with parameters *) 
19392  155 

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

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

157 
(case Symtab.lookup (axclasses_of thy) c of 
36327  158 
SOME info => info 
21919  159 
 NONE => error ("No such axclass: " ^ quote c)); 
6379  160 

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

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

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

165 
fun class_of_param thy = AList.lookup (op =) (params_of thy); 
19460  166 

21919  167 

19511  168 
(* maintain instances *) 
19503  169 

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

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

171 
val arity_prefix = "arity_"; 
25486  172 

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

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

175 

50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

176 
val update_classrel = map_proven_classrels o Symreltab.update; 
36421
066e35d1c0d7
tuned classrel completion  bypass composition with reflexive edges;
wenzelm
parents:
36420
diff
changeset

177 

50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

178 
val is_classrel = Symreltab.defined o proven_classrels_of; 
36421
066e35d1c0d7
tuned classrel completion  bypass composition with reflexive edges;
wenzelm
parents:
36420
diff
changeset

179 

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

181 
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

182 
SOME thm => Thm.transfer thy thm 
24920  183 
 NONE => error ("Unproven class relation " ^ 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

184 
Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); 
36325  185 

186 
fun complete_classrels thy = 

187 
let 

50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

188 
fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) = 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

189 
let 
50769  190 
fun compl c1 c2 (finished2, thy2) = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

191 
if is_classrel thy2 (c1, c2) then (finished2, thy2) 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

192 
else 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

193 
(false, 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

194 
thy2 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

195 
> update_classrel ((c1, c2), 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

196 
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

197 
> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] [] 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

198 
> Thm.close_derivation)); 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

199 

50769  200 
val proven = is_classrel thy1; 
201 
val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; 

202 
val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; 

203 
in 

204 
fold_product compl preds succs (finished1, thy1) 

205 
end; 

36325  206 
in 
50769  207 
(case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of 
208 
(true, _) => NONE 

209 
 (_, thy') => SOME thy') 

36325  210 
end; 
19503  211 

212 

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

214 
(case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

215 
SOME (thm, _) => Thm.transfer thy thm 
24920  216 
 NONE => error ("Unproven type arity " ^ 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

217 
Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); 
19503  218 

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

220 
Symtab.lookup_list (proven_arities_of thy) a 
36418
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

221 
> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE) 
27497  222 
> rev; 
27397  223 

36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

224 
fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) = 
27547  225 
let 
226 
val algebra = Sign.classes_of thy; 

36417  227 
val ars = Symtab.lookup_list arities t; 
33172  228 
val super_class_completions = 
229 
Sign.super_classes thy c 

36417  230 
> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => 
231 
c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars); 

232 

43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42389
diff
changeset

233 
val names = Name.invent Name.context Name.aT (length Ss); 
36417  234 
val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names; 
235 

36325  236 
val completions = super_class_completions > map (fn c1 => 
237 
let 

36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

238 
val th1 = 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

239 
(th RS the_classrel thy (c, c1)) 
36417  240 
> Drule.instantiate' std_vars [] 
36327  241 
> Thm.close_derivation; 
36418
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

242 
in ((th1, thy_name), c1) end); 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

243 

7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

244 
val finished' = finished andalso null completions; 
36418
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

245 
val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities; 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

246 
in (finished', arities') end; 
19503  247 

50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

248 
fun put_arity_completion ((t, Ss, c), th) thy = 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

249 
let val ar = ((c, Ss), (th, Context.theory_name thy)) in 
27547  250 
thy 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

251 
> map_proven_arities 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

252 
(Symtab.insert_list (eq_fst op =) (t, ar) #> 
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

253 
curry (insert_arity_completions thy t ar) true #> #2) 
27547  254 
end; 
19503  255 

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

258 
val arities = proven_arities_of thy; 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

259 
val (finished, arities') = 
50769  260 
Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) 
261 
arities (true, arities); 

33172  262 
in 
36419
7aea10d10113
tuned aritiy completion  slightly less intermediate data structures;
wenzelm
parents:
36418
diff
changeset

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

264 
else SOME (map_proven_arities (K arities') thy) 
27547  265 
end; 
266 

53171  267 
val _ = Theory.setup 
268 
(Theory.at_begin complete_classrels #> Theory.at_begin complete_arities); 

27397  269 

36740  270 
val _ = Proofterm.install_axclass_proofs 
271 
{classrel_proof = Thm.proof_of oo the_classrel, 

272 
arity_proof = Thm.proof_of oo the_arity}; 

36418
752ee03427c2
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
wenzelm
parents:
36417
diff
changeset

273 

27397  274 

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

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

276 

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

277 
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

278 
(case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of 
36327  279 
SOME c' => c' 
280 
 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

281 

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

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

285 

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

286 
val inst_of_param = Symtab.lookup o #2 o inst_params_of; 
36417  287 
val param_of_inst = #1 oo get_inst_param; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

288 

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

290 
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

291 

36417  292 
fun get_inst_tyco consts = try (#1 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

293 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

294 
fun unoverload thy = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

295 
rewrite_rule (Proof_Context.init_global thy) (inst_thms thy); 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

296 

7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

297 
fun overload thy = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

298 
rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy)); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

299 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

300 
fun unoverload_conv thy = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

301 
Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy); 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

302 

7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

303 
fun overload_conv thy = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

304 
Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy)); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

305 

36327  306 
fun lookup_inst_param consts params (c, T) = 
307 
(case get_inst_tyco consts (c, T) of 

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

309 
 NONE => NONE); 

31249  310 

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

311 
fun unoverload_const thy (c_ty as (c, _)) = 
36327  312 
if is_some (class_of_param thy c) then 
313 
(case get_inst_tyco (Sign.consts_of thy) c_ty of 

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

315 
 NONE => c) 

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

317 

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

318 

36327  319 

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

321 

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

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

323 

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

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

326 
val string_of_sort = Syntax.string_of_sort_global thy; 
19405  327 
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; 
52788  328 
val _ = Sign.primitive_classrel (c1, c2) thy; 
19405  329 
val _ = 
19460  330 
(case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of 
19405  331 
[] => () 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26516
diff
changeset

332 
 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

333 
commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); 
19405  334 
in (c1, c2) end; 
335 

336 
fun read_classrel thy raw_rel = 

42360  337 
cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) 
19405  338 
handle TYPE (msg, _, _) => error msg; 
339 

340 

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

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

342 

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

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

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

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

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

347 
quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); 
31249  348 

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

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

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

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

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

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

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

356 
val name_inst = instance_name (tyco, class) ^ "_inst"; 
36417  357 
val c' = instance_name (tyco, c); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

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

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

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

361 
> Sign.qualified_path true (Binding.name name_inst) 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

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

363 
> (fn const' as Const (c'', _) => 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

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

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

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

367 
#> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39134
diff
changeset

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

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

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

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

373 

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

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

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

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

378 
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

379 
val prop = Logic.mk_equals (Const (c', T), t); 
36417  380 
val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25486
diff
changeset

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

382 
thy 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

383 
> Thm.add_def_global false false (b', prop) 
38383  384 
>> (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

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

386 

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

387 

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

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

389 

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

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

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

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

394 
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

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

396 
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); 
50769  397 
val (th', thy') = 
398 
Global_Theory.store_thm 

399 
(Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy; 

37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

400 
val th'' = th' 
36934
ae0809cff6f0
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
krauss
parents:
36881
diff
changeset

401 
> Thm.unconstrainT 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

402 
> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] []; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

403 
in 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

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

405 
> Sign.primitive_classrel (c1, c2) 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

406 
> map_proven_classrels (Symreltab.update ((c1, c2), th'')) 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

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

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

410 

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

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

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

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

415 
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

416 
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); 
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

417 

50769  418 
val (th', thy') = 
419 
Global_Theory.store_thm 

420 
(Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy; 

36417  421 

43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42389
diff
changeset

422 
val args = Name.invent_names Name.context Name.aT Ss; 
36417  423 
val T = Type (t, map TFree args); 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

424 
val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args; 
36417  425 

37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

426 
val missing_params = Sign.complete_sort thy' [c] 
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

427 
> maps (these o Option.map #params o try (get_info thy')) 
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

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

429 
> (map o apsnd o map_atyps) (K T); 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

430 
val th'' = th' 
36934
ae0809cff6f0
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
krauss
parents:
36881
diff
changeset

431 
> Thm.unconstrainT 
ae0809cff6f0
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
krauss
parents:
36881
diff
changeset

432 
> Drule.instantiate' std_vars []; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

433 
in 
37232
c10fb22a5e0c
classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe
parents:
36935
diff
changeset

434 
thy' 
36417  435 
> fold (#2 oo declare_overloaded) missing_params 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

436 
> Sign.primitive_arity (t, Ss, [c]) 
50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

437 
> put_arity_completion ((t, Ss, c), th'') 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

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

439 

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

440 

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

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

442 

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

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

444 
let 
42360  445 
val ctxt = Proof_Context.init_global thy; 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

446 
val (c1, c2) = cert_classrel thy raw_rel; 
51671  447 
val th = 
448 
Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (fn {context, ...} => tac context) 

449 
handle ERROR msg => 

450 
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ 

451 
quote (Syntax.string_of_classrel ctxt [c1, c2])); 

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

452 
in 
37249  453 
thy > add_classrel th 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

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

455 

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

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

457 
let 
42360  458 
val ctxt = Proof_Context.init_global thy; 
459 
val arity = Proof_Context.cert_arity ctxt raw_arity; 

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

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

461 
val props = Logic.mk_arities arity; 
51671  462 
val ths = 
463 
Goal.prove_multi ctxt [] [] props 

464 
(fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context) 

465 
handle ERROR msg => 

466 
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ 

467 
quote (Syntax.string_of_arity ctxt arity)); 

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

468 
in 
37249  469 
thy > fold add_arity ths 
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30519
diff
changeset

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

471 

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

472 

19511  473 

474 
(** class definitions **) 

475 

23421  476 
fun split_defined n eq = 
477 
let 

478 
val intro = 

479 
(eq RS Drule.equal_elim_rule2) 

480 
> Conjunction.curry_balanced n 

481 
> n = 0 ? Thm.eq_assumption 1; 

482 
val dests = 

483 
if n = 0 then [] 

484 
else 

485 
(eq RS Drule.equal_elim_rule1) 

32765  486 
> Balanced_Tree.dest (fn th => 
23421  487 
(th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; 
488 
in (intro, dests) end; 

489 

24964  490 
fun define_class (bclass, raw_super) raw_params raw_specs thy = 
19511  491 
let 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
38383
diff
changeset

492 
val ctxt = Syntax.init_pretty_global thy; 
19511  493 

494 

24964  495 
(* class *) 
19511  496 

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

497 
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

498 
val class = Sign.full_name thy bclass; 
24731  499 
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); 
19511  500 

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

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

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

504 
Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^ 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
38383
diff
changeset

505 
" needs to be weaker than " ^ Syntax.string_of_sort ctxt super); 
24964  506 

507 

508 
(* params *) 

509 

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

511 
let 

512 
val T = Sign.the_const_type thy p; 

513 
val _ = 

514 
(case Term.add_tvarsT T [] of 

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

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

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

518 
in (p, T') end); 

519 

520 

521 
(* axioms *) 

522 

19511  523 
fun prep_axiom t = 
524 
(case Term.add_tfrees t [] of 

24964  525 
[(a, S)] => check_constraint (a, S) 
526 
 [] => () 

39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
38383
diff
changeset

527 
 _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t); 
24964  528 
t 
529 
> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT []  U => U)) 

530 
> Logic.close_form); 

19511  531 

24681  532 
val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; 
22745  533 
val name_atts = map fst raw_specs; 
19511  534 

535 

536 
(* definition *) 

537 

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

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

542 
val ([def], def_thy) = 

543 
thy 

544 
> Sign.primitive_class (bclass, super) 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39134
diff
changeset

545 
> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])]; 
19511  546 
val (raw_intro, (raw_classrel, raw_axioms)) = 
23421  547 
split_defined (length conjs) def > chop (length super); 
19392  548 

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

549 

19511  550 
(* facts *) 
551 

552 
val class_triv = Thm.class_triv def_thy class; 

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

554 
def_thy 

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

555 
> Sign.qualified_path true bconst 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39134
diff
changeset

556 
> Global_Theory.note_thmss "" 
36326  557 
[((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]), 
558 
((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]), 

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

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

561 
> Sign.restore_naming def_thy; 
19511  562 

24847  563 

19511  564 
(* result *) 
565 

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

566 
val axclass = make_axclass (def, intro, axioms, params); 
19511  567 
val result_thy = 
568 
facts_thy 

50764
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

569 
> map_proven_classrels 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

570 
(fold2 (fn c => fn th => Symreltab.update ((class, c), th)) super classrel) 
2bbc7ae80634
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
wenzelm
parents:
50760
diff
changeset

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

572 
> Sign.qualified_path false bconst 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39134
diff
changeset

573 
> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39134
diff
changeset

574 
> #2 
19511  575 
> Sign.restore_naming facts_thy 
36329
85004134055c
more systematic treatment of data  avoid slightly odd nested tuples here;
wenzelm
parents:
36328
diff
changeset

576 
> map_axclasses (Symtab.update (class, axclass)) 
42389  577 
> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params); 
19511  578 

579 
in (class, result_thy) end; 

580 

581 

19531  582 

19511  583 
(** axiomatizations **) 
584 

585 
local 

586 

36417  587 
(*oldstyle axioms*) 
20628  588 
fun axiomatize prep mk name add raw_args thy = 
589 
let 

590 
val args = prep thy raw_args; 

591 
val specs = mk args; 

592 
val names = name args; 

29579  593 
in 
594 
thy 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

595 
> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs) 
37249  596 
> fold (add o Drule.export_without_context o snd) 
29579  597 
end; 
19511  598 

599 
fun ax_classrel prep = 

20628  600 
axiomatize (map o prep) (map Logic.mk_classrel) 
37249  601 
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; 
19511  602 

603 
fun ax_arity prep = 

42360  604 
axiomatize (prep o Proof_Context.init_global) Logic.mk_arities 
37249  605 
(map (prefix arity_prefix) o Logic.name_arities) add_arity; 
19511  606 

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

609 

19511  610 
fun ax_class prep_class prep_classrel (bclass, raw_super) thy = 
611 
let 

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

612 
val class = Sign.full_name thy bclass; 
24731  613 
val super = map (prep_class thy) raw_super > Sign.minimize_sort thy; 
19511  614 
in 
615 
thy 

616 
> Sign.primitive_class (bclass, super) 

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

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

618 
> Theory.add_deps_global "" (class_const class) (map class_const super) 
19511  619 
end; 
620 

621 
in 

622 

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

623 
val axiomatize_class = ax_class Sign.certify_class cert_classrel; 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

624 
val axiomatize_class_cmd = 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

625 
ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel; 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

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

627 
val axiomatize_classrel_cmd = ax_classrel read_classrel; 
42360  628 
val axiomatize_arity = ax_arity Proof_Context.cert_arity; 
629 
val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity; 

19511  630 

631 
end; 

632 

633 
end; 