src/Pure/Isar/proof.ML

 
 Proof states and methods.
 
 TODO:
   - assume: improve schematic Vars handling (!?);
+  - warn_vars;
   - bind: check rhs (extra (T)Vars etc.) (How to handle these anyway?);
   - prep_result: avoid duplicate asms;
-  - goal: need asms field? (may take from goal context!?);
-  - finish: filter results (!??) (no?);
-  - finish_tac: make a parameter (method) (!!?);
   - prep_result error: use error channel (!);
+  - check_finished: trace results (!?);
   - next_block: fetch_facts (!?);
-  - warn_vars;
-  - string constants in one place (e.g. "it", "thesis") (??!);
-  - check_finished: trace results (!?);
 *)
 
 signature PROOF =
 sig
   type context

   val refine: (context -> method) -> state -> state Seq.seq
   val bind: (indexname * string) list -> state -> state
   val bind_i: (indexname * term) list -> state -> state
   val match_bind: (string * string) list -> state -> state
   val match_bind_i: (term * term) list -> state -> state
-  val have_tthms: string -> context attribute list ->
-    (tthm * context attribute list) list -> state -> state
+  val have_tthmss: string -> context attribute list ->
+    (tthm list * context attribute list) list -> state -> state
   val assume: string -> context attribute list -> string list -> state -> state
   val assume_i: string -> context attribute list -> term list -> state -> state
   val fix: (string * string option) list -> state -> state
   val fix_i: (string * typ) list -> state -> state
   val theorem: bstring -> theory attribute list -> string -> theory -> state

 sig
   include PROOF
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> state -> state
 end;
 
-
 structure Proof: PROOF_PRIVATE =
 struct
 
 
 (** proof state **)

 
 val match_bind = gen_bind ProofContext.match_binds;
 val match_bind_i = gen_bind ProofContext.match_binds_i;
 
 
-(* have_tthms *)
-
-val def_name = fn "" => "it" | name => name;
-
-fun have_tthms name atts ths_atts state =
-  state
-  |> assert_forward
-  |> map_context_result (ProofContext.have_tthms (def_name name) atts ths_atts)
+(* have_tthmss *)
+
+fun have_tthmss name atts ths_atts state =
+  state
+  |> assert_forward
+  |> map_context_result (ProofContext.have_tthmss (PureThy.default_name name) atts ths_atts)
   |> these_facts;
 
 
 (* fix *)
 

 (* assume *)
 
 fun gen_assume f name atts props state =
   state
   |> assert_forward
-  |> map_context_result (f (def_name name) atts props)
+  |> map_context_result (f (PureThy.default_name name) atts props)
   |> these_facts
   |> (fn st => let_tthms ("prems", ProofContext.assumptions (context_of st)) st);
 
 val assume = gen_assume ProofContext.assume;
 val assume_i = gen_assume ProofContext.assume_i;

     |> assert_forward_or_chain
     |> enter_forward
     |> opt_block
 
     |> declare_term prop
-    |> put_goal (Some ((kind atts, (def_name name), casms, prop), ([], thm)))
+    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm)))
     |> bind_props [("thesis", prop)]
     |> (if is_chain state then use_facts else reset_facts)
 
     |> new_block
     |> enter_backward

       | Aux atts => (atts, Seq.single)
       | _ => raise STATE ("No local goal!", state));
   in
     state
     |> close_block
-    |> have_tthms name atts [((result, []), [])]
+    |> have_tthmss name atts [([(result, [])], [])]
     |> opt_solve
   end;
 
 fun end_block meth_fun state =
   if can assert_current_goal (close_block state) then

 
     val name = if_none alt_name def_name;
     val atts =
       (case kind of
         Theorem atts => if_none alt_atts atts
-      | Lemma atts => Attribute.tag_lemma :: if_none alt_atts atts
+      | Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma]
       | _ => raise STATE ("No global goal!", state));
 
     val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state);
   in (thy', (kind_name kind, name, result')) end;