equal
deleted
inserted
replaced
91 apply(subgoal_tac "rdistinct rs {} = rs") |
91 apply(subgoal_tac "rdistinct rs {} = rs") |
92 prefer 2 |
92 prefer 2 |
93 apply simp |
93 apply simp |
94 using distinct_not_exist by fastforce |
94 using distinct_not_exist by fastforce |
95 |
95 |
|
96 |
96 lemma distinct_rdistinct_append: |
97 lemma distinct_rdistinct_append: |
97 shows "distinct rs1 \<Longrightarrow> rdistinct (rs1 @ rsa) {} = rs1 @ (rdistinct rsa (set rs1))" |
98 assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc" |
98 sorry |
99 shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))" |
|
100 using assms |
|
101 apply(induct rs1 arbitrary: rsa acc) |
|
102 apply(auto)[1] |
|
103 apply(auto)[1] |
|
104 apply(drule_tac x="rsa" in meta_spec) |
|
105 apply(drule_tac x="{a} \<union> acc" in meta_spec) |
|
106 apply(simp) |
|
107 apply(drule meta_mp) |
|
108 apply(auto)[1] |
|
109 apply(simp) |
|
110 done |
|
111 |
99 |
112 |
100 lemma rdistinct_concat_general: |
113 lemma rdistinct_concat_general: |
101 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
114 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
102 sorry |
115 sorry |
103 |
116 |