--- a/src/ZF/intr_elim.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/intr_elim.ML Fri Aug 12 12:51:34 1994 +0200
@@ -1,83 +1,31 @@
(* Title: ZF/intr-elim.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Introduction/elimination rule module -- for Inductive/Coinductive Definitions
-
-Features:
-* least or greatest fixedpoints
-* user-specified product and sum constructions
-* mutually recursive definitions
-* definitions involving arbitrary monotone operators
-* automatically proves introduction and elimination rules
-
-The recursive sets must *already* be declared as constants in parent theory!
-
- Introduction rules have the form
- [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
- where M is some monotone operator (usually the identity)
- P(x) is any (non-conjunctive) side condition on the free variables
- ti, t are any terms
- Sj, Sk are two of the sets being defined in mutual recursion
-
-Sums are used only for mutual recursion;
-Products are used only to derive "streamlined" induction rules for relations
*)
-signature FP = (** Description of a fixed point operator **)
- sig
- val oper : term (*fixed point operator*)
- val bnd_mono : term (*monotonicity predicate*)
- val bnd_monoI : thm (*intro rule for bnd_mono*)
- val subs : thm (*subset theorem for fp*)
- val Tarski : thm (*Tarski's fixed point theorem*)
- val induct : thm (*induction/coinduction rule*)
- end;
-
-signature PR = (** Description of a Cartesian product **)
+signature INDUCTIVE_ARG = (** Description of a (co)inductive def **)
sig
- val sigma : term (*Cartesian product operator*)
- val pair : term (*pairing operator*)
- val split_const : term (*splitting operator*)
- val fsplit_const : term (*splitting operator for formulae*)
- val pair_iff : thm (*injectivity of pairing, using <->*)
- val split_eq : thm (*equality rule for split*)
- val fsplitI : thm (*intro rule for fsplit*)
- val fsplitD : thm (*destruct rule for fsplit*)
- val fsplitE : thm (*elim rule for fsplit*)
- end;
-
-signature SU = (** Description of a disjoint sum **)
- sig
- val sum : term (*disjoint sum operator*)
- val inl : term (*left injection*)
- val inr : term (*right injection*)
- val elim : term (*case operator*)
- val case_inl : thm (*inl equality rule for case*)
- val case_inr : thm (*inr equality rule for case*)
- val inl_iff : thm (*injectivity of inl, using <->*)
- val inr_iff : thm (*injectivity of inr, using <->*)
- val distinct : thm (*distinctness of inl, inr using <->*)
- val distinct' : thm (*distinctness of inr, inl using <->*)
- end;
-
-signature INDUCTIVE = (** Description of a (co)inductive defn **)
- sig
- val thy : theory (*parent theory*)
- val thy_name : string (*name of generated theory*)
- val rec_doms : (string*string) list (*recursion ops and their domains*)
- val sintrs : string list (*desired introduction rules*)
+ val thy : theory (*new theory with inductive defs*)
val monos : thm list (*monotonicity of each M operator*)
val con_defs : thm list (*definitions of the constructors*)
val type_intrs : thm list (*type-checking intro rules*)
val type_elims : thm list (*type-checking elim rules*)
end;
+(*internal items*)
+signature INDUCTIVE_I =
+ sig
+ val rec_tms : term list (*the recursive sets*)
+ val domts : term list (*their domains*)
+ val intr_tms : term list (*terms for the introduction rules*)
+ end;
+
signature INTR_ELIM =
sig
- val thy : theory (*new theory*)
- val thy_name : string (*name of generated theory*)
+ val thy : theory (*copy of input theory*)
val defs : thm list (*definitions made in thy*)
val bnd_mono : thm (*monotonicity for the lfp definition*)
val unfold : thm (*fixed-point equation*)
@@ -86,145 +34,36 @@
val elim : thm (*case analysis theorem*)
val raw_induct : thm (*raw induction rule from Fp.induct*)
val mk_cases : thm list -> string -> thm (*generates case theorems*)
- (*internal items...*)
- val big_rec_tm : term (*the lhs of the fixedpoint defn*)
- val rec_tms : term list (*the mutually recursive sets*)
- val domts : term list (*domains of the recursive sets*)
- val intr_tms : term list (*terms for the introduction rules*)
- val rec_params : term list (*parameters of the recursion*)
+ val rec_names : string list (*names of recursive sets*)
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*)
end;
-
-functor Intr_elim_Fun (structure Ind: INDUCTIVE and
- Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
+(*prove intr/elim rules for a fixedpoint definition*)
+functor Intr_elim_Fun
+ (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
+ and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
struct
-open Logic Ind;
-
-(*** Extract basic information from arguments ***)
-
-val sign = sign_of Ind.thy;
-
-fun rd T a =
- read_cterm sign (a,T)
- handle ERROR => error ("The error above occurred for " ^ a);
-
-val rec_names = map #1 rec_doms
-and domts = map (term_of o rd iT o #2) rec_doms;
-
-val dummy = assert_all Syntax.is_identifier rec_names
- (fn a => "Name of recursive set not an identifier: " ^ a);
-
-val dummy = assert_all (is_some o lookup_const sign) rec_names
- (fn a => "Name of recursive set not declared as constant: " ^ a);
-
-val intr_tms = map (term_of o rd propT) sintrs;
-
-local (*Checking the introduction rules*)
- val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
-
- fun intr_ok set =
- case head_of set of Const(a,recT) => a mem rec_names | _ => false;
-
- val dummy = assert_all intr_ok intr_sets
- (fn t => "Conclusion of rule does not name a recursive set: " ^
- Sign.string_of_term sign t);
-in
-val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
-end;
-
-val rec_hds = map (fn a=> Const(a,recT)) rec_names;
-val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
-
-val dummy = assert_all is_Free rec_params
- (fn t => "Param in recursion term not a free variable: " ^
- Sign.string_of_term sign t);
-
-(*** Construct the lfp definition ***)
-
-val mk_variant = variant (foldr add_term_names (intr_tms,[]));
+open Logic Inductive Ind_Syntax;
-val z' = mk_variant"z"
-and X' = mk_variant"X"
-and w' = mk_variant"w";
-
-(*simple error-checking in the premises*)
-fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
- error"Premises may not be conjuctive"
- | chk_prem rec_hd (Const("op :",_) $ t $ X) =
- deny (rec_hd occs t) "Recursion term on left of member symbol"
- | chk_prem rec_hd t =
- deny (rec_hd occs t) "Recursion term in side formula";
-
-fun dest_tprop (Const("Trueprop",_) $ P) = P
- | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
- Sign.string_of_term sign Q);
-
-(*Makes a disjunct from an introduction rule*)
-fun lfp_part intr = (*quantify over rule's free vars except parameters*)
- let val prems = map dest_tprop (strip_imp_prems intr)
- val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
- val exfrees = term_frees intr \\ rec_params
- val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
- in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
-
-val dom_sum = fold_bal (app Su.sum) domts;
-
-(*The Part(A,h) terms -- compose injections to make h*)
-fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
- | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
-
-(*Access to balanced disjoint sums via injections*)
-val parts =
- map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
- (length rec_doms));
-
-(*replace each set by the corresponding Part(A,h)*)
-val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
-
-val lfp_abs = absfree(X', iT,
- mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
-
-val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
-
-val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
- "Illegal occurrence of recursion operator")
- rec_hds;
-
-(*** Make the new theory ***)
-
-(*A key definition:
- If no mutual recursion then it equals the one recursive set.
- If mutual recursion then it differs from all the recursive sets. *)
+val rec_names = map (#1 o dest_Const o head_of) rec_tms;
val big_rec_name = space_implode "_" rec_names;
-(*Big_rec... is the union of the mutually recursive sets*)
-val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
-
-(*The individual sets must already be declared*)
-val axpairs = map (mk_defpair sign)
- ((big_rec_tm, lfp_rhs) ::
- (case parts of
- [_] => [] (*no mutual recursion*)
- | _ => rec_tms ~~ (*define the sets as Parts*)
- map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
+(*fetch fp definitions from the theory*)
+val big_rec_def::part_rec_defs =
+ map (get_def thy)
+ (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
-val thy =
- Ind.thy
- |> add_axioms_i axpairs
- |> add_thyname thy_name;
-val defs = map (get_axiom thy o #1) axpairs;
-
-val big_rec_def::part_rec_defs = defs;
-
-val prove = prove_term (sign_of thy);
+val sign = sign_of thy;
(********)
-val dummy = writeln "Proving monotonicity...";
+val _ = writeln " Proving monotonicity...";
+
+val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
+ big_rec_def |> rep_thm |> #prop |> unvarify;
val bnd_mono =
- prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs),
+ prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs),
fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ monos) 1)]);
@@ -234,7 +73,7 @@
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
(********)
-val dummy = writeln "Proving the introduction rules...";
+val _ = writeln " Proving the introduction rules...";
(*Mutual recursion: Needs subset rules for the individual sets???*)
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
@@ -252,22 +91,22 @@
rewrite_goals_tac con_defs,
(*Now can solve the trivial equation*)
REPEAT (rtac refl 2),
- REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
- ORELSE' hyp_subst_tac
- ORELSE' dresolve_tac rec_typechecks)),
+ REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
+ ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
+ ORELSE' hyp_subst_tac)),
DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
val mk_disj_rls =
let fun f rl = rl RS disjI1
- and g rl = rl RS disjI2
+ and g rl = rl RS disjI2
in accesses_bal(f, g, asm_rl) end;
-val intrs = map (prove part_rec_defs)
+val intrs = map (prove_term sign part_rec_defs)
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
(********)
-val dummy = writeln "Proving the elimination rule...";
+val _ = writeln " Proving the elimination rule...";
(*Includes rules for succ and Pair since they are common constructions*)
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
@@ -276,13 +115,13 @@
val sumprod_free_SEs =
map (gen_make_elim [conjE,FalseE])
- ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
+ ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
RL [iffD1]);
(*Breaks down logical connectives in the monotonic function*)
val basic_elim_tac =
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
- ORELSE' bound_hyp_subst_tac))
+ ORELSE' bound_hyp_subst_tac))
THEN prune_params_tac;
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
@@ -301,5 +140,5 @@
val defs = big_rec_def::part_rec_defs;
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
+end;
-end;