# HG changeset patch
# User wenzelm
# Date 1447411271 -3600
# Node ID 4a28eec739e9c1d9ee5cbae1c2bf3d72645a2e06
# Parent  71da80a379c65103573e9feef534f5caa68551d4
support for structure statements in 'assume', 'presume';

diff -r 71da80a379c6 -r 4a28eec739e9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 12 11:30:56 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 13 11:41:11 2015 +0100
@@ -488,6 +488,15 @@
 
 (* statements *)
 
+val structured_statement =
+  Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
+    >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
+
+val structured_statement' =
+  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
+    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
+
+
 fun theorem spec schematic descr =
   Outer_Syntax.local_theory_to_proof' spec
     ("state " ^ descr)
@@ -506,10 +515,6 @@
 val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
 
 
-val structured_statement =
-  Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
-    >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
-
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
     (structured_statement >> (fn (a, b, c, d) =>
@@ -572,11 +577,11 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword assume} "assume propositions"
-    (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
+    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
-    (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
+    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
diff -r 71da80a379c6 -r 4a28eec739e9 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Nov 12 11:30:56 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Fri Nov 13 11:41:11 2015 +0100
@@ -229,7 +229,7 @@
         state'
         |> Proof.fix vars
         |> Proof.map_context declare_asms
-        |> Proof.assm (obtain_export params_ctxt rule cparams) asms
+        |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
       end;
   in
     state
@@ -384,7 +384,7 @@
         |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
-            [(Thm.empty_binding, asms)])
+            [] [] [(Thm.empty_binding, asms)])
         |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
       end;
 
diff -r 71da80a379c6 -r 4a28eec739e9 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Thu Nov 12 11:30:56 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Fri Nov 13 11:41:11 2015 +0100
@@ -23,6 +23,8 @@
   val locale_keyword: string parser
   val locale_expression: Expression.expression parser
   val context_element: Element.context parser
+  val statement': (string * string list) list list parser
+  val if_statement': (string * string list) list list parser
   val statement: (Attrib.binding * (string * string list) list) list parser
   val if_statement: (Attrib.binding * (string * string list) list) list parser
   val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
@@ -132,6 +134,9 @@
 
 (* statements *)
 
+val statement' = Parse.and_list1 (Scan.repeat1 Parse.propp);
+val if_statement' = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement') [];
+
 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
 
diff -r 71da80a379c6 -r 4a28eec739e9 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Nov 12 11:30:56 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Nov 13 11:41:11 2015 +0100
@@ -49,14 +49,24 @@
   val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
   val fix: (binding * typ option * mixfix) list -> state -> state
   val fix_cmd: (binding * string option * mixfix) list -> state -> state
