equal
deleted
inserted
replaced
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 |
56 |
57 |
57 lemma distinct_not_exist: |
|
58 shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)" |
|
59 apply(induct rs arbitrary: rset) |
|
60 apply simp |
|
61 apply(case_tac "aa \<in> rset") |
|
62 apply simp |
|
63 apply(subgoal_tac "a \<noteq> aa") |
|
64 prefer 2 |
|
65 apply simp |
|
66 apply simp |
|
67 done |
58 |
68 |
59 |
69 |
60 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
70 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
61 where |
71 where |
62 "rflts [] = []" |
72 "rflts [] = []" |