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