src/ZF/indrule.ML
author paulson
Fri Apr 10 13:15:28 1998 +0200 (1998-04-10 ago)
changeset 4804 02b7c759159b
parent 4352 7ac9f3e8a97d
child 4971 09b8945cac07
permissions -rw-r--r--
Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct
     1 (*  Title:      ZF/indrule.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Induction rule module -- for Inductive/Coinductive Definitions
     7 
     8 Proves a strong induction rule and a mutual induction rule
     9 *)
    10 
    11 signature INDRULE =
    12   sig
    13   val induct        : thm                       (*main induction rule*)
    14   val mutual_induct : thm                       (*mutual induction rule*)
    15   end;
    16 
    17 
    18 functor Indrule_Fun
    19     (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
    20      and Pr: PR and CP: CARTPROD and Su : SU and 
    21      Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
    22 let
    23 
    24 val sign = sign_of Inductive.thy;
    25 
    26 val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
    27 
    28 val big_rec_name =
    29   Sign.intern_const sign (space_implode "_" (map Sign.base_name Intr_elim.rec_names));
    30 
    31 val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
    32 
    33 val _ = writeln "  Proving the induction rule...";
    34 
    35 (*** Prove the main induction rule ***)
    36 
    37 val pred_name = "P";            (*name for predicate variables*)
    38 
    39 val big_rec_def::part_rec_defs = Intr_elim.defs;
    40 
    41 (*Used to make induction rules;
    42    ind_alist = [(rec_tm1,pred1),...]  -- associates predicates with rec ops
    43    prem is a premise of an intr rule*)
    44 fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
    45                  (Const("op :",_)$t$X), iprems) =
    46      (case gen_assoc (op aconv) (ind_alist, X) of
    47           Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
    48         | None => (*possibly membership in M(rec_tm), for M monotone*)
    49             let fun mk_sb (rec_tm,pred) = 
    50                         (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
    51             in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
    52   | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
    53 
    54 (*Make a premise of the induction rule.*)
    55 fun induct_prem ind_alist intr =
    56   let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
    57       val iprems = foldr (add_induct_prem ind_alist)
    58                          (Logic.strip_imp_prems intr,[])
    59       val (t,X) = Ind_Syntax.rule_concl intr
    60       val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
    61       val concl = FOLogic.mk_Trueprop (pred $ t)
    62   in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
    63   handle Bind => error"Recursion term not found in conclusion";
    64 
    65 (*Minimizes backtracking by delivering the correct premise to each goal.
    66   Intro rules with extra Vars in premises still cause some backtracking *)
    67 fun ind_tac [] 0 = all_tac
    68   | ind_tac(prem::prems) i = 
    69         DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
    70         ind_tac prems (i-1);
    71 
    72 val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
    73 
    74 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
    75                     Inductive.intr_tms;
    76 
    77 val _ = if !Ind_Syntax.trace then 
    78             (writeln "ind_prems = ";
    79 	     seq (writeln o Sign.string_of_term sign) ind_prems;
    80 	     writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
    81         else ();
    82 
    83 
    84 (*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
    85   simplifications.  If the premises get simplified, then the proofs could 
    86   fail.  *)
    87 val min_ss = empty_ss
    88       setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    89       setSolver  (fn prems => resolve_tac (triv_rls@prems) 
    90                               ORELSE' assume_tac
    91                               ORELSE' etac FalseE);
    92 
    93 val quant_induct = 
    94     prove_goalw_cterm part_rec_defs 
    95       (cterm_of sign 
    96        (Logic.list_implies (ind_prems, 
    97                 FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
    98       (fn prems =>
    99        [rtac (impI RS allI) 1,
   100         DETERM (etac Intr_elim.raw_induct 1),
   101         (*Push Part inside Collect*)
   102         full_simp_tac (min_ss addsimps [Part_Collect]) 1,
   103         (*This CollectE and disjE separates out the introduction rules*)
   104 	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
   105 	(*Now break down the individual cases.  No disjE here in case
   106           some premise involves disjunction.*)
   107         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] 
   108                            ORELSE' hyp_subst_tac)),
   109         ind_tac (rev prems) (length prems) ]);
   110 
   111 (*** Prove the simultaneous induction rule ***)
   112 
   113 (*Make distinct predicates for each inductive set*)
   114 
   115 (*The components of the element type, several if it is a product*)
   116 val elem_type = CP.pseudo_type Inductive.dom_sum;
   117 val elem_factors = CP.factors elem_type;
   118 val elem_frees = mk_frees "za" elem_factors;
   119 val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
   120 
   121 (*Given a recursive set and its domain, return the "fsplit" predicate
   122   and a conclusion for the simultaneous induction rule.
   123   NOTE.  This will not work for mutually recursive predicates.  Previously
   124   a summand 'domt' was also an argument, but this required the domain of
   125   mutual recursion to invariably be a disjoint sum.*)
   126 fun mk_predpair rec_tm = 
   127   let val rec_name = (#1 o dest_Const o head_of) rec_tm
   128       val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
   129                        elem_factors ---> FOLogic.oT)
   130       val qconcl = 
   131         foldr FOLogic.mk_all
   132           (elem_frees, 
   133            FOLogic.imp $ 
   134            (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
   135                  $ (list_comb (pfree, elem_frees)))
   136   in  (CP.ap_split elem_type FOLogic.oT pfree, 
   137        qconcl)  
   138   end;
   139 
   140 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
   141 
   142 (*Used to form simultaneous induction lemma*)
   143 fun mk_rec_imp (rec_tm,pred) = 
   144     FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ 
   145                      (pred $ Bound 0);
   146 
   147 (*To instantiate the main induction rule*)
   148 val induct_concl = 
   149     FOLogic.mk_Trueprop
   150       (Ind_Syntax.mk_all_imp
   151        (big_rec_tm,
   152         Abs("z", Ind_Syntax.iT, 
   153             fold_bal (app FOLogic.conj) 
   154             (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
   155 and mutual_induct_concl =
   156  FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
   157 
   158 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
   159                         resolve_tac [allI, impI, conjI, Part_eqI],
   160                         dresolve_tac [spec, mp, Pr.fsplitD]];
   161 
   162 val need_mutual = length Intr_elim.rec_names > 1;
   163 
   164 val lemma = (*makes the link between the two induction rules*)
   165   if need_mutual then
   166      (writeln "  Proving the mutual induction rule...";
   167       prove_goalw_cterm part_rec_defs 
   168 	    (cterm_of sign (Logic.mk_implies (induct_concl,
   169 					      mutual_induct_concl)))
   170 	    (fn prems =>
   171 	     [cut_facts_tac prems 1, 
   172 	      REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
   173 		      lemma_tac 1)]))
   174   else (writeln "  [ No mutual induction rule needed ]";
   175         TrueI);
   176 
   177 (*Mutual induction follows by freeness of Inl/Inr.*)
   178 
   179 (*Simplification largely reduces the mutual induction rule to the 
   180   standard rule*)
   181 val mut_ss = 
   182     min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
   183 
   184 val all_defs = Inductive.con_defs @ part_rec_defs;
   185 
   186 (*Removes Collects caused by M-operators in the intro rules.  It is very
   187   hard to simplify
   188     list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) 
   189   where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
   190   Instead the following rules extract the relevant conjunct.
   191 *)
   192 val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
   193 
   194 (*Minimizes backtracking by delivering the correct premise to each goal*)
   195 fun mutual_ind_tac [] 0 = all_tac
   196   | mutual_ind_tac(prem::prems) i = 
   197       DETERM
   198        (SELECT_GOAL 
   199           (
   200            (*Simplify the assumptions and goal by unfolding Part and
   201              using freeness of the Sum constructors; proves all but one
   202              conjunct by contradiction*)
   203            rewrite_goals_tac all_defs  THEN
   204            simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
   205            IF_UNSOLVED (*simp_tac may have finished it off!*)
   206              ((*simplify assumptions*)
   207               (*some risk of excessive simplification here -- might have
   208                 to identify the bare minimum set of rewrites*)
   209               full_simp_tac 
   210                  (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
   211               THEN
   212               (*unpackage and use "prem" in the corresponding place*)
   213               REPEAT (rtac impI 1)  THEN
   214               rtac (rewrite_rule all_defs prem) 1  THEN
   215               (*prem must not be REPEATed below: could loop!*)
   216               DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
   217                                       eresolve_tac (conjE::mp::cmonos))))
   218           ) i)
   219        THEN mutual_ind_tac prems (i-1);
   220 
   221 val mutual_induct_fsplit = 
   222   if need_mutual then
   223     prove_goalw_cterm []
   224           (cterm_of sign
   225            (Logic.list_implies 
   226               (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
   227                mutual_induct_concl)))
   228           (fn prems =>
   229            [rtac (quant_induct RS lemma) 1,
   230             mutual_ind_tac (rev prems) (length prems)])
   231   else TrueI;
   232 
   233 (** Uncurrying the predicate in the ordinary induction rule **)
   234 
   235 (*instantiate the variable to a tuple, if it is non-trivial, in order to
   236   allow the predicate to be "opened up".
   237   The name "x.1" comes from the "RS spec" !*)
   238 val inst = 
   239     case elem_frees of [_] => I
   240        | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
   241                                  cterm_of sign elem_tuple)]);
   242 
   243 (*strip quantifier and the implication*)
   244 val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
   245 
   246 val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
   247 
   248 in
   249   struct
   250   (*strip quantifier*)
   251   val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0) 
   252                |> standard;
   253 
   254   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   255   val mutual_induct = CP.remove_split mutual_induct_fsplit
   256   end
   257 end;