equal
deleted
inserted
replaced
184 and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))" |
184 and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))" |
185 shows "P x" |
185 shows "P x" |
186 using a b c |
186 using a b c |
187 by (lifting int_induct_raw) |
187 by (lifting int_induct_raw) |
188 |
188 |
|
189 lemma ex1tst: "\<exists>! (x :: nat \<times> nat) \<in> Respects (op \<approx>). True" |
|
190 sorry |
|
191 |
|
192 lemma ex1tst': "\<exists>! (x :: my_int). True" |
|
193 apply(lifting ex1tst) |
|
194 apply(cleaning) |
|
195 apply simp |
|
196 sorry |
|
197 |
189 lemma ho_tst: "foldl my_plus x [] = x" |
198 lemma ho_tst: "foldl my_plus x [] = x" |
190 apply simp |
199 apply simp |
191 done |
200 done |
192 |
201 |
193 |
202 |