src/HOL/Nitpick_Examples/Typedef_Nits.thy
author nipkow
Mon Jan 30 21:49:41 2012 +0100 (2012-01-30)
changeset 46372 6fa9cdb8b850
parent 46082 1c436a920730
child 46547 d1dcb91a512e
permissions -rw-r--r--
added "'a rel"
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
blanchet@33197
     8
header {* 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@42959
    14
nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
krauss@42208
    15
                timeout = 240]
blanchet@33197
    16
wenzelm@45694
    17
definition "three = {0\<Colon>nat, 1, 2}"
wenzelm@45694
    18
typedef (open) 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
blanchet@33197
    25
lemma "x = (y\<Colon>three)"
blanchet@33197
    26
nitpick [expect = genuine]
blanchet@33197
    27
oops
blanchet@33197
    28
wenzelm@45694
    29
definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
wenzelm@45694
    30
wenzelm@45694
    31
typedef (open) 'a one_or_two = "one_or_two :: 'a set"
wenzelm@45694
    32
unfolding one_or_two_def by auto
blanchet@33197
    33
blanchet@33197
    34
lemma "x = (y\<Colon>unit one_or_two)"
blanchet@33197
    35
nitpick [expect = none]
blanchet@33197
    36
sorry
blanchet@33197
    37
blanchet@33197
    38
lemma "x = (y\<Colon>bool one_or_two)"
blanchet@33197
    39
nitpick [expect = genuine]
blanchet@33197
    40
oops
blanchet@33197
    41
blanchet@33197
    42
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y\<Colon>bool one_or_two)"
blanchet@33197
    43
nitpick [expect = none]
blanchet@33197
    44
sorry
blanchet@33197
    45
blanchet@33197
    46
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
blanchet@33197
    47
nitpick [card = 1, expect = potential] (* unfortunate *)
blanchet@33197
    48
oops
blanchet@33197
    49
blanchet@33197
    50
lemma "\<exists>x (y\<Colon>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
haftmann@45970
    55
definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
haftmann@45970
    56
wenzelm@45694
    57
typedef (open) '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
blanchet@33197
    63
lemma "x = (y\<Colon>unit bounded)"
blanchet@33197
    64
nitpick [expect = none]
blanchet@33197
    65
sorry
blanchet@33197
    66
blanchet@33197
    67
lemma "x = (y\<Colon>bool bounded)"
blanchet@33197
    68
nitpick [expect = genuine]
blanchet@33197
    69
oops
blanchet@33197
    70
blanchet@33197
    71
lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@39362
    72
nitpick [expect = potential] (* unfortunate *)
blanchet@33197
    73
sorry
blanchet@33197
    74
blanchet@33197
    75
lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@42959
    76
nitpick [card = 1\<emdash>5, expect = genuine]
blanchet@33197
    77
oops
blanchet@33197
    78
blanchet@33197
    79
lemma "True \<equiv> ((\<lambda>x\<Colon>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@42959
   104
nitpick [card = 1\<emdash>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@42959
   108
nitpick [card = 1\<emdash>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@42959
   117
nitpick [card = 1\<emdash>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]
blanchet@33197
   152
by (rule Zero_nat_def_raw)
blanchet@33197
   153
blanchet@37400
   154
lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
blanchet@35312
   155
nitpick [expect = none]
blanchet@33197
   156
by (rule 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@42959
   167
nitpick [card = 1\<emdash>2, expect = none]
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
blanchet@33197
   182
lemma "Abs_Rat (Rep_Rat a) = a"
blanchet@33737
   183
nitpick [card = 1, expect = none]
blanchet@33197
   184
by (rule Rep_Rat_inverse)
blanchet@33197
   185
blanchet@33197
   186
end