# HG changeset patch
# User haftmann
# Date 1324738391 -3600
# Node ID deda685ba210cc1fbfbc64990ec3502c67453749
# Parent  b27e931326030fa891e85a345bc57f678a1599cb
commented out examples which choke on strict set/pred distinction

diff -r b27e93132603 -r deda685ba210 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -23,12 +23,11 @@
   pset  :: "'a set => 'a set"
   order :: "'a set => ('a * 'a) set"
 
-lemma "a \<in> {x. P x} \<Longrightarrow> P a"
+(*lemma "a \<in> {x. P x} \<Longrightarrow> P a"
 proof -
   assume "a \<in> {x. P x}"
-  hence "a \<in> P" by (metis Collect_def)
-  thus "P a" by (metis mem_def)
-qed
+  thus "P a" by metis
+qed*)
 
 lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
 by (metis mem_Collect_eq)
@@ -36,14 +35,14 @@
 lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
 by (metis Collect_imp_eq ComplD UnE)
 
-lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
+(*lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 proof -
   assume A1: "(a, b) \<in> Sigma A B"
   hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
   have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
   have "b \<in> B a" by (metis F1)
   thus "a \<in> A \<and> b \<in> B a" by (metis F2)
-qed
+qed*)
 
 lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 by (metis SigmaD1 SigmaD2)
@@ -51,7 +50,7 @@
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 by (metis (full_types, lam_lifting) CollectD SigmaD1 SigmaD2)
 
-lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+(*lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 proof -
   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
   hence F1: "a \<in> A" by (metis mem_Sigma_iff)
@@ -59,12 +58,12 @@
   hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
   hence "a = f b" by (unfold mem_def)
   thus "a \<in> A \<and> a = f b" by (metis F1)
-qed
+qed*)
 
 lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 by (metis Collect_mem_eq SigmaD2)
 
-lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
+(*lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 proof -
   assume A1: "(cl, f) \<in> CLF"
   assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
@@ -72,14 +71,14 @@
   have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
   hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
   thus "f \<in> pset cl" by (metis A1)
-qed
+qed*)
 
-lemma
+(*lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (no_types) Collect_def Sigma_triv mem_def)
+by (metis (no_types) Sigma_triv)*)
 
-lemma
+(*lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 proof -
@@ -87,14 +86,14 @@
   have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
   thus "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
-qed
+qed*)
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
 
-lemma
+(*lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 proof -
@@ -105,42 +104,42 @@
   hence "f \<in> Id_on cl `` pset cl" by metis
   hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
   thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
-qed
+qed*)
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
 by auto
 
-lemma
+(*lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)
+by (metis (lam_lifting) Sigma_triv subsetD)*)
 
-lemma
+(*lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) Int_Collect SigmaD2 inf1I mem_def)
+by (metis (lam_lifting) Int_Collect SigmaD2 inf1I mem_def)*)
 
-lemma
+(*lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)
+by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)*)
 
-lemma
+(*lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) Collect_def Sigma_triv mem_def)
+by (metis (lam_lifting) Collect_def Sigma_triv mem_def)*)
 
-lemma
+(*lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
-by auto
+by auto*)
 
 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
@@ -154,16 +153,16 @@
  apply (metis map.simps(1) zip_Nil)
 by auto
 
-lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
-by (metis Collect_def image_eqI mem_def subsetD)
+(*lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
+by (metis Collect_def image_eqI mem_def subsetD)*)
 
-lemma
+(*lemma
   "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
-by (metis Collect_def imageI mem_def set_rev_mp)
+by (metis Collect_def imageI mem_def set_rev_mp)*)
 
-lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
-by (metis (lam_lifting) imageE)
+(*lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
+by (metis (lam_lifting) imageE)*)
 
 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
 by (metis map_pair_def map_pair_surj_on)
diff -r b27e93132603 -r deda685ba210 src/HOL/Metis_Examples/Sets.thy
--- a/src/HOL/Metis_Examples/Sets.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -24,7 +24,7 @@
 sledgehammer_params [isar_proof, isar_shrink_factor = 1]
 
 (*multiple versions of this example*)
-lemma (*equal_union: *)
+(* lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
 proof -
   have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
@@ -200,5 +200,6 @@
   apply (metis mem_def)
  apply (metis all_not_in_conv)
 by (metis pair_in_Id_conv)
+*)
 
 end
diff -r b27e93132603 -r deda685ba210 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -52,9 +52,10 @@
   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
+    is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False}))
   end
 
 fun mono t = is_mono t orelse raise BUG
