# HG changeset patch
# User wenzelm
# Date 1434316951 -7200
# Node ID d1a9d098f870a61eb097852457cafb590ec06b3b
# Parent  f690cb540385cd1304335867809166a613cd7e6b# Parent  051b200f7578b576b61307c1960f0ff693ae2ab8
merged

diff -r f690cb540385 -r d1a9d098f870 NEWS
--- a/NEWS	Sun Jun 14 18:51:34 2015 +0100
+++ b/NEWS	Sun Jun 14 23:22:31 2015 +0200
@@ -12,6 +12,9 @@
 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
 proof body as well, abstracted over relevant parameters.
 
+* Improved type-inference for theorem statement 'obtains': separate
+parameter scope for of each clause.
+
 * Term abbreviations via 'is' patterns also work for schematic
 statements: result is abstracted over unknowns.
 
diff -r f690cb540385 -r d1a9d098f870 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Jun 14 23:22:31 2015 +0200
@@ -13,10 +13,10 @@
   type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
 
   (* Processing of context statements *)
-  val cert_statement: Element.context_i list -> (term * term list) list list ->
-    Proof.context -> (term * term list) list list * Proof.context
-  val read_statement: Element.context list -> (string * string list) list list ->
-    Proof.context -> (term * term list) list list * Proof.context
+  val cert_statement: Element.context_i list -> Element.statement_i ->
+    Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
+  val read_statement: Element.context list -> Element.statement ->
+    Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
 
   (* Declaring locales *)
   val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
@@ -217,13 +217,20 @@
     fact = I,
     attrib = I};
 
