1.1 --- a/src/Pure/Isar/isar_thy.ML Wed Jun 01 12:30:49 2005 +0200
1.2 +++ b/src/Pure/Isar/isar_thy.ML Wed Jun 01 12:30:50 2005 +0200
1.3 @@ -47,8 +47,6 @@
1.4 val using_facts_i: (thm * Proof.context attribute list) list list
1.5 -> ProofHistory.T -> ProofHistory.T
1.6 val chain: ProofHistory.T -> ProofHistory.T
1.7 - val instantiate_locale: (string * Attrib.src list) * string -> ProofHistory.T
1.8 - -> ProofHistory.T
1.9 val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
1.10 val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
1.11 val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
1.12 @@ -291,14 +289,6 @@
1.13 val chain = ProofHistory.apply Proof.chain;
1.14
1.15
1.16 -(* locale instantiation *)
1.17 -
1.18 -fun instantiate_locale ((name, atts), loc) =
1.19 - ProofHistory.apply (fn state =>
1.20 - Proof.instantiate_locale (loc,
1.21 - (name, map (Attrib.local_attribute (Proof.theory_of state)) atts)) state);
1.22 -
1.23 -
1.24 (* context *)
1.25
1.26 val fix = ProofHistory.apply o Proof.fix;
2.1 --- a/src/Pure/Isar/locale.ML Wed Jun 01 12:30:49 2005 +0200
2.2 +++ b/src/Pure/Isar/locale.ML Wed Jun 01 12:30:50 2005 +0200
2.3 @@ -18,11 +18,19 @@
2.4 Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
2.5 *)
2.6
2.7 +(* TODO:
2.8 +- beta-eta normalisation of interpretation parameters
2.9 +- no beta reduction of interpretation witnesses
2.10 +- mix of locales with and without open in activate_elems
2.11 +- dangling type frees in locales
2.12 +*)
2.13 +
2.14 signature LOCALE =
2.15 sig
2.16 type context
2.17 datatype ('typ, 'term, 'fact) elem =
2.18 Fixes of (string * 'typ option * mixfix option) list |
2.19 + Constrains of (string * 'typ) list |
2.20 Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
2.21 Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
2.22 Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
2.23 @@ -78,8 +86,6 @@
2.24 theory * context -> (theory * context) * (string * thm list) list
2.25
2.26 (* Locale interpretation *)
2.27 - val instantiate: string -> string * context attribute list
2.28 - -> thm list option -> context -> context
2.29 val prep_global_registration:
2.30 string * Attrib.src list -> expr -> string option list -> theory ->
2.31 theory * ((string * term list) * term list) list * (theory -> theory)
2.32 @@ -101,6 +107,7 @@
2.33
2.34 datatype ('typ, 'term, 'fact) elem =
2.35 Fixes of (string * 'typ option * mixfix option) list |
2.36 + Constrains of (string * 'typ) list |
2.37 Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
2.38 Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
2.39 Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
2.40 @@ -303,7 +310,7 @@
2.41 end;
2.42
2.43 (* add witness theorem to registration,
2.44 - only if instantiation is exact, otherwise excpetion Option raised *)
2.45 + only if instantiation is exact, otherwise exception Option raised *)
2.46 fun add_witness ts thm regs =
2.47 let
2.48 val t = termify ts;
2.49 @@ -563,6 +570,8 @@
2.50 fun map_elem {name, var, typ, term, fact, attrib} =
2.51 fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
2.52 let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
2.53 + | Constrains csts => Constrains (csts |> map (fn (x, T) =>
2.54 + let val (x', _) = var (x, SOME Syntax.NoSyn) in (x', typ T) end))
2.55 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
2.56 ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
2.57 (term t, (map term ps, map term qs))))))
2.58 @@ -970,6 +979,7 @@
2.59
2.60 fun activate_elem _ ((ctxt, axs), Fixes fixes) =
2.61 ((ctxt |> ProofContext.add_fixes fixes, axs), [])
2.62 + | activate_elem _ ((ctxt, axs), Constrains _) = ((ctxt, axs), [])
2.63 | activate_elem _ ((ctxt, axs), Assumes asms) =
2.64 let
2.65 val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms;
2.66 @@ -1066,14 +1076,14 @@
2.67
2.68 local
2.69
2.70 -fun prep_fixes prep_vars ctxt fixes =
2.71 - let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
2.72 - in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end;
2.73 +fun prep_parms prep_vars ctxt parms =
2.74 + let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms))
2.75 + in map (fn ([x'], T') => (x', T')) vars end;
2.76
2.77 in
2.78
2.79 -fun read_fixes x = prep_fixes ProofContext.read_vars x;
2.80 -fun cert_fixes x = prep_fixes ProofContext.cert_vars x;
2.81 +fun read_parms x = prep_parms ProofContext.read_vars x;
2.82 +fun cert_parms x = prep_parms ProofContext.cert_vars x;
2.83
2.84 end;
2.85
2.86 @@ -1124,17 +1134,27 @@
2.87 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
2.88 | declare_int_elem (ctxt, _) = (ctxt, []);
2.89
2.90 -fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
2.91 - (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
2.92 +fun declare_ext_elem prep_parms (ctxt, Fixes fixes) =
2.93 + let
2.94 + val parms = map (fn (x, T, _) => (x, T)) fixes;
2.95 + val parms' = prep_parms ctxt parms;
2.96 + val fixes' = map (fn ((x, T), (_, _, mx)) => (x, T, mx)) (parms' ~~ fixes);
2.97 + in (ctxt |> ProofContext.add_fixes fixes', []) end
2.98 + | declare_ext_elem prep_parms (ctxt, Constrains csts) =
2.99 + let
2.100 + val parms = map (fn (x, T) => (x, SOME T)) csts;
2.101 + val parms' = prep_parms ctxt parms;
2.102 + val ts = map (fn (x, SOME T) => Free (x, T)) parms';
2.103 + in (Library.fold ProofContext.declare_term ts ctxt, []) end
2.104 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
2.105 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
2.106 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
2.107
2.108 -fun declare_elems prep_fixes (ctxt, (((name, ps), _), elems)) =
2.109 +fun declare_elems prep_parms (ctxt, (((name, ps), _), elems)) =
2.110 let val (ctxt', propps) =
2.111 (case elems of
2.112 Int es => foldl_map declare_int_elem (ctxt, es)
2.113 - | Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
2.114 + | Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
2.115 handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
2.116 in (ctxt', propps) end;
2.117
2.118 @@ -1142,7 +1162,7 @@
2.119
2.120 (* CB: only called by prep_elemss. *)
2.121
2.122 -fun declare_elemss prep_fixes fixed_params raw_elemss ctxt =
2.123 +fun declare_elemss prep_parms fixed_params raw_elemss ctxt =
2.124 let
2.125 (* CB: fix of type bug of goal in target with context elements.
2.126 Parameters new in context elements must receive types that are
2.127 @@ -1156,7 +1176,7 @@
2.128 val (_, raw_elemss') =
2.129 foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
2.130 (int_elemss, raw_elemss);
2.131 - in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end;
2.132 + in foldl_map (declare_elems prep_parms) (ctxt, raw_elemss') end;
2.133
2.134 end;
2.135
2.136 @@ -1198,6 +1218,7 @@
2.137 (* CB: for finish_elems (Int and Ext) *)
2.138
2.139 fun eval_text _ _ _ (text, Fixes _) = text
2.140 + | eval_text _ _ _ (text, Constrains _) = text
2.141 | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
2.142 let
2.143 val ts = List.concat (map (map #1 o #2) asms);
2.144 @@ -1235,6 +1256,8 @@
2.145
2.146 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
2.147 (x, assoc_string (parms, x), mx)) fixes)
2.148 + | finish_ext_elem parms _ (Constrains csts, _) =
2.149 + Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts)
2.150 | finish_ext_elem _ close (Assumes asms, propp) =
2.151 close (Assumes (map #1 asms ~~ propp))
2.152 | finish_ext_elem _ close (Defines defs, propp) =
2.153 @@ -1270,7 +1293,7 @@
2.154
2.155 (* CB: type inference and consistency checks for locales *)
2.156
2.157 -fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
2.158 +fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
2.159 let
2.160 (* CB: contexts computed in the course of this function are discarded.
2.161 They are used for type inference and consistency checks only. *)
2.162 @@ -1278,7 +1301,7 @@
2.163 empty list if there is no target. *)
2.164 (* CB: raw_elemss are list of pairs consisting of identifiers and
2.165 context elements, the latter marked as internal or external. *)
2.166 - val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
2.167 + val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context;
2.168 (* CB: raw_ctxt is context with additional fixed variables derived from
2.169 the fixes elements in raw_elemss,
2.170 raw_proppss contains assumptions and definitions from the
2.171 @@ -1311,8 +1334,8 @@
2.172 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
2.173
2.174 (* CB: extract information from assumes and defines elements
2.175 - (fixes and notes in raw_elemss don't have an effect on text and elemss),
2.176 - compute final form of context elements. *)
2.177 + (fixes, constrains and notes in raw_elemss don't have an effect on
2.178 + text and elemss), compute final form of context elements. *)
2.179 val (text, elemss) = finish_elemss ctxt parms do_close
2.180 (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
2.181 (* CB: text has the following structure:
2.182 @@ -1330,7 +1353,7 @@
2.183 defs: theorems representing the substitutions from defines elements
2.184 (thms are normalised wrt. env).
2.185 elemss is an updated version of raw_elemss:
2.186 - - type info added to Fixes
2.187 + - type info added to Fixes and modified in Constrains
2.188 - axiom and definition statement replaced by corresponding one
2.189 from proppss in Assumes and Defines
2.190 - Facts unchanged
2.191 @@ -1339,8 +1362,8 @@
2.192
2.193 in
2.194
2.195 -fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x;
2.196 -fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x;
2.197 +fun read_elemss x = prep_elemss read_parms ProofContext.read_propp_schematic x;
2.198 +fun cert_elemss x = prep_elemss cert_parms ProofContext.cert_propp_schematic x;
2.199
2.200 end;
2.201
2.202 @@ -1442,182 +1465,6 @@
2.203 end;
2.204
2.205
2.206 -(** CB: experimental instantiation mechanism **)
2.207 -
2.208 -fun instantiate loc_name (prfx, attribs) raw_inst ctxt =
2.209 - let
2.210 - val thy = ProofContext.theory_of ctxt;
2.211 - val sign = Theory.sign_of thy;
2.212 - val tsig = Sign.tsig_of sign;
2.213 - val cert = cterm_of sign;
2.214 -
2.215 - (** process the locale **)
2.216 -
2.217 - val {predicate = (_, axioms), params = (ps, _), ...} =
2.218 - the_locale thy (intern sign loc_name);
2.219 - val fixed_params = param_types (map #1 ps);
2.220 - val init = ProofContext.init thy;
2.221 - val (_, raw_elemss) = flatten (init, intern_expr sign)
2.222 - (([], Symtab.empty), Expr (Locale loc_name));
2.223 - val ((parms, all_elemss, concl),
2.224 - (spec as (_, (ints, _)), (xs, env, defs))) =
2.225 - read_elemss false (* do_close *) init
2.226 - fixed_params (* could also put [] here??? *) raw_elemss
2.227 - [] (* concl *);
2.228 -
2.229 - (** analyse the instantiation theorem inst **)
2.230 -
2.231 - val inst = case raw_inst of
2.232 - NONE => if null ints
2.233 - then NONE
2.234 - else error "Locale has assumptions but no chained fact was found"
2.235 - | SOME [] => if null ints
2.236 - then NONE
2.237 - else error "Locale has assumptions but no chained fact was found"
2.238 - | SOME [thm] => if null ints
2.239 - then (warning "Locale has no assumptions: fact ignored"; NONE)
2.240 - else SOME thm
2.241 - | SOME _ => error "Multiple facts are not allowed";
2.242 -
2.243 - val args = case inst of
2.244 - NONE => []
2.245 - | SOME thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
2.246 - |> Term.strip_comb
2.247 - |>> (fn t as (Const (s, _)) => if (intern sign loc_name = s)
2.248 - then t
2.249 - else error ("Constant " ^ quote loc_name ^
2.250 - " expected but constant " ^ quote s ^ " was found")
2.251 - | t => error ("Constant " ^ quote loc_name ^ " expected \
2.252 - \but term " ^ quote (Sign.string_of_term sign t) ^
2.253 - " was found"))
2.254 - |> snd;
2.255 - val cargs = map cert args;
2.256 -
2.257 - (* process parameters: match their types with those of arguments *)
2.258 -
2.259 - val def_names = map (fn (Free (s, _), _) => s) env;
2.260 - val (defined, assumed) = List.partition
2.261 - (fn (s, _) => s mem def_names) fixed_params;
2.262 - val cassumed = map (cert o Free) assumed;
2.263 - val cdefined = map (cert o Free) defined;
2.264 -
2.265 - val param_types = map snd assumed;
2.266 - val v_param_types = map Type.varifyT param_types;
2.267 - val arg_types = map Term.fastype_of args;
2.268 - val Tenv = Library.foldl (Type.typ_match tsig)
2.269 - (Vartab.empty, v_param_types ~~ arg_types)
2.270 - handle UnequalLengths => error "Number of parameters does not \
2.271 - \match number of arguments of chained fact";
2.272 - (* get their sorts *)
2.273 - val tfrees = foldr Term.add_typ_tfrees [] param_types
2.274 - val Tenv' = map
2.275 - (fn ((a, i), (S, T)) => ((a, S), T))
2.276 - (Vartab.dest Tenv);
2.277 -
2.278 - (* process (internal) elements *)
2.279 -
2.280 - fun inst_type [] T = T
2.281 - | inst_type env T =
2.282 - Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
2.283 -
2.284 - fun inst_term [] t = t
2.285 - | inst_term env t = Term.map_term_types (inst_type env) t;
2.286 -
2.287 - (* parameters with argument types *)
2.288 -
2.289 - val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
2.290 - val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
2.291 - val cdefining = map (cert o inst_term Tenv' o snd) env;
2.292 -
2.293 - fun inst_thm _ [] th = th
2.294 - | inst_thm ctxt Tenv th =
2.295 - let
2.296 - val sign = ProofContext.sign_of ctxt;
2.297 - val cert = Thm.cterm_of sign;
2.298 - val certT = Thm.ctyp_of sign;
2.299 - val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
2.300 - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
2.301 - val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
2.302 - in
2.303 - if null Tenv' then th
2.304 - else
2.305 - th
2.306 - |> Drule.implies_intr_list (map cert hyps)
2.307 - |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
2.308 - |> (fn (th', al) => th' |>
2.309 - Thm.instantiate ((map (fn ((a, _), T) =>
2.310 - (certT (TVar (valOf (assoc (al, a)))), certT T)) Tenv'), []))
2.311 - |> (fn th'' => Drule.implies_elim_list th''
2.312 - (map (Thm.assume o cert o inst_term Tenv') hyps))
2.313 - end;
2.314 -
2.315 - val inst_type' = inst_type Tenv';
2.316 -
2.317 - val inst_term' = Term.subst_atomic
2.318 - (map (pairself term_of) ((cparams' @ cdefined') ~~ (cargs @ cdefining)))
2.319 - o inst_term Tenv';
2.320 -
2.321 - fun inst_thm' thm =
2.322 - let
2.323 - (* not all axs are normally applicable *)
2.324 - val hyps = #hyps (rep_thm thm);
2.325 - val ass = map (fn ax => (prop_of ax, ax)) axioms;
2.326 - val axs' = Library.foldl (fn (axs, hyp) =>
2.327 - (case gen_assoc (op aconv) (ass, hyp) of NONE => axs
2.328 - | SOME ax => axs @ [ax])) ([], hyps);
2.329 - val thm' = Drule.satisfy_hyps axs' thm;
2.330 - (* instantiate types *)
2.331 - val thm'' = inst_thm ctxt Tenv' thm';
2.332 - (* substitute arguments and discharge hypotheses *)
2.333 - val thm''' = case inst of
2.334 - NONE => thm''
2.335 - | SOME inst_thm => let
2.336 - val hyps = #hyps (rep_thm thm'');
2.337 - val th = thm'' |> implies_intr_hyps
2.338 - |> forall_intr_list (cparams' @ cdefined')
2.339 - |> forall_elim_list (cargs @ cdefining)
2.340 - (* th has premises of the form either inst_thm or x==x *)
2.341 - fun mk hyp = if Logic.is_equals hyp
2.342 - then hyp |> Logic.dest_equals |> snd |> cert
2.343 - |> reflexive
2.344 - else inst_thm
2.345 - in implies_elim_list th (map mk hyps)
2.346 - end;
2.347 - in thm''' end
2.348 - handle THM (msg, n, thms) => error ("Exception THM " ^
2.349 - string_of_int n ^ " raised\n" ^
2.350 - "Note: instantiate does not support old-style locales \
2.351 - \declared with (open)\n" ^ msg ^ "\n" ^
2.352 - cat_lines (map string_of_thm thms));
2.353 -
2.354 - fun inst_elem (ctxt, (Ext _)) = ctxt
2.355 - | inst_elem (ctxt, (Int (Notes facts))) =
2.356 - (* instantiate fact *)
2.357 - let
2.358 - val facts = facts |> map_attrib_facts
2.359 - (Attrib.context_attribute_i ctxt o
2.360 - Args.map_values I inst_type' inst_term' inst_thm');
2.361 - val facts' =
2.362 - map (apsnd (map (apfst (map inst_thm')))) facts
2.363 - (* rename fact *)
2.364 - val facts'' = map (apfst (apfst (NameSpace.qualified prfx))) facts'
2.365 - (* add attributes *)
2.366 - val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
2.367 - in fst (ProofContext.note_thmss_i facts''' ctxt)
2.368 - end
2.369 - | inst_elem (ctxt, (Int _)) = ctxt;
2.370 -
2.371 - (* FIXME fold o fold *)
2.372 - fun inst_elems (ctxt, (id, elems)) = Library.foldl inst_elem (ctxt, elems);
2.373 -
2.374 - fun inst_elemss ctxt elemss = Library.foldl inst_elems (ctxt, elemss);
2.375 -
2.376 - (* main part *)
2.377 -
2.378 - val ctxt' = ProofContext.qualified_names ctxt;
2.379 - in ProofContext.restore_naming ctxt (inst_elemss ctxt' all_elemss) end;
2.380 -
2.381 -
2.382 (** define locales **)
2.383
2.384 (* print locale *)
2.385 @@ -1639,6 +1486,7 @@
2.386 fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
2.387 prt_typ T :: Pretty.brk 1 :: prt_syn syn)
2.388 | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
2.389 + fun prt_cst (x, T) = Pretty.block [Pretty.str (x ^ " ::"), prt_typ T];
2.390
2.391 fun prt_name name = Pretty.str (ProofContext.extern ctxt name);
2.392 fun prt_name_atts (name, atts) =
2.393 @@ -1659,6 +1507,7 @@
2.394 fun items _ [] = []
2.395 | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs;
2.396 fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
2.397 + | prt_elem (Constrains csts) = items "constrains" (map prt_cst csts)
2.398 | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
2.399 | prt_elem (Defines defs) = items "defines" (map prt_def defs)
2.400 | prt_elem (Notes facts) = items "notes" (map prt_note facts);
2.401 @@ -2016,21 +1865,12 @@
2.402
2.403 (* extract proof obligations (assms and defs) from elements *)
2.404
2.405 -(* check if defining equation has become t == t, these are dropped
2.406 - in extract_asms_elem, as they lead to trivial proof obligations *)
2.407 -(* currently disabled *)
2.408 -fun check_def (_, (def, _)) = SOME def;
2.409 -(*
2.410 -fun check_def (_, (def, _)) =
2.411 - if def |> Logic.dest_equals |> op aconv
2.412 - then NONE else SOME def;
2.413 -*)
2.414 -
2.415 fun extract_asms_elem (ts, Fixes _) = ts
2.416 + | extract_asms_elem (ts, Constrains _) = ts
2.417 | extract_asms_elem (ts, Assumes asms) =
2.418 ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
2.419 | extract_asms_elem (ts, Defines defs) =
2.420 - ts @ List.mapPartial check_def defs
2.421 + ts @ map (fn (_, (def, _)) => def) defs
2.422 | extract_asms_elem (ts, Notes _) = ts;
2.423
2.424 fun extract_asms_elems (id, elems) =
2.425 @@ -2042,6 +1882,7 @@
2.426 (* activate instantiated facts in theory or context *)
2.427
2.428 fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
2.429 + | activate_facts_elem _ _ _ _ (thy_ctxt, Constrains _) = thy_ctxt
2.430 | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
2.431 | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
2.432 | activate_facts_elem note_thmss attrib
3.1 --- a/src/Pure/Isar/outer_parse.ML Wed Jun 01 12:30:49 2005 +0200
3.2 +++ b/src/Pure/Isar/outer_parse.ML Wed Jun 01 12:30:50 2005 +0200
3.3 @@ -314,11 +314,14 @@
3.4 local
3.5
3.6 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME;
3.7 -val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
3.8 +val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||
3.9 + $$$ "defines" || $$$ "notes" || $$$ "includes";
3.10
3.11 val loc_element =
3.12 $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
3.13 >> triple1)) >> Locale.Fixes ||
3.14 + $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
3.15 + >> Locale.Constrains ||
3.16 $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
3.17 >> Locale.Assumes ||
3.18 $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
4.1 --- a/src/Pure/Isar/proof.ML Wed Jun 01 12:30:49 2005 +0200
4.2 +++ b/src/Pure/Isar/proof.ML Wed Jun 01 12:30:50 2005 +0200
4.3 @@ -68,8 +68,6 @@
4.4 (thm list * context attribute list) list) list -> state -> state
4.5 val using_thmss: ((thmref * context attribute list) list) list -> state -> state
4.6 val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
4.7 - val instantiate_locale: string * (string * context attribute list) -> state
4.8 - -> state
4.9 val fix: (string list * string option) list -> state -> state
4.10 val fix_i: (string list * typ option) list -> state -> state
4.11 val assm: ProofContext.exporter
4.12 @@ -635,20 +633,6 @@
4.13 end;
4.14
4.15
4.16 -(* locale instantiation *)
4.17 -
4.18 -fun instantiate_locale (loc_name, prfx_attribs) state =
4.19 - let
4.20 - val facts = if is_chain state then get_facts state else NONE;
4.21 - in
4.22 - state
4.23 - |> assert_forward_or_chain
4.24 - |> enter_forward
4.25 - |> reset_facts
4.26 - |> map_context (Locale.instantiate loc_name prfx_attribs facts)
4.27 - end;
4.28 -
4.29 -
4.30 (* fix *)
4.31
4.32 fun gen_fix f xs state =