# HG changeset patch
# User wenzelm
# Date 1433881473 -7200
# Node ID 1fd46ced2fa826f71e629a5ff9cd1e590b30730e
# Parent  53ef7b78e78a16b9407d65b12751fce8749fa8a4
more uniform treatment of auto bindings vs. explicit user bindings;
misc tuning;

diff -r 53ef7b78e78a -r 1fd46ced2fa8 NEWS
--- a/NEWS	Tue Jun 09 16:42:17 2015 +0200
+++ b/NEWS	Tue Jun 09 22:24:33 2015 +0200
@@ -12,6 +12,9 @@
 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
 proof body as well, abstracted over relevant parameters.
 
+* Term abbreviations via 'is' patterns also work for schematic
+statements: result is abstracted over unknowns.
+
 * Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
 an optional context of local variables ('for' declaration).
 
diff -r 53ef7b78e78a -r 1fd46ced2fa8 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Tue Jun 09 16:42:17 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Tue Jun 09 22:24:33 2015 +0200
@@ -9,6 +9,7 @@
   val thesisN: string
   val thisN: string
   val assmsN: string
+  val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
   val facts: Proof.context -> term list -> (indexname * term option) list
   val no_facts: indexname list
@@ -25,8 +26,10 @@
 
 fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
 
+fun abs_params prop = fold_rev Term.abs (Logic.strip_params prop);
+
 fun statement_binds ctxt name prop =
-  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
+  [((name, 0), SOME (abs_params prop (strip_judgment ctxt prop)))];
 
 
 (* goal *)
@@ -39,13 +42,14 @@
 
 fun get_arg ctxt prop =
   (case strip_judgment ctxt prop of
-    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
+    _ $ t => SOME (abs_params prop t)
   | _ => NONE);
 
