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