src/HOL/indrule.ML
 changeset 1728 01beef6262aa parent 1653 1a2ffa2fbf7d child 1746 f0c6aabc6c02
equal 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;`