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