-fun facts _ [] = []
-  | facts ctxt props =
-      let val prop = List.last props
-      in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
+fun facts ctxt props =
+  (case try List.last props of
+    NONE => []
+  | SOME prop =>
+      [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
 
 val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
 
diff -r 53ef7b78e78a -r 1fd46ced2fa8 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 16:42:17 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 22:24:33 2015 +0200
@@ -119,18 +119,20 @@
     val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
-    val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
-    val asm_props = flat asm_propss;
-    val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
+    val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
+    val props = flat propss;
+    val declare_asms =
+      fold Variable.declare_term props #>
+      fold Variable.bind_term binds;
     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
-      map (map (rpair [])) asm_propss;
+      map (map (rpair [])) propss;
 
     (*obtain params*)
     val (params, params_ctxt) =
       declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
     val cparams = map (Thm.cterm_of params_ctxt) params;
-    val binds' = map (apsnd (fold_rev Term.dependent_lambda_name (xs ~~ params))) binds;
+    val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
 
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
@@ -141,7 +143,7 @@
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
+        (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
     val obtain_prop =
       Logic.list_rename_params [Auto_Bind.thesisN]
         (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
diff -r 53ef7b78e78a -r 1fd46ced2fa8 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jun 09 16:42:17 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 22:24:33 2015 +0200
@@ -891,10 +891,6 @@
 
 local
 
-fun export_binds ctxt' ctxt params binds =
-  let val ts = map (fold_rev Term.dependent_lambda_name params o snd) binds;
-  in map fst binds ~~ Variable.export_terms ctxt' ctxt ts end;
-
 val is_var =
   can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
   can (dest_Var o Logic.dest_term);
@@ -916,11 +912,10 @@
 
 fun generic_goal kind before_qed after_qed make_statement state =
   let
-    val ctxt = context_of state;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val ((propss, params, binds), goal_state) =
+    val ((propss, result_binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
@@ -928,7 +923,6 @@
       |> map_context_result make_statement;
     val props = flat propss;
     val goal_ctxt = context_of goal_state;
-    val result_binds = export_binds goal_ctxt ctxt params binds;
 
     val vars = implicit_vars props;
     val propss' = vars :: propss;
@@ -940,7 +934,7 @@
     val statement = ((kind, pos), propss', Thm.term_of goal);
 
     val after_qed' = after_qed |>> (fn after_local => fn results =>
-      map_context (fold Variable.bind_term result_binds) #> after_local results);
+      map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
@@ -955,22 +949,16 @@
     |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
-fun generic_qed after_ctxt state =
-  let
-    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
-    val outer_state = state |> close_block;
-    val outer_ctxt = context_of outer_state;
-
-    val props =
-      flat (tl stmt)
-      |> Variable.exportT_terms goal_ctxt outer_ctxt;
-    val results =
-      tl (conclude_goal goal_ctxt goal stmt)
-      |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
-  in
-    outer_state
-    |> map_context (after_ctxt props)
-    |> pair (after_qed, results)
+fun generic_qed state =
+  let val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state in
+    state
+    |> close_block
+    |> `(fn outer_state =>
+      let
+        val results =
+          tl (conclude_goal goal_ctxt goal stmt)
+          |> burrow (Proof_Context.export goal_ctxt (context_of outer_state));
+      in (after_qed, results) end)
   end;
 
 end;
@@ -978,6 +966,18 @@
 
 (* local goals *)
 
+local
+
+fun export_binds ctxt' ctxt binds =
+  let
+    val rhss =
+      map (the_list o snd) binds
+      |> burrow (Variable.export_terms ctxt' ctxt)
+      |> map (try the_single);
+  in map fst binds ~~ rhss end;
+
+in
+
 fun local_goal print_results prep_att prep_propp prep_var
     kind before_qed after_qed fixes stmt state =
   let
@@ -991,16 +991,28 @@
           |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
 
         val (propss, binds) = prep_propp fix_ctxt propp;
+        val props = flat propss;
+
         val (ps, params_ctxt) = fix_ctxt
-          |> (fold o fold) Variable.declare_term propss
-          |> Proof_Context.bind_terms binds
+          |> fold Variable.declare_term props
+          |> fold Variable.bind_term binds
           |> fold_map Proof_Context.inferred_param xs';
 
         val xs = map (Variable.check_name o #1) vars;
         val params = xs ~~ map Free ps;
 
+        val binds' =
+          (case try List.last props of
+            NONE => []
+          | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
+        val result_binds =
+          (Auto_Bind.facts params_ctxt props @ binds')
+          |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
+          |> export_binds params_ctxt ctxt;
+
         val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-      in ((propss, params, binds), params_ctxt) end;
+
+      in ((propss, result_binds), params_ctxt) end;
 
     fun after_qed' results =
       local_results ((names ~~ attss) ~~ results)
@@ -1008,10 +1020,11 @@
       #> after_qed results;
   in generic_goal kind before_qed (after_qed', K I) make_statement state end;
 
+end;
+
 fun local_qeds arg =
   end_proof false arg
-  #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results));
+  #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
 
 fun local_qed arg =
   local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
@@ -1027,8 +1040,8 @@
           prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
         val ctxt' = ctxt
           |> (fold o fold) Variable.auto_fixes propss
-          |> Proof_Context.bind_terms binds;
-      in ((propss, [], []), ctxt') end;
+          |> fold Variable.bind_term binds;
+      in ((propss, []), ctxt') end;
   in init #> generic_goal "" before_qed (K I, after_qed) make_statement end;
 
 val theorem = global_goal Proof_Context.cert_propp;
@@ -1036,7 +1049,7 @@
 
 fun global_qeds arg =
   end_proof true arg
-  #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+  #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
     after_qed results (context_of state)));
 
 fun global_qed arg =
diff -r 53ef7b78e78a -r 1fd46ced2fa8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jun 09 16:42:17 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jun 09 22:24:33 2015 +0200
@@ -105,8 +105,6 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
-  val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
-  val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val match_bind: bool -> (term list * term) list -> Proof.context ->
@@ -815,26 +813,23 @@
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 
-(* bind_terms *)
-
-val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
-  ctxt
-  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
-
-val bind_terms = maybe_bind_terms o map (apsnd SOME);
-
-
 (* auto_bind *)
 
-fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
-  | drop_schematic b = b;
-
-fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
 
 
+(* bind terms (non-schematic) *)
+
+fun cert_maybe_bind_term (xi, t) ctxt =
+  ctxt
+  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
+
+val cert_bind_term = cert_maybe_bind_term o apsnd SOME;
+
+
 (* match_bind *)
 
 local
@@ -857,8 +852,10 @@
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
-        else ctxt' |> bind_terms binds');
+          ctxt (*sic!*)
+          |> fold Variable.declare_term (map #2 binds')
+          |> fold cert_bind_term binds'
+        else ctxt' |> fold cert_bind_term binds');
   in (ts, ctxt'') end;
 
 in
@@ -1161,7 +1158,7 @@
     |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
     |-> (fn premss =>
       auto_bind_facts props
-      #> bind_terms binds
+      #> fold Variable.bind_term binds
       #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
@@ -1182,6 +1179,9 @@
 
 local
 
+fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
+  | drop_schematic b = b;
+
 fun update_case _ _ ("", _) res = res
   | update_case _ _ (name, NONE) (cases, index) =
       (Name_Space.del_table name cases, index)
@@ -1213,7 +1213,7 @@
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
-    |> maybe_bind_terms (map drop_schematic binds)
+    |> fold (cert_maybe_bind_term o drop_schematic) binds
     |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;