equal
deleted
inserted
replaced
9 |
9 |
10 theory Typedef_Nits |
10 theory Typedef_Nits |
11 imports Main Rational |
11 imports Main Rational |
12 begin |
12 begin |
13 |
13 |
14 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s, |
14 nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1, |
15 card = 1\<midarrow>4] |
15 timeout = 60 s] |
16 |
16 |
17 typedef three = "{0\<Colon>nat, 1, 2}" |
17 typedef three = "{0\<Colon>nat, 1, 2}" |
18 by blast |
18 by blast |
19 |
19 |
20 definition A :: three where "A \<equiv> Abs_three 0" |
20 definition A :: three where "A \<equiv> Abs_three 0" |
136 lemma "Inl_Rep a \<noteq> Inr_Rep a" |
136 lemma "Inl_Rep a \<noteq> Inr_Rep a" |
137 nitpick [expect = none] |
137 nitpick [expect = none] |
138 by (rule Inl_Rep_not_Inr_Rep) |
138 by (rule Inl_Rep_not_Inr_Rep) |
139 |
139 |
140 lemma "Abs_Sum (Rep_Sum a) = a" |
140 lemma "Abs_Sum (Rep_Sum a) = a" |
141 nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none] |
141 nitpick [card = 1, expect = none] |
|
142 nitpick [card = 2, expect = none] |
142 by (rule Rep_Sum_inverse) |
143 by (rule Rep_Sum_inverse) |
143 |
144 |
144 lemma "0::nat \<equiv> Abs_Nat Zero_Rep" |
145 lemma "0::nat \<equiv> Abs_Nat Zero_Rep" |
145 (* nitpick [expect = none] FIXME *) |
146 (* nitpick [expect = none] FIXME *) |
146 by (rule Zero_nat_def_raw) |
147 by (rule Zero_nat_def_raw) |