1.1 --- a/src/HOL/Nitpick.thy Sat Jul 03 00:49:12 2010 +0200
1.2 +++ b/src/HOL/Nitpick.thy Sat Jul 03 00:50:35 2010 +0200
1.3 @@ -69,9 +69,6 @@
1.4 apply (erule_tac x = y in allE)
1.5 by (auto simp: mem_def)
1.6
1.7 -lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
1.8 -by (simp add: prod_case_unfold split_def)
1.9 -
1.10 lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
1.11 by simp
1.12
1.13 @@ -252,12 +249,12 @@
1.14 less_frac less_eq_frac of_frac
1.15 hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
1.16 word
1.17 -hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
1.18 - refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
1.19 - fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
1.20 - list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
1.21 - zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
1.22 - plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
1.23 - inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
1.24 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
1.25 + wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
1.26 + The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
1.27 + nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
1.28 + num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
1.29 + uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
1.30 + less_eq_frac_def of_frac_def
1.31
1.32 end
2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Jul 03 00:49:12 2010 +0200
2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Jul 03 00:50:35 2010 +0200
2.3 @@ -17,11 +17,11 @@
2.4 subsection {* Curry in a Hurry *}
2.5
2.6 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
2.7 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
2.8 +nitpick [card = 1\<midarrow>12, expect = none]
2.9 by auto
2.10
2.11 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
2.12 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
2.13 +nitpick [card = 1\<midarrow>12, expect = none]
2.14 by auto
2.15
2.16 lemma "split (curry f) = f"
2.17 @@ -61,12 +61,12 @@
2.18 by auto
2.19
2.20 lemma "split o curry = (\<lambda>x. x)"
2.21 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
2.22 +nitpick [card = 1\<midarrow>12, expect = none]
2.23 apply (rule ext)+
2.24 by auto
2.25
2.26 lemma "curry o split = (\<lambda>x. x)"
2.27 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
2.28 +nitpick [card = 1\<midarrow>12, expect = none]
2.29 apply (rule ext)+
2.30 by auto
2.31
3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Jul 03 00:49:12 2010 +0200
3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Jul 03 00:50:35 2010 +0200
3.3 @@ -69,7 +69,7 @@
3.4 oops
3.5
3.6 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
3.7 -nitpick [card = 1\<midarrow>9, expect = unknown (*none*)]
3.8 +nitpick [card = 1\<midarrow>9, expect = none]
3.9 sorry
3.10
3.11 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
4.1 --- a/src/HOL/Product_Type.thy Sat Jul 03 00:49:12 2010 +0200
4.2 +++ b/src/HOL/Product_Type.thy Sat Jul 03 00:50:35 2010 +0200
4.3 @@ -158,6 +158,8 @@
4.4 by (simp add: Pair_def Abs_prod_inject)
4.5 qed
4.6
4.7 +declare prod.simps(2) [nitpick_simp del]
4.8 +
4.9 declare weak_case_cong [cong del]
4.10
4.11
4.12 @@ -391,7 +393,7 @@
4.13 code_const fst and snd
4.14 (Haskell "fst" and "snd")
4.15
4.16 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
4.17 +lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
4.18 by (simp add: expand_fun_eq split: prod.split)
4.19
4.20 lemma fst_eqD: "fst (x, y) = a ==> x = a"
5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 03 00:49:12 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 03 00:50:35 2010 +0200
5.3 @@ -876,6 +876,20 @@
5.4 "") ^ "."
5.5 end
5.6
5.7 + val (skipped, the_scopes) =
5.8 + all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
5.9 + bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
5.10 + finitizable_dataTs
5.11 + val _ = if skipped > 0 then
5.12 + print_m (fn () => "Too many scopes. Skipping " ^
5.13 + string_of_int skipped ^ " scope" ^
5.14 + plural_s skipped ^
5.15 + ". (Consider using \"mono\" or \
5.16 + \\"merge_type_vars\" to prevent this.)")
5.17 + else
5.18 + ()
5.19 + val _ = scopes := the_scopes
5.20 +
5.21 fun run_batches _ _ []
5.22 (found_really_genuine, max_potential, max_genuine, donno) =
5.23 if donno > 0 andalso max_genuine > 0 then
5.24 @@ -888,7 +902,7 @@
5.25 " This suggests that the induction hypothesis might be \
5.26 \general enough to prove this subgoal."
5.27 else
5.28 - "")); "none")
5.29 + "")); if skipped > 0 then "unknown" else "none")
5.30 else
5.31 (print_m (fn () =>
5.32 "Nitpick could not find a" ^
5.33 @@ -903,20 +917,6 @@
5.34 run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
5.35 end
5.36
5.37 - val (skipped, the_scopes) =
5.38 - all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
5.39 - bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
5.40 - finitizable_dataTs
5.41 - val _ = if skipped > 0 then
5.42 - print_m (fn () => "Too many scopes. Skipping " ^
5.43 - string_of_int skipped ^ " scope" ^
5.44 - plural_s skipped ^
5.45 - ". (Consider using \"mono\" or \
5.46 - \\"merge_type_vars\" to prevent this.)")
5.47 - else
5.48 - ()
5.49 - val _ = scopes := the_scopes
5.50 -
5.51 val batches = batch_list batch_size (!scopes)
5.52 val outcome_code =
5.53 (run_batches 0 (length batches) batches
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jul 03 00:49:12 2010 +0200
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jul 03 00:50:35 2010 +0200
6.3 @@ -628,7 +628,9 @@
6.4 end
6.5 and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
6.6 cset)) =
6.7 - (case t of
6.8 + (print_g (fn () => " \<Gamma> \<turnstile> " ^
6.9 + Syntax.string_of_term ctxt t ^ " : _?");
6.10 + case t of
6.11 Const (x as (s, T)) =>
6.12 (case AList.lookup (op =) consts x of
6.13 SOME M => (M, accum)
6.14 @@ -846,48 +848,54 @@
6.15 Plus => do_term t accum
6.16 | Minus => consider_general_equals mdata false x t1 t2 accum
6.17 in
6.18 - case t of
6.19 - Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
6.20 - do_quantifier x s1 T1 t1
6.21 - | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
6.22 - | @{const Trueprop} $ t1 =>
6.23 - let val (m1, accum) = do_formula sn t1 accum in
6.24 - (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
6.25 - m1), accum)
6.26 - end
6.27 - | @{const Not} $ t1 =>
6.28 - let val (m1, accum) = do_formula (negate sn) t1 accum in
6.29 - (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
6.30 - accum)
6.31 - end
6.32 - | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
6.33 - do_quantifier x s1 T1 t1
6.34 - | Const (x0 as (s0 as @{const_name Ex}, T0))
6.35 - $ (t1 as Abs (s1, T1, t1')) =>
6.36 - (case sn of
6.37 - Plus => do_quantifier x0 s1 T1 t1'
6.38 - | Minus =>
6.39 - (* FIXME: Move elsewhere *)
6.40 - do_term (@{const Not}
6.41 - $ (HOLogic.eq_const (domain_type T0) $ t1
6.42 - $ Abs (Name.uu, T1, @{const False}))) accum)
6.43 - | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
6.44 - do_equals x t1 t2
6.45 - | (t0 as Const (s0, _)) $ t1 $ t2 =>
6.46 - if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
6.47 - s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
6.48 - let
6.49 - val impl = (s0 = @{const_name "==>"} orelse
6.50 - s0 = @{const_name "op -->"})
6.51 - val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
6.52 - val (m2, accum) = do_formula sn t2 accum
6.53 - in
6.54 - (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
6.55 - accum)
6.56 - end
6.57 - else
6.58 - do_term t accum
6.59 - | _ => do_term t accum
6.60 + (print_g (fn () => " \<Gamma> \<turnstile> " ^
6.61 + Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
6.62 + string_for_sign sn ^ "?");
6.63 + case t of
6.64 + Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
6.65 + do_quantifier x s1 T1 t1
6.66 + | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
6.67 + | @{const Trueprop} $ t1 =>
6.68 + let val (m1, accum) = do_formula sn t1 accum in
6.69 + (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
6.70 + m1), accum)
6.71 + end
6.72 + | @{const Not} $ t1 =>
6.73 + let val (m1, accum) = do_formula (negate sn) t1 accum in
6.74 + (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
6.75 + accum)
6.76 + end
6.77 + | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
6.78 + do_quantifier x s1 T1 t1
6.79 + | Const (x0 as (s0 as @{const_name Ex}, T0))
6.80 + $ (t1 as Abs (s1, T1, t1')) =>
6.81 + (case sn of
6.82 + Plus => do_quantifier x0 s1 T1 t1'
6.83 + | Minus =>
6.84 + (* FIXME: Move elsewhere *)
6.85 + do_term (@{const Not}
6.86 + $ (HOLogic.eq_const (domain_type T0) $ t1
6.87 + $ Abs (Name.uu, T1, @{const False}))) accum)
6.88 + | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
6.89 + do_equals x t1 t2
6.90 + | Const (@{const_name Let}, _) $ t1 $ t2 =>
6.91 + do_formula sn (betapply (t2, t1)) accum
6.92 + | (t0 as Const (s0, _)) $ t1 $ t2 =>
6.93 + if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
6.94 + s0 = @{const_name "op |"} orelse
6.95 + s0 = @{const_name "op -->"} then
6.96 + let
6.97 + val impl = (s0 = @{const_name "==>"} orelse
6.98 + s0 = @{const_name "op -->"})
6.99 + val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
6.100 + val (m2, accum) = do_formula sn t2 accum
6.101 + in
6.102 + (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
6.103 + accum)
6.104 + end
6.105 + else
6.106 + do_term t accum
6.107 + | _ => do_term t accum)
6.108 end
6.109 |> tap (fn (m, _) =>
6.110 print_g (fn () => "\<Gamma> \<turnstile> " ^
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Jul 03 00:49:12 2010 +0200
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Jul 03 00:50:35 2010 +0200
7.3 @@ -179,7 +179,8 @@
7.4 let
7.5 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
7.6 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
7.7 - val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
7.8 + val T = if def then T1
7.9 + else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd
7.10 in
7.11 list_comb (Const (s0, T --> T --> body_type T0),
7.12 map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])