author blanchet Tue, 02 Sep 2014 23:59:46 +0200 changeset 58143 7f7026ae9dc5 parent 58142 d6a2e3567f95 child 58144 00c878bd2093
tuned Refute example
```--- a/src/HOL/ex/Refute_Examples.thy	Tue Sep 02 16:38:26 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Sep 02 23:59:46 2014 +0200
@@ -943,7 +943,7 @@
oops

lemma "rec_X a b c d e f A = a"
-refute [maxsize = 3, expect = none]
+refute [maxsize = 2, expect = none]
by simp

lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
@@ -963,7 +963,7 @@
by simp

lemma "rec_Y a b c d e f F = f"
-refute [maxsize = 3, expect = none]
+refute [maxsize = 2, expect = none]
by simp

lemma "P (rec_X a b c d e f x)"
@@ -1216,50 +1216,14 @@
ypos :: 'b

lemma "(x::('a, 'b) point) = y"
-refute
+refute [expect = genuine]
oops

record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
ext :: 'c

lemma "(x::('a, 'b, 'c) extpoint) = y"
-refute
-oops
-
-(*****************************************************************************)
-
-subsubsection {* Inductively defined sets *}
-
-inductive_set arbitrarySet :: "'a set"
-where
-  "undefined : arbitrarySet"
-
-lemma "x : arbitrarySet"
-refute
-oops
-
-inductive_set evenCard :: "'a set set"
-where
-  "{} : evenCard"
-| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
-
-lemma "S : evenCard"
-refute
-oops
-
-consts f :: "'a \<Rightarrow> 'a"
-
-inductive_set
-  a_even :: "'a set"
-  and a_odd :: "'a set"
-where
-  "undefined : a_even"
-| "x : a_even \<Longrightarrow> f x : a_odd"
-| "x : a_odd \<Longrightarrow> f x : a_even"
-
-lemma "x : a_odd"
-(* refute [expect = genuine] -- {* finds a model of size 2 *}
-   NO LONGER WORKS since "lfp"'s interpreter is disabled *)
+refute [expect = genuine]
oops

(*****************************************************************************)
@@ -1267,7 +1231,7 @@
subsubsection {* Examples involving special functions *}

lemma "card x = 0"
-refute
+refute [expect = potential]
oops

lemma "finite x"
@@ -1303,15 +1267,15 @@
oops

lemma "f (lfp f) = lfp f"
-refute
+refute [expect = genuine]
oops

lemma "f (gfp f) = gfp f"
-refute
+refute [expect = genuine]
oops

lemma "lfp f = gfp f"
-refute
+refute [expect = genuine]
oops

(*****************************************************************************)```