9 |
9 |
10 theory Typedef_Nits |
10 theory Typedef_Nits |
11 imports Complex_Main |
11 imports Complex_Main |
12 begin |
12 begin |
13 |
13 |
14 nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1, |
14 nitpick_params [verbose, card = 1-4, sat_solver = MiniSat_JNI, max_threads = 1, |
15 timeout = 240] |
15 timeout = 240] |
16 |
16 |
17 definition "three = {0\<Colon>nat, 1, 2}" |
17 definition "three = {0\<Colon>nat, 1, 2}" |
18 typedef three = three |
18 typedef three = three |
19 unfolding three_def by blast |
19 unfolding three_def by blast |
71 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" |
71 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" |
72 nitpick [expect = potential] (* unfortunate *) |
72 nitpick [expect = potential] (* unfortunate *) |
73 sorry |
73 sorry |
74 |
74 |
75 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y" |
75 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y" |
76 nitpick [card = 1\<emdash>5, expect = genuine] |
76 nitpick [card = 1-5, expect = genuine] |
77 oops |
77 oops |
78 |
78 |
79 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))" |
79 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))" |
80 nitpick [expect = none] |
80 nitpick [expect = none] |
81 by (rule True_def) |
81 by (rule True_def) |
99 lemma "Rep_unit () = False" |
99 lemma "Rep_unit () = False" |
100 nitpick [expect = genuine] |
100 nitpick [expect = genuine] |
101 oops |
101 oops |
102 |
102 |
103 lemma "Pair a b = Abs_prod (Pair_Rep a b)" |
103 lemma "Pair a b = Abs_prod (Pair_Rep a b)" |
104 nitpick [card = 1\<emdash>2, expect = none] |
104 nitpick [card = 1-2, expect = none] |
105 by (rule Pair_def) |
105 by (rule Pair_def) |
106 |
106 |
107 lemma "Pair a b = Abs_prod (Pair_Rep b a)" |
107 lemma "Pair a b = Abs_prod (Pair_Rep b a)" |
108 nitpick [card = 1\<emdash>2, expect = none] |
108 nitpick [card = 1-2, expect = none] |
109 nitpick [dont_box, expect = genuine] |
109 nitpick [dont_box, expect = genuine] |
110 oops |
110 oops |
111 |
111 |
112 lemma "fst (Abs_prod (Pair_Rep a b)) = a" |
112 lemma "fst (Abs_prod (Pair_Rep a b)) = a" |
113 nitpick [card = 2, expect = none] |
113 nitpick [card = 2, expect = none] |
114 by (simp add: Pair_def [THEN sym]) |
114 by (simp add: Pair_def [THEN sym]) |
115 |
115 |
116 lemma "fst (Abs_prod (Pair_Rep a b)) = b" |
116 lemma "fst (Abs_prod (Pair_Rep a b)) = b" |
117 nitpick [card = 1\<emdash>2, expect = none] |
117 nitpick [card = 1-2, expect = none] |
118 nitpick [dont_box, expect = genuine] |
118 nitpick [dont_box, expect = genuine] |
119 oops |
119 oops |
120 |
120 |
121 lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b" |
121 lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b" |
122 nitpick [expect = none] |
122 nitpick [expect = none] |
162 lemma "Abs_Nat (Rep_Nat a) = a" |
162 lemma "Abs_Nat (Rep_Nat a) = a" |
163 nitpick [expect = none] |
163 nitpick [expect = none] |
164 by (rule Rep_Nat_inverse) |
164 by (rule Rep_Nat_inverse) |
165 |
165 |
166 lemma "Abs_list (Rep_list a) = a" |
166 lemma "Abs_list (Rep_list a) = a" |
167 (* nitpick [card = 1\<emdash>2, expect = none] FIXME *) |
167 (* nitpick [card = 1-2, expect = none] FIXME *) |
168 by (rule Rep_list_inverse) |
168 by (rule Rep_list_inverse) |
169 |
169 |
170 record point = |
170 record point = |
171 Xcoord :: int |
171 Xcoord :: int |
172 Ycoord :: int |
172 Ycoord :: int |
184 by (rule Rep_rat_inverse) |
184 by (rule Rep_rat_inverse) |
185 |
185 |
186 typedef check = "{x\<Colon>nat. x < 2}" by (rule exI[of _ 0], auto) |
186 typedef check = "{x\<Colon>nat. x < 2}" by (rule exI[of _ 0], auto) |
187 |
187 |
188 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2" |
188 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2" |
189 nitpick [card = 1\<emdash>3, expect = none] |
189 nitpick [card = 1-3, expect = none] |
190 using Rep_check[of "Abs_check n"] by auto |
190 using Rep_check[of "Abs_check n"] by auto |
191 |
191 |
192 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1" |
192 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1" |
193 nitpick [card = 1\<emdash>3, expect = genuine] |
193 nitpick [card = 1-3, expect = genuine] |
194 oops |
194 oops |
195 |
195 |
196 end |
196 end |