facts: handle multiple lists of arguments;
authorwenzelm
Thu Jun 29 22:32:08 2000 +0200 (2000-06-29)
changeset 91961f6f66fe777a
parent 9195 29f1e53f9937
child 9197 16d88c5547bd
facts: handle multiple lists of arguments;
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     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;
     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jun 29 22:31:53 2000 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jun 29 22:32:08 2000 +0200
     2.3 @@ -66,8 +66,9 @@
     2.4    val put_thms: string * thm list -> context -> context
     2.5    val put_thmss: (string * thm list) list -> context -> context
     2.6    val reset_thms: string -> context -> context
     2.7 -  val have_thmss: thm list -> string -> context attribute list
     2.8 -    -> (thm list * context attribute list) list -> context -> context * (string * thm list)
     2.9 +  val have_thmss:
    2.10 +    ((string * context attribute list) * (thm list * context attribute list) list) list ->
    2.11 +      context -> context * (string * thm list) list
    2.12    val assume: ((int -> tactic) * (int -> tactic))
    2.13      -> (string * context attribute list * (string * (string list * string list)) list) list
    2.14      -> context -> context * ((string * thm list) list * thm list)
    2.15 @@ -864,15 +865,17 @@
    2.16  
    2.17  (* have_thmss *)
    2.18  
    2.19 -fun have_thmss more_ths name more_attrs ths_attrs ctxt =
    2.20 +fun have_thss (ctxt, ((name, more_attrs), ths_attrs)) =
    2.21    let
    2.22      fun app ((ct, ths), (th, attrs)) =
    2.23        let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
    2.24        in (ct', th' :: ths) end
    2.25      val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
    2.26 -    val thms = flat (rev rev_thms) @ more_ths;
    2.27 +    val thms = flat (rev rev_thms);
    2.28    in (ctxt' |> put_thms (name, thms), (name, thms)) end;
    2.29  
    2.30 +fun have_thmss args ctxt = foldl_map have_thss (ctxt, args);
    2.31 +
    2.32  
    2.33  
    2.34  (** assumptions **)
    2.35 @@ -890,10 +893,10 @@
    2.36      val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
    2.37  
    2.38      val ths = map (fn th => ([th], [])) asms;
    2.39 -    val (ctxt'', (_, thms)) =
    2.40 +    val (ctxt'', [(_, thms)]) =
    2.41        ctxt'
    2.42        |> auto_bind_facts name props
    2.43 -      |> have_thmss [] name (attrs @ [Drule.tag_assumption]) ths;
    2.44 +      |> have_thmss [((name, attrs @ [Drule.tag_assumption]), ths)];
    2.45  
    2.46      val ctxt''' =
    2.47        ctxt''