src/ZF/intr-elim.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Initial revision
     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;