no abuse of notation
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03 ago)
changeset 46104eb85282db54e
parent 46103 1e35730bd869
child 46105 9abb756352a6
no abuse of notation
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/nitpick_model.ML
     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