TFL/rules.new.sml
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3629 8e95bd329fff
child 4713 bea2ab2e360b
permissions -rw-r--r--
adapted extend_trfunsT;
     1 (*  Title:      TFL/rules
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Emulation of HOL inference rules for TFL
     7 *)
     8 
     9 structure Rules : Rules_sig = 
    10 struct
    11 
    12 open Utils;
    13 
    14 structure USyntax  = USyntax;
    15 structure S  = USyntax;
    16 structure U  = Utils;
    17 structure D = Dcterm;
    18 
    19 
    20 fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg};
    21 
    22 
    23 fun cconcl thm = D.drop_prop(#prop(crep_thm thm));
    24 fun chyps thm = map D.drop_prop(#hyps(crep_thm thm));
    25 
    26 fun dest_thm thm = 
    27    let val {prop,hyps,...} = rep_thm thm
    28    in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop)
    29    end;
    30 
    31 
    32 
    33 (* Inference rules *)
    34 
    35 (*---------------------------------------------------------------------------
    36  *        Equality (one step)
    37  *---------------------------------------------------------------------------*)
    38 fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq;
    39 fun SYM thm = thm RS sym;
    40 
    41 fun ALPHA thm ctm1 =
    42    let val ctm2 = cprop_of thm
    43        val ctm2_eq = reflexive ctm2
    44        val ctm1_eq = reflexive ctm1
    45    in equal_elim (transitive ctm2_eq ctm1_eq) thm
    46    end;
    47 
    48 
    49 (*----------------------------------------------------------------------------
    50  *        typ instantiation
    51  *---------------------------------------------------------------------------*)
    52 fun INST_TYPE blist thm = 
    53   let val {sign,...} = rep_thm thm
    54       val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist
    55   in Thm.instantiate (blist',[]) thm
    56   end
    57   handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};
    58 
    59 
    60 (*----------------------------------------------------------------------------
    61  *        Implication and the assumption list
    62  *
    63  * Assumptions get stuck on the meta-language assumption list. Implications 
    64  * are in the object language, so discharging an assumption "A" from theorem
    65  * "B" results in something that looks like "A --> B".
    66  *---------------------------------------------------------------------------*)
    67 fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
    68 
    69 
    70 (*---------------------------------------------------------------------------
    71  * Implication in TFL is -->. Meta-language implication (==>) is only used
    72  * in the implementation of some of the inference rules below.
    73  *---------------------------------------------------------------------------*)
    74 fun MP th1 th2 = th2 RS (th1 RS mp);
    75 
    76 fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI;
    77 
    78 fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm;
    79 
    80 
    81 fun FILTER_DISCH_ALL P thm =
    82  let fun check tm = U.holds P (#t(rep_cterm tm))
    83  in  foldr (fn (tm,th) => if (check tm) then DISCH tm th else th)
    84               (chyps thm, thm)
    85  end;
    86 
    87 (* freezeT expensive! *)
    88 fun UNDISCH thm = 
    89    let val tm = D.mk_prop(#1(D.dest_imp(cconcl (freezeT thm))))
    90    in implies_elim (thm RS mp) (ASSUME tm)
    91    end
    92    handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""};
    93 
    94 fun PROVE_HYP ath bth =  MP (DISCH (cconcl ath) bth) ath;
    95 
    96 local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)"
    97       val dummy = by (rtac impI 1)
    98       val dummy = by (rtac (p2 RS mp) 1)
    99       val dummy = by (rtac (p1 RS mp) 1)
   100       val dummy = by (assume_tac 1)
   101       val imp_trans = result()
   102 in
   103 fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans)
   104 end;
   105 
   106 (*----------------------------------------------------------------------------
   107  *        Conjunction
   108  *---------------------------------------------------------------------------*)
   109 fun CONJUNCT1 thm = (thm RS conjunct1)
   110 fun CONJUNCT2 thm = (thm RS conjunct2);
   111 fun CONJUNCTS th  = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th))
   112                     handle _ => [th];
   113 
   114 fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}
   115   | LIST_CONJ [th] = th
   116   | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst);
   117 
   118 
   119 (*----------------------------------------------------------------------------
   120  *        Disjunction
   121  *---------------------------------------------------------------------------*)
   122 local val {prop,sign,...} = rep_thm disjI1
   123       val [P,Q] = term_vars prop
   124       val disj1 = forall_intr (cterm_of sign Q) disjI1
   125 in
   126 fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
   127 end;
   128 
   129 local val {prop,sign,...} = rep_thm disjI2
   130       val [P,Q] = term_vars prop
   131       val disj2 = forall_intr (cterm_of sign P) disjI2
   132 in
   133 fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   134 end;
   135 
   136 
   137 (*----------------------------------------------------------------------------
   138  *
   139  *                   A1 |- M1, ..., An |- Mn
   140  *     ---------------------------------------------------
   141  *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
   142  *
   143  *---------------------------------------------------------------------------*)
   144 
   145 
   146 fun EVEN_ORS thms =
   147   let fun blue ldisjs [] _ = []
   148         | blue ldisjs (th::rst) rdisjs =
   149             let val tail = tl rdisjs
   150                 val rdisj_tl = D.list_mk_disj tail
   151             in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
   152                :: blue (ldisjs@[cconcl th]) rst tail
   153             end handle _ => [itlist DISJ2 ldisjs th]
   154    in
   155    blue [] thms (map cconcl thms)
   156    end;
   157 
   158 
   159 (*----------------------------------------------------------------------------
   160  *
   161  *         A |- P \/ Q   B,P |- R    C,Q |- R
   162  *     ---------------------------------------------------
   163  *                     A U B U C |- R
   164  *
   165  *---------------------------------------------------------------------------*)
   166 local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
   167       val dummy = by (rtac (p1 RS disjE) 1)
   168       val dummy = by (rtac (p2 RS mp) 1)
   169       val dummy = by (assume_tac 1)
   170       val dummy = by (rtac (p3 RS mp) 1)
   171       val dummy = by (assume_tac 1)
   172       val tfl_exE = result()
   173 in
   174 fun DISJ_CASES th1 th2 th3 = 
   175    let val c = D.drop_prop(cconcl th1)
   176        val (disj1,disj2) = D.dest_disj c
   177        val th2' = DISCH disj1 th2
   178        val th3' = DISCH disj2 th3
   179    in
   180    th3' RS (th2' RS (th1 RS tfl_exE))
   181    end
   182 end;
   183 
   184 
   185 (*-----------------------------------------------------------------------------
   186  *
   187  *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
   188  *     ---------------------------------------------------
   189  *                           |- M
   190  *
   191  * Note. The list of theorems may be all jumbled up, so we have to 
   192  * first organize it to align with the first argument (the disjunctive 
   193  * theorem).
   194  *---------------------------------------------------------------------------*)
   195 
   196 fun organize eq =    (* a bit slow - analogous to insertion sort *)
   197  let fun extract a alist =
   198      let fun ex (_,[]) = raise RULES_ERR{func = "organize",
   199                                          mesg = "not a permutation.1"}
   200            | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
   201      in ex ([],alist)
   202      end
   203      fun place [] [] = []
   204        | place (a::rst) alist =
   205            let val (item,next) = extract a alist
   206            in item::place rst next
   207            end
   208        | place _ _ = raise RULES_ERR{func = "organize",
   209                                      mesg = "not a permutation.2"}
   210  in place
   211  end;
   212 (* freezeT expensive! *)
   213 fun DISJ_CASESL disjth thl =
   214    let val c = cconcl disjth
   215        fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t 
   216 			               aconv term_of atm)
   217 	                      (#hyps(rep_thm th))
   218        val tml = D.strip_disj c
   219        fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"}
   220          | DL th [th1] = PROVE_HYP th th1
   221          | DL th [th1,th2] = DISJ_CASES th th1 th2
   222          | DL th (th1::rst) = 
   223             let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
   224              in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
   225    in DL (freezeT disjth) (organize eq tml thl)
   226    end;
   227 
   228 
   229 (*----------------------------------------------------------------------------
   230  *        Universals
   231  *---------------------------------------------------------------------------*)
   232 local (* this is fragile *)
   233       val {prop,sign,...} = rep_thm spec
   234       val x = hd (tl (term_vars prop))
   235       val (TVar (indx,_)) = type_of x
   236       val gspec = forall_intr (cterm_of sign x) spec
   237 in
   238 fun SPEC tm thm = 
   239    let val {sign,T,...} = rep_cterm tm
   240        val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
   241    in thm RS (forall_elim tm gspec')
   242    end
   243 end;
   244 
   245 fun SPEC_ALL thm = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
   246 
   247 val ISPEC = SPEC
   248 val ISPECL = rev_itlist ISPEC;
   249 
   250 (* Not optimized! Too complicated. *)
   251 local val {prop,sign,...} = rep_thm allI
   252       val [P] = add_term_vars (prop, [])
   253       fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
   254       fun ctm_theta s = map (fn (i,tm2) => 
   255                              let val ctm2 = cterm_of s tm2
   256                              in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
   257                              end)
   258       fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta, 
   259                                            ctm_theta s tm_theta)
   260 in
   261 fun GEN v th =
   262    let val gth = forall_intr v th
   263        val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
   264        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   265        val tsig = #tsig(Sign.rep_sg sign)
   266        val theta = Pattern.match tsig (P,P')
   267        val allI2 = instantiate (certify sign theta) allI
   268        val thm = implies_elim allI2 gth
   269        val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
   270        val prop' = tp $ (A $ Abs(x,ty,M))
   271    in ALPHA thm (cterm_of sign prop')
   272    end
   273 end;
   274 
   275 val GENL = itlist GEN;
   276 
   277 fun GEN_ALL thm = 
   278    let val {prop,sign,...} = rep_thm thm
   279        val tycheck = cterm_of sign
   280        val vlist = map tycheck (add_term_vars (prop, []))
   281   in GENL vlist thm
   282   end;
   283 
   284 
   285 fun MATCH_MP th1 th2 = 
   286    if (D.is_forall (D.drop_prop(cconcl th1)))
   287    then MATCH_MP (th1 RS spec) th2
   288    else MP th1 th2;
   289 
   290 
   291 (*----------------------------------------------------------------------------
   292  *        Existentials
   293  *---------------------------------------------------------------------------*)
   294 
   295 
   296 
   297 (*--------------------------------------------------------------------------- 
   298  * Existential elimination
   299  *
   300  *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
   301  *      ------------------------------------     (variable v occurs nowhere)
   302  *                A1 u A2 |- t'
   303  *
   304  *---------------------------------------------------------------------------*)
   305 
   306 local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q"
   307       val dummy = by (rtac (p1 RS exE) 1)
   308       val dummy = by (rtac ((p2 RS allE) RS mp) 1)
   309       val dummy = by (assume_tac 2)
   310       val dummy = by (assume_tac 1)
   311       val choose_thm = result()
   312 in
   313 fun CHOOSE(fvar,exth) fact =
   314    let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
   315        val redex = capply lam fvar
   316        val {sign, t = t$u,...} = rep_cterm redex
   317        val residue = cterm_of sign (betapply(t,u))
   318     in GEN fvar (DISCH residue fact)  RS (exth RS choose_thm)
   319    end
   320 end;
   321 
   322 
   323 local val {prop,sign,...} = rep_thm exI
   324       val [P,x] = term_vars prop
   325 in
   326 fun EXISTS (template,witness) thm =
   327    let val {prop,sign,...} = rep_thm thm
   328        val P' = cterm_of sign P
   329        val x' = cterm_of sign x
   330        val abstr = #2(dest_comb template)
   331    in
   332    thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   333    end
   334 end;
   335 
   336 (*----------------------------------------------------------------------------
   337  *
   338  *         A |- M
   339  *   -------------------   [v_1,...,v_n]
   340  *    A |- ?v1...v_n. M
   341  *
   342  *---------------------------------------------------------------------------*)
   343 
   344 fun EXISTL vlist th = 
   345   U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
   346            vlist th;
   347 
   348 
   349 (*----------------------------------------------------------------------------
   350  *
   351  *       A |- M[x_1,...,x_n]
   352  *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
   353  *       A |- ?y_1...y_n. M
   354  *
   355  *---------------------------------------------------------------------------*)
   356 (* Could be improved, but needs "subst_free" for certified terms *)
   357 
   358 fun IT_EXISTS blist th = 
   359    let val {sign,...} = rep_thm th
   360        val tych = cterm_of sign
   361        val detype = #t o rep_cterm
   362        val blist' = map (fn (x,y) => (detype x, detype y)) blist
   363        fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
   364        
   365   in
   366   U.itlist (fn (b as (r1,r2)) => fn thm => 
   367         EXISTS(?r2(subst_free[b] 
   368 		   (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
   369               thm)
   370        blist' th
   371   end;
   372 
   373 (*---------------------------------------------------------------------------
   374  *  Faster version, that fails for some as yet unknown reason
   375  * fun IT_EXISTS blist th = 
   376  *    let val {sign,...} = rep_thm th
   377  *        val tych = cterm_of sign
   378  *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
   379  *   in
   380  *  fold (fn (b as (r1,r2), thm) => 
   381  *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
   382  *           r1) thm)  blist th
   383  *   end;
   384  *---------------------------------------------------------------------------*)
   385 
   386 (*----------------------------------------------------------------------------
   387  *        Rewriting
   388  *---------------------------------------------------------------------------*)
   389 
   390 fun SUBS thl = 
   391    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
   392 
   393 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
   394 in
   395 fun simpl_conv ss thl ctm = 
   396  rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
   397  RS meta_eq_to_obj_eq
   398 end;
   399 
   400 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
   401 in
   402 val RIGHT_ASSOC = rewrite_rule [prover"((a|b)|c) = (a|(b|c))" RS eq_reflection]
   403 val ASM = refl RS iffD1
   404 end;
   405 
   406 
   407 
   408 
   409 (*---------------------------------------------------------------------------
   410  *                  TERMINATION CONDITION EXTRACTION
   411  *---------------------------------------------------------------------------*)
   412 
   413 
   414 (* Object language quantifier, i.e., "!" *)
   415 fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   416 
   417 
   418 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   419 fun is_cong thm = 
   420   let val {prop, ...} = rep_thm thm
   421   in case prop 
   422      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
   423          (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
   424       | _ => true
   425   end;
   426 
   427 
   428    
   429 fun dest_equal(Const ("==",_) $ 
   430 	       (Const ("Trueprop",_) $ lhs) 
   431 	       $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
   432   | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   433   | dest_equal tm = S.dest_eq tm;
   434 
   435 fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   436 
   437 fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
   438   | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
   439 
   440 val is_all = Utils.can dest_all;
   441 
   442 fun strip_all fm =
   443    if (is_all fm)
   444    then let val {Bvar,Body} = dest_all fm
   445             val (bvs,core)  = strip_all Body
   446         in ((Bvar::bvs), core)
   447         end
   448    else ([],fm);
   449 
   450 fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   451   | break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
   452 
   453 fun list_break_all(Const("all",_) $ Abs (s,ty,body)) = 
   454      let val (L,core) = list_break_all body
   455      in ((s,ty)::L, core)
   456      end
   457   | list_break_all tm = ([],tm);
   458 
   459 (*---------------------------------------------------------------------------
   460  * Rename a term of the form
   461  *
   462  *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn 
   463  *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
   464  * to one of
   465  *
   466  *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn 
   467  *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
   468  * 
   469  * This prevents name problems in extraction, and helps the result to read
   470  * better. There is a problem with varstructs, since they can introduce more
   471  * than n variables, and some extra reasoning needs to be done.
   472  *---------------------------------------------------------------------------*)
   473 
   474 fun get ([],_,L) = rev L
   475   | get (ant::rst,n,L) =  
   476       case (list_break_all ant)
   477         of ([],_) => get (rst, n+1,L)
   478          | (vlist,body) =>
   479             let val eq = Logic.strip_imp_concl body
   480                 val (f,args) = S.strip_comb (get_lhs eq)
   481                 val (vstrl,_) = S.strip_abs f
   482                 val names  = variantlist (map (#1 o dest_Free) vstrl,
   483 					  add_term_names(body, []))
   484             in get (rst, n+1, (names,n)::L)
   485             end handle _ => get (rst, n+1, L);
   486 
   487 (* Note: rename_params_rule counts from 1, not 0 *)
   488 fun rename thm = 
   489   let val {prop,sign,...} = rep_thm thm
   490       val tych = cterm_of sign
   491       val ants = Logic.strip_imp_prems prop
   492       val news = get (ants,1,[])
   493   in 
   494   U.rev_itlist rename_params_rule news thm
   495   end;
   496 
   497 
   498 (*---------------------------------------------------------------------------
   499  * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
   500  *---------------------------------------------------------------------------*)
   501 
   502 fun list_beta_conv tm =
   503   let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
   504       fun iter [] = reflexive tm
   505         | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
   506   in iter  end;
   507 
   508 
   509 (*---------------------------------------------------------------------------
   510  * Trace information for the rewriter
   511  *---------------------------------------------------------------------------*)
   512 val term_ref = ref[] : term list ref
   513 val mss_ref = ref [] : meta_simpset list ref;
   514 val thm_ref = ref [] : thm list ref;
   515 val tracing = ref false;
   516 
   517 fun say s = if !tracing then prs s else ();
   518 
   519 fun print_thms s L = 
   520    (say s; 
   521     map (fn th => say (string_of_thm th ^"\n")) L;
   522     say"\n");
   523 
   524 fun print_cterms s L = 
   525    (say s; 
   526     map (fn th => say (string_of_cterm th ^"\n")) L;
   527     say"\n");
   528 
   529 (*---------------------------------------------------------------------------
   530  * General abstraction handlers, should probably go in USyntax.
   531  *---------------------------------------------------------------------------*)
   532 fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body}
   533                          handle _ => S.mk_pabs{varstruct = vstr, body = body};
   534 
   535 fun list_mk_aabs (vstrl,tm) =
   536     U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
   537 
   538 fun dest_aabs tm = 
   539    let val {Bvar,Body} = S.dest_abs tm
   540    in (Bvar,Body)
   541    end handle _ => let val {varstruct,body} = S.dest_pabs tm
   542                    in (varstruct,body)
   543                    end;
   544 
   545 fun strip_aabs tm =
   546    let val (vstr,body) = dest_aabs tm
   547        val (bvs, core) = strip_aabs body
   548    in (vstr::bvs, core)
   549    end
   550    handle _ => ([],tm);
   551 
   552 fun dest_combn tm 0 = (tm,[])
   553   | dest_combn tm n = 
   554      let val {Rator,Rand} = S.dest_comb tm
   555          val (f,rands) = dest_combn Rator (n-1)
   556      in (f,Rand::rands)
   557      end;
   558 
   559 
   560 
   561 
   562 local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   563       fun mk_fst tm = 
   564           let val ty as Type("*", [fty,sty]) = type_of tm
   565           in  Const ("fst", ty --> fty) $ tm  end
   566       fun mk_snd tm = 
   567           let val ty as Type("*", [fty,sty]) = type_of tm
   568           in  Const ("snd", ty --> sty) $ tm  end
   569 in
   570 fun XFILL tych x vstruct = 
   571   let fun traverse p xocc L =
   572         if (is_Free p)
   573         then tych xocc::L
   574         else let val (p1,p2) = dest_pair p
   575              in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   576              end
   577   in 
   578   traverse vstruct x []
   579 end end;
   580 
   581 (*---------------------------------------------------------------------------
   582  * Replace a free tuple (vstr) by a universally quantified variable (a).
   583  * Note that the notion of "freeness" for a tuple is different than for a
   584  * variable: if variables in the tuple also occur in any other place than
   585  * an occurrences of the tuple, they aren't "free" (which is thus probably
   586  *  the wrong word to use).
   587  *---------------------------------------------------------------------------*)
   588 
   589 fun VSTRUCT_ELIM tych a vstr th = 
   590   let val L = S.free_vars_lr vstr
   591       val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   592       val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   593       val thm2 = forall_intr_list (map tych L) thm1
   594       val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   595   in refl RS
   596      rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3
   597   end;
   598 
   599 fun PGEN tych a vstr th = 
   600   let val a1 = tych a
   601       val vstr1 = tych vstr
   602   in
   603   forall_intr a1 
   604      (if (is_Free vstr) 
   605       then cterm_instantiate [(vstr1,a1)] th
   606       else VSTRUCT_ELIM tych a vstr th)
   607   end;
   608 
   609 
   610 (*---------------------------------------------------------------------------
   611  * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
   612  *
   613  *     (([x,y],N),vstr)
   614  *---------------------------------------------------------------------------*)
   615 fun dest_pbeta_redex M n = 
   616   let val (f,args) = dest_combn M n
   617       val dummy = dest_aabs f
   618   in (strip_aabs f,args)
   619   end;
   620 
   621 fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
   622 
   623 fun dest_impl tm = 
   624   let val ants = Logic.strip_imp_prems tm
   625       val eq = Logic.strip_imp_concl tm
   626   in (ants,get_lhs eq)
   627   end;
   628 
   629 fun restricted t = is_some (S.find_term
   630 			    (fn (Const("cut",_)) =>true | _ => false) 
   631 			    t)
   632 
   633 fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th =
   634  let val pbeta_reduce = simpl_conv ss [split RS eq_reflection];
   635      val tc_list = ref[]: term list ref
   636      val dummy = term_ref := []
   637      val dummy = thm_ref  := []
   638      val dummy = mss_ref  := []
   639      val cut_lemma' = (cut_lemma RS mp) RS eq_reflection
   640      fun prover mss thm =
   641      let fun cong_prover mss thm =
   642          let val dummy = say "cong_prover:\n"
   643              val cntxt = prems_of_mss mss
   644              val dummy = print_thms "cntxt:\n" cntxt
   645              val dummy = say "cong rule:\n"
   646              val dummy = say (string_of_thm thm^"\n")
   647              val dummy = thm_ref := (thm :: !thm_ref)
   648              val dummy = mss_ref := (mss :: !mss_ref)
   649              (* Unquantified eliminate *)
   650              fun uq_eliminate (thm,imp,sign) = 
   651                  let val tych = cterm_of sign
   652                      val dummy = print_cterms "To eliminate:\n" [tych imp]
   653                      val ants = map tych (Logic.strip_imp_prems imp)
   654                      val eq = Logic.strip_imp_concl imp
   655                      val lhs = tych(get_lhs eq)
   656                      val mss' = add_prems(mss, map ASSUME ants)
   657                      val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
   658                        handle _ => reflexive lhs
   659                      val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
   660                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   661                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   662                   in
   663                   lhs_eeq_lhs2 COMP thm
   664                   end
   665              fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
   666               let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)
   667                   val dummy = assert (forall (op aconv)
   668                                       (ListPair.zip (vlist, args)))
   669                                "assertion failed in CONTEXT_REWRITE_RULE"
   670                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
   671                                              imp_body
   672                   val tych = cterm_of sign
   673                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   674                   val eq1 = Logic.strip_imp_concl imp_body1
   675                   val Q = get_lhs eq1
   676                   val QeqQ1 = pbeta_reduce (tych Q)
   677                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   678                   val mss' = add_prems(mss, map ASSUME ants1)
   679                   val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
   680                                 handle _ => reflexive Q1
   681                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
   682                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   683                   val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
   684                   val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   685                   val QeeqQ3 = transitive thA Q2eeqQ3 handle _ =>
   686                                ((Q2eeqQ3 RS meta_eq_to_obj_eq) 
   687                                 RS ((thA RS meta_eq_to_obj_eq) RS trans))
   688                                 RS eq_reflection
   689                   val impth = implies_intr_list ants1 QeeqQ3
   690                   val impth1 = impth RS meta_eq_to_obj_eq
   691                   (* Need to abstract *)
   692                   val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   693               in ant_th COMP thm
   694               end
   695              fun q_eliminate (thm,imp,sign) =
   696               let val (vlist,imp_body) = strip_all imp
   697                   val (ants,Q) = dest_impl imp_body
   698               in if (pbeta_redex Q) (length vlist)
   699                  then pq_eliminate (thm,sign,vlist,imp_body,Q)
   700                  else 
   701                  let val tych = cterm_of sign
   702                      val ants1 = map tych ants
   703                      val mss' = add_prems(mss, map ASSUME ants1)
   704                      val Q_eeq_Q1 = rewrite_cterm(false,true) mss' 
   705                                                      prover (tych Q)
   706                       handle _ => reflexive (tych Q)
   707                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   708                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   709                      val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   710                  in
   711                  ant_th COMP thm
   712               end end
   713 
   714              fun eliminate thm = 
   715                case (rep_thm thm)
   716                of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
   717                    eliminate
   718                     (if not(is_all imp)
   719                      then uq_eliminate (thm,imp,sign)
   720                      else q_eliminate (thm,imp,sign))
   721                             (* Assume that the leading constant is ==,   *)
   722                 | _ => thm  (* if it is not a ==>                        *)
   723          in Some(eliminate (rename thm))
   724          end handle _ => None
   725 
   726         fun restrict_prover mss thm =
   727           let val dummy = say "restrict_prover:\n"
   728               val cntxt = rev(prems_of_mss mss)
   729               val dummy = print_thms "cntxt:\n" cntxt
   730               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   731                    sign,...} = rep_thm thm
   732               fun genl tm = let val vlist = gen_rems (op aconv)
   733                                            (add_term_frees(tm,[]), [func,R])
   734                             in U.itlist Forall vlist tm
   735                             end
   736               (*--------------------------------------------------------------
   737                * This actually isn't quite right, since it will think that
   738                * not-fully applied occs. of "f" in the context mean that the
   739                * current call is nested. The real solution is to pass in a
   740                * term "f v1..vn" which is a pattern that any full application
   741                * of "f" will match.
   742                *-------------------------------------------------------------*)
   743               val func_name = #1(dest_Const func)
   744               fun is_func (Const (name,_)) = (name = func_name)
   745 		| is_func _                = false
   746               val rcontext = rev cntxt
   747               val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   748               val antl = case rcontext of [] => [] 
   749                          | _   => [S.list_mk_conj(map cncl rcontext)]
   750               val TC = genl(S.list_mk_imp(antl, A))
   751               val dummy = print_cterms "func:\n" [cterm_of sign func]
   752               val dummy = print_cterms "TC:\n" 
   753 		              [cterm_of sign (HOLogic.mk_Trueprop TC)]
   754               val dummy = tc_list := (TC :: !tc_list)
   755               val nestedp = is_some (S.find_term is_func TC)
   756               val dummy = if nestedp then say"nested\n" else say"not_nested\n"
   757               val dummy = term_ref := ([func,TC]@(!term_ref))
   758               val th' = if nestedp then raise RULES_ERR{func = "solver", 
   759                                                       mesg = "nested function"}
   760                         else let val cTC = cterm_of sign 
   761 			                      (HOLogic.mk_Trueprop TC)
   762                              in case rcontext of
   763                                 [] => SPEC_ALL(ASSUME cTC)
   764                                | _ => MP (SPEC_ALL (ASSUME cTC)) 
   765                                          (LIST_CONJ rcontext)
   766                              end
   767               val th'' = th' RS thm
   768           in Some (th'')
   769           end handle _ => None
   770     in
   771     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
   772     end
   773     val ctm = cprop_of th
   774     val th1 = rewrite_cterm(false,true) (add_congs(mss_of [cut_lemma'], congs))
   775                             prover ctm
   776     val th2 = equal_elim th1 th
   777  in
   778  (th2, filter (not o restricted) (!tc_list))
   779  end;
   780 
   781 
   782 
   783 fun prove (ptm,tac) = 
   784     #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));
   785 
   786 
   787 end; (* Rules *)