src/Pure/Isar/proof_context.ML
changeset 7606 7905a74eb068
parent 7575 e1e2d07287d8
child 7663 460fedf14b09
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Sep 25 13:19:33 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Sep 25 13:20:12 1999 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4    val declare_term: term -> context -> context
     1.5    val declare_terms: term list -> context -> context
     1.6    val declare_thm: thm -> context -> context
     1.7 -  val add_binds: (indexname * string) list -> context -> context
     1.8 -  val add_binds_i: (indexname * term) list -> context -> context
     1.9 +  val add_binds: (indexname * string option) list -> context -> context
    1.10 +  val add_binds_i: (indexname * term option) list -> context -> context
    1.11    val match_binds: (string list * string) list -> context -> context
    1.12    val match_binds_i: (term list * term) list -> context -> context
    1.13    val bind_propp: context * (string * (string list * string list)) -> context * term
    1.14 @@ -47,6 +47,7 @@
    1.15    val put_thm: string * thm -> context -> context
    1.16    val put_thms: string * thm list -> context -> context
    1.17    val put_thmss: (string * thm list) list -> context -> context
    1.18 +  val reset_thms: string -> context -> context
    1.19    val have_thmss: thm list -> string -> context attribute list
    1.20      -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    1.21    val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list
    1.22 @@ -86,8 +87,8 @@
    1.23        ((cterm * ((int -> tactic) * (int -> tactic))) list *		(*assumes: A ==> _*)
    1.24          (string * thm list) list) *
    1.25        ((string * string) list * string list),                           (*fixes: !!x. _*)
    1.26 -    binds: (term * typ) Vartab.table,                                   (*term bindings*)
    1.27 -    thms: thm list Symtab.table,                                        (*local thms*)
    1.28 +    binds: (term * typ) option Vartab.table,                            (*term bindings*)
    1.29 +    thms: thm list option Symtab.table,                                 (*local thms*)
    1.30      defs:
    1.31        typ Vartab.table *                                                (*type constraints*)
    1.32        sort Vartab.table *                                               (*default sorts*)
    1.33 @@ -134,14 +135,16 @@
    1.34  
    1.35  (* term bindings *)
    1.36  
    1.37 +val smash_option = fn (_, None) => None | (xi, Some b) => Some (xi, b);
    1.38 +
    1.39  fun strings_of_binds (ctxt as Context {binds, ...}) =
    1.40    let
    1.41      val prt_term = Sign.pretty_term (sign_of ctxt);
    1.42      fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
    1.43 +    val bs = mapfilter smash_option (Vartab.dest binds);
    1.44    in
    1.45 -    if Vartab.is_empty binds andalso not (! verbose) then []
    1.46 -    else [Pretty.string_of (Pretty.big_list "term bindings:"
    1.47 -      (map pretty_bind (Vartab.dest binds)))]
    1.48 +    if null bs andalso not (! verbose) then []
    1.49 +    else [Pretty.string_of (Pretty.big_list "term bindings:" (map pretty_bind bs))]
    1.50    end;
    1.51  
    1.52  val print_binds = seq writeln o strings_of_binds;
    1.53 @@ -150,7 +153,7 @@
    1.54  (* local theorems *)
    1.55  
    1.56  fun strings_of_thms (Context {thms, ...}) =
    1.57 -  strings_of_items pretty_thm "local theorems:" (Symtab.dest thms);
    1.58 +  strings_of_items pretty_thm "local theorems:" (mapfilter smash_option (Symtab.dest thms));
    1.59  
    1.60  val print_thms = seq writeln o strings_of_thms;
    1.61  
    1.62 @@ -175,8 +178,11 @@
    1.63      val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
    1.64  
    1.65      (*fixes*)
    1.66 +    fun prt_fix (x, x') = Pretty.block
    1.67 +      [prt_term (Syntax.free x), Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
    1.68 +
    1.69      fun prt_fixes xs = Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
    1.70 -      Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs));
    1.71 +      Pretty.commas (map prt_fix xs));
    1.72  
    1.73  
    1.74      (* defaults *)
    1.75 @@ -387,10 +393,10 @@
    1.76  
    1.77      fun norm (t as Var (xi, T)) =
    1.78            (case Vartab.lookup (binds, xi) of
    1.79 -            Some (u, U) =>
    1.80 +            Some (Some (u, U)) =>
    1.81                if T = U then (norm u handle SAME => u)
    1.82                else raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u])
    1.83 -          | None => raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
    1.84 +          | _ => raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
    1.85        | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
    1.86        | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
    1.87        | norm (f $ t) =
    1.88 @@ -429,7 +435,9 @@
    1.89    let
    1.90      fun def_type xi =
    1.91        (case Vartab.lookup (types, xi) of
    1.92 -        None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
    1.93 +        None =>
    1.94 +          if is_pat then None
    1.95 +          else (case Vartab.lookup (binds, xi) of Some (Some (_, T)) => Some T | _ => None)
    1.96        | some => some);
    1.97  
    1.98      fun def_sort xi = Vartab.lookup (sorts, xi);
    1.99 @@ -512,23 +520,33 @@
   1.100  
   1.101  (* update_binds *)
   1.102  
   1.103 +fun del_bind (ctxt, xi) =
   1.104 +  ctxt
   1.105 +  |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   1.106 +      (thy, data, asms, Vartab.update ((xi, None), binds), thms, defs));
   1.107 +
   1.108  fun upd_bind (ctxt, (xi, t)) =
   1.109    let val T = fastype_of t in
   1.110      ctxt
   1.111      |> declare_term t
   1.112      |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   1.113 -        (thy, data, asms, Vartab.update ((xi, (t, T)), binds), thms, defs))
   1.114 +        (thy, data, asms, Vartab.update ((xi, Some (t, T)), binds), thms, defs))
   1.115    end;
   1.116  
   1.117 +fun del_upd_bind (ctxt, (xi, None)) = del_bind (ctxt, xi)
   1.118 +  | del_upd_bind (ctxt, (xi, Some t)) = upd_bind (ctxt, (xi, t));
   1.119 +
   1.120  fun update_binds bs ctxt = foldl upd_bind (ctxt, bs);
   1.121  fun update_binds_env env = (*Envir.norm_term ensures proper type instantiation*)
   1.122    update_binds (map (apsnd (Envir.norm_term env)) (Envir.alist_of env));
   1.123  
   1.124 +fun delete_update_binds bs ctxt = foldl del_upd_bind (ctxt, bs);
   1.125 +
   1.126  
   1.127  (* add_binds(_i) -- sequential *)
   1.128  
   1.129  fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) =
   1.130 -  ctxt |> update_binds [(xi, prep ctxt raw_t)];
   1.131 +  ctxt |> delete_update_binds [(xi, apsome (prep ctxt) raw_t)];
   1.132  
   1.133  fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds);
   1.134  
   1.135 @@ -543,7 +561,6 @@
   1.136      val t = prep ctxt raw_t;
   1.137      val ctxt' = ctxt |> declare_term t;
   1.138      val matches = map (fn (f, raw_pat) => (prep_pat ctxt' raw_pat, f t)) raw_pats;
   1.139 -           (* FIXME seq / par / simult (??) *)
   1.140    in (ctxt', (matches, t)) end;
   1.141  
   1.142  fun gen_match_binds _ [] ctxt = ctxt
   1.143 @@ -589,14 +606,14 @@
   1.144  
   1.145  fun get_thm (ctxt as Context {thy, thms, ...}) name =
   1.146    (case Symtab.lookup (thms, name) of
   1.147 -    Some [th] => th
   1.148 -  | Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
   1.149 -  | None => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.150 +    Some (Some [th]) => th
   1.151 +  | Some (Some _) => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
   1.152 +  | _ => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.153  
   1.154  fun get_thms (ctxt as Context {thy, thms, ...}) name =
   1.155    (case Symtab.lookup (thms, name) of
   1.156 -    Some ths => ths
   1.157 -  | None => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.158 +    Some (Some ths) => ths
   1.159 +  | _ => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.160  
   1.161  fun get_thmss ctxt names = flat (map (get_thms ctxt) names);
   1.162  
   1.163 @@ -606,7 +623,7 @@
   1.164  fun put_thms ("", _) = I
   1.165    | put_thms (name, ths) = map_context
   1.166        (fn (thy, data, asms, binds, thms, defs) =>
   1.167 -        (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
   1.168 +        (thy, data, asms, binds, Symtab.update ((name, Some ths), thms), defs));
   1.169  
   1.170  fun put_thm (name, th) = put_thms (name, [th]);
   1.171  
   1.172 @@ -614,6 +631,12 @@
   1.173    | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
   1.174  
   1.175  
   1.176 +(* reset_thms *)
   1.177 +
   1.178 +fun reset_thms name = map_context (fn (thy, data, asms, binds, thms, defs) =>
   1.179 +  (thy, data, asms, binds, Symtab.update ((name, None), thms), defs));
   1.180 +
   1.181 +
   1.182  (* have_thmss *)
   1.183  
   1.184  fun have_thmss more_ths name more_attrs ths_attrs ctxt =