src/Pure/Isar/proof_context.ML
changeset 6797 f86b96a0f6fb
parent 6789 0e5a965de17a
child 6847 f175f56c57a6
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jun 07 22:16:56 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jun 07 22:17:23 1999 +0200
     1.3 @@ -3,10 +3,6 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Proof context information.
     1.7 -
     1.8 -TODO:
     1.9 -  - pretty_bind: use syntax (!?) (show_types etc.);
    1.10 -  - smash_unifiers: ever invents new vars (???);
    1.11  *)
    1.12  
    1.13  signature PROOF_CONTEXT =
    1.14 @@ -40,7 +36,7 @@
    1.15    val bind_propp: context * (string * string list) -> context * term
    1.16    val bind_propp_i: context * (term * term list) -> context * term
    1.17    val auto_bind_goal: term -> context -> context
    1.18 -  val auto_bind_facts: term list -> context -> context
    1.19 +  val auto_bind_facts: string -> term list -> context -> context
    1.20    val thms_closure: context -> xstring -> thm list option
    1.21    val get_thm: context -> string -> thm
    1.22    val get_thms: context -> string -> thm list
    1.23 @@ -50,12 +46,12 @@
    1.24    val put_thmss: (string * thm list) list -> context -> context
    1.25    val have_thmss: string -> context attribute list
    1.26      -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    1.27 -  val assumptions: context -> thm list
    1.28 +  val assumptions: context -> cterm list
    1.29    val fixed_names: context -> string list
    1.30    val assume: string -> context attribute list -> (string * string list) list -> context
    1.31 -    -> context * (string * thm list)
    1.32 +    -> context * ((string * thm list) * thm list)
    1.33    val assume_i: string -> context attribute list -> (term * term list) list -> context
    1.34 -    -> context * (string * thm list)
    1.35 +    -> context * ((string * thm list) * thm list)
    1.36    val fix: (string * string option) list -> context -> context
    1.37    val fix_i: (string * typ) list -> context -> context
    1.38    val setup: (theory -> theory) list
    1.39 @@ -82,7 +78,7 @@
    1.40     {thy: theory,                                (*current theory*)
    1.41      data: Object.T Symtab.table,                (*user data*)
    1.42      asms:
    1.43 -      (string * thm list) list *                (*assumes: A ==> _*)
    1.44 +      (cterm list * (string * thm list) list) * (*assumes: A ==> _*)
    1.45        ((string * string) list * string list),   (*fixes: !!x. _*)
    1.46      binds: (term * typ) Vartab.table,           (*term bindings*)
    1.47      thms: thm list Symtab.table,                (*local thms*)
    1.48 @@ -147,7 +143,7 @@
    1.49  
    1.50  (* main context *)
    1.51  
    1.52 -fun print_context (ctxt as Context {thy, data = _, asms = (assumes, (fixes, _)), binds = _,
    1.53 +fun print_context (ctxt as Context {thy, data = _, asms = ((_, prems), (fixes, _)), binds = _,
    1.54      thms = _, defs = (types, sorts, maxidx, used)}) =
    1.55    let
    1.56      val sign = Theory.sign_of thy;
    1.57 @@ -179,7 +175,7 @@
    1.58      verb Pretty.writeln pretty_thy;
    1.59      if null fixes andalso not (! verbose) then ()
    1.60      else Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
    1.61 -    print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
    1.62 +    print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" prems;
    1.63      verb print_binds ctxt;
    1.64      verb print_thms ctxt;
    1.65      verb Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
    1.66 @@ -278,7 +274,7 @@
    1.67  
    1.68  fun init thy =
    1.69    let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
    1.70 -    make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty,
    1.71 +    make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty,
    1.72        (Vartab.empty, Vartab.empty, ~1, []))
    1.73    end;
    1.74  
    1.75 @@ -567,7 +563,7 @@
    1.76  (* auto binds *)
    1.77  
    1.78  val auto_bind_goal = add_binds_i o AutoBind.goal;
    1.79 -val auto_bind_facts = add_binds_i o AutoBind.facts;
    1.80 +val auto_bind_facts = add_binds_i oo AutoBind.facts;
    1.81  
    1.82  
    1.83  
    1.84 @@ -630,30 +626,34 @@
    1.85  
    1.86  (* get assumptions *)
    1.87  
    1.88 -fun assumptions (Context {asms = (asms, _), ...}) = flat (map #2 asms);
    1.89 +fun assumptions (Context {asms = ((asms_ct, _), _), ...}) = asms_ct;
    1.90  fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes;
    1.91  
    1.92  
    1.93  (* assume *)
    1.94  
    1.95 +fun prems (Context {asms = ((_, asms_th), _), ...}) = flat (map #2 asms_th);
    1.96 +
    1.97  fun gen_assume prepp name attrs raw_prop_pats ctxt =
    1.98    let
    1.99      val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
   1.100      val sign = sign_of ctxt';
   1.101 +    val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   1.102  
   1.103 -    val asms = map (Thm.assume o Thm.cterm_of sign) props;
   1.104 +    val cprops = map (Thm.cterm_of sign) props;
   1.105 +    val asms = map (Drule.forall_elim_vars (maxidx + 1) o Thm.assume) cprops;
   1.106  
   1.107      val ths = map (fn th => ([th], [])) asms;
   1.108      val (ctxt'', (_, thms)) =
   1.109        ctxt'
   1.110 -      |> auto_bind_facts props
   1.111 +      |> auto_bind_facts name props
   1.112        |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
   1.113  
   1.114      val ctxt''' =
   1.115        ctxt''
   1.116 -      |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
   1.117 -        (thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs));
   1.118 -  in (ctxt''', (name, thms)) end;
   1.119 +      |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, defs) =>
   1.120 +        (thy, data, ((asms_ct @ cprops, asms_th @ [(name, asms)]), fixes), binds, thms, defs));
   1.121 +  in (ctxt''', ((name, thms), prems ctxt')) end;
   1.122  
   1.123  val assume = gen_assume bind_propp;
   1.124  val assume_i = gen_assume bind_propp_i;