src/Pure/Isar/proof_context.ML
changeset 5874 a58d4528121d
parent 5819 5fff21d4ca3a
child 5919 a5b2d4b9ed6f
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 16 10:44:55 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 16 10:45:52 1998 +0100
     1.3 @@ -22,9 +22,10 @@
     1.4    val print_thms: context -> unit
     1.5    val print_context: context -> unit
     1.6    val print_proof_data: theory -> unit
     1.7 -  val init_context: theory -> context
     1.8 +  val init: theory -> context
     1.9    val read_typ: context -> string -> typ
    1.10    val cert_typ: context -> typ -> typ
    1.11 +  val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
    1.12    val read_term: context -> string -> term
    1.13    val read_prop: context -> string -> term
    1.14    val read_pat: context -> string -> term
    1.15 @@ -32,6 +33,7 @@
    1.16    val cert_prop: context -> term -> term
    1.17    val declare_term: term -> context -> context
    1.18    val declare_terms: term list -> context -> context
    1.19 +  val declare_thm: thm -> context -> context
    1.20    val add_binds: (indexname * string) list -> context -> context
    1.21    val add_binds_i: (indexname * term) list -> context -> context
    1.22    val match_binds: (string * string) list -> context -> context
    1.23 @@ -66,7 +68,6 @@
    1.24    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
    1.25  end;
    1.26  
    1.27 -
    1.28  structure ProofContext: PROOF_CONTEXT_PRIVATE =
    1.29  struct
    1.30  
    1.31 @@ -265,8 +266,8 @@
    1.32  
    1.33  (* init context *)
    1.34  
    1.35 -fun init_context thy =
    1.36 -  let val data = Symtab.map (fn (_, (init, _)) => init thy) (ProofDataData.get thy) in
    1.37 +fun init thy =
    1.38 +  let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
    1.39      make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty,
    1.40        (Vartab.empty, Vartab.empty, ~1, []))
    1.41    end;
    1.42 @@ -301,13 +302,18 @@
    1.43  
    1.44  (* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
    1.45  
    1.46 -fun read_def_termT sg (types, sorts, used) (s, T) =
    1.47 -  Thm.term_of (#1 (Thm.read_def_cterm (sg, types, sorts) used true (s, T)));
    1.48 +fun read_def_termTs freeze sg (types, sorts, used) sTs =
    1.49 +  let val (cts, env) = Thm.read_def_cterms (sg, types, sorts) used freeze sTs
    1.50 +  in (map Thm.term_of cts, env) end;
    1.51 +
    1.52 +fun read_def_termT freeze sg defs sT = apfst hd (read_def_termTs freeze sg defs [sT]);
    1.53 +
    1.54  
    1.55  fun read_term_sg sg (defs as (_, _, used)) s =
    1.56 -  read_def_termT sg defs (s, TVar ((variant used "'z", 0), logicS));
    1.57 +  #1 (read_def_termT true sg defs (s, TVar ((variant used "'z", 0), logicS)));
    1.58  
    1.59 -fun read_prop_sg sg defs s = read_def_termT sg defs (s, propT);
    1.60 +fun read_prop_sg sg defs s =
    1.61 +  #1 (read_def_termT true sg defs (s, propT));
    1.62  
    1.63  
    1.64  fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
    1.65 @@ -375,7 +381,7 @@
    1.66  
    1.67  (* read terms *)
    1.68  
    1.69 -fun gen_read read is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
    1.70 +fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
    1.71    let
    1.72      val sign = sign_of ctxt;
    1.73  
    1.74 @@ -389,13 +395,14 @@
    1.75      (transform_error (read sign (def_type, def_sort, used)) s
    1.76        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
    1.77        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
    1.78 -    |> intern_skolem ctxt true
    1.79 -    |> (if is_pat then I else norm_term ctxt)
    1.80 +    |> app (intern_skolem ctxt true)
    1.81 +    |> app (if is_pat then I else norm_term ctxt)
    1.82    end;
    1.83  
    1.84 -val read_term = gen_read read_term_sg false;
    1.85 -val read_prop = gen_read read_prop_sg false;
    1.86 -val read_pat = gen_read read_term_sg true;
    1.87 +val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;
    1.88 +val read_term = gen_read read_term_sg I false;
    1.89 +val read_prop = gen_read read_prop_sg I false;
    1.90 +val read_pat = gen_read read_term_sg I true;
    1.91  
    1.92  
    1.93  (* certify terms *)
    1.94 @@ -442,6 +449,10 @@
    1.95  fun declare_term t ctxt = declare (ctxt, t);
    1.96  fun declare_terms ts ctxt = foldl declare (ctxt, ts);
    1.97  
    1.98 +fun declare_thm thm ctxt =
    1.99 +  let val {prop, hyps, ...} = Thm.rep_thm thm
   1.100 +  in ctxt |> declare_terms (prop :: hyps) end;
   1.101 +
   1.102  fun prep_declare prep (ctxt, s) =
   1.103    let val t = prep ctxt s
   1.104    in (ctxt |> declare_term t, t) end;