src/HOL/Nitpick_Examples/Typedef_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35284 9edc2bd6d2bd
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
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
blanchet@33197
    11
imports Main Rational
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@35078
    14
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
blanchet@35078
    15
                card = 1\<midarrow>4]
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@33197
    67
nitpick [expect = none]
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]
blanchet@33197
    92
by (insert Rep_unit) (simp add: unit_def)
blanchet@33197
    93
blanchet@33197
    94
lemma "Rep_unit () = False"
blanchet@33197
    95
nitpick [expect = genuine]
blanchet@33197
    96
oops
blanchet@33197
    97
blanchet@33197
    98
lemma "Pair a b \<equiv> 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@33197
   102
lemma "Pair a b \<equiv> 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@33197
   107
lemma "fst (Abs_Prod (Pair_Rep a b)) = a"
blanchet@33197
   108
nitpick [card = 2, expect = none]
blanchet@33197
   109
by (simp add: Pair_def [THEN symmetric])
blanchet@33197
   110
blanchet@33197
   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@33197
   120
apply (drule subst [where P = "\<lambda>r. Abs_Prod r = Abs_Prod (Pair_Rep a b)"])
blanchet@33197
   121
 apply (rule refl)
blanchet@33197
   122
by (simp add: Pair_def [THEN symmetric])
blanchet@33197
   123
blanchet@33197
   124
lemma "Abs_Prod (Rep_Prod a) = a"
blanchet@33197
   125
nitpick [card = 2, expect = none]
blanchet@33197
   126
by (rule Rep_Prod_inverse)
blanchet@33197
   127
blanchet@33197
   128
lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
blanchet@33197
   129
nitpick [card = 1, expect = none]
blanchet@33979
   130
by (simp only: Inl_def o_def)
blanchet@33197
   131
blanchet@33197
   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@33197
   140
lemma "Abs_Sum (Rep_Sum a) = a"
blanchet@34083
   141
nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
blanchet@33197
   142
by (rule Rep_Sum_inverse)
blanchet@33197
   143
blanchet@33197
   144
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
blanchet@33737
   145
(* nitpick [expect = none] FIXME *)
blanchet@33197
   146
by (rule Zero_nat_def_raw)
blanchet@33197
   147
blanchet@33197
   148
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
blanchet@33737
   149
(* nitpick [expect = none] FIXME *)
blanchet@33197
   150
by (rule Suc_def)
blanchet@33197
   151
blanchet@33197
   152
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
blanchet@33197
   153
nitpick [expect = genuine]
blanchet@33197
   154
oops
blanchet@33197
   155
blanchet@33197
   156
lemma "Abs_Nat (Rep_Nat a) = a"
blanchet@33197
   157
nitpick [expect = none]
blanchet@33197
   158
by (rule Rep_Nat_inverse)
blanchet@33197
   159
blanchet@33197
   160
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
blanchet@34126
   161
nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
blanchet@33197
   162
by (rule Zero_int_def_raw)
blanchet@33197
   163
blanchet@33197
   164
lemma "Abs_Integ (Rep_Integ a) = a"
blanchet@34126
   165
nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
blanchet@33197
   166
by (rule Rep_Integ_inverse)
blanchet@33197
   167
blanchet@33197
   168
lemma "Abs_list (Rep_list a) = a"
blanchet@34126
   169
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
   170
by (rule Rep_list_inverse)
blanchet@33197
   171
blanchet@33197
   172
record point =
blanchet@33197
   173
  Xcoord :: int
blanchet@33197
   174
  Ycoord :: int
blanchet@33197
   175
blanchet@33197
   176
lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
blanchet@33571
   177
nitpick [expect = none]
blanchet@33197
   178
by (rule Rep_point_ext_type_inverse)
blanchet@33197
   179
blanchet@33197
   180
lemma "Fract a b = of_int a / of_int b"
blanchet@33737
   181
nitpick [card = 1, expect = none]
blanchet@33197
   182
by (rule Fract_of_int_quotient)
blanchet@33197
   183
blanchet@33197
   184
lemma "Abs_Rat (Rep_Rat a) = a"
blanchet@33737
   185
nitpick [card = 1, expect = none]
blanchet@33197
   186
by (rule Rep_Rat_inverse)
blanchet@33197
   187
blanchet@33197
   188
end