more robust destruction of "set Collect" idiom
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03)
changeset 46102b669437de253
parent 46101 da17bfdadef6
child 46103 1e35730bd869
more robust destruction of "set Collect" idiom
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -1661,8 +1661,6 @@
     1.4            do_term depth Ts
     1.5                    (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
     1.6                     $ t1 $ incr_boundvars ~1 t2')
     1.7 -      | Const (@{const_name Set.member}, _) $ t1
     1.8 -        $ (Const (@{const_name Collect}, _) $ t2) => do_term depth Ts (t2 $ t1)
     1.9        | Const (x as (@{const_name distinct},
    1.10                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
    1.11          $ (t1 as _ $ _) =>
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jan 03 18:33:18 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jan 03 18:33:18 2012 +0100
     2.3 @@ -281,6 +281,16 @@
     2.4          Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
     2.5    in do_term [] [] Pos orig_t end
     2.6  
     2.7 +(** Destruction of set membership and comprehensions **)
     2.8 +
     2.9 +fun destroy_set_Collect (Const (@{const_name Set.member}, _) $ t1
    2.10 +                         $ (Const (@{const_name Collect}, _) $ t2)) =
    2.11 +    destroy_set_Collect (t2 $ t1)
    2.12 +  | destroy_set_Collect (t1 $ t2) =
    2.13 +    destroy_set_Collect t1 $ destroy_set_Collect t2
    2.14 +  | destroy_set_Collect (Abs (s, T, t')) = Abs (s, T, destroy_set_Collect t')
    2.15 +  | destroy_set_Collect t = t
    2.16 +
    2.17  (** Destruction of constructors **)
    2.18  
    2.19  val val_var_prefix = nitpick_prefix ^ "v"
    2.20 @@ -1268,8 +1278,9 @@
    2.21        #> box ? uncurry_term table
    2.22        #> box ? box_fun_and_pair_in_term hol_ctxt def
    2.23      fun do_tail def =
    2.24 -      destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
    2.25 -                         #> pull_out_existential_constrs hol_ctxt)
    2.26 +      destroy_set_Collect
    2.27 +      #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
    2.28 +                            #> pull_out_existential_constrs hol_ctxt)
    2.29        #> destroy_pulled_out_constrs hol_ctxt def destroy_constrs
    2.30        #> curry_assms
    2.31        #> destroy_universal_equalities