# HG changeset patch
# User blanchet
# Date 1325611997 -3600
# Node ID 1c436a920730b3b34c906ab9d27db40d4bbc0636
# Parent  8f6465f7021b56224f0417c297cebc811260de18
reintroduced failing examples now that they work again, after reintroduction of "set"

diff -r 8f6465f7021b -r 1c436a920730 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
@@ -53,7 +53,7 @@
 nitpick [card room = 1, card guest = 2, card "guest option" = 3,
          card key = 4, card state = 6, show_consts, format = 2,
          expect = genuine]
-(* nitpick [card room = 1, card guest = 2, expect = genuine] *)
+(* nitpick [card room = 1, card guest = 2, expect = genuine] *) (* slow *)
 oops
 
 end
diff -r 8f6465f7021b -r 1c436a920730 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
@@ -8,7 +8,9 @@
 header {* Examples Featuring Nitpick's Monotonicity Check *}
 
 theory Mono_Nits
-imports Main (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
+imports Main
+        (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
+        (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
 begin
 
 ML {*
@@ -52,10 +54,9 @@
   Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])
 
 fun is_const t =
-  let
-    val T = fastype_of t
-  in
-    is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False}))
+  let val T = fastype_of t in
+    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})
+    |> is_mono
   end
 
 fun mono t = is_mono t orelse raise BUG
@@ -92,9 +93,9 @@
 ML {* const @{term "A (a\<Colon>'a)"} *}
 ML {* const @{term "insert (a\<Colon>'a) A = B"} *}
 ML {* const @{term "- (A\<Colon>'a set)"} *}
-(* ML {* const @{term "finite (A\<Colon>'a set)"} *} *)
-(* ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *} *)
-(* ML {* const @{term "finite (A\<Colon>'a set set)"} *} *)
+ML {* const @{term "finite (A\<Colon>'a set)"} *}
+ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
+ML {* const @{term "finite (A\<Colon>'a set set)"} *}
 ML {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
 ML {* const @{term "A < (B\<Colon>'a set)"} *}
 ML {* const @{term "A \<le> (B\<Colon>'a set)"} *}
@@ -120,11 +121,12 @@
 ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
 ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
 ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
-(* ML {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *} *)
+ML {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
 ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
 ML {* mono @{prop "P (a\<Colon>'a)"} *}
 ML {* mono @{prop "{a} = {b\<Colon>'a}"} *}
+ML {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
 ML {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
 ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
 ML {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
@@ -136,7 +138,7 @@
 ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
 
 ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
-(* ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *} *)
+ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
 ML {*
 val preproc_timeout = SOME (seconds 5.0)
diff -r 8f6465f7021b -r 1c436a920730 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
@@ -163,10 +163,6 @@
 nitpick [expect = none]
 by (rule Rep_Nat_inverse)
 
-lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-(*nitpick [card = 1, unary_ints, max_potential = 0, expect = none] (?)*)
-by (rule Zero_int_def_raw)
-
 lemma "Abs_list (Rep_list a) = a"
 nitpick [card = 1\<emdash>2, expect = none]
 by (rule Rep_list_inverse)