don't apply "ext_cong_neq" to biimplications
authorblanchet
Tue May 22 16:59:27 2012 +0200 (2012-05-22)
changeset 479562a420750248b
parent 47955 a2a821abab83
child 47957 d2bdd85ee23c
don't apply "ext_cong_neq" to biimplications
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -574,7 +574,7 @@
     1.4  
     1.5  exception NO_F_PATTERN of unit
     1.6  
     1.7 -fun get_F_pattern t u =
     1.8 +fun get_F_pattern T t u =
     1.9    let
    1.10      fun pat t u =
    1.11        let
    1.12 @@ -593,11 +593,13 @@
    1.13            end
    1.14        end
    1.15    in
    1.16 -    (case pat t u of
    1.17 -       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
    1.18 -     | _ => NONE)
    1.19 -    handle NO_F_PATTERN () => NONE
    1.20 +    if T = @{typ bool} then
    1.21 +      NONE
    1.22 +    else case pat t u of
    1.23 +      (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
    1.24 +    | _ => NONE
    1.25    end
    1.26 +  handle NO_F_PATTERN () => NONE
    1.27  
    1.28  val ext_cong_neq = @{thm ext_cong_neq}
    1.29  val F_ext_cong_neq =
    1.30 @@ -608,9 +610,10 @@
    1.31  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    1.32  fun cong_extensionalize_thm thy th =
    1.33    case concl_of th of
    1.34 -    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    1.35 -                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    1.36 -    (case get_F_pattern t u of
    1.37 +    @{const Trueprop} $ (@{const Not}
    1.38 +        $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    1.39 +           $ (t as _ $ _) $ (u as _ $ _))) =>
    1.40 +    (case get_F_pattern T t u of
    1.41         SOME p =>
    1.42         let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
    1.43           th RS cterm_instantiate inst ext_cong_neq