src/Pure/drule.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25)
changeset 1194 563ecd14c1d8
parent 952 9e10962866b0
child 1218 59ed8ef1a3a1
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
     1 (*  Title:      Pure/drule.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Derived rules and other operations on theorems and theories
     7 *)
     8 
     9 infix 0 RS RSN RL RLN MRS MRL COMP;
    10 
    11 signature DRULE =
    12   sig
    13   structure Thm : THM
    14   local open Thm  in
    15   val add_defs		: (string * string) list -> theory -> theory
    16   val add_defs_i	: (string * term) list -> theory -> theory
    17   val asm_rl		: thm
    18   val assume_ax		: theory -> string -> thm
    19   val COMP		: thm * thm -> thm
    20   val compose		: thm * int * thm -> thm list
    21   val cprems_of		: thm -> cterm list
    22   val cskip_flexpairs	: cterm -> cterm
    23   val cstrip_imp_prems	: cterm -> cterm list
    24   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    25   val cut_rl		: thm
    26   val equal_abs_elim	: cterm  -> thm -> thm
    27   val equal_abs_elim_list: cterm list -> thm -> thm
    28   val eq_thm		: thm * thm -> bool
    29   val eq_thm_sg		: thm * thm -> bool
    30   val flexpair_abs_elim_list: cterm list -> thm -> thm
    31   val forall_intr_list	: cterm list -> thm -> thm
    32   val forall_intr_frees	: thm -> thm
    33   val forall_intr_vars	: thm -> thm
    34   val forall_elim_list	: cterm list -> thm -> thm
    35   val forall_elim_var	: int -> thm -> thm
    36   val forall_elim_vars	: int -> thm -> thm
    37   val implies_elim_list	: thm -> thm list -> thm
    38   val implies_intr_list	: cterm list -> thm -> thm
    39   val MRL		: thm list list * thm list -> thm list
    40   val MRS		: thm list * thm -> thm
    41   val pprint_cterm	: cterm -> pprint_args -> unit
    42   val pprint_ctyp	: ctyp -> pprint_args -> unit
    43   val pprint_theory	: theory -> pprint_args -> unit
    44   val pprint_thm	: thm -> pprint_args -> unit
    45   val pretty_thm	: thm -> Sign.Syntax.Pretty.T
    46   val print_cterm	: cterm -> unit
    47   val print_ctyp	: ctyp -> unit
    48   val print_goals	: int -> thm -> unit
    49   val print_goals_ref	: (int -> thm -> unit) ref
    50   val print_syntax	: theory -> unit
    51   val print_theory	: theory -> unit
    52   val print_thm		: thm -> unit
    53   val prth		: thm -> thm
    54   val prthq		: thm Sequence.seq -> thm Sequence.seq
    55   val prths		: thm list -> thm list
    56   val read_instantiate	: (string*string)list -> thm -> thm
    57   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    58   val read_insts	:
    59           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    60                   -> (indexname -> typ option) * (indexname -> sort option)
    61                   -> string list -> (string*string)list
    62                   -> (indexname*ctyp)list * (cterm*cterm)list
    63   val reflexive_thm	: thm
    64   val revcut_rl		: thm
    65   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    66         -> meta_simpset -> int -> thm -> thm
    67   val rewrite_goals_rule: thm list -> thm -> thm
    68   val rewrite_rule	: thm list -> thm -> thm
    69   val RS		: thm * thm -> thm
    70   val RSN		: thm * (int * thm) -> thm
    71   val RL		: thm list * thm list -> thm list
    72   val RLN		: thm list * (int * thm list) -> thm list
    73   val show_hyps		: bool ref
    74   val size_of_thm	: thm -> int
    75   val standard		: thm -> thm
    76   val string_of_cterm	: cterm -> string
    77   val string_of_ctyp	: ctyp -> string
    78   val string_of_thm	: thm -> string
    79   val symmetric_thm	: thm
    80   val thin_rl		: thm
    81   val transitive_thm	: thm
    82   val triv_forall_equality: thm
    83   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    84   val zero_var_indexes	: thm -> thm
    85   end
    86   end;
    87 
    88 
    89 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
    90 struct
    91 structure Thm = Thm;
    92 structure Sign = Thm.Sign;
    93 structure Type = Sign.Type;
    94 structure Syntax = Sign.Syntax;
    95 structure Pretty = Syntax.Pretty
    96 structure Symtab = Sign.Symtab;
    97 
    98 local open Thm
    99 in
   100 
   101 (**** Extend Theories ****)
   102 
   103 (** add constant definitions **)
   104 
   105 (* all_axioms_of *)
   106 
   107 (*results may contain duplicates!*)
   108 
   109 fun ancestry_of thy =
   110   thy :: flat (map ancestry_of (parents_of thy));
   111 
   112 val all_axioms_of = 
   113   flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
   114 
   115 
   116 (* clash_types, clash_consts *)
   117 
   118 (*check if types have common instance (ignoring sorts)*)
   119 
   120 fun clash_types ty1 ty2 =
   121   let
   122     val ty1' = Type.varifyT ty1;
   123     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
   124   in
   125     Type.raw_unify (ty1', ty2')
   126   end;
   127 
   128 fun clash_consts (c1, ty1) (c2, ty2) =
   129   c1 = c2 andalso clash_types ty1 ty2;
   130 
   131 
   132 (* clash_defns *)
   133 
   134 fun clash_defn c_ty (name, tm) =
   135   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
   136     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   137   end handle TERM _ => None;
   138 
   139 fun clash_defns c_ty axms =
   140   distinct (mapfilter (clash_defn c_ty) axms);
   141 
   142 
   143 (* dest_defn *)
   144 
   145 fun dest_defn tm =
   146   let
   147     fun err msg = raise_term msg [tm];
   148 
   149     val (lhs, rhs) = Logic.dest_equals tm
   150       handle TERM _ => err "Not a meta-equality (==)";
   151     val (head, args) = strip_comb lhs;
   152     val (c, ty) = dest_Const head
   153       handle TERM _ => err "Head of lhs not a constant";
   154 
   155     fun occs_const (Const c_ty') = (c_ty' = (c, ty))
   156       | occs_const (Abs (_, _, t)) = occs_const t
   157       | occs_const (t $ u) = occs_const t orelse occs_const u
   158       | occs_const _ = false;
   159 
   160     val show_frees = commas_quote o map (fst o dest_Free);
   161     val show_tfrees = commas_quote o map fst;
   162 
   163     val lhs_dups = duplicates args;
   164     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   165     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   166   in
   167     if not (forall is_Free args) then
   168       err "Arguments of lhs have to be variables"
   169     else if not (null lhs_dups) then
   170       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   171     else if not (null rhs_extras) then
   172       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   173     else if not (null rhs_extrasT) then
   174       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   175     else if occs_const rhs then
   176       err ("Constant to be defined occurs on rhs")
   177     else (c, ty)
   178   end;
   179 
   180 
   181 (* check_defn *)
   182 
   183 fun err_in_defn name msg =
   184   (writeln msg; error ("The error(s) above occurred in definition " ^ quote name));
   185 
   186 fun check_defn sign (axms, (name, tm)) =
   187   let
   188     fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
   189       [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
   190 
   191     fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
   192     fun show_defns c = commas o map (show_defn c);
   193 
   194     val (c, ty) = dest_defn tm
   195       handle TERM (msg, _) => err_in_defn name msg;
   196     val defns = clash_defns (c, ty) axms;
   197   in
   198     if not (null defns) then
   199       err_in_defn name ("Definition of " ^ show_const (c, ty) ^
   200         " clashes with " ^ show_defns c defns)
   201     else (name, tm) :: axms
   202   end;
   203 
   204 
   205 (* add_defs *)
   206 
   207 fun ext_defns prep_axm raw_axms thy =
   208   let
   209     val axms = map (prep_axm (sign_of thy)) raw_axms;
   210     val all_axms = all_axioms_of thy;
   211   in
   212     foldl (check_defn (sign_of thy)) (all_axms, axms);
   213     add_axioms_i axms thy
   214   end;
   215 
   216 val add_defs_i = ext_defns cert_axm;
   217 val add_defs = ext_defns read_axm;
   218 
   219 
   220 
   221 (**** More derived rules and operations on theorems ****)
   222 
   223 (** some cterm->cterm operations: much faster than calling cterm_of! **)
   224 
   225 (*Discard flexflex pairs; return a cterm*)
   226 fun cskip_flexpairs ct =
   227     case term_of ct of
   228 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   229 	    cskip_flexpairs (#2 (dest_cimplies ct))
   230       | _ => ct;
   231 
   232 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   233 fun cstrip_imp_prems ct =
   234     let val (cA,cB) = dest_cimplies ct
   235     in  cA :: cstrip_imp_prems cB  end
   236     handle TERM _ => [];
   237 
   238 (*The premises of a theorem, as a cterm list*)
   239 val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
   240 
   241 
   242 (** reading of instantiations **)
   243 
   244 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   245         | _ => error("Lexical error in variable name " ^ quote (implode cs));
   246 
   247 fun absent ixn =
   248   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   249 
   250 fun inst_failure ixn =
   251   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   252 
   253 (* this code is a bit of a mess. add_cterm could be simplified greatly if
   254    simultaneous instantiations were read or at least type checked
   255    simultaneously rather than one after the other. This would make the tricky
   256    composition of implicit type instantiations (parameter tye) superfluous.
   257 *)
   258 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
   259 let val {tsig,...} = Sign.rep_sg sign
   260     fun split([],tvs,vs) = (tvs,vs)
   261       | split((sv,st)::l,tvs,vs) = (case explode sv of
   262                   "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   263                 | cs => split(l,tvs,(indexname cs,st)::vs));
   264     val (tvs,vs) = split(insts,[],[]);
   265     fun readT((a,i),st) =
   266         let val ixn = ("'" ^ a,i);
   267             val S = case rsorts ixn of Some S => S | None => absent ixn;
   268             val T = Sign.read_typ (sign,sorts) st;
   269         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   270            else inst_failure ixn
   271         end
   272     val tye = map readT tvs;
   273     fun add_cterm ((cts,tye,used), (ixn,st)) =
   274         let val T = case rtypes ixn of
   275                       Some T => typ_subst_TVars tye T
   276                     | None => absent ixn;
   277             val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
   278             val cts' = (ixn,T,ct)::cts
   279             fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
   280             val used' = add_term_tvarnames(term_of ct,used);
   281         in (map inst cts',tye2 @ tye,used') end
   282     val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
   283 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
   284     map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
   285 end;
   286 
   287 
   288 
   289 (*** Printing of theories, theorems, etc. ***)
   290 
   291 (*If false, hypotheses are printed as dots*)
   292 val show_hyps = ref true;
   293 
   294 fun pretty_thm th =
   295 let val {sign, hyps, prop,...} = rep_thm th
   296     val hsymbs = if null hyps then []
   297                  else if !show_hyps then
   298                       [Pretty.brk 2,
   299                        Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
   300                  else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
   301                       [Pretty.str"]"];
   302 in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
   303 
   304 val string_of_thm = Pretty.string_of o pretty_thm;
   305 
   306 val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   307 
   308 
   309 (** Top-level commands for printing theorems **)
   310 val print_thm = writeln o string_of_thm;
   311 
   312 fun prth th = (print_thm th; th);
   313 
   314 (*Print and return a sequence of theorems, separated by blank lines. *)
   315 fun prthq thseq =
   316   (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
   317 
   318 (*Print and return a list of theorems, separated by blank lines. *)
   319 fun prths ths = (print_list_ln print_thm ths; ths);
   320 
   321 
   322 (* other printing commands *)
   323 
   324 fun pprint_ctyp cT =
   325   let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
   326 
   327 fun string_of_ctyp cT =
   328   let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
   329 
   330 val print_ctyp = writeln o string_of_ctyp;
   331 
   332 fun pprint_cterm ct =
   333   let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
   334 
   335 fun string_of_cterm ct =
   336   let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
   337 
   338 val print_cterm = writeln o string_of_cterm;
   339 
   340 
   341 (* print theory *)
   342 
   343 val pprint_theory = Sign.pprint_sg o sign_of;
   344 
   345 val print_syntax = Syntax.print_syntax o syn_of;
   346 
   347 fun print_axioms thy =
   348   let
   349     val {sign, new_axioms, ...} = rep_theory thy;
   350     val axioms = Symtab.dest new_axioms;
   351 
   352     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
   353       Pretty.quote (Sign.pretty_term sign t)];
   354   in
   355     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
   356   end;
   357 
   358 fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
   359 
   360 
   361 
   362 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
   363 
   364 (* get type_env, sort_env of term *)
   365 
   366 local
   367   open Syntax;
   368 
   369   fun ins_entry (x, y) [] = [(x, [y])]
   370     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   371         if x = x' then (x', y ins ys') :: pairs
   372         else pair :: ins_entry (x, y) pairs;
   373 
   374   fun add_type_env (Free (x, T), env) = ins_entry (T, x) env
   375     | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env
   376     | add_type_env (Abs (_, _, t), env) = add_type_env (t, env)
   377     | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env))
   378     | add_type_env (_, env) = env;
   379 
   380   fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env)
   381     | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
   382     | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
   383 
   384   val sort = map (apsnd sort_strings);
   385 in
   386   fun type_env t = sort (add_type_env (t, []));
   387   fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
   388 end;
   389 
   390 
   391 (* print_goals *)
   392 
   393 fun print_goals maxgoals state =
   394   let
   395     open Syntax;
   396 
   397     val {sign, prop, ...} = rep_thm state;
   398 
   399     val pretty_term = Sign.pretty_term sign;
   400     val pretty_typ = Sign.pretty_typ sign;
   401     val pretty_sort = Sign.pretty_sort;
   402 
   403     fun pretty_vars prtf (X, vs) = Pretty.block
   404       [Pretty.block (Pretty.commas (map Pretty.str vs)),
   405         Pretty.str " ::", Pretty.brk 1, prtf X];
   406 
   407     fun print_list _ _ [] = ()
   408       | print_list name prtf lst =
   409           (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst)));
   410 
   411 
   412     fun print_goals (_, []) = ()
   413       | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
   414           [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A]));
   415             print_goals (n + 1, As));
   416 
   417     val print_ffpairs =
   418       print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair);
   419 
   420     val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env;
   421     val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env;
   422 
   423 
   424     val (tpairs, As, B) = Logic.strip_horn prop;
   425     val ngoals = length As;
   426 
   427     val orig_no_freeTs = ! show_no_free_types;
   428     val orig_sorts = ! show_sorts;
   429 
   430     fun restore () =
   431       (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
   432   in
   433     (show_no_free_types := true; show_sorts := false;
   434       Pretty.writeln (pretty_term B);
   435       if ngoals = 0 then writeln "No subgoals!"
   436       else if ngoals > maxgoals then
   437         (print_goals (1, take (maxgoals, As));
   438           writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   439       else print_goals (1, As);
   440 
   441       print_ffpairs tpairs;
   442 
   443       if orig_sorts then
   444         (print_types prop; print_sorts prop)
   445       else if ! show_types then
   446         print_types prop
   447       else ())
   448     handle exn => (restore (); raise exn);
   449     restore ()
   450   end;
   451 
   452 
   453 (*"hook" for user interfaces: allows print_goals to be replaced*)
   454 val print_goals_ref = ref print_goals;
   455 
   456 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
   457      Used for establishing default types (of variables) and sorts (of
   458      type variables) when reading another term.
   459      Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
   460 ***)
   461 
   462 fun types_sorts thm =
   463     let val {prop,hyps,...} = rep_thm thm;
   464         val big = list_comb(prop,hyps); (* bogus term! *)
   465         val vars = map dest_Var (term_vars big);
   466         val frees = map dest_Free (term_frees big);
   467         val tvars = term_tvars big;
   468         val tfrees = term_tfrees big;
   469         fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
   470         fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
   471     in (typ,sort) end;
   472 
   473 (** Standardization of rules **)
   474 
   475 (*Generalization over a list of variables, IGNORING bad ones*)
   476 fun forall_intr_list [] th = th
   477   | forall_intr_list (y::ys) th =
   478         let val gth = forall_intr_list ys th
   479         in  forall_intr y gth   handle THM _ =>  gth  end;
   480 
   481 (*Generalization over all suitable Free variables*)
   482 fun forall_intr_frees th =
   483     let val {prop,sign,...} = rep_thm th
   484     in  forall_intr_list
   485          (map (cterm_of sign) (sort atless (term_frees prop)))
   486          th
   487     end;
   488 
   489 (*Replace outermost quantified variable by Var of given index.
   490     Could clash with Vars already present.*)
   491 fun forall_elim_var i th =
   492     let val {prop,sign,...} = rep_thm th
   493     in case prop of
   494           Const("all",_) $ Abs(a,T,_) =>
   495               forall_elim (cterm_of sign (Var((a,i), T)))  th
   496         | _ => raise THM("forall_elim_var", i, [th])
   497     end;
   498 
   499 (*Repeat forall_elim_var until all outer quantifiers are removed*)
   500 fun forall_elim_vars i th =
   501     forall_elim_vars i (forall_elim_var i th)
   502         handle THM _ => th;
   503 
   504 (*Specialization over a list of cterms*)
   505 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
   506 
   507 (* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
   508 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
   509 
   510 (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
   511 fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
   512 
   513 (*Reset Var indexes to zero, renaming to preserve distinctness*)
   514 fun zero_var_indexes th =
   515     let val {prop,sign,...} = rep_thm th;
   516         val vars = term_vars prop
   517         val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
   518         val inrs = add_term_tvars(prop,[]);
   519         val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
   520         val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
   521         val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
   522         fun varpairs([],[]) = []
   523           | varpairs((var as Var(v,T)) :: vars, b::bs) =
   524                 let val T' = typ_subst_TVars tye T
   525                 in (cterm_of sign (Var(v,T')),
   526                     cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   527                 end
   528           | varpairs _ = raise TERM("varpairs", []);
   529     in instantiate (ctye, varpairs(vars,rev bs)) th end;
   530 
   531 
   532 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   533     all generality expressed by Vars having index 0.*)
   534 fun standard th =
   535     let val {maxidx,...} = rep_thm th
   536     in  varifyT (zero_var_indexes (forall_elim_vars(maxidx+1)
   537                          (forall_intr_frees(implies_intr_hyps th))))
   538     end;
   539 
   540 (*Assume a new formula, read following the same conventions as axioms.
   541   Generalizes over Free variables,
   542   creates the assumption, and then strips quantifiers.
   543   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   544              [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   545 fun assume_ax thy sP =
   546     let val sign = sign_of thy
   547         val prop = Logic.close_form (term_of (read_cterm sign
   548                          (sP, propT)))
   549     in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   550 
   551 (*Resolution: exactly one resolvent must be produced.*)
   552 fun tha RSN (i,thb) =
   553   case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
   554       ([th],_) => th
   555     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
   556     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
   557 
   558 (*resolution: P==>Q, Q==>R gives P==>R. *)
   559 fun tha RS thb = tha RSN (1,thb);
   560 
   561 (*For joining lists of rules*)
   562 fun thas RLN (i,thbs) =
   563   let val resolve = biresolution false (map (pair false) thas) i
   564       fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
   565   in  flat (map resb thbs)  end;
   566 
   567 fun thas RL thbs = thas RLN (1,thbs);
   568 
   569 (*Resolve a list of rules against bottom_rl from right to left;
   570   makes proof trees*)
   571 fun rls MRS bottom_rl =
   572   let fun rs_aux i [] = bottom_rl
   573         | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
   574   in  rs_aux 1 rls  end;
   575 
   576 (*As above, but for rule lists*)
   577 fun rlss MRL bottom_rls =
   578   let fun rs_aux i [] = bottom_rls
   579         | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   580   in  rs_aux 1 rlss  end;
   581 
   582 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   583   with no lifting or renaming!  Q may contain ==> or meta-quants
   584   ALWAYS deletes premise i *)
   585 fun compose(tha,i,thb) =
   586     Sequence.list_of_s (bicompose false (false,tha,0) i thb);
   587 
   588 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
   589 fun tha COMP thb =
   590     case compose(tha,1,thb) of
   591         [th] => th
   592       | _ =>   raise THM("COMP", 1, [tha,thb]);
   593 
   594 (*Instantiate theorem th, reading instantiations under signature sg*)
   595 fun read_instantiate_sg sg sinsts th =
   596     let val ts = types_sorts th;
   597         val used = add_term_tvarnames(#prop(rep_thm th),[]);
   598     in  instantiate (read_insts sg ts ts used sinsts) th  end;
   599 
   600 (*Instantiate theorem th, reading instantiations under theory of th*)
   601 fun read_instantiate sinsts th =
   602     read_instantiate_sg (#sign (rep_thm th)) sinsts th;
   603 
   604 
   605 (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   606   Instantiates distinct Vars by terms, inferring type instantiations. *)
   607 local
   608   fun add_types ((ct,cu), (sign,tye)) =
   609     let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   610         and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   611         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   612         val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
   613           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   614     in  (sign', tye')  end;
   615 in
   616 fun cterm_instantiate ctpairs0 th =
   617   let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
   618       val tsig = #tsig(Sign.rep_sg sign);
   619       fun instT(ct,cu) = let val inst = subst_TVars tye
   620                          in (cterm_fun inst ct, cterm_fun inst cu) end
   621       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   622   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   623   handle TERM _ =>
   624            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   625        | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
   626 end;
   627 
   628 
   629 (** theorem equality test is exported and used by BEST_FIRST **)
   630 
   631 (*equality of theorems uses equality of signatures and
   632   the a-convertible test for terms*)
   633 fun eq_thm (th1,th2) =
   634     let val {sign=sg1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   635         and {sign=sg2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   636     in  Sign.eq_sg (sg1,sg2) andalso
   637         aconvs(hyps1,hyps2) andalso
   638         prop1 aconv prop2
   639     end;
   640 
   641 (*Do the two theorems have the same signature?*)
   642 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   643 
   644 (*Useful "distance" function for BEST_FIRST*)
   645 val size_of_thm = size_of_term o #prop o rep_thm;
   646 
   647 
   648 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   649     (some) type variable renaming **)
   650 
   651  (* Can't use term_vars, because it sorts the resulting list of variable names.
   652     We instead need the unique list noramlised by the order of appearance
   653     in the term. *)
   654 fun term_vars' (t as Var(v,T)) = [t]
   655   | term_vars' (Abs(_,_,b)) = term_vars' b
   656   | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
   657   | term_vars' _ = [];
   658 
   659 fun forall_intr_vars th =
   660   let val {prop,sign,...} = rep_thm th;
   661       val vars = distinct (term_vars' prop);
   662   in forall_intr_list (map (cterm_of sign) vars) th end;
   663 
   664 fun weak_eq_thm (tha,thb) = 
   665     eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
   666 
   667 
   668 
   669 (*** Meta-Rewriting Rules ***)
   670 
   671 
   672 val reflexive_thm =
   673   let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
   674   in Thm.reflexive cx end;
   675 
   676 val symmetric_thm =
   677   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   678   in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   679 
   680 val transitive_thm =
   681   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   682       val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
   683       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   684   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   685 
   686 (** Below, a "conversion" has type cterm -> thm **)
   687 
   688 val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
   689 
   690 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   691 (*Do not rewrite flex-flex pairs*)
   692 fun goals_conv pred cv =
   693   let fun gconv i ct =
   694         let val (A,B) = Thm.dest_cimplies ct
   695             val (thA,j) = case term_of A of
   696                   Const("=?=",_)$_$_ => (reflexive A, i)
   697                 | _ => (if pred i then cv A else reflexive A, i+1)
   698         in  combination (combination refl_cimplies thA) (gconv j B) end
   699         handle TERM _ => reflexive ct
   700   in gconv 1 end;
   701 
   702 (*Use a conversion to transform a theorem*)
   703 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   704 
   705 (*rewriting conversion*)
   706 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   707 
   708 (*Rewrite a theorem*)
   709 fun rewrite_rule thms =
   710   fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms));
   711 
   712 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   713 fun rewrite_goals_rule thms =
   714   fconv_rule (goals_conv (K true) (rew_conv (true,false) (K(K None))
   715              (Thm.mss_of thms)));
   716 
   717 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   718 fun rewrite_goal_rule mode prover mss i thm =
   719   if 0 < i  andalso  i <= nprems_of thm
   720   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   721   else raise THM("rewrite_goal_rule",i,[thm]);
   722 
   723 
   724 (** Derived rules mainly for METAHYPS **)
   725 
   726 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   727 fun equal_abs_elim ca eqth =
   728   let val {sign=signa, t=a, ...} = rep_cterm ca
   729       and combth = combination eqth (reflexive ca)
   730       val {sign,prop,...} = rep_thm eqth
   731       val (abst,absu) = Logic.dest_equals prop
   732       val cterm = cterm_of (Sign.merge (sign,signa))
   733   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   734            (transitive combth (beta_conversion (cterm (absu$a))))
   735   end
   736   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   737 
   738 (*Calling equal_abs_elim with multiple terms*)
   739 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   740 
   741 local
   742   open Logic
   743   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   744   fun err th = raise THM("flexpair_inst: ", 0, [th])
   745   fun flexpair_inst def th =
   746     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   747         val cterm = cterm_of sign
   748         fun cvar a = cterm(Var((a,0),alpha))
   749         val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   750                    def
   751     in  equal_elim def' th
   752     end
   753     handle THM _ => err th | bind => err th
   754 in
   755 val flexpair_intr = flexpair_inst (symmetric flexpair_def)
   756 and flexpair_elim = flexpair_inst flexpair_def
   757 end;
   758 
   759 (*Version for flexflex pairs -- this supports lifting.*)
   760 fun flexpair_abs_elim_list cts =
   761     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   762 
   763 
   764 (*** Some useful meta-theorems ***)
   765 
   766 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   767 val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
   768 
   769 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   770 val cut_rl = trivial(read_cterm Sign.proto_pure
   771         ("PROP ?psi ==> PROP ?theta", propT));
   772 
   773 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   774      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   775 val revcut_rl =
   776   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   777       and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
   778   in  standard (implies_intr V
   779                 (implies_intr VW
   780                  (implies_elim (assume VW) (assume V))))
   781   end;
   782 
   783 (*for deleting an unwanted assumption*)
   784 val thin_rl =
   785   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   786       and W = read_cterm Sign.proto_pure ("PROP W", propT);
   787   in  standard (implies_intr V (implies_intr W (assume W)))
   788   end;
   789 
   790 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   791 val triv_forall_equality =
   792   let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
   793       and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
   794       and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
   795   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   796                            (implies_intr V  (forall_intr x (assume V))))
   797   end;
   798 
   799 end
   800 end;
   801