# HG changeset patch
# User wenzelm
# Date 1434030240 -7200
# Node ID 64f48e7f921f0bf47bee00e1d81f1c3cf2ada94a
# Parent  1338e6b4395214f09b62c6c47836d41d1c4eb98d
support to parse obtain clause without type-checking yet;
tuned signature;

diff -r 1338e6b43952 -r 64f48e7f921f src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Jun 11 11:09:05 2015 +0200
+++ b/src/Pure/Isar/element.ML	Thu Jun 11 15:44:00 2015 +0200
@@ -31,6 +31,8 @@
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_ctxt_no_attribs: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
+  val close_form: Proof.context -> (string -> string option) -> (string -> typ option) ->
+    term -> term
   type witness
   val prove_witness: Proof.context -> term -> tactic -> witness
   val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
@@ -243,6 +245,26 @@
 end;
 
 
+(** abstract syntax operations: before type-inference **)
+
+fun close_form ctxt default_name default_type A =
+  let
+    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
+      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
+      | abs_body lev y (t as Free (x, T)) =
+          if x = y then
+            Type.constraint (the_default dummyT (default_type x))
+              (Type.constraint T (Bound lev))
+          else t
+      | abs_body _ _ a = a;
+    fun close y B =
+      let
+        val y' = perhaps default_name y;
+        val B' = abs_body 0 y (Term.incr_boundvars 1 B);
+      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y', dummyT, B') else B end;
+  in fold close (Variable.add_free_names ctxt A []) A end;
+
+
 
 (** logical operations **)
 
diff -r 1338e6b43952 -r 64f48e7f921f src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Jun 11 11:09:05 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jun 11 15:44:00 2015 +0200
@@ -39,6 +39,8 @@
 signature OBTAIN =
 sig
   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 thatN: string
   val obtain: string -> (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
@@ -103,15 +105,30 @@
   in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end;
 
 
+fun declare_thesis ctxt =
+  let
+    val ([x], ctxt') =
+      Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt;
+    val t = Object_Logic.fixed_judgment ctxt x;
+    val v = dest_Free (Object_Logic.drop_judgment ctxt t);
+  in ((v, t), ctxt') end;
+
+fun parse_clause ctxt thesis vars raw_props =
+  let
+    val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
+    val xs = map (Variable.check_name o #1) vars;
+
+    val default_name = AList.lookup (op =) (xs' ~~ xs);
+    val default_type = Variable.default_type ctxt';
+  in
+    Logic.list_implies (map (Syntax.parse_prop ctxt') raw_props, thesis)
+    |> Element.close_form ctxt default_name default_type
+  end;
+
+
 
 (** obtain **)
 
-fun bind_judgment ctxt name =
-  let
-    val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
-    val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
-  in ((v, t), ctxt') end;
-
 val thatN = "that";
 
 local
@@ -123,13 +140,14 @@
     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
-    (*obtain vars*)
-    val ((xs', vars), fix_ctxt) = ctxt
+    (*vars*)
+    val ((thesis_var, thesis), thesis_ctxt) = declare_thesis ctxt;
+    val ((xs', vars), fix_ctxt) = thesis_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;
 
-    (*obtain asms*)
+    (*asms*)
     val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
     val props = flat propss;
     val declare_asms =
@@ -139,7 +157,7 @@
       map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
       map (map (rpair [])) propss;
 
-    (*obtain params*)
+    (*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;
@@ -147,10 +165,7 @@
 
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
-    (*obtain statements*)
-    val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
-    val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
-
+    (*statements*)
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Logic.list_rename_params xs
@@ -171,7 +186,7 @@
     |> 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)]
+    |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.assume
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
@@ -202,7 +217,7 @@
 
 fun result tac facts ctxt =
   let
-    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
+    val ((thesis_var, thesis), thesis_ctxt) = declare_thesis ctxt;
     val st = Goal.init (Thm.cterm_of ctxt thesis);
     val rule =
       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
@@ -285,7 +300,7 @@
     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
-    val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
+    val (thesis_var, thesis) = #1 (declare_thesis ctxt);
     val vars = ctxt
       |> fold_map prep_var raw_vars |-> fold_map inferred_type
       |> fst |> polymorphic ctxt;
diff -r 1338e6b43952 -r 64f48e7f921f src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Jun 11 11:09:05 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Jun 11 15:44:00 2015 +0200
@@ -108,19 +108,8 @@
     val frees = rev (fold (Variable.add_free_names ctxt) As []);
     val types =
       map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
-    val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
-
-    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
-      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
-      | abs_body lev y (t as Free (x, T)) =
-          if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
-          else t
-      | abs_body _ _ a = a;
-    fun close y B =
-      let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
-      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, dummyT, B') else B end;
-    fun close_form A = fold close (Variable.add_free_names ctxt A []) A;
-  in map close_form As end;
+    val uniform_typing = AList.lookup (op =) (frees ~~ types);
+  in map (Element.close_form ctxt (K NONE) uniform_typing) As end;
 
 fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let