# HG changeset patch
# User boehmes
# Date 1265135194 -3600
# Node ID cc39103321833f216c4d2e2df4feac56ca713d09
# Parent  97903dadf5ffe193180abfad870ba6c045784400# Parent  e3194b70f24b81aca273f34fba91a77d246c12a2
merged

diff -r 97903dadf5ff -r cc3910332183 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/FOL/FOL.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -383,6 +383,7 @@
     val atomize = @{thms induct_atomize}
     val rulify = @{thms induct_rulify}
     val rulify_fallback = @{thms induct_rulify_fallback}
+    val equal_def = @{thm induct_equal_def}
     fun dest_def _ = NONE
     fun trivial_tac _ = no_tac
   );
diff -r 97903dadf5ff -r cc3910332183 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -915,23 +915,15 @@
     assume "G \<turnstile> m member_of C"
     then show "n=m"
     proof (cases)
-      case (Immediate m' _)
-      with eqid 
-      have "m=m'"
-           "memberid n = memberid m" 
-           "G\<turnstile> mbr m declared_in C" 
-           "declclass m = C"
-        by auto
-      with member_n   
+      case Immediate
+      with eqid member_n
       show ?thesis
         by (cases n, cases m) 
            (auto simp add: declared_in_def 
                            cdeclaredmethd_def cdeclaredfield_def
                     split: memberdecl.splits)
     next
-      case (Inherited m' _ _)
-      then have "G\<turnstile> memberid m undeclared_in C"
-        by simp
+      case Inherited
       with eqid member_n
       show ?thesis
         by (cases n) (auto dest: declared_not_undeclared)
@@ -1656,10 +1648,7 @@
     from member_of
     show "?Methd C"
     proof (cases)
-      case (Immediate membr Ca)
-      then have "Ca=C" "membr = method sig m" and 
-                "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
-        by (cases m,auto)
+      case Immediate
       with clsC 
       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
         by (cases m)
@@ -1669,13 +1658,12 @@
       show ?thesis
         by (simp add: methd_rec)
     next
-      case (Inherited membr Ca S)
+      case (Inherited S)
       with clsC
-      have eq_Ca_C: "Ca=C" and
-            undecl: "G\<turnstile>mid sig undeclared_in C" and
+      have  undecl: "G\<turnstile>mid sig undeclared_in C" and
              super: "G \<turnstile>Methd sig m member_of (super c)"
         by (auto dest: subcls1D)
-      from eq_Ca_C clsC undecl 
+      from clsC undecl 
       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
         by (auto simp add: undeclared_in_def cdeclaredmethd_def
                     intro: table_of_mapconst_NoneI)
diff -r 97903dadf5ff -r cc3910332183 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/HOL.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -1453,6 +1453,7 @@
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
+  val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   val trivial_tac = match_tac @{thms induct_trueI}
diff -r 97903dadf5ff -r cc3910332183 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/IMP/Transition.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -205,20 +205,16 @@
     (is "\<exists>i j s'. ?Q i j s'")
   proof (cases set: evalc1)
     case Semi1
-    then obtain s' where
-        "co = Some c2" and "s''' = s'" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-      by auto
-    with 1 n have "?Q 1 n s'" by simp
+    from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
+    have "?Q 1 n s'''" by simp
     thus ?thesis by blast
   next
-    case Semi2
-    then obtain c1' s' where
-        "co = Some (c1'; c2)" "s''' = s'" and
-        c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
-      by auto
-    with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
+    case (Semi2 c1')
+    note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
+    with `co = Some (c1'; c2)` and n
+    have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
     with Suc.hyps obtain i j s0 where
-        c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
+        c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
         c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
         i:   "n = i+j"
       by fast
@@ -228,7 +224,7 @@
     with c2 i
     have "?Q (i+1) j s0" by simp
     thus ?thesis by blast
-  qed auto -- "the remaining cases cannot occur"
+  qed
 qed
 
 
diff -r 97903dadf5ff -r cc3910332183 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/Lambda/Eta.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -273,13 +273,13 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (abs r u)
-    hence "r \<rightarrow>\<^sub>\<eta> s'" by simp
-    then obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
+    case (abs r)
+    from `r \<rightarrow>\<^sub>\<eta> s'`
+    obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
     from r have "Abs r => Abs t'" ..
     moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
     ultimately show ?thesis using abs by simp iprover
-  qed simp_all
+  qed
 next
   case (app u u' t t')
   from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
@@ -291,20 +291,20 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (appL s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> u" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
+    case (appL s')
+    from `s' \<rightarrow>\<^sub>\<eta> u`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
     from s' and app have "s' \<degree> t => r \<degree> t'" by simp
     moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
     ultimately show ?thesis using appL by simp iprover
   next
-    case (appR s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
+    case (appR s')
+    from `s' \<rightarrow>\<^sub>\<eta> t`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
     from s' and app have "u \<degree> s' => u' \<degree> r" by simp
     moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
     ultimately show ?thesis using appR by simp iprover
-  qed simp
+  qed
 next
   case (beta u u' t t')
   from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
@@ -316,9 +316,8 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (appL s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> Abs u" by simp
-    thus ?thesis
+    case (appL s')
+    from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis
     proof cases
       case (eta s'' dummy)
       have "Abs (lift u 1) = lift (Abs u) 0" by simp
@@ -332,23 +331,23 @@
       with s have "s => u'[t'/0]" by simp
       thus ?thesis by iprover
     next
-      case (abs r r')
-      hence "r \<rightarrow>\<^sub>\<eta> u" by simp
-      then obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
+      case (abs r)
+      from `r \<rightarrow>\<^sub>\<eta> u`
+      obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
       from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
       moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
         by (rule rtrancl_eta_subst')
       ultimately show ?thesis using abs and appL by simp iprover
-    qed simp_all
+    qed
   next
-    case (appR s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
+    case (appR s')
+    from `s' \<rightarrow>\<^sub>\<eta> t`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
     from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
     moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
       by (rule rtrancl_eta_subst'')
     ultimately show ?thesis using appR by simp iprover
-  qed simp
+  qed
 qed
 
 theorem eta_postponement':
diff -r 97903dadf5ff -r cc3910332183 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Tue Feb 02 19:26:34 2010 +0100
@@ -575,13 +575,13 @@
   and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
   shows P using ty
 proof cases
-  case (Abs x' T' \<Gamma>' t' U)
+  case (Abs x' T' t' U)
   obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
     by (rule exists_fresh) (auto intro: fin_supp)
   from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
   have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
-  from `(x', T') # \<Gamma>' \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>'"
+  from `(x', T') # \<Gamma> \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>"
     by (auto dest: valid_typing)
   have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
   also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
@@ -592,10 +592,10 @@
   then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
     by (simp_all add: trm.inject alpha)
   from Abs T have "S = T \<rightarrow> U" by simp
-  moreover from `(x', T') # \<Gamma>' \<turnstile> t' : U`
-  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma>' \<turnstile> t' : U)"
+  moreover from `(x', T') # \<Gamma> \<turnstile> t' : U`
+  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma> \<turnstile> t' : U)"
     by (simp add: perm_bool)
-  with T t y `\<Gamma> = \<Gamma>'` x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
+  with T t y x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
     by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
   ultimately show ?thesis by (rule R)
 qed simp_all
@@ -764,7 +764,7 @@
   and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
   shows P using ty
 proof cases
-  case (Let p' t' \<Gamma>' T \<Delta> u' U')
+  case (Let p' t' T \<Delta> u')
   then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
     by (auto intro: valid_typing valid_app_freshs)
   with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
@@ -776,7 +776,7 @@
   moreover from Let have "pat_type p = pat_type p'"
     by (simp add: trm.inject)
   moreover note distinct
-  moreover from `\<Delta> @ \<Gamma>' \<turnstile> u' : U'` have "valid (\<Delta> @ \<Gamma>')"
+  moreover from `\<Delta> @ \<Gamma> \<turnstile> u' : U` have "valid (\<Delta> @ \<Gamma>)"
     by (rule valid_typing)
   then have "valid \<Delta>" by (rule valid_appD)
   with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"
diff -r 97903dadf5ff -r cc3910332183 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Feb 02 19:26:34 2010 +0100
@@ -72,7 +72,7 @@
     term list -> (binding * mixfix) list ->
     local_theory -> inductive_result * local_theory
   val declare_rules: binding -> bool -> bool -> string list ->
-    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
+    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
@@ -411,7 +411,7 @@
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
           |> rulify
           |> singleton (ProofContext.export ctxt'' ctxt),
-         map #2 c_intrs)
+         map #2 c_intrs, length Ts)
       end
 
    in map prove_elim cs end;
@@ -724,11 +724,12 @@
     val (((_, elims'), (_, [induct'])), lthy2) =
       lthy1 |>
       Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
-      fold_map (fn (name, (elim, cases)) =>
+      fold_map (fn (name, (elim, cases, k)) =>
         Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             [Attrib.internal (K (Rule_Cases.case_names cases)),
              Attrib.internal (K (Rule_Cases.consumes 1)),
+             Attrib.internal (K (Rule_Cases.constraints k)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
diff -r 97903dadf5ff -r cc3910332183 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Tue Feb 02 19:26:34 2010 +0100
@@ -522,7 +522,8 @@
       Inductive.declare_rules rec_name coind no_ind cnames
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
-           map fst (fst (Rule_Cases.get th)))) elims)
+           map fst (fst (Rule_Cases.get th)),
+           Rule_Cases.get_constraints th)) elims)
         raw_induct' lthy3;
   in
     ({intrs = intrs', elims = elims', induct = induct,
diff -r 97903dadf5ff -r cc3910332183 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Feb 02 19:26:34 2010 +0100
@@ -288,6 +288,8 @@
   setup (Binding.name "folded") folded "folded definitions" #>
   setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
+  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
+    "number of equality constraints" #>
   setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
     "named rule cases" #>
   setup (Binding.name "case_conclusion")
diff -r 97903dadf5ff -r cc3910332183 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Tue Feb 02 19:26:34 2010 +0100
@@ -34,6 +34,8 @@
   val get_consumes: thm -> int
   val consumes: int -> attribute
   val consumes_default: int -> attribute
+  val get_constraints: thm -> int
+  val constraints: int -> attribute
   val name: string list -> thm -> thm
   val case_names: string list -> attribute
   val case_conclusion: string * string list -> attribute
@@ -236,6 +238,30 @@
 
 
 
+(** equality constraints **)
+
+val constraints_tagN = "constraints";
+
+fun lookup_constraints th =
+  (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
+    NONE => NONE
+  | SOME s =>
+      (case Lexicon.read_nat s of SOME n => SOME n
+      | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
+
+fun get_constraints th = the_default 0 (lookup_constraints th);
+
+fun put_constraints NONE th = th
+  | put_constraints (SOME n) th = th
+      |> Thm.untag_rule constraints_tagN
+      |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
+
+val save_constraints = put_constraints o lookup_constraints;
+
+fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
+
+
+
 (** case names **)
 
 val implode_args = space_implode ";";
@@ -308,6 +334,7 @@
 
 fun save th =
   save_consumes th #>
+  save_constraints th #>
   save_case_names th #>
   save_case_concls th #>
   save_inner_rule th;
diff -r 97903dadf5ff -r cc3910332183 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Feb 02 19:10:48 2010 +0100
+++ b/src/Tools/induct.ML	Tue Feb 02 19:26:34 2010 +0100
@@ -10,6 +10,7 @@
   val atomize: thm list
   val rulify: thm list
   val rulify_fallback: thm list
+  val equal_def: thm
   val dest_def: term -> (term * term) option
   val trivial_tac: int -> tactic
 end;
@@ -69,7 +70,7 @@
   val rotate_tac: int -> int -> int -> tactic
   val internalize: int -> thm -> thm
   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
-  val cases_tac: Proof.context -> term option list list -> thm option ->
+  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
   val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
@@ -410,6 +411,38 @@
   | trace_rules ctxt _ rules = Method.trace ctxt rules;
 
 
+(* mark equality constraints in cases rule *)
+
+val equal_def' = Thm.symmetric Data.equal_def;
+
+fun mark_constraints n ctxt = Conv.fconv_rule
+  (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
+     (MetaSimplifier.rewrite false [equal_def']))) ctxt));
+
+val unmark_constraints = Conv.fconv_rule
+  (MetaSimplifier.rewrite true [Data.equal_def]);
+
+(* simplify *)
+
+fun simplify_conv' ctxt =
+  Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
+
+fun simplify_conv ctxt ct =
+  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
+    (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
+  else Conv.all_conv ct;
+
+fun gen_simplified_rule cv ctxt =
+  Conv.fconv_rule (Conv.prems_conv ~1 (cv ctxt));
+
+val simplified_rule' = gen_simplified_rule simplify_conv';
+val simplified_rule = gen_simplified_rule simplify_conv;
+
+fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
+
+val trivial_tac = Data.trivial_tac;
+
+
 
 (** cases method **)
 
@@ -431,15 +464,17 @@
 
 in
 
-fun cases_tac ctxt insts opt_rule facts =
+fun cases_tac ctxt simp insts opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
 
     fun inst_rule r =
-      if null insts then `Rule_Cases.get r
-      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
-        |> maps (prep_inst ctxt align_left I)
-        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
+      (if null insts then r
+       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
+         |> maps (prep_inst ctxt align_left I)
+         |> Drule.cterm_instantiate) r) |>
+      (if simp then mark_constraints (Rule_Cases.get_constraints r) ctxt else I) |>
+      pair (Rule_Cases.get r);
 
     val ruleq =
       (case opt_rule of
@@ -453,9 +488,14 @@
       ruleq
       |> Seq.maps (Rule_Cases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
-        CASES (Rule_Cases.make_common (thy,
-            Thm.prop_of (Rule_Cases.internalize_params rule)) cases)
-          (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
+        let val rule' =
+          (if simp then simplified_rule' ctxt #> unmark_constraints else I) rule
+        in
+          CASES (Rule_Cases.make_common (thy,
+              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
+            ((Method.insert_tac more_facts THEN' Tactic.rtac rule' THEN_ALL_NEW
+                (if simp then TRY o trivial_tac else K all_tac)) i) st
+        end)
   end;
 
 end;
@@ -501,22 +541,6 @@
   (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
 
 
-(* simplify *)
-
-fun simplify_conv ctxt ct =
-  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
-    (Conv.try_conv (rulify_defs_conv ctxt) then_conv
-       Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)))) ct
-  else Conv.all_conv ct;
-
-fun simplified_rule ctxt thm =
-  Conv.fconv_rule (Conv.prems_conv ~1 (simplify_conv ctxt)) thm;
-
-fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
-
-val trivial_tac = Data.trivial_tac;
-
-
 (* prepare rule *)
 
 fun rule_instance ctxt inst rule =
@@ -870,9 +894,11 @@
 
 val cases_setup =
   Method.setup @{binding cases}
-    (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
-      (fn (insts, opt_rule) => fn ctxt =>
-        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
+    (Args.mode no_simpN --
+      (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+      (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
+        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
+          (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
     "case analysis on types or predicates/sets";
 
 val induct_setup =