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