author blanchet Tue Jan 03 18:33:18 2012 +0100 (2012-01-03) changeset 46104 eb85282db54e parent 46103 1e35730bd869 child 46105 9abb756352a6
no abuse of notation
```     1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
1.3 @@ -17,8 +17,7 @@
1.4
1.5  chapter {* 2. First Steps *}
1.6
1.7 -nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
1.8 -                timeout = 240]
1.9 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
1.10
1.11  subsection {* 2.1. Propositional Logic *}
1.12
1.13 @@ -31,23 +30,23 @@
1.14
1.15  subsection {* 2.2. Type Variables *}
1.16
1.17 -lemma "P x \<Longrightarrow> P (THE y. P y)"
1.18 +lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
1.19  nitpick [verbose, expect = genuine]
1.20  oops
1.21
1.22  subsection {* 2.3. Constants *}
1.23
1.24 -lemma "P x \<Longrightarrow> P (THE y. P y)"
1.25 +lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
1.26  nitpick [show_consts, expect = genuine]
1.27  nitpick [dont_specialize, show_consts, expect = genuine]
1.28  oops
1.29
1.30 -lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
1.31 +lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
1.32  nitpick [expect = none]
1.33  nitpick [card 'a = 1\<emdash>50, expect = none]
1.34  (* sledgehammer *)
1.35 -apply (metis the_equality)
1.36 -done
1.37 +sledgehammer
1.38 +by (metis the_equality)
1.39
1.40  subsection {* 2.4. Skolemization *}
1.41
1.42 @@ -67,6 +66,7 @@
1.43
1.44  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
1.45  nitpick [expect = genuine]
1.46 +nitpick [binary_ints, bits = 16, expect = genuine]
1.47  oops
1.48
1.49  lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
1.50 @@ -95,15 +95,14 @@
1.51
1.52  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
1.53
1.54 -definition "three = {0\<Colon>nat, 1, 2}"
1.55 -typedef (open) three = three
1.56 -unfolding three_def by blast
1.57 +typedef three = "{0\<Colon>nat, 1, 2}"
1.58 +by blast
1.59
1.60  definition A :: three where "A \<equiv> Abs_three 0"
1.61  definition B :: three where "B \<equiv> Abs_three 1"
1.62  definition C :: three where "C \<equiv> Abs_three 2"
1.63
1.64 -lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
1.65 +lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
1.66  nitpick [show_datatypes, expect = genuine]
1.67  oops
1.68
```
```     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
2.3 @@ -836,11 +836,9 @@
2.4
2.5  fun assign_operator_for_const (s, T) =
2.6    if String.isPrefix ubfp_prefix s then
2.7 -    if is_fun_type T then xsym "\<subseteq>" "<=" ()
2.8 -    else xsym "\<le>" "<=" ()
2.9 +    xsym "\<le>" "<=" ()
2.10    else if String.isPrefix lbfp_prefix s then
2.11 -    if is_fun_type T then xsym "\<supseteq>" ">=" ()
2.12 -    else xsym "\<ge>" ">=" ()
2.13 +    xsym "\<ge>" ">=" ()
2.14    else if original_name s <> s then
2.15      assign_operator_for_const (strip_first_name_sep s |> snd, T)
2.16    else
```