author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1735  96244c247b07 
permissions  rwrr 
1461  1 
(* Title: ZF/add_ind_def.ML 
516  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
516  4 
Copyright 1994 University of Cambridge 
5 

6 
Fixedpoint definition module  for Inductive/Coinductive Definitions 

7 

8 
Features: 

9 
* least or greatest fixedpoints 

10 
* userspecified product and sum constructions 

11 
* mutually recursive definitions 

12 
* definitions involving arbitrary monotone operators 

13 
* automatically proves introduction and elimination rules 

14 

15 
The recursive sets must *already* be declared as constants in parent theory! 

16 

17 
Introduction rules have the form 

18 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ] 

19 
where M is some monotone operator (usually the identity) 

20 
P(x) is any (nonconjunctive) side condition on the free variables 

21 
ti, t are any terms 

22 
Sj, Sk are two of the sets being defined in mutual recursion 

23 

24 
Sums are used only for mutual recursion; 

25 
Products are used only to derive "streamlined" induction rules for relations 

26 
*) 

27 

1461  28 
signature FP = (** Description of a fixed point operator **) 
516  29 
sig 
1461  30 
val oper : term (*fixed point operator*) 
31 
val bnd_mono : term (*monotonicity predicate*) 

32 
val bnd_monoI : thm (*intro rule for bnd_mono*) 

33 
val subs : thm (*subset theorem for fp*) 

34 
val Tarski : thm (*Tarski's fixed point theorem*) 

35 
val induct : thm (*induction/coinduction rule*) 

516  36 
end; 
37 

1461  38 
signature PR = (** Description of a Cartesian product **) 
516  39 
sig 
1461  40 
val sigma : term (*Cartesian product operator*) 
41 
val pair : term (*pairing operator*) 

42 
val split_const : term (*splitting operator*) 

43 
val fsplit_const : term (*splitting operator for formulae*) 

44 
val pair_iff : thm (*injectivity of pairing, using <>*) 

45 
val split_eq : thm (*equality rule for split*) 

46 
val fsplitI : thm (*intro rule for fsplit*) 

47 
val fsplitD : thm (*destruct rule for fsplit*) 

48 
val fsplitE : thm (*elim rule; apparently never used*) 

516  49 
end; 
50 

1461  51 
signature SU = (** Description of a disjoint sum **) 
516  52 
sig 
1461  53 
val sum : term (*disjoint sum operator*) 
54 
val inl : term (*left injection*) 

55 
val inr : term (*right injection*) 

56 
val elim : term (*case operator*) 

57 
val case_inl : thm (*inl equality rule for case*) 

58 
val case_inr : thm (*inr equality rule for case*) 

59 
val inl_iff : thm (*injectivity of inl, using <>*) 

60 
val inr_iff : thm (*injectivity of inr, using <>*) 

61 
val distinct : thm (*distinctness of inl, inr using <>*) 

62 
val distinct' : thm (*distinctness of inr, inl using <>*) 

63 
val free_SEs : thm list (*elim rules for SU, and pair_iff!*) 

516  64 
end; 
65 

66 
signature ADD_INDUCTIVE_DEF = 

67 
sig 

727
711e4eb8c213
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
612
diff
changeset

68 
val add_fp_def_i : term list * term * term list > theory > theory 
516  69 
val add_constructs_def : 
70 
string list * ((string*typ*mixfix) * 

71 
string * term list * term list) list list > 

72 
theory > theory 

73 
end; 

74 

75 

76 

77 
(*Declares functions to add fixedpoint/constructor defs to a theory*) 

78 
functor Add_inductive_def_Fun 

79 
(structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF = 

80 
struct 

81 
open Logic Ind_Syntax; 

82 

83 
(*internal version*) 

727
711e4eb8c213
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
612
diff
changeset

84 
fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
516  85 
let 
86 
val sign = sign_of thy; 

87 

88 
(*recT and rec_params should agree for all mutually recursive components*) 

750
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

89 
val rec_hds = map head_of rec_tms; 
516  90 

750
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

91 
val _ = assert_all is_Const rec_hds 
1461  92 
(fn t => "Recursive set not previously declared as constant: " ^ 
93 
Sign.string_of_term sign t); 

750
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

94 

019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

95 
(*Now we know they are all Consts, so get their names, type and params*) 
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

96 
val rec_names = map (#1 o dest_Const) rec_hds 
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset

97 
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); 
516  98 

99 
val _ = assert_all Syntax.is_identifier rec_names 

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

101 

102 
local (*Checking the introduction rules*) 

103 
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; 

104 
fun intr_ok set = 

1461  105 
case head_of set of Const(a,recT) => a mem rec_names  _ => false; 
516  106 
in 
107 
val _ = assert_all intr_ok intr_sets 

1461  108 
(fn t => "Conclusion of rule does not name a recursive set: " ^ 
109 
Sign.string_of_term sign t); 

516  110 
end; 
111 

112 
val _ = assert_all is_Free rec_params 

1461  113 
(fn t => "Param in recursion term not a free variable: " ^ 
114 
Sign.string_of_term sign t); 

516  115 

116 
(*** Construct the lfp definition ***) 

117 
val mk_variant = variant (foldr add_term_names (intr_tms,[])); 

118 

119 
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; 

120 

121 
fun dest_tprop (Const("Trueprop",_) $ P) = P 

122 
 dest_tprop Q = error ("Illformed premise of introduction rule: " ^ 

1461  123 
Sign.string_of_term sign Q); 
516  124 

125 
(*Makes a disjunct from an introduction rule*) 

126 
fun lfp_part intr = (*quantify over rule's free vars except parameters*) 

127 
let val prems = map dest_tprop (strip_imp_prems intr) 

1461  128 
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds 
129 
val exfrees = term_frees intr \\ rec_params 

130 
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr)) 

516  131 
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; 
132 

133 
(*The Part(A,h) terms  compose injections to make h*) 

1461  134 
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) 
516  135 
 mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); 
