diff -r 000000000000 -r a5a9c433f639 src/ZF/intr-elim.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/intr-elim.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,279 @@ +(* Title: ZF/intr-elim.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 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 defiend 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 **) + 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 rec_doms : (string*string) list (*recursion ops and their domains*) + val sintrs : string list (*desired introduction rules*) + 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; + +signature INTR_ELIM = + sig + val thy : theory (*new theory*) + val defs : thm list (*definitions made in thy*) + val bnd_mono : thm (*monotonicity for the lfp definition*) + val unfold : thm (*fixed-point equation*) + val dom_subset : thm (*inclusion of recursive set in dom*) + val intrs : thm list (*introduction rules*) + 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 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 = +struct +open Logic Ind; + +(*** Extract basic information from arguments ***) + +val sign = sign_of Ind.thy; + +fun rd T a = + Sign.read_cterm sign (a,T) + handle ERROR => error ("The error above occurred for " ^ a); + +val rec_names = map #1 rec_doms +and domts = map (Sign.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 (Sign.term_of o rd propT) sintrs; +val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms))) +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,[])); + +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"; + +(*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 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)); + +val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive") + ([], [], [], [], [], None) axpairs; + +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 dummy = writeln "Proving monotonocity..."; + +val bnd_mono = + prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), + fn _ => + [rtac (Collect_subset RS bnd_monoI) 1, + REPEAT (ares_tac (basic_monos @ monos) 1)]); + +val dom_subset = standard (big_rec_def RS Fp.subs); + +val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski)); + +(********) +val dummy = 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]; + +(*Type-checking is hardest aspect of proof; + disjIn selects the correct disjunct after unfolding*) +fun intro_tacsf disjIn prems = + [(*insert prems and underlying sets*) + cut_facts_tac (prems @ (prems RL [PartD1])) 1, + rtac (unfold RS ssubst) 1, + REPEAT (resolve_tac [Part_eqI,CollectI] 1), + (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) + rtac disjIn 2, + REPEAT (ares_tac [refl,exI,conjI] 2), + rewrite_goals_tac con_defs, + (*Now can solve the trivial equation*) + REPEAT (rtac refl 2), + REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims) + ORELSE' dresolve_tac rec_typechecks)), + DEPTH_SOLVE (ares_tac 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 + in accesses_bal(f, g, asm_rl) end; + +val intrs = map (prove part_rec_defs) + (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms))); + +(********) +val dummy = writeln "Proving the elimination rule..."; + +val elim_rls = [asm_rl, FalseE, conjE, exE, disjE]; + +val sumprod_free_SEs = + map (gen_make_elim [conjE,FalseE]) + ([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)) + THEN prune_params_tac; + +val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD); + +(*Applies freeness of the given constructors. + NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *) +fun con_elim_tac defs = + rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs; + +(*String s should have the form t:Si where Si is an inductive set*) +fun mk_cases defs s = + rule_by_tactic (con_elim_tac defs) + (assume_read thy s RS elim); + +val defs = big_rec_def::part_rec_defs; + +val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct); + +end;