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