author  nipkow 
Tue, 21 Dec 1993 16:38:45 +0100  
changeset 202  4e68398cdc06 
parent 6  8ce8c4d13d4d 
child 231  cb6a24451544 
permissions  rwrr 
0  1 
(* Title: ZF/constructor.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Constructor function module  for Datatype Definitions 

7 

8 
Defines constructors and a casestyle eliminator (no primitive recursion) 

9 

10 
Features: 

11 
* least or greatest fixedpoints 

12 
* userspecified product and sum constructions 

13 
* mutually recursive datatypes 

14 
* recursion over arbitrary monotone operators 

15 
* flexible: can derive any reasonable set of introduction rules 

16 
* automatically constructs a case analysis operator (but no recursion op) 

17 
* efficient treatment of large declarations (e.g. 60 constructors) 

18 
*) 

19 

20 
(** STILL NEEDS: some treatment of recursion **) 

21 

22 
signature CONSTRUCTOR = 

23 
sig 

24 
val thy : theory (*parent theory*) 

25 
val rec_specs : (string * string * (string list * string)list) list 

26 
(*recursion ops, types, domains, constructors*) 

27 
val rec_styp : string (*common type of all recursion ops*) 

28 
val ext : Syntax.sext option (*syntax extension for new theory*) 

29 
val sintrs : string list (*desired introduction rules*) 

30 
val monos : thm list (*monotonicity of each M operator*) 

31 
val type_intrs : thm list (*typechecking intro rules*) 

32 
val type_elims : thm list (*typechecking elim rules*) 

33 
end; 

34 

35 
signature CONSTRUCTOR_RESULT = 

36 
sig 

37 
val con_thy : theory (*theory defining the constructors*) 

38 
val con_defs : thm list (*definitions made in con_thy*) 

39 
val case_eqns : thm list (*equations for case operator*) 

40 
val free_iffs : thm list (*freeness rewrite rules*) 

41 
val free_SEs : thm list (*freeness destruct rules*) 

42 
val mk_free : string > thm (*makes freeness theorems*) 

43 
end; 

44 

45 

46 
functor Constructor_Fun (structure Const: CONSTRUCTOR and 

47 
Pr : PR and Su : SU) : CONSTRUCTOR_RESULT = 

48 
struct 

49 
open Logic Const; 

50 

51 
val dummy = writeln"Defining the constructor functions..."; 

52 

53 
val case_name = "f"; (*name for case variables*) 

54 

55 
(** Extract basic information from arguments **) 

56 

57 
val sign = sign_of thy; 

58 
val rdty = Sign.typ_of o Sign.read_ctyp sign; 

59 

60 
val rec_names = map #1 rec_specs; 

61 

62 
val dummy = assert_all Syntax.is_identifier rec_names 

63 
(fn a => "Name of recursive set not an identifier: " ^ a); 

64 

65 
(*Expands multiple constant declarations*) 

66 
fun pairtypes (cs,st) = map (rpair st) cs; 

67 

68 
(*Constructors with types and arguments*) 

69 
fun mk_con_ty_list cons_pairs = 

70 
let fun mk_con_ty (a,st) = 

71 
let val T = rdty st 

72 
val args = mk_frees "xa" (binder_types T) 

73 
in (a,T,args) end 

74 
in map mk_con_ty (flat (map pairtypes cons_pairs)) end; 

75 

76 
val con_ty_lists = map (mk_con_ty_list o #3) rec_specs; 

77 

78 
(** Define the constructors **) 

79 

80 
(*We identify 0 (the empty set) with the empty tuple*) 

81 
fun mk_tuple [] = Const("0",iT) 

82 
 mk_tuple args = foldr1 (app Pr.pair) args; 

83 

84 
fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k; 

85 

86 
val npart = length rec_names; (*number of mutually recursive parts*) 

87 

88 
(*Make constructor definition*) 

89 
fun mk_con_defs (kpart, con_ty_list) = 

90 
let val ncon = length con_ty_list (*number of constructors*) 

91 
fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*) 

92 
mk_defpair sign 

93 
(list_comb (Const(a,T), args), 

94 
mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args))) 

