# HG changeset patch
# User wenzelm
# Date 963481442 -7200
# Node ID c5cda71de65d0e970a3c2e1b2ca1dde0324abee8
# Parent  7d9b562a750b25e941b25576323c518ef66ec868
added simp_case_tac;
proper handling of case names with simplification;
support "(opaque)" mode;
tuned;

diff -r 7d9b562a750b -r c5cda71de65d src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Thu Jul 13 11:42:11 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Thu Jul 13 11:44:02 2000 +0200
@@ -26,8 +26,7 @@
   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;
 
@@ -168,15 +167,11 @@
 
 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;
 
@@ -201,10 +196,23 @@
     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 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));
 
-fun cases_tac (ctxt, (simplified, args)) facts =
+    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;
@@ -212,8 +220,6 @@
     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)));
@@ -229,15 +235,17 @@
           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
 
@@ -296,7 +304,7 @@
       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;
@@ -330,15 +338,15 @@
           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
@@ -359,6 +367,7 @@
 
 val simplifiedN = "simplified";
 val strippedN = "stripped";
+val opaqN = "opaque";
 
 val typeN = "type";
 val setN = "set";
@@ -413,9 +422,11 @@
 
 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;