src/Pure/Isar/proof.ML
changeset 7271 442456b2a8bb
parent 7201 59b9b7aec3c5
child 7412 35ebe1452c10
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Aug 18 20:45:18 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Aug 18 20:45:52 1999 +0200
     1.3 @@ -42,17 +42,19 @@
     1.4    val simple_have_thms: string -> thm list -> state -> state
     1.5    val fix: (string * string option) list -> state -> state
     1.6    val fix_i: (string * typ) list -> state -> state
     1.7 -  val assm: (int -> tactic) * (int -> tactic) -> string -> context attribute list
     1.8 -    -> (string * (string list * string list)) list -> state -> state
     1.9 -  val assm_i: (int -> tactic) * (int -> tactic) -> string -> context attribute list
    1.10 -    -> (term * (term list * term list)) list -> state -> state
    1.11 -  val assume: string -> context attribute list -> (string * (string list * string list)) list
    1.12 +  val assm: (int -> tactic) * (int -> tactic)
    1.13 +    -> (string * context attribute list * (string * (string list * string list)) list) list
    1.14 +    -> state -> state
    1.15 +  val assm_i: (int -> tactic) * (int -> tactic)
    1.16 +    -> (string * context attribute list * (term * (term list * term list)) list) list
    1.17      -> state -> state
    1.18 -  val assume_i: string -> context attribute list -> (term * (term list * term list)) list
    1.19 +  val assume: (string * context attribute list * (string * (string list * string list)) list) list
    1.20 +    -> state -> state
    1.21 +  val assume_i: (string * context attribute list * (term * (term list * term list)) list) list
    1.22      -> state -> state
    1.23 -  val presume: string -> context attribute list -> (string * (string list * string list)) list
    1.24 +  val presume: (string * context attribute list * (string * (string list * string list)) list) list
    1.25      -> state -> state
    1.26 -  val presume_i: string -> context attribute list -> (term * (term list * term list)) list
    1.27 +  val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
    1.28      -> state -> state
    1.29    val theorem: bstring -> theory attribute list -> string * (string list * string list)
    1.30      -> theory -> state
    1.31 @@ -526,26 +528,33 @@
    1.32  
    1.33  (* assume *)
    1.34  
    1.35 -fun gen_assume f tacs name atts props state =
    1.36 +local
    1.37 +
    1.38 +fun def_name (name, x, y) = (PureThy.default_name name, x, y);
    1.39 +
    1.40 +fun gen_assume f tac args state =
    1.41    state
    1.42    |> assert_forward
    1.43 -  |> map_context_result (f tacs (PureThy.default_name name) atts props)
    1.44 -  |> (fn (st, (facts, prems)) =>
    1.45 -    (st, facts)
    1.46 -    |> these_facts
    1.47 -    |> put_thms ("prems", prems));
    1.48 -
    1.49 -val assm = gen_assume ProofContext.assume;
    1.50 -val assm_i = gen_assume ProofContext.assume_i;
    1.51 +  |> map_context_result (f tac (map def_name args))
    1.52 +  |> (fn (st, (factss, prems)) =>
    1.53 +    foldl these_facts (st, factss)
    1.54 +    |> put_thms ("prems", prems)
    1.55 +    |> put_facts (Some (flat (map #2 factss))));
    1.56  
    1.57  val hard_asm_tac = Tactic.etac Drule.triv_goal;
    1.58  val soft_asm_tac = Tactic.rtac Drule.triv_goal;
    1.59  
    1.60 +in
    1.61 +
    1.62 +val assm = gen_assume ProofContext.assume;
    1.63 +val assm_i = gen_assume ProofContext.assume_i;
    1.64  val assume = assm (hard_asm_tac, soft_asm_tac);
    1.65  val assume_i = assm_i (hard_asm_tac, soft_asm_tac);
    1.66  val presume = assm (soft_asm_tac, soft_asm_tac);
    1.67  val presume_i = assm_i (soft_asm_tac, soft_asm_tac);
    1.68  
    1.69 +end;
    1.70 +
    1.71  
    1.72  
    1.73  (** goals **)