--- 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
);
--- 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)
--- 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}
--- 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
--- 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':
--- 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')"
--- 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) ||>>
--- 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,
--- 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")
--- 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;
--- 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 =