author  wenzelm 
Wed, 27 Jul 1994 15:14:31 +0200  
changeset 487  af83700cb771 
parent 474  ac1d1988d528 
child 560  6702a715281d 
permissions  rwrr 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/axclass.ML 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

3 
Author: Markus Wenzel, TU Muenchen 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

4 

423  5 
Higher level user interfaces for axiomatic type classes. 
449  6 

7 
TODO: 

8 
remove add_sigclass (?) 

9 
remove goal_... (?) 

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

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

12 

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

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

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

15 
structure Tactical: TACTICAL 
423  16 
local open Tactical Tactical.Thm Tactical.Thm.Sign.Syntax.Mixfix in 
17 
val add_thms_as_axms: (string * thm) list > theory > theory 

18 
val add_classrel_thms: thm list > theory > theory 

19 
val add_arity_thms: thm list > theory > theory 

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

20 
val add_axclass: class * class list > (string * string) list 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

22 
val add_axclass_i: class * class list > (string * term) list 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

23 
> theory > theory 
423  24 
val add_sigclass: class * class list > (string * string * mixfix) list 
25 
> theory > theory 

26 
val add_sigclass_i: class * class list > (string * typ * mixfix) list 

27 
> theory > theory 

28 
val prove_classrel: theory > class * class > thm list 

29 
> tactic option > thm 

30 
val prove_arity: theory > string * sort list * class > thm list 

31 
> tactic option > thm 

449  32 
val add_inst_subclass: class * class > string list > thm list 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

33 
> tactic option > theory > theory 
449  34 
val add_inst_arity: string * sort list * class list > string list 
423  35 
> thm list > tactic option > theory > theory 
487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

36 
val add_defns: (string * string) list > theory > theory 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

37 
val add_defns_i: (string * term) list > theory > theory 
474  38 
val mk_classrel: class * class > term 
39 
val dest_classrel: term > class * class 

40 
val mk_arity: string * sort list * class > term 

41 
val dest_arity: term > string * sort list * class 

42 
val class_axms: theory > thm list 

43 
val axclass_tac: theory > thm list > tactic 

44 
val goal_subclass: theory > class * class > thm list 

45 
val goal_arity: theory > string * sort list * class > thm list 

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

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

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

48 

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

49 
functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC 
474  50 
sharing Goals.Tactical = Tactic.Tactical): AX_CLASS = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

52 

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

53 
structure Tactical = Goals.Tactical; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

54 
structure Thm = Tactical.Thm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

55 
structure Sign = Thm.Sign; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

56 
structure Type = Sign.Type; 
487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

57 
structure Pretty = Sign.Syntax.Pretty; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

58 

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

59 
open Logic Thm Tactical Tactic Goals; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

60 

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

61 

487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

