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