src/Pure/drule.ML
author wenzelm
Wed Jul 23 10:22:48 1997 +0200 (1997-07-23)
changeset 3555 5a720f6b9f38
parent 3530 d9ca80f0759c
child 3575 4e9beacb5339
permissions -rw-r--r--
added rewrite_thm;
     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 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 []   th = th
   552   | rewrite_rule thms th =
   553 	fconv_rule (rew_conv (true,false) (K(K None)) (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 []   th = th
   559   | rewrite_goals_rule thms th =
   560 	fconv_rule (goals_conv (K true) 
   561 		    (rew_conv (true,false) (K(K None))
   562 		     (Thm.mss_of thms))) 
   563 	           th;
   564 
   565 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   566 fun rewrite_goal_rule mode prover mss i thm =
   567   if 0 < i  andalso  i <= nprems_of thm
   568   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   569   else raise THM("rewrite_goal_rule",i,[thm]);
   570 
   571 
   572 (** Derived rules mainly for METAHYPS **)
   573 
   574 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   575 fun equal_abs_elim ca eqth =
   576   let val {sign=signa, t=a, ...} = rep_cterm ca
   577       and combth = combination eqth (reflexive ca)
   578       val {sign,prop,...} = rep_thm eqth
   579       val (abst,absu) = Logic.dest_equals prop
   580       val cterm = cterm_of (Sign.merge (sign,signa))
   581   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   582            (transitive combth (beta_conversion (cterm (absu$a))))
   583   end
   584   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   585 
   586 (*Calling equal_abs_elim with multiple terms*)
   587 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   588 
   589 local
   590   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   591   fun err th = raise THM("flexpair_inst: ", 0, [th])
   592   fun flexpair_inst def th =
   593     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   594         val cterm = cterm_of sign
   595         fun cvar a = cterm(Var((a,0),alpha))
   596         val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   597                    def
   598     in  equal_elim def' th
   599     end
   600     handle THM _ => err th | bind => err th
   601 in
   602 val flexpair_intr = flexpair_inst (symmetric flexpair_def)
   603 and flexpair_elim = flexpair_inst flexpair_def
   604 end;
   605 
   606 (*Version for flexflex pairs -- this supports lifting.*)
   607 fun flexpair_abs_elim_list cts =
   608     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   609 
   610 
   611 (*** Some useful meta-theorems ***)
   612 
   613 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   614 val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
   615 
   616 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   617 val cut_rl = trivial(read_cterm Sign.proto_pure
   618         ("PROP ?psi ==> PROP ?theta", propT));
   619 
   620 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   621      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   622 val revcut_rl =
   623   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   624       and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
   625   in  standard (implies_intr V
   626                 (implies_intr VW
   627                  (implies_elim (assume VW) (assume V))))
   628   end;
   629 
   630 (*for deleting an unwanted assumption*)
   631 val thin_rl =
   632   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   633       and W = read_cterm Sign.proto_pure ("PROP W", propT);
   634   in  standard (implies_intr V (implies_intr W (assume W)))
   635   end;
   636 
   637 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   638 val triv_forall_equality =
   639   let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
   640       and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
   641       and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
   642   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   643                            (implies_intr V  (forall_intr x (assume V))))
   644   end;
   645 
   646 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   647    (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
   648    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   649 *)
   650 val swap_prems_rl =
   651   let val cmajor = read_cterm Sign.proto_pure
   652             ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
   653       val major = assume cmajor;
   654       val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
   655       val minor1 = assume cminor1;
   656       val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
   657       val minor2 = assume cminor2;
   658   in standard
   659        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   660          (implies_elim (implies_elim major minor1) minor2))))
   661   end;
   662 
   663 end;
   664 
   665 open Drule;