@@ -68,14 +69,14 @@
 ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
 ML {* const @{term "(A\<Colon>'a set) = A"} *}
 ML {* const @{term "(A\<Colon>'a set set) = A"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
+ML {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
 ML {* const @{term "{{a\<Colon>'a}} = C"} *}
 ML {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
 ML {* const @{term "A \<union> (B\<Colon>'a set)"} *}
 ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
 ML {* const @{term "P (a\<Colon>'a)"} *}
 ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
-ML {* const @{term "\<forall>A\<Colon>'a set. A a"} *}
+ML {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
 ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
 ML {* const @{term "P \<or> Q"} *}
 ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
@@ -91,9 +92,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)"} *}
@@ -119,14 +120,14 @@
 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> f a \<and> g a \<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 "P (a\<Colon>'a) \<and> P \<union> P = P"} *}
+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> f a \<and> g a \<longrightarrow> F h)"} *}
+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)"} *}
 ML {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
 ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
 ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
@@ -135,7 +136,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> f a \<and> g a \<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 b27e93132603 -r deda685ba210 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -513,11 +513,11 @@
 context complete_lattice
 begin
 
-lemma 
+(*lemma 
   assumes "Sup { a | i::bool . True } \<le> Sup { b | i::bool . True }"
   and     "Sup { b | i::bool . True } \<le> Sup { a | i::bool . True }"
   shows   "Sup { a | i::bool . True } \<le> Sup { a | i::bool . True }"
-  using assms by (smt order_trans)
+  using assms by (smt order_trans)*)
 
 end
 
diff -r b27e93132603 -r deda685ba210 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -6,7 +6,7 @@
 header {* Examples for the 'quickcheck' command *}
 
 theory Quickcheck_Examples
-imports Complex_Main "~~/src/HOL/Library/Dlist"
+imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/More_Set"
 begin
 
 text {*
@@ -271,12 +271,12 @@
 
 lemma
   "acyclic R ==> acyclic S ==> acyclic (R Un S)"
-quickcheck[expect = counterexample]
+(* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
 oops
 
 lemma
   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
-quickcheck[expect = counterexample]
+(* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
 oops
 
 
diff -r b27e93132603 -r deda685ba210 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Sat Dec 24 15:53:11 2011 +0100
@@ -110,7 +110,7 @@
 oops
 
 lemma "distinct [a,b]"
-  refute
+  (*refute*)
   apply simp
   refute
 oops
@@ -379,44 +379,44 @@
 subsubsection {* Sets *}
 
 lemma "P (A::'a set)"
-  refute
+ (* refute *)
 oops
 
 lemma "P (A::'a set set)"
-  refute
+ (* refute *)
 oops
 
 lemma "{x. P x} = {y. P y}"
-  refute
+ (* refute *)
   apply simp
 done
 
 lemma "x : {x. P x}"
-  refute
+ (* refute *)
 oops
 
 lemma "P op:"
-  refute
+ (* refute *)
 oops
 
 lemma "P (op: x)"
-  refute
+ (* refute *)
 oops
 
 lemma "P Collect"
-  refute
+ (* refute *)
 oops
 
 lemma "A Un B = A Int B"
-  refute
+ (* refute *)
 oops
 
 lemma "(A Int B) Un C = (A Un C) Int B"
-  refute
+ (* refute *)
 oops
 
 lemma "Ball A P \<longrightarrow> Bex A P"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
@@ -500,7 +500,7 @@
   unfolding myTdef_def by auto
 
 lemma "(x::'a myTdef) = y"
-  refute
+ (* refute *)
 oops
 
 typedecl myTdecl
@@ -511,7 +511,7 @@
   unfolding T_bij_def by auto
 
 lemma "P (f::(myTdecl myTdef) T_bij)"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
@@ -1310,14 +1310,14 @@
   ypos :: 'b
 
 lemma "(x::('a, 'b) point) = y"
-  refute
+ (* refute *)
 oops
 
 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
   ext :: 'c
 
 lemma "(x::('a, 'b, 'c) extpoint) = y"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
@@ -1329,7 +1329,7 @@
   "undefined : arbitrarySet"
 
 lemma "x : arbitrarySet"
-  refute
+ (* refute *)
 oops
 
 inductive_set evenCard :: "'a set set"
@@ -1338,7 +1338,7 @@
 | "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
 
 lemma "S : evenCard"
-  refute
+ (* refute *)
 oops
 
 inductive_set
@@ -1374,11 +1374,11 @@
 subsubsection {* Examples involving special functions *}
 
 lemma "card x = 0"
-  refute
+ (* refute *)
 oops
 
 lemma "finite x"
-  refute  -- {* no finite countermodel exists *}
+ (* refute *) -- {* no finite countermodel exists *}
 oops
 
 lemma "(x::nat) + y = 0"
@@ -1410,15 +1410,15 @@
 oops
 
 lemma "f (lfp f) = lfp f"
-  refute
+ (* refute *)
 oops
 
 lemma "f (gfp f) = gfp f"
-  refute
+ (* refute *)
 oops
 
 lemma "lfp f = gfp f"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
@@ -1494,7 +1494,7 @@
 oops
 
 lemma "P (inverse (S::'a set))"
-  refute
+ (* refute*)
 oops
 
 lemma "P (inverse (p::'a\<times>'b))"
@@ -1515,3 +1515,4 @@
 refute_params [satsolver="auto"]
 
 end
+