infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names

--- a/src/HOL/Bali/DefiniteAssignment.thy	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Aug 01 12:08:53 2011 +0200
@@ -1056,8 +1056,7 @@
        (is "PROP ?Hyp Env B t A")  
   proof (induct)
     case Skip 
-    from Skip.prems Skip.hyps 
-    show ?case by cases simp
+    then show ?case by cases simp
   next
     case Expr 
     from Expr.prems Expr.hyps 

--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -91,7 +91,7 @@
       CASES
         (Rule_Cases.make_common
           (Proof_Context.theory_of ctxt,
-           Thm.prop_of (Rule_Cases.internalize_params st)) names)
+           Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names))
         Tactical.all_tac st))
 in
 val setup_boogie_cases = Method.setup @{binding boogie_cases}

--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -158,7 +158,7 @@
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
-    val induct_cases = map fst (fst (Rule_Cases.get (the
+    val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));
     val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>

--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -165,7 +165,7 @@
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
-    val induct_cases = map fst (fst (Rule_Cases.get (the
+    val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));
     val induct_cases' = if null induct_cases then replicate (length intrs) ""
       else induct_cases;

--- a/src/HOL/Tools/inductive_set.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Tools/inductive_set.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -524,7 +524,7 @@
       Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
         (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)),
+           map (fst o fst) (fst (Rule_Cases.get th)),
            Rule_Cases.get_constraints th)) elims)
         (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
   in

--- a/src/Pure/Isar/proof.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/Pure/Isar/proof.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -391,7 +391,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
 fun apply_method current_context meth state =
   let

--- a/src/Pure/Isar/rule_cases.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/Pure/Isar/rule_cases.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -24,9 +24,12 @@
     assumes: (string * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
+  val case_hypsN: string
   val strip_params: term -> (string * typ) list
-  val make_common: theory * term -> (string * string list) list -> cases
-  val make_nested: term -> theory * term -> (string * string list) list -> cases
+  val make_common: theory * term ->
+    ((string * string list) * string list) list -> cases
+  val make_nested: term -> theory * term ->
+    ((string * string list) * string list) list -> cases
   val apply: term list -> T -> T
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
@@ -38,11 +41,12 @@
   val constraints: int -> attribute
   val name: string list -> thm -> thm
   val case_names: string list -> attribute
+  val cases_hyp_names: string list list -> attribute
   val case_conclusion: string * string list -> attribute
   val is_inner_rule: thm -> bool
   val inner_rule: attribute
   val save: thm -> thm -> thm
-  val get: thm -> (string * string list) list * int
+  val get: thm -> ((string * string list) * string list) list * int
   val rename_params: string list list -> thm -> thm
   val params: string list list -> attribute
   val internalize_params: thm -> thm
@@ -87,15 +91,21 @@
   | extract_fixes (SOME outline) prop =
       chop (length (Logic.strip_params outline)) (strip_params prop);
 
-fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
-  | extract_assumes qual (SOME outline) prop =
-      let val (hyps, prems) =
-        chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
-      in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
+fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
+  | extract_assumes qual hnames (SOME outline) prop =
+      let
+        val (hyps, prems) =
+          chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
+        fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
+        val (hyps1,hyps2) = chop (length hnames) hyps;
+        val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1;
+        val pairs = pairs1 @ (map (pair case_hypsN) hyps2);
+        val named_hyps = map extract (partition_eq (eq_fst op =) pairs)
+      in (named_hyps, [(qual case_premsN, prems)]) end;
 
 fun bindings args = map (apfst Binding.name) args;
 
-fun extract_case thy (case_outline, raw_prop) name concls =
+fun extract_case thy (case_outline, raw_prop) name hnames concls =
   let
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
     val len = length props;
@@ -108,8 +118,7 @@
         fun abs_fixes1 t =
           if not nested then abs_fixes t
           else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
-
-        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
+        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
 
         val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
@@ -142,11 +151,11 @@
   let
     val n = length cases;
     val nprems = Logic.count_prems prop;
-    fun add_case (name, concls) (cs, i) =
+    fun add_case ((name, hnames), concls) (cs, i) =
       ((case try (fn () =>
           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
         NONE => (name, NONE)
-      | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
+      | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
 
 in
@@ -286,6 +295,26 @@
 fun case_names ss = Thm.rule_attribute (K (name ss));
 
 
+(** hyp names **)
+
+val implode_hyps = implode_args o map (suffix "," o space_implode ",");
+val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
+
+val cases_hyp_names_tagN = "cases_hyp_names";
+
+fun add_cases_hyp_names NONE = I
+  | add_cases_hyp_names (SOME namess) =
+      Thm.untag_rule cases_hyp_names_tagN
+      #> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess);
+
+fun lookup_cases_hyp_names th =
+  AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN
+  |> Option.map explode_hyps;
+
+val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
+fun cases_hyp_names ss =
+  Thm.rule_attribute (K (add_cases_hyp_names (SOME ss)));
+
 
 (** case conclusions **)
 
@@ -339,6 +368,7 @@
   save_consumes th #>
   save_constraints th #>
   save_case_names th #>
+  save_cases_hyp_names th #>
   save_case_concls th #>
   save_inner_rule th;
 
@@ -349,7 +379,11 @@
       (case lookup_case_names th of
         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
       | SOME names => map (fn name => (name, get_case_concls th name)) names);
-  in (cases, n) end;
+    val cases_hyps = (case lookup_cases_hyp_names th of
+        NONE => replicate (length cases) []
+      | SOME names => names);
+    fun regroup ((name,concls),hyps) = ((name,hyps),concls)
+  in (map regroup (cases ~~ cases_hyps), n) end;
 
 
 (* params *)

--- a/src/Tools/case_product.ML	Sun Jul 31 11:13:38 2011 -0700
+++ b/src/Tools/case_product.ML	Mon Aug 01 12:08:53 2011 +0200
@@ -90,9 +90,9 @@
 
 fun annotation thm1 thm2 =
   let
-    val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
-    val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
-    val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
+    val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
+    val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
+    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
   in
     Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
   end