# HG changeset patch
# User wenzelm
# Date 1461692267 -7200
# Node ID 50802acac277a3bf16dc82a87c263d0f19aca053
# Parent  9b95ae9ec6719d98b9cf7c36e843b362ebc56ee3
more uniform operations for structured statements;

diff -r 9b95ae9ec671 -r 50802acac277 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Apr 26 16:20:28 2016 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 19:37:47 2016 +0200
@@ -193,13 +193,13 @@
 
 local
 
-fun gen_obtain prep_statement prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_stmt prep_att that_binding raw_vars raw_asms int state =
   let
     val _ = Proof.assert_forward_or_chain state;
 
     val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
     val ((vars, propss, binds, binds'), params_ctxt) =
-      prep_statement raw_vars (map #2 raw_asms) thesis_ctxt;
+      prep_stmt raw_vars (map #2 raw_asms) thesis_ctxt;
     val params = map #2 vars;
     val that_prop =
       Logic.list_rename_params (map #1 params)
@@ -229,8 +229,8 @@
 
 in
 
-val obtain = gen_obtain Proof_Context.cert_statement (K I);
-val obtain_cmd = gen_obtain Proof_Context.read_statement Attrib.attribute_cmd;
+val obtain = gen_obtain Proof_Context.cert_stmt (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd;
 
 end;
 
diff -r 9b95ae9ec671 -r 50802acac277 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 26 16:20:28 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 26 19:37:47 2016 +0200
@@ -641,61 +641,17 @@
 end;
 
 
-(* structured clause *)
-
-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;
-
-fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
-  let
-    (*fixed variables*)
-    val ((xs', vars), fix_ctxt) = ctxt
-      |> fold_map prep_var raw_fixes
-      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
-
-    (*propositions with term bindings*)
-    val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows);
-    val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss;
-
-    (*params*)
-    val (ps, params_ctxt) = fix_ctxt
-      |> (fold o fold) Variable.declare_term all_propss
-      |> 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 _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-
-    (*result term bindings*)
-    val shows_props = flat shows_propss;
-    val binds' =
-      (case try List.last shows_props of
-        NONE => []
-      | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
-    val result_binds =
-      (Auto_Bind.facts params_ctxt shows_props @ binds')
-      |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
-      |> export_binds params_ctxt ctxt;
-  in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end;
-
-
 (* assume *)
 
 local
 
-fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state =
+fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
   let
     val ctxt = context_of state;
 
     val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
     val ((params, prems_propss, concl_propss, result_binds), _) =
-      prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt;
+      prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
     val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
   in
     state
@@ -712,8 +668,8 @@
 
 in
 
-val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I);
-val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd;
+val assm = gen_assume Proof_Context.cert_statement (K I);
+val assm_cmd = gen_assume Proof_Context.read_statement Attrib.attribute_cmd;
 
 val assume = assm Assumption.assume_export;
 val assume_cmd = assm_cmd Assumption.assume_export;
@@ -889,14 +845,14 @@
 
 local
 
-fun gen_define prep_statement prep_att raw_decls raw_fixes raw_defs state =
+fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
   let
     val _ = assert_forward state;
     val ctxt = context_of state;
 
     (*vars*)
     val ((vars, propss, _, binds'), vars_ctxt) =
-      prep_statement (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
+      prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
     val (decls, fixes) = chop (length raw_decls) vars;
     val show_term = Syntax.string_of_term vars_ctxt;
 
@@ -935,8 +891,8 @@
 
 in
 
-val define = gen_define Proof_Context.cert_statement (K I);
-val define_cmd = gen_define Proof_Context.read_statement Attrib.attribute_cmd;
+val define = gen_define Proof_Context.cert_stmt (K I);
+val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd;
 
 end;
 
@@ -1116,7 +1072,7 @@
 
 (* local goals *)
 
-fun local_goal print_results prep_att prep_propp prep_var strict_asm
+fun local_goal print_results prep_statement prep_att strict_asm
     kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
     val ctxt = context_of state;
@@ -1127,7 +1083,7 @@
 
     (*params*)
     val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
-      |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
+      |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
 
     (*prems*)
     val (assumes_bindings, shows_bindings) =
@@ -1242,18 +1198,16 @@
 (* 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_goal print_results
+    (fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I);
 
 local
 
-fun gen_have prep_att prep_propp prep_var
-    strict_asm before_qed after_qed fixes assumes shows int =
+fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
+    prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
 
-fun gen_show prep_att prep_propp prep_var
-    strict_asm before_qed after_qed fixes assumes shows int state =
+fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1284,7 +1238,7 @@
       |> after_qed (result_ctxt, results);
   in
     state
-    |> local_goal print_results prep_att prep_propp prep_var strict_asm
+    |> local_goal print_results prep_statement prep_att strict_asm
       "show" before_qed after_qed' fixes assumes shows
     ||> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
@@ -1294,10 +1248,10 @@
 
 in
 
-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;
+val have = gen_have Proof_Context.cert_statement (K I);
+val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd;
+val show = gen_show Proof_Context.cert_statement (K I);
+val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd;
 
 end;
 
diff -r 9b95ae9ec671 -r 50802acac277 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 26 16:20:28 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 26 19:37:47 2016 +0200
@@ -166,14 +166,22 @@
   val generic_add_abbrev: string -> binding * term -> Context.generic ->
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
-  val cert_statement:
+  val cert_stmt:
     (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
     (((binding * typ option * mixfix) * (string * term)) list * term list list *
       (indexname * term) list * (indexname * term) list) * Proof.context
-  val read_statement:
+  val read_stmt:
     (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
     (((binding * typ option * mixfix) * (string * term)) list * term list list *
       (indexname * term) list * (indexname * term) list) * Proof.context
+  val cert_statement: (binding * typ option * mixfix) list ->
+    (term * term list) list list -> (term * term list) list list -> Proof.context ->
+    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+      Proof.context
+  val read_statement: (binding * string option * mixfix) list ->
+    (string * string list) list list -> (string * string list) list list -> Proof.context ->
+    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+      Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1328,11 +1336,19 @@
 end;
 
 
-(* structured statement *)
+(* structured statements *)
 
 local
 
-fun prep_statement prep_var prep_propp raw_vars raw_propps ctxt =
+fun export_binds ctxt' ctxt params binds =
+  let
+    val rhss =
+      map (the_list o Option.map (Logic.close_term params) o snd) binds
+      |> burrow (Variable.export_terms ctxt' ctxt)
+      |> map (try the_single);
+  in map fst binds ~~ rhss end;
+
+fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
   let
     val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
     val xs = map (Variable.check_name o #1) vars;
@@ -1345,13 +1361,33 @@
     val params = xs ~~ map Free ps;
 
     val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
-    val binds' = (map o apsnd) (Logic.close_term params) binds;
+    val binds' = binds
+      |> map (apsnd SOME)
+      |> export_binds params_ctxt ctxt params
+      |> map (apsnd the);
 
     val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
   in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
 
+fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
+  let
+    val ((fixes, (assumes, shows), binds), ctxt') = ctxt
+      |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
+      |-> (fn (vars, propss, binds, _) =>
+        fold Variable.bind_term binds #>
+        pair (map #2 vars, chop (length raw_assumes) propss, binds));
+    val binds' =
+      (Auto_Bind.facts ctxt' (flat shows) @
+        (case try List.last (flat shows) of
+          NONE => []
+        | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
+      |> export_binds ctxt' ctxt fixes;
+  in ((fixes, assumes, shows, binds'), ctxt') end;
+
 in
 
+val cert_stmt = prep_stmt cert_var cert_propp;
+val read_stmt = prep_stmt read_var read_propp;
 val cert_statement = prep_statement cert_var cert_propp;
 val read_statement = prep_statement read_var read_propp;