117 |
117 |
118 lemma rdistinct_set_equality: |
118 lemma rdistinct_set_equality: |
119 shows "set (rdistinct rs {}) = set rs" |
119 shows "set (rdistinct rs {}) = set rs" |
120 by (simp add: rdistinct_set_equality1) |
120 by (simp add: rdistinct_set_equality1) |
121 |
121 |
|
122 |
|
123 lemma distinct_removes_middle: |
|
124 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
125 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
126 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
127 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
128 apply simp |
|
129 apply simp |
|
130 apply(case_tac "a \<in> rset") |
|
131 apply simp |
|
132 apply metis |
|
133 apply simp |
|
134 apply (metis insertI1) |
|
135 apply(case_tac "a = ab") |
|
136 apply simp |
|
137 apply(case_tac "ab \<in> rset") |
|
138 apply simp |
|
139 apply presburger |
|
140 apply (meson insertI1) |
|
141 apply(case_tac "a \<in> rset") |
|
142 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
143 apply(case_tac "ab \<in> rset") |
|
144 apply simp |
|
145 apply (meson insert_iff) |
|
146 apply simp |
|
147 by (metis insertI1) |
|
148 |
|
149 lemma distinct_removes_middle3: |
|
150 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
151 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
152 using distinct_removes_middle(1) by fastforce |
|
153 |
|
154 lemma last_elem_out: |
|
155 shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" |
|
156 apply(induct xs arbitrary: rset) |
|
157 apply simp+ |
|
158 done |
|
159 |
|
160 |
|
161 |
|
162 |
|
163 lemma rdistinct_concat_general: |
|
164 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
165 apply(induct rs1 arbitrary: rs2 rule: rev_induct) |
|
166 apply simp |
|
167 apply(drule_tac x = "x # rs2" in meta_spec) |
|
168 apply simp |
|
169 apply(case_tac "x \<in> set xs") |
|
170 apply simp |
|
171 |
|
172 apply (simp add: distinct_removes_middle3 insert_absorb) |
|
173 apply simp |
|
174 by (simp add: last_elem_out) |
|
175 |
|
176 |
|
177 lemma distinct_once_enough: |
|
178 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
179 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
180 apply(subgoal_tac |
|
181 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
182 apply(simp only:) |
|
183 using rdistinct_concat_general apply blast |
|
184 apply (simp add: distinct_rdistinct_append rdistinct_set_equality1) |
|
185 by (simp add: rdistinct_does_the_job) |
|
186 |
122 |
187 |
123 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
188 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
124 where |
189 where |
125 "rflts [] = []" |
190 "rflts [] = []" |
126 | "rflts (RZERO # rs) = rflts rs" |
191 | "rflts (RZERO # rs) = rflts rs" |
921 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
986 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
922 apply simp |
987 apply simp |
923 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
988 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
924 |
989 |
925 |
990 |
926 lemma distinct_removes_middle: |
991 |
927 shows "\<lbrakk>a \<in> set as\<rbrakk> |
992 |
928 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
929 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
930 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
931 apply simp |
|
932 apply simp |
|
933 apply(case_tac "a \<in> rset") |
|
934 apply simp |
|
935 apply metis |
|
936 apply simp |
|
937 apply (metis insertI1) |
|
938 apply(case_tac "a = ab") |
|
939 apply simp |
|
940 apply(case_tac "ab \<in> rset") |
|
941 apply simp |
|
942 apply presburger |
|
943 apply (meson insertI1) |
|
944 apply(case_tac "a \<in> rset") |
|
945 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
946 apply(case_tac "ab \<in> rset") |
|
947 apply simp |
|
948 apply (meson insert_iff) |
|
949 apply simp |
|
950 by (metis insertI1) |
|
951 |
|
952 |
|
953 lemma distinct_removes_middle3: |
|
954 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
955 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
956 using distinct_removes_middle(1) by fastforce |
|
957 |
993 |
958 |
994 |
959 lemma distinct_removes_list: |
995 lemma distinct_removes_list: |
960 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
996 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
961 apply(induct rs) |
997 apply(induct rs) |
1036 apply simp_all |
1072 apply simp_all |
1037 |
1073 |
1038 apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
1074 apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
1039 by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
1075 by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
1040 |
1076 |
1041 lemma last_elem_out: |
1077 |
1042 shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" |
1078 |
1043 apply(induct xs arbitrary: rset) |
1079 |
1044 apply simp+ |
|
1045 done |
|
1046 |
|
1047 |
|
1048 |
|
1049 |
|
1050 lemma rdistinct_concat_general: |
|
1051 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
1052 apply(induct rs1 arbitrary: rs2 rule: rev_induct) |
|
1053 apply simp |
|
1054 apply(drule_tac x = "x # rs2" in meta_spec) |
|
1055 apply simp |
|
1056 apply(case_tac "x \<in> set xs") |
|
1057 apply simp |
|
1058 |
|
1059 apply (simp add: distinct_removes_middle3 insert_absorb) |
|
1060 apply simp |
|
1061 by (simp add: last_elem_out) |
|
1062 |
|
1063 |
|
1064 |
|
1065 |
|
1066 lemma distinct_once_enough: |
|
1067 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
1068 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
1069 apply(subgoal_tac |
|
1070 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
1071 apply(simp only:) |
|
1072 using rdistinct_concat_general apply blast |
|
1073 apply (simp add: distinct_rdistinct_append rdistinct_set_equality1) |
|
1074 by (simp add: rdistinct_does_the_job) |
|
1075 |
|
1076 |
1080 |
1077 lemma simp_flatten: |
1081 lemma simp_flatten: |
1078 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
1082 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
1079 apply simp |
1083 apply simp |
1080 apply(subst flatten_rsimpalts) |
1084 apply(subst flatten_rsimpalts) |