0
|
1 |
(* Title: ZF/intr-elim.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Introduction/elimination rule 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 defiend 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 |
|
|
28 |
signature FP = (** Description of a fixed point operator **)
|
|
29 |
sig
|
|
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*)
|
|
36 |
end;
|
|
37 |
|
|
38 |
signature PR = (** Description of a Cartesian product **)
|
|
39 |
sig
|
|
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 for fsplit*)
|
|
49 |
end;
|
|
50 |
|
|
51 |
signature SU = (** Description of a disjoint sum **)
|
|
52 |
sig
|
|
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 |
end;
|
|
64 |
|
|
65 |
signature INDUCTIVE = (** Description of a (co)inductive defn **)
|
|
66 |
sig
|
|
67 |
val thy : theory (*parent theory*)
|
|
68 |
val rec_doms : (string*string) list (*recursion ops and their domains*)
|
|
69 |
val sintrs : string list (*desired introduction rules*)
|
|
70 |
val monos : thm list (*monotonicity of each M operator*)
|
|
71 |
val con_defs : thm list (*definitions of the constructors*)
|
|
72 |
val type_intrs : thm list (*type-checking intro rules*)
|
|
73 |
val type_elims : thm list (*type-checking elim rules*)
|
|
74 |
end;
|
|
75 |
|
|
76 |
signature INTR_ELIM =
|
|
77 |
sig
|
|
78 |
val thy : theory (*new theory*)
|
|
79 |
val defs : thm list (*definitions made in thy*)
|
|
80 |
val bnd_mono : thm (*monotonicity for the lfp definition*)
|
|
81 |
val unfold : thm (*fixed-point equation*)
|
|
82 |
val dom_subset : thm (*inclusion of recursive set in dom*)
|
|
83 |
val intrs : thm list (*introduction rules*)
|
|
84 |
val elim : thm (*case analysis theorem*)
|
|
85 |
val raw_induct : thm (*raw induction rule from Fp.induct*)
|
|
86 |
val mk_cases : thm list -> string -> thm (*generates case theorems*)
|
|
87 |
(*internal items...*)
|
|
88 |
val big_rec_tm : term (*the lhs of the fixedpoint defn*)
|
|
89 |
val rec_tms : term list (*the mutually recursive sets*)
|
|
90 |
val domts : term list (*domains of the recursive sets*)
|
|
91 |
val intr_tms : term list (*terms for the introduction rules*)
|
|
92 |
val rec_params : term list (*parameters of the recursion*)
|
|
93 |
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*)
|
|
94 |
end;
|
|
95 |
|
|
96 |
|
|
97 |
functor Intr_elim_Fun (structure Ind: INDUCTIVE and
|
|
98 |
Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
|
|
99 |
struct
|
|
100 |
open Logic Ind;
|
|
101 |
|
|
102 |
(*** Extract basic information from arguments ***)
|
|
103 |
|
|
104 |
val sign = sign_of Ind.thy;
|
|
105 |
|
|
106 |
fun rd T a =
|
|
107 |
Sign.read_cterm sign (a,T)
|
|
108 |
handle ERROR => error ("The error above occurred for " ^ a);
|
|
109 |
|
|
110 |
val rec_names = map #1 rec_doms
|
|
111 |
and domts = map (Sign.term_of o rd iT o #2) rec_doms;
|
|
112 |
|
|
113 |
val dummy = assert_all Syntax.is_identifier rec_names
|
|
114 |
(fn a => "Name of recursive set not an identifier: " ^ a);
|
|
115 |
|
|
116 |
val dummy = assert_all (is_some o lookup_const sign) rec_names
|
|
117 |
(fn a => "Name of recursive set not declared as constant: " ^ a);
|
|
118 |
|
|
119 |
val intr_tms = map (Sign.term_of o rd propT) sintrs;
|
|
120 |
val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
|
|
121 |
val rec_hds = map (fn a=> Const(a,recT)) rec_names;
|
|
122 |
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
|
|
123 |
|
|
124 |
val dummy = assert_all is_Free rec_params
|
|
125 |
(fn t => "Param in recursion term not a free variable: " ^
|
|
126 |
Sign.string_of_term sign t);
|
|
127 |
|
|
128 |
(*** Construct the lfp definition ***)
|
|
129 |
|
|
130 |
val mk_variant = variant (foldr add_term_names (intr_tms,[]));
|
|
131 |
|
|
132 |
val z' = mk_variant"z"
|
|
133 |
and X' = mk_variant"X"
|
|
134 |
and w' = mk_variant"w";
|
|
135 |
|
|
136 |
(*simple error-checking in the premises*)
|
|
137 |
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
|
|
138 |
error"Premises may not be conjuctive"
|
|
139 |
| chk_prem rec_hd (Const("op :",_) $ t $ X) =
|
|
140 |
deny (rec_hd occs t) "Recursion term on left of member symbol"
|
|
141 |
| chk_prem rec_hd t =
|
|
142 |
deny (rec_hd occs t) "Recursion term in side formula";
|
|
143 |
|
|
144 |
(*Makes a disjunct from an introduction rule*)
|
|
145 |
fun lfp_part intr = (*quantify over rule's free vars except parameters*)
|
|
146 |
let val prems = map dest_tprop (strip_imp_prems intr)
|
|
147 |
val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
|
|
148 |
val exfrees = term_frees intr \\ rec_params
|
|
149 |
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
|
|
150 |
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
|
|
151 |
|
|
152 |
val dom_sum = fold_bal (app Su.sum) domts;
|
|
153 |
|
|
154 |
(*The Part(A,h) terms -- compose injections to make h*)
|
|
155 |
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
|
|
156 |
| mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
|
|
157 |
|
|
158 |
(*Access to balanced disjoint sums via injections*)
|
|
159 |
val parts =
|
|
160 |
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
|
|
161 |
(length rec_doms));
|
|
162 |
|
|
163 |
(*replace each set by the corresponding Part(A,h)*)
|
|
164 |
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
|
|
165 |
|
|
166 |
val lfp_abs = absfree(X', iT,
|
|
167 |
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
|
|
168 |
|
|
169 |
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
|
|
170 |
|
|
171 |
val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
|
|
172 |
"Illegal occurrence of recursion operator")
|
|
173 |
rec_hds;
|
|
174 |
|
|
175 |
(*** Make the new theory ***)
|
|
176 |
|
|
177 |
(*A key definition:
|
|
178 |
If no mutual recursion then it equals the one recursive set.
|
|
179 |
If mutual recursion then it differs from all the recursive sets. *)
|
|
180 |
val big_rec_name = space_implode "_" rec_names;
|
|
181 |
|
|
182 |
(*Big_rec... is the union of the mutually recursive sets*)
|
|
183 |
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
|
|
184 |
|
|
185 |
(*The individual sets must already be declared*)
|
|
186 |
val axpairs = map (mk_defpair sign)
|
|
187 |
((big_rec_tm, lfp_rhs) ::
|
|
188 |
(case parts of
|
|
189 |
[_] => [] (*no mutual recursion*)
|
|
190 |
| _ => rec_tms ~~ (*define the sets as Parts*)
|
|
191 |
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
|
|
192 |
|
|
193 |
val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
|
|
194 |
([], [], [], [], [], None) axpairs;
|
|
195 |
|
|
196 |
val defs = map (get_axiom thy o #1) axpairs;
|
|
197 |
|
|
198 |
val big_rec_def::part_rec_defs = defs;
|
|
199 |
|
|
200 |
val prove = prove_term (sign_of thy);
|
|
201 |
|
|
202 |
(********)
|
|
203 |
val dummy = writeln "Proving monotonocity...";
|
|
204 |
|
|
205 |
val bnd_mono =
|
|
206 |
prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs),
|
|
207 |
fn _ =>
|
|
208 |
[rtac (Collect_subset RS bnd_monoI) 1,
|
|
209 |
REPEAT (ares_tac (basic_monos @ monos) 1)]);
|
|
210 |
|
|
211 |
val dom_subset = standard (big_rec_def RS Fp.subs);
|
|
212 |
|
|
213 |
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
|
|
214 |
|
|
215 |
(********)
|
|
216 |
val dummy = writeln "Proving the introduction rules...";
|
|
217 |
|
|
218 |
(*Mutual recursion: Needs subset rules for the individual sets???*)
|
|
219 |
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
|
|
220 |
|
|
221 |
(*Type-checking is hardest aspect of proof;
|
|
222 |
disjIn selects the correct disjunct after unfolding*)
|
|
223 |
fun intro_tacsf disjIn prems =
|
|
224 |
[(*insert prems and underlying sets*)
|
|
225 |
cut_facts_tac (prems @ (prems RL [PartD1])) 1,
|
|
226 |
rtac (unfold RS ssubst) 1,
|
|
227 |
REPEAT (resolve_tac [Part_eqI,CollectI] 1),
|
|
228 |
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
|
|
229 |
rtac disjIn 2,
|
|
230 |
REPEAT (ares_tac [refl,exI,conjI] 2),
|
|
231 |
rewrite_goals_tac con_defs,
|
|
232 |
(*Now can solve the trivial equation*)
|
|
233 |
REPEAT (rtac refl 2),
|
|
234 |
REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
|
|
235 |
ORELSE' dresolve_tac rec_typechecks)),
|
|
236 |
DEPTH_SOLVE (ares_tac type_intrs 1)];
|
|
237 |
|
|
238 |
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
|
|
239 |
val mk_disj_rls =
|
|
240 |
let fun f rl = rl RS disjI1
|
|
241 |
and g rl = rl RS disjI2
|
|
242 |
in accesses_bal(f, g, asm_rl) end;
|
|
243 |
|
|
244 |
val intrs = map (prove part_rec_defs)
|
|
245 |
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
|
|
246 |
|
|
247 |
(********)
|
|
248 |
val dummy = writeln "Proving the elimination rule...";
|
|
249 |
|
|
250 |
val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];
|
|
251 |
|
|
252 |
val sumprod_free_SEs =
|
|
253 |
map (gen_make_elim [conjE,FalseE])
|
|
254 |
([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
|
|
255 |
RL [iffD1]);
|
|
256 |
|
|
257 |
(*Breaks down logical connectives in the monotonic function*)
|
|
258 |
val basic_elim_tac =
|
|
259 |
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
|
|
260 |
ORELSE' bound_hyp_subst_tac))
|
|
261 |
THEN prune_params_tac;
|
|
262 |
|
|
263 |
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
|
|
264 |
|
|
265 |
(*Applies freeness of the given constructors.
|
|
266 |
NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
|
|
267 |
fun con_elim_tac defs =
|
|
268 |
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
|
|
269 |
|
|
270 |
(*String s should have the form t:Si where Si is an inductive set*)
|
|
271 |
fun mk_cases defs s =
|
|
272 |
rule_by_tactic (con_elim_tac defs)
|
|
273 |
(assume_read thy s RS elim);
|
|
274 |
|
|
275 |
val defs = big_rec_def::part_rec_defs;
|
|
276 |
|
|
277 |
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
|
|
278 |
|
|
279 |
end;
|