src/HOL/Nitpick_Examples/Typedef_Nits.thy
author hoelzl
Tue Jan 18 21:37:23 2011 +0100 (2011-01-18)
changeset 41654 32fe42892983
parent 41278 8e1cde88aae6
child 42142 d24a93025feb
permissions -rw-r--r--
Gauge measure removed
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
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@41278
    14
nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
blanchet@40341
    15
                timeout = 60]
blanchet@33197
    16
blanchet@33197
    17
typedef three = "{0\<Colon>nat, 1, 2}"
blanchet@33197
    18
by blast
blanchet@33197
    19
blanchet@33197
    20
definition A :: three where "A \<equiv> Abs_three 0"
blanchet@33197
    21
definition B :: three where "B \<equiv> Abs_three 1"
blanchet@33197
    22
definition C :: three where "C \<equiv> Abs_three 2"
blanchet@33197
    23
blanchet@33197
    24
lemma "x = (y\<Colon>three)"
blanchet@33197
    25
nitpick [expect = genuine]
blanchet@33197
    26
oops
blanchet@33197
    27
blanchet@33197
    28
typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
blanchet@33197
    29
by auto
blanchet@33197
    30
blanchet@33197
    31
lemma "x = (y\<Colon>unit one_or_two)"
blanchet@33197
    32
nitpick [expect = none]
blanchet@33197
    33
sorry
blanchet@33197
    34
blanchet@33197
    35
lemma "x = (y\<Colon>bool one_or_two)"
blanchet@33197
    36
nitpick [expect = genuine]
blanchet@33197
    37
oops
blanchet@33197
    38
blanchet@33197
    39
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y\<Colon>bool one_or_two)"
blanchet@33197
    40
nitpick [expect = none]
blanchet@33197
    41
sorry
blanchet@33197
    42
blanchet@33197
    43
lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
blanchet@33197
    44
nitpick [card = 1, expect = potential] (* unfortunate *)
blanchet@33197
    45
oops
blanchet@33197
    46
blanchet@33197
    47
lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
blanchet@33197
    48
nitpick [card = 1, expect = potential] (* unfortunate *)
blanchet@33197
    49
nitpick [card = 2, expect = none]
blanchet@33197
    50
oops
blanchet@33197
    51
blanchet@33197
    52
typedef 'a bounded =
blanchet@33197
    53
        "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
blanchet@33197
    54
apply (rule_tac x = 0 in exI)
blanchet@33197
    55
apply (case_tac "card UNIV = 0")
blanchet@33197
    56
by auto
blanchet@33197
    57
blanchet@33197
    58
lemma "x = (y\<Colon>unit bounded)"
blanchet@33197
    59
nitpick [expect = none]
blanchet@33197
    60
sorry
blanchet@33197
    61
blanchet@33197
    62
lemma "x = (y\<Colon>bool bounded)"
blanchet@33197
    63
nitpick [expect = genuine]
blanchet@33197
    64
oops
blanchet@33197
    65
blanchet@33197
    66
lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@39362
    67
nitpick [expect = potential] (* unfortunate *)
blanchet@33197
    68
sorry
blanchet@33197
    69
blanchet@33197
    70
lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
blanchet@34126
    71
nitpick [card = 1\<midarrow>5, expect = genuine]
blanchet@33197
    72
oops
blanchet@33197
    73
blanchet@33197
    74
lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
blanchet@33197
    75
nitpick [expect = none]
blanchet@33197
    76
by (rule True_def)
blanchet@33197
    77
blanchet@33197
    78
lemma "False \<equiv> \<forall>P. P"
blanchet@33197
    79
nitpick [expect = none]
blanchet@33197
    80
by (rule False_def)
blanchet@33197
    81
blanchet@33197
    82
lemma "() = Abs_unit True"
blanchet@33197
    83
nitpick [expect = none]
blanchet@33197
    84
by (rule Unity_def)
blanchet@33197
    85
blanchet@33197
    86
lemma "() = Abs_unit False"
blanchet@33197
    87
nitpick [expect = none]
blanchet@33197
    88
by simp
blanchet@33197
    89
blanchet@33197
    90
lemma "Rep_unit () = True"
blanchet@33197
    91
nitpick [expect = none]
huffman@40590
    92
by (insert Rep_unit) simp
blanchet@33197
    93
blanchet@33197
    94
lemma "Rep_unit () = False"
blanchet@33197
    95
nitpick [expect = genuine]
blanchet@33197
    96
oops
blanchet@33197
    97
blanchet@37400
    98
lemma "Pair a b = Abs_prod (Pair_Rep a b)"
blanchet@33197
    99
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
   100