136 

137 
(*Access to balanced disjoint sums via injections*) 

138 
val parts = 

1461  139 
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
140 
(length rec_tms)); 

516  141 

142 
(*replace each set by the corresponding Part(A,h)*) 

143 
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; 

144 

145 
val lfp_abs = absfree(X', iT, 

1461  146 
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs)); 
516  147 

148 
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs 

149 

150 
val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 

1461  151 
"Illegal occurrence of recursion operator") 
152 
rec_hds; 

516  153 

154 
(*** Make the new theory ***) 

155 

156 
(*A key definition: 

157 
If no mutual recursion then it equals the one recursive set. 

158 
If mutual recursion then it differs from all the recursive sets. *) 

159 
val big_rec_name = space_implode "_" rec_names; 

160 

161 
(*Big_rec... is the union of the mutually recursive sets*) 

162 
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); 

163 

164 
(*The individual sets must already be declared*) 

165 
val axpairs = map mk_defpair 

1461  166 
((big_rec_tm, lfp_rhs) :: 
167 
(case parts of 

168 
[_] => [] (*no mutual recursion*) 

169 
 _ => rec_tms ~~ (*define the sets as Parts*) 

170 
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); 

516  171 

591
5a6b0ed377cb
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp
parents:
567
diff
changeset

172 
val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs 
5a6b0ed377cb
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp
parents:
567
diff
changeset

173 

567  174 
in thy > add_defs_i axpairs end 
516  175 

176 

177 
(*Expects the recursive sets to have been defined already. 

178 
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) 

179 
fun add_constructs_def (rec_names, con_ty_lists) thy = 

180 
let 

181 
val _ = writeln" Defining the constructor functions..."; 

1461  182 
val case_name = "f"; (*name for case variables*) 
516  183 

184 
(** Define the constructors **) 

185 

186 
(*The empty tuple is 0*) 

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

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

189 

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

191 

1461  192 
val npart = length rec_names; (*total # of mutually recursive parts*) 
516  193 

194 
(*Make constructor definition; kpart is # of this mutually recursive part*) 

195 
fun mk_con_defs (kpart, con_ty_list) = 

1461  196 
let val ncon = length con_ty_list (*number of constructors*) 
197 
fun mk_def (((id,T,syn), name, args, prems), kcon) = 

198 
(*kcon is index of constructor*) 

199 
mk_defpair (list_comb (Const(name,T), args), 

200 
mk_inject npart kpart 

201 
(mk_inject ncon kcon (mk_tuple args))) 

516  202 
in map mk_def (con_ty_list ~~ (1 upto ncon)) end; 
203 

204 
(** Define the case operator **) 

205 

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

207 
fun call_case case_list = 

208 
let fun call_f (free,args) = 

1461  209 
ap_split Pr.split_const free (map (#2 o dest_Free) args) 
516  210 
in fold_bal (app Su.elim) (map call_f case_list) end; 
211 

212 
(** Generating function variables for the case definition 

1461  213 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 
516  214 

215 
(*Treatment of a single constructor*) 

216 
fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = 

1461  217 
if Syntax.is_identifier id 
218 
then (opno, 

219 
(Free(case_name ^ "_" ^ id, T), args) :: cases) 

220 
else (opno+1, 

221 
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 

222 
cases) 

516  223 

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

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

1461  226 
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) 
227 
in (opno', case_list :: case_lists) end; 

516  228 

229 
(*Treatment of all parts*) 

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

231 

232 
val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) > (iT>iT); 

233 

234 
val big_rec_name = space_implode "_" rec_names; 

235 

236 
val big_case_name = big_rec_name ^ "_case"; 

237 

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

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

240 

241 
val big_case_tm = 

1461  242 
list_comb (Const(big_case_name, big_case_typ), big_case_args); 
516  243 

244 
val big_case_def = mk_defpair 

1461  245 
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
516  246 

247 
(** Build the new theory **) 

248 

249 
val const_decs = 

1461  250 
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); 
516  251 

252 
val axpairs = 

1461  253 
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) 
516  254 

567  255 
in thy > add_consts_i const_decs > add_defs_i axpairs end; 
516  256 
end; 