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