src/Pure/goals.ML
author wenzelm
Mon Jun 21 16:41:06 2004 +0200 (2004-06-21)
changeset 14990 582b655da757
parent 14900 c66394c408f7
child 15457 1fbd4aba46e3
permissions -rw-r--r--
pretty_abbr;
     1 (*  Title: 	Pure/goals.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Old-style locales and goal stack package.  The goal stack initially
     7 holds a dummy proof, and can never become empty.  Each goal stack
     8 consists of a list of levels.  The undo list is a list of goal stacks.
     9 Finally, there may be a stack of pending proofs.  Additional support
    10 for locales.
    11 *)
    12 
    13 signature BASIC_GOALS =
    14 sig
    15   val Open_locale: xstring -> unit
    16   val Close_locale: xstring -> unit
    17   val Print_scope: unit -> unit
    18   val thm: xstring -> thm
    19   val thms: xstring -> thm list
    20   type proof
    21   val reset_goals       : unit -> unit
    22   val atomic_goal	: theory -> string -> thm list
    23   val atomic_goalw	: theory -> thm list -> string -> thm list
    24   val Goal		: string -> thm list
    25   val Goalw		: thm list -> string -> thm list
    26   val ba		: int -> unit
    27   val back		: unit -> unit
    28   val bd		: thm -> int -> unit
    29   val bds		: thm list -> int -> unit
    30   val be		: thm -> int -> unit
    31   val bes		: thm list -> int -> unit
    32   val br		: thm -> int -> unit
    33   val brs		: thm list -> int -> unit
    34   val bw		: thm -> unit
    35   val bws		: thm list -> unit
    36   val by		: tactic -> unit
    37   val byev		: tactic list -> unit
    38   val chop		: unit -> unit
    39   val choplev		: int -> unit
    40   val export_thy        : theory -> thm -> thm
    41   val export            : thm -> thm
    42   val Export		: thm -> thm
    43   val fa		: unit -> unit
    44   val fd		: thm -> unit
    45   val fds		: thm list -> unit
    46   val fe		: thm -> unit
    47   val fes		: thm list -> unit
    48   val filter_goal	: (term*term->bool) -> thm list -> int -> thm list
    49   val fr		: thm -> unit
    50   val frs		: thm list -> unit
    51   val getgoal		: int -> term
    52   val gethyps		: int -> thm list
    53   val goal		: theory -> string -> thm list
    54   val goalw		: theory -> thm list -> string -> thm list
    55   val goalw_cterm	: thm list -> cterm -> thm list
    56   val pop_proof		: unit -> thm list
    57   val pr		: unit -> unit
    58   val disable_pr        : unit -> unit
    59   val enable_pr         : unit -> unit
    60   val prlev		: int -> unit
    61   val prlim		: int -> unit
    62   val premises		: unit -> thm list
    63   val prin		: term -> unit
    64   val printyp		: typ -> unit
    65   val pprint_term	: term -> pprint_args -> unit
    66   val pprint_typ	: typ -> pprint_args -> unit
    67   val print_exn		: exn -> 'a
    68   val print_sign_exn	: Sign.sg -> exn -> 'a
    69   val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
    70   val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
    71   val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
    72   val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
    73   val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
    74     -> (thm list -> tactic list) -> thm
    75   val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
    76   val push_proof	: unit -> unit
    77   val read		: string -> term
    78   val ren		: string -> int -> unit
    79   val restore_proof	: proof -> thm list
    80   val result		: unit -> thm  
    81   val result_error_fn   : (thm -> string -> thm) ref
    82   val rotate_proof	: unit -> thm list
    83   val uresult		: unit -> thm  
    84   val save_proof	: unit -> proof
    85   val topthm		: unit -> thm
    86   val undo		: unit -> unit
    87   val bind_thm          : string * thm -> unit
    88   val bind_thms         : string * thm list -> unit
    89   val qed               : string -> unit
    90   val qed_goal          : string -> theory -> string -> (thm list -> tactic list) -> unit
    91   val qed_goalw         : string -> theory -> thm list -> string
    92     -> (thm list -> tactic list) -> unit
    93   val qed_spec_mp       : string -> unit
    94   val qed_goal_spec_mp  : string -> theory -> string -> (thm list -> tactic list) -> unit
    95   val qed_goalw_spec_mp : string -> theory -> thm list -> string
    96     -> (thm list -> tactic list) -> unit
    97   val no_qed: unit -> unit
    98   val thms_containing   : xstring list -> (string * thm) list
    99   val findI             : int -> (string * thm) list
   100   val findEs            : int -> (string * thm) list
   101   val findE             : int -> int -> (string * thm) list
   102 end;
   103 
   104 signature GOALS =
   105 sig
   106   include BASIC_GOALS
   107   type locale
   108   val print_locales: theory -> unit
   109   val get_thm: theory -> xstring -> thm
   110   val get_thms: theory -> xstring -> thm list
   111   val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
   112     (string * string) list -> (string * string) list -> theory -> theory
   113   val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
   114     (string * term) list -> (string * term) list -> theory -> theory
   115   val open_locale: xstring -> theory -> theory
   116   val close_locale: xstring -> theory -> theory
   117   val print_scope: theory -> unit
   118   val read_cterm: Sign.sg -> string * typ -> cterm
   119   val setup: (theory -> theory) list
   120 end;
   121 
   122 structure Goals: GOALS =
   123 struct
   124 
   125 (*** Old-style locales ***)
   126 
   127 (* Locales. The theory section 'locale' declarings constants,
   128 assumptions and definitions that have local scope.  Typical form is
   129 
   130     locale Locale_name =
   131       fixes   (*variables that are fixed in the locale's scope*)
   132 	v :: T
   133       assumes (*meta-hypothesis that hold in the locale*)
   134 	Asm_name "meta-formula"  
   135       defines (*local definitions of fixed variables in terms of others*)
   136 	v_def "v x == ...x..."
   137 *)
   138 
   139 (** type locale **)
   140 
   141 type locale =
   142  {ancestor: string option,
   143   consts: (string * typ) list,
   144   nosyn: string list,
   145   rules: (string * term) list,
   146   defs: (string * term) list,
   147   thms: (string * thm) list,
   148   defaults: (string * sort) list * (string * typ) list * string list};
   149 
   150 fun make_locale ancestor consts nosyn rules defs thms defaults =
   151   {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules, 
   152    defs = defs, thms = thms, defaults = defaults}: locale;
   153 
   154 fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
   155   let
   156     val prt_typ = Pretty.quote o Sign.pretty_typ sg;
   157     val prt_term = Pretty.quote o Sign.pretty_term sg;
   158 
   159     fun pretty_const (c, T) = Pretty.block
   160       [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
   161 
   162     fun pretty_axiom (a, t) = Pretty.block
   163       [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
   164 
   165     val anc = case ancestor of
   166                   None => ""
   167                 | Some(loc) => ((Sign.base_name loc) ^ " +")
   168   in
   169     Pretty.big_list (name ^ " = " ^ anc)
   170      [Pretty.big_list "consts:" (map pretty_const consts),
   171       Pretty.big_list "rules:" (map pretty_axiom rules),
   172       Pretty.big_list "defs:" (map pretty_axiom defs)]
   173   end;
   174 
   175 
   176 
   177 (** theory data **)
   178 
   179 (* data kind 'Pure/old-locales' *)
   180 
   181 type locale_data =
   182   {space: NameSpace.T,
   183     locales: locale Symtab.table,
   184     scope: (string * locale) list ref};
   185 
   186 fun make_locale_data space locales scope =
   187   {space = space, locales = locales, scope = scope}: locale_data;
   188 
   189 structure LocalesArgs =
   190 struct
   191   val name = "Pure/old-locales";
   192   type T = locale_data;
   193 
   194   val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
   195   fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
   196   fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   197   fun merge ({space = space1, locales = locales1, scope = _},
   198     {space = space2, locales = locales2, scope = _}) =
   199       make_locale_data (NameSpace.merge (space1, space2))
   200         (Symtab.merge (K true) (locales1, locales2))
   201         (ref []);
   202 
   203   fun print sg {space, locales, scope} =
   204     let
   205       fun extrn name =
   206         if ! long_names then name else NameSpace.extern space name;
   207       val locs = map (apfst extrn) (Symtab.dest locales);
   208       val scope_names = rev (map (extrn o fst) (! scope));
   209     in
   210       [Display.pretty_name_space ("locale name space", space),
   211         Pretty.big_list "locales:" (map (pretty_locale sg) locs),
   212         Pretty.strs ("current scope:" :: scope_names)]
   213       |> Pretty.chunks |> Pretty.writeln
   214     end;
   215 end;
   216 
   217 
   218 structure LocalesData = TheoryDataFun(LocalesArgs);
   219 val print_locales = LocalesData.print;
   220 
   221 
   222 (* access locales *)
   223 
   224 fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
   225 
   226 val get_locale = get_locale_sg o Theory.sign_of;
   227 
   228 fun put_locale (name, locale) thy =
   229   let
   230     val {space, locales, scope} = LocalesData.get thy;
   231     val space' = NameSpace.extend (space, [name]);
   232     val locales' = Symtab.update ((name, locale), locales);
   233   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
   234 
   235 fun lookup_locale thy xname =
   236   let
   237     val {space, locales, ...} = LocalesData.get thy;
   238     val name = NameSpace.intern space xname;
   239   in apsome (pair name) (get_locale thy name) end;
   240 
   241 
   242 (* access scope *)
   243 
   244 fun get_scope_sg sg =
   245   if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
   246   else ! (#scope (LocalesData.get_sg sg));
   247 
   248 val get_scope = get_scope_sg o Theory.sign_of;
   249 
   250 fun change_scope f thy =
   251   let val {scope, ...} = LocalesData.get thy
   252   in scope := f (! scope) end;
   253 
   254 
   255 
   256 (** scope operations **)
   257 
   258 (* change scope *)
   259 
   260 fun the_locale thy xname =
   261   (case lookup_locale thy xname of
   262     Some loc => loc
   263   | None => error ("Unknown locale " ^ quote xname));
   264 
   265 fun open_locale xname thy =
   266   let val loc = the_locale thy xname;
   267       val anc = #ancestor(#2(loc));
   268       val cur_sc = get_scope thy;
   269       fun opn lc th = (change_scope (cons lc) th; th)
   270   in case anc of
   271          None => opn loc thy
   272        | Some(loc') => 
   273            if loc' mem (map fst cur_sc) 
   274            then opn loc thy
   275            else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^ 
   276 			  quote xname);
   277                  opn loc (open_locale (Sign.base_name loc') thy))
   278   end;
   279 
   280 fun pop_locale [] = error "Currently no open locales"
   281   | pop_locale (_ :: locs) = locs;
   282 
   283 fun close_locale name thy = 
   284    let val lname = (case get_scope thy of (ln,_)::_ => ln
   285                                         | _ => error "No locales are open!")
   286        val ok = (name = Sign.base_name lname) handle _ => false
   287    in if ok then (change_scope pop_locale thy; thy)
   288       else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
   289    end;
   290 
   291 fun print_scope thy = 
   292 Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
   293 
   294 (*implicit context versions*)
   295 fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
   296 fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
   297 fun Print_scope () = (print_scope (Context.the_context ()); ());
   298 
   299 
   300 (** functions for goals.ML **)
   301 
   302 (* in_locale: check if hyps (: term list) of a proof are contained in the
   303    (current) scope. This function is needed in prepare_proof. It needs to
   304    refer to the signature, because theory is not available in prepare_proof. *)
   305 
   306 fun in_locale hyps sg =
   307     let val cur_sc = get_scope_sg sg;
   308         val rule_lists = map (#rules o snd) cur_sc;
   309         val def_lists = map (#defs o snd) cur_sc;
   310         val rules = map snd (foldr (op union) (rule_lists, []));
   311         val defs = map snd (foldr (op union) (def_lists, []));
   312         val defnrules = rules @ defs;
   313     in
   314         hyps subset defnrules
   315     end;
   316 
   317 
   318 (* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
   319 fun is_open_loc_sg sign =
   320     let val cur_sc = get_scope_sg sign
   321     in not(null(cur_sc)) end;
   322 
   323 val is_open_loc = is_open_loc_sg o Theory.sign_of;
   324 
   325 
   326 (* get theorems *)
   327 
   328 fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
   329 
   330 fun get_thmx f get thy name =
   331   (case get_first (get_thm_locale name) (get_scope thy) of
   332     Some thm => f thm
   333   | None => get thy name);
   334 
   335 val get_thm = get_thmx I PureThy.get_thm;
   336 val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
   337 
   338 fun thm name = get_thm (Context.the_context ()) name;
   339 fun thms name = get_thms (Context.the_context ()) name;
   340 
   341 
   342 (* get the defaults of a locale, for extension *)
   343 
   344 fun get_defaults thy name = 
   345   let val (lname, loc) = the_locale thy name;
   346   in #defaults(loc)
   347   end;
   348 
   349 
   350 (** define locales **)
   351 
   352 (* prepare types *)
   353 
   354 fun read_typ sg (envT, s) =
   355   let
   356     fun def_sort (x, ~1) = assoc (envT, x)
   357       | def_sort _ = None;
   358     val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
   359   in (Term.add_typ_tfrees (T, envT), T) end;
   360 
   361 fun cert_typ sg (envT, raw_T) =
   362   let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
   363   in (Term.add_typ_tfrees (T, envT), T) end;
   364 
   365 
   366 (* prepare props *)
   367 
   368 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   369 
   370 fun enter_term t (envS, envT, used) =
   371   (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
   372 
   373 fun read_axm sg ((envS, envT, used), (name, s)) =
   374   let
   375     fun def_sort (x, ~1) = assoc (envS, x)
   376       | def_sort _ = None;
   377     fun def_type (x, ~1) = assoc (envT, x)
   378       | def_type _ = None;
   379     val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
   380   in
   381     (enter_term t (envS, envT, used), t)
   382   end;
   383 
   384 
   385 fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
   386   let val (_, t) = Theory.cert_axm sg (name, raw_t)
   387   in (enter_term t (envS, envT, used), t) end;
   388 
   389 
   390 (* read_cterm: read in a string as a certified term, and respect the bindings
   391    that already exist for subterms. If no locale is open, this function is equal to
   392    Thm.read_cterm  *)
   393 
   394 fun read_cterm sign =
   395     let val cur_sc = get_scope_sg sign;
   396         val defaults = map (#defaults o snd) cur_sc;
   397         val envS = flat (map #1 defaults);
   398         val envT = flat (map #2 defaults);
   399         val used = flat (map #3 defaults);
   400         fun def_sort (x, ~1) = assoc (envS, x)
   401           | def_sort _ = None;
   402         fun def_type (x, ~1) = assoc (envT, x)
   403           | def_type _ = None;
   404     in (if (is_open_loc_sg sign)
   405         then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
   406         else Thm.read_cterm sign)
   407     end;
   408 
   409 (* basic functions needed for definitions and display *)
   410 (* collect all locale constants of a scope, i.e. a list of locales *)
   411 fun collect_consts sg =
   412     let val cur_sc = get_scope_sg sg;
   413         val locale_list = map snd cur_sc;
   414         val const_list = flat (map #consts locale_list)
   415     in map fst const_list end;
   416 
   417 (* filter out the Free's in a term *)
   418 fun list_frees t =
   419     case t of Const(c,T) => []
   420   | Var(v,T) => []
   421   | Free(v,T)=> [Free(v,T)]
   422   | Bound x  => []
   423   | Abs(a,T,u) => list_frees u
   424   | t1 $ t2  => (list_frees t1)  @ (list_frees t2);
   425 
   426 (* filter out all Free's in a term that are not contained
   427    in a list of strings. Used to prepare definitions. The list of strings
   428    will be the consts of the scope. We filter out the "free" Free's to be
   429    able to bind them *)
   430 fun difflist term clist =
   431     let val flist = list_frees term;
   432         fun builddiff [] sl = []
   433           | builddiff (t :: tl) sl =
   434             let val Free(v,T) = t
   435             in
   436                 if (v mem sl)
   437                 then builddiff tl sl
   438                 else t :: (builddiff tl sl)
   439             end;
   440     in distinct(builddiff flist clist) end;
   441 
   442 (* Bind a term with !! over a list of "free" Free's.
   443    To enable definitions like x + y == .... (without quantifier).
   444    Complications, because x and y have to be removed from defaults *)
   445 fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
   446     let val diffl = rev(difflist term clist);
   447         fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
   448           | abs_o (_ , _) = error ("Can't be: abs_over_free");
   449         val diffl' = map (fn (Free (s, T)) => s) diffl;
   450         val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
   451     in (defaults', (s, foldl abs_o (term, diffl))) end;
   452 
   453 (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
   454    the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
   455 fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
   456 
   457 
   458 (* concrete syntax *)
   459 
   460 fun mark_syn c = "\\<^locale>" ^ c;
   461 
   462 fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
   463 
   464 
   465 (* add_locale *)
   466 
   467 fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
   468   let val sign = Theory.sign_of thy;
   469 
   470     val name = Sign.full_name sign bname;
   471 
   472     val (envSb, old_loc_consts, _) = 
   473                     case bancestor of
   474                        Some(loc) => (get_defaults thy loc)
   475                      | None      => ([],[],[]);
   476 
   477     val old_nosyn = case bancestor of 
   478                        Some(loc) => #nosyn(#2(the_locale thy loc))
   479                      | None      => [];
   480 
   481     (* Get the full name of the ancestor *)
   482     val ancestor = case bancestor of 
   483                        Some(loc) => Some(#1(the_locale thy loc))
   484                      | None      => None;
   485 
   486      (* prepare locale consts *)
   487 
   488     fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
   489       let
   490         val c = Syntax.const_name raw_c raw_mx;
   491         val c_syn = mark_syn c;
   492         val mx = Syntax.fix_mixfix raw_c raw_mx;
   493         val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
   494           error ("The error(s) above occured in locale constant " ^ quote c);
   495         val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
   496       in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
   497 
   498     val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
   499     val loc_consts = map #1 loc_consts_syn;
   500     val loc_consts = old_loc_consts @ loc_consts;
   501     val loc_syn = map #2 loc_consts_syn;
   502     val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
   503     val loc_trfuns = mapfilter #3 loc_consts_syn;
   504 
   505 
   506     (* 1st stage: syntax_thy *)
   507 
   508     val syntax_thy =
   509       thy
   510       |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
   511       |> Theory.add_trfuns ([], loc_trfuns, [], []);
   512 
   513     val syntax_sign = Theory.sign_of syntax_thy;
   514 
   515 
   516     (* prepare rules and defs *)
   517 
   518     fun prep_axiom (env, (a, raw_t)) =
   519       let
   520         val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
   521           error ("The error(s) above occured in locale rule / definition " ^ quote a);
   522       in (env', (a, t)) end;
   523 
   524     val ((envS1, envT1, used1), loc_rules) =
   525       foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
   526     val (defaults, loc_defs) = 
   527 	foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
   528 
   529     val old_loc_consts = collect_consts syntax_sign;
   530     val new_loc_consts = (map #1 loc_consts);
   531     val all_loc_consts = old_loc_consts @ new_loc_consts;
   532 
   533     val (defaults, loc_defs_terms) = 
   534 	foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
   535     val loc_defs_thms = 
   536 	map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
   537     val (defaults, loc_thms_terms) = 
   538 	foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
   539     val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
   540 		       (loc_thms_terms)
   541                    @ loc_defs_thms;
   542 
   543 
   544     (* error messages *) 
   545 
   546     fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
   547 
   548     val err_dup_locale =
   549       if is_none (get_locale thy name) then []
   550       else ["Duplicate definition of locale " ^ quote name];
   551 
   552     (* check if definientes are locale constants 
   553        (in the same locale, so no redefining!) *)
   554     val err_def_head =
   555       let fun peal_appl t = 
   556             case t of 
   557                  t1 $ t2 => peal_appl t1
   558                | Free(t) => t
   559                | _ => locale_error ("Bad form of LHS in locale definition");
   560 	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
   561 	    | lhs _ = locale_error ("Definitions must use the == relation");
   562           val defs = map lhs loc_defs;
   563           val check = defs subset loc_consts
   564       in if check then [] 
   565          else ["defined item not declared fixed in locale " ^ quote name]
   566       end; 
   567 
   568     (* check that variables on rhs of definitions are either fixed or on lhs *)
   569     val err_var_rhs = 
   570       let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
   571 		let val varl1 = difflist d1 all_loc_consts;
   572 		    val varl2 = difflist d2 all_loc_consts
   573 		in t andalso (varl2 subset varl1)
   574 		end
   575             | compare_var_sides (_,_) = 
   576 		locale_error ("Definitions must use the == relation")
   577           val check = foldl compare_var_sides (true, loc_defs)
   578       in if check then []
   579          else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
   580       end;
   581 
   582     val errs = err_dup_locale @ err_def_head @ err_var_rhs;
   583   in
   584     if null errs then ()
   585     else error (cat_lines errs);
   586 
   587     syntax_thy
   588     |> put_locale (name, 
   589 		   make_locale ancestor loc_consts nosyn loc_thms_terms 
   590                                         loc_defs_terms   loc_thms defaults)
   591   end;
   592 
   593 
   594 val add_locale = gen_add_locale read_typ read_axm;
   595 val add_locale_i = gen_add_locale cert_typ cert_axm;
   596 
   597 (** print functions **)
   598 (* idea: substitute all locale contants (Free's) that are syntactical by their
   599          "real" constant representation (i.e. \\<^locale>constname).
   600    - function const_ssubst does this substitution
   601    - function pretty_term:
   602              if locale is open then do this substitution & then call Sign.pretty_term
   603              else call Sign.pretty_term
   604 *)
   605 (* substitutes all Free variables s in t by Const's s *)
   606 fun const_ssubst t s =
   607     case t  of
   608         Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
   609       | Const(c,T) => Const(c,T)
   610       | Var(v,T) => Var(v,T)
   611       | Bound x  => Bound x
   612       | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
   613       | t1 $ t2  => const_ssubst t1 s $ const_ssubst t2 s;
   614 
   615 (* FIXME: improve: can be expressed with foldl *)
   616 fun const_ssubst_list [] t = t
   617   | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
   618 
   619 (* pretty_term *)
   620 fun pretty_term sign =
   621     if (is_open_loc_sg sign) then
   622         let val locale_list = map snd(get_scope_sg sign);
   623             val nosyn = flat (map #nosyn locale_list);
   624             val str_list = (collect_consts sign) \\ nosyn
   625         in Sign.pretty_term sign o (const_ssubst_list str_list)
   626         end
   627     else Sign.pretty_term sign;
   628 
   629 
   630 (** locale theory setup **)
   631 
   632 val setup =
   633  [LocalesData.init];
   634 
   635 
   636 
   637 (*** Goal package ***)
   638 
   639 (*Each level of goal stack includes a proof state and alternative states,
   640   the output of the tactic applied to the preceeding level.  *)
   641 type gstack = (thm * thm Seq.seq) list;
   642 
   643 datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
   644 
   645 
   646 (*** References ***)
   647 
   648 (*Current assumption list -- set by "goal".*)
   649 val curr_prems = ref([] : thm list);
   650 
   651 (*Return assumption list -- useful if you didn't save "goal"'s result. *)
   652 fun premises() = !curr_prems;
   653 
   654 (*Current result maker -- set by "goal", used by "result".  *)
   655 fun init_mkresult _ = error "No goal has been supplied in subgoal module";
   656 val curr_mkresult = ref (init_mkresult: bool*thm->thm);
   657 
   658 val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
   659     ("PROP No_goal_has_been_supplied",propT));
   660 
   661 (*List of previous goal stacks, for the undo operation.  Set by setstate. 
   662   A list of lists!*)
   663 val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
   664 
   665 (* Stack of proof attempts *)
   666 val proofstack = ref([]: proof list);
   667 
   668 (*reset all refs*)
   669 fun reset_goals () =
   670   (curr_prems := []; curr_mkresult := init_mkresult;
   671     undo_list := [[(dummy, Seq.empty)]]);
   672 
   673 
   674 (*** Setting up goal-directed proof ***)
   675 
   676 (*Generates the list of new theories when the proof state's signature changes*)
   677 fun sign_error (sign,sign') =
   678   let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign
   679   in  case names of
   680         [name] => "\nNew theory: " ^ name
   681       | _       => "\nNew theories: " ^ space_implode ", " names
   682   end;
   683 
   684 (*Default action is to print an error message; could be suppressed for
   685   special applications.*)
   686 fun result_error_default state msg : thm =
   687   Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @
   688     [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
   689 
   690 val result_error_fn = ref result_error_default;
   691 
   692 (* alternative to standard: this function does not discharge the hypotheses
   693    first. Is used for locales, in the following function prepare_proof *)
   694 fun varify th =
   695   let val {maxidx,...} = rep_thm th
   696   in
   697     th |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
   698        |> Drule.strip_shyps_warning
   699        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   700   end;
   701 
   702 (** exporting a theorem out of a locale means turning all meta-hyps into assumptions
   703     and expand and cancel the locale definitions. 
   704     export goes through all levels in case of nested locales, whereas
   705     export_thy just goes one up. **)
   706 
   707 fun get_top_scope_thms thy = 
   708    let val sc = (get_scope_sg (Theory.sign_of thy))
   709    in if (null sc) then (warning "No locale in theory"; [])
   710       else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
   711    end;
   712 
   713 fun implies_intr_some_hyps thy A_set th = 
   714    let 
   715        val sign = Theory.sign_of thy;
   716        val used_As = A_set inter #hyps(rep_thm(th));
   717        val ctl = map (cterm_of sign) used_As
   718    in foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
   719    end; 
   720 
   721 fun standard_some thy A_set th =
   722   let val {maxidx,...} = rep_thm th
   723   in
   724     th |> implies_intr_some_hyps thy A_set
   725        |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
   726        |> Drule.strip_shyps_warning
   727        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   728   end;
   729 
   730 fun export_thy thy th = 
   731   let val A_set = get_top_scope_thms thy
   732   in
   733      standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th)))
   734   end;
   735 
   736 val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard;
   737 
   738 fun Export th = export_thy (the_context ()) th;
   739 
   740 
   741 (*Common treatment of "goal" and "prove_goal":
   742   Return assumptions, initial proof state, and function to make result.
   743   "atomic" indicates if the goal should be wrapped up in the function
   744   "Goal::prop=>prop" to avoid assumptions being returned separately.
   745 *)
   746 fun prepare_proof atomic rths chorn =
   747   let val {sign, t=horn,...} = rep_cterm chorn;
   748       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
   749       val (As, B) = Logic.strip_horn horn;
   750       val atoms = atomic andalso
   751             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
   752       val (As,B) = if atoms then ([],horn) else (As,B);
   753       val cAs = map (cterm_of sign) As;
   754       val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
   755       val cB = cterm_of sign B;
   756       val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
   757                 in  rewrite_goals_rule rths st end
   758       (*discharges assumptions from state in the order they appear in goal;
   759 	checks (if requested) that resulting theorem is equivalent to goal. *)
   760       fun mkresult (check,state) =
   761         let val state = Seq.hd (flexflex_rule state)
   762 	    		handle THM _ => state   (*smash flexflex pairs*)
   763 	    val ngoals = nprems_of state
   764             val ath = implies_intr_list cAs state
   765             val th = ath RS Drule.rev_triv_goal
   766             val {hyps,prop,sign=sign',...} = rep_thm th
   767             val final_th = if (null(hyps)) then standard th else varify th
   768         in  if not check then final_th
   769 	    else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state
   770 		("Signature of proof state has changed!" ^
   771 		 sign_error (sign,sign'))
   772             else if ngoals>0 then !result_error_fn state
   773 		(string_of_int ngoals ^ " unsolved goals!")
   774             else if (not (null hyps) andalso (not (in_locale hyps sign)))
   775 		 then !result_error_fn state
   776                   ("Additional hypotheses:\n" ^ 
   777 		   cat_lines 
   778 		    (map (Sign.string_of_term sign) 
   779 		     (filter (fn x => (not (in_locale [x] sign))) 
   780 		      hyps)))
   781 	    else if Pattern.matches (Sign.tsig_of sign)
   782 			            (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   783 		 then final_th
   784 	    else  !result_error_fn state "proved a different theorem"
   785         end
   786   in
   787      if Sign.eq_sg(sign, Thm.sign_of_thm st0)
   788      then (prems, st0, mkresult)
   789      else error ("Definitions would change the proof state's signature" ^
   790 		 sign_error (sign, Thm.sign_of_thm st0))
   791   end
   792   handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
   793 
   794 (*Prints exceptions readably to users*)
   795 fun print_sign_exn_unit sign e = 
   796   case e of
   797      THM (msg,i,thms) =>
   798 	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   799 	  seq print_thm thms)
   800    | THEORY (msg,thys) =>
   801 	 (writeln ("Exception THEORY raised:\n" ^ msg);
   802 	  seq (Pretty.writeln o Display.pretty_theory) thys)
   803    | TERM (msg,ts) =>
   804 	 (writeln ("Exception TERM raised:\n" ^ msg);
   805 	  seq (writeln o Sign.string_of_term sign) ts)
   806    | TYPE (msg,Ts,ts) =>
   807 	 (writeln ("Exception TYPE raised:\n" ^ msg);
   808 	  seq (writeln o Sign.string_of_typ sign) Ts;
   809 	  seq (writeln o Sign.string_of_term sign) ts)
   810    | e => raise e;
   811 
   812 (*Prints an exception, then fails*)
   813 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR);
   814 
   815 (** the prove_goal.... commands
   816     Prove theorem using the listed tactics; check it has the specified form.
   817     Augment signature with all type assignments of goal.
   818     Syntax is similar to "goal" command for easy keyboard use. **)
   819 
   820 (*Version taking the goal as a cterm*)
   821 fun prove_goalw_cterm_general check rths chorn tacsf =
   822   let val (prems, st0, mkresult) = prepare_proof false rths chorn
   823       val tac = EVERY (tacsf prems)
   824       fun statef() = 
   825 	  (case Seq.pull (tac st0) of 
   826 	       Some(st,_) => st
   827 	     | _ => error ("prove_goal: tactic failed"))
   828   in  mkresult (check, cond_timeit (!Output.timing) statef)  end
   829   handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
   830 	       writeln ("The exception above was raised for\n" ^ 
   831 		      Display.string_of_cterm chorn); raise e);
   832 
   833 (*Two variants: one checking the result, one not.  
   834   Neither prints runtime messages: they are for internal packages.*)
   835 fun prove_goalw_cterm rths chorn = 
   836 	setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
   837 and prove_goalw_cterm_nocheck rths chorn = 
   838 	setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
   839 
   840 
   841 (*Version taking the goal as a string*)
   842 fun prove_goalw thy rths agoal tacsf =
   843   let val sign = Theory.sign_of thy
   844       val chorn = read_cterm sign (agoal,propT)
   845   in  prove_goalw_cterm_general true rths chorn tacsf end
   846   handle ERROR => error (*from read_cterm?*)
   847 		("The error(s) above occurred for " ^ quote agoal);
   848 
   849 (*String version with no meta-rewrite-rules*)
   850 fun prove_goal thy = prove_goalw thy [];
   851 
   852 (*quick and dirty version (conditional)*)
   853 fun quick_and_dirty_prove_goalw_cterm thy rews ct tacs =
   854   prove_goalw_cterm rews ct
   855     (if ! quick_and_dirty then (K [SkipProof.cheat_tac thy]) else tacs);
   856 
   857 
   858 (*** Commands etc ***)
   859 
   860 (*Return the current goal stack, if any, from undo_list*)
   861 fun getstate() : gstack = case !undo_list of 
   862       []   => error"No current state in subgoal module"
   863     | x::_ => x;
   864 
   865 (*Pops the given goal stack*)
   866 fun pop [] = error"Cannot go back past the beginning of the proof!"
   867   | pop (pair::pairs) = (pair,pairs);
   868 
   869 
   870 (* Print a level of the goal stack -- subject to quiet mode *)
   871 
   872 val quiet = ref false;
   873 fun disable_pr () = quiet := true;
   874 fun enable_pr () = quiet := false;
   875 
   876 fun print_top ((th, _), pairs) =
   877   if ! quiet then ()
   878   else ! Display.print_current_goals_fn (length pairs) (! goals_limit) th;
   879 
   880 (*Printing can raise exceptions, so the assignment occurs last.
   881   Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
   882 fun setstate newgoals = 
   883   (print_top (pop newgoals);  undo_list := newgoals :: !undo_list);
   884 
   885 (*Given a proof state transformation, return a command that updates
   886     the goal stack*)
   887 fun make_command com = setstate (com (pop (getstate())));
   888 
   889 (*Apply a function on proof states to the current goal stack*)
   890 fun apply_fun f = f (pop(getstate()));
   891 
   892 (*Return the top theorem, representing the proof state*)
   893 fun topthm () = apply_fun  (fn ((th,_), _) => th);
   894 
   895 (*Return the final result.  *)
   896 fun result () = !curr_mkresult (true, topthm());
   897 
   898 (*Return the result UNCHECKED that it equals the goal -- for synthesis,
   899   answer extraction, or other instantiation of Vars *)
   900 fun uresult () = !curr_mkresult (false, topthm());
   901 
   902 (*Get subgoal i from goal stack*)
   903 fun getgoal i = Logic.get_goal (prop_of (topthm())) i;
   904 
   905 (*Return subgoal i's hypotheses as meta-level assumptions.
   906   For debugging uses of METAHYPS*)
   907 local exception GETHYPS of thm list
   908 in
   909 fun gethyps i = 
   910     (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm());  [])
   911     handle GETHYPS hyps => hyps
   912 end;
   913 
   914 (*Which thms could apply to goal i? (debugs tactics involving filter_thms) *)
   915 fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
   916 
   917 (*For inspecting earlier levels of the backward proof*)
   918 fun chop_level n (pair,pairs) = 
   919   let val level = length pairs
   920   in  if n<0 andalso ~n <= level
   921       then  List.drop (pair::pairs, ~n) 
   922       else if 0<=n andalso n<= level
   923       then  List.drop (pair::pairs, level - n) 
   924       else  error ("Level number must lie between 0 and " ^ 
   925 		   string_of_int level)
   926   end;
   927 
   928 (*Print the given level of the proof; prlev ~1 prints previous level*)
   929 fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n)));
   930 fun pr () = (enable_pr (); apply_fun print_top);
   931 
   932 (*Set goals_limit and print again*)
   933 fun prlim n = (goals_limit:=n; pr());
   934 
   935 (** the goal.... commands
   936     Read main goal.  Set global variables curr_prems, curr_mkresult. 
   937     Initial subgoal and premises are rewritten using rths. **)
   938 
   939 (*Version taking the goal as a cterm; if you have a term t and theory thy, use
   940     goalw_cterm rths (cterm_of (Theory.sign_of thy) t);      *)
   941 fun agoalw_cterm atomic rths chorn = 
   942   let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
   943   in  undo_list := [];
   944       setstate [ (st0, Seq.empty) ];  
   945       curr_prems := prems;
   946       curr_mkresult := mkresult;
   947       prems
   948   end;
   949 
   950 val goalw_cterm = agoalw_cterm false;
   951 
   952 (*Version taking the goal as a string*)
   953 fun agoalw atomic thy rths agoal = 
   954     agoalw_cterm atomic rths (read_cterm(Theory.sign_of thy)(agoal,propT))
   955     handle ERROR => error (*from type_assign, etc via prepare_proof*)
   956 	("The error(s) above occurred for " ^ quote agoal);
   957 
   958 val goalw = agoalw false;
   959 
   960 (*String version with no meta-rewrite-rules*)
   961 fun agoal atomic thy = agoalw atomic thy [];
   962 val goal = agoal false;
   963 
   964 (*now the versions that wrap the goal up in `Goal' to make it atomic*)
   965 val atomic_goalw = agoalw true;
   966 val atomic_goal = agoal true;
   967 
   968 (*implicit context versions*)
   969 fun Goal s = atomic_goal (Context.the_context ()) s;
   970 fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s;
   971 
   972 (*simple version with minimal amount of checking and postprocessing*)
   973 fun simple_prove_goal_cterm G f =
   974   let
   975     val As = Drule.strip_imp_prems G;
   976     val B = Drule.strip_imp_concl G;
   977     val asms = map (norm_hhf_rule o assume) As;
   978     fun check None = error "prove_goal: tactic failed"
   979       | check (Some (thm, _)) = (case nprems_of thm of
   980             0 => thm
   981           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   982   in
   983     standard (implies_intr_list As
   984       (check (Seq.pull (EVERY (f asms) (trivial B)))))
   985   end;
   986 
   987 
   988 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
   989 fun by_com tac ((th,ths), pairs) : gstack =
   990   (case  Seq.pull(tac th)  of
   991      None      => error"by: tactic failed"
   992    | Some(th2,ths2) => 
   993        (if eq_thm(th,th2) 
   994 	  then warning "Warning: same as previous level"
   995 	  else if eq_thm_sg(th,th2) then ()
   996 	  else warning ("Warning: signature of proof state has changed" ^
   997 		       sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
   998        ((th2,ths2)::(th,ths)::pairs)));
   999 
  1000 fun by tac = cond_timeit (!Output.timing) 
  1001     (fn() => make_command (by_com tac));
  1002 
  1003 (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
  1004    Good for debugging proofs involving prove_goal.*)
  1005 val byev = by o EVERY;
  1006 
  1007 
  1008 (*Backtracking means find an alternative result from a tactic.
  1009   If none at this level, try earlier levels*)
  1010 fun backtrack [] = error"back: no alternatives"
  1011   | backtrack ((th,thstr) :: pairs) =
  1012      (case Seq.pull thstr of
  1013 	  None      => (writeln"Going back a level..."; backtrack pairs)
  1014 	| Some(th2,thstr2) =>  
  1015 	   (if eq_thm(th,th2) 
  1016 	      then warning "Warning: same as previous choice at this level"
  1017 	      else if eq_thm_sg(th,th2) then ()
  1018 	      else warning "Warning: signature of proof state has changed";
  1019 	    (th2,thstr2)::pairs));
  1020 
  1021 fun back() = setstate (backtrack (getstate()));
  1022 
  1023 (*Chop back to previous level of the proof*)
  1024 fun choplev n = make_command (chop_level n);
  1025 
  1026 (*Chopping back the goal stack*)
  1027 fun chop () = make_command (fn (_,pairs) => pairs);
  1028 
  1029 (*Restore the previous proof state;  discard current state. *)
  1030 fun undo() = case !undo_list of
  1031       [] => error"No proof state"
  1032     | [_] => error"Already at initial state"
  1033     | _::newundo =>  (undo_list := newundo;  pr()) ;
  1034 
  1035 
  1036 (*** Managing the proof stack ***)
  1037 
  1038 fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult);
  1039 
  1040 fun restore_proof(Proof(ul,prems,mk)) =
  1041  (undo_list:= ul;  curr_prems:= prems;  curr_mkresult := mk;  prems);
  1042 
  1043 
  1044 fun top_proof() = case !proofstack of
  1045 	[] => error("Stack of proof attempts is empty!")
  1046     | p::ps => (p,ps);
  1047 
  1048 (*  push a copy of the current proof state on to the stack *)
  1049 fun push_proof() = (proofstack := (save_proof() :: !proofstack));
  1050 
  1051 (* discard the top proof state of the stack *)
  1052 fun pop_proof() = 
  1053   let val (p,ps) = top_proof()
  1054       val prems = restore_proof p
  1055   in proofstack := ps;  pr();  prems end;
  1056 
  1057 (* rotate the stack so that the top element goes to the bottom *)
  1058 fun rotate_proof() = let val (p,ps) = top_proof()
  1059 		    in proofstack := ps@[save_proof()];
  1060 		       restore_proof p;
  1061 		       pr();
  1062 		       !curr_prems
  1063 		    end;
  1064 
  1065 
  1066 (** Shortcuts for commonly-used tactics **)
  1067 
  1068 fun bws rls = by (rewrite_goals_tac rls);
  1069 fun bw rl = bws [rl];
  1070 
  1071 fun brs rls i = by (resolve_tac rls i);
  1072 fun br rl = brs [rl];
  1073 
  1074 fun bes rls i = by (eresolve_tac rls i);
  1075 fun be rl = bes [rl];
  1076 
  1077 fun bds rls i = by (dresolve_tac rls i);
  1078 fun bd rl = bds [rl];
  1079 
  1080 fun ba i = by (assume_tac i);
  1081 
  1082 fun ren str i = by (rename_tac str i);
  1083 
  1084 (** Shortcuts to work on the first applicable subgoal **)
  1085 
  1086 fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls)));
  1087 fun fr rl = frs [rl];
  1088 
  1089 fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls)));
  1090 fun fe rl = fes [rl];
  1091 
  1092 fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls)));
  1093 fun fd rl = fds [rl];
  1094 
  1095 fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
  1096 
  1097 (** Reading and printing terms wrt the current theory **)
  1098 
  1099 fun top_sg() = Thm.sign_of_thm (topthm());
  1100 
  1101 fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
  1102 
  1103 (*Print a term under the current signature of the proof state*)
  1104 fun prin t = writeln (Sign.string_of_term (top_sg()) t);
  1105 
  1106 fun printyp T = writeln (Sign.string_of_typ (top_sg()) T);
  1107 
  1108 fun pprint_term t = Sign.pprint_term (top_sg()) t;
  1109 
  1110 fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
  1111 
  1112 
  1113 (*Prints exceptions nicely at top level; 
  1114   raises the exception in order to have a polymorphic type!*)
  1115 fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
  1116 
  1117 
  1118 
  1119 (** theorem database operations **)
  1120 
  1121 (* storing *)
  1122 
  1123 fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm);
  1124 fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms);
  1125 
  1126 fun qed name = ThmDatabase.ml_store_thm (name, result ());
  1127 fun qed_goal name thy goal tacsf = ThmDatabase.ml_store_thm (name, prove_goal thy goal tacsf);
  1128 fun qed_goalw name thy rews goal tacsf =
  1129   ThmDatabase.ml_store_thm (name, prove_goalw thy rews goal tacsf);
  1130 fun qed_spec_mp name =
  1131   ThmDatabase.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
  1132 fun qed_goal_spec_mp name thy s p =
  1133   bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
  1134 fun qed_goalw_spec_mp name thy defs s p =
  1135   bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
  1136 
  1137 fun no_qed () = ();
  1138 
  1139 
  1140 (* retrieval *)
  1141 
  1142 fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (topthm ()));
  1143 
  1144 fun thms_containing raw_consts =
  1145   let
  1146     val thy = theory_of_goal ();
  1147     val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
  1148   in
  1149     (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
  1150       [] => ()
  1151     | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
  1152     PureThy.thms_containing_consts thy consts
  1153   end;
  1154 
  1155 fun findI i = PureThy.find_intros_goal (theory_of_goal()) (topthm()) i;
  1156 
  1157 fun findEs i =
  1158   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
  1159       val prems = Logic.prems_of_goal (prop_of (topthm())) i
  1160       val thy = theory_of_goal();
  1161       val thmss = map (PureThy.find_elims thy) prems
  1162   in foldl (gen_union eq_nth) ([],thmss) end;
  1163 
  1164 fun findE i j =
  1165   let val prems = Logic.prems_of_goal (prop_of (topthm())) i
  1166       val thy = theory_of_goal();
  1167   in PureThy.find_elims thy (nth_elem(j-1, prems)) end;
  1168 
  1169 end;
  1170 
  1171 structure BasicGoals: BASIC_GOALS = Goals;
  1172 open BasicGoals;