support for split assumptions in cases (hyps vs. prems);

--- a/NEWS	Fri Jul 26 21:07:57 2002 +0200
+++ b/NEWS	Fri Jul 26 21:09:39 2002 +0200
@@ -15,6 +15,10 @@
 context; potential INCOMPATIBILITY, use "(open)" option to fall back
 on the old view without predicates;
 
+* improved induct method: assumptions introduced by case "foo" are
+split into "foo.hyps" (from the rule) and "foo.prems" (from the goal
+statement); "foo" still refers to all facts collectively;
+
 * improved thms_containing: proper indexing of facts instead of raw
 theorems; check validity of results wrt. current name space; include
 local facts of proof configuration (also covers active locales); an

--- a/doc-src/IsarRef/generic.tex	Fri Jul 26 21:07:57 2002 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Jul 26 21:09:39 2002 +0200
@@ -1227,6 +1227,12 @@
 $\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
 
+In induction proofs, local assumptions introduced by cases are split into two
+different kinds: $hyps$ stemming from the rule and $prems$ from the goal
+statement.  This is reflected in the extracted cases accordingly, so invoking
+``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and
+$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list.
+
 \medskip
 
 Facts presented to either method are consumed according to the number of

--- a/src/Provers/induct_method.ML	Fri Jul 26 21:07:57 2002 +0200
+++ b/src/Provers/induct_method.ML	Fri Jul 26 21:09:39 2002 +0200
@@ -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 open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
+  in resolveq_cases_tac (RuleCases.make open_parms None) (Seq.flat (Seq.map prep_rule ruleq)) end;
 
 in
 
@@ -186,7 +186,7 @@
             (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
           |> Drule.implies_intr_list cprems
           |> Drule.standard'
-          |> RuleCases.save th]
+          |> RuleCases.save r]
         end;
 
 
@@ -230,7 +230,7 @@
     |> (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 (make (rulified_term rule') cases)))
+          |> Seq.map (rpair (make (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
       |> Seq.flat)
     |> Seq.flat)
   |> Seq.flat;
@@ -329,7 +329,7 @@
 val term_dummy = Scan.unless (Scan.lift kind_inst)
   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
 
-val instss = Args.and_list (Scan.repeat1 term_dummy);
+val instss = Args.and_list (Scan.repeat term_dummy);
 
 in
 

--- a/src/Pure/Isar/proof.ML	Fri Jul 26 21:07:57 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jul 26 21:09:39 2002 +0200
@@ -621,10 +621,17 @@
   let
     val (state', (lets, asms)) =
       map_context_result (ProofContext.apply_case (get_case state name xs)) state;
+    val assumptions = asms |> map (fn (a, ts) =>
+      ((if a = "" then "" else NameSpace.append name a, atts), map (rpair ([], [])) ts));
+    val qnames = filter_out (equal "") (map (#1 o #1) assumptions);
   in
     state'
     |> add_binds_i lets
-    |> assume_i [((name, atts), map (rpair ([], [])) asms)]
+    |> map_context (ProofContext.qualified true)
+    |> assume_i assumptions
+    |> map_context (ProofContext.hide_thms false qnames)
+    |> (fn st => simple_have_thms name (the_facts st) st)
+    |> map_context (ProofContext.restore_qualified (context_of state))
   end;
 
 
@@ -678,7 +685,7 @@
       (after_qed o map_context gen_binds, pr)))
     |> map_context (ProofContext.add_cases
      (if length props = 1 then
-      RuleCases.make true (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/proof_context.ML	Fri Jul 26 21:07:57 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 26 21:09:39 2002 +0200
@@ -79,6 +79,7 @@
   val cond_extern: context -> string -> xstring
   val qualified: bool -> context -> context
   val restore_qualified: context -> context -> context
+  val hide_thms: bool -> string list -> context -> context
   val put_thm: string * thm -> context -> context
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
@@ -109,7 +110,8 @@
   val bind_skolem: context -> string list -> term -> term
   val get_case: context -> string -> string option list -> RuleCases.T
   val add_cases: (string * RuleCases.T) list -> context -> context
-  val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
+  val apply_case: RuleCases.T -> context
+    -> context * ((indexname * term option) list * (string * term list) list)
   val pretty_term: context -> term -> Pretty.T
   val pretty_typ: context -> typ -> Pretty.T
   val pretty_sort: context -> sort -> Pretty.T
@@ -946,7 +948,7 @@
 val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I);
 
 
-(* qualified names *)
+(* name space operations *)
 
 fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
 
@@ -956,6 +958,11 @@
 
 fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
 
+fun hide_thms fully names =
+  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
+    (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
+      cases, defs));
+
 
 (* put_thm(s) *)
 
@@ -1201,7 +1208,7 @@
       | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
   in
     if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso
-      null (foldr Term.add_term_vars (assumes, [])) then
+      null (foldr Term.add_term_vars (flat (map #2 assumes), [])) then
         {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
     else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   end;
@@ -1272,7 +1279,7 @@
     fun bind (c, (x, T)) = (c |> fix_i [([x], Some T)], bind_skolem c [x] (Free (x, T)));
     val (ctxt', xs) = foldl_map bind (ctxt, fixes);
     fun app t = foldl Term.betapply (t, xs);
-  in (ctxt', (map (apsnd (apsome app)) binds, map app assumes)) end;
+  in (ctxt', (map (apsnd (apsome app)) binds, map (apsnd (map app)) assumes)) end;
 
 fun pretty_cases (ctxt as Context {cases, ...}) =
   let
@@ -1282,6 +1289,9 @@
       [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
 
+    fun prt_asm (a, ts) = Pretty.block (Pretty.breaks
+      ((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts));
+
     fun prt_sect _ _ _ [] = []
       | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s ::
             flat (Library.separate sep (map (Library.single o prt) xs))))];
@@ -1291,7 +1301,8 @@
         prt_sect "fix" [] (Pretty.str o fst) fixes @
         prt_sect "let" [Pretty.str "and"] prt_let
           (mapfilter (fn (xi, Some t) => Some (xi, t) | _ => None) lets) @
-        prt_sect "assume" [] (Pretty.quote o prt_term) asms));
+        (if forall (null o #2) asms then []
+          else prt_sect "assume" [Pretty.str "and"] prt_asm asms)));
 
     val cases' = rev (Library.gen_distinct Library.eq_fst cases);
   in

--- a/src/Pure/Isar/rule_cases.ML	Fri Jul 26 21:07:57 2002 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri Jul 26 21:09:39 2002 +0200
@@ -17,7 +17,7 @@
   val add: thm -> thm * (string list * int)
   type T
   val empty: T
-  val make: bool -> 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;
@@ -86,23 +86,35 @@
 
 (* prepare cases *)
 
-type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
+type T =
+ {fixes: (string * typ) list,
+  assumes: (string * term list) list,
+  binds: (indexname * term option) list};
+
+val hypsN = "hyps";
+val premsN = "prems";
 
 val empty = {fixes = [], assumes = [], binds = []};
 
-fun prep_case open_parms sg prop name i =
+fun prep_case is_open split sg prop name i =
   let
     val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop))));
-    val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
+    val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi);
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
+    val named_asms =
+      (case split of None => [("", asms)]
+      | Some t =>
+          let val h = length (Logic.strip_assums_hyp
+            (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t)))))
+          in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end);
     val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
     val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
-  in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
+  in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
 
-fun make open_parms (sg, prop) names =
+fun make is_open split (sg, prop) names =
   let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in
-    #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms sg prop name i :: cases, i - 1))
-      (Library.drop (length names - nprems, names), ([], length names)))
+    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;