1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 09 23:22:56 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Jan 10 18:01:04 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  structure NominalInduct:
     1.6  sig
     1.7 -  val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     1.8 +  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     1.9      (string * typ) list -> (string * typ) list list -> thm list ->
    1.10      thm list -> int -> Rule_Cases.cases_tactic
    1.11    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    1.12 @@ -74,26 +74,29 @@
    1.13            else map (tune o #1) (take (p - n) ps) @ xs;
    1.14        in Logic.list_rename_params (ys, prem) end;
    1.15      fun rename_prems prop =
    1.16 -      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
    1.17 +      let val (As, C) = Logic.strip_horn prop
    1.18        in Logic.list_implies (map rename As, C) end;
    1.19    in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
    1.20  
    1.21  
    1.22  (* nominal_induct_tac *)
    1.23  
    1.24 -fun nominal_induct_tac ctxt def_insts avoiding fixings rules facts =
    1.25 +fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
    1.26    let
    1.27      val thy = ProofContext.theory_of ctxt;
    1.28      val cert = Thm.cterm_of thy;
    1.29  
    1.30      val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    1.31 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    1.32 +    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
    1.33  
    1.34      val finish_rule =
    1.35        split_all_tuples
    1.36        #> rename_params_rule true
    1.37          (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.38 -    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.39 +
    1.40 +    fun rule_cases ctxt r =
    1.41 +      let val r' = if simp then Induct.simplified_rule ctxt r else r
    1.42 +      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
    1.43    in
    1.44      (fn i => fn st =>
    1.45        rules
    1.46 @@ -102,19 +105,32 @@
    1.47        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.48          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.49            (CONJUNCTS (ALLGOALS
    1.50 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
    1.51 -              THEN' Induct.fix_tac defs_ctxt
    1.52 -                (nth concls (j - 1) + more_consumes)
    1.53 -                (nth_list fixings (j - 1))))
    1.54 +            let
    1.55 +              val adefs = nth_list atomized_defs (j - 1);
    1.56 +              val frees = fold (Term.add_frees o prop_of) adefs [];
    1.57 +              val xs = nth_list fixings (j - 1);
    1.58 +              val k = nth concls (j - 1) + more_consumes
    1.59 +            in
    1.60 +              Method.insert_tac (more_facts @ adefs) THEN'
    1.61 +                (if simp then
    1.62 +                   Induct.rotate_tac k (length adefs) THEN'
    1.63 +                   Induct.fix_tac defs_ctxt k
    1.64 +                     (List.partition (member op = frees) xs |> op @)
    1.65 +                 else
    1.66 +                   Induct.fix_tac defs_ctxt k xs)
    1.67 +            end)
    1.68            THEN' Induct.inner_atomize_tac) j))
    1.69          THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
    1.70              Induct.guess_instance ctxt
    1.71                (finish_rule (Induct.internalize more_consumes rule)) i st'
    1.72              |> Seq.maps (fn rule' =>
    1.73 -              CASES (rule_cases rule' cases)
    1.74 +              CASES (rule_cases ctxt rule' cases)
    1.75                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    1.76                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
    1.77 -    THEN_ALL_NEW_CASES Induct.rulify_tac
    1.78 +    THEN_ALL_NEW_CASES
    1.79 +      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
    1.80 +        else K all_tac)
    1.81 +       THEN_ALL_NEW Induct.rulify_tac)
    1.82    end;
    1.83  
    1.84  
    1.85 @@ -128,11 +144,14 @@
    1.86  val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
    1.87  val ruleN = "rule";
    1.88  
    1.89 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
    1.90 +val inst = Scan.lift (Args.$$$ "_") >> K NONE ||
    1.91 +  Args.term >> (SOME o rpair false) ||
    1.92 +  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
    1.93 +    Scan.lift (Args.$$$ ")");
    1.94  
    1.95  val def_inst =
    1.96    ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    1.97 -      -- Args.term) >> SOME ||
    1.98 +      -- (Args.term >> rpair false)) >> SOME ||
    1.99      inst >> Option.map (pair NONE);
   1.100  
   1.101  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   1.102 @@ -153,11 +172,11 @@
   1.103  in
   1.104  
   1.105  val nominal_induct_method =
   1.106 -  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   1.107 -  avoiding -- fixing -- rule_spec >>
   1.108 -  (fn (((x, y), z), w) => fn ctxt =>
   1.109 +  Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   1.110 +  avoiding -- fixing -- rule_spec) >>
   1.111 +  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
   1.112      RAW_METHOD_CASES (fn facts =>
   1.113 -      HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
   1.114 +      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
   1.115  
   1.116  end;
   1.117  

     2.1 --- a/src/Tools/induct.ML	Sat Jan 09 23:22:56 2010 +0100
     2.2 +++ b/src/Tools/induct.ML	Sun Jan 10 18:01:04 2010 +0100
     2.3 @@ -10,6 +10,8 @@
     2.4    val atomize: thm list
     2.5    val rulify: thm list
     2.6    val rulify_fallback: thm list
     2.7 +  val dest_def: term -> (term * term) option
     2.8 +  val trivial_tac: int -> tactic
     2.9  end;
    2.10  
    2.11  signature INDUCT =
    2.12 @@ -42,6 +44,9 @@
    2.13    val coinduct_type: string -> attribute
    2.14    val coinduct_pred: string -> attribute
    2.15    val coinduct_del: attribute
    2.16 +  val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
    2.17 +  val add_simp_rule: attribute
    2.18 +  val no_simpN: string
    2.19    val casesN: string
    2.20    val inductN: string
    2.21    val coinductN: string
    2.22 @@ -50,19 +55,24 @@
    2.23    val setN: string
    2.24    (*proof methods*)
    2.25    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    2.26 -  val add_defs: (binding option * term) option list -> Proof.context ->
    2.27 +  val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
    2.28      (term option list * thm list) * Proof.context
    2.29    val atomize_term: theory -> term -> term
    2.30 +  val atomize_cterm: conv
    2.31    val atomize_tac: int -> tactic
    2.32    val inner_atomize_tac: int -> tactic
    2.33    val rulified_term: thm -> theory * term
    2.34    val rulify_tac: int -> tactic
    2.35 +  val simplified_rule: Proof.context -> thm -> thm
    2.36 +  val simplify_tac: Proof.context -> int -> tactic
    2.37 +  val trivial_tac: int -> tactic
    2.38 +  val rotate_tac: int -> int -> int -> tactic
    2.39    val internalize: int -> thm -> thm
    2.40    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    2.41    val cases_tac: Proof.context -> term option list list -> thm option ->
    2.42      thm list -> int -> cases_tactic
    2.43    val get_inductT: Proof.context -> term option list list -> thm list list
    2.44 -  val induct_tac: Proof.context -> (binding option * term) option list list ->
    2.45 +  val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    2.46      (string * typ) list list -> term option list -> thm list option ->
    2.47      thm list -> int -> cases_tactic
    2.48    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    2.49 @@ -107,6 +117,77 @@
    2.50  
    2.51  
    2.52  
    2.53 +(** constraint simplification **)
    2.54 +
    2.55 +(* rearrange parameters and premises to allow application of one-point-rules *)
    2.56 +
    2.57 +fun swap_params_conv ctxt i j cv =
    2.58 +  let
    2.59 +    fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
    2.60 +      | conv1 k ctxt =
    2.61 +          Conv.rewr_conv @{thm swap_params} then_conv
    2.62 +          Conv.forall_conv (conv1 (k-1) o snd) ctxt
    2.63 +    fun conv2 0 ctxt = conv1 j ctxt
    2.64 +      | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
    2.65 +  in conv2 i ctxt end;
    2.66 +
    2.67 +fun swap_prems_conv 0 = Conv.all_conv
    2.68 +  | swap_prems_conv i =
    2.69 +      Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
    2.70 +      Conv.rewr_conv Drule.swap_prems_eq
    2.71 +
    2.72 +fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
    2.73 +
    2.74 +fun find_eq ctxt t =
    2.75 +  let
    2.76 +    val l = length (Logic.strip_params t);
    2.77 +    val Hs = Logic.strip_assums_hyp t;
    2.78 +    fun find (i, t) =
    2.79 +      case Data.dest_def (drop_judgment ctxt t) of
    2.80 +        SOME (Bound j, _) => SOME (i, j)
    2.81 +      | SOME (_, Bound j) => SOME (i, j)
    2.82 +      | _ => NONE
    2.83 +  in
    2.84 +    case get_first find (map_index I Hs) of
    2.85 +      NONE => NONE
    2.86 +    | SOME (0, 0) => NONE
    2.87 +    | SOME (i, j) => SOME (i, l-j-1, j)
    2.88 +  end;
    2.89 +
    2.90 +fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of
    2.91 +    NONE => NONE
    2.92 +  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
    2.93 +
    2.94 +val rearrange_eqs_simproc = Simplifier.simproc
    2.95 +  (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
    2.96 +  (fn thy => fn ss => fn t =>
    2.97 +     mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t))
    2.98 +
    2.99 +(* rotate k premises to the left by j, skipping over first j premises *)
   2.100 +
   2.101 +fun rotate_conv 0 j 0 = Conv.all_conv
   2.102 +  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1)
   2.103 +  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k);
   2.104 +
   2.105 +fun rotate_tac j 0 = K all_tac
   2.106 +  | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv
   2.107 +      j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
   2.108 +
   2.109 +(* rulify operators around definition *)
   2.110 +
   2.111 +fun rulify_defs_conv ctxt ct =
   2.112 +  if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
   2.113 +    not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
   2.114 +  then
   2.115 +    (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
   2.116 +     Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
   2.117 +       (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
   2.118 +     Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
   2.119 +       Conv.try_conv (rulify_defs_conv ctxt)) ct
   2.120 +  else Conv.no_conv ct;
   2.121 +
   2.122 +
   2.123 +
   2.124  (** induct data **)
   2.125  
   2.126  (* rules *)
   2.127 @@ -132,23 +213,25 @@
   2.128  
   2.129  structure InductData = Generic_Data
   2.130  (
   2.131 -  type T = (rules * rules) * (rules * rules) * (rules * rules);
   2.132 +  type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
   2.133    val empty =
   2.134      ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   2.135       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   2.136 -     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   2.137 +     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
   2.138 +     empty_ss addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]);
   2.139    val extend = I;
   2.140 -  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
   2.141 -      ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
   2.142 +  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
   2.143 +      ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
   2.144      ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
   2.145 -      (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
   2.146 -      (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)));
   2.147 +     (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
   2.148 +     (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)),
   2.149 +     merge_ss (simpset1, simpset2));
   2.150  );
   2.151  
   2.152  val get_local = InductData.get o Context.Proof;
   2.153  
   2.154  fun dest_rules ctxt =
   2.155 -  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   2.156 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
   2.157      {type_cases = Item_Net.content casesT,
   2.158       pred_cases = Item_Net.content casesP,
   2.159       type_induct = Item_Net.content inductT,
   2.160 @@ -158,7 +241,7 @@
   2.161    end;
   2.162  
   2.163  fun print_rules ctxt =
   2.164 -  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   2.165 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
   2.166     [pretty_rules ctxt "coinduct type:" coinductT,
   2.167      pretty_rules ctxt "coinduct pred:" coinductP,
   2.168      pretty_rules ctxt "induct type:" inductT,
   2.169 @@ -206,9 +289,10 @@
   2.170  fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
   2.171    fold Item_Net.remove (filter_rules rs th) rs))));
   2.172  
   2.173 -fun map1 f (x, y, z) = (f x, y, z);
   2.174 -fun map2 f (x, y, z) = (x, f y, z);
   2.175 -fun map3 f (x, y, z) = (x, y, f z);
   2.176 +fun map1 f (x, y, z, s) = (f x, y, z, s);
   2.177 +fun map2 f (x, y, z, s) = (x, f y, z, s);
   2.178 +fun map3 f (x, y, z, s) = (x, y, f z, s);
   2.179 +fun map4 f (x, y, z, s) = (x, y, z, f s);
   2.180  
   2.181  fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
   2.182  fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
   2.183 @@ -234,12 +318,17 @@
   2.184  val coinduct_pred = mk_att add_coinductP consumes1;
   2.185  val coinduct_del = del_att map3;
   2.186  
   2.187 +fun map_simpset f = InductData.map (map4 f);
   2.188 +fun add_simp_rule (ctxt, thm) =
   2.189 +  (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
   2.190 +
   2.191  end;
   2.192  
   2.193  
   2.194  
   2.195  (** attribute syntax **)
   2.196  
   2.197 +val no_simpN = "no_simp";
   2.198  val casesN = "cases";
   2.199  val inductN = "induct";
   2.200  val coinductN = "coinduct";
   2.201 @@ -268,7 +357,9 @@
   2.202    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
   2.203      "declaration of induction rule" #>
   2.204    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   2.205 -    "declaration of coinduction rule";
   2.206 +    "declaration of coinduction rule" #>
   2.207 +  Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
   2.208 +    "declaration of rules for simplifying induction or cases rules";
   2.209  
   2.210  end;
   2.211  
   2.212 @@ -362,7 +453,8 @@
   2.213        ruleq
   2.214        |> Seq.maps (Rule_Cases.consume [] facts)
   2.215        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   2.216 -        CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
   2.217 +        CASES (Rule_Cases.make_common (thy,
   2.218 +            Thm.prop_of (Rule_Cases.internalize_params rule)) cases)
   2.219            (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   2.220    end;
   2.221  
   2.222 @@ -409,6 +501,22 @@
   2.223    (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   2.224  
   2.225  
   2.226 +(* simplify *)
   2.227 +
   2.228 +fun simplify_conv ctxt ct =
   2.229 +  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
   2.230 +    (Conv.try_conv (rulify_defs_conv ctxt) then_conv
   2.231 +       Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)))) ct
   2.232 +  else Conv.all_conv ct;
   2.233 +
   2.234 +fun simplified_rule ctxt thm =
   2.235 +  Conv.fconv_rule (Conv.prems_conv ~1 (simplify_conv ctxt)) thm;
   2.236 +
   2.237 +fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
   2.238 +
   2.239 +val trivial_tac = Data.trivial_tac;
   2.240 +
   2.241 +
   2.242  (* prepare rule *)
   2.243  
   2.244  fun rule_instance ctxt inst rule =
   2.245 @@ -548,11 +656,19 @@
   2.246  
   2.247  fun add_defs def_insts =
   2.248    let
   2.249 -    fun add (SOME (SOME x, t)) ctxt =
   2.250 +    fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
   2.251 +      | add (SOME (SOME x, (t, _))) ctxt =
   2.252            let val ([(lhs, (_, th))], ctxt') =
   2.253              LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
   2.254            in ((SOME lhs, [th]), ctxt') end
   2.255 -      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
   2.256 +      | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
   2.257 +      | add (SOME (NONE, (t, _))) ctxt =
   2.258 +          let
   2.259 +            val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
   2.260 +            val ([(lhs, (_, th))], ctxt') =
   2.261 +              LocalDefs.add_defs [((Binding.name s, NoSyn),
   2.262 +                (Thm.empty_binding, t))] ctxt
   2.263 +          in ((SOME lhs, [th]), ctxt') end
   2.264        | add NONE ctxt = ((NONE, []), ctxt);
   2.265    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
   2.266  
   2.267 @@ -576,12 +692,12 @@
   2.268  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   2.269    | get_inductP _ _ = [];
   2.270  
   2.271 -fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   2.272 +fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
   2.273    let
   2.274      val thy = ProofContext.theory_of ctxt;
   2.275  
   2.276      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   2.277 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   2.278 +    val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
   2.279  
   2.280      fun inst_rule (concls, r) =
   2.281        (if null insts then `Rule_Cases.get r
   2.282 @@ -601,8 +717,10 @@
   2.283            |> tap (trace_rules ctxt inductN o map #2)
   2.284            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   2.285  
   2.286 -    fun rule_cases rule =
   2.287 -      Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
   2.288 +    fun rule_cases ctxt rule =
   2.289 +      let val rule' = (if simp then simplified_rule ctxt else I)
   2.290 +        (Rule_Cases.internalize_params rule);
   2.291 +      in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end;
   2.292    in
   2.293      (fn i => fn st =>
   2.294        ruleq
   2.295 @@ -610,19 +728,32 @@
   2.296        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   2.297          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   2.298            (CONJUNCTS (ALLGOALS
   2.299 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   2.300 -              THEN' fix_tac defs_ctxt
   2.301 -                (nth concls (j - 1) + more_consumes)
   2.302 -                (nth_list arbitrary (j - 1))))
   2.303 +            let
   2.304 +              val adefs = nth_list atomized_defs (j - 1);
   2.305 +              val frees = fold (Term.add_frees o prop_of) adefs [];
   2.306 +              val xs = nth_list arbitrary (j - 1);
   2.307 +              val k = nth concls (j - 1) + more_consumes
   2.308 +            in
   2.309 +              Method.insert_tac (more_facts @ adefs) THEN'
   2.310 +                (if simp then
   2.311 +                   rotate_tac k (length adefs) THEN'
   2.312 +                   fix_tac defs_ctxt k
   2.313 +                     (List.partition (member op = frees) xs |> op @)
   2.314 +                 else
   2.315 +                   fix_tac defs_ctxt k xs)
   2.316 +             end)
   2.317            THEN' inner_atomize_tac) j))
   2.318          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
   2.319              guess_instance ctxt (internalize more_consumes rule) i st'
   2.320              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   2.321              |> Seq.maps (fn rule' =>
   2.322 -              CASES (rule_cases rule' cases)
   2.323 +              CASES (rule_cases ctxt rule' cases)
   2.324                  (Tactic.rtac rule' i THEN
   2.325                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   2.326 -    THEN_ALL_NEW_CASES rulify_tac
   2.327 +    THEN_ALL_NEW_CASES
   2.328 +      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
   2.329 +        else K all_tac)
   2.330 +       THEN_ALL_NEW rulify_tac)
   2.331    end;
   2.332  
   2.333  
   2.334 @@ -672,7 +803,8 @@
   2.335          guess_instance ctxt rule i st
   2.336          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   2.337          |> Seq.maps (fn rule' =>
   2.338 -          CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
   2.339 +          CASES (Rule_Cases.make_common (thy,
   2.340 +              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   2.341              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   2.342    end;
   2.343  
   2.344 @@ -711,10 +843,15 @@
   2.345  
   2.346  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   2.347  
   2.348 +val inst' = Scan.lift (Args.$$$ "_") >> K NONE ||
   2.349 +  Args.term >> (SOME o rpair false) ||
   2.350 +  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
   2.351 +    Scan.lift (Args.$$$ ")");
   2.352 +
   2.353  val def_inst =
   2.354    ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
   2.355 -      -- Args.term) >> SOME ||
   2.356 -    inst >> Option.map (pair NONE);
   2.357 +      -- (Args.term >> rpair false)) >> SOME ||
   2.358 +    inst' >> Option.map (pair NONE);
   2.359  
   2.360  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   2.361    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
   2.362 @@ -740,11 +877,11 @@
   2.363  
   2.364  val induct_setup =
   2.365    Method.setup @{binding induct}
   2.366 -    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   2.367 -      (arbitrary -- taking -- Scan.option induct_rule) >>
   2.368 -      (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
   2.369 +    (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   2.370 +      (arbitrary -- taking -- Scan.option induct_rule)) >>
   2.371 +      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
   2.372          RAW_METHOD_CASES (fn facts =>
   2.373 -          Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
   2.374 +          Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
   2.375      "induction on types or predicates/sets";
   2.376  
   2.377  val coinduct_setup =