src/Pure/Isar/proof.ML
changeset 9196 1f6f66fe777a
parent 8991 dc70b797827f
child 9292 c5875175751f
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jun 29 22:31:53 2000 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jun 29 22:32:08 2000 +0200
     1.3 @@ -50,9 +50,11 @@
     1.4    val match_bind_i: (term list * term) list -> state -> state
     1.5    val let_bind: (string list * string) list -> state -> state
     1.6    val let_bind_i: (term list * term) list -> state -> state
     1.7 -  val have_thmss: thm list -> string -> context attribute list ->
     1.8 -    (thm list * context attribute list) list -> state -> state
     1.9    val simple_have_thms: string -> thm list -> state -> state
    1.10 +  val have_thmss: ((string * context attribute list) *
    1.11 +    (thm list * context attribute list) list) list -> state -> state
    1.12 +  val with_thmss: ((string * context attribute list) *
    1.13 +    (thm list * context attribute list) list) list -> state -> state
    1.14    val fix: (string list * string option) list -> state -> state
    1.15    val fix_i: (string list * typ option) list -> state -> state
    1.16    val assm: (int -> tactic) * (int -> tactic)
    1.17 @@ -218,12 +220,10 @@
    1.18  
    1.19  val reset_facts = put_facts None;
    1.20  
    1.21 -fun have_facts (name, facts) state =
    1.22 +fun these_factss (state, named_factss) =
    1.23    state
    1.24 -  |> put_facts (Some facts)
    1.25 -  |> put_thms (name, facts);
    1.26 -
    1.27 -fun these_facts (state, ths) = have_facts ths state;
    1.28 +  |> put_thmss named_factss
    1.29 +  |> put_facts (Some (flat (map #2 named_factss)));
    1.30  
    1.31  
    1.32  (* goal *)
    1.33 @@ -268,7 +268,7 @@
    1.34  fun assert_mode pred state =
    1.35    let val mode = get_mode state in
    1.36      if pred mode then state
    1.37 -    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
    1.38 +    else raise STATE ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode", state)
    1.39    end;
    1.40  
    1.41  fun is_chain state = get_mode state = ForwardChain;
    1.42 @@ -466,15 +466,19 @@
    1.43  val let_bind_i = gen_bind (ProofContext.match_bind_i true);
    1.44  
    1.45  
    1.46 -(* have_thmss *)
    1.47 +(* have_thmss etc. *)
    1.48  
    1.49 -fun have_thmss ths name atts ths_atts state =
    1.50 +fun have_thmss args state =
    1.51    state
    1.52    |> assert_forward
    1.53 -  |> map_context_result (ProofContext.have_thmss ths name atts ths_atts)
    1.54 -  |> these_facts;
    1.55 +  |> map_context_result (ProofContext.have_thmss args)
    1.56 +  |> these_factss;
    1.57  
    1.58 -fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
    1.59 +fun simple_have_thms name thms = have_thmss [((name, []), [(thms, [])])];
    1.60 +
    1.61 +fun with_thmss args state =
    1.62 +  let val state' = state |> have_thmss args
    1.63 +  in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end;
    1.64  
    1.65  
    1.66  (* fix *)
    1.67 @@ -498,9 +502,8 @@
    1.68    |> assert_forward
    1.69    |> map_context_result (f tac args)
    1.70    |> (fn (st, (factss, prems)) =>
    1.71 -    foldl these_facts (st, factss)
    1.72 -    |> put_thms ("prems", prems)
    1.73 -    |> put_facts (Some (flat (map #2 factss))));
    1.74 +    these_factss (st, factss)
    1.75 +    |> put_thms ("prems", prems));
    1.76  
    1.77  val hard_asm_tac = Tactic.etac Drule.triv_goal;
    1.78  val soft_asm_tac = Tactic.rtac Drule.triv_goal
    1.79 @@ -641,8 +644,8 @@
    1.80      print_result {kind = kind_name kind, name = name, thm = result};
    1.81      outer_state
    1.82      |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t]
    1.83 -    |> have_thmss [] name atts [Thm.no_attributes
    1.84 -        [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]]
    1.85 +    |> have_thmss [((name, atts), [Thm.no_attributes
    1.86 +        [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]])]
    1.87      |> opt_solve
    1.88      |> (Seq.flat o Seq.map after_qed)
    1.89    end;