multi_theorem: common statement header (covers *all* results);
authorwenzelm
Mon Nov 19 20:47:39 2001 +0100 (2001-11-19 ago)
changeset 12242282a92bc5655
parent 12241 c4a2a0686238
child 12243 a2c0aaf94460
multi_theorem: common statement header (covers *all* results);
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:46:38 2001 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:47:39 2001 +0100
     1.3 @@ -302,20 +302,14 @@
     1.4  
     1.5  val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
     1.6  
     1.7 -val theoremP =
     1.8 -  OuterSyntax.command "theorem" "state theorem" K.thy_goal
     1.9 -    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
    1.10 -      uncurry (IsarThy.multi_theorem Drule.theoremK)));
    1.11 +fun gen_theorem k =
    1.12 +  OuterSyntax.command k ("state " ^ k) K.thy_goal
    1.13 +    (P.opt_thm_name ":" -- in_locale_elems -- statement >> (fn ((x, y), z) =>
    1.14 +      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
    1.15  
    1.16 -val lemmaP =
    1.17 -  OuterSyntax.command "lemma" "state lemma" K.thy_goal
    1.18 -    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
    1.19 -      uncurry (IsarThy.multi_theorem Drule.lemmaK)));
    1.20 -
    1.21 -val corollaryP =
    1.22 -  OuterSyntax.command "corollary" "state corollary" K.thy_goal
    1.23 -    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
    1.24 -      uncurry (IsarThy.multi_theorem Drule.corollaryK)));
    1.25 +val theoremP = gen_theorem Drule.theoremK;
    1.26 +val lemmaP = gen_theorem Drule.lemmaK;
    1.27 +val corollaryP = gen_theorem Drule.corollaryK;
    1.28  
    1.29  val showP =
    1.30    OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:46:38 2001 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:47:39 2001 +0100
     2.3 @@ -99,11 +99,13 @@
     2.4      -> ((bstring * Theory.theory Thm.attribute list) *
     2.5        (Term.term * (Term.term list * Term.term list))) * Comment.text
     2.6      -> bool -> theory -> ProofHistory.T
     2.7 -  val multi_theorem: string -> (xstring * Args.src list) option * Args.src Locale.element list ->
     2.8 -    (((bstring * Args.src list) * (string * (string list * string list)) list)
     2.9 +  val multi_theorem: string -> (bstring * Args.src list)
    2.10 +    -> (xstring * Args.src list) option * Args.src Locale.element list
    2.11 +    -> (((bstring * Args.src list) * (string * (string list * string list)) list)
    2.12      * Comment.text) list -> bool -> theory -> ProofHistory.T
    2.13 -  val multi_theorem_i: string -> (string * Proof.context attribute list) option
    2.14 -    * Proof.context attribute Locale.element_i list ->
    2.15 +  val multi_theorem_i: string -> (bstring * theory attribute list)
    2.16 +    -> (string * Proof.context attribute list) option
    2.17 +      * Proof.context attribute Locale.element_i list ->
    2.18      (((bstring * Theory.theory Thm.attribute list) *
    2.19        (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
    2.20      -> bool -> theory -> ProofHistory.T
    2.21 @@ -445,16 +447,16 @@
    2.22  
    2.23  in
    2.24  
    2.25 -fun multi_theorem k (locale, elems) args int thy =
    2.26 -  global_statement (Proof.multi_theorem k
    2.27 +fun multi_theorem k a (locale, elems) args int thy =
    2.28 +  global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a)
    2.29      (apsome (apsnd (map (Attrib.local_attribute thy))) locale)
    2.30      (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
    2.31  
    2.32 -fun multi_theorem_i k (locale, elems) =
    2.33 -  global_statement_i (Proof.multi_theorem_i k locale elems) o map Comment.ignore;
    2.34 +fun multi_theorem_i k a (locale, elems) =
    2.35 +  global_statement_i (Proof.multi_theorem_i k a locale elems) o map Comment.ignore;
    2.36  
    2.37 -fun theorem k loc ((a, t), cmt) = multi_theorem k loc [((a, [t]), cmt)];
    2.38 -fun theorem_i k loc ((a, t), cmt) = multi_theorem_i k loc [((a, [t]), cmt)];
    2.39 +fun theorem k loc ((a, t), cmt) = multi_theorem k a loc [((("", []), [t]), cmt)];
    2.40 +fun theorem_i k loc ((a, t), cmt) = multi_theorem_i k a loc [((("", []), [t]), cmt)];
    2.41  
    2.42  val assume      = local_statement Proof.assume I o map Comment.ignore;
    2.43  val assume_i    = local_statement_i Proof.assume_i I o map Comment.ignore;
     3.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 19 20:46:38 2001 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 19 20:47:39 2001 +0100
     3.3 @@ -76,11 +76,11 @@
     3.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
     3.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
     3.6    val invoke_case: string * string option list * context attribute list -> state -> state
     3.7 -  val multi_theorem: string
     3.8 +  val multi_theorem: string -> bstring * theory attribute list
     3.9      -> (xstring * context attribute list) option -> context attribute Locale.element list
    3.10      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
    3.11      -> theory -> state
    3.12 -  val multi_theorem_i: string
    3.13 +  val multi_theorem_i: string -> bstring * theory attribute list
    3.14      -> (string * context attribute list) option -> context attribute Locale.element_i list
    3.15      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    3.16      -> theory -> state
    3.17 @@ -133,13 +133,18 @@
    3.18  (* type goal *)
    3.19  
    3.20  datatype kind =
    3.21 -  Theorem of string * (string * context attribute list) option * theory attribute list list |
    3.22 -    (*theorem with kind, locale target, attributes*)
    3.23 -  Show of context attribute list list |  (*intermediate result, solving subgoal*)
    3.24 -  Have of context attribute list list;   (*intermediate result*)
    3.25 +  Theorem of string *                           (*theorem kind*)
    3.26 +    (bstring * theory attribute list) *         (*common result binding*)
    3.27 +    (string * context attribute list) option *  (*target locale*)
    3.28 +    theory attribute list list |                (*attributes of individual result binding*)
    3.29 +  Show of context attribute list list |         (*intermediate result, solving subgoal*)
    3.30 +  Have of context attribute list list;          (*intermediate result*)
    3.31  
    3.32 -fun kind_name _ (Theorem (s, None, _)) = s
    3.33 -  | kind_name sg (Theorem (s, Some (name, _), _)) = s ^ " (in " ^ Locale.cond_extern sg name ^ ")"
    3.34 +fun common_name "" = "" | common_name a = " " ^ a;
    3.35 +
    3.36 +fun kind_name _ (Theorem (s, (a, _), None, _)) = s ^ common_name a
    3.37 +  | kind_name sg (Theorem (s, (a, _), Some (name, _), _)) =
    3.38 +      s ^ common_name a ^ " (in " ^ Locale.cond_extern sg name ^ ")"
    3.39    | kind_name _ (Show _) = "show"
    3.40    | kind_name _ (Have _) = "have";
    3.41  
    3.42 @@ -342,7 +347,8 @@
    3.43        | subgoals n = ", " ^ string_of_int n ^ " subgoals";
    3.44  
    3.45      fun prt_names names =
    3.46 -      (case filter_out (equal "") names of [] => "" | nms => " " ^ space_implode " and " nms);
    3.47 +      (case filter_out (equal "") names of [] => ""
    3.48 +      | nms => " " ^ enclose "(" ")" (space_implode " and " nms));
    3.49  
    3.50      fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
    3.51        pretty_facts "using " ctxt
    3.52 @@ -642,7 +648,7 @@
    3.53    end;
    3.54  
    3.55  (*global goals*)
    3.56 -fun global_goal prepp prep_locale activate kind raw_locale elems args thy =
    3.57 +fun global_goal prepp prep_locale activate kind a raw_locale elems args thy =
    3.58    let val locale = apsome (apfst (prep_locale (Theory.sign_of thy))) raw_locale in
    3.59      thy
    3.60      |> init_state
    3.61 @@ -650,7 +656,7 @@
    3.62      |> (case locale of Some (name, _) => map_context (Locale.activate_locale_i name) | None => I)
    3.63      |> open_block
    3.64      |> map_context (activate elems)
    3.65 -    |> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, locale, map (snd o fst) args))
    3.66 +    |> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, a, locale, map (snd o fst) args))
    3.67        Seq.single (map (fst o fst) args) (map snd args)
    3.68    end;
    3.69  
    3.70 @@ -659,8 +665,10 @@
    3.71  val multi_theorem_i =
    3.72    global_goal ProofContext.bind_propp_schematic_i (K I) Locale.activate_elements_i;
    3.73  
    3.74 -fun theorem k locale elems name atts p = multi_theorem k locale elems [((name, atts), [p])];
    3.75 -fun theorem_i k locale elems name atts p = multi_theorem_i k locale elems [((name, atts), [p])];
    3.76 +fun theorem k locale elems name atts p =
    3.77 +  multi_theorem k (name, atts) locale elems [(("", []), [p])];
    3.78 +fun theorem_i k locale elems name atts p =
    3.79 +  multi_theorem_i k (name, atts) locale elems [(("", []), [p])];
    3.80  
    3.81  
    3.82  (*local goals*)
    3.83 @@ -773,14 +781,15 @@
    3.84      val results = locale_results
    3.85        |> map (Drule.strip_shyps_warning o export locale_ctxt theory_ctxt);
    3.86  
    3.87 -    val (k, locale, attss) =
    3.88 +    val (k, (cname, catts), locale, attss) =
    3.89        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
    3.90 -    val (thy', res') =
    3.91 +    val (thy1, res') =
    3.92        theory_of state
    3.93        |> locale_prefix locale (PureThy.have_thmss [Drule.kind k]
    3.94            ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)))
    3.95        |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results);
    3.96 -  in (thy', (k, res')) end;
    3.97 +    val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1;
    3.98 +  in (thy2, (k, res')) end;
    3.99  
   3.100  (*note: clients should inspect first result only, as backtracking may destroy theory*)
   3.101  fun global_qed finalize state =