95 
in map mk_def (con_ty_list ~~ (1 upto ncon)) end; 

96 

97 
(** Define the case operator **) 

98 

99 
(*Combine split terms using case; yields the case operator for one part*) 

100 
fun call_case case_list = 

101 
let fun call_f (free,args) = 

102 
ap_split Pr.split_const free (map (#2 o dest_Free) args) 

103 
in fold_bal (app Su.elim) (map call_f case_list) end; 

104 

105 
(** Generating function variables for the case definition 

106 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

107 

108 
(*Treatment of a single constructor*) 

109 
fun add_case ((a,T,args), (opno,cases)) = 

110 
if Syntax.is_identifier a 

111 
then (opno, 

112 
(Free(case_name ^ "_" ^ a, T), args) :: cases) 

113 
else (opno+1, 

114 
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases); 

115 

116 
(*Treatment of a list of constructors, for one part*) 

117 
fun add_case_list (con_ty_list, (opno,case_lists)) = 

118 
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) 

119 
in (opno', case_list :: case_lists) end; 

120 

121 
(*Treatment of all parts*) 

122 
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); 

123 

124 
val big_case_typ = flat (map (map #2) con_ty_lists) > (iT>iT); 

125 

126 
val big_rec_name = space_implode "_" rec_names; 

127 

128 
val big_case_name = big_rec_name ^ "_case"; 

129 

130 
(*The list of all the function variables*) 

131 
val big_case_args = flat (map (map #1) case_lists); 

132 

133 
val big_case_tm = 

134 
list_comb (Const(big_case_name, big_case_typ), big_case_args); 

135 

136 
val big_case_def = 

137 
mk_defpair sign 

138 
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 

139 

140 
(** Build the new theory **) 

141 

142 
val axpairs = 

143 
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)); 

144 

145 
val const_decs = remove_mixfixes ext 

146 
(([big_case_name], flatten_typ sign big_case_typ) :: 

147 
(big_rec_name ins rec_names, rec_styp) :: 

148 
flat (map #3 rec_specs)); 

149 

150 
val con_thy = extend_theory thy (big_rec_name ^ "_Constructors") 

202
4e68398cdc06
added []field to extend_theory: no type abbreviations.
nipkow
parents:
6
diff
changeset

151 
([], [], [], [], [], const_decs, ext) axpairs; 
0  152 

153 
(*1st element is the case definition; others are the constructors*) 

154 
val con_defs = map (get_axiom con_thy o #1) axpairs; 

155 

156 
(** Prove the case theorem **) 

157 

158 
(*Each equation has the form 

159 
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) 

160 
fun mk_case_equation ((a,T,args), case_free) = 

161 
mk_tprop 

162 
(eq_const $ (big_case_tm $ (list_comb (Const(a,T), args))) 

163 
$ (list_comb (case_free, args))); 

164 

165 
val case_trans = hd con_defs RS def_trans; 

166 

167 
(*proves a single case equation*) 

168 
fun case_tacsf con_def _ = 

169 
[rewtac con_def, 

170 
rtac case_trans 1, 

171 
REPEAT (resolve_tac [refl, Pr.split_eq RS trans, 

172 
Su.case_inl RS trans, 

173 
Su.case_inr RS trans] 1)]; 

174 

175 
fun prove_case_equation (arg,con_def) = 

176 
prove_term (sign_of con_thy) [] 

177 
(mk_case_equation arg, case_tacsf con_def); 

178 

179 
val free_iffs = 

180 
map standard (con_defs RL [def_swap_iff]) @ 

181 
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]; 

182 

183 
val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]); 

184 

185 
val free_cs = ZF_cs addSEs free_SEs; 

186 

187 
(*Typical theorems have the form ~con1=con2, con1=con2==>False, 

188 
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <> x=y, etc. *) 

189 
fun mk_free s = 

190 
prove_goalw con_thy con_defs s 

191 
(fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]); 

192 

193 
val case_eqns = map prove_case_equation 

194 
(flat con_ty_lists ~~ big_case_args ~~ tl con_defs); 

195 

196 
end; 

197 

198 