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