src/Pure/drule.ML
author paulson
Wed Nov 13 10:38:08 1996 +0100 (1996-11-13)
changeset 2180 934572a94139
parent 2152 76d5ed939545
child 2266 82aef6857c5b
permissions -rw-r--r--
Removal of polymorphic equality via mem, subset, eq_set, etc
     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 = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
   343         val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
   344         fun varpairs([],[]) = []
   345           | varpairs((var as Var(v,T)) :: vars, b::bs) =
   346                 let val T' = typ_subst_TVars tye T
   347                 in (cterm_of sign (Var(v,T')),
   348                     cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   349                 end
   350           | varpairs _ = raise TERM("varpairs", []);
   351     in instantiate (ctye, varpairs(vars,rev bs)) th end;
   352 
   353 
   354 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   355     all generality expressed by Vars having index 0.*)
   356 fun standard th =
   357   let val {maxidx,...} = rep_thm th
   358   in
   359     th |> implies_intr_hyps
   360        |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
   361        |> Thm.strip_shyps |> Thm.implies_intr_shyps
   362        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   363   end;
   364 
   365 
   366 (*Assume a new formula, read following the same conventions as axioms.
   367   Generalizes over Free variables,
   368   creates the assumption, and then strips quantifiers.
   369   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   370              [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   371 fun assume_ax thy sP =
   372     let val sign = sign_of thy
   373         val prop = Logic.close_form (term_of (read_cterm sign
   374                          (sP, propT)))
   375     in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   376 
   377 (*Resolution: exactly one resolvent must be produced.*)
   378 fun tha RSN (i,thb) =
   379   case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
   380       ([th],_) => th
   381     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
   382     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
   383 
   384 (*resolution: P==>Q, Q==>R gives P==>R. *)
   385 fun tha RS thb = tha RSN (1,thb);
   386 
   387 (*For joining lists of rules*)
   388 fun thas RLN (i,thbs) =
   389   let val resolve = biresolution false (map (pair false) thas) i
   390       fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
   391   in  flat (map resb thbs)  end;
   392 
   393 fun thas RL thbs = thas RLN (1,thbs);
   394 
   395 (*Resolve a list of rules against bottom_rl from right to left;
   396   makes proof trees*)
   397 fun rls MRS bottom_rl =
   398   let fun rs_aux i [] = bottom_rl
   399         | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
   400   in  rs_aux 1 rls  end;
   401 
   402 (*As above, but for rule lists*)
   403 fun rlss MRL bottom_rls =
   404   let fun rs_aux i [] = bottom_rls
   405         | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   406   in  rs_aux 1 rlss  end;
   407 
   408 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   409   with no lifting or renaming!  Q may contain ==> or meta-quants
   410   ALWAYS deletes premise i *)
   411 fun compose(tha,i,thb) =
   412     Sequence.list_of_s (bicompose false (false,tha,0) i thb);
   413 
   414 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
   415 fun tha COMP thb =
   416     case compose(tha,1,thb) of
   417         [th] => th
   418       | _ =>   raise THM("COMP", 1, [tha,thb]);
   419 
   420 (*Instantiate theorem th, reading instantiations under signature sg*)
   421 fun read_instantiate_sg sg sinsts th =
   422     let val ts = types_sorts th;
   423         val used = add_term_tvarnames(#prop(rep_thm th),[]);
   424     in  instantiate (read_insts sg ts ts used sinsts) th  end;
   425 
   426 (*Instantiate theorem th, reading instantiations under theory of th*)
   427 fun read_instantiate sinsts th =
   428     read_instantiate_sg (#sign (rep_thm th)) sinsts th;
   429 
   430 
   431 (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   432   Instantiates distinct Vars by terms, inferring type instantiations. *)
   433 local
   434   fun add_types ((ct,cu), (sign,tye,maxidx)) =
   435     let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   436         and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   437         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   438         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   439         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
   440           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   441     in  (sign', tye', maxi')  end;
   442 in
   443 fun cterm_instantiate ctpairs0 th =
   444   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
   445       val tsig = #tsig(Sign.rep_sg sign);
   446       fun instT(ct,cu) = let val inst = subst_TVars tye
   447                          in (cterm_fun inst ct, cterm_fun inst cu) end
   448       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   449   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   450   handle TERM _ =>
   451            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   452        | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
   453 end;
   454 
   455 
   456 (** theorem equality test is exported and used by BEST_FIRST **)
   457 
   458 (*equality of theorems uses equality of signatures and
   459   the a-convertible test for terms*)
   460 fun eq_thm (th1,th2) =
   461     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   462         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   463     in  Sign.eq_sg (sg1,sg2) andalso
   464         eq_set_sort (shyps1, shyps2) andalso
   465         aconvs(hyps1,hyps2) andalso
   466         prop1 aconv prop2
   467     end;
   468 
   469 (*equality of theorems using similarity of signatures,
   470   i.e. the theorems belong to the same theory but not necessarily to the same
   471   version of this theory*)
   472 fun same_thm (th1,th2) =
   473     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   474         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   475     in  Sign.same_sg (sg1,sg2) andalso
   476         eq_set_sort (shyps1, shyps2) andalso
   477         aconvs(hyps1,hyps2) andalso
   478         prop1 aconv prop2
   479     end;
   480 
   481 (*Do the two theorems have the same signature?*)
   482 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   483 
   484 (*Useful "distance" function for BEST_FIRST*)
   485 val size_of_thm = size_of_term o #prop o rep_thm;
   486 
   487 
   488 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   489     (some) type variable renaming **)
   490 
   491  (* Can't use term_vars, because it sorts the resulting list of variable names.
   492     We instead need the unique list noramlised by the order of appearance
   493     in the term. *)
   494 fun term_vars' (t as Var(v,T)) = [t]
   495   | term_vars' (Abs(_,_,b)) = term_vars' b
   496   | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
   497   | term_vars' _ = [];
   498 
   499 fun forall_intr_vars th =
   500   let val {prop,sign,...} = rep_thm th;
   501       val vars = distinct (term_vars' prop);
   502   in forall_intr_list (map (cterm_of sign) vars) th end;
   503 
   504 fun weak_eq_thm (tha,thb) =
   505     eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
   506 
   507 
   508 
   509 (*** Meta-Rewriting Rules ***)
   510 
   511 
   512 val reflexive_thm =
   513   let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
   514   in Thm.reflexive cx end;
   515 
   516 val symmetric_thm =
   517   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   518   in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   519 
   520 val transitive_thm =
   521   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   522       val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
   523       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   524   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   525 
   526 (** Below, a "conversion" has type cterm -> thm **)
   527 
   528 val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
   529 
   530 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   531 (*Do not rewrite flex-flex pairs*)
   532 fun goals_conv pred cv =
   533   let fun gconv i ct =
   534         let val (A,B) = dest_implies ct
   535             val (thA,j) = case term_of A of
   536                   Const("=?=",_)$_$_ => (reflexive A, i)
   537                 | _ => (if pred i then cv A else reflexive A, i+1)
   538         in  combination (combination refl_implies thA) (gconv j B) end
   539         handle TERM _ => reflexive ct
   540   in gconv 1 end;
   541 
   542 (*Use a conversion to transform a theorem*)
   543 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   544 
   545 (*rewriting conversion*)
   546 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   547 
   548 (*Rewrite a theorem*)
   549 fun rewrite_rule []   th = th
   550   | rewrite_rule thms th =
   551 	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
   552 
   553 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   554 fun rewrite_goals_rule []   th = th
   555   | rewrite_goals_rule thms th =
   556 	fconv_rule (goals_conv (K true) 
   557 		    (rew_conv (true,false) (K(K None))
   558 		     (Thm.mss_of thms))) 
   559 	           th;
   560 
   561 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   562 fun rewrite_goal_rule mode prover mss i thm =
   563   if 0 < i  andalso  i <= nprems_of thm
   564   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   565   else raise THM("rewrite_goal_rule",i,[thm]);
   566 
   567 
   568 (** Derived rules mainly for METAHYPS **)
   569 
   570 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   571 fun equal_abs_elim ca eqth =
   572   let val {sign=signa, t=a, ...} = rep_cterm ca
   573       and combth = combination eqth (reflexive ca)
   574       val {sign,prop,...} = rep_thm eqth
   575       val (abst,absu) = Logic.dest_equals prop
   576       val cterm = cterm_of (Sign.merge (sign,signa))
   577   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   578            (transitive combth (beta_conversion (cterm (absu$a))))
   579   end
   580   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   581 
   582 (*Calling equal_abs_elim with multiple terms*)
   583 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   584 
   585 local
   586   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   587   fun err th = raise THM("flexpair_inst: ", 0, [th])
   588   fun flexpair_inst def th =
   589     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   590         val cterm = cterm_of sign
   591         fun cvar a = cterm(Var((a,0),alpha))
   592         val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   593                    def
   594     in  equal_elim def' th
   595     end
   596     handle THM _ => err th | bind => err th
   597 in
   598 val flexpair_intr = flexpair_inst (symmetric flexpair_def)
   599 and flexpair_elim = flexpair_inst flexpair_def
   600 end;
   601 
   602 (*Version for flexflex pairs -- this supports lifting.*)
   603 fun flexpair_abs_elim_list cts =
   604     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   605 
   606 
   607 (*** Some useful meta-theorems ***)
   608 
   609 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   610 val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
   611 
   612 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   613 val cut_rl = trivial(read_cterm Sign.proto_pure
   614         ("PROP ?psi ==> PROP ?theta", propT));
   615 
   616 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   617      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   618 val revcut_rl =
   619   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   620       and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
   621   in  standard (implies_intr V
   622                 (implies_intr VW
   623                  (implies_elim (assume VW) (assume V))))
   624   end;
   625 
   626 (*for deleting an unwanted assumption*)
   627 val thin_rl =
   628   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   629       and W = read_cterm Sign.proto_pure ("PROP W", propT);
   630   in  standard (implies_intr V (implies_intr W (assume W)))
   631   end;
   632 
   633 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   634 val triv_forall_equality =
   635   let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
   636       and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
   637       and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
   638   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   639                            (implies_intr V  (forall_intr x (assume V))))
   640   end;
   641 
   642 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   643    (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
   644    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   645 *)
   646 val swap_prems_rl =
   647   let val cmajor = read_cterm Sign.proto_pure
   648             ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
   649       val major = assume cmajor;
   650       val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
   651       val minor1 = assume cminor1;
   652       val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
   653       val minor2 = assume cminor2;
   654   in standard
   655        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   656          (implies_elim (implies_elim major minor1) minor2))))
   657   end;
   658 
   659 end;
   660 
   661 open Drule;