src/HOL/Tools/induct_method.ML

   val cases_set_local: string -> Proof.context attribute
   val induct_type_global: string -> theory attribute
   val induct_set_global: string -> theory attribute
   val induct_type_local: string -> Proof.context attribute
   val induct_set_local: string -> Proof.context attribute
-  val con_elim_tac: simpset -> tactic
-  val con_elim_solved_tac: simpset -> tactic
+  val simp_case_tac: bool -> simpset -> int -> tactic
   val setup: (theory -> theory) list
 end;
 
 structure InductMethod: INDUCT_METHOD =
 struct

 
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
 
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
 
-fun simp_case_tac ss = 
-  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac];
-
 in
 
-fun con_elim_tac ss = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
-
-fun con_elim_solved_tac ss =
-  ALLGOALS (fn i => TRY (simp_case_tac ss i THEN_MAYBE no_tac)) THEN prune_params_tac;
+fun simp_case_tac solved ss i =
+  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
+  THEN_MAYBE (if solved then no_tac else all_tac);
 
 end;
 
 
 

 fun cases_var thm =
   (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
     None => raise THM ("Malformed cases rule", 0, [thm])
   | Some x => x);
 
-fun simplify_cases ctxt =
-  Tactic.rule_by_tactic (con_elim_solved_tac (Simplifier.get_local_simpset ctxt));
-
-fun cases_tac (ctxt, (simplified, args)) facts =
+fun simplified_cases ctxt cases thm =
+  let
+    val nprems = Thm.nprems_of thm;
+    val opt_cases =
+      Library.replicate (nprems - Int.min (nprems, length cases)) None @
+      map Some (Library.take (nprems, cases));
+
+    val tac = simp_case_tac true (Simplifier.get_local_simpset ctxt);
+    fun simp ((i, c), (th, cs)) =
+      (case try (Tactic.rule_by_tactic (tac i)) th of
+        None => (th, None :: cs)
+      | Some th' => (th', c :: cs));
+
+    val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, []));
+  in (thm', mapfilter I opt_cases') end;
+
+fun cases_tac (ctxt, ((simplified, opaque), args)) facts =
   let
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
 
     fun inst_rule t thm =
       Drule.cterm_instantiate [(cert (cases_var thm), cert t)] thm;
-
-    val cond_simp = if simplified then simplify_cases ctxt else I;
 
     fun find_cases th =
       NetRules.may_unify (#2 (get_cases ctxt))
         (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
 

               None => error ("No cases rule for type: " ^ quote name)
             | Some thm => [(inst_rule t thm, RuleCases.get thm)])
           end
       | ((None, None), th :: _) => map (RuleCases.add o #2) (find_cases th)
       | ((Some t, None), th :: _) =>
-          (case find_cases th of	(*may instantiate first rule only!*)
+          (case find_cases th of        (*may instantiate first rule only!*)
             (_, thm) :: _ => [(inst_rule t thm, RuleCases.get thm)]
           | [] => [])
       | ((None, Some thm), _) => [RuleCases.add thm]
       | ((Some t, Some thm), _) => [(inst_rule t thm, RuleCases.get thm)]);
 
+    val cond_simp = if simplified then simplified_cases ctxt else rpair;
+
     fun prep_rule (thm, cases) =
-      Seq.map (rpair cases o cond_simp) (Method.multi_resolves facts [thm]);
-  in Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
+      Seq.map (cond_simp cases) (Method.multi_resolves facts [thm]);
+  in Method.resolveq_cases_tac opaque (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
 
 in
 
 val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
 

         | [] => error "No rule given"
         | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
       end;
 
 
-fun induct_tac (ctxt, (stripped, args)) facts =
+fun induct_tac (ctxt, ((stripped, opaque), args)) facts =
   let
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
 
     fun prep_var (x, Some t) = Some (cert x, cert t)

           let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
             handle Library.LIST _ => error "Unable to figure out type induction rule"
           in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
       | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
       | ((insts, None), th :: _) =>
-          (case find_induct th of	(*may instantiate first rule only!*)
-	    (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
+          (case find_induct th of       (*may instantiate first rule only!*)
+            (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
           | [] => [])
       | (([], Some thm), _) => [RuleCases.add thm]
       | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]);
 
     fun prep_rule (thm, cases) =
       Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
-    val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
+    val tac = Method.resolveq_cases_tac opaque (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in
     if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
     else tac
   end;
 

 val casesN = "cases";
 val inductN = "induct";
 
 val simplifiedN = "simplified";
 val strippedN = "stripped";
+val opaqN = "opaque";
 
 val typeN = "type";
 val setN = "set";
 val ruleN = "rule";
 

 fun mode name =
   Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
 
 in
 
-val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
+val cases_args = Method.syntax
+  (mode simplifiedN -- mode opaqN -- (Scan.option term -- Scan.option cases_rule));
+
 val induct_args = Method.syntax
-  (mode strippedN -- (Args.and_list (Scan.repeat term_dummy) -- Scan.option induct_rule));
+  (mode strippedN -- mode opaqN -- (Args.and_list (Scan.repeat term_dummy) -- Scan.option induct_rule));
 
 end;