62 
(** add constant definitions **) (* FIXME > drule.ML (?) *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

63 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

64 
(* all_axioms_of *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

65 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

66 
(*results may contain duplicates!*) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

67 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

68 
fun ancestry_of thy = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

69 
thy :: flat (map ancestry_of (parents_of thy)); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

70 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

71 
val all_axioms_of = flat o map axioms_of o ancestry_of; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

72 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

73 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

74 
(* clash_types, clash_consts *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

75 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

76 
(*check if types have common instance (ignoring sorts)*) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

77 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

78 
fun clash_types ty1 ty2 = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

79 
let 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

80 
val ty1' = Type.varifyT ty1; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

81 
val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

82 
in 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

83 
Type.raw_unify (ty1', ty2') 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

84 
end; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

85 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

86 
fun clash_consts (c1, ty1) (c2, ty2) = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

87 
c1 = c2 andalso clash_types ty1 ty2; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

88 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

89 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

90 
(* clash_defns *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

91 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

92 
fun clash_defn c_ty (name, tm) = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

93 
let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

94 
if clash_consts c_ty (c, ty') then Some (name, ty') else None 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

95 
end handle TERM _ => None; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

96 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

97 
fun clash_defns c_ty axms = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

98 
distinct (mapfilter (clash_defn c_ty) axms); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

99 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

100 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

101 
(* dest_defn *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

102 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

103 
fun dest_defn tm = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

104 
let 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

105 
fun err msg = raise_term msg [tm]; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

106 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

107 
val (lhs, rhs) = Logic.dest_equals tm 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

108 
handle TERM _ => err "Not a metaequality (==)"; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

109 
val (head, args) = strip_comb lhs; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

110 
val (c, ty) = dest_Const head 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

111 
handle TERM _ => err "Head of lhs not a constant"; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

112 

487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

113 
fun occs_const (Const c_ty') = clash_consts (c, ty) c_ty' 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

114 
 occs_const (Abs (_, _, t)) = occs_const t 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

115 
 occs_const (t $ u) = occs_const t orelse occs_const u 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

116 
 occs_const _ = false; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

117 
in 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

118 
if not (forall is_Free args) then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

119 
err "Arguments of lhs have to be variables" 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

120 
else if not (null (duplicates args)) then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

121 
err "Duplicate variables on lhs" 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

122 
else if not (term_frees rhs subset args) then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

123 
err "Extra variables on rhs" 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

124 
else if not (term_tfrees rhs subset typ_tfrees ty) then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

125 
err "Extra type variables on rhs" 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

126 
else if occs_const rhs then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

127 
err "Constant to be defined clashes with occurrence(s) on rhs" 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

128 
else (c, ty) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

129 
end; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

130 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

131 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

132 
(* check_defn *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

133 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

134 
fun err_in_axm name msg = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

135 
(writeln msg; error ("The error(s) above occurred in axiom " ^ quote name)); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

136 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

137 
fun check_defn sign (axms, (name, tm)) = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

138 
let 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

139 
fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

140 
[Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty])); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

141 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

142 
fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

143 
fun show_defns c = commas o map (show_defn c); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

144 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

145 
val (c, ty) = dest_defn tm 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

146 
handle TERM (msg, _) => err_in_axm name msg; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

147 
val defns = clash_defns (c, ty) axms; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

148 
in 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

149 
if not (null defns) then 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

150 
err_in_axm name ("Definition of " ^ show_const (c, ty) ^ 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

151 
" clashes with " ^ show_defns c defns) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

152 
else (name, tm) :: axms 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

153 
end; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

154 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

155 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

156 
(* add_defns *) 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

157 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

158 
fun ext_defns prep_axm raw_axms thy = 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

159 
let 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

160 
val axms = map (prep_axm (sign_of thy)) raw_axms; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

161 
val all_axms = all_axioms_of thy; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

162 
in 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

163 
foldl (check_defn (sign_of thy)) (all_axms, axms); 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

164 
add_axioms_i axms thy 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

165 
end; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

166 

af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

167 
val add_defns_i = ext_defns cert_axm; 
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

168 
val add_defns = ext_defns read_axm; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

169 

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

170 

423  171 

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

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

173 

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

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

175 

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

176 
fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

179 

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

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

181 

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

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

183 

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

184 

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

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

186 

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

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

188 
Some (get_axiom thy name) handle THEORY _ => None; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

189 

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

190 
val get_axioms = mapfilter o get_ax; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

191 

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

192 

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

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

194 

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

195 
fun is_defn thm = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

196 
(case #prop (rep_thm thm) of 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

197 
Const ("==", _) $ _ $ _ => true 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

198 
 _ => false); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

199 

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

200 

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

201 

423  202 
(** abstract syntax operations **) (* FIXME > logic.ML (?) *) 
203 

204 
(* subclass relations as terms *) 

205 

206 
fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2); 

207 

208 
fun dest_classrel tm = 

209 
let 

210 
fun err () = raise_term "dest_classrel" [tm]; 

211 

212 
val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err (); 

213 
val c1 = (case ty of TFree (_, [c]) => c  _ => err ()); 

214 
in 

215 
(c1, c2) 

216 
end; 

217 

218 

219 
(* arities as terms *) 

220 

221 
fun mk_arity (t, ss, c) = 

222 
let 

449  223 
val names = tl (variantlist (replicate (length ss + 1) "'", [])); 
423  224 
val tfrees = map TFree (names ~~ ss); 
225 
in 

226 
mk_inclass (Type (t, tfrees), c) 

227 
end; 

228 

229 
fun dest_arity tm = 

230 
let 

231 
fun err () = raise_term "dest_arity" [tm]; 

232 

233 
val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err (); 

234 
val (t, tfrees) = 

235 
(case ty of 

236 
Type (t, tys) => (t, map (fn TFree x => x  _ => err ()) tys) 

237 
 _ => err ()); 

238 
val ss = 

239 
if null (gen_duplicates eq_fst tfrees) 

240 
then map snd tfrees else err (); 

241 
in 

242 
(t, ss, c) 

243 
end; 

244 

245 

246 

247 
(** add theorems as axioms **) (* FIXME > drule.ML (?) *) 

248 

249 
fun prep_thm_axm thy thm = 

250 
let 

251 
fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); 

252 

253 
val {sign, hyps, prop, ...} = rep_thm thm; 

254 
in 

255 
if not (Sign.subsig (sign, sign_of thy)) then 

256 
err "theorem not of same theory" 

257 
else if not (null hyps) then 

258 
err "theorem may not contain hypotheses" 

259 
else prop 

260 
end; 

261 

262 
(*general theorems*) 

263 
fun add_thms_as_axms thms thy = 

264 
add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy; 

265 

266 
(*theorems expressing class relations*) 

267 
fun add_classrel_thms thms thy = 

268 
let 

269 
fun prep_thm thm = 

270 
let 

271 
val prop = prep_thm_axm thy thm; 

272 
val (c1, c2) = dest_classrel prop handle TERM _ => 

273 
raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]); 

274 
in (c1, c2) end; 

275 
in 

276 
add_classrel (map prep_thm thms) thy 

277 
end; 

278 

279 
(*theorems expressing arities*) 

280 
fun add_arity_thms thms thy = 

281 
let 

282 
fun prep_thm thm = 

283 
let 

284 
val prop = prep_thm_axm thy thm; 

285 
val (t, ss, c) = dest_arity prop handle TERM _ => 

286 
raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]); 

