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