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