287 
in (t, ss, [c]) end; 

288 
in 

289 
add_arities (map prep_thm thms) thy 

290 
end; 

291 

292 

293 

294 
(** add axiomatic type classes **) 

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

295 

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

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

297 

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

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

299 
error ("Axiomatic class " ^ quote c ^ " not subclass of \"logic\""); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

300 

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

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

302 
error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

303 

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

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

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

306 

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

307 

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

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

309 

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

310 
fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

312 
val axioms = map (prep_axm (sign_of old_thy)) raw_axioms; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

313 
val thy = add_classes [([], class, super_classes)] old_thy; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

314 
val sign = sign_of thy; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

315 

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

316 

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

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

318 

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

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

320 
if null (term_tfrees ax) then 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

321 
mk_implies (mk_inclass (aT logicS, class), ax) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

323 
map_term_tfrees (K (aT [class])) ax; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

324 

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

325 
val abs_axioms = map (apsnd abs_axm) axioms; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

326 

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

327 

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

328 
(* prepare introduction orule *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

329 

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

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

331 
if Sign.subsort sign ([class], logicS) then () 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

333 

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

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

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

336 
[] => [] 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

337 
 [(_, S)] => 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

338 
if Sign.subsort sign ([class], S) then S 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

340 
 _ => err_bad_tfrees name); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

341 

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

342 
val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms)); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

343 

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

344 
val int_axm = close_form o map_term_tfrees (K (aT axS)); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

345 
fun inclass c = mk_inclass (aT axS, c); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

346 

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

347 
val intro_axm = list_implies 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

348 
(map inclass super_classes @ map (int_axm o snd) axioms, inclass class); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

350 
add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

352 

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

353 

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

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

355 

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

356 
val add_axclass = ext_axclass read_axm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

357 
val add_axclass_i = ext_axclass cert_axm; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

358 

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

359 

423  360 
(* add signature classes *) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

361 

423  362 
fun ext_sigclass add_cnsts (class, super_classes) consts old_thy = 
363 
old_thy 

364 
> add_axclass (class, super_classes) [] 

365 
> add_defsort [class] 

366 
> add_cnsts consts 

367 
> add_defsort (Type.defaultS (#tsig (Sign.rep_sg (sign_of old_thy)))); 

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

368 

423  369 
val add_sigclass = ext_sigclass add_consts; 
370 
val add_sigclass_i = ext_sigclass add_consts_i; 

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

371 

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

372 

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

373 

423  374 
(** prove class relations and type arities **) 
375 

376 
(* class_axms *) 

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

377 

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

378 
fun class_axms thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

380 
val classes = Sign.classes (sign_of thy); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

381 
val intros = map (fn c => c ^ "I") classes; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

383 
get_axioms thy intros @ 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

384 
map (class_triv thy) classes 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

386 

423  387 

388 
(* axclass_tac *) 

389 

487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset

390 
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", 
423  391 
try "cI" axioms first and use class_triv as last resort 
392 
(2) rewrite goals using user supplied definitions 

393 
(3) repeatedly resolve goals with user supplied nondefinitions*) 

394 

395 
fun axclass_tac thy thms = 

396 
TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN 

397 
TRY (rewrite_goals_tac (filter is_defn thms)) THEN 

398 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))); 

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

399 

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

400 

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

402 

423  403 
fun prove term_of str_of thy sig_prop thms usr_tac = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

405 
val sign = sign_of thy; 
423  406 
val goal = cterm_of sign (term_of sig_prop); 
407 
val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac); 

408 
in 

409 
prove_goalw_cterm [] goal (K [tac]) 

410 
end 

411 
handle ERROR => error ("The error(s) above occurred while trying to prove " 

412 
^ quote (str_of sig_prop)); 

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

413 

423  414 
val prove_classrel = 
415 
prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2); 

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

416 

423  417 
val prove_arity = 
418 
prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c])); 

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

419 

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

420 

423  421 
(* make goals (for interactive use) *) 
422 

423 
fun mk_goal term_of thy sig_prop = 

424 
goalw_cterm [] (cterm_of (sign_of thy) (term_of sig_prop)); 

425 

426 
val goal_subclass = mk_goal mk_classrel; 

427 
val goal_arity = mk_goal mk_arity; 

428 

429 

430 

449  431 
(** add proved subclass relations and arities **) 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

432 

449  433 
fun add_inst_subclass (c1, c2) axms thms usr_tac thy = 
423  434 
add_classrel_thms 
435 
[prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy; 

436 

449  437 
fun add_inst_arity (t, ss, cs) axms thms usr_tac thy = 
423  438 
let 
439 
val usr_thms = get_axioms thy axms @ thms; 

440 
fun prove c = 

441 
prove_arity thy (t, ss, c) usr_thms usr_tac; 

442 
in 

443 
add_arity_thms (map prove cs) thy 

444 
end; 

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

445 

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

446 

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

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

448 