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.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.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;
```