equal
deleted
inserted
replaced
331 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" |
331 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" |
332 by (induct xs) auto |
332 by (induct xs) auto |
333 |
333 |
334 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" |
334 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" |
335 by (induct xs) auto |
335 by (induct xs) auto |
|
336 |
|
337 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0" |
|
338 by auto |
336 |
339 |
337 lemma length_Suc_conv: |
340 lemma length_Suc_conv: |
338 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" |
341 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" |
339 by (induct xs) auto |
342 by (induct xs) auto |
340 |
343 |
2050 lemma remove1_append: |
2053 lemma remove1_append: |
2051 "remove1 x (xs @ ys) = |
2054 "remove1 x (xs @ ys) = |
2052 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)" |
2055 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)" |
2053 by (induct xs) auto |
2056 by (induct xs) auto |
2054 |
2057 |
|
2058 lemma in_set_remove1[simp]: |
|
2059 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)" |
|
2060 apply (induct xs) |
|
2061 apply auto |
|
2062 done |
|
2063 |
2055 lemma set_remove1_subset: "set(remove1 x xs) <= set xs" |
2064 lemma set_remove1_subset: "set(remove1 x xs) <= set xs" |
2056 apply(induct xs) |
2065 apply(induct xs) |
2057 apply simp |
2066 apply simp |
2058 apply simp |
2067 apply simp |
2059 apply blast |
2068 apply blast |
2062 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}" |
2071 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}" |
2063 apply(induct xs) |
2072 apply(induct xs) |
2064 apply simp |
2073 apply simp |
2065 apply simp |
2074 apply simp |
2066 apply blast |
2075 apply blast |
|
2076 done |
|
2077 |
|
2078 lemma length_remove1: |
|
2079 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)" |
|
2080 apply (induct xs) |
|
2081 apply (auto dest!:length_pos_if_in_set) |
2067 done |
2082 done |
2068 |
2083 |
2069 lemma remove1_filter_not[simp]: |
2084 lemma remove1_filter_not[simp]: |
2070 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs" |
2085 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs" |
2071 by(induct xs) auto |
2086 by(induct xs) auto |