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