optimized multisets in Nitpick by fishing "finite"
authorblanchet
Tue Feb 23 14:50:44 2010 +0100 (2010-02-23)
changeset 3533222442ab3e7a3
parent 35331 450ab945c451
child 35333 f61de25f71f9
optimized multisets in Nitpick by fishing "finite"
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 14:11:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 14:50:44 2010 +0100
     1.3 @@ -619,12 +619,19 @@
     1.4  fun is_univ_typedef thy (Type (s, _)) =
     1.5      (case typedef_info thy s of
     1.6         SOME {set_def, prop_of_Rep, ...} =>
     1.7 -       (case set_def of
     1.8 -          SOME thm =>
     1.9 -          try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
    1.10 -        | NONE =>
    1.11 -          try (fst o dest_Const o snd o HOLogic.dest_mem
    1.12 -               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
    1.13 +       let
    1.14 +         val t_opt =
    1.15 +           case set_def of
    1.16 +             SOME thm => try (snd o Logic.dest_equals o prop_of) thm
    1.17 +           | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
    1.18 +                         prop_of_Rep
    1.19 +       in
    1.20 +         case t_opt of
    1.21 +           SOME (Const (@{const_name top}, _)) => true
    1.22 +         | SOME (Const (@{const_name Collect}, _)
    1.23 +                 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
    1.24 +         | _ => false
    1.25 +       end
    1.26       | NONE => false)
    1.27    | is_univ_typedef _ _ = false
    1.28  (* theory -> (typ option * bool) list -> typ -> bool *)