# HG changeset patch # User blanchet # Date 1291719361 -3600 # Node ID f2e94005d28346afa44133e9f0aa94fd8f72fb8b # Parent 2a41709f34c1960c67b23e06822bd5c7dcc9bc8c fix special handling of set products diff -r 2a41709f34c1 -r f2e94005d283 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Nitpick.thy Tue Dec 07 11:56:01 2010 +0100 @@ -76,6 +76,9 @@ "tranclp r a b \ trancl (split r) (a, b)" by (simp add: trancl_def Collect_def mem_def) +definition prod :: "'a set \ 'b set \ ('a \ 'b) set" where +"prod A B = {(a, b). a \ A \ b \ B}" + definition refl' :: "('a \ 'a \ bool) \ bool" where "refl' r \ \x. (x, x) \ r" @@ -237,18 +240,18 @@ setup {* Nitpick_Isar.setup *} hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The - FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' - fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac - one_frac num denom norm_frac frac plus_frac times_frac uminus_frac + FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' + setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac + zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac less_frac less_eq_frac of_frac hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit word -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def - wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def - The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def - nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def - num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def - uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def - less_eq_frac_def of_frac_def +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def + refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def + fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def + list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def + zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def + plus_frac_def times_frac_def uminus_frac_def number_of_frac_def + inverse_frac_def less_frac_def less_eq_frac_def of_frac_def end diff -r 2a41709f34c1 -r f2e94005d283 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Dec 07 11:56:01 2010 +0100 @@ -424,6 +424,7 @@ (@{const_name converse}, 1), (@{const_name trancl}, 1), (@{const_name rel_comp}, 2), + (@{const_name prod}, 2), (@{const_name image}, 2), (@{const_name finite}, 1), (@{const_name unknown}, 0), @@ -1645,9 +1646,14 @@ s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)) | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 => do_const depth Ts t (@{const_name refl'}, range_type T) [t2] - | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) => - s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts, - map (do_term depth Ts) [t1, t2]) + | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])]))) + $ t1 $ (t2 as Abs (_, _, t2')) => + if loose_bvar1 (t2', 0) then + s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2]) + else + do_term depth Ts + (Const (@{const_name prod}, T1 --> range_type T2 --> T3) + $ t1 $ incr_boundvars ~1 t2') | Const (x as (@{const_name distinct}, Type (@{type_name fun}, [Type (@{type_name list}, [T']), _]))) $ (t1 as _ $ _) => diff -r 2a41709f34c1 -r f2e94005d283 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Dec 07 11:56:01 2010 +0100 @@ -528,8 +528,8 @@ Op1 (Closure, range_type T, Any, sub t1) | (Const (@{const_name rel_comp}, T), [t1, t2]) => Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) - | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) => - Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2') + | (Const (@{const_name prod}, T), [t1, t2]) => + Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (@{const_name image}, T), [t1, t2]) => Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (x as (s as @{const_name Suc}, T)), []) =>