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