equal
deleted
inserted
replaced
529 lemma set_upt [simp]: "set[i..j(] = {k. i \<le> k \<and> k < j}" |
529 lemma set_upt [simp]: "set[i..j(] = {k. i \<le> k \<and> k < j}" |
530 apply (induct j) |
530 apply (induct j) |
531 apply simp_all |
531 apply simp_all |
532 apply(erule ssubst) |
532 apply(erule ssubst) |
533 apply auto |
533 apply auto |
534 apply arith |
|
535 done |
534 done |
536 |
535 |
537 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" |
536 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" |
538 apply (induct xs) |
537 apply (induct xs) |
539 apply simp |
538 apply simp |