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