Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Mini_Nits.thy
changeset 54845 10df188349b3
parent 54680 93f6d33a754e
child 58889 5b7a9633cfa8
equal deleted inserted replaced
54844:630ba4d8a206 54845:10df188349b3 
    11 imports Main
 
    11 imports Main
 
    12 begin
 
    12 begin
 
    13 
    13 
    14 ML_file "minipick.ML"
 
    14 ML_file "minipick.ML"
 
    15 
    15 
    16 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
 
    16 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
 
    17 
    17   total_consts = smart]
 
    18 nitpick_params [total_consts = smart]
 
       
    19 
    18 
    20 ML {*
 
    19 ML {*
 
    21 val check = Minipick.minipick @{context}
 
    20 val check = Minipick.minipick @{context}
 
    22 val expect = Minipick.minipick_expect @{context}
 
    21 val expect = Minipick.minipick_expect @{context}
 
    23 val none = expect "none"
 
    22 val none = expect "none"
 
    32 ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
 
    31 ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
 
    33 ML_val {* none 1 @{prop True} *}
 
    32 ML_val {* none 1 @{prop True} *}
 
    34 ML_val {* genuine 1 @{prop False} *}
 
    33 ML_val {* genuine 1 @{prop False} *}
 
    35 ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
 
    34 ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
 
    36 ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
 
    35 ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
 
    37 ML_val {* none 5 @{prop "\<forall>x. x = x"} *}
 
    36 ML_val {* none 4 @{prop "\<forall>x. x = x"} *}
 
    38 ML_val {* none 5 @{prop "\<exists>x. x = x"} *}
 
    37 ML_val {* none 4 @{prop "\<exists>x. x = x"} *}
 
    39 ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
 
    38 ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
 
    40 ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
 
    39 ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
 
    41 ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
 
    40 ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
 
    42 ML_val {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
 
    41 ML_val {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
 
    43 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
 
    42 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
 
    45 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
 
    44 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
 
    46 ML_val {* none 1 @{prop "All = Ex"} *}
 
    45 ML_val {* none 1 @{prop "All = Ex"} *}
 
    47 ML_val {* genuine 2 @{prop "All = Ex"} *}
 
    46 ML_val {* genuine 2 @{prop "All = Ex"} *}
 
    48 ML_val {* none 1 @{prop "All P = Ex P"} *}
 
    47 ML_val {* none 1 @{prop "All P = Ex P"} *}
 
    49 ML_val {* genuine 2 @{prop "All P = Ex P"} *}
 
    48 ML_val {* genuine 2 @{prop "All P = Ex P"} *}
 
    50 ML_val {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
 
    49 ML_val {* none 4 @{prop "x = y \<longrightarrow> P x = P y"} *}
 
    51 ML_val {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
 
    50 ML_val {* none 4 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
 
    52 ML_val {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
 
    51 ML_val {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
 
    53 ML_val {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
 
    52 ML_val {* none 4 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
 
    54 ML_val {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
 
    53 ML_val {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
 
    55 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
 
    54 ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
 
    56 ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
 
    55 ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
 
    57 ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
 
    56 ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
 
    58 ML_val {* none 1 @{prop "x = y"} *}
 
    57 ML_val {* none 1 @{prop "x = y"} *}
 
    62 ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
 
    61 ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
 
    63 ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
 
    62 ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
 
    64 ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
 
    63 ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
 
    65 ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
 
    64 ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
 
    66 ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
 
    65 ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
 
    67 ML_val {* none 5 @{prop "{a} = {a, a}"} *}
 
    66 ML_val {* none 4 @{prop "{a} = {a, a}"} *}
 
    68 ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
 
    67 ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
 
    69 ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
 
    68 ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
 
    70 ML_val {* none 5 @{prop "{}\<^sup>+ = {}"} *}
 
    69 ML_val {* none 4 @{prop "{}\<^sup>+ = {}"} *}
 
    71 ML_val {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
 
    70 ML_val {* none 4 @{prop "UNIV\<^sup>+ = UNIV"} *}
 
    72 ML_val {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
 
    71 ML_val {* none 4 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
 
    73 ML_val {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
 
    72 ML_val {* none 4 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
 
    74 ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    73 ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    75 ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    74 ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    76 ML_val {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    75 ML_val {* none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
 
    77 ML_val {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
 
    76 ML_val {* none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
 
    78 ML_val {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
 
    77 ML_val {* none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
 
    79 ML_val {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
 
    78 ML_val {* none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
 
    80 ML_val {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
 
    79 ML_val {* none 4 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
 
    81 ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
 
    80 ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
 
    82 ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
 
    81 ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
 
    83 ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
 
    82 ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
 
    84 ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
 
    83 ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
 
    85 ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
 
    84 ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
 
    86 ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
 
    85 ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
 
    87 ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
 
    86 ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
 
    88 ML_val {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
 
    87 ML_val {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
 
    89 ML_val {* none 5 @{prop "fst (a, b) = a"} *}
 
    88 ML_val {* none 4 @{prop "fst (a, b) = a"} *}
 
    90 ML_val {* none 1 @{prop "fst (a, b) = b"} *}
 
    89 ML_val {* none 1 @{prop "fst (a, b) = b"} *}
 
    91 ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
 
    90 ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
 
    92 ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
 
    91 ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
 
    93 ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
 
    92 ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
 
    94 ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
 
    93 ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
 
    95 ML_val {* none 5 @{prop "snd (a, b) = b"} *}
 
    94 ML_val {* none 4 @{prop "snd (a, b) = b"} *}
 
    96 ML_val {* none 1 @{prop "snd (a, b) = a"} *}
 
    95 ML_val {* none 1 @{prop "snd (a, b) = a"} *}
 
    97 ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
 
    96 ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
 
    98 ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
 
    97 ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
 
    99 ML_val {* genuine 1 @{prop P} *}
 
    98 ML_val {* genuine 1 @{prop P} *}
 
   100 ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
 
    99 ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
 
   101 ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
 
   100 ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
 
   102 ML_val {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
 
   101 ML_val {* none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
 
   103 ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
 
   102 ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
 
   104 ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
 
   103 ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
 
   105 ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
 
   104 ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
 
   106 ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
 
   105 ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
 
   107 ML_val {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
 
   106 ML_val {* none 4 @{prop "f = (\<lambda>x. f x)"} *}
 
   108 ML_val {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
 
   107 ML_val {* none 4 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
 
   109 ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
 
   108 ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y)"} *}
 
   110 ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
 
   109 ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
 
   111 
   110 
   112 end
 
   111 end
isabelle