# HG changeset patch
# User wenzelm
# Date 1434316928 -7200
# Node ID 051b200f7578b576b61307c1960f0ff693ae2ab8
# Parent  05fd100e7971d7a74b7aff3af9b19d6154bbe2b2
improved treatment of Element.Obtains via Expression.prepare_stmt;
discontinued pointless all_types ctxt: prep_var is always sequential;

diff -r 05fd100e7971 -r 051b200f7578 NEWS
--- a/NEWS	Sun Jun 14 20:10:21 2015 +0200
+++ b/NEWS	Sun Jun 14 23:22:08 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 05fd100e7971 -r 051b200f7578 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Jun 14 20:10:21 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Jun 14 23:22:08 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,7 +282,7 @@
   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;
@@ -283,7 +290,7 @@
   in
     ((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;
 
@@ -393,8 +400,8 @@
     val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
 
-    fun prep_concl elems ctxt =
-      check_autofix insts' elems (parse_concl parse_prop ctxt raw_concl) ctxt;
+    fun prep_stmt elems ctxt =
+      check_autofix insts' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
 
     val _ =
       if fixed_frees then ()
@@ -407,7 +414,7 @@
     val ((insts, elems', concl), ctxt4) = ctxt3
       |> init_body
       |> fold_map prep_elem raw_elems
-      |-> prep_concl;
+      |-> prep_stmt;
 
 
     (* parameters from expression and elements *)
@@ -426,29 +433,29 @@
 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;
@@ -473,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 |>
@@ -509,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 05fd100e7971 -r 051b200f7578 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 14 20:10:21 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 14 23:22:08 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;
 
diff -r 05fd100e7971 -r 051b200f7578 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Jun 14 20:10:21 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Jun 14 23:22:08 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 =