summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Tue, 14 Sep 2010 14:22:49 +0200 | |

changeset 39362 | ee65900bfced |

parent 39361 | 520ea38711e4 |

child 39363 | 1c4e38d635e1 |

adapt examples to latest Nitpick changes + speed them up a little bit

--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 14 14:12:18 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 14 14:22:49 2010 +0200 @@ -11,7 +11,7 @@ imports Nitpick begin -nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8, +nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] lemma "Suc x = x + 1" @@ -232,13 +232,13 @@ oops lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2" -nitpick [expect = none] -nitpick [dont_finitize, expect = none] +nitpick [expect = potential] (* unfortunate *) +nitpick [dont_finitize, expect = potential] sorry lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)" -nitpick [expect = none] (* unfortunate *) -nitpick [dont_finitize, expect = none] +nitpick [expect = potential] (* unfortunate *) +nitpick [dont_finitize, expect = potential] oops end

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 14 14:12:18 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 14 14:22:49 2010 +0200 @@ -38,8 +38,7 @@ lemma "P x \<Longrightarrow> P (THE y. P y)" nitpick [show_consts, expect = genuine] -nitpick [full_descrs, show_consts, expect = genuine] -nitpick [dont_specialize, full_descrs, show_consts, expect = genuine] +nitpick [dont_specialize, show_consts, expect = genuine] oops lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Sep 14 14:12:18 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Sep 14 14:22:49 2010 +0200 @@ -64,7 +64,7 @@ oops lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" -nitpick [expect = none] +nitpick [expect = potential] (* unfortunate *) sorry lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y" @@ -162,10 +162,6 @@ nitpick [card = 1, unary_ints, max_potential = 0, expect = none] by (rule Zero_int_def_raw) -lemma "Abs_Integ (Rep_Integ a) = a" -nitpick [card = 1, unary_ints, max_potential = 0, expect = none] -by (rule Rep_Integ_inverse) - lemma "Abs_list (Rep_list a) = a" nitpick [card = 1\<midarrow>2, expect = none] by (rule Rep_list_inverse)