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