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