# HG changeset patch
# User wenzelm
# Date 1378231080 -7200
# Node ID 08f3491c50bf3b5987d5329a425cc7632098d674
# Parent  74920496ab718ed5c6f144c9306d46427ebc7fc1
cases: formal binding of 'assumes', with position provided via invoke_case;
allow literal equality on type Binding.binding;

diff -r 74920496ab71 -r 08f3491c50bf src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -456,7 +456,7 @@
        provide a hint to the user. *)
     fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
       not (null fixes) andalso
-      exists (String.isSuffix ".hyps" o fst) assumes andalso
+      exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso
       exists (exists (curry (op =) name o shortest_name o fst)
               o datatype_constrs hol_ctxt) deep_dataTs
     val likely_in_struct_induct_step =
diff -r 74920496ab71 -r 08f3491c50bf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -1574,6 +1574,9 @@
   Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
     "adding alternative introduction rules for code generation of inductive predicates"
 
+fun qualified_binding a =
+  Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
 (* FIXME ... this is important to avoid changing the background theory below *)
 fun generic_code_pred prep_const options raw_const lthy =
@@ -1593,9 +1596,12 @@
     val cases_rules = map mk_cases preds
     val cases =
       map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
-        assumes = ("that", tl (Logic.strip_imp_prems case_rule))
-          :: (map_filter (fn (fact_name, fact) => Option.map (rpair [fact]) fact_name)
-            ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
+        assumes =
+          (Binding.name "that", tl (Logic.strip_imp_prems case_rule)) ::
+          map_filter (fn (fact_name, fact) =>
+              Option.map (fn a => (qualified_binding a, [fact])) fact_name)
+            ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~
+              Logic.strip_imp_prems case_rule),
         binds = [], cases = []}) preds cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'
diff -r 74920496ab71 -r 08f3491c50bf src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/Pure/General/binding.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -9,10 +9,11 @@
 
 signature BINDING =
 sig
-  type binding
+  eqtype binding
   val dest: binding -> bool * (string * bool) list * bstring
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
+  val set_pos: Position.T -> binding -> binding
   val name: bstring -> binding
   val name_of: binding -> bstring
   val map_name: (bstring -> bstring) -> binding -> binding
@@ -41,13 +42,12 @@
 
 (* datatype *)
 
-abstype binding = Binding of
+datatype binding = Binding of
  {conceal: bool,                    (*internal -- for foundational purposes only*)
   prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
-  pos: Position.T}                  (*source position*)
-with
+  pos: Position.T};                 (*source position*)
 
 fun make_binding (conceal, prefix, qualifier, name, pos) =
   Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -65,9 +65,12 @@
 (* name and position *)
 
 fun make (name, pos) = make_binding (false, [], [], name, pos);
-fun name name = make (name, Position.none);
 
 fun pos_of (Binding {pos, ...}) = pos;
+fun set_pos pos =
+  map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
+
+fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
 
 fun eq_name (b, b') = name_of b = name_of b';
@@ -140,7 +143,6 @@
   else legacy_feature (bad binding);
 
 end;
-end;
 
 type binding = Binding.binding;
 
diff -r 74920496ab71 -r 08f3491c50bf src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -743,15 +743,13 @@
 
 local
 
-fun qualified_binding a =
-  Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
-
 fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state =
   let
     val atts = map (prep_att (context_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt (name, pos) xs));
-    val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
+    val assumptions =
+      asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
   in
     state'
     |> assume assumptions
diff -r 74920496ab71 -r 08f3491c50bf src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -133,7 +133,7 @@
     Proof.context -> (string * thm list) list * Proof.context
   val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
   val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
-  val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
+  val apply_case: Rule_Cases.T -> Proof.context -> (binding * term list) list * Proof.context
   val check_case: Proof.context -> string * Position.T -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
@@ -1273,8 +1273,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_asm (b, ts) = Pretty.block (Pretty.breaks
+      ((if Binding.is_empty b then []
+        else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
       | prt_sect s sep prt xs =
diff -r 74920496ab71 -r 08f3491c50bf src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Sep 03 18:21:43 2013 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Sep 03 19:58:00 2013 +0200
@@ -21,7 +21,7 @@
   include BASIC_RULE_CASES
   datatype T = Case of
    {fixes: (binding * typ) list,
-    assumes: (string * term list) list,
+    assumes: (binding * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
   val case_hypsN: string
@@ -62,7 +62,7 @@
 
 datatype T = Case of
  {fixes: (binding * typ) list,
-  assumes: (string * term list) list,
+  assumes: (binding * term list) list,
   binds: (indexname * term option) list,
   cases: (string * T) list};
 
@@ -91,21 +91,22 @@
   | 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 hnames (SOME outline) prop =
+fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
+  | extract_assumes qualifier hyp_names (SOME outline) prop =
       let
+        val qual = Binding.qualify true qualifier o Binding.name;
         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)
+        fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
+        val (hyps1, hyps2) = chop (length hyp_names) hyps;
+        val pairs1 = if null hyps1 then [] else hyp_names ~~ 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 hnames concls =
+fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
   let
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
     val len = length props;
@@ -120,7 +121,8 @@
           else
             fold_rev Term.abs fixes1
               (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
-        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
+        val (assumes1, assumes2) =
+          extract_assumes name hyp_names case_outline prop
           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
 
         val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
@@ -153,11 +155,11 @@
   let
     val n = length cases;
     val nprems = Logic.count_prems prop;
-    fun add_case ((name, hnames), concls) (cs, i) =
+    fun add_case ((name, hyp_names), 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 hnames concls)) :: cs, i - 1);
+      | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
 
 in