1.1 --- a/src/HOL/Nitpick.thy	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -76,6 +76,9 @@
     1.4  "tranclp r a b \<equiv> trancl (split r) (a, b)"
     1.5  by (simp add: trancl_def Collect_def mem_def)
     1.6  
     1.7 +definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
     1.8 +"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
     1.9 +
    1.10  definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.11  "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
    1.12  
    1.13 @@ -237,18 +240,18 @@
    1.14  setup {* Nitpick_Isar.setup *}
    1.15  
    1.16  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.17 -    FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.18 -    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.19 -    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.20 +    FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card'
    1.21 +    setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.22 +    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.23      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.24  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.25      word
    1.26 -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.27 -    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.28 -    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    1.29 -    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.30 -    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    1.31 -    uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
    1.32 -    less_eq_frac_def of_frac_def
    1.33 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
    1.34 +    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.35 +    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    1.36 +    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.37 +    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.38 +    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.39 +    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    1.40  
    1.41  end

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     2.3 @@ -424,6 +424,7 @@
     2.4     (@{const_name converse}, 1),
     2.5     (@{const_name trancl}, 1),
     2.6     (@{const_name rel_comp}, 2),
     2.7 +   (@{const_name prod}, 2),
     2.8     (@{const_name image}, 2),
     2.9     (@{const_name finite}, 1),
    2.10     (@{const_name unknown}, 0),
    2.11 @@ -1645,9 +1646,14 @@
    2.12                  s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
    2.13        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
    2.14          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
    2.15 -      | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
    2.16 -        s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
    2.17 -                        map (do_term depth Ts) [t1, t2])
    2.18 +      | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
    2.19 +        $ t1 $ (t2 as Abs (_, _, t2')) =>
    2.20 +        if loose_bvar1 (t2', 0) then
    2.21 +          s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
    2.22 +        else
    2.23 +          do_term depth Ts
    2.24 +                  (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
    2.25 +                   $ t1 $ incr_boundvars ~1 t2')
    2.26        | Const (x as (@{const_name distinct},
    2.27                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
    2.28          $ (t1 as _ $ _) =>

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     3.3 @@ -528,8 +528,8 @@
     3.4            Op1 (Closure, range_type T, Any, sub t1)
     3.5          | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
     3.6            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
     3.7 -        | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
     3.8 -          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
     3.9 +        | (Const (@{const_name prod}, T), [t1, t2]) =>
    3.10 +          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2)
    3.11          | (Const (@{const_name image}, T), [t1, t2]) =>
    3.12            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    3.13          | (Const (x as (s as @{const_name Suc}, T)), []) =>