src/HOL/Tools/inductive_package.ML
changeset 7293 959e060f4a2f
parent 7257 745cfc8871e2
child 7349 228b711ad68c
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 19 18:36:41 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 19 19:00:42 1999 +0200
     1.3 @@ -455,6 +455,10 @@
     1.4  
     1.5      val sign = Theory.sign_of thy;
     1.6  
     1.7 +    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
     1.8 +        None => []
     1.9 +      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
    1.10 +
    1.11      val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    1.12  
    1.13      (* make predicate for instantiation of abstract induction rule *)
    1.14 @@ -463,7 +467,7 @@
    1.15        | mk_ind_pred T Ps =
    1.16           let val n = (length Ps) div 2;
    1.17               val Type (_, [T1, T2]) = T
    1.18 -         in Const ("basic_sum_case",
    1.19 +         in Const ("Datatype.sum.sum_case",
    1.20             [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
    1.21               mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
    1.22           end;
    1.23 @@ -482,8 +486,7 @@
    1.24            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
    1.25             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
    1.26               nth_elem (find_index_eq c cs, preds)))))
    1.27 -        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
    1.28 -           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.29 +        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
    1.30            rtac refl 1])) cs;
    1.31  
    1.32      val induct = prove_goalw_cterm [] (cterm_of sign
    1.33 @@ -498,7 +501,7 @@
    1.34             some premise involves disjunction.*)
    1.35           REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
    1.36                       ORELSE' hyp_subst_tac)),
    1.37 -         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.38 +         rewrite_goals_tac sum_case_rewrites,
    1.39           EVERY (map (fn prem =>
    1.40             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.41  
    1.42 @@ -508,7 +511,7 @@
    1.43           REPEAT (EVERY
    1.44             [REPEAT (resolve_tac [conjI, impI] 1),
    1.45              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
    1.46 -            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.47 +            rewrite_goals_tac sum_case_rewrites,
    1.48              atac 1])])
    1.49  
    1.50    in standard (split_rule (induct RS lemma))