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" |
189 lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
190 sorry |
190 sorry |
191 |
191 |
192 lemma ex1tst': "\<exists>! (x :: my_int). True" |
192 lemma ex1tst': "\<exists>! (x :: my_int). x = x" |
193 apply(lifting ex1tst) |
193 apply(lifting ex1tst) |
194 apply(cleaning) |
194 |
195 apply simp |
195 apply injection |
196 sorry |
196 apply (rule quot_respect(9)) |
|
197 apply (rule Quotient_my_int) |
|
198 |
|
199 apply(cleaning) |
|
200 apply (simp add: ex1_prs[OF Quotient_my_int]) |
|
201 done |
197 |
202 |
198 lemma ho_tst: "foldl my_plus x [] = x" |
203 lemma ho_tst: "foldl my_plus x [] = x" |
199 apply simp |
204 apply simp |
200 done |
205 done |
201 |
206 |