improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
authorblanchet
Tue Mar 09 14:18:21 2010 +0100 (2010-03-09)
changeset 35671ed2c3830d881
parent 35665 ff2bf50505ab
child 35672 ff484d4f2e14
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Nitpick.thy	Tue Mar 09 09:25:23 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Mar 09 14:18:21 2010 +0100
     1.3 @@ -36,7 +36,8 @@
     1.4             and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.5             and bisim_iterator_max :: bisim_iterator
     1.6             and Quot :: "'a \<Rightarrow> 'b"
     1.7 -           and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.8 +           and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.9 +           and safe_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.10  
    1.11  datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
    1.12  datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    1.13 @@ -237,10 +238,11 @@
    1.14  setup {* Nitpick_Isar.setup *}
    1.15  
    1.16  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.17 -    bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
    1.18 -    wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
    1.19 -    Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.20 -    times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.21 +    bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
    1.22 +    wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
    1.23 +    int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
    1.24 +    norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
    1.25 +    less_eq_frac of_frac
    1.26  hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.27      word
    1.28  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
     2.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Mar 09 09:25:23 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Mar 09 14:18:21 2010 +0100
     2.3 @@ -61,7 +61,7 @@
     2.4  lemma "q2 = {}"
     2.5  nitpick [expect = genuine]
     2.6  nitpick [dont_star_linear_preds, expect = genuine]
     2.7 -nitpick [wf, expect = likely_genuine]
     2.8 +nitpick [wf, expect = quasi_genuine]
     2.9  oops
    2.10  
    2.11  lemma "p2 = UNIV"
    2.12 @@ -72,7 +72,7 @@
    2.13  lemma "q2 = UNIV"
    2.14  nitpick [expect = none]
    2.15  nitpick [dont_star_linear_preds, expect = none]
    2.16 -nitpick [wf, expect = likely_genuine]
    2.17 +nitpick [wf, expect = quasi_genuine]
    2.18  sorry
    2.19  
    2.20  lemma "p2 = q2"
     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Mar 09 09:25:23 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Mar 09 14:18:21 2010 +0100
     3.3 @@ -18,29 +18,29 @@
     3.4  subsection {* 3.1. Propositional Logic *}
     3.5  
     3.6  lemma "P \<longleftrightarrow> Q"
     3.7 -nitpick
     3.8 +nitpick [expect = genuine]
     3.9  apply auto
    3.10 -nitpick 1
    3.11 -nitpick 2
    3.12 +nitpick [expect = genuine] 1
    3.13 +nitpick [expect = genuine] 2
    3.14  oops
    3.15  
    3.16  subsection {* 3.2. Type Variables *}
    3.17  
    3.18  lemma "P x \<Longrightarrow> P (THE y. P y)"
    3.19 -nitpick [verbose]
    3.20 +nitpick [verbose, expect = genuine]
    3.21  oops
    3.22  
    3.23  subsection {* 3.3. Constants *}
    3.24  
    3.25  lemma "P x \<Longrightarrow> P (THE y. P y)"
    3.26 -nitpick [show_consts]
    3.27 -nitpick [full_descrs, show_consts]
    3.28 -nitpick [dont_specialize, full_descrs, show_consts]
    3.29 +nitpick [show_consts, expect = genuine]
    3.30 +nitpick [full_descrs, show_consts, expect = genuine]
    3.31 +nitpick [dont_specialize, full_descrs, show_consts, expect = genuine]
    3.32  oops
    3.33  
    3.34  lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
    3.35 -nitpick
    3.36 -nitpick [card 'a = 1-50]
    3.37 +nitpick [expect = none]
    3.38 +nitpick [card 'a = 1\<midarrow>50, expect = none]
    3.39  (* sledgehammer *)
    3.40  apply (metis the_equality)
    3.41  done
    3.42 @@ -48,45 +48,45 @@
    3.43  subsection {* 3.4. Skolemization *}
    3.44  
    3.45  lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    3.46 -nitpick
    3.47 +nitpick [expect = genuine]
    3.48  oops
    3.49  
    3.50  lemma "\<exists>x. \<forall>f. f x = x"
    3.51 -nitpick
    3.52 +nitpick [expect = genuine]
    3.53  oops
    3.54  
    3.55  lemma "refl r \<Longrightarrow> sym r"
    3.56 -nitpick
    3.57 +nitpick [expect = genuine]
    3.58  oops
    3.59  
    3.60  subsection {* 3.5. Natural Numbers and Integers *}
    3.61  
    3.62  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    3.63 -nitpick
    3.64 +nitpick [expect = genuine]
    3.65  oops
    3.66  
    3.67  lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
    3.68 -nitpick [card nat = 100, check_potential]
    3.69 +nitpick [card nat = 100, check_potential, expect = genuine]
    3.70  oops
    3.71  
    3.72  lemma "P Suc"
    3.73 -nitpick
    3.74 +nitpick [expect = none]
    3.75  oops
    3.76  
    3.77  lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
    3.78 -nitpick [card nat = 1]
    3.79 -nitpick [card nat = 2]
    3.80 +nitpick [card nat = 1, expect = genuine]
    3.81 +nitpick [card nat = 2, expect = none]
    3.82  oops
    3.83  
    3.84  subsection {* 3.6. Inductive Datatypes *}
    3.85  
    3.86  lemma "hd (xs @ [y, y]) = hd xs"
    3.87 -nitpick
    3.88 -nitpick [show_consts, show_datatypes]
    3.89 +nitpick [expect = genuine]
    3.90 +nitpick [show_consts, show_datatypes, expect = genuine]
    3.91  oops
    3.92  
    3.93  lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    3.94 -nitpick [show_datatypes]
    3.95 +nitpick [show_datatypes, expect = genuine]
    3.96  oops
    3.97  
    3.98  subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
    3.99 @@ -99,7 +99,7 @@
   3.100  definition C :: three where "C \<equiv> Abs_three 2"
   3.101  
   3.102  lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
   3.103 -nitpick [show_datatypes]
   3.104 +nitpick [show_datatypes, expect = genuine]
   3.105  oops
   3.106  
   3.107  fun my_int_rel where
   3.108 @@ -114,7 +114,7 @@
   3.109  quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
   3.110  
   3.111  lemma "add x y = add x x"
   3.112 -nitpick [show_datatypes]
   3.113 +nitpick [show_datatypes, expect = genuine]
   3.114  oops
   3.115  
   3.116  record point =
   3.117 @@ -122,11 +122,11 @@
   3.118    Ycoord :: int
   3.119  
   3.120  lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
   3.121 -nitpick [show_datatypes]
   3.122 +nitpick [show_datatypes, expect = genuine]
   3.123  oops
   3.124  
   3.125  lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
   3.126 -nitpick [show_datatypes]
   3.127 +nitpick [show_datatypes, expect = genuine]
   3.128  oops
   3.129  
   3.130  subsection {* 3.8. Inductive and Coinductive Predicates *}
   3.131 @@ -136,11 +136,11 @@
   3.132  "even n \<Longrightarrow> even (Suc (Suc n))"
   3.133  
   3.134  lemma "\<exists>n. even n \<and> even (Suc n)"
   3.135 -nitpick [card nat = 100, unary_ints, verbose]
   3.136 +nitpick [card nat = 100, unary_ints, verbose, expect = potential]
   3.137  oops
   3.138  
   3.139  lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
   3.140 -nitpick [card nat = 100, unary_ints, verbose]
   3.141 +nitpick [card nat = 100, unary_ints, verbose, expect = genuine]
   3.142  oops
   3.143  
   3.144  inductive even' where
   3.145 @@ -149,18 +149,18 @@
   3.146  "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
   3.147  
   3.148  lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
   3.149 -nitpick [card nat = 10, unary_ints, verbose, show_consts]
   3.150 +nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
   3.151  oops
   3.152  
   3.153  lemma "even' (n - 2) \<Longrightarrow> even' n"
   3.154 -nitpick [card nat = 10, show_consts]
   3.155 +nitpick [card nat = 10, show_consts, expect = genuine]
   3.156  oops
   3.157  
   3.158  coinductive nats where
   3.159  "nats (x\<Colon>nat) \<Longrightarrow> nats x"
   3.160  
   3.161  lemma "nats = {0, 1, 2, 3, 4}"
   3.162 -nitpick [card nat = 10, show_consts]
   3.163 +nitpick [card nat = 10, show_consts, expect = genuine]
   3.164  oops
   3.165  
   3.166  inductive odd where
   3.167 @@ -168,7 +168,7 @@
   3.168  "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
   3.169  
   3.170  lemma "odd n \<Longrightarrow> odd (n - 2)"
   3.171 -nitpick [card nat = 10, show_consts]
   3.172 +nitpick [card nat = 10, show_consts, expect = genuine]
   3.173  oops
   3.174  
   3.175  subsection {* 3.9. Coinductive Datatypes *}
   3.176 @@ -179,7 +179,8 @@
   3.177  
   3.178  typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
   3.179  
   3.180 -definition LNil where "LNil = Abs_llist (Inl [])"
   3.181 +definition LNil where
   3.182 +"LNil = Abs_llist (Inl [])"
   3.183  definition LCons where
   3.184  "LCons y ys = Abs_llist (case Rep_llist ys of
   3.185                             Inl ys' \<Rightarrow> Inl (y # ys')
   3.186 @@ -197,16 +198,16 @@
   3.187  *}
   3.188  
   3.189  lemma "xs \<noteq> LCons a xs"
   3.190 -nitpick
   3.191 +nitpick [expect = genuine]
   3.192  oops
   3.193  
   3.194  lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
   3.195 -nitpick [verbose]
   3.196 +nitpick [verbose, expect = genuine]
   3.197  oops
   3.198  
   3.199  lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
   3.200 -nitpick [bisim_depth = -1, show_datatypes]
   3.201 -nitpick
   3.202 +nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
   3.203 +nitpick [expect = none]
   3.204  sorry
   3.205  
   3.206  subsection {* 3.10. Boxing *}
   3.207 @@ -230,9 +231,9 @@
   3.208  "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
   3.209  
   3.210  lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
   3.211 -nitpick [verbose]
   3.212 -nitpick [eval = "subst\<^isub>1 \<sigma> t"]
   3.213 -(* nitpick [dont_box] *)
   3.214 +nitpick [verbose, expect = genuine]
   3.215 +nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
   3.216 +(* nitpick [dont_box, expect = unknown] *)
   3.217  oops
   3.218  
   3.219  primrec subst\<^isub>2 where
   3.220 @@ -242,19 +243,19 @@
   3.221  "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
   3.222  
   3.223  lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
   3.224 -nitpick [card = 1\<midarrow>6]
   3.225 +nitpick [card = 1\<midarrow>6, expect = none]
   3.226  sorry
   3.227  
   3.228  subsection {* 3.11. Scope Monotonicity *}
   3.229  
   3.230  lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   3.231 -nitpick [verbose]
   3.232 -nitpick [card = 8, verbose]
   3.233 +nitpick [verbose, expect = genuine]
   3.234 +nitpick [card = 8, verbose, expect = genuine]
   3.235  oops
   3.236  
   3.237  lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
   3.238 -nitpick [mono]
   3.239 -nitpick
   3.240 +nitpick [mono, expect = none]
   3.241 +nitpick [expect = genuine]
   3.242  oops
   3.243  
   3.244  subsection {* 3.12. Inductive Properties *}
   3.245 @@ -265,21 +266,21 @@
   3.246  "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
   3.247  
   3.248  lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
   3.249 -nitpick [unary_ints]
   3.250 +nitpick [unary_ints, expect = none]
   3.251  apply (induct set: reach)
   3.252    apply auto
   3.253 - nitpick
   3.254 + nitpick [expect = none]
   3.255   apply (thin_tac "n \<in> reach")
   3.256 - nitpick
   3.257 + nitpick [expect = genuine]
   3.258  oops
   3.259  
   3.260  lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
   3.261 -nitpick [unary_ints]
   3.262 +nitpick [unary_ints, expect = none]
   3.263  apply (induct set: reach)
   3.264    apply auto
   3.265 - nitpick
   3.266 + nitpick [expect = none]
   3.267   apply (thin_tac "n \<in> reach")
   3.268 - nitpick
   3.269 + nitpick [expect = genuine]
   3.270  oops
   3.271  
   3.272  lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   3.273 @@ -297,13 +298,13 @@
   3.274  "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
   3.275  
   3.276  lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
   3.277 -nitpick
   3.278 +(* nitpick *)
   3.279  proof (induct t)
   3.280    case Leaf thus ?case by simp
   3.281  next
   3.282    case (Branch t u) thus ?case
   3.283 -  nitpick
   3.284 -  nitpick [non_std, show_all]
   3.285 +  (* nitpick *)
   3.286 +  nitpick [non_std, show_all, expect = genuine]
   3.287  oops
   3.288  
   3.289  lemma "labels (swap t a b) =
   3.290 @@ -338,7 +339,7 @@
   3.291  
   3.292  theorem S\<^isub>1_sound:
   3.293  "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   3.294 -nitpick
   3.295 +nitpick [expect = genuine]
   3.296  oops
   3.297  
   3.298  inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   3.299 @@ -351,7 +352,7 @@
   3.300  
   3.301  theorem S\<^isub>2_sound:
   3.302  "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   3.303 -nitpick
   3.304 +nitpick [expect = genuine]
   3.305  oops
   3.306  
   3.307  inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   3.308 @@ -369,7 +370,7 @@
   3.309  
   3.310  theorem S\<^isub>3_complete:
   3.311  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   3.312 -nitpick
   3.313 +nitpick [expect = genuine]
   3.314  oops
   3.315  
   3.316  inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   3.317 @@ -465,11 +466,11 @@
   3.318                               (if x > y then insort\<^isub>1 u x else u))"
   3.319  
   3.320  theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
   3.321 -nitpick
   3.322 +nitpick [expect = genuine]
   3.323  oops
   3.324  
   3.325  theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
   3.326 -nitpick [eval = "insort\<^isub>1 t x"]
   3.327 +nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
   3.328  oops
   3.329  
   3.330  primrec insort\<^isub>2 where
     4.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Mar 09 09:25:23 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Mar 09 14:18:21 2010 +0100
     4.3 @@ -2,13 +2,13 @@
     4.4  
     4.5    * Added and implemented "binary_ints" and "bits" options
     4.6    * Added "std" option and implemented support for nonstandard models
     4.7 +  * Added and implemented "finitize" option to improve the precision of infinite
     4.8 +    datatypes based on a monotonicity analysis
     4.9    * Added support for quotient types
    4.10 -  * Added support for local definitions
    4.11 -  * Disabled "fast_descrs" option by default
    4.12 +  * Added support for local definitions (for "function" and "termination"
    4.13 +    proofs)
    4.14    * Optimized "Multiset.multiset" and "FinFun.finfun"
    4.15    * Improved efficiency of "destroy_constrs" optimization
    4.16 -  * Improved precision of infinite datatypes whose constructors don't appear
    4.17 -    in the formula to falsify based on a monotonicity analysis
    4.18    * Fixed soundness bugs related to "destroy_constrs" optimization and record
    4.19      getters
    4.20    * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 09 09:25:23 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 09 14:18:21 2010 +0100
     5.3 @@ -326,8 +326,6 @@
     5.4      val sound_finitizes =
     5.5        none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
     5.6                            | _ => false) finitizes)
     5.7 -    val genuine_means_genuine =
     5.8 -      got_all_user_axioms andalso none_true wfs andalso sound_finitizes
     5.9      val standard = forall snd stds
    5.10  (*
    5.11      val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
    5.12 @@ -603,7 +601,7 @@
    5.13      fun show_kodkod_warning "" = ()
    5.14        | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
    5.15  
    5.16 -    (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
    5.17 +    (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *)
    5.18      fun print_and_check_model genuine bounds
    5.19              ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
    5.20               : problem_extension) =
    5.21 @@ -614,119 +612,126 @@
    5.22                                   show_consts = show_consts}
    5.23                scope formats frees free_names sel_names nonsel_names rel_table
    5.24                bounds
    5.25 -        val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok
    5.26 +        val genuine_means_genuine =
    5.27 +          got_all_user_axioms andalso none_true wfs andalso
    5.28 +          sound_finitizes andalso codatatypes_ok
    5.29        in
    5.30 -        pprint (Pretty.chunks
    5.31 -            [Pretty.blk (0,
    5.32 -                 (pstrs ("Nitpick found a" ^
    5.33 -                         (if not genuine then " potential "
    5.34 -                          else if genuine_means_genuine then " "
    5.35 -                          else " likely genuine ") ^ das_wort_model) @
    5.36 -                  (case pretties_for_scope scope verbose of
    5.37 -                     [] => []
    5.38 -                   | pretties => pstrs " for " @ pretties) @
    5.39 -                  [Pretty.str ":\n"])),
    5.40 -             Pretty.indent indent_size reconstructed_model]);
    5.41 -        if genuine then
    5.42 -          (if check_genuine andalso standard then
    5.43 -             (case prove_hol_model scope tac_timeout free_names sel_names
    5.44 +        (pprint (Pretty.chunks
    5.45 +             [Pretty.blk (0,
    5.46 +                  (pstrs ("Nitpick found a" ^
    5.47 +                          (if not genuine then " potential "
    5.48 +                           else if genuine_means_genuine then " "
    5.49 +                           else " quasi genuine ") ^ das_wort_model) @
    5.50 +                   (case pretties_for_scope scope verbose of
    5.51 +                      [] => []
    5.52 +                    | pretties => pstrs " for " @ pretties) @
    5.53 +                   [Pretty.str ":\n"])),
    5.54 +              Pretty.indent indent_size reconstructed_model]);
    5.55 +         if genuine then
    5.56 +           (if check_genuine andalso standard then
    5.57 +              case prove_hol_model scope tac_timeout free_names sel_names
    5.58                                     rel_table bounds assms_t of
    5.59 -                SOME true => print ("Confirmation by \"auto\": The above " ^
    5.60 -                                    das_wort_model ^ " is really genuine.")
    5.61 +                SOME true =>
    5.62 +                print ("Confirmation by \"auto\": The above " ^
    5.63 +                       das_wort_model ^ " is really genuine.")
    5.64                | SOME false =>
    5.65                  if genuine_means_genuine then
    5.66                    error ("A supposedly genuine " ^ das_wort_model ^ " was \
    5.67                           \shown to be spurious by \"auto\".\nThis should never \
    5.68                           \happen.\nPlease send a bug report to blanchet\
    5.69                           \te@in.tum.de.")
    5.70 -                else
    5.71 -                  print ("Refutation by \"auto\": The above " ^ das_wort_model ^
    5.72 -                         " is spurious.")
    5.73 -              | NONE => print "No confirmation by \"auto\".")
    5.74 -           else
    5.75 -             ();
    5.76 -           if not standard andalso likely_in_struct_induct_step then
    5.77 -             print "The existence of a nonstandard model suggests that the \
    5.78 -                   \induction hypothesis is not general enough or perhaps even \
    5.79 -                   \wrong. See the \"Inductive Properties\" section of the \
    5.80 -                   \Nitpick manual for details (\"isabelle doc nitpick\")."
    5.81 -           else
    5.82 -             ();
    5.83 -           if has_syntactic_sorts orig_t then
    5.84 -             print "Hint: Maybe you forgot a type constraint?"
    5.85 +                 else
    5.86 +                   print ("Refutation by \"auto\": The above " ^
    5.87 +                          das_wort_model ^ " is spurious.")
    5.88 +               | NONE => print "No confirmation by \"auto\"."
    5.89 +            else
    5.90 +              ();
    5.91 +            if not standard andalso likely_in_struct_induct_step then
    5.92 +              print "The existence of a nonstandard model suggests that the \
    5.93 +                    \induction hypothesis is not general enough or perhaps \
    5.94 +                    \even wrong. See the \"Inductive Properties\" section of \
    5.95 +                    \the Nitpick manual for details (\"isabelle doc nitpick\")."
    5.96 +            else
    5.97 +              ();
    5.98 +            if has_syntactic_sorts orig_t then
    5.99 +              print "Hint: Maybe you forgot a type constraint?"
   5.100 +            else
   5.101 +              ();
   5.102 +            if not genuine_means_genuine then
   5.103 +              if no_poly_user_axioms then
   5.104 +                let
   5.105 +                  val options =
   5.106 +                    [] |> not got_all_mono_user_axioms
   5.107 +                          ? cons ("user_axioms", "\"true\"")
   5.108 +                       |> not (none_true wfs)
   5.109 +                          ? cons ("wf", "\"smart\" or \"false\"")
   5.110 +                       |> not sound_finitizes
   5.111 +                          ? cons ("finitize", "\"smart\" or \"false\"")
   5.112 +                       |> not codatatypes_ok
   5.113 +                          ? cons ("bisim_depth", "a nonnegative value")
   5.114 +                  val ss =
   5.115 +                    map (fn (name, value) => quote name ^ " set to " ^ value)
   5.116 +                        options
   5.117 +                in
   5.118 +                  print ("Try again with " ^
   5.119 +                         space_implode " " (serial_commas "and" ss) ^
   5.120 +                         " to confirm that the " ^ das_wort_model ^
   5.121 +                         " is genuine.")
   5.122 +                end
   5.123 +              else
   5.124 +                print ("Nitpick is unable to guarantee the authenticity of \
   5.125 +                       \the " ^ das_wort_model ^ " in the presence of \
   5.126 +                       \polymorphic axioms.")
   5.127 +            else
   5.128 +              ();
   5.129 +            NONE)
   5.130 +         else
   5.131 +           if not genuine then
   5.132 +             (Unsynchronized.inc met_potential;
   5.133 +              if check_potential then
   5.134 +                let
   5.135 +                  val status = prove_hol_model scope tac_timeout free_names
   5.136 +                                              sel_names rel_table bounds assms_t
   5.137 +                in
   5.138 +                  (case status of
   5.139 +                     SOME true => print ("Confirmation by \"auto\": The \
   5.140 +                                         \above " ^ das_wort_model ^
   5.141 +                                         " is genuine.")
   5.142 +                   | SOME false => print ("Refutation by \"auto\": The above " ^
   5.143 +                                          das_wort_model ^ " is spurious.")
   5.144 +                   | NONE => print "No confirmation by \"auto\".");
   5.145 +                  status
   5.146 +                end
   5.147 +              else
   5.148 +                NONE)
   5.149             else
   5.150 -             ();
   5.151 -           if not genuine_means_genuine then
   5.152 -             if no_poly_user_axioms then
   5.153 -               let
   5.154 -                 val options =
   5.155 -                   [] |> not got_all_mono_user_axioms
   5.156 -                         ? cons ("user_axioms", "\"true\"")
   5.157 -                      |> not (none_true wfs)
   5.158 -                         ? cons ("wf", "\"smart\" or \"false\"")
   5.159 -                      |> not sound_finitizes
   5.160 -                         ? cons ("finitize", "\"smart\" or \"false\"")
   5.161 -                      |> not codatatypes_ok
   5.162 -                         ? cons ("bisim_depth", "a nonnegative value")
   5.163 -                 val ss =
   5.164 -                   map (fn (name, value) => quote name ^ " set to " ^ value)
   5.165 -                       options
   5.166 -               in
   5.167 -                 print ("Try again with " ^
   5.168 -                        space_implode " " (serial_commas "and" ss) ^
   5.169 -                        " to confirm that the " ^ das_wort_model ^
   5.170 -                        " is genuine.")
   5.171 -               end
   5.172 -             else
   5.173 -               print ("Nitpick is unable to guarantee the authenticity of \
   5.174 -                      \the " ^ das_wort_model ^ " in the presence of \
   5.175 -                      \polymorphic axioms.")
   5.176 -           else
   5.177 -             ();
   5.178 -           NONE)
   5.179 -        else
   5.180 -          if not genuine then
   5.181 -            (Unsynchronized.inc met_potential;
   5.182 -             if check_potential then
   5.183 -               let
   5.184 -                 val status = prove_hol_model scope tac_timeout free_names
   5.185 -                                              sel_names rel_table bounds assms_t
   5.186 -               in
   5.187 -                 (case status of
   5.188 -                    SOME true => print ("Confirmation by \"auto\": The above " ^
   5.189 -                                        das_wort_model ^ " is genuine.")
   5.190 -                  | SOME false => print ("Refutation by \"auto\": The above " ^
   5.191 -                                         das_wort_model ^ " is spurious.")
   5.192 -                  | NONE => print "No confirmation by \"auto\".");
   5.193 -                 status
   5.194 -               end
   5.195 -             else
   5.196 -               NONE)
   5.197 -          else
   5.198 -            NONE
   5.199 +             NONE)
   5.200 +        |> pair genuine_means_genuine
   5.201        end
   5.202 -    (* int -> int -> int -> bool -> rich_problem list -> int * int * int *)
   5.203 -    fun solve_any_problem max_potential max_genuine donno first_time problems =
   5.204 +    (* bool * int * int * int -> bool -> rich_problem list
   5.205 +       -> bool * int * int * int *)
   5.206 +    fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
   5.207 +                           donno) first_time problems =
   5.208        let
   5.209          val max_potential = Int.max (0, max_potential)
   5.210          val max_genuine = Int.max (0, max_genuine)
   5.211 -        (* bool -> int * KK.raw_bound list -> bool option *)
   5.212 +        (* bool -> int * KK.raw_bound list -> bool * bool option *)
   5.213          fun print_and_check genuine (j, bounds) =
   5.214            print_and_check_model genuine bounds (snd (nth problems j))
   5.215          val max_solutions = max_potential + max_genuine
   5.216                              |> not need_incremental ? curry Int.min 1
   5.217        in
   5.218          if max_solutions <= 0 then
   5.219 -          (0, 0, donno)
   5.220 +          (found_really_genuine, 0, 0, donno)
   5.221          else
   5.222            case KK.solve_any_problem overlord deadline max_threads max_solutions
   5.223                                      (map fst problems) of
   5.224              KK.NotInstalled =>
   5.225              (print_m install_kodkodi_message;
   5.226 -             (max_potential, max_genuine, donno + 1))
   5.227 +             (found_really_genuine, max_potential, max_genuine, donno + 1))
   5.228            | KK.Normal ([], unsat_js, s) =>
   5.229              (update_checked_problems problems unsat_js; show_kodkod_warning s;
   5.230 -             (max_potential, max_genuine, donno))
   5.231 +             (found_really_genuine, max_potential, max_genuine, donno))
   5.232            | KK.Normal (sat_ps, unsat_js, s) =>
   5.233              let
   5.234                val (lib_ps, con_ps) =
   5.235 @@ -736,16 +741,19 @@
   5.236                show_kodkod_warning s;
   5.237                if null con_ps then
   5.238                  let
   5.239 -                  val num_genuine = take max_potential lib_ps
   5.240 -                                    |> map (print_and_check false)
   5.241 -                                    |> filter (curry (op =) (SOME true))
   5.242 -                                    |> length
   5.243 +                  val genuine_codes =
   5.244 +                    lib_ps |> take max_potential
   5.245 +                           |> map (print_and_check false)
   5.246 +                           |> filter (curry (op =) (SOME true) o snd)
   5.247 +                  val found_really_genuine =
   5.248 +                    found_really_genuine orelse exists fst genuine_codes
   5.249 +                  val num_genuine = length genuine_codes
   5.250                    val max_genuine = max_genuine - num_genuine
   5.251                    val max_potential = max_potential
   5.252                                        - (length lib_ps - num_genuine)
   5.253                  in
   5.254                    if max_genuine <= 0 then
   5.255 -                    (0, 0, donno)
   5.256 +                    (found_really_genuine, 0, 0, donno)
   5.257                    else
   5.258                      let
   5.259                        (* "co_js" is the list of sound problems whose unsound
   5.260 @@ -765,18 +773,21 @@
   5.261                                   |> max_potential <= 0
   5.262                                      ? filter_out (#unsound o snd)
   5.263                      in
   5.264 -                      solve_any_problem max_potential max_genuine donno false
   5.265 -                                        problems
   5.266 +                      solve_any_problem (found_really_genuine, max_potential,
   5.267 +                                         max_genuine, donno) false problems
   5.268                      end
   5.269                  end
   5.270                else
   5.271                  let
   5.272 -                  val _ = take max_genuine con_ps
   5.273 -                          |> List.app (ignore o print_and_check true)
   5.274 -                  val max_genuine = max_genuine - length con_ps
   5.275 +                  val genuine_codes =
   5.276 +                    con_ps |> take max_genuine
   5.277 +                           |> map (print_and_check true)
   5.278 +                  val max_genuine = max_genuine - length genuine_codes
   5.279 +                  val found_really_genuine =
   5.280 +                    found_really_genuine orelse exists fst genuine_codes
   5.281                  in
   5.282                    if max_genuine <= 0 orelse not first_time then
   5.283 -                    (0, max_genuine, donno)
   5.284 +                    (found_really_genuine, 0, max_genuine, donno)
   5.285                    else
   5.286                      let
   5.287                        val bye_js = sort_distinct int_ord
   5.288 @@ -784,7 +795,10 @@
   5.289                        val problems =
   5.290                          problems |> filter_out_indices bye_js
   5.291                                   |> filter_out (#unsound o snd)
   5.292 -                    in solve_any_problem 0 max_genuine donno false problems end
   5.293 +                    in
   5.294 +                      solve_any_problem (found_really_genuine, 0, max_genuine,
   5.295 +                                         donno) false problems
   5.296 +                    end
   5.297                  end
   5.298              end
   5.299            | KK.TimedOut unsat_js =>
   5.300 @@ -795,11 +809,13 @@
   5.301            | KK.Error (s, unsat_js) =>
   5.302              (update_checked_problems problems unsat_js;
   5.303               print_v (K ("Kodkod error: " ^ s ^ "."));
   5.304 -             (max_potential, max_genuine, donno + 1))
   5.305 +             (found_really_genuine, max_potential, max_genuine, donno + 1))
   5.306        end
   5.307  
   5.308 -    (* int -> int -> scope list -> int * int * int -> int * int * int *)
   5.309 -    fun run_batch j n scopes (max_potential, max_genuine, donno) =
   5.310 +    (* int -> int -> scope list -> bool * int * int * int
   5.311 +       -> bool * int * int * int *)
   5.312 +    fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
   5.313 +                              donno) =
   5.314        let
   5.315          val _ =
   5.316            if null scopes then
   5.317 @@ -869,7 +885,8 @@
   5.318            else
   5.319              ()
   5.320        in
   5.321 -        solve_any_problem max_potential max_genuine donno true (rev problems)
   5.322 +        solve_any_problem (found_really_genuine, max_potential, max_genuine,
   5.323 +                           donno) true (rev problems)
   5.324        end
   5.325  
   5.326      (* rich_problem list -> scope -> int *)
   5.327 @@ -901,8 +918,9 @@
   5.328             "") ^ "."
   5.329        end
   5.330  
   5.331 -    (* int -> int -> scope list -> int * int * int -> KK.outcome *)
   5.332 -    fun run_batches _ _ [] (max_potential, max_genuine, donno) =
   5.333 +    (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *)
   5.334 +    fun run_batches _ _ []
   5.335 +                    (found_really_genuine, max_potential, max_genuine, donno) =
   5.336          if donno > 0 andalso max_genuine > 0 then
   5.337            (print_m (fn () => excipit "ran out of some resource"); "unknown")
   5.338          else if max_genuine = original_max_genuine then
   5.339 @@ -919,10 +937,12 @@
   5.340                   "Nitpick could not find a" ^
   5.341                   (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
   5.342                    else "ny better " ^ das_wort_model ^ "s.")); "potential")
   5.343 +        else if found_really_genuine then
   5.344 +          "genuine"
   5.345          else
   5.346 -          if genuine_means_genuine then "genuine" else "likely_genuine"
   5.347 +          "quasi_genuine"
   5.348        | run_batches j n (batch :: batches) z =
   5.349 -        let val (z as (_, max_genuine, _)) = run_batch j n batch z in
   5.350 +        let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
   5.351            run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
   5.352          end
   5.353  
   5.354 @@ -942,7 +962,8 @@
   5.355  
   5.356      val batches = batch_list batch_size (!scopes)
   5.357      val outcome_code =
   5.358 -      (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
   5.359 +      (run_batches 0 (length batches) batches
   5.360 +                   (false, max_potential, max_genuine, 0)
   5.361         handle Exn.Interrupt => do_interrupted ())
   5.362        handle TimeLimit.TimeOut =>
   5.363               (print_m (fn () => excipit "ran out of time");
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Mar 09 09:25:23 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Mar 09 14:18:21 2010 +0100
     6.3 @@ -361,7 +361,8 @@
     6.4     (@{const_name finite}, 1),
     6.5     (@{const_name unknown}, 0),
     6.6     (@{const_name is_unknown}, 1),
     6.7 -   (@{const_name Tha}, 1),
     6.8 +   (@{const_name safe_The}, 1),
     6.9 +   (@{const_name safe_Eps}, 1),
    6.10     (@{const_name Frac}, 0),
    6.11     (@{const_name norm_frac}, 0)]
    6.12  val built_in_nat_consts =
    6.13 @@ -1821,7 +1822,7 @@
    6.14      val bisim_max = @{const bisim_iterator_max}
    6.15      val n_var = Var (("n", 0), iter_T)
    6.16      val n_var_minus_1 =
    6.17 -      Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
    6.18 +      Const (@{const_name safe_The}, (iter_T --> bool_T) --> iter_T)
    6.19        $ Abs ("m", iter_T, HOLogic.eq_const iter_T
    6.20                            $ (suc_const iter_T $ Bound 0) $ n_var)
    6.21      val x_var = Var (("x", 0), T)
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 09 09:25:23 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 09 14:18:21 2010 +0100
     7.3 @@ -1388,7 +1388,7 @@
     7.4                                                (Func (R1, Formula Neut)) r))
     7.5                 (to_opt R1 u1)
     7.6           | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
     7.7 -      | Op1 (Tha, _, R, u1) =>
     7.8 +      | Op1 (SafeThe, _, R, u1) =>
     7.9          if is_opt_rep R then
    7.10            kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
    7.11          else
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 09:25:23 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 14:18:21 2010 +0100
     8.3 @@ -768,12 +768,9 @@
     8.4                | @{const_name rtrancl} =>
     8.5                  (print_g "*** rtrancl"; mtype_unsolvable)
     8.6                | @{const_name finite} =>
     8.7 -                if is_finite_type hol_ctxt T then
     8.8 -                  let val M1 = mtype_for (domain_type (domain_type T)) in
     8.9 -                    (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
    8.10 -                  end
    8.11 -                else
    8.12 -                  (print_g "*** finite"; mtype_unsolvable)
    8.13 +                let val M1 = mtype_for (domain_type (domain_type T)) in
    8.14 +                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
    8.15 +                end
    8.16                | @{const_name rel_comp} =>
    8.17                  let
    8.18                    val x = Unsynchronized.inc max_fresh
    8.19 @@ -813,14 +810,15 @@
    8.20                    (MFun (a_set_M, S Minus,
    8.21                           MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
    8.22                  end
    8.23 -              | @{const_name Tha} =>
    8.24 -                let
    8.25 -                  val a_M = mtype_for (domain_type (domain_type T))
    8.26 -                  val a_set_M = plus_set_mtype_for_dom a_M
    8.27 -                in (MFun (a_set_M, S Minus, a_M), accum) end
    8.28                | _ =>
    8.29 -                if s = @{const_name minus_class.minus} andalso
    8.30 -                   is_set_type (domain_type T) then
    8.31 +                if s = @{const_name safe_The} orelse
    8.32 +                   s = @{const_name safe_Eps} then
    8.33 +                  let
    8.34 +                    val a_set_M = mtype_for (domain_type T)
    8.35 +                    val a_M = dest_MFun a_set_M |> #1
    8.36 +                  in (MFun (a_set_M, S Minus, a_M), accum) end
    8.37 +                else if s = @{const_name minus_class.minus} andalso
    8.38 +                        is_set_type (domain_type T) then
    8.39                    let
    8.40                      val set_T = domain_type T
    8.41                      val left_set_M = mtype_for set_T
    8.42 @@ -1206,7 +1204,13 @@
    8.43            in
    8.44              case t of
    8.45                Const (x as (s, T)) =>
    8.46 -              if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
    8.47 +              if s = @{const_name finite} then
    8.48 +                case domain_type T' of
    8.49 +                  T1' as Type (@{type_name fin_fun}, _) =>
    8.50 +                  Abs (Name.uu, T1', @{const True})
    8.51 +                | _ => Const (s, T')
    8.52 +              else if s = @{const_name "=="} orelse
    8.53 +                      s = @{const_name "op ="} then
    8.54                  Const (s, T')
    8.55                else if is_built_in_const thy stds fast_descrs x then
    8.56                  coerce_term hol_ctxt Ts T' T t
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Mar 09 09:25:23 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Mar 09 14:18:21 2010 +0100
     9.3 @@ -39,7 +39,7 @@
     9.4      Closure |
     9.5      SingletonSet |
     9.6      IsUnknown |
     9.7 -    Tha |
     9.8 +    SafeThe |
     9.9      First |
    9.10      Second |
    9.11      Cast
    9.12 @@ -158,7 +158,7 @@
    9.13    Closure |
    9.14    SingletonSet |
    9.15    IsUnknown |
    9.16 -  Tha |
    9.17 +  SafeThe |
    9.18    First |
    9.19    Second |
    9.20    Cast
    9.21 @@ -232,7 +232,7 @@
    9.22    | string_for_op1 Closure = "Closure"
    9.23    | string_for_op1 SingletonSet = "SingletonSet"
    9.24    | string_for_op1 IsUnknown = "IsUnknown"
    9.25 -  | string_for_op1 Tha = "Tha"
    9.26 +  | string_for_op1 SafeThe = "SafeThe"
    9.27    | string_for_op1 First = "First"
    9.28    | string_for_op1 Second = "Second"
    9.29    | string_for_op1 Cast = "Cast"
    9.30 @@ -516,8 +516,15 @@
    9.31              val t1 = list_comb (t0, ts')
    9.32              val T1 = fastype_of1 (Ts, t1)
    9.33            in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
    9.34 -        (* styp -> term list -> term *)
    9.35 -        fun construct (x as (_, T)) ts =
    9.36 +        (* op2 -> string -> styp -> term -> nut *)
    9.37 +        fun do_description_operator oper undef_s (x as (_, T)) t1 =
    9.38 +          if fast_descrs then
    9.39 +            Op2 (oper, range_type T, Any, sub t1,
    9.40 +                 sub (Const (undef_s, range_type T)))
    9.41 +          else
    9.42 +            do_apply (Const x) [t1]
    9.43 +        (* styp -> term list -> nut *)
    9.44 +        fun do_construct (x as (_, T)) ts =
    9.45            case num_binder_types T - length ts of
    9.46              0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
    9.47                                    o nth_sel_for_constr x)
    9.48 @@ -552,18 +559,10 @@
    9.49            do_quantifier Exist s T t1
    9.50          | (t0 as Const (@{const_name Ex}, _), [t1]) =>
    9.51            sub' (t0 $ eta_expand Ts t1 1)
    9.52 -        | (t0 as Const (@{const_name The}, T), [t1]) =>
    9.53 -          if fast_descrs then
    9.54 -            Op2 (The, range_type T, Any, sub t1,
    9.55 -                 sub (Const (@{const_name undefined_fast_The}, range_type T)))
    9.56 -          else
    9.57 -            do_apply t0 [t1]
    9.58 -        | (t0 as Const (@{const_name Eps}, T), [t1]) =>
    9.59 -          if fast_descrs then
    9.60 -            Op2 (Eps, range_type T, Any, sub t1,
    9.61 -                 sub (Const (@{const_name undefined_fast_Eps}, range_type T)))
    9.62 -          else
    9.63 -            do_apply t0 [t1]
    9.64 +        | (Const (x as (@{const_name The}, _)), [t1]) =>
    9.65 +          do_description_operator The @{const_name undefined_fast_The} x t1
    9.66 +        | (Const (x as (@{const_name Eps}, _)), [t1]) =>
    9.67 +          do_description_operator Eps @{const_name undefined_fast_Eps} x t1
    9.68          | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
    9.69          | (Const (@{const_name "op &"}, _), [t1, t2]) =>
    9.70            Op2 (And, bool_T, Any, sub' t1, sub' t2)
    9.71 @@ -605,7 +604,7 @@
    9.72            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    9.73          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    9.74            if is_built_in_const thy stds false x then Cst (Suc, T, Any)
    9.75 -          else if is_constr thy stds x then construct x []
    9.76 +          else if is_constr thy stds x then do_construct x []
    9.77            else ConstName (s, T, Any)
    9.78          | (Const (@{const_name finite}, T), [t1]) =>
    9.79            (if is_finite_type hol_ctxt (domain_type T) then
    9.80 @@ -616,7 +615,7 @@
    9.81          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    9.82          | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
    9.83            if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
    9.84 -          else if is_constr thy stds x then construct x []
    9.85 +          else if is_constr thy stds x then do_construct x []
    9.86            else ConstName (s, T, Any)
    9.87          | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
    9.88            if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
    9.89 @@ -670,8 +669,11 @@
    9.90          | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
    9.91          | (Const (@{const_name is_unknown}, _), [t1]) =>
    9.92            Op1 (IsUnknown, bool_T, Any, sub t1)
    9.93 -        | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
    9.94 -          Op1 (Tha, T2, Any, sub t1)
    9.95 +        | (Const (@{const_name safe_The},
    9.96 +                  Type (@{type_name fun}, [_, T2])), [t1]) =>
    9.97 +          Op1 (SafeThe, T2, Any, sub t1)
    9.98 +        | (Const (x as (@{const_name safe_Eps}, _)), [t1]) =>
    9.99 +          do_description_operator Eps @{const_name undefined_fast_Eps} x t1
   9.100          | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
   9.101          | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
   9.102          | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
   9.103 @@ -691,7 +693,7 @@
   9.104            Op2 (Union, T1, Any, sub t1, sub t2)
   9.105          | (t0 as Const (x as (s, T)), ts) =>
   9.106            if is_constr thy stds x then
   9.107 -            construct x ts
   9.108 +            do_construct x ts
   9.109            else if String.isPrefix numeral_prefix s then
   9.110              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   9.111            else
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 09:25:23 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 14:18:21 2010 +0100
    10.3 @@ -221,7 +221,8 @@
    10.4          $ do_term new_Ts old_Ts polar t2
    10.5        | Const (s as @{const_name The}, T) => do_description_operator s T
    10.6        | Const (s as @{const_name Eps}, T) => do_description_operator s T
    10.7 -      | Const (s as @{const_name Tha}, T) => do_description_operator s T
    10.8 +      | Const (s as @{const_name safe_The}, T) => do_description_operator s T
    10.9 +      | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T
   10.10        | Const (x as (s, T)) =>
   10.11          Const (s, if s = @{const_name converse} orelse
   10.12                       s = @{const_name trancl} then