equal
deleted
inserted
replaced
931 by (metis list_ext_len nth_list_update_eq) |
931 by (metis list_ext_len nth_list_update_eq) |
932 |
932 |
933 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)" |
933 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)" |
934 by (metis not_less nth_append) |
934 by (metis not_less nth_append) |
935 |
935 |
936 (* FIXME in Hoare_gen? *) |
|
937 lemma pred_exI: |
|
938 assumes "(P(x) \<and>* r) s" |
|
939 shows "((EXS x. P(x)) \<and>* r) s" |
|
940 by (metis assms pred_ex_def sep_globalise) |
|
941 |
936 |
942 lemma list_ext_tail: |
937 lemma list_ext_tail: |
943 assumes h1: "length xs \<le> a" |
938 assumes h1: "length xs \<le> a" |
944 and h2: "length xs \<le> a'" |
939 and h2: "length xs \<le> a'" |
945 and h3: "a' \<le> a" |
940 and h3: "a' \<le> a" |