src/HOL/Tools/inductive_package.ML
changeset 11682 d9063229b4a1
parent 11628 e57a6e51715e
child 11740 86ac4189a1c1
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:00 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:43 2001 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  val all_not_allowed = 
     1.5      "Introduction rule must not have a leading \"!!\" quantifier";
     1.6  
     1.7 -val atomize_cterm = hol_rewrite_cterm inductive_atomize;
     1.8 +val atomize_cterm = full_rewrite_cterm inductive_atomize;
     1.9  
    1.10  in
    1.11  
    1.12 @@ -543,14 +543,26 @@
    1.13    the given defs.  Cannot simply use the local con_defs because con_defs=[]
    1.14    for inference systems. (??) *)
    1.15  
    1.16 +local
    1.17 +
    1.18  (*cprop should have the form t:Si where Si is an inductive set*)
    1.19 +val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
    1.20  
    1.21 -val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
    1.22 +(*delete needless equality assumptions*)
    1.23 +val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
    1.24 +val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
    1.25 +val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    1.26 +
    1.27 +fun simp_case_tac solved ss i =
    1.28 +  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
    1.29 +  THEN_MAYBE (if solved then no_tac else all_tac);
    1.30 +
    1.31 +in
    1.32  
    1.33  fun mk_cases_i elims ss cprop =
    1.34    let
    1.35      val prem = Thm.assume cprop;
    1.36 -    val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
    1.37 +    val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
    1.38      fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
    1.39    in
    1.40      (case get_first (try mk_elim) elims of
    1.41 @@ -569,6 +581,8 @@
    1.42      val (_, {elims, ...}) = the_inductive thy c;
    1.43    in mk_cases_i elims ss cprop end;
    1.44  
    1.45 +end;
    1.46 +
    1.47  
    1.48  (* inductive_cases(_i) *)
    1.49