author  wenzelm 
Thu, 26 May 1994 16:53:58 +0200  
changeset 404  dd3d3d6467db 
child 423  a42892e72854 
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 

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

5 
User interface for axiomatic type classes. 
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 
TODO: 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

8 
arity_tac: FILTER is_arity (?), assume_tac (?) (no?) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

10 

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

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

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

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

14 
local open Tactical Tactical.Thm in 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

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

19 
val add_instance: string * sort list * class > string list > thm list 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

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

24 

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

25 
functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

26 
sharing Goals.Tactical = Tactic.Tactical)(*: AX_CLASS *) = (* FIXME *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

28 

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

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

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

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

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

33 

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

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

35 

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

36 

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

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

38 

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

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

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

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

42 

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

43 
fun str_of_sort [c] = c 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

44 
 str_of_sort cs = parents "{" "}" (commas cs); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

45 

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

46 
fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom)); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

47 

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

48 
fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

49 
 str_of_arity (t, SS, S) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

50 
t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

51 
end; 
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 

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

54 
(** add constant definitions **) (* FIXME > drule.ML (?) *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

55 

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

56 
(* FIXME fake! *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

59 

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

60 

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

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

62 

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

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

64 

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

65 
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

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

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

68 

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

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

70 

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

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

72 

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

73 

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

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

75 

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

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

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

78 

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

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

80 

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

81 

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

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

83 

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

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

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

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

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

88 

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

89 

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

90 

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

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

92 

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

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

94 

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

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

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

97 

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

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

99 
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

100 

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

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

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

103 

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

104 

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

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

106 

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

107 
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

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

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

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

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

112 

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

113 

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

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

115 

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

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

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

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

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

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

121 

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

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

123 

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

124 

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

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

126 

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

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

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

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

130 

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

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

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

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

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

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

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

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

138 

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

139 
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

140 

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

141 
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

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

143 

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

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

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

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

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

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

149 

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

150 

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

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

152 

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

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

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

155 

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

156 

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

157 

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

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

159 

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

160 
(* arities as terms *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

161 

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

162 
fun mk_arity (t, ss, c) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

164 
val names = variantlist (replicate (length ss) "'a", []); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

165 
val tvars = map (fn a => TVar ((a, 0), logicS)) names; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

167 
mk_inclass (Type (t, tvars), c) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

168 
end; 
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 
fun dest_arity tm = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

172 
fun err () = raise_term "dest_arity" [tm]; 
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 
val (ty, c) = dest_inclass tm handle TERM _ => err (); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

175 
val (t, tvars) = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

177 
Type (t, tys) => (t, map (fn TVar x => x  _ => err ()) tys) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

180 
if null (gen_duplicates eq_fst tvars) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

181 
then map snd tvars else err (); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

183 
(t, ss, c) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

185 

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 
(* axclass_tac *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

188 

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

189 
(*repeatedly resolve subgoals of form "( ty : c_class )"; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

190 
try "cI" axioms first and use class_triv as last resort*) 
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 
fun class_axms thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

199 
end; 
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 
fun axclass_tac thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

202 
REPEAT_FIRST (resolve_tac (class_axms thy)); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

203 

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

204 

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

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

206 

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

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

208 
(* FIXME state sign vs sign (!?) *) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

209 
fun weaker_arity state = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

210 
all_subsort (ss, #2 (dest_arity (concl_of state))) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

213 

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

214 
fun prove_arity thy (arity as (t, ss, c)) thms usr_tac = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

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

217 
val all_subsort = forall2 (Sign.subsort sign); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

218 

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

219 
val arity_goal = cterm_of sign (mk_arity arity); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

220 

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

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

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

223 
TRY (rewrite_goals_tac (filter is_defn thms)) THEN 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

224 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))) THEN 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

226 

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

227 
val arity_thm = prove_goalw_cterm [] arity_goal (K [arity_tac]); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

228 

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

229 
val (t', ss', c') = dest_arity (#prop (rep_thm arity_thm)) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

230 
handle TERM _ => error "Result is not an arity"; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

232 
if t = t' andalso all_subsort (ss, ss') andalso c = c' then () 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

233 
else error ("Proved different arity: " ^ Type.str_of_arity (t', ss', [c'])) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

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

235 
handle ERROR => error ("The error(s) above occurred while trying to prove: " ^ 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

236 
Type.str_of_arity (t, ss, [c])); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

237 

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

238 

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

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

240 

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

241 
fun add_instance (t, ss, c) axms thms usr_tac thy = 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

242 
(prove_arity thy (t, ss, c) (get_axioms thy axms @ thms) usr_tac; 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

243 
add_arities [(t, ss, [c])] thy); 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

244 

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

245 

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

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

247 