introduced hack to exploit the symmetry of equality in monotonicity calculus
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 41016343cdf923c02
parent 41015 3eeb25d953d2
child 41017 666d8ed0b73a
introduced hack to exploit the symmetry of equality in monotonicity calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -852,6 +852,10 @@
     1.4           (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
     1.5         | @{const True} =>
     1.6           (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
     1.7 +       | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
     1.8 +         (* hack to exploit symmetry of equality when typing "insert" *)
     1.9 +         (if t2 = Bound 0 then do_term @{term True}
    1.10 +          else do_term (t0 $ t2 $ Bound 0)) accum
    1.11         | Const (x as (s, T)) =>
    1.12           (case AList.lookup (op =) consts x of
    1.13              SOME M => (M, accum)