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\4, sat_solver = MiniSat_JNI, max_threads = 1, ``` blanchet@40341 ` 15` ``` timeout = 60] ``` blanchet@33197 ` 16` blanchet@33197 ` 17` ```typedef three = "{0\nat, 1, 2}" ``` blanchet@33197 ` 18` ```by blast ``` blanchet@33197 ` 19` blanchet@33197 ` 20` ```definition A :: three where "A \ Abs_three 0" ``` blanchet@33197 ` 21` ```definition B :: three where "B \ Abs_three 1" ``` blanchet@33197 ` 22` ```definition C :: three where "C \ Abs_three 2" ``` blanchet@33197 ` 23` blanchet@33197 ` 24` ```lemma "x = (y\three)" ``` blanchet@33197 ` 25` ```nitpick [expect = genuine] ``` blanchet@33197 ` 26` ```oops ``` blanchet@33197 ` 27` blanchet@33197 ` 28` ```typedef 'a one_or_two = "{undefined False\'a, undefined True}" ``` blanchet@33197 ` 29` ```by auto ``` blanchet@33197 ` 30` blanchet@33197 ` 31` ```lemma "x = (y\unit one_or_two)" ``` blanchet@33197 ` 32` ```nitpick [expect = none] ``` blanchet@33197 ` 33` ```sorry ``` blanchet@33197 ` 34` blanchet@33197 ` 35` ```lemma "x = (y\bool one_or_two)" ``` blanchet@33197 ` 36` ```nitpick [expect = genuine] ``` blanchet@33197 ` 37` ```oops ``` blanchet@33197 ` 38` blanchet@33197 ` 39` ```lemma "undefined False \ undefined True \ x = (y\bool one_or_two)" ``` blanchet@33197 ` 40` ```nitpick [expect = none] ``` blanchet@33197 ` 41` ```sorry ``` blanchet@33197 ` 42` blanchet@33197 ` 43` ```lemma "undefined False \ undefined True \ \x (y\bool one_or_two). x \ y" ``` blanchet@33197 ` 44` ```nitpick [card = 1, expect = potential] (* unfortunate *) ``` blanchet@33197 ` 45` ```oops ``` blanchet@33197 ` 46` blanchet@33197 ` 47` ```lemma "\x (y\bool one_or_two). x \ 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\nat. finite (UNIV\'a \ bool) \ n < card (UNIV\'a \ 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\unit bounded)" ``` blanchet@33197 ` 59` ```nitpick [expect = none] ``` blanchet@33197 ` 60` ```sorry ``` blanchet@33197 ` 61` blanchet@33197 ` 62` ```lemma "x = (y\bool bounded)" ``` blanchet@33197 ` 63` ```nitpick [expect = genuine] ``` blanchet@33197 ` 64` ```oops ``` blanchet@33197 ` 65` blanchet@33197 ` 66` ```lemma "x \ (y\bool bounded) \ z = x \ z = y" ``` blanchet@39362 ` 67` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@33197 ` 68` ```sorry ``` blanchet@33197 ` 69` blanchet@33197 ` 70` ```lemma "x \ (y\(bool \ bool) bounded) \ z = x \ z = y" ``` blanchet@34126 ` 71` ```nitpick [card = 1\5, expect = genuine] ``` blanchet@33197 ` 72` ```oops ``` blanchet@33197 ` 73` blanchet@33197 ` 74` ```lemma "True \ ((\x\bool. x) = (\x. x))" ``` blanchet@33197 ` 75` ```nitpick [expect = none] ``` blanchet@33197 ` 76` ```by (rule True_def) ``` blanchet@33197 ` 77` blanchet@33197 ` 78` ```lemma "False \ \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\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\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\2, expect = none] ``` blanchet@33197 ` 113` ```nitpick [dont_box, expect = genuine] ``` blanchet@33197 ` 114` ```oops ``` blanchet@33197 ` 115` blanchet@33197 ` 116` ```lemma "a \ a' \ Pair_Rep a b \ 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 = "\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 \ \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 \ \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 \ 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 \ 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 \ 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\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 ```