Transitive_Closure: added consumes and case_names attributes
Isar: fixed parameter name handling in simulatneous induction
which I had not done properly 2 years ago.

--- a/src/HOL/Transitive_Closure.thy	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Feb 21 08:43:08 2004 +0100
@@ -70,11 +70,10 @@
   thus ?thesis by rules
 qed
 
-ML_setup {*
-  bind_thm ("rtrancl_induct2", split_rule
-    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
-*}
-
+lemmas rtrancl_induct2 =
+  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+                 consumes 1, case_names refl step]
+ 
 lemma trans_rtrancl: "trans(r^*)"
   -- {* transitivity of transitive closure!! -- by induction *}
 proof (rule transI)
@@ -165,7 +164,7 @@
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
 
-theorem converse_rtrancl_induct:
+theorem converse_rtrancl_induct[consumes 1]:
   assumes major: "(a, b) : r^*"
     and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
   shows "P a"
@@ -175,10 +174,9 @@
     by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
 qed
 
-ML_setup {*
-  bind_thm ("converse_rtrancl_induct2", split_rule
-    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
-*}
+lemmas converse_rtrancl_induct2 =
+  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+                 consumes 1, case_names refl step]
 
 lemma converse_rtranclE:
   "[| (x,z):r^*;

--- a/src/Provers/induct_method.ML	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/Provers/induct_method.ML	Sat Feb 21 08:43:08 2004 +0100
@@ -111,7 +111,7 @@
 
     fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
       (Method.multi_resolves (take (n, facts)) [th]);
-  in resolveq_cases_tac (RuleCases.make (if is_open then None else Some 0) None) (Seq.flat (Seq.map prep_rule ruleq)) end;
+  in resolveq_cases_tac (RuleCases.make is_open None) (Seq.flat (Seq.map prep_rule ruleq)) end;
 
 in
 
@@ -225,24 +225,15 @@
 
 fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
 
-fun nof_params i st =
-  let val Bi = RuleCases.hhf_nth_subgoal (sign_of_thm st) (i,prop_of st)
-  in length(Logic.strip_params Bi) end
-  handle TERM("strip_prems",_) => 0 (* in case i is out of range *)
-
 fun resolveq_cases_tac' make is_open ruleq i st =
-  let val n = nof_params i st
-      val mk = make (if is_open then None else Some n)
-  in
   ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
     |> (Method.insert_tac more_facts THEN' atomize_tac) i
     |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
           st' |> Tactic.rtac rule' i
-          |> Seq.map (rpair (mk (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
+          |> Seq.map (rpair (make is_open (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
       |> Seq.flat)
     |> Seq.flat)
-  |> Seq.flat
-  end;
+  |> Seq.flat;
 
 infix 1 THEN_ALL_NEW_CASES;
 

--- a/src/Pure/Isar/proof.ML	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Feb 21 08:43:08 2004 +0100
@@ -690,7 +690,7 @@
       (after_qed o map_context gen_binds, pr)))
     |> map_context (ProofContext.add_cases
      (if length props = 1 then
-      RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
+      RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
       else [(rule_contextN, RuleCases.empty)]))
     |> auto_bind_goal props
     |> (if is_chain state then use_facts else reset_facts)

--- a/src/Pure/Isar/rule_cases.ML	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Feb 21 08:43:08 2004 +0100
@@ -17,8 +17,7 @@
   val add: thm -> thm * (string list * int)
   type T
   val empty: T
-  val hhf_nth_subgoal: Sign.sg -> int * term -> term
-  val make: int option -> term option -> Sign.sg * term -> string list -> (string * T) list
+  val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
 end;
@@ -99,22 +98,15 @@
 
 fun nth_subgoal(i,prop) =
   hd (#1 (Logic.strip_prems (i, [], prop)));
-
-fun hhf_nth_subgoal sg = Drule.norm_hhf sg o nth_subgoal
   
-(* open_params = None
-   ==> all parameters are "open", ie their default names are used.
-   open_params = Some k
-   ==> only the last k parameters, the ones coming from the original
-   goal, not from the induction rule, are "open"
-*)
-fun prep_case open_params split sg prop name i =
+fun prep_case is_open split sg prop name i =
   let
-    val Bi = hhf_nth_subgoal sg (i,prop);
+    val Bi = Drule.norm_hhf sg (nth_subgoal(i,prop));
     val all_xs = Logic.strip_params Bi
-    val n = length all_xs - (if_none open_params 0)
+    val n = (case split of None => length all_xs
+             | Some t => length (Logic.strip_params(nth_subgoal(i,t))))
     val (ind_xs, goal_xs) = splitAt(n,all_xs)
-    val rename = if is_none open_params then I else apfst Syntax.internal
+    val rename = if is_open then I else apfst Syntax.internal
     val xs = map rename ind_xs @ goal_xs
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
     val named_asms =
@@ -127,9 +119,9 @@
     val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
   in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
 
-fun make open_params split (sg, prop) names =
+fun make is_open split (sg, prop) names =
   let val nprems = Logic.count_prems (prop, 0) in
-    foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1))
+    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
       (Library.drop (length names - nprems, names), ([], length names)) |> #1
   end;