# HG changeset patch # User wenzelm # Date 1129751562 -7200 # Node ID e8d7d463436dbee3c2e357b6a374dbf622eaa11a # Parent c567e5f885bfc93975e8fcaa7e2b1e5f48c6f45b removed obsolete old-locales; moved thm(s) retrieval functions back to pure_thy.ML; removed atomic_goal(w) interface; removed user-level (top_sg, prin, printyp, pprint_term/typ, which tend to cause some confusion about the implicit goal (!) context being used here; diff -r c567e5f885bf -r e8d7d463436d src/Pure/goals.ML --- 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;