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