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