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