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