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