# HG changeset patch
# User wenzelm
# Date 1434055673 -7200
# Node ID 78f3c67bc35e58347cba73577740fb4193fd3eee
# Parent  fa9bff5cd67969e59d8fec6bf9f35aee524a38b9
support for 'consider' command;
allow full "fixes" for 'obtain' command;
tuned signature;

diff -r fa9bff5cd679 -r 78f3c67bc35e src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Jun 11 22:47:53 2015 +0200
@@ -999,7 +999,7 @@
   occur in the conclusion.
 
   @{rail \<open>
-    @@{command obtain} @{syntax par_name}? (@{syntax vars} + @'and')
+    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
       @'where' (@{syntax props} + @'and')
     ;
     @@{command guess} (@{syntax vars} + @'and')
diff -r fa9bff5cd679 -r 78f3c67bc35e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -222,7 +222,7 @@
 fun is_low_level_class_const s =
   s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
 
-val sep_that = Long_Name.separator ^ Obtain.thatN
+val sep_that = Long_Name.separator ^ Auto_Bind.thatN
 val skolem_thesis = Name.skolem Auto_Bind.thesisN
 
 fun is_that_fact th =
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -8,6 +8,7 @@
 sig
   val thesisN: string
   val thisN: string
+  val thatN: string
   val premsN: string
   val assmsN: string
   val abs_params: term -> term -> term
@@ -23,6 +24,7 @@
 
 val thesisN = "thesis";
 val thisN = "this";
+val thatN = "that";
 val assmsN = "assms";
 val premsN = "prems";
 
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/element.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -7,7 +7,9 @@
 
 signature ELEMENT =
 sig
-  type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list)
+  type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list)
+  type obtains = (string, string) obtain list
+  type obtains_i = (typ, term) obtain list
   datatype ('typ, 'term) stmt =
     Shows of (Attrib.binding * ('term * 'term list) list) list |
     Obtains of ('typ, 'term) obtain list
@@ -64,7 +66,10 @@
 
 (* statement *)
 
-type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list);
+type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list);
+type obtains = (string, string) obtain list;
+type obtains_i = (typ, term) obtain list;
+
 datatype ('typ, 'term) stmt =
   Shows of (Attrib.binding * ('term * 'term list) list) list |
   Obtains of ('typ, 'term) obtain list;
@@ -129,14 +134,14 @@
     fun prt_show (a, ts) =
       Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
 
-    fun prt_var (x, SOME T) = Pretty.block
+    fun prt_var (x, SOME T, _) = Pretty.block
           [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
-      | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
+      | prt_var (x, NONE, _) = Pretty.str (Binding.name_of x);
     val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
 
-    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
-      | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
-          (prt_vars xs @ [Pretty.keyword2 "where"] @ prt_terms ts));
+    fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props))
+      | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks
+          (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props));
   in
     fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
      | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
@@ -213,7 +218,7 @@
 fun obtain prop ctxt =
   let
     val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
