src/HOL/Tools/inductive_package.ML
changeset 8336 fdf3ac335f77
parent 8316 74639e19eca0
child 8375 0544749a5e8f
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Mar 03 21:00:58 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 03 21:01:57 2000 +0100
     1.3 @@ -203,13 +203,6 @@
     1.4  
     1.5  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
     1.6  
     1.7 -(*Delete needless equality assumptions*)
     1.8 -val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
     1.9 -     (fn _ => [assume_tac 1]);
    1.10 -
    1.11 -(*For simplifying the elimination rule*)
    1.12 -val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
    1.13 -
    1.14  val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
    1.15  val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
    1.16  
    1.17 @@ -493,20 +486,13 @@
    1.18    the given defs.  Cannot simply use the local con_defs because con_defs=[] 
    1.19    for inference systems.
    1.20   *)
    1.21 -fun con_elim_tac ss =
    1.22 -  let val elim_tac = REPEAT o (eresolve_tac elim_rls)
    1.23 -  in ALLGOALS(EVERY'[elim_tac,
    1.24 -		     asm_full_simp_tac ss,
    1.25 -		     elim_tac,
    1.26 -		     REPEAT o bound_hyp_subst_tac])
    1.27 -     THEN prune_params_tac
    1.28 -  end;
    1.29  
    1.30  (*cprop should have the form t:Si where Si is an inductive set*)
    1.31 -fun mk_cases_i elims ss cprop =
    1.32 +fun mk_cases_i solved elims ss cprop =
    1.33    let
    1.34      val prem = Thm.assume cprop;
    1.35 -    fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
    1.36 +    val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
    1.37 +    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
    1.38    in
    1.39      (case get_first (try mk_elim) elims of
    1.40        Some r => r
    1.41 @@ -516,7 +502,7 @@
    1.42    end;
    1.43  
    1.44  fun mk_cases elims s =
    1.45 -  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
    1.46 +  mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
    1.47  
    1.48  
    1.49  (* inductive_cases(_i) *)
    1.50 @@ -529,7 +515,7 @@
    1.51      val atts = map (prep_att thy) raw_atts;
    1.52      val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
    1.53      val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    1.54 -    val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
    1.55 +    val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
    1.56    in
    1.57      thy
    1.58      |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)