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