src/Pure/Isar/proof_context.ML
changeset 16458 4c6fd0c01d28
parent 16348 7504fe04170f
child 16501 fec0cf020bad
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type exporter
     1.5    exception CONTEXT of string * context
     1.6    val theory_of: context -> theory
     1.7 -  val sign_of: context -> Sign.sg
     1.8 +  val sign_of: context -> theory    (*obsolete*)
     1.9    val is_fixed: context -> string -> bool
    1.10    val is_known: context -> string -> bool
    1.11    val fixed_names_of: context -> string list
    1.12 @@ -198,7 +198,7 @@
    1.13    make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
    1.14  
    1.15  fun theory_of (Context {thy, ...}) = thy;
    1.16 -val sign_of = Theory.sign_of o theory_of;
    1.17 +val sign_of = theory_of;
    1.18  fun syntax_of (Context {syntax, ...}) = syntax;
    1.19  
    1.20  fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
    1.21 @@ -218,7 +218,7 @@
    1.22  
    1.23  (* errors *)
    1.24  
    1.25 -fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
    1.26 +fun of_theory thy = "\nof theory " ^ Context.str_of_thy thy;
    1.27  
    1.28  fun err_inconsistent kinds =
    1.29    error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
    1.30 @@ -240,20 +240,19 @@
    1.31  
    1.32  (* data kind 'Isar/proof_data' *)
    1.33  
    1.34 -structure ProofDataDataArgs =
    1.35 -struct
    1.36 +structure ProofDataData = TheoryDataFun
    1.37 +(struct
    1.38    val name = "Isar/proof_data";
    1.39    type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
    1.40  
    1.41    val empty = Symtab.empty;
    1.42    val copy = I;
    1.43 -  val prep_ext = I;
    1.44 -  fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    1.45 +  val extend = I;
    1.46 +  fun merge _ tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    1.47      handle Symtab.DUPS kinds => err_inconsistent kinds;
    1.48    fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
    1.49 -end;
    1.50 +end);
    1.51  
    1.52 -structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
    1.53  val _ = Context.add_setup [ProofDataData.init];
    1.54  val print_proof_data = ProofDataData.print;
    1.55  
    1.56 @@ -304,7 +303,7 @@
    1.57  
    1.58  fun init thy =
    1.59    let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
    1.60 -    make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
    1.61 +    make_context (thy, (Sign.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
    1.62        (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
    1.63        (Vartab.empty, Vartab.empty, [], Symtab.empty))
    1.64    end;
    1.65 @@ -364,7 +363,7 @@
    1.66  fun add_syntax decls =
    1.67    map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
    1.68      let
    1.69 -      val is_logtype = Sign.is_logtype (Theory.sign_of thy);
    1.70 +      val is_logtype = Sign.is_logtype thy;
    1.71        val structs' = structs @ List.mapPartial prep_struct decls;
    1.72        val mxs = List.mapPartial prep_mixfix decls;
    1.73        val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
    1.74 @@ -385,11 +384,11 @@
    1.75  
    1.76  (** pretty printing **)
    1.77  
    1.78 -fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) (context_tr' ctxt t);
    1.79 -fun pretty_typ ctxt T = Sign.pretty_typ (sign_of ctxt) T;
    1.80 -fun pretty_sort ctxt S = Sign.pretty_sort (sign_of ctxt) S;
    1.81 -fun pretty_classrel ctxt cs = Sign.pretty_classrel (sign_of ctxt) cs;
    1.82 -fun pretty_arity ctxt ar = Sign.pretty_arity (sign_of ctxt) ar;
    1.83 +fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (theory_of ctxt) (context_tr' ctxt t);
    1.84 +fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
    1.85 +fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
    1.86 +fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
    1.87 +fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;
    1.88  
    1.89  fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
    1.90    pretty_classrel ctxt, pretty_arity ctxt);
    1.91 @@ -433,11 +432,11 @@
    1.92  local
    1.93  
    1.94  fun read_typ_aux read ctxt s =
    1.95 -  transform_error (read (syn_of ctxt) (sign_of ctxt, def_sort ctxt)) s
    1.96 +  transform_error (read (syn_of ctxt) (theory_of ctxt, def_sort ctxt)) s
    1.97      handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
    1.98  
    1.99  fun cert_typ_aux cert ctxt raw_T =
   1.100 -  cert (sign_of ctxt) raw_T
   1.101 +  cert (theory_of ctxt) raw_T
   1.102      handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
   1.103  
   1.104  in
   1.105 @@ -505,29 +504,29 @@
   1.106  
   1.107  (* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
   1.108  
   1.109 -fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs =
   1.110 -  Sign.read_def_terms' pp (Sign.is_logtype sg) syn (sg, types, sorts) used freeze sTs;
   1.111 +fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
   1.112 +  Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
   1.113  
   1.114 -fun read_def_termT freeze pp syn sg defs sT =
   1.115 -  apfst hd (read_def_termTs freeze pp syn sg defs [sT]);
   1.116 +fun read_def_termT freeze pp syn thy defs sT =
   1.117 +  apfst hd (read_def_termTs freeze pp syn thy defs [sT]);
   1.118  
   1.119 -fun read_term_sg freeze pp syn sg defs s =
   1.120 -  #1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT));
   1.121 +fun read_term_thy freeze pp syn thy defs s =
   1.122 +  #1 (read_def_termT freeze pp syn thy defs (s, TypeInfer.logicT));
   1.123  
   1.124 -fun read_prop_sg freeze pp syn sg defs s =
   1.125 -  #1 (read_def_termT freeze pp syn sg defs (s, propT));
   1.126 +fun read_prop_thy freeze pp syn thy defs s =
   1.127 +  #1 (read_def_termT freeze pp syn thy defs (s, propT));
   1.128  
   1.129 -fun read_terms_sg freeze pp syn sg defs =
   1.130 -  #1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT);
   1.131 +fun read_terms_thy freeze pp syn thy defs =
   1.132 +  #1 o read_def_termTs freeze pp syn thy defs o map (rpair TypeInfer.logicT);
   1.133  
   1.134 -fun read_props_sg freeze pp syn sg defs =
   1.135 -  #1 o read_def_termTs freeze pp syn sg defs o map (rpair propT);
   1.136 +fun read_props_thy freeze pp syn thy defs =
   1.137 +  #1 o read_def_termTs freeze pp syn thy defs o map (rpair propT);
   1.138  
   1.139  
   1.140 -fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t);
   1.141 +fun cert_term_thy pp thy t = #1 (Sign.certify_term pp thy t);
   1.142  
   1.143 -fun cert_prop_sg pp sg tm =
   1.144 -  let val (t, T, _) = Sign.certify_term pp sg tm
   1.145 +fun cert_prop_thy pp thy tm =
   1.146 +  let val (t, T, _) = Sign.certify_term pp thy tm
   1.147    in if T = propT then t else raise TERM ("Term not of type prop", [t]) end;
   1.148  
   1.149  
   1.150 @@ -538,7 +537,7 @@
   1.151  
   1.152  fun unifyT ctxt (T, U) =
   1.153    let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
   1.154 -  in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   1.155 +  in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   1.156  
   1.157  fun norm_term (ctxt as Context {binds, ...}) schematic =
   1.158    let
   1.159 @@ -588,7 +587,7 @@
   1.160      val sorts = append_env (def_sort ctxt) more_sorts;
   1.161      val used = used_types ctxt @ more_used;
   1.162    in
   1.163 -    (transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s
   1.164 +    (transform_error (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used)) s
   1.165        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   1.166          | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   1.167      |> app (intern_skolem ctxt internal)
   1.168 @@ -609,13 +608,13 @@
   1.169  val read_prop_pats = read_term_pats propT;
   1.170  
   1.171  fun read_term_liberal ctxt =
   1.172 -  gen_read' (read_term_sg true) I false false ctxt (K true) (K NONE) (K NONE) [];
   1.173 +  gen_read' (read_term_thy true) I false false ctxt (K true) (K NONE) (K NONE) [];
   1.174  
   1.175 -val read_term              = gen_read (read_term_sg true) I false false;
   1.176 -val read_prop              = gen_read (read_prop_sg true) I false false;
   1.177 -val read_prop_schematic    = gen_read (read_prop_sg true) I false true;
   1.178 -val read_terms             = gen_read (read_terms_sg true) map false false;
   1.179 -fun read_props schematic   = gen_read (read_props_sg true) map false schematic;
   1.180 +val read_term              = gen_read (read_term_thy true) I false false;
   1.181 +val read_prop              = gen_read (read_prop_thy true) I false false;
   1.182 +val read_prop_schematic    = gen_read (read_prop_thy true) I false true;
   1.183 +val read_terms             = gen_read (read_terms_thy true) map false false;
   1.184 +fun read_props schematic   = gen_read (read_props_thy true) map false schematic;
   1.185  
   1.186  end;
   1.187  
   1.188 @@ -626,17 +625,17 @@
   1.189  
   1.190  fun gen_cert cert pattern schematic ctxt t = t
   1.191    |> (if pattern then I else norm_term ctxt schematic)
   1.192 -  |> (fn t' => cert (pp ctxt) (sign_of ctxt) t'
   1.193 +  |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
   1.194      handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
   1.195  
   1.196  in
   1.197  
   1.198 -val cert_term = gen_cert cert_term_sg false false;
   1.199 -val cert_prop = gen_cert cert_prop_sg false false;
   1.200 -val cert_props = map oo gen_cert cert_prop_sg false;
   1.201 +val cert_term = gen_cert cert_term_thy false false;
   1.202 +val cert_prop = gen_cert cert_prop_thy false false;
   1.203 +val cert_props = map oo gen_cert cert_prop_thy false;
   1.204  
   1.205 -fun cert_term_pats _ = map o gen_cert cert_term_sg true false;
   1.206 -val cert_prop_pats = map o gen_cert cert_prop_sg true false;
   1.207 +fun cert_term_pats _ = map o gen_cert cert_term_thy true false;
   1.208 +val cert_prop_pats = map o gen_cert cert_prop_thy true false;
   1.209  
   1.210  end;
   1.211  
   1.212 @@ -693,13 +692,13 @@
   1.213  
   1.214  fun read_tyname ctxt c =
   1.215    if c mem_string used_types ctxt then
   1.216 -    TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (sign_of ctxt)))
   1.217 -  else Sign.read_tyname (sign_of ctxt) c;
   1.218 +    TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (theory_of ctxt)))
   1.219 +  else Sign.read_tyname (theory_of ctxt) c;
   1.220  
   1.221  fun read_const ctxt c =
   1.222    (case lookup_skolem ctxt c of
   1.223      SOME c' => Free (c', dummyT)
   1.224 -  | NONE => Sign.read_const (sign_of ctxt) c);
   1.225 +  | NONE => Sign.read_const (theory_of ctxt) c);
   1.226  
   1.227  
   1.228  
   1.229 @@ -774,8 +773,8 @@
   1.230      |> Seq.map (Drule.implies_intr_list view)
   1.231      |> Seq.map (fn rule =>
   1.232        let
   1.233 -        val {sign, prop, ...} = Thm.rep_thm rule;
   1.234 -        val frees = map (Thm.cterm_of sign) (List.mapPartial (find_free prop) fixes);
   1.235 +        val {thy, prop, ...} = Thm.rep_thm rule;
   1.236 +        val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
   1.237          val tfrees = gen (Term.add_term_tfree_names (prop, []));
   1.238        in
   1.239          rule
   1.240 @@ -852,7 +851,7 @@
   1.241  
   1.242          val maxidx = fold (fn (t1, t2) => fn i =>
   1.243            Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
   1.244 -        val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx,
   1.245 +        val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
   1.246            map swap pairs);    (*prefer assignment of variables from patterns*)
   1.247          val env =
   1.248            (case Seq.pull envs of
   1.249 @@ -882,7 +881,7 @@
   1.250  val add_binds = fold (gen_bind read_term);
   1.251  val add_binds_i = fold (gen_bind cert_term);
   1.252  
   1.253 -fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (sign_of ctxt) ts));
   1.254 +fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
   1.255  val auto_bind_goal = auto_bind AutoBind.goal;
   1.256  val auto_bind_facts = auto_bind AutoBind.facts;
   1.257  
   1.258 @@ -977,12 +976,12 @@
   1.259  (*beware of proper order of evaluation!*)
   1.260  fun retrieve_thms f g (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
   1.261    let
   1.262 -    val sg_ref = Sign.self_ref (Theory.sign_of thy);
   1.263 +    val thy_ref = Theory.self_ref thy;
   1.264      val get_from_thy = f thy;
   1.265    in
   1.266      fn xnamei as (xname, _) =>
   1.267        (case Symtab.lookup (tab, NameSpace.intern space xname) of
   1.268 -        SOME ths => map (Thm.transfer_sg (Sign.deref sg_ref)) (PureThy.select_thm xnamei ths)
   1.269 +        SOME ths => map (Thm.transfer (Theory.deref thy_ref)) (PureThy.select_thm xnamei ths)
   1.270        | _ => get_from_thy xnamei) |> g xname
   1.271    end;
   1.272  
   1.273 @@ -1116,7 +1115,7 @@
   1.274  
   1.275  fun head_of_def cprop =
   1.276    #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
   1.277 -  |> Thm.cterm_of (Thm.sign_of_cterm cprop);
   1.278 +  |> Thm.cterm_of (Thm.theory_of_cterm cprop);
   1.279  
   1.280  fun export_def _ cprops thm =
   1.281    thm
   1.282 @@ -1132,7 +1131,7 @@
   1.283  
   1.284  fun add_assm (ctxt, ((name, attrs), props)) =
   1.285    let
   1.286 -    val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
   1.287 +    val cprops = map (Thm.cterm_of (theory_of ctxt)) props;
   1.288      val asms = map (Tactic.norm_hhf_rule o Thm.assume) cprops;
   1.289  
   1.290      val ths = map (fn th => ([th], [])) asms;
   1.291 @@ -1438,7 +1437,7 @@
   1.292  
   1.293      (*theory*)
   1.294      val pretty_thy = Pretty.block
   1.295 -      [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg (sign_of ctxt)];
   1.296 +      [Pretty.str "Theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
   1.297  
   1.298      (*defaults*)
   1.299      fun prt_atom prt prtT (x, X) = Pretty.block