src/HOL/Nitpick_Examples/Typedef_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@33197
     1
(*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2011
blanchet@33197
     4
blanchet@33197
     5
Examples featuring Nitpick applied to typedefs.
blanchet@33197
     6
*)
blanchet@33197
     7
wenzelm@58889
     8
section {* Examples Featuring Nitpick Applied to Typedefs *}
blanchet@33197
     9
blanchet@33197
    10
theory Typedef_Nits
haftmann@35372
    11
imports Complex_Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@55893
    14
nitpick_params [verbose, card = 1-4, sat_solver = MiniSat_JNI, max_threads = 1,
krauss@42208
    15
                timeout = 240]
blanchet@33197
    16
wenzelm@61076
    17
definition "three = {0::nat, 1, 2}"
wenzelm@49834
    18
typedef three = three
wenzelm@45694
    19
unfolding three_def by blast
blanchet@33197
    20
blanchet@33197
    21
definition A :: three where "A \<equiv> Abs_three 0"
blanchet@33197
    22
definition B :: three where "B \<equiv> Abs_three 1"
blanchet@33197
    23
definition C :: three where "C \<equiv> Abs_three 2"
blanchet@33197
    24
wenzelm@61076
    25
lemma "x = (y::three)"
blanchet@33197
    26
nitpick [expect = genuine]
blanchet@33197
    27
oops
blanchet@33197
    28
wenzelm@61076
    29
definition "one_or_two = {undefined False::'a, undefined True}"
wenzelm@45694
    30
wenzelm@49834
    31
typedef 'a one_or_two = "one_or_two :: 'a set"
wenzelm@45694
    32
unfolding one_or_two_def by auto
blanchet@33197
    33
wenzelm@61076
    34
lemma "x = (y::unit one_or_two)"
blanchet@33197
    35
nitpick [expect = none]
blanchet@33197
    36
sorry
blanchet@33197
    37
wenzelm@61076
    38
lemma "x = (y::bool one_or_two)"
blanchet@33197
    39
nitpick [expect = genuine]
blanchet@33197
    40
oops
blanchet@33197
    41
wenzelm@61076
    42
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y::bool one_or_two)"
blanchet@33197
    43
nitpick [expect = none]
blanchet@33197
    44
sorry
blanchet@33197
    45
wenzelm@61076
    46
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y::bool one_or_two). x \<noteq> y"
blanchet@33197
    47
nitpick [card = 1, expect = potential] (* unfortunate *)
blanchet@33197
    48
oops
blanchet@33197
    49
wenzelm@61076
    50
lemma "\<exists>x (y::bool one_or_two). x \<noteq> y"
blanchet@33197
    51
nitpick [card = 1, expect = potential] (* unfortunate *)
blanchet@33197
    52
nitpick [card = 2, expect = none]
blanchet@33197
    53
oops
blanchet@33197
    54
wenzelm@61076
    55
definition "bounded = {n::nat. finite (UNIV :: 'a set) \<longrightarrow> n < card (UNIV :: 'a set)}"
haftmann@45970
    56
wenzelm@49834
    57
typedef 'a bounded = "bounded(TYPE('a))"
wenzelm@45694
    58
unfolding bounded_def
blanchet@33197
    59
apply (rule_tac x = 0 in exI)
blanchet@33197
    60
apply (case_tac "card UNIV = 0")
blanchet@33197
    61
by auto
blanchet@33197
    62
wenzelm@61076
    63
lemma "x = (y::unit bounded)"
blanchet@33197
    64
nitpick [expect = none]
blanchet@33197
    65
sorry
blanchet@33197
    66
wenzelm@61076
    67
lemma "x = (y::bool bounded)"
blanchet@33197
    68
nitpick [expect = genuine]
blanchet@33197
    69
oops
blanchet@33197
    70
wenzelm@61076
    71
lemma "x \<noteq> (y::bool bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@39362
    72
nitpick [expect = potential] (* unfortunate *)
blanchet@33197
    73
sorry
blanchet@33197
    74
wenzelm@61076
    75
lemma "x \<noteq> (y::(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@55893
    76
nitpick [card = 1-5, expect = genuine]
blanchet@33197
    77
oops
blanchet@33197
    78
wenzelm@61076
    79
lemma "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
blanchet@33197
    80
nitpick [expect = none]
blanchet@33197
    81
by (rule True_def)
blanchet@33197
    82
blanchet@33197
    83
lemma "False \<equiv> \<forall>P. P"
blanchet@33197
    84
nitpick [expect = none]
blanchet@33197
    85
by (rule False_def)
blanchet@33197
    86
blanchet@33197
    87
lemma "() = Abs_unit True"
blanchet@33197
    88
nitpick [expect = none]
blanchet@33197
    89
by (rule Unity_def)
blanchet@33197
    90
blanchet@33197
    91
lemma "() = Abs_unit False"
blanchet@33197
    92
nitpick [expect = none]
blanchet@33197
    93
by simp
blanchet@33197
    94
blanchet@33197
    95
lemma "Rep_unit () = True"
blanchet@33197
    96
nitpick [expect = none]
huffman@40590
    97
by (insert Rep_unit) simp
blanchet@33197
    98
blanchet@33197
    99
lemma "Rep_unit () = False"
blanchet@33197
   100
nitpick [expect = genuine]
blanchet@33197
   101
oops
blanchet@33197
   102
