|
1 theory HarderProps imports BasicIdentities |
|
2 begin |
|
3 |
|
4 |
|
5 |
|
6 |
|
7 lemma spawn_simp_rsimpalts: |
|
8 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" |
|
9 apply(cases rs) |
|
10 apply simp |
|
11 apply(case_tac list) |
|
12 apply simp |
|
13 apply(subst rsimp_idem[symmetric]) |
|
14 apply simp |
|
15 apply(subgoal_tac "rsimp_ALTs rs = RALTS rs") |
|
16 apply(simp only:) |
|
17 apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)") |
|
18 apply(simp only:) |
|
19 prefer 2 |
|
20 apply simp |
|
21 prefer 2 |
|
22 using rsimp_ALTs.simps(3) apply presburger |
|
23 apply auto |
|
24 apply(subst rsimp_idem)+ |
|
25 by (metis comp_apply rsimp_idem) |
|
26 |
|
27 |
|
28 |
|
29 |
|
30 lemma good1_rsimpalts: |
|
31 shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
32 by (metis no_alt_short_list_after_simp) |
|
33 |
|
34 |
|
35 |
|
36 |
|
37 lemma good1_flatten: |
|
38 shows "\<lbrakk> rsimp r = (RALTS rs1)\<rbrakk> |
|
39 \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)" |
|
40 apply(subst good1_rsimpalts) |
|
41 apply simp+ |
|
42 apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)") |
|
43 apply simp |
|
44 using flts_append rsimp_inner_idem4 by presburger |
|
45 |
|
46 |
|
47 lemma flatten_rsimpalts: |
|
48 shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = |
|
49 rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)" |
|
50 apply(case_tac "map rsimp rsa") |
|
51 apply simp |
|
52 apply(case_tac "list") |
|
53 apply simp |
|
54 apply(case_tac a) |
|
55 apply simp+ |
|
56 apply(rename_tac rs1) |
|
57 apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp) |
|
58 |
|
59 apply simp |
|
60 |
|
61 apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r") |
|
62 apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}") |
|
63 apply simp |
|
64 apply(case_tac "listb") |
|
65 apply simp+ |
|
66 apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3)) |
|
67 by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map) |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 lemma simp_flatten: |
|
75 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
76 apply simp |
|
77 apply(subst flatten_rsimpalts) |
|
78 apply(simp add: flts_append) |
|
79 by (metis Diff_empty distinct_once_enough flts_append nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality1) |
|
80 |
|
81 |
|
82 |
|
83 |
|
84 |
|
85 lemma simp_flatten_aux0: |
|
86 shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))" |
|
87 apply(induct rs) |
|
88 apply simp+ |
|
89 by (metis (mono_tags, opaque_lifting) comp_eq_dest_lhs map_eq_conv rsimp_idem) |
|
90 |
|
91 |
|
92 |
|
93 |
|
94 |
|
95 |
|
96 lemma good_singleton: |
|
97 shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]" |
|
98 using good.simps(1) k0b by blast |
|
99 |
|
100 |
|
101 |
|
102 |
|
103 |
|
104 lemma good_flatten_aux_aux1: |
|
105 shows "\<lbrakk> size rs \<ge>2; |
|
106 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk> |
|
107 \<Longrightarrow> rdistinct (rs @ rsb) rset = |
|
108 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" |
|
109 apply(induct rs arbitrary: rset) |
|
110 apply simp |
|
111 apply(case_tac "a \<in> rset") |
|
112 apply simp |
|
113 apply(case_tac "rdistinct rs {a}") |
|
114 apply simp |
|
115 apply(subst good_singleton) |
|
116 apply force |
|
117 apply simp |
|
118 apply (meson all_that_same_elem) |
|
119 apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ") |
|
120 prefer 2 |
|
121 using k0a rsimp_ALTs.simps(3) apply presburger |
|
122 apply(simp only:) |
|
123 apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ") |
|
124 apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2)) |
|
125 apply (meson distinct_eq_interesting1) |
|
126 apply simp |
|
127 apply(case_tac "rdistinct rs {a}") |
|
128 prefer 2 |
|
129 apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})") |
|
130 apply(simp only:) |
|
131 apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) = |
|
132 rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset") |
|
133 apply simp |
|
134 apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2)) |
|
135 using rsimp_ALTs.simps(3) apply presburger |
|
136 by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left) |
|
137 |
|
138 |
|
139 |
|
140 |
|
141 |
|
142 lemma good_flatten_aux_aux: |
|
143 shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; |
|
144 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk> |
|
145 \<Longrightarrow> rdistinct (rs @ rsb) rset = |
|
146 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" |
|
147 apply(erule exE)+ |
|
148 apply(subgoal_tac "size rs \<ge> 2") |
|
149 apply (metis good_flatten_aux_aux1) |
|
150 by (simp add: Suc_leI length_Cons less_add_Suc1) |
|
151 |
|
152 |
|
153 |
|
154 lemma good_flatten_aux: |
|
155 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; |
|
156 \<forall>r\<in>set rsb. good r \<or> r = RZERO; |
|
157 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
|
158 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
159 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
|
160 map rsimp rsa = rsa; |
|
161 map rsimp rsb = rsb; |
|
162 map rsimp rs = rs; |
|
163 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
|
164 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); |
|
165 rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
|
166 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk> |
|
167 \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset = |
|
168 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset" |
|
169 apply simp |
|
170 apply(case_tac "rflts rs ") |
|
171 apply simp |
|
172 apply(case_tac "list") |
|
173 apply simp |
|
174 apply(case_tac "a \<in> rset") |
|
175 apply simp |
|
176 apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2)) |
|
177 apply simp |
|
178 apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) |
|
179 apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
|
180 prefer 2 |
|
181 apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1) |
|
182 apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
|
183 prefer 2 |
|
184 apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1) |
|
185 by (smt (verit, ccfv_threshold) good_flatten_aux_aux) |
|
186 |
|
187 |
|
188 |
|
189 |
|
190 lemma good_flatten_middle: |
|
191 shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; |
|
192 \<forall>r \<in> set rsa. good r \<or> r = RZERO; |
|
193 \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow> |
|
194 rsimp (RALTS (rsa @ rs @ rsb)) = |
|
195 rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" |
|
196 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
|
197 map rsimp rs @ map rsimp rsb)) {})") |
|
198 prefer 2 |
|
199 apply simp |
|
200 apply(simp only:) |
|
201 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
|
202 [rsimp (RALTS rs)] @ map rsimp rsb)) {})") |
|
203 prefer 2 |
|
204 apply simp |
|
205 apply(simp only:) |
|
206 apply(subgoal_tac "map rsimp rsa = rsa") |
|
207 prefer 2 |
|
208 apply (metis map_idI rsimp.simps(3) test) |
|
209 apply(simp only:) |
|
210 apply(subgoal_tac "map rsimp rsb = rsb") |
|
211 prefer 2 |
|
212 apply (metis map_idI rsimp.simps(3) test) |
|
213 apply(simp only:) |
|
214 apply(subst flts_append)+ |
|
215 apply(subgoal_tac "map rsimp rs = rs") |
|
216 apply(simp only:) |
|
217 prefer 2 |
|
218 apply (metis map_idI rsimp.simps(3) test) |
|
219 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
|
220 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") |
|
221 apply(simp only:) |
|
222 prefer 2 |
|
223 using rdistinct_concat_general apply blast |
|
224 apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
|
225 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
|
226 apply(simp only:) |
|
227 prefer 2 |
|
228 using rdistinct_concat_general apply blast |
|
229 apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = |
|
230 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
|
231 apply presburger |
|
232 using good_flatten_aux by blast |
|
233 |
|
234 |
|
235 |
|
236 lemma simp_flatten3: |
|
237 shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
|
238 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
239 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
|
240 prefer 2 |
|
241 apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) |
|
242 apply (simp only:) |
|
243 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = |
|
244 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))") |
|
245 prefer 2 |
|
246 apply (metis map_append simp_flatten_aux0) |
|
247 apply(simp only:) |
|
248 apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = |
|
249 rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") |
|
250 |
|
251 apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) |
|
252 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO") |
|
253 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO") |
|
254 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO") |
|
255 |
|
256 using good_flatten_middle apply presburger |
|
257 apply (simp add: good1) |
|
258 apply (simp add: good1) |
|
259 apply (simp add: good1) |
|
260 done |
|
261 |
|
262 |
|
263 lemma simp_removes_duplicate1: |
|
264 shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" |
|
265 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" |
|
266 apply(induct rsa arbitrary: a1) |
|
267 apply simp |
|
268 apply simp |
|
269 prefer 2 |
|
270 apply(case_tac "a = aa") |
|
271 apply simp |
|
272 apply simp |
|
273 apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) |
|
274 apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) |
|
275 by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) |
|
276 |
|
277 lemma simp_removes_duplicate2: |
|
278 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
279 apply(induct rsb arbitrary: rsa) |
|
280 apply simp |
|
281 using distinct_removes_duplicate_flts apply auto[1] |
|
282 by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) |
|
283 |
|
284 lemma simp_removes_duplicate3: |
|
285 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
286 using simp_removes_duplicate2 by auto |
|
287 |
|
288 |
|
289 end |