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