src/ZF/intr_elim.ML
changeset 0 a5a9c433f639
child 14 1c0926788772
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/intr_elim.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,279 @@
     1.4 +(*  Title: 	ZF/intr-elim.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Introduction/elimination rule module -- for Inductive/Coinductive Definitions
    1.10 +
    1.11 +Features:
    1.12 +* least or greatest fixedpoints
    1.13 +* user-specified product and sum constructions
    1.14 +* mutually recursive definitions
    1.15 +* definitions involving arbitrary monotone operators
    1.16 +* automatically proves introduction and elimination rules
    1.17 +
    1.18 +The recursive sets must *already* be declared as constants in parent theory!
    1.19 +
    1.20 +  Introduction rules have the form
    1.21 +  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
    1.22 +  where M is some monotone operator (usually the identity)
    1.23 +  P(x) is any (non-conjunctive) side condition on the free variables
    1.24 +  ti, t are any terms
    1.25 +  Sj, Sk are two of the sets being defiend in mutual recursion
    1.26 +
    1.27 +Sums are used only for mutual recursion;
    1.28 +Products are used only to derive "streamlined" induction rules for relations
    1.29 +*)
    1.30 +
    1.31 +signature FP =		(** Description of a fixed point operator **)
    1.32 +  sig
    1.33 +  val oper	: term			(*fixed point operator*)
    1.34 +  val bnd_mono	: term			(*monotonicity predicate*)
    1.35 +  val bnd_monoI	: thm			(*intro rule for bnd_mono*)
    1.36 +  val subs	: thm			(*subset theorem for fp*)
    1.37 +  val Tarski	: thm			(*Tarski's fixed point theorem*)
    1.38 +  val induct	: thm			(*induction/coinduction rule*)
    1.39 +  end;
    1.40 +
    1.41 +signature PR =			(** Description of a Cartesian product **)
    1.42 +  sig
    1.43 +  val sigma	: term			(*Cartesian product operator*)
    1.44 +  val pair	: term			(*pairing operator*)
    1.45 +  val split_const  : term		(*splitting operator*)
    1.46 +  val fsplit_const : term		(*splitting operator for formulae*)
    1.47 +  val pair_iff	: thm			(*injectivity of pairing, using <->*)
    1.48 +  val split_eq	: thm			(*equality rule for split*)
    1.49 +  val fsplitI	: thm			(*intro rule for fsplit*)
    1.50 +  val fsplitD	: thm			(*destruct rule for fsplit*)
    1.51 +  val fsplitE	: thm			(*elim rule for fsplit*)
    1.52 +  end;
    1.53 +
    1.54 +signature SU =			(** Description of a disjoint sum **)
    1.55 +  sig
    1.56 +  val sum	: term			(*disjoint sum operator*)
    1.57 +  val inl	: term			(*left injection*)
    1.58 +  val inr	: term			(*right injection*)
    1.59 +  val elim	: term			(*case operator*)
    1.60 +  val case_inl	: thm			(*inl equality rule for case*)
    1.61 +  val case_inr	: thm			(*inr equality rule for case*)
    1.62 +  val inl_iff	: thm			(*injectivity of inl, using <->*)
    1.63 +  val inr_iff	: thm			(*injectivity of inr, using <->*)
    1.64 +  val distinct	: thm			(*distinctness of inl, inr using <->*)
    1.65 +  val distinct'	: thm			(*distinctness of inr, inl using <->*)
    1.66 +  end;
    1.67 +
    1.68 +signature INDUCTIVE =		(** Description of a (co)inductive defn **)
    1.69 +  sig
    1.70 +  val thy        : theory		(*parent theory*)
    1.71 +  val rec_doms   : (string*string) list	(*recursion ops and their domains*)
    1.72 +  val sintrs     : string list		(*desired introduction rules*)
    1.73 +  val monos      : thm list		(*monotonicity of each M operator*)
    1.74 +  val con_defs   : thm list		(*definitions of the constructors*)
    1.75 +  val type_intrs : thm list		(*type-checking intro rules*)
    1.76 +  val type_elims : thm list		(*type-checking elim rules*)
    1.77 +  end;
    1.78 +
    1.79 +signature INTR_ELIM =
    1.80 +  sig
    1.81 +  val thy        : theory		(*new theory*)
    1.82 +  val defs	 : thm list		(*definitions made in thy*)
    1.83 +  val bnd_mono   : thm			(*monotonicity for the lfp definition*)
    1.84 +  val unfold     : thm			(*fixed-point equation*)
    1.85 +  val dom_subset : thm			(*inclusion of recursive set in dom*)
    1.86 +  val intrs      : thm list		(*introduction rules*)
    1.87 +  val elim       : thm			(*case analysis theorem*)
    1.88 +  val raw_induct : thm			(*raw induction rule from Fp.induct*)
    1.89 +  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
    1.90 +  (*internal items...*)
    1.91 +  val big_rec_tm : term			(*the lhs of the fixedpoint defn*)
    1.92 +  val rec_tms    : term list		(*the mutually recursive sets*)
    1.93 +  val domts      : term list		(*domains of the recursive sets*)
    1.94 +  val intr_tms   : term list		(*terms for the introduction rules*)
    1.95 +  val rec_params : term list		(*parameters of the recursion*)
    1.96 +  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
    1.97 +  end;
    1.98 +
    1.99 +
   1.100 +functor Intr_elim_Fun (structure Ind: INDUCTIVE and 
   1.101 +		       Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
   1.102 +struct
   1.103 +open Logic Ind;
   1.104 +
   1.105 +(*** Extract basic information from arguments ***)
   1.106 +
   1.107 +val sign = sign_of Ind.thy;
   1.108 +
   1.109 +fun rd T a = 
   1.110 +    Sign.read_cterm sign (a,T)
   1.111 +    handle ERROR => error ("The error above occurred for " ^ a);
   1.112 +
   1.113 +val rec_names = map #1 rec_doms
   1.114 +and domts     = map (Sign.term_of o rd iT o #2) rec_doms;
   1.115 +
   1.116 +val dummy = assert_all Syntax.is_identifier rec_names
   1.117 +   (fn a => "Name of recursive set not an identifier: " ^ a);
   1.118 +
   1.119 +val dummy = assert_all (is_some o lookup_const sign) rec_names
   1.120 +   (fn a => "Name of recursive set not declared as constant: " ^ a);
   1.121 +
   1.122 +val intr_tms = map (Sign.term_of o rd propT) sintrs;
   1.123 +val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
   1.124 +val rec_hds = map (fn a=> Const(a,recT)) rec_names;
   1.125 +val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
   1.126 +
   1.127 +val dummy = assert_all is_Free rec_params
   1.128 +    (fn t => "Param in recursion term not a free variable: " ^
   1.129 +             Sign.string_of_term sign t);
   1.130 +
   1.131 +(*** Construct the lfp definition ***)
   1.132 +
   1.133 +val mk_variant = variant (foldr add_term_names (intr_tms,[]));
   1.134 +
   1.135 +val z' = mk_variant"z"
   1.136 +and X' = mk_variant"X"
   1.137 +and w' = mk_variant"w";
   1.138 +
   1.139 +(*simple error-checking in the premises*)
   1.140 +fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
   1.141 +	error"Premises may not be conjuctive"
   1.142 +  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
   1.143 +	deny (rec_hd occs t) "Recursion term on left of member symbol"
   1.144 +  | chk_prem rec_hd t = 
   1.145 +	deny (rec_hd occs t) "Recursion term in side formula";
   1.146 +
   1.147 +(*Makes a disjunct from an introduction rule*)
   1.148 +fun lfp_part intr = (*quantify over rule's free vars except parameters*)
   1.149 +  let val prems = map dest_tprop (strip_imp_prems intr)
   1.150 +      val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
   1.151 +      val exfrees = term_frees intr \\ rec_params
   1.152 +      val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
   1.153 +  in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
   1.154 +
   1.155 +val dom_sum = fold_bal (app Su.sum) domts;
   1.156 +
   1.157 +(*The Part(A,h) terms -- compose injections to make h*)
   1.158 +fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
   1.159 +  | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
   1.160 +
   1.161 +(*Access to balanced disjoint sums via injections*)
   1.162 +val parts = 
   1.163 +    map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
   1.164 +		              (length rec_doms));
   1.165 +
   1.166 +(*replace each set by the corresponding Part(A,h)*)
   1.167 +val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
   1.168 +
   1.169 +val lfp_abs = absfree(X', iT, 
   1.170 +	         mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
   1.171 +
   1.172 +val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
   1.173 +
   1.174 +val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
   1.175 +			   "Illegal occurrence of recursion operator")
   1.176 +	 rec_hds;
   1.177 +
   1.178 +(*** Make the new theory ***)
   1.179 +
   1.180 +(*A key definition:
   1.181 +  If no mutual recursion then it equals the one recursive set.
   1.182 +  If mutual recursion then it differs from all the recursive sets. *)
   1.183 +val big_rec_name = space_implode "_" rec_names;
   1.184 +
   1.185 +(*Big_rec... is the union of the mutually recursive sets*)
   1.186 +val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   1.187 +
   1.188 +(*The individual sets must already be declared*)
   1.189 +val axpairs = map (mk_defpair sign) 
   1.190 +      ((big_rec_tm, lfp_rhs) ::
   1.191 +       (case parts of 
   1.192 +	   [_] => [] 			(*no mutual recursion*)
   1.193 +	 | _ => rec_tms ~~		(*define the sets as Parts*)
   1.194 +		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   1.195 +
   1.196 +val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
   1.197 +    ([], [], [], [], [], None) axpairs;
   1.198 +
   1.199 +val defs = map (get_axiom thy o #1) axpairs;
   1.200 +
   1.201 +val big_rec_def::part_rec_defs = defs;
   1.202 +
   1.203 +val prove = prove_term (sign_of thy);
   1.204 +
   1.205 +(********)
   1.206 +val dummy = writeln "Proving monotonocity...";
   1.207 +
   1.208 +val bnd_mono = 
   1.209 +    prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 
   1.210 +       fn _ =>
   1.211 +       [rtac (Collect_subset RS bnd_monoI) 1,
   1.212 +	REPEAT (ares_tac (basic_monos @ monos) 1)]);
   1.213 +
   1.214 +val dom_subset = standard (big_rec_def RS Fp.subs);
   1.215 +
   1.216 +val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
   1.217 +
   1.218 +(********)
   1.219 +val dummy = writeln "Proving the introduction rules...";
   1.220 +
   1.221 +(*Mutual recursion: Needs subset rules for the individual sets???*)
   1.222 +val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
   1.223 +
   1.224 +(*Type-checking is hardest aspect of proof;
   1.225 +  disjIn selects the correct disjunct after unfolding*)
   1.226 +fun intro_tacsf disjIn prems = 
   1.227 +  [(*insert prems and underlying sets*)
   1.228 +   cut_facts_tac (prems @ (prems RL [PartD1])) 1,
   1.229 +   rtac (unfold RS ssubst) 1,
   1.230 +   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
   1.231 +   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   1.232 +   rtac disjIn 2,
   1.233 +   REPEAT (ares_tac [refl,exI,conjI] 2),
   1.234 +   rewrite_goals_tac con_defs,
   1.235 +   (*Now can solve the trivial equation*)
   1.236 +   REPEAT (rtac refl 2),
   1.237 +   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
   1.238 +		      ORELSE' dresolve_tac rec_typechecks)),
   1.239 +   DEPTH_SOLVE (ares_tac type_intrs 1)];
   1.240 +
   1.241 +(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
   1.242 +val mk_disj_rls = 
   1.243 +    let fun f rl = rl RS disjI1
   1.244 +        and g rl = rl RS disjI2
   1.245 +    in  accesses_bal(f, g, asm_rl)  end;
   1.246 +
   1.247 +val intrs = map (prove part_rec_defs) 
   1.248 +	       (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
   1.249 +
   1.250 +(********)
   1.251 +val dummy = writeln "Proving the elimination rule...";
   1.252 +
   1.253 +val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];
   1.254 +
   1.255 +val sumprod_free_SEs = 
   1.256 +    map (gen_make_elim [conjE,FalseE])
   1.257 +        ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   1.258 +	 RL [iffD1]);
   1.259 +
   1.260 +(*Breaks down logical connectives in the monotonic function*)
   1.261 +val basic_elim_tac =
   1.262 +    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
   1.263 +              ORELSE' bound_hyp_subst_tac))
   1.264 +    THEN prune_params_tac;
   1.265 +
   1.266 +val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   1.267 +
   1.268 +(*Applies freeness of the given constructors.
   1.269 +  NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
   1.270 +fun con_elim_tac defs =
   1.271 +    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
   1.272 +
   1.273 +(*String s should have the form t:Si where Si is an inductive set*)
   1.274 +fun mk_cases defs s = 
   1.275 +    rule_by_tactic (con_elim_tac defs)
   1.276 +      (assume_read thy s  RS  elim);
   1.277 +
   1.278 +val defs = big_rec_def::part_rec_defs;
   1.279 +
   1.280 +val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
   1.281 +
   1.282 +end;