# HG changeset patch
# User wenzelm
# Date 1162924792 -3600
# Node ID abfdce60b371addd75e9ba499cac52f09987afba
# Parent  9c96c1ec235f56a1dd0d01199201d19f32f81b85
theorem statements: incorporate Obtain.statement, tuned;

diff -r 9c96c1ec235f -r abfdce60b371 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Nov 07 19:39:50 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Nov 07 19:39:52 2006 +0100
@@ -51,6 +51,7 @@
 structure Specification: SPECIFICATION =
 struct
 
+
 (* diagnostics *)
 
 val quiet_mode = ref false;
@@ -172,7 +173,7 @@
 val abbreviation_i = gen_abbrevs cert_specification;
 
 
-(* const syntax *)
+(* notation *)
 
 fun gen_notation prep_const mode args lthy =
   lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
@@ -198,21 +199,53 @@
 val theorems_i = gen_theorems (K I) (K I);
 
 
-(* goal statements *)
+(* complex goal statements *)
 
 local
 
-val global_goal =
-  Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i;
+fun conclusion prep_att (Element.Shows concl) =
+      let
+        fun mk_stmt propp ctxt =
+          ((Attrib.map_specs prep_att (map fst concl ~~ propp), []),
+            fold (fold (Variable.fix_frees o fst)) propp ctxt);
+      in (([], map snd concl), mk_stmt) end
+  | conclusion _ (Element.Obtains cases) =
+      let
+        val names =
+          cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
+        val elems = cases |> map (fn (_, (vars, _)) =>
+          Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
+        val concl = cases |> map (fn (_, (_, props)) => map (rpair []) props);
 
-fun mk_shows prep_att stmt ctxt =
-  ((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt);
+        fun mk_stmt propp ctxt =
+          let
+            val thesis =
+              ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
+            val atts = map Attrib.internal
+              [RuleCases.consumes (~ (length cases)), RuleCases.case_names names];
 
-fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att)
-  | conclusion _ (Element.Obtains cases) =
-      apfst (apfst (map Locale.Elem)) (Obtain.statement cases);
-
-in
+            fun assume_case ((name, (vars, _)), asms) ctxt' =
+              let
+                val xs = map fst vars;
+                val props = map fst asms;
+                val (parms, _) = ctxt'
+                  |> fold Variable.declare_term props
+                  |> fold_map ProofContext.inferred_param xs;
+                val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
+              in
+                ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
+                ctxt' |> Variable.fix_frees asm
+                |> ProofContext.add_assms_i Assumption.assume_export
+                  [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
+                |>> (fn [(_, [th])] => th)
+              end;
+            val (ths, ctxt') = ctxt
+              |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
+              |> fold_map assume_case (cases ~~ propp)
+              |-> (fn ths =>
+                ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+          in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
+      in ((map Locale.Elem elems, concl), mk_stmt) end;
 
 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
@@ -223,8 +256,7 @@
     val (loc, ctxt, lthy) =
       (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
         (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
-          (warning "Re-initializing theory target for locale inclusion";
-            (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0))
+          (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0)
       | _ => (NONE, lthy0, lthy0));
 
     val attrib = prep_att thy;
@@ -234,12 +266,12 @@
     val ((concl_elems, concl), mk_stmt) = conclusion attrib raw_concl;
     val elems = map elem_attrib (raw_elems @ concl_elems);
 
-    val (_, _, elems_ctxt, propp) = prep_stmt loc elems (map snd concl) ctxt;
-    val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt;
+    val (_, _, elems_ctxt, propp) = prep_stmt loc elems concl ctxt;
+    val ((stmt, facts), goal_ctxt) = mk_stmt propp elems_ctxt;
 
     val k = if kind = "" then [] else [Attrib.kind kind];
-    val names = map (fst o fst) concl;
-    val attss = map (fn ((_, atts), _) => map attrib atts @ k) concl;
+    val names = map (fst o fst) stmt;
+    val attss = map (fn ((_, atts), _) => map attrib atts @ k) stmt;
     val atts = map attrib raw_atts @ k;
 
     fun after_qed' results goal_ctxt' =
@@ -254,10 +286,13 @@
       end;
   in
     goal_ctxt
-    |> global_goal kind before_qed after_qed' NONE (name, []) stmt
+    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
+      kind before_qed after_qed' NONE (name, []) stmt
     |> Proof.refine_insert facts
   end;
 
+in
+
 val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
 val theorem_i = gen_theorem (K I) Locale.cert_context_statement;