blanchet@37400
   103
lemma "Pair a b = Abs_prod (Pair_Rep a b)"
blanchet@55893
   104
nitpick [card = 1-2, expect = none]
blanchet@33197
   105
by (rule Pair_def)
blanchet@33197
   106
blanchet@37400
   107
lemma "Pair a b = Abs_prod (Pair_Rep b a)"
blanchet@55893
   108
nitpick [card = 1-2, expect = none]
blanchet@33197
   109
nitpick [dont_box, expect = genuine]
blanchet@33197
   110
oops
blanchet@33197
   111
blanchet@37400
   112
lemma "fst (Abs_prod (Pair_Rep a b)) = a"
blanchet@33197
   113
nitpick [card = 2, expect = none]
blanchet@37400
   114
by (simp add: Pair_def [THEN sym])
blanchet@33197
   115
blanchet@37400
   116
lemma "fst (Abs_prod (Pair_Rep a b)) = b"
blanchet@55893
   117
nitpick [card = 1-2, expect = none]
blanchet@33197
   118
nitpick [dont_box, expect = genuine]
blanchet@33197
   119
oops
blanchet@33197
   120
blanchet@33197
   121
lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
blanchet@33197
   122
nitpick [expect = none]
blanchet@33197
   123
apply (rule ccontr)
blanchet@33197
   124
apply simp
blanchet@37400
   125
apply (drule subst [where P = "\<lambda>r. Abs_prod r = Abs_prod (Pair_Rep a b)"])
blanchet@33197
   126
 apply (rule refl)
blanchet@37400
   127
by (simp add: Pair_def [THEN sym])
blanchet@33197
   128
blanchet@37400
   129
lemma "Abs_prod (Rep_prod a) = a"
blanchet@33197
   130
nitpick [card = 2, expect = none]
blanchet@37400
   131
by (rule Rep_prod_inverse)
blanchet@33197
   132
blanchet@37400
   133
lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inl_Rep a)"
blanchet@33197
   134
nitpick [card = 1, expect = none]
blanchet@37400
   135
by (simp add: Inl_def o_def)
blanchet@33197
   136
blanchet@37400
   137
lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inr_Rep a)"
blanchet@33197
   138
nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
blanchet@33197
   139
oops
blanchet@33197
   140
blanchet@33197
   141
lemma "Inl_Rep a \<noteq> Inr_Rep a"
blanchet@33197
   142
nitpick [expect = none]
blanchet@33197
   143
by (rule Inl_Rep_not_Inr_Rep)
blanchet@33197
   144
blanchet@37400
   145
lemma "Abs_sum (Rep_sum a) = a"
blanchet@35284
   146
nitpick [card = 1, expect = none]
blanchet@35284
   147
nitpick [card = 2, expect = none]
blanchet@37400
   148
by (rule Rep_sum_inverse)
blanchet@33197
   149
blanchet@33197
   150
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
blanchet@35312
   151
nitpick [expect = none]
wenzelm@46905
   152
by (rule Zero_nat_def [abs_def])
blanchet@33197
   153
blanchet@37400
   154
lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
blanchet@35312
   155
nitpick [expect = none]
huffman@46547
   156
by (rule Nat.Suc_def)
blanchet@33197
   157
blanchet@37400
   158
lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
blanchet@33197
   159
nitpick [expect = genuine]
blanchet@33197
   160
oops
blanchet@33197
   161
blanchet@33197
   162
lemma "Abs_Nat (Rep_Nat a) = a"
blanchet@33197
   163
nitpick [expect = none]
blanchet@33197
   164
by (rule Rep_Nat_inverse)
blanchet@33197
   165
blanchet@33197
   166
lemma "Abs_list (Rep_list a) = a"
blanchet@55893
   167
(* nitpick [card = 1-2, expect = none] FIXME *)
blanchet@33197
   168
by (rule Rep_list_inverse)
blanchet@33197
   169
blanchet@33197
   170
record point =
blanchet@33197
   171
  Xcoord :: int
blanchet@33197
   172
  Ycoord :: int
blanchet@33197
   173
haftmann@38542
   174
lemma "Abs_point_ext (Rep_point_ext a) = a"
blanchet@33571
   175
nitpick [expect = none]
haftmann@38542
   176
by (fact Rep_point_ext_inverse)
blanchet@33197
   177
blanchet@33197
   178
lemma "Fract a b = of_int a / of_int b"
blanchet@33737
   179
nitpick [card = 1, expect = none]
blanchet@33197
   180
by (rule Fract_of_int_quotient)
blanchet@33197
   181
huffman@47908
   182
lemma "Abs_rat (Rep_rat a) = a"
blanchet@33737
   183
nitpick [card = 1, expect = none]
huffman@47908
   184
by (rule Rep_rat_inverse)
blanchet@33197
   185
wenzelm@61076
   186
typedef check = "{x::nat. x < 2}" by (rule exI[of _ 0], auto)
blanchet@51706
   187
blanchet@51706
   188
lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2"
blanchet@55893
   189
nitpick [card = 1-3, expect = none]
blanchet@51706
   190
using Rep_check[of "Abs_check n"] by auto
blanchet@51706
   191
blanchet@51706
   192
lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1"
blanchet@55893
   193
nitpick [card = 1-3, expect = genuine]
blanchet@51706
   194
oops
blanchet@51706
   195
blanchet@33197
   196
end