1 (* Title: HOL/Nitpick_Examples/Typedef_Nits.thy
2 Author: Jasmin Blanchette, TU Muenchen
5 Examples featuring Nitpick applied to typedefs.
8 header {* Examples Featuring Nitpick Applied to Typedefs *}
14 nitpick_params [verbose, card = 1\<emdash>4, sat_solver = Riss3g, max_threads = 1,
17 definition "three = {0\<Colon>nat, 1, 2}"
19 unfolding three_def by blast
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"
25 lemma "x = (y\<Colon>three)"
26 nitpick [expect = genuine]
29 definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
31 typedef 'a one_or_two = "one_or_two :: 'a set"
32 unfolding one_or_two_def by auto
34 lemma "x = (y\<Colon>unit one_or_two)"
35 nitpick [expect = none]
38 lemma "x = (y\<Colon>bool one_or_two)"
39 nitpick [expect = genuine]
42 lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y\<Colon>bool one_or_two)"
43 nitpick [expect = none]
46 lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
47 nitpick [card = 1, expect = potential] (* unfortunate *)
50 lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
51 nitpick [card = 1, expect = potential] (* unfortunate *)
52 nitpick [card = 2, expect = none]
55 definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
57 typedef 'a bounded = "bounded(TYPE('a))"
59 apply (rule_tac x = 0 in exI)
60 apply (case_tac "card UNIV = 0")
63 lemma "x = (y\<Colon>unit bounded)"
64 nitpick [expect = none]
67 lemma "x = (y\<Colon>bool bounded)"
68 nitpick [expect = genuine]
71 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
72 nitpick [expect = potential] (* unfortunate *)
75 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
76 nitpick [card = 1\<emdash>5, expect = genuine]
79 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
80 nitpick [expect = none]
83 lemma "False \<equiv> \<forall>P. P"
84 nitpick [expect = none]
87 lemma "() = Abs_unit True"
88 nitpick [expect = none]
91 lemma "() = Abs_unit False"
92 nitpick [expect = none]
95 lemma "Rep_unit () = True"
96 nitpick [expect = none]
97 by (insert Rep_unit) simp
99 lemma "Rep_unit () = False"
100 nitpick [expect = genuine]
103 lemma "Pair a b = Abs_prod (Pair_Rep a b)"
104 nitpick [card = 1\<emdash>2, expect = none]
107 lemma "Pair a b = Abs_prod (Pair_Rep b a)"
108 nitpick [card = 1\<emdash>2, expect = none]
109 nitpick [dont_box, expect = genuine]
112 lemma "fst (Abs_prod (Pair_Rep a b)) = a"
113 nitpick [card = 2, expect = none]
114 by (simp add: Pair_def [THEN sym])
116 lemma "fst (Abs_prod (Pair_Rep a b)) = b"
117 nitpick [card = 1\<emdash>2, expect = none]
118 nitpick [dont_box, expect = genuine]
121 lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
122 nitpick [expect = none]
125 apply (drule subst [where P = "\<lambda>r. Abs_prod r = Abs_prod (Pair_Rep a b)"])
127 by (simp add: Pair_def [THEN sym])
129 lemma "Abs_prod (Rep_prod a) = a"
130 nitpick [card = 2, expect = none]
131 by (rule Rep_prod_inverse)
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)
137 lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inr_Rep a)"
138 nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
141 lemma "Inl_Rep a \<noteq> Inr_Rep a"
142 nitpick [expect = none]
143 by (rule Inl_Rep_not_Inr_Rep)
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)
150 lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
151 nitpick [expect = none]
152 by (rule Zero_nat_def [abs_def])
154 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
155 nitpick [expect = none]
156 by (rule Nat.Suc_def)
158 lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
159 nitpick [expect = genuine]
162 lemma "Abs_Nat (Rep_Nat a) = a"
163 nitpick [expect = none]
164 by (rule Rep_Nat_inverse)
166 lemma "Abs_list (Rep_list a) = a"
167 nitpick [card = 1\<emdash>2, expect = none]
168 by (rule Rep_list_inverse)
174 lemma "Abs_point_ext (Rep_point_ext a) = a"
175 nitpick [expect = none]
176 by (fact Rep_point_ext_inverse)
178 lemma "Fract a b = of_int a / of_int b"
179 nitpick [card = 1, expect = none]
180 by (rule Fract_of_int_quotient)
182 lemma "Abs_rat (Rep_rat a) = a"
183 nitpick [card = 1, expect = none]
184 by (rule Rep_rat_inverse)
186 typedef check = "{x\<Colon>nat. x < 2}" by (rule exI[of _ 0], auto)
188 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2"
189 nitpick [card = 1\<emdash>3, expect = none]
190 using Rep_check[of "Abs_check n"] by auto
192 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1"
193 nitpick [card = 1\<emdash>3, expect = genuine]