improved treatment of common result name;
authorwenzelm
Mon Nov 19 23:37:01 2001 +0100 (2001-11-19 ago)
changeset 12244179f142ffb03
parent 12243 a2c0aaf94460
child 12245 3dd9aae402bb
improved treatment of common result name;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:47:57 2001 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 19 23:37:01 2001 +0100
     1.3 @@ -297,14 +297,16 @@
     1.4  (* statements *)
     1.5  
     1.6  val in_locale_elems =
     1.7 -  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.xname -- P.opt_attribs --| P.$$$ ")") --
     1.8 -  Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.locale_element --| P.$$$ ")")) [];
     1.9 +  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname -- P.opt_attribs --| P.$$$ ")")) --
    1.10 +  Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
    1.11  
    1.12  val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
    1.13 +val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement;
    1.14  
    1.15  fun gen_theorem k =
    1.16    OuterSyntax.command k ("state " ^ k) K.thy_goal
    1.17 -    (P.opt_thm_name ":" -- in_locale_elems -- statement >> (fn ((x, y), z) =>
    1.18 +    (Scan.optional (P.thm_name ":" --| Scan.ahead (P.$$$ "(")) ("", [])
    1.19 +      -- in_locale_elems -- statement' >> (fn ((x, y), z) =>
    1.20        (Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
    1.21  
    1.22  val theoremP = gen_theorem Drule.theoremK;
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:47:57 2001 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 19 23:37:01 2001 +0100
     2.3 @@ -203,6 +203,7 @@
     2.4  struct
     2.5  
     2.6  
     2.7 +
     2.8  (** derived theory and proof operations **)
     2.9  
    2.10  (* markup commands *)
    2.11 @@ -382,13 +383,18 @@
    2.12  
    2.13  local
    2.14  
    2.15 -fun pretty_result ctxt k (name, ths) = Pretty.block
    2.16 -  [Pretty.str (k ^ (if name = "" then "" else " " ^ name ^ ":")), Pretty.brk 1,
    2.17 -    ProofContext.pretty_thms ctxt ths];
    2.18 +fun prt_fact ctxt ("", ths) = ProofContext.pretty_thms ctxt ths
    2.19 +  | prt_fact ctxt (name, ths) =
    2.20 +      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, ProofContext.pretty_thms ctxt ths];
    2.21  
    2.22 -fun pretty_results ctxt (kind, r :: rs) =
    2.23 -      pretty_result ctxt kind r :: map (pretty_result ctxt "and") rs
    2.24 -  | pretty_results _ (_, []) = [];
    2.25 +fun prt_facts ctxt =
    2.26 +  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o map (single o prt_fact ctxt);
    2.27 +
    2.28 +fun pretty_results ctxt ((kind, ""), facts) =
    2.29 +      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts)
    2.30 +  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    2.31 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    2.32 +        Pretty.blk (1, Pretty.str "(" :: prt_facts ctxt facts @ [Pretty.str ")"])]);
    2.33  
    2.34  fun pretty_rule s ctxt thm =
    2.35    Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
    2.36 @@ -396,10 +402,11 @@
    2.37  
    2.38  in
    2.39  
    2.40 -val print_result = (Pretty.writeln o Pretty.chunks) oo pretty_results;
    2.41 +val print_result = Pretty.writeln oo pretty_results;
    2.42 +fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
    2.43  
    2.44  fun cond_print_result_rule int =
    2.45 -  if int then (print_result, priority oo (Pretty.string_of oo pretty_rule "Attempt"))
    2.46 +  if int then (print_result', priority oo (Pretty.string_of oo pretty_rule "Attempt"))
    2.47    else (K (K ()), K (K ()));
    2.48  
    2.49  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
    2.50 @@ -422,7 +429,7 @@
    2.51            |> Library.transform_error;
    2.52          val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
    2.53        in (case result of (Some _, None) => () | (_, exn) => warn exn); state end;
    2.54 -      
    2.55 +
    2.56  end;
    2.57  
    2.58  
    2.59 @@ -536,10 +543,10 @@
    2.60    let
    2.61      val state = ProofHistory.current prf;
    2.62      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    2.63 -    val (thy, (kind, res)) = finish state;
    2.64 +    val (thy, ((kind, name), res)) = finish state;
    2.65    in
    2.66      if kind = "" orelse kind = Drule.internalK then ()
    2.67 -    else (print_result (Proof.context_of state) (kind, res);
    2.68 +    else (print_result (Proof.context_of state) ((kind, name), res);
    2.69        Context.setmp (Some thy) Present.multi_result (kind, res));
    2.70      thy
    2.71    end);
     3.1 --- a/src/Pure/Isar/method.ML	Mon Nov 19 20:47:57 2001 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Mon Nov 19 23:37:01 2001 +0100
     3.3 @@ -115,12 +115,13 @@
     3.4    val local_done_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     3.5      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
     3.6    val global_qed: bool -> text option
     3.7 -    -> Proof.state -> theory * (string * (string * thm list) list)
     3.8 +    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
     3.9    val global_terminal_proof: text * text option
    3.10 -    -> Proof.state -> theory * (string * (string * thm list) list)
    3.11 -  val global_default_proof: Proof.state -> theory * (string * (string * thm list) list)
    3.12 -  val global_immediate_proof: Proof.state -> theory * (string * (string * thm list) list)
    3.13 -  val global_done_proof: Proof.state -> theory * (string * (string * thm list) list)
    3.14 +    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
    3.15 +  val global_default_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
    3.16 +  val global_immediate_proof: Proof.state ->
    3.17 +    theory * ((string * string) * (string * thm list) list)
    3.18 +  val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
    3.19    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
    3.20      -> Args.src -> Proof.context -> Proof.method
    3.21    val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
     4.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 19 20:47:57 2001 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 19 23:37:01 2001 +0100
     4.3 @@ -109,7 +109,7 @@
     4.4      -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
     4.5      -> state -> state Seq.seq
     4.6    val global_qed: (state -> state Seq.seq) -> state
     4.7 -    -> (theory * (string * (string * thm list) list)) Seq.seq
     4.8 +    -> (theory * ((string * string) * (string * thm list) list)) Seq.seq
     4.9    val begin_block: state -> state
    4.10    val end_block: state -> state Seq.seq
    4.11    val next_block: state -> state
    4.12 @@ -789,7 +789,7 @@
    4.13            ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)))
    4.14        |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results);
    4.15      val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1;
    4.16 -  in (thy2, (k, res')) end;
    4.17 +  in (thy2, ((k, cname), res')) end;
    4.18  
    4.19  (*note: clients should inspect first result only, as backtracking may destroy theory*)
    4.20  fun global_qed finalize state =
     5.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Nov 19 20:47:57 2001 +0100
     5.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 19 23:37:01 2001 +0100
     5.3 @@ -14,7 +14,7 @@
     5.4    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     5.5    val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     5.6      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
     5.7 -  val global_skip_proof: Proof.state -> theory * (string * (string * thm list) list)
     5.8 +  val global_skip_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
     5.9    val setup: (theory -> theory) list
    5.10  end;
    5.11