-  val assm: Assumption.export ->
-    (Thm.binding * (term * term list) list) list -> state -> state
-  val assm_cmd: Assumption.export ->
-    (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume: (Thm.binding * (term * term list) list) list -> state -> state
-  val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume: (Thm.binding * (term * term list) list) list -> state -> state
-  val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+  val assm: Assumption.export -> (binding * typ option * mixfix) list ->
+    (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
+    state -> state
+  val assm_cmd: Assumption.export -> (binding * string option * mixfix) list ->
+    (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
+    state -> state
+  val assume: (binding * typ option * mixfix) list ->
+    (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
+    state -> state
+  val assume_cmd: (binding * string option * mixfix) list ->
+    (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
+    state -> state
+  val presume: (binding * typ option * mixfix) list ->
+    (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
+    state -> state
+  val presume_cmd: (binding * string option * mixfix) list ->
+    (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
+    state -> state
   val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
@@ -618,22 +628,86 @@
 end;
 
 
-(* assume etc. *)
+(* 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 asm prep_att exp args state =
-  state
-  |> assert_forward
-  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
-  |> these_factss [] |> #2;
+fun gen_assume prep_var prep_propp 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) =
+      #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
+
+    fun close prop =
+      fold_rev Logic.all_name params (Logic.list_implies (flat prems_propss, prop));
+    val propss = (map o map) close concl_propss;
+  in
+    state
+    |> assert_forward
+    |> map_context_result (fn ctxt =>
+      ctxt
+      |> (fold o fold) Variable.declare_term propss
+      |> fold Variable.maybe_bind_term result_binds
+      |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
+      |-> (fn premss =>
+        Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss)))
+    |> these_factss [] |> #2
+  end;
 
 in
 
-val assm = gen_assume Proof_Context.add_assms (K I);
-val assm_cmd = gen_assume Proof_Context.add_assms_cmd Attrib.attribute_cmd;
+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 assume = assm Assumption.assume_export;
 val assume_cmd = assm_cmd Assumption.assume_export;
+
 val presume = assm Assumption.presume_export;
 val presume_cmd = assm_cmd Assumption.presume_export;
 
@@ -788,7 +862,7 @@
       asms |> map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts));
   in
     state'
-    |> assume assumptions
+    |> assume [] [] assumptions
     |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((binding, atts), [(thms, [])])])
   end;
@@ -982,18 +1056,6 @@
 
 (* 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 strict_asm
     kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
@@ -1002,57 +1064,26 @@
     val add_assumes =
       Assumption.add_assms
         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
+
     val (assumes_bindings, shows_bindings) =
       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
-    val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
 
-    val (goal_ctxt, goal_propss, result_binds, that_fact) =
-      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 (assumes_propp @ shows_propp);
-        val (assumes_propss, shows_propss) = chop (length assumes_propp) 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 ((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);
 
-        (*prems*)
-        val (that_fact, goal_ctxt) = params_ctxt
-          |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
-          |> (fn (premss, ctxt') =>
-              let
-                val prems = Assumption.local_prems_of ctxt' ctxt;
-                val ctxt'' =
-                  ctxt'
-                  |> not (null assumes_propss) ?
-                    (snd o Proof_Context.note_thmss ""
-                      [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
-                  |> (snd o Proof_Context.note_thmss ""
-                      (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
-              in (prems, ctxt'') end);
-
-        val _ = Variable.warn_extra_tfrees fix_ctxt goal_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 goal_ctxt shows_props @ binds')
-          |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
-          |> export_binds goal_ctxt ctxt;
-      in (goal_ctxt, shows_propss, result_binds, that_fact) end;
+    val (that_fact, goal_ctxt) = params_ctxt
+      |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
+      |> (fn (premss, ctxt') =>
+          let
+            val prems = Assumption.local_prems_of ctxt' ctxt;
+            val ctxt'' =
+              ctxt'
+              |> not (null assumes_propss) ?
+                (snd o Proof_Context.note_thmss ""
+                  [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
+              |> (snd o Proof_Context.note_thmss ""
+                  (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
+          in (prems, ctxt'') end);
 
     fun after_qed' (result_ctxt, results) state' = state'
       |> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results)
@@ -1060,12 +1091,10 @@
       |> after_qed (result_ctxt, results);
   in
     state
-    |> generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds
+    |> generic_goal kind before_qed (after_qed', K I) goal_ctxt shows_propss result_binds
     |> pair that_fact
   end;
 
-end;
-
 fun local_qeds arg =
   end_proof false arg
   #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
diff -r 71da80a379c6 -r 4a28eec739e9 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Nov 12 11:30:56 2015 +0100
+++ b/src/Pure/logic.ML	Fri Nov 13 11:41:11 2015 +0100
@@ -9,6 +9,7 @@
 sig
   val all_const: typ -> term
   val all: term -> term -> term
+  val all_name: string * term -> term -> term
   val is_all: term -> bool
   val dest_all: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
@@ -98,6 +99,7 @@
 fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
 
 fun all v t = all_const (Term.fastype_of v) $ lambda v t;
+fun all_name (x, v) t = all_const (Term.fastype_of v) $ Term.lambda_name (x, v) t;
 
 fun is_all (Const ("Pure.all", _) $ Abs _) = true
   | is_all _ = false;