src/HOL/Import/shuffler.ML
changeset 17188 a26a4fc323ed
parent 16428 d2203a276b07
child 17440 df77edc4f5d0
     1.1 --- a/src/HOL/Import/shuffler.ML	Mon Aug 29 16:25:24 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Aug 29 16:51:39 2005 +0200
     1.3 @@ -350,6 +350,13 @@
     1.4  fun beta_fun sg assume t =
     1.5      SOME (beta_conversion true (cterm_of sg t))
     1.6  
     1.7 +val meta_sym_rew = thm "refl"
     1.8 +
     1.9 +fun equals_fun sg assume t =
    1.10 +    case t of
    1.11 +	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
    1.12 +      | _ => NONE
    1.13 +
    1.14  fun eta_expand sg assumes origt =
    1.15      let
    1.16  	val (typet,Tinst) = freeze_thaw_term origt
    1.17 @@ -413,6 +420,7 @@
    1.18  val Q  = Var(("Q",0),xT-->yT)
    1.19  val R  = Var(("R",0),xT-->yT)
    1.20  val S  = Var(("S",0),xT)
    1.21 +val S'  = Var(("S'",0),xT)
    1.22  in
    1.23  fun beta_simproc sg = Simplifier.simproc_i
    1.24  		      sg
    1.25 @@ -420,6 +428,12 @@
    1.26  		      [Abs("x",xT,Q) $ S]
    1.27  		      beta_fun
    1.28  
    1.29 +fun equals_simproc sg = Simplifier.simproc_i
    1.30 +		      sg
    1.31 +		      "Ordered rewriting of meta equalities"
    1.32 +		      [Const("op ==",xT) $ S $ S']
    1.33 +		      equals_fun
    1.34 +
    1.35  fun quant_simproc sg = Simplifier.simproc_i
    1.36  			   sg
    1.37  			   "Ordered rewriting of nested quantifiers"
    1.38 @@ -584,7 +598,7 @@
    1.39  		val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
    1.40  		val triv_th = trivial rhs
    1.41  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
    1.42 -		val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of
    1.43 +		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
    1.44  				 SOME(th,_) => SOME th
    1.45  			       | NONE => NONE
    1.46  	    in