by (rule Pair_def)
blanchet@33197
   101
blanchet@37400
   102
lemma "Pair a b = Abs_prod (Pair_Rep b a)"
blanchet@33197
   103
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
   104
nitpick [dont_box, expect = genuine]
blanchet@33197
   105
oops
blanchet@33197
   106
blanchet@37400
   107
lemma "fst (Abs_prod (Pair_Rep a b)) = a"
blanchet@33197
   108
nitpick [card = 2, expect = none]
blanchet@37400
   109
by (simp add: Pair_def [THEN sym])
blanchet@33197
   110
blanchet@37400
   111
lemma "fst (Abs_prod (Pair_Rep a b)) = b"
blanchet@33197
   112
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
   113
nitpick [dont_box, expect = genuine]
blanchet@33197
   114
oops
blanchet@33197
   115
blanchet@33197
   116
lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
blanchet@33197
   117
nitpick [expect = none]
blanchet@33197
   118
apply (rule ccontr)
blanchet@33197
   119
apply simp
blanchet@37400
   120
apply (drule subst [where P = "\<lambda>r. Abs_prod r = Abs_prod (Pair_Rep a b)"])
blanchet@33197
   121
 apply (rule refl)
blanchet@37400
   122
by (simp add: Pair_def [THEN sym])
blanchet@33197
   123
blanchet@37400
   124
lemma "Abs_prod (Rep_prod a) = a"
blanchet@33197
   125
nitpick [card = 2, expect = none]
blanchet@37400
   126
by (rule Rep_prod_inverse)
blanchet@33197
   127
blanchet@37400
   128
lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inl_Rep a)"
blanchet@33197
   129
nitpick [card = 1, expect = none]
blanchet@37400
   130
by (simp add: Inl_def o_def)
blanchet@33197
   131
blanchet@37400
   132
lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inr_Rep a)"
blanchet@33197
   133
nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
blanchet@33197
   134
oops
blanchet@33197
   135
blanchet@33197
   136
lemma "Inl_Rep a \<noteq> Inr_Rep a"
blanchet@33197
   137
nitpick [expect = none]
blanchet@33197
   138
by (rule Inl_Rep_not_Inr_Rep)
blanchet@33197
   139
blanchet@37400
   140
lemma "Abs_sum (Rep_sum a) = a"
blanchet@35284
   141
nitpick [card = 1, expect = none]
blanchet@35284
   142
nitpick [card = 2, expect = none]
blanchet@37400
   143
by (rule Rep_sum_inverse)
blanchet@33197
   144
blanchet@33197
   145
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
blanchet@35312
   146
nitpick [expect = none]
blanchet@33197
   147
by (rule Zero_nat_def_raw)
blanchet@33197
   148
blanchet@37400
   149
lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
blanchet@35312
   150
nitpick [expect = none]
blanchet@33197
   151
by (rule Suc_def)
blanchet@33197
   152
blanchet@37400
   153
lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
blanchet@33197
   154
nitpick [expect = genuine]
blanchet@33197
   155
oops
blanchet@33197
   156
blanchet@33197
   157
lemma "Abs_Nat (Rep_Nat a) = a"
blanchet@33197
   158
nitpick [expect = none]
blanchet@33197
   159
by (rule Rep_Nat_inverse)
blanchet@33197
   160
blanchet@33197
   161
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
blanchet@34126
   162
nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
blanchet@33197
   163
by (rule Zero_int_def_raw)
blanchet@33197
   164
blanchet@33197
   165
lemma "Abs_list (Rep_list a) = a"
blanchet@34126
   166
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
   167
by (rule Rep_list_inverse)
blanchet@33197
   168
blanchet@33197
   169
record point =
blanchet@33197
   170
  Xcoord :: int
blanchet@33197
   171
  Ycoord :: int
blanchet@33197
   172
haftmann@38542
   173
lemma "Abs_point_ext (Rep_point_ext a) = a"
blanchet@33571
   174
nitpick [expect = none]
haftmann@38542
   175
by (fact Rep_point_ext_inverse)
blanchet@33197
   176
blanchet@33197
   177
lemma "Fract a b = of_int a / of_int b"
blanchet@33737
   178
nitpick [card = 1, expect = none]
blanchet@33197
   179
by (rule Fract_of_int_quotient)
blanchet@33197
   180
blanchet@33197
   181
lemma "Abs_Rat (Rep_Rat a) = a"
blanchet@33737
   182
nitpick [card = 1, expect = none]
blanchet@33197
   183
by (rule Rep_Rat_inverse)
blanchet@33197
   184
blanchet@33197
   185
end