author | wenzelm |
Mon, 22 May 2017 23:24:25 +0200 | |
changeset 65907 | 637d18b325d0 |
parent 63167 | 0909deb8059b |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
45035 | 1 |
(* Title: HOL/Nitpick_Examples/Mini_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2009-2011 |
|
4 |
||
5 |
Examples featuring Minipick, the minimalistic version of Nitpick. |
|
6 |
*) |
|
7 |
||
63167 | 8 |
section \<open>Examples Featuring Minipick, the Minimalistic Version of Nitpick\<close> |
45035 | 9 |
|
10 |
theory Mini_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
48891 | 14 |
ML_file "minipick.ML" |
15 |
||
54845 | 16 |
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1, |
17 |
total_consts = smart] |
|
45035 | 18 |
|
63167 | 19 |
ML \<open> |
45062
9598cada31b3
first step towards extending Minipick with more translations
blanchet
parents:
45035
diff
changeset
|
20 |
val check = Minipick.minipick @{context} |
9598cada31b3
first step towards extending Minipick with more translations
blanchet
parents:
45035
diff
changeset
|
21 |
val expect = Minipick.minipick_expect @{context} |
9598cada31b3
first step towards extending Minipick with more translations
blanchet
parents:
45035
diff
changeset
|
22 |
val none = expect "none" |
9598cada31b3
first step towards extending Minipick with more translations
blanchet
parents:
45035
diff
changeset
|
23 |
val genuine = expect "genuine" |
9598cada31b3
first step towards extending Minipick with more translations
blanchet
parents:
45035
diff
changeset
|
24 |
val unknown = expect "unknown" |
63167 | 25 |
\<close> |
45035 | 26 |
|
65907
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
27 |
ML \<open>genuine 1 @{prop "x = Not"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
28 |
ML \<open>none 1 @{prop "\<exists>x. x = Not"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
29 |
ML \<open>none 1 @{prop "\<not> False"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
30 |
ML \<open>genuine 1 @{prop "\<not> True"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
31 |
ML \<open>none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
32 |
ML \<open>none 1 @{prop True}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
33 |
ML \<open>genuine 1 @{prop False}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
34 |
ML \<open>genuine 1 @{prop "True \<longleftrightarrow> False"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
35 |
ML \<open>none 1 @{prop "True \<longleftrightarrow> \<not> False"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
36 |
ML \<open>none 4 @{prop "\<forall>x. x = x"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
37 |
ML \<open>none 4 @{prop "\<exists>x. x = x"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
38 |
ML \<open>none 1 @{prop "\<forall>x. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
39 |
ML \<open>genuine 2 @{prop "\<forall>x. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
40 |
ML \<open>none 2 @{prop "\<exists>x. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
41 |
ML \<open>none 2 @{prop "\<forall>x::'a \<times> 'a. x = x"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
42 |
ML \<open>none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
43 |
ML \<open>genuine 2 @{prop "\<forall>x::'a \<times> 'a. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
44 |
ML \<open>none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
45 |
ML \<open>none 1 @{prop "All = Ex"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
46 |
ML \<open>genuine 2 @{prop "All = Ex"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
47 |
ML \<open>none 1 @{prop "All P = Ex P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
48 |
ML \<open>genuine 2 @{prop "All P = Ex P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
49 |
ML \<open>none 4 @{prop "x = y \<longrightarrow> P x = P y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
50 |
ML \<open>none 4 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x = P y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
51 |
ML \<open>none 2 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x y = P y x"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
52 |
ML \<open>none 4 @{prop "\<exists>x::'a \<times> 'a. x = y \<longrightarrow> P x = P y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
53 |
ML \<open>none 2 @{prop "(x::'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
54 |
ML \<open>none 2 @{prop "\<exists>x::'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
55 |
ML \<open>genuine 1 @{prop "(op =) X = Ex"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
56 |
ML \<open>none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
57 |
ML \<open>none 1 @{prop "x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
58 |
ML \<open>genuine 1 @{prop "x \<longleftrightarrow> y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
59 |
ML \<open>genuine 2 @{prop "x = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
60 |
ML \<open>genuine 1 @{prop "X \<subseteq> Y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
61 |
ML \<open>none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
62 |
ML \<open>none 1 @{prop "P \<and> Q \<longrightarrow> P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
63 |
ML \<open>none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
64 |
ML \<open>genuine 1 @{prop "P \<or> Q \<longrightarrow> P"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
65 |
ML \<open>none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
66 |
ML \<open>none 4 @{prop "{a} = {a, a}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
67 |
ML \<open>genuine 2 @{prop "{a} = {a, b}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
68 |
ML \<open>genuine 1 @{prop "{a} \<noteq> {a, b}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
69 |
ML \<open>none 4 @{prop "{}\<^sup>+ = {}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
70 |
ML \<open>none 4 @{prop "UNIV\<^sup>+ = UNIV"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
71 |
ML \<open>none 4 @{prop "(UNIV :: ('a \<times> 'b) set) - {} = UNIV"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
72 |
ML \<open>none 4 @{prop "{} - (UNIV :: ('a \<times> 'b) set) = {}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
73 |
ML \<open>none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
74 |
ML \<open>genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
75 |
ML \<open>none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
76 |
ML \<open>none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
77 |
ML \<open>none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
78 |
ML \<open>none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
79 |
ML \<open>none 4 @{prop "\<exists>a b. (a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
80 |
ML \<open>genuine 2 @{prop "(a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
81 |
ML \<open>genuine 2 @{prop "(a, b) \<noteq> (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
82 |
ML \<open>none 4 @{prop "\<exists>a b::'a \<times> 'a. (a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
83 |
ML \<open>genuine 2 @{prop "(a::'a \<times> 'a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
84 |
ML \<open>none 4 @{prop "\<exists>a b::'a \<times> 'a \<times> 'a. (a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
85 |
ML \<open>genuine 2 @{prop "(a::'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
86 |
ML \<open>none 4 @{prop "\<exists>a b::'a \<Rightarrow> 'a. (a, b) = (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
87 |
ML \<open>genuine 1 @{prop "(a::'a \<Rightarrow> 'a, b) \<noteq> (b, a)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
88 |
ML \<open>none 4 @{prop "fst (a, b) = a"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
89 |
ML \<open>none 1 @{prop "fst (a, b) = b"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
90 |
ML \<open>genuine 2 @{prop "fst (a, b) = b"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
91 |
ML \<open>genuine 2 @{prop "fst (a, b) \<noteq> b"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
92 |
ML \<open>genuine 2 @{prop "f ((x, z), y) = (x, z)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
93 |
ML \<open>none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
94 |
ML \<open>none 4 @{prop "snd (a, b) = b"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
95 |
ML \<open>none 1 @{prop "snd (a, b) = a"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
96 |
ML \<open>genuine 2 @{prop "snd (a, b) = a"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
97 |
ML \<open>genuine 2 @{prop "snd (a, b) \<noteq> a"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
98 |
ML \<open>genuine 1 @{prop P}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
99 |
ML \<open>genuine 1 @{prop "(\<lambda>x. P) a"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
100 |
ML \<open>genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
101 |
ML \<open>none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
102 |
ML \<open>genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
103 |
ML \<open>none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
104 |
ML \<open>none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
105 |
ML \<open>genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
106 |
ML \<open>none 4 @{prop "f = (\<lambda>x. f x)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
107 |
ML \<open>none 4 @{prop "f = (\<lambda>x. f x::'a \<Rightarrow> bool)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
108 |
ML \<open>none 4 @{prop "f = (\<lambda>x y. f x y)"}\<close> |
637d18b325d0
less ambitious parallelism to make this work more robustly on Windows;
wenzelm
parents:
63167
diff
changeset
|
109 |
ML \<open>none 4 @{prop "f = (\<lambda>x y. f x y::'a \<Rightarrow> bool)"}\<close> |
45035 | 110 |
|
111 |
end |