eliminated clone of Inductive.mk_cases_tac;
authorwenzelm
Mon Sep 30 13:45:17 2013 +0200 (2013-09-30)
changeset 539944237859c186d
parent 53993 28fefe1d6749
child 53995 1d457fc83f5c
eliminated clone of Inductive.mk_cases_tac;
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:35:05 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:45:17 2013 +0200
     1.3 @@ -17,19 +17,6 @@
     1.4  structure Fun_Cases : FUN_CASES =
     1.5  struct
     1.6  
     1.7 -local
     1.8 -
     1.9 -val refl_thin =
    1.10 -  Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
    1.11 -    (fn _ => assume_tac 1);
    1.12 -val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    1.13 -val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    1.14 -
    1.15 -fun simp_case_tac ctxt i =
    1.16 -  EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
    1.17 -
    1.18 -in
    1.19 -
    1.20  fun mk_fun_cases ctxt prop =
    1.21    let
    1.22      val thy = Proof_Context.theory_of ctxt;
    1.23 @@ -44,9 +31,9 @@
    1.24      val {elims, pelims, is_partial, ...} = info;
    1.25      val elims = if is_partial then pelims else the elims;
    1.26      val cprop = cterm_of thy prop;
    1.27 -    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.28      fun mk_elim rl =
    1.29 -      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    1.30 +      Thm.implies_intr cprop
    1.31 +        (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
    1.32        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    1.33    in
    1.34      (case get_first (try mk_elim) (flat elims) of
    1.35 @@ -54,9 +41,6 @@
    1.36      | NONE => err ())
    1.37    end;
    1.38  
    1.39 -end;
    1.40 -
    1.41 -
    1.42  fun gen_fun_cases prep_att prep_prop args lthy =
    1.43    let
    1.44      val thy = Proof_Context.theory_of lthy;
     2.1 --- a/src/HOL/Tools/inductive.ML	Mon Sep 30 13:35:05 2013 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Mon Sep 30 13:45:17 2013 +0200
     2.3 @@ -30,6 +30,7 @@
     2.4    val get_monos: Proof.context -> thm list
     2.5    val mono_add: attribute
     2.6    val mono_del: attribute
     2.7 +  val mk_cases_tac: Proof.context -> tactic
     2.8    val mk_cases: Proof.context -> term -> thm
     2.9    val inductive_forall_def: thm
    2.10    val rulify: Proof.context -> thm -> thm
    2.11 @@ -540,6 +541,8 @@
    2.12  
    2.13  in
    2.14  
    2.15 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    2.16 +
    2.17  fun mk_cases ctxt prop =
    2.18    let
    2.19      val thy = Proof_Context.theory_of ctxt;
    2.20 @@ -551,9 +554,9 @@
    2.21      val elims = Induct.find_casesP ctxt prop;
    2.22  
    2.23      val cprop = Thm.cterm_of thy prop;
    2.24 -    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    2.25      fun mk_elim rl =
    2.26 -      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    2.27 +      Thm.implies_intr cprop
    2.28 +        (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
    2.29        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    2.30    in
    2.31      (case get_first (try mk_elim) elims of