src/HOL/Nitpick_Examples/Mini_Nits.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61076 bdc1e2f0a86a
child 63167 0909deb8059b
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
blanchet@45035
     1
(*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
blanchet@45035
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2011
blanchet@45035
     4
blanchet@45035
     5
Examples featuring Minipick, the minimalistic version of Nitpick.
blanchet@45035
     6
*)
blanchet@45035
     7
wenzelm@58889
     8
section {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
blanchet@45035
     9
blanchet@45035
    10
theory Mini_Nits
blanchet@45035
    11
imports Main
blanchet@45035
    12
begin
blanchet@45035
    13
wenzelm@48891
    14
ML_file "minipick.ML"
wenzelm@48891
    15
blanchet@54845
    16
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
blanchet@54845
    17
  total_consts = smart]
blanchet@45035
    18
blanchet@45062
    19
ML {*
blanchet@45062
    20
val check = Minipick.minipick @{context}
blanchet@45062
    21
val expect = Minipick.minipick_expect @{context}
blanchet@45062
    22
val none = expect "none"
blanchet@45062
    23
val genuine = expect "genuine"
blanchet@45062
    24
val unknown = expect "unknown"
blanchet@45035
    25
*}
blanchet@45035
    26
wenzelm@51272
    27
ML_val {* genuine 1 @{prop "x = Not"} *}
wenzelm@51272
    28
ML_val {* none 1 @{prop "\<exists>x. x = Not"} *}
wenzelm@51272
    29
ML_val {* none 1 @{prop "\<not> False"} *}
wenzelm@51272
    30
ML_val {* genuine 1 @{prop "\<not> True"} *}
wenzelm@51272
    31
ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
wenzelm@51272
    32
ML_val {* none 1 @{prop True} *}
wenzelm@51272
    33
ML_val {* genuine 1 @{prop False} *}
wenzelm@51272
    34
ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
wenzelm@51272
    35
ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
blanchet@54845
    36
ML_val {* none 4 @{prop "\<forall>x. x = x"} *}
blanchet@54845
    37
ML_val {* none 4 @{prop "\<exists>x. x = x"} *}
wenzelm@51272
    38
ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
wenzelm@51272
    39
ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
wenzelm@51272
    40
ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
wenzelm@61076
    41
ML_val {* none 2 @{prop "\<forall>x::'a \<times> 'a. x = x"} *}
wenzelm@61076
    42
ML_val {* none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"} *}
wenzelm@61076
    43
ML_val {* genuine 2 @{prop "\<forall>x::'a \<times> 'a. x = y"} *}
wenzelm@61076
    44
ML_val {* none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"} *}
wenzelm@51272
    45
ML_val {* none 1 @{prop "All = Ex"} *}
wenzelm@51272
    46
ML_val {* genuine 2 @{prop "All = Ex"} *}
wenzelm@51272
    47
ML_val {* none 1 @{prop "All P = Ex P"} *}
wenzelm@51272
    48
ML_val {* genuine 2 @{prop "All P = Ex P"} *}
blanchet@54845
    49
ML_val {* none 4 @{prop "x = y \<longrightarrow> P x = P y"} *}
wenzelm@61076
    50
ML_val {* none 4 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
wenzelm@61076
    51
ML_val {* none 2 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
wenzelm@61076
    52
ML_val {* none 4 @{prop "\<exists>x::'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
wenzelm@61076
    53
ML_val {* none 2 @{prop "(x::'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
wenzelm@61076
    54
ML_val {* none 2 @{prop "\<exists>x::'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
wenzelm@51272
    55
ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
wenzelm@51272
    56
ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
wenzelm@51272
    57
ML_val {* none 1 @{prop "x = y"} *}
wenzelm@51272
    58
ML_val {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
wenzelm@51272
    59
ML_val {* genuine 2 @{prop "x = y"} *}
wenzelm@51272
    60
ML_val {* genuine 1 @{prop "X \<subseteq> Y"} *}
wenzelm@51272
    61
ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
wenzelm@51272
    62
ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
wenzelm@51272
    63
ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
wenzelm@51272
    64
ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
wenzelm@51272
    65
ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
blanchet@54845
    66
ML_val {* none 4 @{prop "{a} = {a, a}"} *}
wenzelm@51272
    67
ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
wenzelm@51272
    68
ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
blanchet@54845
    69
ML_val {* none 4 @{prop "{}\<^sup>+ = {}"} *}
blanchet@54845
    70
ML_val {* none 4 @{prop "UNIV\<^sup>+ = UNIV"} *}
wenzelm@61076
    71
ML_val {* none 4 @{prop "(UNIV :: ('a \<times> 'b) set) - {} = UNIV"} *}
wenzelm@61076
    72
ML_val {* none 4 @{prop "{} - (UNIV :: ('a \<times> 'b) set) = {}"} *}
wenzelm@51272
    73
ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
wenzelm@51272
    74
ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
blanchet@54845
    75
ML_val {* none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
blanchet@54845
    76
ML_val {* none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
blanchet@54845
    77
ML_val {* none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
blanchet@54845
    78
ML_val {* none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
blanchet@54845
    79
ML_val {* none 4 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
wenzelm@51272
    80
ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
wenzelm@51272
    81
ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
wenzelm@61076
    82
ML_val {* none 4 @{prop "\<exists>a b::'a \<times> 'a. (a, b) = (b, a)"} *}
wenzelm@61076
    83
ML_val {* genuine 2 @{prop "(a::'a \<times> 'a, b) = (b, a)"} *}
wenzelm@61076
    84
ML_val {* none 4 @{prop "\<exists>a b::'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
wenzelm@61076
    85
ML_val {* genuine 2 @{prop "(a::'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
wenzelm@61076
    86
ML_val {* none 4 @{prop "\<exists>a b::'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
wenzelm@61076
    87
ML_val {* genuine 1 @{prop "(a::'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
blanchet@54845
    88
ML_val {* none 4 @{prop "fst (a, b) = a"} *}
wenzelm@51272
    89
ML_val {* none 1 @{prop "fst (a, b) = b"} *}
wenzelm@51272
    90
ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
wenzelm@51272
    91
ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
wenzelm@51272
    92
ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
wenzelm@51272
    93
ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
blanchet@54845
    94
ML_val {* none 4 @{prop "snd (a, b) = b"} *}
wenzelm@51272
    95
ML_val {* none 1 @{prop "snd (a, b) = a"} *}
wenzelm@51272
    96
ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
wenzelm@51272
    97
ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
wenzelm@51272
    98
ML_val {* genuine 1 @{prop P} *}
wenzelm@51272
    99
ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
wenzelm@51272
   100
ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
blanchet@54845
   101
ML_val {* none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
wenzelm@51272
   102
ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
wenzelm@51272
   103
ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
wenzelm@51272
   104
ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
wenzelm@51272
   105
ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
blanchet@54845
   106
ML_val {* none 4 @{prop "f = (\<lambda>x. f x)"} *}
wenzelm@61076
   107
ML_val {* none 4 @{prop "f = (\<lambda>x. f x::'a \<Rightarrow> bool)"} *}
blanchet@54845
   108
ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y)"} *}
wenzelm@61076
   109
ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y::'a \<Rightarrow> bool)"} *}
blanchet@45035
   110
blanchet@45035
   111
end