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