equal
deleted
inserted
replaced
51 "rdistinct [] acc = []" |
51 "rdistinct [] acc = []" |
52 | "rdistinct (x#xs) acc = |
52 | "rdistinct (x#xs) acc = |
53 (if x \<in> acc then rdistinct xs acc |
53 (if x \<in> acc then rdistinct xs acc |
54 else x # (rdistinct xs ({x} \<union> acc)))" |
54 else x # (rdistinct xs ({x} \<union> acc)))" |
55 |
55 |
|
56 lemma rdistinct_concat: |
|
57 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
58 apply(induct rs) |
|
59 apply simp+ |
|
60 done |
|
61 |
|
62 lemma rdistinct_concat2: |
|
63 shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
64 by (simp add: rdistinct_concat subsetI) |
|
65 |
56 |
66 |
57 lemma distinct_not_exist: |
67 lemma distinct_not_exist: |
58 shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)" |
68 shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)" |
59 apply(induct rs arbitrary: rset) |
69 apply(induct rs arbitrary: rset) |
60 apply simp |
70 apply simp |