# HG changeset patch
# User wenzelm
# Date 1433858831 -7200
# Node ID 12cc54fac9b028382252607e8a0b296f02efd4bc
# Parent  990c9fea67738f8b60337e4baf66aa14b679bb3d
allow for_fixes for 'have', 'show' etc.;
tuned signature;

diff -r 990c9fea6773 -r 12cc54fac9b0 NEWS
--- a/NEWS	Tue Jun 09 15:28:06 2015 +0200
+++ b/NEWS	Tue Jun 09 16:07:11 2015 +0200
@@ -7,14 +7,20 @@
 New in this Isabelle version
 ----------------------------
 
+*** Isar ***
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
+an optional context of local variables ('for' declaration).
+
+* New command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
+
 *** Pure ***
 
-* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over relevant parameters.
-
-* New Isar command 'supply' supports fact definitions during goal
-refinement ('apply' scripts).
-
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
diff -r 990c9fea6773 -r 12cc54fac9b0 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Tue Jun 09 16:07:11 2015 +0200
@@ -432,19 +432,20 @@
   @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
-     @@{command schematic_corollary}) (goal | statement)
+     @@{command schematic_corollary}) (stmt | statement)
     ;
-    (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
+    (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
+      stmt @{syntax for_fixes}
     ;
     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
   
-    goal: (@{syntax props} + @'and')
+    stmt: (@{syntax props} + @'and')
     ;
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
-    conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
+    conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
     ;
     obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
diff -r 990c9fea6773 -r 12cc54fac9b0 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -280,8 +280,8 @@
 
 fun proof_local cmd goal_ctxt int after_qed' propp =
   Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
-    after_qed' (map (pair Thm.empty_binding) propp);
+  Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+    NONE after_qed' [] (map (pair Thm.empty_binding) propp);
 
 in
 
diff -r 990c9fea6773 -r 12cc54fac9b0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -490,22 +490,23 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
+    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes stmt int)));
+
+val _ =
+  Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
+    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes stmt int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (Parse_Spec.statement >> (fn stmt =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
-
-val _ =
-  Outer_Syntax.command @{command_keyword show}
-    "state local goal, solving current obligation"
-    (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
+    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes stmt int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (Parse_Spec.statement >> (fn stmt =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
+    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes stmt int)));
 
 
 (* facts *)
diff -r 990c9fea6773 -r 12cc54fac9b0 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -155,7 +155,7 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.have NONE (K I) [] [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.map_context (fold Variable.bind_term binds')
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
@@ -163,7 +163,7 @@
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [] [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -314,8 +314,8 @@
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.local_goal print_result (K I) (K (rpair []))
-      "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+      (SOME before_qed) after_qed [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
   end;
diff -r 990c9fea6773 -r 12cc54fac9b0 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -89,11 +89,6 @@
   val apply_end: Method.text -> state -> state Seq.seq
   val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
   val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
-  val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
-    (context -> 'a -> attribute) ->
-    (context -> 'b list -> (term list list * (indexname * term) list)) ->
-    string -> Method.text option -> (thm list list -> state -> state) ->
-    ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text_range option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
@@ -110,13 +105,21 @@
   val global_immediate_proof: state -> context
   val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
+  val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
+    Proof_Context.mode -> string -> Method.text option -> (thm list list -> state -> state) ->
+    (binding * typ option * mixfix) list ->
+    (Thm.binding * (term * term list) list) list -> state -> state
   val have: Method.text option -> (thm list list -> state -> state) ->
+    (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val have_cmd: Method.text option -> (thm list list -> state -> state) ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
+    (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
@@ -888,6 +891,10 @@
 
 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);
@@ -907,33 +914,33 @@
 
 in
 
-fun generic_goal kind before_qed after_qed make_propp state =
+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, binds), goal_state) =
+    val ((propss, params, binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context_result make_propp;
+      |> 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;
     val goal_propss = filter_out null propss';
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
-      |> Thm.cterm_of ctxt
+      |> Thm.cterm_of goal_ctxt
       |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
 
-    val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds);
     val after_qed' = after_qed |>> (fn after_local => fn results =>
-      map_context (fold Variable.bind_term binds') #> after_local results);
+      map_context (fold Variable.bind_term result_binds) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
@@ -971,28 +978,35 @@
 
 (* local goals *)
 
-fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
+fun local_goal print_results prep_att prep_propp prep_var
+    kind before_qed after_qed fixes stmt state =
   let
     val ((names, attss), propp) =
       Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
 
-    fun make_propp ctxt' =
+    fun make_statement ctxt =
       let
-        val (propss, binds) = prep_propp ctxt' propp;
-        val ctxt'' = ctxt'
+        val ((xs', vars), fix_ctxt) = ctxt
+          |> fold_map prep_var fixes
+          |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
+
+        val (propss, binds) = prep_propp fix_ctxt propp;
+        val (Ts, params_ctxt) = fix_ctxt
           |> (fold o fold) Variable.declare_term propss
-          |> Proof_Context.bind_terms binds;
-      in ((propss, binds), ctxt'') end;
+          |> Proof_Context.bind_terms binds
+          |> fold_map Proof_Context.inferred_param xs';
+
+        val xs = map (Variable.check_name o #1) vars;
+        val params = xs ~~ map Free (xs' ~~ Ts);
+
+        val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
+      in ((propss, params, binds), params_ctxt) end;
 
     fun after_qed' results =
       local_results ((names ~~ attss) ~~ results)
       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       #> after_qed results;
-  in
-    state
-    |> generic_goal kind before_qed (after_qed', K I) make_propp
-    |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
-  end;
+  in generic_goal kind before_qed (after_qed', K I) make_statement state end;
 
 fun local_qeds arg =
   end_proof false arg
@@ -1007,15 +1021,15 @@
 
 fun global_goal prep_propp before_qed after_qed propp =
   let
-    fun make_propp ctxt' =
+    fun make_statement ctxt =
       let
         val (propss, binds) =
-          prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') propp;
-        val ctxt'' = ctxt'
+          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, binds), ctxt'') end;
-  in init #> generic_goal "" before_qed (K I, after_qed) make_propp end;
+      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;
 val theorem_cmd = global_goal Proof_Context.read_propp;
@@ -1065,13 +1079,19 @@
 
 (* common goal statements *)
 
+fun internal_goal print_results mode =
+  local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
+    Proof_Context.cert_var;
+
 local
 
-fun gen_have prep_att prep_propp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp prep_var
+    before_qed after_qed fixes stmt int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prep_propp "have" before_qed after_qed stmt;
+    prep_att prep_propp prep_var "have" before_qed after_qed fixes stmt;
 
-fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp prep_var
+    before_qed after_qed fixes stmt int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1102,7 +1122,8 @@
       #> after_qed results;
   in
     state
-    |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
+    |> local_goal print_results prep_att prep_propp prep_var
+      "show" before_qed after_qed' fixes stmt
     |> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
         Exn.Res _ => goal_state
@@ -1111,10 +1132,10 @@
 
 in
 
-val have = gen_have (K I) Proof_Context.cert_propp;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp;
-val show = gen_show (K I) Proof_Context.cert_propp;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp;
+val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
 
 end;