--- a/src/Pure/goals.ML Wed Oct 19 21:52:41 2005 +0200
+++ b/src/Pure/goals.ML Wed Oct 19 21:52:42 2005 +0200
@@ -1,26 +1,18 @@
(* Title: Pure/goals.ML
ID: $Id$
- Author: Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Old-style locales and goal stack package. The goal stack initially
-holds a dummy proof, and can never become empty. Each goal stack
-consists of a list of levels. The undo list is a list of goal stacks.
-Finally, there may be a stack of pending proofs. Additional support
-for locales.
+Old-style goal stack package. The goal stack initially holds a dummy
+proof, and can never become empty. Each goal stack consists of a list
+of levels. The undo list is a list of goal stacks. Finally, there
+may be a stack of pending proofs.
*)
-signature BASIC_GOALS =
+signature GOALS =
sig
- val Open_locale: xstring -> unit
- val Close_locale: xstring -> unit
- val Print_scope: unit -> unit
- val thm: xstring -> thm
- val thms: xstring -> thm list
type proof
val reset_goals : unit -> unit
- val atomic_goal : theory -> string -> thm list
- val atomic_goalw : theory -> thm list -> string -> thm list
val Goal : string -> thm list
val Goalw : thm list -> string -> thm list
val ba : int -> unit
@@ -37,9 +29,6 @@
val byev : tactic list -> unit
val chop : unit -> unit
val choplev : int -> unit
- val export_thy : theory -> thm -> thm
- val export : thm -> thm
- val Export : thm -> thm
val fa : unit -> unit
val fd : thm -> unit
val fds : thm list -> unit
@@ -60,10 +49,6 @@
val prlev : int -> unit
val prlim : int -> unit
val premises : unit -> thm list
- val prin : term -> unit
- val printyp : typ -> unit
- val pprint_term : term -> pprint_args -> unit
- val pprint_typ : typ -> pprint_args -> unit
val print_exn : exn -> 'a
val print_sign_exn : theory -> exn -> 'a
val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
@@ -74,7 +59,6 @@
-> (thm list -> tactic list) -> thm
val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
val push_proof : unit -> unit
- val read : string -> term
val ren : string -> int -> unit
val restore_proof : proof -> thm list
val result : unit -> thm
@@ -98,518 +82,9 @@
val thms_containing : xstring list -> (string * thm) list
end;
-signature GOALS =
-sig
- include BASIC_GOALS
- type locale
- val print_locales: theory -> unit
- val get_thm: theory -> xstring -> thm
- val get_thms: theory -> xstring -> thm list
- val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
- (string * string) list -> (string * string) list -> theory -> theory
- val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
- (string * term) list -> (string * term) list -> theory -> theory
- val open_locale: xstring -> theory -> theory
- val close_locale: xstring -> theory -> theory
- val print_scope: theory -> unit
- val read_cterm: theory -> string * typ -> cterm
-end;
-
structure Goals: GOALS =
struct
-(*** Old-style locales ***)
-
-(* Locales. The theory section 'locale' declarings constants,
-assumptions and definitions that have local scope. Typical form is
-
- locale Locale_name =
- fixes (*variables that are fixed in the locale's scope*)
- v :: T
- assumes (*meta-hypothesis that hold in the locale*)
- Asm_name "meta-formula"
- defines (*local definitions of fixed variables in terms of others*)
- v_def "v x == ...x..."
-*)
-
-(** type locale **)
-
-type locale =
- {ancestor: string option,
- consts: (string * typ) list,
- nosyn: string list,
- rules: (string * term) list,
- defs: (string * term) list,
- thms: (string * thm) list,
- defaults: (string * sort) list * (string * typ) list * string list};
-
-fun make_locale ancestor consts nosyn rules defs thms defaults =
- {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
- defs = defs, thms = thms, defaults = defaults}: locale;
-
-fun pretty_locale thy (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
- let
- val prt_typ = Pretty.quote o Sign.pretty_typ thy;
- val prt_term = Pretty.quote o Sign.pretty_term thy;
-
- fun pretty_const (c, T) = Pretty.block
- [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
-
- fun pretty_axiom (a, t) = Pretty.block
- [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
-
- val anc = case ancestor of
- NONE => ""
- | SOME(loc) => ((Sign.base_name loc) ^ " +")
- in
- Pretty.big_list (name ^ " = " ^ anc)
- [Pretty.big_list "consts:" (map pretty_const consts),
- Pretty.big_list "rules:" (map pretty_axiom rules),
- Pretty.big_list "defs:" (map pretty_axiom defs)]
- end;
-
-
-
-(** theory data **)
-
-(* data kind 'Pure/old-locales' *)
-
-type locale_data =
- {space: NameSpace.T,
- locales: locale Symtab.table,
- scope: (string * locale) list ref};
-
-fun make_locale_data space locales scope =
- {space = space, locales = locales, scope = scope}: locale_data;
-
-structure LocalesData = TheoryDataFun
-(struct
- val name = "Pure/old-locales";
- type T = locale_data;
-
- val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
- fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
- fun extend {space, locales, scope = _} = make_locale_data space locales (ref []);
- fun merge _ ({space = space1, locales = locales1, scope = _},
- {space = space2, locales = locales2, scope = _}) =
- make_locale_data (NameSpace.merge (space1, space2))
- (Symtab.merge (K true) (locales1, locales2))
- (ref []);
-
- fun print thy {space, locales, scope} =
- let
- val locs = NameSpace.extern_table (space, locales);
- val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
- in
- [Pretty.big_list "locales:" (map (pretty_locale thy) locs),
- Pretty.strs ("current scope:" :: scope_names)]
- |> Pretty.chunks |> Pretty.writeln
- end;
-end);
-
-val _ = Context.add_setup [LocalesData.init];
-val print_locales = LocalesData.print;
-
-
-(* access locales *)
-
-val get_locale = Symtab.lookup o #locales o LocalesData.get;
-
-fun put_locale (name, locale) thy =
- let
- val {space, locales, scope} = LocalesData.get thy;
- val space' = Sign.declare_name thy name space;
- val locales' = Symtab.update (name, locale) locales;
- in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
-
-fun lookup_locale thy xname =
- let
- val {space, locales, ...} = LocalesData.get thy;
- val name = NameSpace.intern space xname;
- in Option.map (pair name) (get_locale thy name) end;
-
-
-(* access scope *)
-
-fun get_scope thy =
- if eq_thy (thy, ProtoPure.thy) then []
- else ! (#scope (LocalesData.get thy));
-
-fun change_scope f thy =
- let val {scope, ...} = LocalesData.get thy
- in scope := f (! scope) end;
-
-
-
-(** scope operations **)
-
-(* change scope *)
-
-fun the_locale thy xname =
- (case lookup_locale thy xname of
- SOME loc => loc
- | NONE => error ("Unknown locale " ^ quote xname));
-
-fun open_locale xname thy =
- let val loc = the_locale thy xname;
- val anc = #ancestor(#2(loc));
- val cur_sc = get_scope thy;
- fun opn lc th = (change_scope (cons lc) th; th)
- in case anc of
- NONE => opn loc thy
- | SOME(loc') =>
- if loc' mem (map fst cur_sc)
- then opn loc thy
- else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
- quote xname);
- opn loc (open_locale (Sign.base_name loc') thy))
- end;
-
-fun pop_locale [] = error "Currently no open locales"
- | pop_locale (_ :: locs) = locs;
-
-fun close_locale name thy =
- let val lname = (case get_scope thy of (ln,_)::_ => ln
- | _ => error "No locales are open!")
- val ok = name = Sign.base_name lname
- in if ok then (change_scope pop_locale thy; thy)
- else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
- end;
-
-fun print_scope thy =
-Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
-
-(*implicit context versions*)
-fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
-fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
-fun Print_scope () = (print_scope (Context.the_context ()); ());
-
-
-(** functions for goals.ML **)
-
-(* in_locale: check if hyps (: term list) of a proof are contained in the
- (current) scope. This function is needed in prepare_proof. *)
-
-fun in_locale hyps thy =
- let val cur_sc = get_scope thy;
- val rule_lists = map (#rules o snd) cur_sc;
- val def_lists = map (#defs o snd) cur_sc;
- val rules = map snd (foldr (op union) [] rule_lists);
- val defs = map snd (foldr (op union) [] def_lists);
- val defnrules = rules @ defs;
- in
- hyps subset defnrules
- end;
-
-
-(* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
-fun is_open_loc thy =
- let val cur_sc = get_scope thy
- in not(null(cur_sc)) end;
-
-
-(* get theorems *)
-
-fun get_thm_locale name ((_, {thms, ...}: locale)) = AList.lookup (op =) thms name;
-
-fun get_thmx f get thy name =
- (case get_first (get_thm_locale name) (get_scope thy) of
- SOME thm => f thm
- | NONE => get thy (Name name));
-
-val get_thm = get_thmx I PureThy.get_thm;
-val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
-
-fun thm name = get_thm (Context.the_context ()) name;
-fun thms name = get_thms (Context.the_context ()) name;
-
-
-(* get the defaults of a locale, for extension *)
-
-fun get_defaults thy name =
- let val (lname, loc) = the_locale thy name;
- in #defaults(loc)
- end;
-
-
-(** define locales **)
-
-(* prepare types *)
-
-fun read_typ thy (envT, s) =
- let
- fun def_sort (x, ~1) = AList.lookup (op =) envT x
- | def_sort _ = NONE;
- val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
- in (Term.add_typ_tfrees (T, envT), T) end;
-
-fun cert_typ thy (envT, raw_T) =
- let val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg
- in (Term.add_typ_tfrees (T, envT), T) end;
-
-
-(* prepare props *)
-
-val add_frees = fold_aterms (fn Free v => (fn vs => v ins vs) | _ => I);
-
-fun enter_term t (envS, envT, used) =
- (Term.add_term_tfrees (t, envS), add_frees t envT, Term.add_term_tfree_names (t, used));
-
-fun read_axm thy ((envS, envT, used), (name, s)) =
- let
- fun def_sort (x, ~1) = AList.lookup (op =) envS x
- | def_sort _ = NONE;
- fun def_type (x, ~1) = AList.lookup (op =) envT x
- | def_type _ = NONE;
- val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
- in
- (enter_term t (envS, envT, used), t)
- end;
-
-
-fun cert_axm thy ((envS, envT, used), (name, raw_t)) =
- let val (_, t) = Theory.cert_axm thy (name, raw_t)
- in (enter_term t (envS, envT, used), t) end;
-
-
-(* read_cterm: read in a string as a certified term, and respect the bindings
- that already exist for subterms. If no locale is open, this function is equal to
- Thm.read_cterm *)
-
-fun read_cterm thy =
- let val cur_sc = get_scope thy;
- val defaults = map (#defaults o snd) cur_sc;
- val envS = List.concat (map #1 defaults);
- val envT = List.concat (map #2 defaults);
- val used = List.concat (map #3 defaults);
- fun def_sort (x, ~1) = AList.lookup (op =) envS x
- | def_sort _ = NONE;
- fun def_type (x, ~1) = AList.lookup (op =) envT x
- | def_type _ = NONE;
- in (if (is_open_loc thy)
- then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
- else Thm.read_cterm thy)
- end;
-
-(* basic functions needed for definitions and display *)
-(* collect all locale constants of a scope, i.e. a list of locales *)
-fun collect_consts thy =
- let val cur_sc = get_scope thy;
- val locale_list = map snd cur_sc;
- val const_list = List.concat (map #consts locale_list)
- in map fst const_list end;
-
-(* filter out the Free's in a term *)
-fun list_frees t =
- case t of Const(c,T) => []
- | Var(v,T) => []
- | Free(v,T)=> [Free(v,T)]
- | Bound x => []
- | Abs(a,T,u) => list_frees u
- | t1 $ t2 => (list_frees t1) @ (list_frees t2);
-
-(* filter out all Free's in a term that are not contained
- in a list of strings. Used to prepare definitions. The list of strings
- will be the consts of the scope. We filter out the "free" Free's to be
- able to bind them *)
-fun difflist term clist =
- let val flist = list_frees term;
- fun builddiff [] sl = []
- | builddiff (t :: tl) sl =
- let val Free(v,T) = t
- in
- if (v mem sl)
- then builddiff tl sl
- else t :: (builddiff tl sl)
- end;
- in distinct(builddiff flist clist) end;
-
-(* Bind a term with !! over a list of "free" Free's.
- To enable definitions like x + y == .... (without quantifier).
- Complications, because x and y have to be removed from defaults *)
-fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
- let val diffl = rev(difflist term clist);
- fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
- | abs_o (_ , _) = error ("Can't be: abs_over_free");
- val diffl' = map (fn (Free (s, T)) => s) diffl;
- val defaults' = (#1 defaults, List.filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
- in (defaults', (s, Library.foldl abs_o (term, diffl))) end;
-
-(* assume a definition, i.e assume the cterm of a definiton term and then eliminate
- the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
-fun prep_hyps clist thy = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of thy);
-
-
-(* concrete syntax *)
-
-fun mark_syn c = "\\<^locale>" ^ c;
-
-fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
-
-
-(* add_locale *)
-
-fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
- let
- val name = Sign.full_name thy bname;
-
- val (envSb, old_loc_consts, _) =
- case bancestor of
- SOME(loc) => (get_defaults thy loc)
- | NONE => ([],[],[]);
-
- val old_nosyn = case bancestor of
- SOME(loc) => #nosyn(#2(the_locale thy loc))
- | NONE => [];
-
- (* Get the full name of the ancestor *)
- val ancestor = case bancestor of
- SOME(loc) => SOME(#1(the_locale thy loc))
- | NONE => NONE;
-
- (* prepare locale consts *)
-
- fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
- let
- val c = Syntax.const_name raw_c raw_mx;
- val c_syn = mark_syn c;
- val mx = Syntax.fix_mixfix raw_c raw_mx;
- val (envS', T) = prep_typ thy (envS, raw_T) handle ERROR =>
- error ("The error(s) above occured in locale constant " ^ quote c);
- val trfun = if mx = Syntax.NoSyn then NONE else SOME (c_syn, mk_loc_tr c);
- in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
-
- val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
- val loc_consts = map #1 loc_consts_syn;
- val loc_consts = old_loc_consts @ loc_consts;
- val loc_syn = map #2 loc_consts_syn;
- val nosyn = old_nosyn @ (map (#1 o #1) (List.filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
- val loc_trfuns = List.mapPartial #3 loc_consts_syn;
-
-
- (* 1st stage: syntax_thy *)
-
- val syntax_thy =
- thy
- |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
- |> Theory.add_trfuns ([], loc_trfuns, [], []);
-
-
- (* prepare rules and defs *)
-
- fun prep_axiom (env, (a, raw_t)) =
- let
- val (env', t) = prep_term syntax_thy (env, (a, raw_t)) handle ERROR =>
- error ("The error(s) above occured in locale rule / definition " ^ quote a);
- in (env', (a, t)) end;
-
- val ((envS1, envT1, used1), loc_rules) =
- foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
- val (defaults, loc_defs) =
- foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
-
- val old_loc_consts = collect_consts syntax_thy;
- val new_loc_consts = (map #1 loc_consts);
- val all_loc_consts = old_loc_consts @ new_loc_consts;
-
- val (defaults, loc_defs_terms) =
- foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
- val loc_defs_thms =
- map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy)) loc_defs_terms;
- val (defaults, loc_thms_terms) =
- foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
- val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy))
- (loc_thms_terms)
- @ loc_defs_thms;
-
-
- (* error messages *)
-
- fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
-
- val err_dup_locale =
- if is_none (get_locale thy name) then []
- else ["Duplicate definition of locale " ^ quote name];
-
- (* check if definientes are locale constants
- (in the same locale, so no redefining!) *)
- val err_def_head =
- let fun peal_appl t =
- case t of
- t1 $ t2 => peal_appl t1
- | Free(t) => t
- | _ => locale_error ("Bad form of LHS in locale definition");
- fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
- | lhs _ = locale_error ("Definitions must use the == relation");
- val defs = map lhs loc_defs;
- val check = defs subset loc_consts
- in if check then []
- else ["defined item not declared fixed in locale " ^ quote name]
- end;
-
- (* check that variables on rhs of definitions are either fixed or on lhs *)
- val err_var_rhs =
- let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
- let val varl1 = difflist d1 all_loc_consts;
- val varl2 = difflist d2 all_loc_consts
- in t andalso (varl2 subset varl1)
- end
- | compare_var_sides (_,_) =
- locale_error ("Definitions must use the == relation")
- val check = Library.foldl compare_var_sides (true, loc_defs)
- in if check then []
- else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
- end;
-
- val errs = err_dup_locale @ err_def_head @ err_var_rhs;
- in
- if null errs then ()
- else error (cat_lines errs);
-
- syntax_thy
- |> put_locale (name,
- make_locale ancestor loc_consts nosyn loc_thms_terms
- loc_defs_terms loc_thms defaults)
- end;
-
-
-val add_locale = gen_add_locale read_typ read_axm;
-val add_locale_i = gen_add_locale cert_typ cert_axm;
-
-(** print functions **)
-(* idea: substitute all locale contants (Free's) that are syntactical by their
- "real" constant representation (i.e. \\<^locale>constname).
- - function const_ssubst does this substitution
- - function pretty_term:
- if locale is open then do this substitution & then call Sign.pretty_term
- else call Sign.pretty_term
-*)
-(* substitutes all Free variables s in t by Const's s *)
-fun const_ssubst t s =
- case t of
- Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
- | Const(c,T) => Const(c,T)
- | Var(v,T) => Var(v,T)
- | Bound x => Bound x
- | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
- | t1 $ t2 => const_ssubst t1 s $ const_ssubst t2 s;
-
-(* FIXME: improve: can be expressed with foldl *)
-fun const_ssubst_list [] t = t
- | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
-
-(* pretty_term *)
-fun pretty_term thy =
- if (is_open_loc thy) then
- let val locale_list = map snd(get_scope thy);
- val nosyn = List.concat (map #nosyn locale_list);
- val str_list = (collect_consts thy) \\ nosyn
- in Sign.pretty_term thy o (const_ssubst_list str_list)
- end
- else Sign.pretty_term thy;
-
-
-
(*** Goal package ***)
(*Each level of goal stack includes a proof state and alternative states,
@@ -664,53 +139,6 @@
val result_error_fn = ref result_error_default;
-(* alternative to standard: this function does not discharge the hypotheses
- first. Is used for locales, in the following function prepare_proof *)
-fun varify th =
- let val {maxidx,...} = rep_thm th
- in
- th |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
- |> Drule.strip_shyps_warning
- |> zero_var_indexes |> Thm.varifyT |> Thm.compress
- end;
-
-(** exporting a theorem out of a locale means turning all meta-hyps into assumptions
- and expand and cancel the locale definitions.
- export goes through all levels in case of nested locales, whereas
- export_thy just goes one up. **)
-
-fun get_top_scope_thms thy =
- let val sc = get_scope thy
- in if null sc then (warning "No locale in theory"; [])
- else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
- end;
-
-fun implies_intr_some_hyps thy A_set th =
- let
- val used_As = A_set inter #hyps(rep_thm(th));
- val ctl = map (cterm_of thy) used_As
- in Library.foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
- end;
-
-fun standard_some thy A_set th =
- let val {maxidx,...} = rep_thm th
- in
- th |> implies_intr_some_hyps thy A_set
- |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
- |> Drule.strip_shyps_warning
- |> zero_var_indexes |> Thm.varifyT |> Thm.compress
- end;
-
-fun export_thy thy th =
- let val A_set = get_top_scope_thms thy
- in
- standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th)))
- end;
-
-val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard;
-
-fun Export th = export_thy (the_context ()) th;
-
(*Common treatment of "goal" and "prove_goal":
Return assumptions, initial proof state, and function to make result.
@@ -738,20 +166,16 @@
val ath = implies_intr_list cAs state
val th = ath RS Drule.rev_triv_goal
val {hyps,prop,thy=thy',...} = rep_thm th
- val final_th = if (null(hyps)) then standard th else varify th
+ val final_th = standard th
in if not check then final_th
else if not (eq_thy(thy,thy')) then !result_error_fn state
("Theory of proof state has changed!" ^
thy_error (thy,thy'))
else if ngoals>0 then !result_error_fn state
(string_of_int ngoals ^ " unsolved goals!")
- else if (not (null hyps) andalso (not (in_locale hyps thy)))
- then !result_error_fn state
- ("Additional hypotheses:\n" ^
- cat_lines
- (map (Sign.string_of_term thy)
- (List.filter (fn x => (not (in_locale [x] thy)))
- hyps)))
+ else if not (null hyps) then !result_error_fn state
+ ("Additional hypotheses:\n" ^
+ cat_lines (map (Sign.string_of_term thy) hyps))
else if Pattern.matches thy
(Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
then final_th
@@ -884,6 +308,10 @@
handle GETHYPS hyps => hyps
end;
+(*Prints exceptions nicely at top level;
+ raises the exception in order to have a polymorphic type!*)
+fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e; raise e);
+
(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *)
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
@@ -929,18 +357,11 @@
("The error(s) above occurred for " ^ quote agoal);
val goalw = agoalw false;
-
-(*String version with no meta-rewrite-rules*)
-fun agoal atomic thy = agoalw atomic thy [];
-val goal = agoal false;
+fun goal thy = goalw thy [];
(*now the versions that wrap the goal up in `Goal' to make it atomic*)
-val atomic_goalw = agoalw true;
-val atomic_goal = agoal true;
-
-(*implicit context versions*)
-fun Goal s = atomic_goal (Context.the_context ()) s;
-fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s;
+fun Goalw thms s = agoalw true (Context.the_context ()) thms s;
+val Goal = Goalw [];
(*simple version with minimal amount of checking and postprocessing*)
fun simple_prove_goal_cterm G f =
@@ -1067,31 +488,10 @@
fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
-(** Reading and printing terms wrt the current theory **)
-
-fun top_sg() = Thm.theory_of_thm (topthm());
-
-fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
-
-(*Print a term under the current theory of the proof state*)
-fun prin t = writeln (Sign.string_of_term (top_sg()) t);
-
-fun printyp T = writeln (Sign.string_of_typ (top_sg()) T);
-
-fun pprint_term t = Sign.pprint_term (top_sg()) t;
-
-fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
-
-
-(*Prints exceptions nicely at top level;
- raises the exception in order to have a polymorphic type!*)
-fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e);
-
-
(** theorem database operations **)
-(* storing *)
+(* store *)
fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm);
fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms);
@@ -1110,14 +510,11 @@
fun no_qed () = ();
-(* retrieval *)
-
-fun theory_of_goal () = Thm.theory_of_thm (topthm ());
-val context_of_goal = ProofContext.init o theory_of_goal;
+(* retrieve *)
fun thms_containing raw_consts =
let
- val thy = theory_of_goal ();
+ val thy = Thm.theory_of_thm (topthm ());
val consts = map (Sign.intern_const thy) raw_consts;
in
(case List.filter (is_none o Sign.const_type thy) consts of
@@ -1128,5 +525,4 @@
end;
-structure BasicGoals: BASIC_GOALS = Goals;
-open BasicGoals;
+open Goals;