src/HOL/Import/shuffler.ML
author wenzelm
Mon Jul 12 20:21:39 2010 +0200 (2010-07-12)
changeset 37778 87b5dfe00387
parent 37146 f652333bbf8e
child 38549 d0385f2764d8
permissions -rw-r--r--
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
use up-to-date ML_Compiler.exn_message;
     1 (*  Title:      HOL/Import/shuffler.ML
     2     Author:     Sebastian Skalberg, TU Muenchen
     3 
     4 Package for proving two terms equal by normalizing (hence the
     5 "shuffler" name).  Uses the simplifier for the normalization.
     6 *)
     7 
     8 signature Shuffler =
     9 sig
    10     val debug      : bool Unsynchronized.ref
    11 
    12     val norm_term  : theory -> term -> thm
    13     val make_equal : theory -> term -> term -> thm option
    14     val set_prop   : theory -> term -> (string * thm) list -> (string * thm) option
    15 
    16     val find_potential: theory -> term -> (string * thm) list
    17 
    18     val gen_shuffle_tac: Proof.context -> bool -> (string * thm) list -> int -> tactic
    19     val shuffle_tac: Proof.context -> thm list -> int -> tactic
    20     val search_tac : Proof.context -> int -> tactic
    21 
    22     val print_shuffles: theory -> unit
    23 
    24     val add_shuffle_rule: thm -> theory -> theory
    25     val shuffle_attr: attribute
    26 
    27     val setup      : theory -> theory
    28 end
    29 
    30 structure Shuffler :> Shuffler =
    31 struct
    32 
    33 val debug = Unsynchronized.ref false
    34 
    35 fun if_debug f x = if !debug then f x else ()
    36 val message = if_debug writeln
    37 
    38 (*Prints exceptions readably to users*)
    39 fun print_sign_exn_unit sign e =
    40   case e of
    41      THM (msg,i,thms) =>
    42          (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    43           List.app (writeln o Display.string_of_thm_global sign) thms)
    44    | THEORY (msg,thys) =>
    45          (writeln ("Exception THEORY raised:\n" ^ msg);
    46           List.app (writeln o Context.str_of_thy) thys)
    47    | TERM (msg,ts) =>
    48          (writeln ("Exception TERM raised:\n" ^ msg);
    49           List.app (writeln o Syntax.string_of_term_global sign) ts)
    50    | TYPE (msg,Ts,ts) =>
    51          (writeln ("Exception TYPE raised:\n" ^ msg);
    52           List.app (writeln o Syntax.string_of_typ_global sign) Ts;
    53           List.app (writeln o Syntax.string_of_term_global sign) ts)
    54    | e => raise e
    55 
    56 (*Prints an exception, then fails*)
    57 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
    58 
    59 val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
    60 
    61 fun mk_meta_eq th =
    62     (case concl_of th of
    63          Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
    64        | Const("==",_) $ _ $ _ => th
    65        | _ => raise THM("Not an equality",0,[th]))
    66     handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
    67 
    68 fun mk_obj_eq th =
    69     (case concl_of th of
    70          Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
    71        | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
    72        | _ => raise THM("Not an equality",0,[th]))
    73     handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    74 
    75 structure ShuffleData = Theory_Data
    76 (
    77   type T = thm list
    78   val empty = []
    79   val extend = I
    80   val merge = Thm.merge_thms
    81 )
    82 
    83 fun print_shuffles thy =
    84   Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    85     (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
    86 
    87 val weaken =
    88     let
    89         val cert = cterm_of Pure.thy
    90         val P = Free("P",propT)
    91         val Q = Free("Q",propT)
    92         val PQ = Logic.mk_implies(P,Q)
    93         val PPQ = Logic.mk_implies(P,PQ)
    94         val cP = cert P
    95         val cQ = cert Q
    96         val cPQ = cert PQ
    97         val cPPQ = cert PPQ
    98         val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP]
    99         val th3 = Thm.assume cP
   100         val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3]
   101                                     |> implies_intr_list [cPPQ,cP]
   102     in
   103         Thm.equal_intr th4 th1 |> Drule.export_without_context
   104     end
   105 
   106 val imp_comm =
   107     let
   108         val cert = cterm_of Pure.thy
   109         val P = Free("P",propT)
   110         val Q = Free("Q",propT)
   111         val R = Free("R",propT)
   112         val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
   113         val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
   114         val cP = cert P
   115         val cQ = cert Q
   116         val cPQR = cert PQR
   117         val cQPR = cert QPR
   118         val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ]
   119                                     |> implies_intr_list [cPQR,cQ,cP]
   120         val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP]
   121                                     |> implies_intr_list [cQPR,cP,cQ]
   122     in
   123         Thm.equal_intr th1 th2 |> Drule.export_without_context
   124     end
   125 
   126 val def_norm =
   127     let
   128         val cert = cterm_of Pure.thy
   129         val aT = TFree("'a",[])
   130         val bT = TFree("'b",[])
   131         val v = Free("v",aT)
   132         val P = Free("P",aT-->bT)
   133         val Q = Free("Q",aT-->bT)
   134         val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
   135         val cPQ = cert (Logic.mk_equals(P,Q))
   136         val cv = cert v
   137         val rew = Thm.assume cvPQ
   138                          |> Thm.forall_elim cv
   139                          |> Thm.abstract_rule "v" cv
   140         val (lhs,rhs) = Logic.dest_equals(concl_of rew)
   141         val th1 = Thm.transitive (Thm.transitive
   142                                   (Thm.eta_conversion (cert lhs) |> Thm.symmetric)
   143                                   rew)
   144                              (Thm.eta_conversion (cert rhs))
   145                              |> Thm.implies_intr cvPQ
   146         val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv)
   147                               |> Thm.forall_intr cv
   148                               |> Thm.implies_intr cPQ
   149     in
   150         Thm.equal_intr th1 th2 |> Drule.export_without_context
   151     end
   152 
   153 val all_comm =
   154     let
   155         val cert = cterm_of Pure.thy
   156         val xT = TFree("'a",[])
   157         val yT = TFree("'b",[])
   158         val x = Free("x",xT)
   159         val y = Free("y",yT)
   160         val P = Free("P",xT-->yT-->propT)
   161         val lhs = Logic.all x (Logic.all y (P $ x $ y))
   162         val rhs = Logic.all y (Logic.all x (P $ x $ y))
   163         val cl = cert lhs
   164         val cr = cert rhs
   165         val cx = cert x
   166         val cy = cert y
   167         val th1 = Thm.assume cr
   168                          |> forall_elim_list [cy,cx]
   169                          |> forall_intr_list [cx,cy]
   170                          |> Thm.implies_intr cr
   171         val th2 = Thm.assume cl
   172                          |> forall_elim_list [cx,cy]
   173                          |> forall_intr_list [cy,cx]
   174                          |> Thm.implies_intr cl
   175     in
   176         Thm.equal_intr th1 th2 |> Drule.export_without_context
   177     end
   178 
   179 val equiv_comm =
   180     let
   181         val cert = cterm_of Pure.thy
   182         val T    = TFree("'a",[])
   183         val t    = Free("t",T)
   184         val u    = Free("u",T)
   185         val ctu  = cert (Logic.mk_equals(t,u))
   186         val cut  = cert (Logic.mk_equals(u,t))
   187         val th1  = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu
   188         val th2  = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut
   189     in
   190         Thm.equal_intr th1 th2 |> Drule.export_without_context
   191     end
   192 
   193 (* This simplification procedure rewrites !!x y. P x y
   194 deterministicly, in order for the normalization function, defined
   195 below, to handle nested quantifiers robustly *)
   196 
   197 local
   198 
   199 exception RESULT of int
   200 
   201 fun find_bound n (Bound i) = if i = n then raise RESULT 0
   202                              else if i = n+1 then raise RESULT 1
   203                              else ()
   204   | find_bound n (t $ u) = (find_bound n t; find_bound n u)
   205   | find_bound n (Abs(_,_,t)) = find_bound (n+1) t
   206   | find_bound _ _ = ()
   207 
   208 fun swap_bound n (Bound i) = if i = n then Bound (n+1)
   209                              else if i = n+1 then Bound n
   210                              else Bound i
   211   | swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u)
   212   | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
   213   | swap_bound n t = t
   214 
   215 fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
   216     let
   217         val lhs = list_all ([xv,yv],t)
   218         val rhs = list_all ([yv,xv],swap_bound 0 t)
   219         val rew = Logic.mk_equals (lhs,rhs)
   220         val init = Thm.trivial (cterm_of thy rew)
   221     in
   222         all_comm RS init
   223     end
   224 
   225 fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
   226     let
   227         val res = (find_bound 0 body;2) handle RESULT i => i
   228     in
   229         case res of
   230             0 => SOME (rew_th thy (x,xT) (y,yT) body)
   231           | 1 => if string_ord(y,x) = LESS
   232                  then
   233                      let
   234                          val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
   235                          val t_th    = Thm.reflexive (cterm_of thy t)
   236                          val newt_th = Thm.reflexive (cterm_of thy newt)
   237                      in
   238                          SOME (Thm.transitive t_th newt_th)
   239                      end
   240                  else NONE
   241           | _ => error "norm_term (quant_rewrite) internal error"
   242      end
   243   | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
   244 
   245 fun freeze_thaw_term t =
   246     let
   247         val tvars = OldTerm.term_tvars t
   248         val tfree_names = OldTerm.add_term_tfree_names(t,[])
   249         val (type_inst,_) =
   250             fold (fn (w as (v,_), S) => fn (inst, used) =>
   251                       let
   252                           val v' = Name.variant used v
   253                       in
   254                           ((w,TFree(v',S))::inst,v'::used)
   255                       end)
   256                   tvars ([], tfree_names)
   257         val t' = subst_TVars type_inst t
   258     in
   259         (t', map (fn (w,TFree(v,S)) => (v,TVar(w,S))
   260                   | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
   261     end
   262 
   263 fun inst_tfrees thy [] thm = thm
   264   | inst_tfrees thy ((name,U)::rest) thm =
   265     let
   266         val cU = ctyp_of thy U
   267         val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
   268         val (rens, thm') = Thm.varifyT_global'
   269     (remove (op = o apsnd fst) name tfrees) thm
   270         val mid =
   271             case rens of
   272                 [] => thm'
   273               | [((_, S), idx)] => instantiate
   274             ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
   275               | _ => error "Shuffler.inst_tfrees internal error"
   276     in
   277         inst_tfrees thy rest mid
   278     end
   279 
   280 fun is_Abs (Abs _) = true
   281   | is_Abs _ = false
   282 
   283 fun eta_redex (t $ Bound 0) =
   284     let
   285         fun free n (Bound i) = i = n
   286           | free n (t $ u) = free n t orelse free n u
   287           | free n (Abs(_,_,t)) = free (n+1) t
   288           | free n _ = false
   289     in
   290         not (free 0 t)
   291     end
   292   | eta_redex _ = false
   293 
   294 fun eta_contract thy assumes origt =
   295     let
   296         val (typet,Tinst) = freeze_thaw_term origt
   297         val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
   298         val final = inst_tfrees thy Tinst o thaw
   299         val t = #1 (Logic.dest_equals (prop_of init))
   300         val _ =
   301             let
   302                 val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   303             in
   304                 if not (lhs aconv origt)
   305                 then
   306                   writeln (cat_lines
   307                     (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
   308                       Syntax.string_of_term_global thy origt,
   309                       Syntax.string_of_term_global thy lhs,
   310                       Syntax.string_of_term_global thy typet,
   311                       Syntax.string_of_term_global thy t] @
   312                       map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
   313                 else ()
   314             end
   315     in
   316         case t of
   317             Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
   318             (if eta_redex P andalso eta_redex Q
   319               then
   320                   let
   321                       val cert = cterm_of thy
   322                       val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
   323                       val cv = cert v
   324                       val ct = cert t
   325                       val th = (Thm.assume ct)
   326                                    |> Thm.forall_elim cv
   327                                    |> Thm.abstract_rule x cv
   328                       val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P)))
   329                       val th' = Thm.transitive (Thm.symmetric ext_th) th
   330                       val cu = cert (prop_of th')
   331                       val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv)
   332                       val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v)))
   333                                      |> Thm.transitive uth
   334                                      |> Thm.forall_intr cv
   335                                      |> Thm.implies_intr cu
   336                       val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth'
   337                       val res = final rew_th
   338                       val lhs = (#1 (Logic.dest_equals (prop_of res)))
   339                   in
   340                        SOME res
   341                   end
   342               else NONE)
   343           | _ => NONE
   344        end
   345 
   346 fun beta_fun thy assume t =
   347     SOME (Thm.beta_conversion true (cterm_of thy t))
   348 
   349 val meta_sym_rew = thm "refl"
   350 
   351 fun equals_fun thy assume t =
   352     case t of
   353         Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
   354       | _ => NONE
   355 
   356 fun eta_expand thy assumes origt =
   357     let
   358         val (typet,Tinst) = freeze_thaw_term origt
   359         val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
   360         val final = inst_tfrees thy Tinst o thaw
   361         val t = #1 (Logic.dest_equals (prop_of init))
   362         val _ =
   363             let
   364                 val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   365             in
   366                 if not (lhs aconv origt)
   367                 then
   368                   writeln (cat_lines
   369                     (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
   370                       Syntax.string_of_term_global thy origt,
   371                       Syntax.string_of_term_global thy lhs,
   372                       Syntax.string_of_term_global thy typet,
   373                       Syntax.string_of_term_global thy t] @
   374                       map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
   375                 else ()
   376             end
   377     in
   378         case t of
   379             Const("==",T) $ P $ Q =>
   380             if is_Abs P orelse is_Abs Q
   381             then (case domain_type T of
   382                       Type("fun",[aT,bT]) =>
   383                       let
   384                           val cert = cterm_of thy
   385                           val vname = Name.variant (Term.add_free_names t []) "v"
   386                           val v = Free(vname,aT)
   387                           val cv = cert v
   388                           val ct = cert t
   389                           val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv))
   390                                         |> Thm.forall_intr cv
   391                                         |> Thm.implies_intr ct
   392                           val concl = cert (concl_of th1)
   393                           val th2 = (Thm.assume concl)
   394                                         |> Thm.forall_elim cv
   395                                         |> Thm.abstract_rule vname cv
   396                           val (lhs,rhs) = Logic.dest_equals (prop_of th2)
   397                           val elhs = Thm.eta_conversion (cert lhs)
   398                           val erhs = Thm.eta_conversion (cert rhs)
   399                           val th2' = Thm.transitive
   400                                          (Thm.transitive (Thm.symmetric elhs) th2)
   401                                          erhs
   402                           val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl)
   403                           val res' = final res
   404                       in
   405                           SOME res'
   406                       end
   407                     | _ => NONE)
   408             else NONE
   409           | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
   410     end;
   411 
   412 fun mk_tfree s = TFree("'"^s,[])
   413 fun mk_free s t = Free (s,t)
   414 val xT = mk_tfree "a"
   415 val yT = mk_tfree "b"
   416 val x = Free ("x", xT)
   417 val y = Free ("y", yT)
   418 val P  = mk_free "P" (xT-->yT-->propT)
   419 val Q  = mk_free "Q" (xT-->yT)
   420 val R  = mk_free "R" (xT-->yT)
   421 val S  = mk_free "S" xT
   422 val S'  = mk_free "S'" xT
   423 in
   424 fun beta_simproc thy = Simplifier.simproc_i
   425                       thy
   426                       "Beta-contraction"
   427                       [Abs("x",xT,Q) $ S]
   428                       beta_fun
   429 
   430 fun equals_simproc thy = Simplifier.simproc_i
   431                       thy
   432                       "Ordered rewriting of meta equalities"
   433                       [Const("op ==",xT) $ S $ S']
   434                       equals_fun
   435 
   436 fun quant_simproc thy = Simplifier.simproc_i
   437                            thy
   438                            "Ordered rewriting of nested quantifiers"
   439                            [Logic.all x (Logic.all y (P $ x $ y))]
   440                            quant_rewrite
   441 fun eta_expand_simproc thy = Simplifier.simproc_i
   442                          thy
   443                          "Smart eta-expansion by equivalences"
   444                          [Logic.mk_equals(Q,R)]
   445                          eta_expand
   446 fun eta_contract_simproc thy = Simplifier.simproc_i
   447                          thy
   448                          "Smart handling of eta-contractions"
   449                          [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
   450                          eta_contract
   451 end
   452 
   453 (* Disambiguates the names of bound variables in a term, returning t
   454 == t' where all the names of bound variables in t' are unique *)
   455 
   456 fun disamb_bound thy t =
   457     let
   458 
   459         fun F (t $ u,idx) =
   460             let
   461                 val (t',idx') = F (t,idx)
   462                 val (u',idx'') = F (u,idx')
   463             in
   464                 (t' $ u',idx'')
   465             end
   466           | F (Abs(x,xT,t),idx) =
   467             let
   468                 val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
   469                 val (t',idx') = F (t,idx+1)
   470             in
   471                 (Abs(x',xT,t'),idx')
   472             end
   473           | F arg = arg
   474         val (t',_) = F (t,0)
   475         val ct = cterm_of thy t
   476         val ct' = cterm_of thy t'
   477         val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct')
   478         val _ = message ("disamb_term: " ^ (string_of_thm res))
   479     in
   480         res
   481     end
   482 
   483 (* Transforms a term t to some normal form t', returning the theorem t
   484 == t'.  This is originally a help function for make_equal, but might
   485 be handy in its own right, for example for indexing terms. *)
   486 
   487 fun norm_term thy t =
   488     let
   489         val norms = ShuffleData.get thy
   490         val ss = Simplifier.global_context thy empty_ss
   491           setmksimps (K single)
   492           addsimps (map (Thm.transfer thy) norms)
   493           addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
   494         fun chain f th =
   495             let
   496                 val rhs = Thm.rhs_of th
   497             in
   498                 Thm.transitive th (f rhs)
   499             end
   500         val th =
   501             t |> disamb_bound thy
   502               |> chain (Simplifier.full_rewrite ss)
   503               |> chain Thm.eta_conversion
   504               |> Thm.strip_shyps
   505         val _ = message ("norm_term: " ^ (string_of_thm th))
   506     in
   507         th
   508     end
   509     handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
   510 
   511 
   512 (* Closes a theorem with respect to free and schematic variables (does
   513 not touch type variables, though). *)
   514 
   515 fun close_thm th =
   516     let
   517         val thy = Thm.theory_of_thm th
   518         val c = prop_of th
   519         val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
   520     in
   521         Drule.forall_intr_list (map (cterm_of thy) vars) th
   522     end
   523 
   524 
   525 (* Normalizes a theorem's conclusion using norm_term. *)
   526 
   527 fun norm_thm thy th =
   528     let
   529         val c = prop_of th
   530     in
   531         Thm.equal_elim (norm_term thy c) th
   532     end
   533 
   534 (* make_equal thy t u tries to construct the theorem t == u under the
   535 signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
   536 NONE is returned. *)
   537 
   538 fun make_equal thy t u =
   539     let
   540         val t_is_t' = norm_term thy t
   541         val u_is_u' = norm_term thy u
   542         val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u')
   543         val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   544     in
   545         SOME th
   546     end
   547     handle e as THM _ => (message "make_equal: NONE";NONE)
   548 
   549 fun match_consts ignore t (* th *) =
   550     let
   551         fun add_consts (Const (c, _), cs) =
   552             if member (op =) ignore c
   553             then cs
   554             else insert (op =) c cs
   555           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
   556           | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
   557           | add_consts (_, cs) = cs
   558         val t_consts = add_consts(t,[])
   559     in
   560      fn (name,th) =>
   561         let
   562             val th_consts = add_consts(prop_of th,[])
   563         in
   564             eq_set (op =) (t_consts, th_consts)
   565         end
   566     end
   567 
   568 val collect_ignored = fold_rev (fn thm => fn cs =>
   569   let
   570     val (lhs, rhs) = Logic.dest_equals (prop_of thm);
   571     val consts_lhs = Term.add_const_names lhs [];
   572     val consts_rhs = Term.add_const_names rhs [];
   573     val ignore_lhs = subtract (op =) consts_rhs consts_lhs;
   574     val ignore_rhs = subtract (op =) consts_lhs consts_rhs;
   575   in
   576     fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
   577   end)
   578 
   579 (* set_prop t thms tries to make a theorem with the proposition t from
   580 one of the theorems thms, by shuffling the propositions around.  If it
   581 succeeds, SOME theorem is returned, otherwise NONE.  *)
   582 
   583 fun set_prop thy t =
   584     let
   585         val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
   586         val closed_t = fold_rev Logic.all vars t
   587         val rew_th = norm_term thy closed_t
   588         val rhs = Thm.rhs_of rew_th
   589 
   590         val shuffles = ShuffleData.get thy
   591         fun process [] = NONE
   592           | process ((name,th)::thms) =
   593             let
   594                 val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
   595                 val triv_th = Thm.trivial rhs
   596                 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   597                 val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   598                                  SOME(th,_) => SOME th
   599                                | NONE => NONE
   600             in
   601                 case mod_th of
   602                     SOME mod_th =>
   603                     let
   604                         val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th
   605                     in
   606                         message ("Shuffler.set_prop succeeded by " ^ name);
   607                         SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
   608                     end
   609                   | NONE => process thms
   610             end
   611             handle e as THM _ => process thms
   612     in
   613         fn thms =>
   614            case process thms of
   615                res as SOME (name,th) => if (prop_of th) aconv t
   616                                         then res
   617                                         else error "Internal error in set_prop"
   618              | NONE => NONE
   619     end
   620 
   621 fun find_potential thy t =
   622     let
   623         val shuffles = ShuffleData.get thy
   624         val ignored = collect_ignored shuffles []
   625         val all_thms =
   626           map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
   627     in
   628         filter (match_consts ignored t) all_thms
   629     end
   630 
   631 fun gen_shuffle_tac ctxt search thms i st =
   632     let
   633         val thy = ProofContext.theory_of ctxt
   634         val _ = message ("Shuffling " ^ (string_of_thm st))
   635         val t = List.nth(prems_of st,i-1)
   636         val set = set_prop thy t
   637         fun process_tac thms st =
   638             case set thms of
   639                 SOME (_,th) => Seq.of_list (compose (th,i,st))
   640               | NONE => Seq.empty
   641     in
   642         (process_tac thms APPEND (if search
   643                                   then process_tac (find_potential thy t)
   644                                   else no_tac)) st
   645     end
   646 
   647 fun shuffle_tac ctxt thms =
   648   gen_shuffle_tac ctxt false (map (pair "") thms);
   649 
   650 fun search_tac ctxt =
   651   gen_shuffle_tac ctxt true (map (pair "premise") (Assumption.all_prems_of ctxt));
   652 
   653 fun add_shuffle_rule thm thy =
   654     let
   655         val shuffles = ShuffleData.get thy
   656     in
   657         if exists (curry Thm.eq_thm thm) shuffles
   658         then (warning ((string_of_thm thm) ^ " already known to the shuffler");
   659               thy)
   660         else ShuffleData.put (thm::shuffles) thy
   661     end
   662 
   663 val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
   664 
   665 val setup =
   666   Method.setup @{binding shuffle_tac}
   667     (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt ths)))
   668     "solve goal by shuffling terms around" #>
   669   Method.setup @{binding search_tac}
   670     (Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #>
   671   add_shuffle_rule weaken #>
   672   add_shuffle_rule equiv_comm #>
   673   add_shuffle_rule imp_comm #>
   674   add_shuffle_rule Drule.norm_hhf_eq #>
   675   add_shuffle_rule Drule.triv_forall_equality #>
   676   Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
   677 
   678 end