author | paulson |
Tue, 18 Jun 1996 16:38:48 +0200 | |
changeset 1816 | b03dba9116d4 |
parent 1735 | 96244c247b07 |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
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 |
* user-specified 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 (non-conjunctive) 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 SU = (** Description of a disjoint sum **) |
516 | 39 |
sig |
1461 | 40 |
val sum : term (*disjoint sum operator*) |
41 |
val inl : term (*left injection*) |
|
42 |
val inr : term (*right injection*) |
|
43 |
val elim : term (*case operator*) |
|
44 |
val case_inl : thm (*inl equality rule for case*) |
|
45 |
val case_inr : thm (*inr equality rule for case*) |
|
46 |
val inl_iff : thm (*injectivity of inl, using <->*) |
|
47 |
val inr_iff : thm (*injectivity of inr, using <->*) |
|
48 |
val distinct : thm (*distinctness of inl, inr using <->*) |
|
49 |
val distinct' : thm (*distinctness of inr, inl using <->*) |
|
50 |
val free_SEs : thm list (*elim rules for SU, and pair_iff!*) |
|
516 | 51 |
end; |
52 |
||
53 |
signature ADD_INDUCTIVE_DEF = |
|
54 |
sig |
|
727
711e4eb8c213
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
612
diff
changeset
|
55 |
val add_fp_def_i : term list * term * term list -> theory -> theory |
516 | 56 |
val add_constructs_def : |
57 |
string list * ((string*typ*mixfix) * |
|
58 |
string * term list * term list) list list -> |
|
59 |
theory -> theory |
|
60 |
end; |
|
61 |
||
62 |
||
63 |
||
64 |
(*Declares functions to add fixedpoint/constructor defs to a theory*) |
|
65 |
functor Add_inductive_def_Fun |
|
1735 | 66 |
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU) |
67 |
: ADD_INDUCTIVE_DEF = |
|
516 | 68 |
struct |
69 |
open Logic Ind_Syntax; |
|
70 |
||
71 |
(*internal version*) |
|
727
711e4eb8c213
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
612
diff
changeset
|
72 |
fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = |
516 | 73 |
let |
74 |
val sign = sign_of thy; |
|
75 |
||
76 |
(*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
|
77 |
val rec_hds = map head_of rec_tms; |
516 | 78 |
|
750
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset
|
79 |
val _ = assert_all is_Const rec_hds |
1461 | 80 |
(fn t => "Recursive set not previously declared as constant: " ^ |
81 |
Sign.string_of_term sign t); |
|
750
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset
|
82 |
|
019aadf0e315
checks that the recursive sets are Consts before taking
lcp
parents:
727
diff
changeset
|
83 |
(*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
|
84 |
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
|
85 |
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
516 | 86 |
|
87 |
val _ = assert_all Syntax.is_identifier rec_names |
|
88 |
(fn a => "Name of recursive set not an identifier: " ^ a); |
|
89 |
||
90 |
local (*Checking the introduction rules*) |
|
91 |
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
|
92 |
fun intr_ok set = |
|
1461 | 93 |
case head_of set of Const(a,recT) => a mem rec_names | _ => false; |
516 | 94 |
in |
95 |
val _ = assert_all intr_ok intr_sets |
|
1461 | 96 |
(fn t => "Conclusion of rule does not name a recursive set: " ^ |
97 |
Sign.string_of_term sign t); |
|
516 | 98 |
end; |
99 |
||
100 |
val _ = assert_all is_Free rec_params |
|
1461 | 101 |
(fn t => "Param in recursion term not a free variable: " ^ |
102 |
Sign.string_of_term sign t); |
|
516 | 103 |
|
104 |
(*** Construct the lfp definition ***) |
|
105 |
val mk_variant = variant (foldr add_term_names (intr_tms,[])); |
|
106 |
||
107 |
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; |
|
108 |
||
109 |
fun dest_tprop (Const("Trueprop",_) $ P) = P |
|
110 |
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |
|
1461 | 111 |
Sign.string_of_term sign Q); |
516 | 112 |
|
113 |
(*Makes a disjunct from an introduction rule*) |
|
114 |
fun lfp_part intr = (*quantify over rule's free vars except parameters*) |
|
115 |
let val prems = map dest_tprop (strip_imp_prems intr) |
|
1461 | 116 |
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds |
117 |
val exfrees = term_frees intr \\ rec_params |
|
118 |
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr)) |
|
516 | 119 |
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; |
120 |
||
121 |
(*The Part(A,h) terms -- compose injections to make h*) |
|
1461 | 122 |
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) |
516 | 123 |
| mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); |
124 |
||
125 |
(*Access to balanced disjoint sums via injections*) |
|
126 |
val parts = |
|
1461 | 127 |
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) |
128 |
(length rec_tms)); |
|
516 | 129 |
|
130 |
(*replace each set by the corresponding Part(A,h)*) |
|
131 |
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; |
|
132 |
||
133 |
val lfp_abs = absfree(X', iT, |
|
1461 | 134 |
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs)); |
516 | 135 |
|
136 |
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs |
|
137 |
||
138 |
val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) |
|
1461 | 139 |
"Illegal occurrence of recursion operator") |
140 |
rec_hds; |
|
516 | 141 |
|
142 |
(*** Make the new theory ***) |
|
143 |
||
144 |
(*A key definition: |
|
145 |
If no mutual recursion then it equals the one recursive set. |
|
146 |
If mutual recursion then it differs from all the recursive sets. *) |
|
147 |
val big_rec_name = space_implode "_" rec_names; |
|
148 |
||
149 |
(*Big_rec... is the union of the mutually recursive sets*) |
|
150 |
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); |
|
151 |
||
152 |
(*The individual sets must already be declared*) |
|
153 |
val axpairs = map mk_defpair |
|
1461 | 154 |
((big_rec_tm, lfp_rhs) :: |
155 |
(case parts of |
|
156 |
[_] => [] (*no mutual recursion*) |
|
157 |
| _ => rec_tms ~~ (*define the sets as Parts*) |
|
158 |
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); |
|
516 | 159 |
|
591
5a6b0ed377cb
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp
parents:
567
diff
changeset
|
160 |
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
|
161 |
|
567 | 162 |
in thy |> add_defs_i axpairs end |
516 | 163 |
|
164 |
||
165 |
(*Expects the recursive sets to have been defined already. |
|
166 |
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) |
|
167 |
fun add_constructs_def (rec_names, con_ty_lists) thy = |
|
168 |
let |
|
169 |
val _ = writeln" Defining the constructor functions..."; |
|
1461 | 170 |
val case_name = "f"; (*name for case variables*) |
516 | 171 |
|
172 |
(** Define the constructors **) |
|
173 |
||
174 |
(*The empty tuple is 0*) |
|
175 |
fun mk_tuple [] = Const("0",iT) |
|
176 |
| mk_tuple args = foldr1 (app Pr.pair) args; |
|
177 |
||
178 |
fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k; |
|
179 |
||
1461 | 180 |
val npart = length rec_names; (*total # of mutually recursive parts*) |
516 | 181 |
|
182 |
(*Make constructor definition; kpart is # of this mutually recursive part*) |
|
183 |
fun mk_con_defs (kpart, con_ty_list) = |
|
1461 | 184 |
let val ncon = length con_ty_list (*number of constructors*) |
185 |
fun mk_def (((id,T,syn), name, args, prems), kcon) = |
|
186 |
(*kcon is index of constructor*) |
|
187 |
mk_defpair (list_comb (Const(name,T), args), |
|
188 |
mk_inject npart kpart |
|
189 |
(mk_inject ncon kcon (mk_tuple args))) |
|
516 | 190 |
in map mk_def (con_ty_list ~~ (1 upto ncon)) end; |
191 |
||
192 |
(** Define the case operator **) |
|
193 |
||
194 |
(*Combine split terms using case; yields the case operator for one part*) |
|
195 |
fun call_case case_list = |
|
1735 | 196 |
let fun call_f (free,[]) = Abs("null", iT, free) |
197 |
| call_f (free,args) = |
|
198 |
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) |
|
199 |
Ind_Syntax.iT |
|
200 |
free |
|
516 | 201 |
in fold_bal (app Su.elim) (map call_f case_list) end; |
202 |
||
203 |
(** Generating function variables for the case definition |
|
1461 | 204 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
516 | 205 |
|
206 |
(*Treatment of a single constructor*) |
|
207 |
fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = |
|
1461 | 208 |
if Syntax.is_identifier id |
209 |
then (opno, |
|
210 |
(Free(case_name ^ "_" ^ id, T), args) :: cases) |
|
211 |
else (opno+1, |
|
212 |
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: |
|
213 |
cases) |
|
516 | 214 |
|
215 |
(*Treatment of a list of constructors, for one part*) |
|
216 |
fun add_case_list (con_ty_list, (opno,case_lists)) = |
|
1461 | 217 |
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) |
218 |
in (opno', case_list :: case_lists) end; |
|
516 | 219 |
|
220 |
(*Treatment of all parts*) |
|
221 |
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); |
|
222 |
||
223 |
val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT); |
|
224 |
||
225 |
val big_rec_name = space_implode "_" rec_names; |
|
226 |
||
227 |
val big_case_name = big_rec_name ^ "_case"; |
|
228 |
||
229 |
(*The list of all the function variables*) |
|
230 |
val big_case_args = flat (map (map #1) case_lists); |
|
231 |
||
232 |
val big_case_tm = |
|
1461 | 233 |
list_comb (Const(big_case_name, big_case_typ), big_case_args); |
516 | 234 |
|
235 |
val big_case_def = mk_defpair |
|
1461 | 236 |
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); |
516 | 237 |
|
238 |
(** Build the new theory **) |
|
239 |
||
240 |
val const_decs = |
|
1461 | 241 |
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); |
516 | 242 |
|
243 |
val axpairs = |
|
1461 | 244 |
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) |
516 | 245 |
|
567 | 246 |
in thy |> add_consts_i const_decs |> add_defs_i axpairs end; |
516 | 247 |
end; |