1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:12:45 2011 +0200
     1.3 @@ -23,6 +23,11 @@
     1.4      -> typ
     1.5    val is_type_surely_finite : Proof.context -> bool -> typ -> bool
     1.6    val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
     1.7 +  val s_not : term -> term
     1.8 +  val s_conj : term * term -> term
     1.9 +  val s_disj : term * term -> term
    1.10 +  val s_imp : term * term -> term
    1.11 +  val s_iff : term * term -> term
    1.12    val monomorphic_term : Type.tyenv -> term -> term
    1.13    val eta_expand : typ list -> term -> int -> term
    1.14    val transform_elim_prop : term -> term
    1.15 @@ -203,6 +208,34 @@
    1.16  fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
    1.17  fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
    1.18  
    1.19 +(* Simple simplifications to ensure that sort annotations don't leave a trail of
    1.20 +   spurious "True"s. *)
    1.21 +fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    1.22 +    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
    1.23 +  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    1.24 +    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
    1.25 +  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
    1.26 +  | s_not (@{const HOL.conj} $ t1 $ t2) =
    1.27 +    @{const HOL.disj} $ s_not t1 $ s_not t2
    1.28 +  | s_not (@{const HOL.disj} $ t1 $ t2) =
    1.29 +    @{const HOL.conj} $ s_not t1 $ s_not t2
    1.30 +  | s_not (@{const False}) = @{const True}
    1.31 +  | s_not (@{const True}) = @{const False}
    1.32 +  | s_not (@{const Not} $ t) = t
    1.33 +  | s_not t = @{const Not} $ t
    1.34 +fun s_conj (@{const True}, t2) = t2
    1.35 +  | s_conj (t1, @{const True}) = t1
    1.36 +  | s_conj p = HOLogic.mk_conj p
    1.37 +fun s_disj (@{const False}, t2) = t2
    1.38 +  | s_disj (t1, @{const False}) = t1
    1.39 +  | s_disj p = HOLogic.mk_disj p
    1.40 +fun s_imp (@{const True}, t2) = t2
    1.41 +  | s_imp (t1, @{const False}) = s_not t1
    1.42 +  | s_imp p = HOLogic.mk_imp p
    1.43 +fun s_iff (@{const True}, t2) = t2
    1.44 +  | s_iff (t1, @{const True}) = t1
    1.45 +  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    1.46 +
    1.47  fun monomorphic_term subst =
    1.48    map_types (map_type_tvar (fn v =>
    1.49        case Type.lookup subst v of