src/HOL/Nitpick_Examples/Integer_Nits.thy
author wenzelm
Sat, 25 Feb 2012 12:34:56 +0100
changeset 46665 919dfcdf6d8a
parent 46090 f1796596ef60
child 47108 2a1953f0d20d
permissions -rw-r--r--
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
45035
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 42959
diff changeset
     3
    Copyright   2009-2011
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     4
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     5
Examples featuring Nitpick applied to natural numbers and integers.
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     6
*)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     7
46090
f1796596ef60 tuned import
blanchet
parents: 45035
diff changeset
     8
header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
     9
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    10
theory Integer_Nits
46090
f1796596ef60 tuned import
blanchet
parents: 45035
diff changeset
    11
imports Main
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    12
begin
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    13
42959
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42208
diff changeset
    14
nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
42208
02513eb26eb7 raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
krauss
parents: 41278
diff changeset
    15
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    16
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    17
lemma "Suc x = x + 1"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    18
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    19
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    20
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    21
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    22
lemma "x < Suc x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    23
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    24
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    25
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    26
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    27
lemma "x + y \<ge> (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    28
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    29
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    30
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    31
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    32
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    33
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    34
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    35
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    36
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    37
lemma "x + y = y + (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    38
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    39
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    40
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    41
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    42
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    43
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    44
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    45
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    46
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    47
lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    48
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    49
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    50
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    51
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    52
lemma "x - (0::nat) = x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    53
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    54
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    55
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    56
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    57
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    58
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    59
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    60
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    61
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    62
lemma "0 * y = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    63
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    64
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    65
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    66
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    67
lemma "y * 0 = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    68
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    69
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    70
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    71
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    72
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    73
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    74
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    75
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    76
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    77
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    78
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    79
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    80
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    81
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    82
lemma "x * y div y = (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    83
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    84
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    85
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    86
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    87
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    88
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    89
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    90
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    91
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    92
lemma "5 * 55 < (260::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    93
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    94
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    95
nitpick [binary_ints, bits = 9, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    96
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    97
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    98
lemma "nat (of_nat n) = n"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
    99
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   100
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   101
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   102
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   103
lemma "x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   104
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   105
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   106
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   107
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   108
lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   109
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   110
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   111
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   112
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   113
lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   114
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   115
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   116
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   117
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   118
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   119
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   120
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   121
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   122
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   123
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   124
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   125
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   126
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   127
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   128
lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   129
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   130
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   131
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   132
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   133
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   134
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   135
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   136
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   137
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   138
lemma "x + y = y + (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   139
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   140
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   141
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   142
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   143
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   144
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   145
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   146
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   147
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   148
lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   149
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   150
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   151
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   152
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   153
lemma "x - (0::int) = x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   154
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   155
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   156
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   157
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   158
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   159
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   160
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   161
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   162
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   163
lemma "0 * y = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   164
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   165
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   166
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   167
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   168
lemma "y * 0 = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   169
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   170
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   171
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   172
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   173
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   174
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   175
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   176
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   177
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   178
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   179
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   180
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   181
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   182
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   183
lemma "x * y div y = (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   184
nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   185
nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   186
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   187
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   188
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   189
nitpick [unary_ints, expect = none]
42959
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42208
diff changeset
   190
nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   191
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   192
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   193
lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   194
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   195
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   196
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   197
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   198
lemma "-5 * 55 > (-260::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   199
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   200
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   201
nitpick [binary_ints, bits = 9, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   202
oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   203
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   204
lemma "nat (of_nat n) = n"
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   205
nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   206
nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   207
sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   208
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   209
datatype tree = Null | Node nat tree tree
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   210
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   211
primrec labels where
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   212
"labels Null = {}" |
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   213
"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   214
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   215
lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 35695
diff changeset
   216
nitpick [expect = potential] (* unfortunate *)
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   217
nitpick [dont_finitize, expect = potential]
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   218
oops
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   219
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   220
lemma "labels (Node x t u) \<noteq> {}"
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   221
nitpick [expect = none]
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   222
oops
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   223
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   224
lemma "card (labels t) > 0"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 35695
diff changeset
   225
nitpick [expect = potential] (* unfortunate *)
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   226
nitpick [dont_finitize, expect = potential]
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   227
oops
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   228
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   229
lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 35695
diff changeset
   230
nitpick [expect = potential] (* unfortunate *)
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   231
nitpick [dont_finitize, expect = potential]
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   232
oops
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   233
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   234
lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
39362
ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents: 38185
diff changeset
   235
nitpick [expect = potential] (* unfortunate *)
ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents: 38185
diff changeset
   236
nitpick [dont_finitize, expect = potential]
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   237
sorry
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   238
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   239
lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
39362
ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents: 38185
diff changeset
   240
nitpick [expect = potential] (* unfortunate *)
ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents: 38185
diff changeset
   241
nitpick [dont_finitize, expect = potential]
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   242
oops
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35078
diff changeset
   243
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents:
diff changeset
   244
end