-fun parse_concl prep_term ctxt concl =
-  (map o map) (fn (t, ps) =>
-    (prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
-      map (prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) concl;
+fun prepare_stmt prep_prop prep_obtains ctxt stmt =
+  (case stmt of
+    Element.Shows raw_shows =>
+      raw_shows |> (map o apsnd o map) (fn (t, ps) =>
+        (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
+          map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps))
+  | Element.Obtains raw_obtains =>
+      let
+        val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt;
+        val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
+      in map (fn (b, t) => ((b, []), [(t, [])])) obtains end);
 
 
-(** Simultaneous type inference: instantiations + elements + conclusion **)
+(** Simultaneous type inference: instantiations + elements + statement **)
 
 local
 
@@ -275,15 +282,15 @@
   let
     val inst_cs = map extract_inst insts;
     val elem_css = map extract_elem elems;
-    val concl_cs = (map o map) mk_propp concl;
+    val concl_cs = (map o map) mk_propp (map snd concl);
     (* Type inference *)
     val (inst_cs' :: css', ctxt') =
       (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
     val (elem_css', [concl_cs']) = chop (length elem_css) css';
   in
-    (map restore_inst (insts ~~ inst_cs'),
+    ((map restore_inst (insts ~~ inst_cs'),
       map restore_elem (elems ~~ elem_css'),
-      concl_cs', ctxt')
+      map fst concl ~~ concl_cs'), ctxt')
   end;
 
 end;
@@ -351,15 +358,15 @@
 end;
 
 
-(** Process full context statement: instantiations + elements + conclusion **)
+(** Process full context statement: instantiations + elements + statement **)
 
 (* Interleave incremental parsing and type inference over entire parsed stretch. *)
 
 local
 
 fun prep_full_context_statement
-    parse_typ parse_prop prep_var_elem prep_inst prep_var_inst prep_expr
-    {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
+    parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_var_inst prep_expr
+    {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
 
@@ -374,7 +381,7 @@
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
-        val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
+        val ((insts'', _, _), _) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
         val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
@@ -389,15 +396,13 @@
         val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
       in (elems', ctxt') end;
 
-    fun prep_concl raw_concl (insts, elems, ctxt) =
-      let
-        val concl = parse_concl parse_prop ctxt raw_concl;
-      in check_autofix insts elems concl ctxt end;
-
     val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
 
+    fun prep_stmt elems ctxt =
+      check_autofix insts' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
+
     val _ =
       if fixed_frees then ()
       else
@@ -406,50 +411,51 @@
         | frees => error ("Illegal free variables in expression: " ^
             commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
 
-    val ctxt4 = init_body ctxt3;
-    val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
-    val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
+    val ((insts, elems', concl), ctxt4) = ctxt3
+      |> init_body
+      |> fold_map prep_elem raw_elems
+      |-> prep_stmt;
 
 
     (* parameters from expression and elements *)
 
     val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
       (Fixes fors :: elems');
-    val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
+    val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4;
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
-    val deps = map (finish_inst ctxt6) insts;
-    val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
+    val deps = map (finish_inst ctxt5) insts;
+    val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
 
-  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end;
+  in ((fixed, deps, elems'', concl), (parms, ctxt5)) end;
 
 in
 
 fun cert_full_context_statement x =
-  prep_full_context_statement (K I) (K I) Proof_Context.cert_var
-  make_inst Proof_Context.cert_var (K I) x;
+  prep_full_context_statement (K I) (K I) Obtain.cert_obtains
+    Proof_Context.cert_var make_inst Proof_Context.cert_var (K I) x;
 
 fun cert_read_full_context_statement x =
-  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
-  make_inst Proof_Context.cert_var (K I) x;
+  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
+    Proof_Context.read_var make_inst Proof_Context.cert_var (K I) x;
 
 fun read_full_context_statement x =
-  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
-  parse_inst Proof_Context.read_var check_expr x;
+  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
+    Proof_Context.read_var parse_inst Proof_Context.read_var check_expr x;
 
 end;
 
 
-(* Context statement: elements + conclusion *)
+(* Context statement: elements + statement *)
 
 local
 
-fun prep_statement prep activate raw_elems raw_concl context =
+fun prep_statement prep activate raw_elems raw_stmt context =
   let
     val ((_, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
-        ([], []) I raw_elems raw_concl context;
+        ([], []) I raw_elems raw_stmt context;
     val (_, context') = context
       |> Proof_Context.set_stmt true
       |> fold_map activate elems;
@@ -474,7 +480,7 @@
   let
     val ((fixed, deps, elems, _), (parms, ctxt')) =
       prep {strict = false, do_close = true, fixed_frees = false}
-        raw_import init_body raw_elems [] context;
+        raw_import init_body raw_elems (Element.Shows []) context;
     (* Declare parameters and imported facts *)
     val context' = context |>
       fix_params fixed |>
@@ -510,7 +516,8 @@
     val thy = Proof_Context.theory_of context;
 
     val ((fixed, deps, _, _), _) =
-      prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
+      prep {strict = true, do_close = true, fixed_frees = true} expression I []
+        (Element.Shows []) context;
     (* proof obligations *)
     val propss = map (props_of thy) deps;
 
diff -r f690cb540385 -r d1a9d098f870 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 14 23:22:31 2015 +0200
@@ -6,11 +6,11 @@
 
 signature OBTAIN =
 sig
+  val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context
   val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
-  val parse_clause: Proof.context -> term ->
-    (binding * typ option * mixfix) list -> string list -> term
   val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
   val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
+  val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
   val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
   val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
   val obtain: binding -> (binding * typ option * mixfix) list ->
@@ -92,38 +92,38 @@
 
 local
 
-fun prepare_clause parse_prop ctxt thesis vars raw_props =
+val mk_all_external = Logic.all_constraint o Variable.default_type;
+fun mk_all_internal _ (y, z) t =
+  let val T = the (AList.lookup (op =) (Term.add_frees t []) z);
+  in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
+
+fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props =
   let
-    val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
+    val ((xs', vars), ctxt') = ctxt
+      |> fold_map prep_var raw_vars
+      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
     val xs = map (Variable.check_name o #1) vars;
   in
     Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
-    |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
+    |> fold_rev (mk_all ctxt') (xs ~~ xs')
   end;
 
-fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
+fun prepare_obtains prep_clause check_terms
+    ctxt thesis (raw_obtains: ('typ, 'term) Element.obtain list) =
   let
-    val all_types =
-      fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains)
-        (ctxt |> Context_Position.set_visible false)
-      |> #1 |> map_filter (fn (_, opt_T, _) => opt_T);
-    val types_ctxt = fold Variable.declare_typ all_types ctxt;
+    val clauses = raw_obtains
+      |> map (fn (_, (raw_vars, raw_props)) => prep_clause ctxt thesis raw_vars raw_props)
+      |> check_terms ctxt;
+  in map fst raw_obtains ~~ clauses end;
 
-    val clauses =
-      raw_obtains |> map (fn (_, (raw_vars, raw_props)) =>
-        let
-          val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt;
-          val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props;
-        in clause end)
-      |> Syntax.check_terms ctxt;
-  in map fst raw_obtains ~~ clauses end;
+val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external;
+val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal;
 
 in
 
-val parse_clause = prepare_clause Syntax.parse_prop;
-
-val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop;
-val cert_obtains = prepare_obtains Proof_Context.cert_var (K I);
+val read_obtains = prepare_obtains parse_clause Syntax.check_terms;
+val cert_obtains = prepare_obtains cert_clause (K I);
+val parse_obtains = prepare_obtains parse_clause (K I);
 
 end;
 
@@ -132,11 +132,11 @@
 (** consider: generalized elimination and cases rule **)
 
 (*
-  consider x where (a) "A x" | y (b) where "B x" | ... ==
+  consider (a) x where "A x" | (b) y where "B y" | ... ==
 
   have thesis
     if a [intro?]: "!!x. A x ==> thesis"
-    and b [intro?]: "!!x. B x ==> thesis"
+    and b [intro?]: "!!y. B y ==> thesis"
     and ...
     for thesis
     apply (insert that)
@@ -287,9 +287,9 @@
   {
     fix thesis
     <chain_facts> have "PROP ?guess"
-      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
+      apply magic      -- {* turn goal into "thesis ==> #thesis" *}
       <proof body>
-      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
+      apply_end magic  -- {* turn final "(!!x. P x ==> thesis) ==> #thesis" into
         "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
       <proof end>
   }
diff -r f690cb540385 -r d1a9d098f870 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Jun 14 23:22:31 2015 +0200
@@ -318,56 +318,30 @@
 
 local
 
-fun prep_statement prep_att prep_stmt elems concl ctxt =
-  (case concl of
-    Element.Shows shows =>
-      let
-        val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
-        val prems = Assumption.local_prems_of elems_ctxt ctxt;
-        val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
-        val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
-      in (([], prems, stmt, NONE), goal_ctxt) end
-  | Element.Obtains obtains =>
-      let
-        val constraints = obtains |> map (fn (_, (vars, _)) =>
-          Element.Constrains
-            (vars |> map_filter (fn (x, SOME T, _) => SOME (Variable.check_name x, T) | _ => NONE)));
-
-        val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
-        val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
-
-        val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
+fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
+  let
+    val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
+    val prems = Assumption.local_prems_of elems_ctxt ctxt;
+    val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd) stmt elems_ctxt;
+  in
+    (case raw_stmt of
+      Element.Shows _ =>
+        let val stmt' = Attrib.map_specs (map prep_att) stmt
+        in (([], prems, stmt', NONE), stmt_ctxt) end
+    | Element.Obtains raw_obtains =>
+        let
+          val asms_ctxt = stmt_ctxt
+            |> fold (fn ((name, _), asm) =>
+                snd o Proof_Context.add_assms Assumption.assume_export
+                  [((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
+          val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
+          val ([(_, that')], that_ctxt) = asms_ctxt
+            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])];
 
-        fun assume_case ((name, (vars, _)), asms) ctxt' =
-          let
-            val bs = map (fn (b, _, _) => b) vars;
-            val xs = map Variable.check_name bs;
-            val props = map fst asms;
-            val (params, _) = ctxt'
-              |> fold Variable.declare_term props
-              |> fold_map Proof_Context.inferred_param xs
-              |>> map Free;
-            val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
-            val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
-          in
-            ctxt'
-            |> Variable.auto_fixes asm
-            |> Proof_Context.add_assms Assumption.assume_export
-              [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
-            |>> (fn [(_, [th])] => th)
-          end;
-
-        val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes obtains);
-        val prems = Assumption.local_prems_of elems_ctxt ctxt;
-        val stmt = [((Binding.empty, []), [(thesis, [])])];
-
-        val (facts, goal_ctxt) = elems_ctxt
-          |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
-          |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths =>
-            Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(ths, [])])] #>
-            #2 #> pair ths);
-      in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
+          val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes raw_obtains);
+          val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
+        in ((more_atts, prems, stmt', SOME that'), that_ctxt) end)
+  end;
 
 fun gen_theorem schematic bundle_includes prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =