src/HOL/indrule.ML
changeset 1728 01beef6262aa
parent 1653 1a2ffa2fbf7d
child 1746 f0c6aabc6c02
equal deleted inserted replaced
1727:7d0fbdc46e8e 1728:01beef6262aa
    97     handle e => print_sign_exn sign e;
    97     handle e => print_sign_exn sign e;
    98 
    98 
    99 (*** Prove the simultaneous induction rule ***)
    99 (*** Prove the simultaneous induction rule ***)
   100 
   100 
   101 (*Make distinct predicates for each inductive set.
   101 (*Make distinct predicates for each inductive set.
   102   Splits cartesian products in elem_type, IF nested to the right! *)
   102   Splits cartesian products in elem_type, however nested*)
       
   103 
       
   104 (*The components of the element type, several if it is a product*)
       
   105 val elem_factors = Ind_Syntax.factors elem_type;
       
   106 val elem_frees = mk_frees "za" elem_factors;
       
   107 val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;
   103 
   108 
   104 (*Given a recursive set, return the "split" predicate
   109 (*Given a recursive set, return the "split" predicate
   105   and a conclusion for the simultaneous induction rule*)
   110   and a conclusion for the simultaneous induction rule*)
   106 fun mk_predpair rec_tm = 
   111 fun mk_predpair rec_tm = 
   107   let val rec_name = (#1 o dest_Const o head_of) rec_tm
   112   let val rec_name = (#1 o dest_Const o head_of) rec_tm
   108       val T = Ind_Syntax.factors elem_type ---> Ind_Syntax.boolT
   113       val pfree = Free(pred_name ^ "_" ^ rec_name, 
   109       val pfree = Free(pred_name ^ "_" ^ rec_name, T)
   114 		       elem_factors ---> Ind_Syntax.boolT)
   110       val frees = mk_frees "za" (binder_types T)
       
   111       val qconcl = 
   115       val qconcl = 
   112         foldr Ind_Syntax.mk_all 
   116         foldr Ind_Syntax.mk_all 
   113           (frees, 
   117           (elem_frees, 
   114            Ind_Syntax.imp $ (Ind_Syntax.mk_mem 
   118            Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
   115                              (foldr1 Ind_Syntax.mk_Pair frees, rec_tm))
   119                 $ (list_comb (pfree, elem_frees)))
   116                 $ (list_comb (pfree,frees)))
   120   in  (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
   117   in  (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T), 
   121        qconcl)  
   118       qconcl)  
       
   119   end;
   122   end;
   120 
   123 
   121 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
   124 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
   122 
   125 
   123 (*Used to form simultaneous induction lemma*)
   126 (*Used to form simultaneous induction lemma*)
   133             fold_bal (app Ind_Syntax.conj) 
   136             fold_bal (app Ind_Syntax.conj) 
   134             (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   137             (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   135 and mutual_induct_concl = 
   138 and mutual_induct_concl = 
   136     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
   139     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
   137 
   140 
       
   141 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
       
   142 			resolve_tac [allI, impI, conjI, Part_eqI, refl],
       
   143 			dresolve_tac [spec, mp, splitD]];
       
   144 
   138 val lemma = (*makes the link between the two induction rules*)
   145 val lemma = (*makes the link between the two induction rules*)
   139     prove_goalw_cterm part_rec_defs 
   146     prove_goalw_cterm part_rec_defs 
   140           (cterm_of sign (Logic.mk_implies (induct_concl,
   147           (cterm_of sign (Logic.mk_implies (induct_concl,
   141                                             mutual_induct_concl)))
   148                                             mutual_induct_concl)))
   142           (fn prems =>
   149           (fn prems =>
   143            [cut_facts_tac prems 1,
   150            [cut_facts_tac prems 1,
   144             REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
   151             REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
   145              ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1
   152 		    lemma_tac 1)])
   146              ORELSE dresolve_tac [spec, mp, splitD] 1)])
       
   147     handle e => print_sign_exn sign e;
   153     handle e => print_sign_exn sign e;
   148 
   154 
   149 (*Mutual induction follows by freeness of Inl/Inr.*)
   155 (*Mutual induction follows by freeness of Inl/Inr.*)
   150 
   156 
   151 (*Simplification largely reduces the mutual induction rule to the 
   157 (*Simplification largely reduces the mutual induction rule to the 
   152   standard rule*)
   158   standard rule*)
   153 val mut_ss = simpset_of "Fun"
   159 val mut_ss = simpset_of "Fun"
   154              addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
   160              addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
   155 
   161 
   156 val all_defs = Inductive.con_defs @ part_rec_defs;
   162 val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;
   157 
   163 
   158 (*Removes Collects caused by M-operators in the intro rules*)
   164 (*Removes Collects caused by M-operators in the intro rules*)
   159 val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
   165 val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
   160              (2,[rev_subsetD]);
   166              (2,[rev_subsetD]);
   161 
   167 
   170              conjunct by contradiction*)
   176              conjunct by contradiction*)
   171            rewrite_goals_tac all_defs  THEN
   177            rewrite_goals_tac all_defs  THEN
   172            simp_tac (mut_ss addsimps [Part_def]) 1  THEN
   178            simp_tac (mut_ss addsimps [Part_def]) 1  THEN
   173            IF_UNSOLVED (*simp_tac may have finished it off!*)
   179            IF_UNSOLVED (*simp_tac may have finished it off!*)
   174              ((*simplify assumptions, but don't accept new rewrite rules!*)
   180              ((*simplify assumptions, but don't accept new rewrite rules!*)
   175               asm_full_simp_tac (mut_ss setmksimps K[]) 1  THEN
   181               full_simp_tac mut_ss 1  THEN
   176               (*unpackage and use "prem" in the corresponding place*)
   182               (*unpackage and use "prem" in the corresponding place*)
   177               REPEAT (rtac impI 1)  THEN
   183               REPEAT (rtac impI 1)  THEN
   178               rtac (rewrite_rule all_defs prem) 1  THEN
   184               rtac (rewrite_rule all_defs prem) 1  THEN
   179               (*prem must not be REPEATed below: could loop!*)
   185               (*prem must not be REPEATed below: could loop!*)
   180               DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
   186               DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
   193           (fn prems =>
   199           (fn prems =>
   194            [rtac (quant_induct RS lemma) 1,
   200            [rtac (quant_induct RS lemma) 1,
   195             mutual_ind_tac (rev prems) (length prems)])
   201             mutual_ind_tac (rev prems) (length prems)])
   196     handle e => print_sign_exn sign e;
   202     handle e => print_sign_exn sign e;
   197 
   203 
   198 (*Attempts to remove all occurrences of split*)
   204 (** Uncurrying the predicate in the ordinary induction rule **)
   199 val split_tac =
   205 
   200     REPEAT (SOMEGOAL (FIRST' [rtac splitI, 
   206 (*The name "x.1" comes from the "RS spec" !*)
   201                               dtac splitD,
   207 val xvar = cterm_of sign (Var(("x",1), elem_type));
   202                               etac splitE,
   208 
   203                               bound_hyp_subst_tac]))
   209 (*strip quantifier and instantiate the variable to a tuple*)
   204     THEN prune_params_tac;
   210 val induct0 = quant_induct RS spec RSN (2,rev_mp) |>
       
   211               freezeT |>     (*Because elem_type contains TFrees not TVars*)
       
   212               instantiate ([], [(xvar, cterm_of sign elem_tuple)]);
   205 
   213 
   206 in
   214 in
   207   struct
   215   struct
   208   (*strip quantifier*)
   216   val induct = standard 
   209   val induct = standard (quant_induct RS spec RSN (2,rev_mp));
   217                   (Ind_Syntax.split_rule_var
   210 
   218 		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
       
   219 		     induct0));
       
   220 
       
   221   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   211   val mutual_induct = 
   222   val mutual_induct = 
   212       if length Intr_elim.rec_names > 1 orelse
   223       if length Intr_elim.rec_names > 1
   213          length (Ind_Syntax.factors elem_type) > 1
   224       then Ind_Syntax.remove_split mutual_induct_split
   214       then rule_by_tactic split_tac mutual_induct_split
       
   215       else TrueI;
   225       else TrueI;
   216   end
   226   end
   217 end;
   227 end;