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: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
189 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
190 sorry |
190 sorry |
191 |
191 |
192 lemma ex1tst': "\<exists>! (x :: my_int). x = x" |
192 lemma ex1tst': "\<exists>!(x::my_int). x = x" |
193 apply(lifting ex1tst) |
193 apply(lifting ex1tst) |
194 done |
194 done |
|
195 |
195 |
196 |
196 lemma ho_tst: "foldl my_plus x [] = x" |
197 lemma ho_tst: "foldl my_plus x [] = x" |
197 apply simp |
198 apply simp |
198 done |
199 done |
199 |
200 |