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