src/HOL/Nitpick_Examples/Mono_Nits.thy

--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
@@ -30,7 +30,7 @@
    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} [] []
+fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{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),
@@ -46,26 +46,26 @@
 ML {* const @{term "(A::'a set) = A"} *}
 ML {* const @{term "(A::'a set set) = A"} *}
 ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
-ML {* const @{term "{{a}} = C"} *}
+ML {* const @{term "{{a::'a}} = C"} *}
 ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
-ML {* const @{term "A \<union> B"} *}
+ML {* const @{term "A \<union> (B::'a set)"} *}
 ML {* const @{term "P (a::'a)"} *}
 ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
 ML {* const @{term "\<forall>A::'a set. A a"} *}
 ML {* const @{term "\<forall>A::'a set. P A"} *}
 ML {* const @{term "P \<or> Q"} *}
-ML {* const @{term "A \<union> B = C"} *}
+ML {* const @{term "A \<union> B = (C::'a set)"} *}
 ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
-ML {* const @{term "let A = C in A \<union> B"} *}
+ML {* const @{term "let A = (C::'a set) in A \<union> B"} *}
 ML {* const @{term "THE x::'b. P x"} *}
-ML {* const @{term "{}::'a set"} *}
+ML {* const @{term "(\<lambda>x::'a. False)"} *}
 ML {* const @{term "(\<lambda>x::'a. True)"} *}
-ML {* const @{term "Let a A"} *}
+ML {* const @{term "Let (a::'a) A"} *}
 ML {* const @{term "A (a::'a)"} *}
-ML {* const @{term "insert a A = B"} *}
+ML {* const @{term "insert (a::'a) A = B"} *}
 ML {* const @{term "- (A::'a set)"} *}
-ML {* const @{term "finite A"} *}
-ML {* const @{term "\<not> finite A"} *}
+ML {* const @{term "finite (A::'a set)"} *}
+ML {* const @{term "\<not> finite (A::'a set)"} *}
 ML {* const @{term "finite (A::'a set set)"} *}
 ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
 ML {* const @{term "A < (B::'a set)"} *}
@@ -74,27 +74,25 @@
 ML {* const @{term "[a::'a set]"} *}
 ML {* const @{term "[A \<union> (B::'a set)]"} *}
 ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
-ML {* const @{term "\<forall>P. P a"} *}
 
-ML {* nonconst @{term "{%x. True}"} *}
-ML {* nonconst @{term "{(%x. x = a)} = C"} *}
+ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *}
 ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
 ML {* nonconst @{term "\<forall>a::'a. P a"} *}
 ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
-ML {* nonconst @{term "THE x. P x"} *}
-ML {* nonconst @{term "SOME x. P x"} *}
+ML {* nonconst @{term "THE x::'a. P x"} *}
+ML {* nonconst @{term "SOME x::'a. P x"} *}
 
 ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
 ML {* mono @{prop "P (a::'a)"} *}
-ML {* mono @{prop "{a} = {b}"} *}
+ML {* mono @{prop "{a} = {b::'a}"} *}
 ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
 ML {* mono @{prop "\<forall>F::'a set set. P"} *}
 ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
 ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
-ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
+ML {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *}
 
-ML {* nonmono @{prop "\<forall>x. P x"} *}
+ML {* nonmono @{prop "\<forall>x::'a. P x"} *}
+ML {* nonmono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *}
 ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
-ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
 
 end