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