-    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
+    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
     val xs = map (fix o #2) ps;
     val As = Logic.strip_imp_prems prop';
   in ((Binding.empty, (xs, As)), ctxt') end;
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -570,6 +570,10 @@
     >> (Toplevel.proof o Proof.def_cmd));
 
 val _ =
+  Outer_Syntax.command @{command_keyword consider} "state cases rule"
+    (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
+
+val _ =
   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
       >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -7,17 +7,23 @@
 similar, but derives these elements from the course of reasoning!
 
   <chain_facts>
-  obtain x where "A x" <proof> ==
+  consider x where "A x" | y where "B x" | ... <proof> ==
 
-  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
+  have "!!thesis. (!!x. A x ==> thesis) ==> (!!x. B x ==> thesis) ==> ... ==> thesis"
   proof succeed
     fix thesis
-    assume that [intro?]: "!!x. A x ==> thesis"
+    assume that [intro?]: "!!x. A x ==> thesis" "!!x. B x ==> thesis" ...
     <chain_facts>
     show thesis
       apply (insert that)
       <proof>
   qed
+
+
+  <chain_facts>
+  obtain x where "A x" <proof> ==
+
+  consider x where "A x" <chain_facts> <proof>
   fix x assm <<obtain_export>> "A x"
 
 
@@ -39,9 +45,12 @@
 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 parse_clause: Proof.context -> term ->
+    (binding * typ option * mixfix) list -> string list -> term
+  val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
+  val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
+  val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
+  val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
   val obtain: string -> (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_cmd: string -> (binding * string option * mixfix) list ->
@@ -98,6 +107,8 @@
 
 (** specification elements **)
 
+(* result declaration *)
+
 fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) =
   let
     val case_names = obtains |> map_index (fn (i, (b, _)) =>
@@ -105,7 +116,9 @@
   in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end;
 
 
-fun declare_thesis ctxt =
+(* obtain thesis *)
+
+fun obtain_thesis ctxt =
   let
     val ([x], ctxt') =
       Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt;
@@ -113,7 +126,12 @@
     val v = dest_Free (Object_Logic.drop_judgment ctxt t);
   in ((v, t), ctxt') end;
 
-fun parse_clause ctxt thesis vars raw_props =
+
+(* obtain clauses *)
+
+local
+
+fun prepare_clause parse_prop ctxt thesis vars raw_props =
   let
     val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
     val xs = map (Variable.check_name o #1) vars;
@@ -121,16 +139,81 @@
     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)
+    Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
     |> Element.close_form ctxt default_name default_type
   end;
 
+fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
+  let
+    val all_types =
+      fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains)
+        (ctxt |> Context_Position.set_visible false)
+      |> #1 |> map_filter (fn (_, opt_T, _) => opt_T);
+    val types_ctxt = fold Variable.declare_typ all_types ctxt;
+
+    val clauses =
+      raw_obtains |> map (fn (_, (raw_vars, raw_props)) =>
+        let
+          val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt;
+          val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props;
+        in clause end)
+      |> Syntax.check_terms ctxt;
+  in map fst raw_obtains ~~ clauses end;
+
+in
+
+val parse_clause = prepare_clause Syntax.parse_prop;
+
+val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop;
+val cert_obtains = prepare_obtains Proof_Context.cert_var (K I);
+
+end;
+
+
+
+(** consider **)
+
+local
+
+fun gen_consider prep_obtains raw_obtains int state =
+  let
+    val _ = Proof.assert_forward_or_chain state;
+    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), thesis_ctxt) = obtain_thesis ctxt;
+    val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
+
+    val obtain_prop =
+      Logic.list_rename_params [Auto_Bind.thesisN]
+        (Logic.all (Free thesis_var)
+          (fold_rev (fn (_, A) => fn B => Logic.mk_implies (A, B)) obtains thesis));
+  in
+    state
+    |> Proof.enter_forward
+    |> Proof.have NONE (K I) [] []
+      [((Binding.empty, obtains_attributes raw_obtains), [(obtain_prop, [])])] int
+    |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
+    |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+    |> Proof.assume (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
+    |> `Proof.the_facts
+    ||> Proof.chain_facts chain_facts
+    ||> Proof.show NONE (K (Proof.local_qed (NONE, false)))
+      [] [] [(Thm.empty_binding, [(thesis, [])])] false
+    |-> Proof.refine_insert
+  end;
+
+in
+
+val consider = gen_consider cert_obtains;
+val consider_cmd = gen_consider read_obtains;
+
+end;
+
 
 
 (** obtain **)
 
-val thatN = "that";
-
 local
 
 fun gen_obtain prep_att prep_var prep_propp
@@ -141,7 +224,7 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*vars*)
-    val ((thesis_var, thesis), thesis_ctxt) = declare_thesis ctxt;
+    val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
     val ((xs', vars), fix_ctxt) = thesis_ctxt
       |> fold_map prep_var raw_vars
       |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
@@ -166,7 +249,7 @@
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
     (*statements*)
-    val that_name = if name = "" then thatN else name;
+    val that_name = if name = "" then Auto_Bind.thatN else name;
     val that_prop =
       Logic.list_rename_params xs
         (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
@@ -217,7 +300,7 @@
 
 fun result tac facts ctxt =
   let
-    val ((thesis_var, thesis), thesis_ctxt) = declare_thesis ctxt;
+    val ((thesis_var, thesis), thesis_ctxt) = obtain_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
@@ -300,7 +383,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 (declare_thesis ctxt);
+    val (thesis_var, thesis) = #1 (obtain_thesis ctxt);
     val vars = ctxt
       |> fold_map prep_var raw_vars |-> fold_map inferred_type
       |> fst |> polymorphic ctxt;
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -90,7 +90,7 @@
   val where_: string parser
   val const_decl: (string * string * mixfix) parser
   val const_binding: (binding * string * mixfix) parser
-  val params: (binding * string option) list parser
+  val params: (binding * string option * mixfix) list parser
   val fixes: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: Input.source parser
@@ -358,13 +358,12 @@
 val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
 val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
 
-val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
-  >> (fn (xs, T) => map (rpair T) xs);
+val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1);
+val params =
+  Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
+    >> (fn (xs, T) => map (fn x => (x, T, NoSyn)) xs);
 
-val fixes =
-  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
-    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
-
+val fixes = and_list1 (param_mixfix || params) >> flat;
 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
 
 
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -25,6 +25,7 @@
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
   val if_prems: (Attrib.binding * (string * string list) list) list parser
+  val obtains: Element.obtains parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
 end;
@@ -72,7 +73,7 @@
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
     >> (single o Parse.triple1) ||
-  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
+  Parse.params) >> flat;
 
 val locale_insts =
   Scan.optional
@@ -136,13 +137,15 @@
 
 val obtain_case =
   Parse.parbinding --
-    (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
+    (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
       (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
 
+val obtains = Parse.enum1 "|" obtain_case;
+
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||
   Scan.repeat context_element --
-   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+   (Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains ||
     Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
 
 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Jun 11 22:47:53 2015 +0200
@@ -330,7 +330,7 @@
       let
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T, _) => SOME (Variable.check_name x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -339,7 +339,7 @@
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
-            val bs = map fst vars;
+            val bs = map (fn (b, _, _) => b) vars;
             val xs = map Variable.check_name bs;
             val props = map fst asms;
             val (params, _) = ctxt'
@@ -364,7 +364,7 @@
           |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths =>
-            Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+            Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(ths, [])])] #>
             #2 #> pair ths);
       in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
 
diff -r fa9bff5cd679 -r 78f3c67bc35e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Jun 11 16:15:27 2015 +0200
+++ b/src/Pure/Pure.thy	Thu Jun 11 22:47:53 2015 +0200
@@ -55,6 +55,7 @@
   and "supply" :: prf_script % "proof"
   and "using" "unfolding" :: prf_decl % "proof"
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
+  and "consider" :: prf_goal % "proof"
   and "obtain" :: prf_asm_goal % "proof"
   and "guess" :: prf_asm_goal_script % "proof"
   and "let" "write" :: prf_decl % "proof"