propp: 'concl' patterns;
authorwenzelm
Thu Jul 08 18:32:43 1999 +0200 (1999-07-08)
changeset 6931bd8aa6ae6bcd
parent 6930 4b40fb299f9f
child 6932 77c14313af51
propp: 'concl' patterns;
assumptions: tactics for non-goal export;
use Display.pretty_thm_no_hyps;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jul 08 18:31:04 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jul 08 18:32:43 1999 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4    val add_binds_i: (indexname * term) list -> context -> context
     1.5    val match_binds: (string list * string) list -> context -> context
     1.6    val match_binds_i: (term list * term) list -> context -> context
     1.7 -  val bind_propp: context * (string * string list) -> context * term
     1.8 -  val bind_propp_i: context * (term * term list) -> context * term
     1.9 +  val bind_propp: context * (string * (string list * string list)) -> context * term
    1.10 +  val bind_propp_i: context * (term * (term list * term list)) -> context * term
    1.11    val auto_bind_goal: term -> context -> context
    1.12    val auto_bind_facts: string -> term list -> context -> context
    1.13    val thms_closure: context -> xstring -> thm list option
    1.14 @@ -46,11 +46,13 @@
    1.15    val put_thmss: (string * thm list) list -> context -> context
    1.16    val have_thmss: thm list -> string -> context attribute list
    1.17      -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    1.18 -  val assumptions: context -> (cterm * (int -> tactic)) list
    1.19 +  val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list
    1.20    val fixed_names: context -> string list
    1.21 -  val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    1.22 +  val assume: ((int -> tactic) * (int -> tactic)) -> string -> context attribute list
    1.23 +    -> (string * (string list * string list)) list
    1.24      -> context -> context * ((string * thm list) * thm list)
    1.25 -  val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    1.26 +  val assume_i: ((int -> tactic) * (int -> tactic)) -> string -> context attribute list
    1.27 +    -> (term * (term list * term list)) list
    1.28      -> context -> context * ((string * thm list) * thm list)
    1.29    val fix: (string * string option) list -> context -> context
    1.30    val fix_i: (string * typ) list -> context -> context
    1.31 @@ -79,7 +81,8 @@
    1.32     {thy: theory,                                                        (*current theory*)
    1.33      data: Object.T Symtab.table,                                        (*user data*)
    1.34      asms:
    1.35 -      ((cterm * (int -> tactic)) list * (string * thm list) list) *     (*assumes: A ==> _*)
    1.36 +      ((cterm * ((int -> tactic) * (int -> tactic))) list *		(*assumes: A ==> _*)
    1.37 +        (string * thm list) list) *
    1.38        ((string * string) list * string list),                           (*fixes: !!x. _*)
    1.39      binds: (term * typ) Vartab.table,                                   (*term bindings*)
    1.40      thms: thm list Symtab.table,                                        (*local thms*)
    1.41 @@ -142,8 +145,7 @@
    1.42  (* local theorems *)
    1.43  
    1.44  fun strings_of_thms (Context {thms, ...}) =
    1.45 -  strings_of_items (setmp Display.show_hyps false Display.pretty_thm)
    1.46 -    "Local theorems:" (Symtab.dest thms);
    1.47 +  strings_of_items Display.pretty_thm_no_hyps "Local theorems:" (Symtab.dest thms);
    1.48  
    1.49  val print_thms = seq writeln o strings_of_thms;
    1.50  
    1.51 @@ -537,12 +539,14 @@
    1.52    let
    1.53      val t = prep ctxt raw_t;
    1.54      val ctxt' = ctxt |> declare_term t;
    1.55 -    val pats = map (prep_pat ctxt') raw_pats;           (* FIXME seq / par / simult (??) *)
    1.56 -  in (ctxt', (map (rpair t) pats, t)) end;
    1.57 +    val matches = map (fn (f, raw_pat) => (prep_pat ctxt' raw_pat, f t)) raw_pats;
    1.58 +           (* FIXME seq / par / simult (??) *)
    1.59 +  in (ctxt', (matches, t)) end;
    1.60  
    1.61  fun gen_match_binds _ [] ctxt = ctxt
    1.62 -  | gen_match_binds prepp raw_pairs ctxt =
    1.63 +  | gen_match_binds prepp args ctxt =
    1.64        let
    1.65 +        val raw_pairs = map (apfst (map (pair I))) args;
    1.66          val (ctxt', matches) = foldl_map (prep_declare_match prepp) (ctxt, raw_pairs);
    1.67          val pairs = flat (map #1 matches);
    1.68          val Context {defs = (_, _, maxidx, _), ...} = ctxt';
    1.69 @@ -559,8 +563,10 @@
    1.70  
    1.71  (* bind proposition patterns *)
    1.72  
    1.73 -fun gen_bind_propp prepp (ctxt, (raw_prop, raw_pats)) =
    1.74 -  let val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop))
    1.75 +fun gen_bind_propp prepp (ctxt, (raw_prop, (raw_pats1, raw_pats2))) =
    1.76 +  let
    1.77 +    val raw_pats = map (pair I) raw_pats1 @ map (pair Logic.strip_imp_concl) raw_pats2;
    1.78 +    val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop));
    1.79    in (ctxt' |> match_binds_i (map (apfst single) pairs), prop) end;
    1.80  
    1.81  val bind_propp = gen_bind_propp (read_prop_pat, read_prop);
    1.82 @@ -661,7 +667,7 @@
    1.83        ctxt''
    1.84        |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, defs) =>
    1.85          (thy, data, ((asms_ct @ cprops_tac, asms_th @ [(name, asms)]), fixes), binds, thms, defs));
    1.86 -  in (ctxt''', ((name, thms), prems ctxt')) end;
    1.87 +  in (ctxt''', ((name, thms), prems ctxt''')) end;
    1.88  
    1.89  val assume = gen_assume bind_propp;
    1.90  val assume_i = gen_assume bind_propp_i;
    1.91 @@ -687,7 +693,7 @@
    1.92  val fix_i = gen_fixs cert_typ false;
    1.93  
    1.94  
    1.95 -(* transfer_used_names *)
    1.96 +(* used names *)
    1.97  
    1.98  fun transfer_used_names (Context {asms = (_, (_, names)), defs = (_, _, _, used), ...}) =
    1.99    map_context (fn (thy, data, (asms, (fixes, _)), binds, thms, (types, sorts, maxidx, _)) =>