444
+ − 1 theory ClosedForms imports
+ − 2 "BasicIdentities"
443
+ − 3 begin
+ − 4
489
+ − 5 lemma flts_middle0:
+ − 6 shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+ − 7 apply(induct rsa)
+ − 8 apply simp
+ − 9 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+ − 10
490
+ − 11
+ − 12
+ − 13 lemma simp_flatten_aux0:
+ − 14 shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
+ − 15 by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)
+ − 16
+ − 17
+ − 18
+ − 19
+ − 20
+ − 21
+ − 22
+ − 23
+ − 24
489
+ − 25
+ − 26
+ − 27 inductive
492
+ − 28 hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
489
+ − 29 where
492
+ − 30 "RSEQ RZERO r2 h\<leadsto> RZERO"
+ − 31 | "RSEQ r1 RZERO h\<leadsto> RZERO"
+ − 32 | "RSEQ RONE r h\<leadsto> r"
+ − 33 | "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r2 r3"
+ − 34 | "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"
+ − 35 | "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
489
+ − 36 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
492
+ − 37 | "RALTS (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS (rsa @ rsb)"
+ − 38 | "RALTS (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"
+ − 39 | "RALTS [] h\<leadsto> RZERO"
+ − 40 | "RALTS [r] h\<leadsto> r"
+ − 41 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
489
+ − 42
+ − 43 inductive
492
+ − 44 hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)
489
+ − 45 where
492
+ − 46 rs1[intro, simp]:"r h\<leadsto>* r"
+ − 47 | rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
+ − 48
+ − 49
+ − 50 lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"
489
+ − 51 using hrewrites.intros(1) hrewrites.intros(2) by blast
+ − 52
+ − 53 lemma hreal_trans[trans]:
492
+ − 54 assumes a1: "r1 h\<leadsto>* r2" and a2: "r2 h\<leadsto>* r3"
+ − 55 shows "r1 h\<leadsto>* r3"
489
+ − 56 using a2 a1
+ − 57 apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct)
+ − 58 apply(auto)
+ − 59 done
+ − 60
492
+ − 61 lemma hmany_steps_later: "\<lbrakk>r1 h\<leadsto> r2; r2 h\<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
489
+ − 62 by (meson hr_in_rstar hreal_trans)
+ − 63
+ − 64 lemma hrewrites_seq_context:
492
+ − 65 shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"
489
+ − 66 apply(induct r1 r2 rule: hrewrites.induct)
+ − 67 apply simp
+ − 68 using hrewrite.intros(4) by blast
+ − 69
+ − 70 lemma hrewrites_seq_context2:
492
+ − 71 shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"
489
+ − 72 apply(induct r1 r2 rule: hrewrites.induct)
+ − 73 apply simp
+ − 74 using hrewrite.intros(5) by blast
+ − 75
+ − 76 lemma hrewrites_seq_context0:
492
+ − 77 shows "r1 h\<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RZERO"
+ − 78 apply(subgoal_tac "RSEQ r1 r3 h\<leadsto>* RSEQ RZERO r3")
489
+ − 79 using hrewrite.intros(1) apply blast
+ − 80 by (simp add: hrewrites_seq_context)
+ − 81
+ − 82 lemma hrewrites_seq_contexts:
492
+ − 83 shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
489
+ − 84 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
+ − 85
+ − 86
+ − 87
453
+ − 88 lemma map_concat_cons:
+ − 89 shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
+ − 90 by simp
+ − 91
+ − 92 lemma neg_removal_element_of:
+ − 93 shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
+ − 94 by simp
+ − 95
465
+ − 96
+ − 97
+ − 98
+ − 99
478
+ − 100
465
+ − 101
+ − 102
478
+ − 103
465
+ − 104
+ − 105
+ − 106 lemma flts_middle01:
+ − 107 shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
+ − 108 by (simp add: flts_middle0)
+ − 109
+ − 110 lemma flts_append1:
+ − 111 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow>
+ − 112 rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)"
+ − 113 apply(induct rsa arbitrary: rsb)
+ − 114 apply simp
+ − 115 using rflts_def_idiot apply presburger
+ − 116 apply(case_tac aa)
+ − 117 apply simp+
+ − 118 done
+ − 119
478
+ − 120
465
+ − 121
+ − 122 lemma simp_removes_duplicate1:
+ − 123 shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))"
+ − 124 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
+ − 125 apply(induct rsa arbitrary: a1)
+ − 126 apply simp
+ − 127 apply simp
+ − 128 prefer 2
+ − 129 apply(case_tac "a = aa")
+ − 130 apply simp
+ − 131 apply simp
+ − 132 apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
+ − 133 apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
+ − 134 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))
+ − 135
+ − 136 lemma simp_removes_duplicate2:
+ − 137 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
+ − 138 apply(induct rsb arbitrary: rsa)
+ − 139 apply simp
+ − 140 using distinct_removes_duplicate_flts apply auto[1]
+ − 141 by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
+ − 142
+ − 143 lemma simp_removes_duplicate3:
+ − 144 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
+ − 145 using simp_removes_duplicate2 by auto
+ − 146
+ − 147 lemma distinct_removes_middle4:
+ − 148 shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
+ − 149 using distinct_removes_middle(1) by fastforce
+ − 150
+ − 151 lemma distinct_removes_middle_list:
+ − 152 shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
+ − 153 apply(induct x)
+ − 154 apply simp
+ − 155 by (simp add: distinct_removes_middle3)
+ − 156
+ − 157
+ − 158 lemma distinct_removes_duplicate_flts2:
+ − 159 shows " a \<in> set rsa
+ − 160 \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} =
+ − 161 rdistinct (rflts (rsa @ rsb)) {}"
+ − 162 apply(induct a arbitrary: rsb)
+ − 163 using flts_middle01 apply presburger
+ − 164 apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb")
+ − 165 prefer 2
+ − 166 using flts_append1 apply blast
+ − 167 apply simp
+ − 168 apply(subgoal_tac "RONE \<in> set (rflts rsa)")
+ − 169 prefer 2
+ − 170 using rflts_def_idiot2 apply blast
+ − 171 apply(subst distinct_removes_middle3)
+ − 172 apply simp
+ − 173 using flts_append apply presburger
+ − 174 apply simp
+ − 175 apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5))
+ − 176 apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+ − 177 apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb")
+ − 178 prefer 2
+ − 179 apply (simp add: flts_append)
+ − 180 apply (simp only:)
+ − 181
+ − 182 apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)")
+ − 183 prefer 2
+ − 184 using spilled_alts_contained apply blast
+ − 185 apply(subst flts_append)
+ − 186 using distinct_removes_middle_list apply blast
+ − 187 using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce
+ − 188
+ − 189
+ − 190 lemma simp_removes_duplicate:
+ − 191 shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (rsimp_ALTs (rsa @ rs))"
+ − 192 apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))")
+ − 193 prefer 2
+ − 194 apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims)
+ − 195 apply(simp only:)
+ − 196 apply simp
+ − 197 apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @ map rsimp rs)) {})")
+ − 198 apply(simp only:)
+ − 199 prefer 2
+ − 200 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+ − 201 prefer 2
+ − 202 apply simp
+ − 203 using distinct_removes_duplicate_flts2 apply force
+ − 204 apply(case_tac rsa)
+ − 205 apply simp
+ − 206 apply(case_tac rs)
+ − 207 apply simp
+ − 208 apply(case_tac list)
+ − 209 apply simp
+ − 210 using idem_after_simp1 apply presburger
+ − 211 apply simp+
+ − 212 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")
+ − 213 apply simp
+ − 214 using rsimpalts_conscons by presburger
467
+ − 215
+ − 216
+ − 217
+ − 218
468
+ − 219
467
+ − 220
+ − 221
471
+ − 222
+ − 223 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
+ − 224 where
+ − 225 "(RZERO # rs) \<leadsto>f rs"
+ − 226 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"
+ − 227 | "rs1 \<leadsto>f rs2 \<Longrightarrow> (r # rs1) \<leadsto>f (r # rs2)"
+ − 228
+ − 229
+ − 230 inductive
+ − 231 frewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f* _" [10, 10] 10)
+ − 232 where
473
+ − 233 [intro, simp]:"rs \<leadsto>f* rs"
+ − 234 | [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"
+ − 235
+ − 236 inductive grewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g _" [10, 10] 10)
+ − 237 where
+ − 238 "(RZERO # rs) \<leadsto>g rs"
+ − 239 | "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"
+ − 240 | "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
+ − 241 | "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc"
+ − 242
478
+ − 243 lemma grewrite_variant1:
+ − 244 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ a # rs \<leadsto>g rs1 @ rs"
+ − 245 apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
+ − 246 done
+ − 247
473
+ − 248
+ − 249 inductive
+ − 250 grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)
+ − 251 where
+ − 252 [intro, simp]:"rs \<leadsto>g* rs"
+ − 253 | [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"
478
+ − 254
+ − 255
+ − 256
473
+ − 257 (*
+ − 258 inductive
+ − 259 frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)
+ − 260 where
+ − 261 [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"
+ − 262 *)
471
+ − 263
+ − 264 lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"
+ − 265 using frewrites.intros(1) frewrites.intros(2) by blast
+ − 266
+ − 267 lemma freal_trans[trans]:
+ − 268 assumes a1: "r1 \<leadsto>f* r2" and a2: "r2 \<leadsto>f* r3"
+ − 269 shows "r1 \<leadsto>f* r3"
+ − 270 using a2 a1
+ − 271 apply(induct r2 r3 arbitrary: r1 rule: frewrites.induct)
+ − 272 apply(auto)
+ − 273 done
+ − 274
+ − 275
+ − 276 lemma many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3"
+ − 277 by (meson fr_in_rstar freal_trans)
+ − 278
+ − 279
475
+ − 280 lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2"
+ − 281 using grewrites.intros(1) grewrites.intros(2) by blast
+ − 282
+ − 283 lemma greal_trans[trans]:
+ − 284 assumes a1: "r1 \<leadsto>g* r2" and a2: "r2 \<leadsto>g* r3"
+ − 285 shows "r1 \<leadsto>g* r3"
+ − 286 using a2 a1
+ − 287 apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct)
+ − 288 apply(auto)
+ − 289 done
+ − 290
+ − 291
+ − 292 lemma gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"
+ − 293 by (meson gr_in_rstar greal_trans)
+ − 294
478
+ − 295 lemma gstar_rdistinct_general:
+ − 296 shows "rs1 @ rs \<leadsto>g* rs1 @ (rdistinct rs (set rs1))"
+ − 297 apply(induct rs arbitrary: rs1)
+ − 298 apply simp
+ − 299 apply(case_tac " a \<in> set rs1")
+ − 300 apply simp
+ − 301 apply(subgoal_tac "rs1 @ a # rs \<leadsto>g rs1 @ rs")
+ − 302 using gmany_steps_later apply auto[1]
+ − 303 apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
+ − 304 apply simp
+ − 305 apply(drule_tac x = "rs1 @ [a]" in meta_spec)
+ − 306 by simp
+ − 307
+ − 308
+ − 309 lemma gstar_rdistinct:
+ − 310 shows "rs \<leadsto>g* rdistinct rs {}"
+ − 311 apply(induct rs)
+ − 312 apply simp
+ − 313 by (metis append.left_neutral empty_set gstar_rdistinct_general)
+ − 314
475
+ − 315
+ − 316
471
+ − 317 lemma frewrite_append:
+ − 318 shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
+ − 319 apply(induct rs)
472
+ − 320 apply simp+
+ − 321 using frewrite.intros(3) by blast
475
+ − 322
+ − 323 lemma grewrite_append:
+ − 324 shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb"
+ − 325 apply(induct rs)
+ − 326 apply simp+
+ − 327 using grewrite.intros(3) by blast
472
+ − 328
471
+ − 329
+ − 330
+ − 331 lemma frewrites_cons:
+ − 332 shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"
472
+ − 333 apply(induct rsa rsb rule: frewrites.induct)
+ − 334 apply simp
+ − 335 using frewrite.intros(3) by blast
471
+ − 336
+ − 337
475
+ − 338 lemma grewrites_cons:
+ − 339 shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb"
+ − 340 apply(induct rsa rsb rule: grewrites.induct)
+ − 341 apply simp
+ − 342 using grewrite.intros(3) by blast
+ − 343
+ − 344
471
+ − 345 lemma frewrites_append:
+ − 346 shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"
472
+ − 347 apply(induct rs)
471
+ − 348 apply simp
472
+ − 349 by (simp add: frewrites_cons)
471
+ − 350
475
+ − 351 lemma grewrites_append:
+ − 352 shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)"
+ − 353 apply(induct rs)
+ − 354 apply simp
+ − 355 by (simp add: grewrites_cons)
+ − 356
471
+ − 357
+ − 358
+ − 359 lemma frewrites_concat:
+ − 360 shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)"
+ − 361 apply(induct rs1 rs2 rule: frewrite.induct)
+ − 362 apply(simp)
+ − 363 apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)")
+ − 364 prefer 2
+ − 365 using frewrite.intros(1) apply blast
+ − 366 apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)")
+ − 367 using many_steps_later apply blast
472
+ − 368 apply (simp add: frewrites_append)
+ − 369 apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)
+ − 370 using frewrites_cons by auto
471
+ − 371
475
+ − 372 lemma grewrites_concat:
+ − 373 shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)"
+ − 374 apply(induct rs1 rs2 rule: grewrite.induct)
+ − 375 apply(simp)
+ − 376 apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)")
+ − 377 prefer 2
+ − 378 using grewrite.intros(1) apply blast
+ − 379 apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)")
+ − 380 using gmany_steps_later apply blast
+ − 381 apply (simp add: grewrites_append)
+ − 382 apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later)
+ − 383 using grewrites_cons apply auto
+ − 384 apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb")
+ − 385 using grewrite.intros(4) grewrites.intros(2) apply force
+ − 386 using grewrites_append by auto
+ − 387
+ − 388
+ − 389 lemma grewritess_concat:
+ − 390 shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)"
+ − 391 apply(induct rsa rsb rule: grewrites.induct)
+ − 392 apply(case_tac rs)
+ − 393 apply simp
+ − 394 using grewrites_append apply blast
+ − 395 by (meson greal_trans grewrites.simps grewrites_concat)
+ − 396
476
+ − 397 fun alt_set:: "rrexp \<Rightarrow> rrexp set"
+ − 398 where
+ − 399 "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
+ − 400 | "alt_set r = {r}"
+ − 401
+ − 402 lemma alt_set_has_all:
+ − 403 shows "RALTS rs \<in> alt_set rx \<Longrightarrow> set rs \<subseteq> alt_set rx"
+ − 404 apply(induct rx arbitrary: rs)
+ − 405 apply simp_all
+ − 406 apply(rename_tac rSS rss)
+ − 407 using in_mono by fastforce
+ − 408
+ − 409
+ − 410
+ − 411
+ − 412
478
+ − 413 lemma grewrite_cases_middle:
+ − 414 shows "rs1 \<leadsto>g rs2 \<Longrightarrow>
+ − 415 (\<exists>rsa rsb rsc. rs1 = (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
+ − 416 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
+ − 417 (\<exists>rsa rsb rsc a. rs1 = rsa @ [a] @ rsb @ [a] @ rsc \<and> rs2 = rsa @ [a] @ rsb @ rsc)"
+ − 418 apply( induct rs1 rs2 rule: grewrite.induct)
+ − 419 apply simp
+ − 420 apply blast
+ − 421 apply (metis append_Cons append_Nil)
+ − 422 apply (metis append_Cons)
+ − 423 by blast
476
+ − 424
+ − 425
490
+ − 426 lemma good_singleton:
+ − 427 shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]"
+ − 428 using good.simps(1) k0b by blast
+ − 429
+ − 430
+ − 431
+ − 432
+ − 433
+ − 434
+ − 435
+ − 436 lemma all_that_same_elem:
+ − 437 shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
+ − 438 \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
+ − 439 apply(induct rs)
+ − 440 apply simp
+ − 441 apply(subgoal_tac "aa = a")
+ − 442 apply simp
+ − 443 by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
+ − 444
+ − 445 lemma distinct_early_app1:
+ − 446 shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
+ − 447 apply(induct rs arbitrary: rset rset1)
+ − 448 apply simp
+ − 449 apply simp
+ − 450 apply(case_tac "a \<in> rset1")
+ − 451 apply simp
+ − 452 apply(case_tac "a \<in> rset")
+ − 453 apply simp+
+ − 454
+ − 455 apply blast
+ − 456 apply(case_tac "a \<in> rset1")
+ − 457 apply simp+
+ − 458 apply(case_tac "a \<in> rset")
+ − 459 apply simp
+ − 460 apply (metis insert_subsetI)
+ − 461 apply simp
+ − 462 by (meson insert_mono)
+ − 463
+ − 464
+ − 465 lemma distinct_early_app:
+ − 466 shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
+ − 467 apply(induct rsb)
+ − 468 apply simp
+ − 469 using distinct_early_app1 apply blast
+ − 470 by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
+ − 471
+ − 472
+ − 473 lemma distinct_eq_interesting1:
+ − 474 shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
+ − 475 apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
+ − 476 apply(simp only:)
+ − 477 using distinct_early_app apply blast
+ − 478 by (metis append_Cons distinct_early_app rdistinct.simps(2))
+ − 479
+ − 480
+ − 481
+ − 482 lemma good_flatten_aux_aux1:
+ − 483 shows "\<lbrakk> size rs \<ge>2;
+ − 484 \<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>
+ − 485 \<Longrightarrow> rdistinct (rs @ rsb) rset =
+ − 486 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+ − 487 apply(induct rs arbitrary: rset)
+ − 488 apply simp
+ − 489 apply(case_tac "a \<in> rset")
+ − 490 apply simp
+ − 491 apply(case_tac "rdistinct rs {a}")
+ − 492 apply simp
+ − 493 apply(subst good_singleton)
+ − 494 apply force
+ − 495 apply simp
+ − 496 apply (meson all_that_same_elem)
+ − 497 apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
+ − 498 prefer 2
+ − 499 using k0a rsimp_ALTs.simps(3) apply presburger
+ − 500 apply(simp only:)
+ − 501 apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
+ − 502 apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
+ − 503 apply (meson distinct_eq_interesting1)
+ − 504 apply simp
+ − 505 apply(case_tac "rdistinct rs {a}")
+ − 506 prefer 2
+ − 507 apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
+ − 508 apply(simp only:)
+ − 509 apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
+ − 510 rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
+ − 511 apply simp
+ − 512 apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
+ − 513 using rsimp_ALTs.simps(3) apply presburger
+ − 514 by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
+ − 515
+ − 516
+ − 517
+ − 518
+ − 519
+ − 520 lemma good_flatten_aux_aux:
+ − 521 shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista;
+ − 522 \<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>
+ − 523 \<Longrightarrow> rdistinct (rs @ rsb) rset =
+ − 524 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+ − 525 apply(erule exE)+
+ − 526 apply(subgoal_tac "size rs \<ge> 2")
+ − 527 apply (metis good_flatten_aux_aux1)
+ − 528 by (simp add: Suc_leI length_Cons less_add_Suc1)
+ − 529
+ − 530
+ − 531
+ − 532 lemma good_flatten_aux:
491
+ − 533 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO;
+ − 534 \<forall>r\<in>set rsb. good r \<or> r = RZERO;
490
+ − 535 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
+ − 536 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ − 537 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
+ − 538 map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs;
+ − 539 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+ − 540 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
+ − 541 rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+ − 542 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
+ − 543 \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset =
+ − 544 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
+ − 545 apply simp
+ − 546 apply(case_tac "rflts rs ")
+ − 547 apply simp
+ − 548 apply(case_tac "list")
+ − 549 apply simp
+ − 550 apply(case_tac "a \<in> rset")
+ − 551 apply simp
+ − 552 apply (metis append_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff)
+ − 553 apply simp
+ − 554 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)
+ − 555 apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+ − 556 prefer 2
491
+ − 557 apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality)
490
+ − 558 apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+ − 559 prefer 2
491
+ − 560 apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality)
490
+ − 561 by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
+ − 562
+ − 563
+ − 564
+ − 565
+ − 566 lemma good_flatten_middle:
491
+ − 567 shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
490
+ − 568 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
+ − 569 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @
+ − 570 map rsimp rs @ map rsimp rsb)) {})")
+ − 571 prefer 2
+ − 572 apply simp
+ − 573 apply(simp only:)
+ − 574 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @
+ − 575 [rsimp (RALTS rs)] @ map rsimp rsb)) {})")
+ − 576 prefer 2
+ − 577 apply simp
+ − 578 apply(simp only:)
+ − 579 apply(subgoal_tac "map rsimp rsa = rsa")
+ − 580 prefer 2
491
+ − 581 apply (metis map_idI rsimp.simps(3) test)
490
+ − 582 apply(simp only:)
+ − 583 apply(subgoal_tac "map rsimp rsb = rsb")
+ − 584 prefer 2
491
+ − 585 apply (metis map_idI rsimp.simps(3) test)
490
+ − 586 apply(simp only:)
+ − 587 apply(subst k00)+
+ − 588 apply(subgoal_tac "map rsimp rs = rs")
+ − 589 apply(simp only:)
+ − 590 prefer 2
491
+ − 591 apply (metis map_idI rsimp.simps(3) test)
490
+ − 592 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+ − 593 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))")
+ − 594 apply(simp only:)
+ − 595 prefer 2
+ − 596 using rdistinct_concat_general apply blast
+ − 597 apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+ − 598 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+ − 599 apply(simp only:)
+ − 600 prefer 2
+ − 601 using rdistinct_concat_general apply blast
+ − 602 apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) =
+ − 603 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
491
+ − 604 apply presburger
490
+ − 605 using good_flatten_aux by blast
+ − 606
+ − 607
+ − 608 lemma simp_flatten3:
+ − 609 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
+ − 610 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ − 611 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
+ − 612 prefer 2
+ − 613 apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
+ − 614 apply (simp only:)
+ − 615 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) =
+ − 616 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
+ − 617 prefer 2
+ − 618 apply (metis map_append simp_flatten_aux0)
+ − 619 apply(simp only:)
+ − 620 apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
+ − 621 rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
+ − 622
+ − 623 apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
491
+ − 624 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
+ − 625 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
+ − 626 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
490
+ − 627
+ − 628 using good_flatten_middle apply presburger
+ − 629
491
+ − 630 apply (simp add: good1)
+ − 631 apply (simp add: good1)
+ − 632 apply (simp add: good1)
+ − 633
+ − 634 done
490
+ − 635
+ − 636
+ − 637
+ − 638
+ − 639
476
+ − 640 lemma grewrite_equal_rsimp:
+ − 641 shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
478
+ − 642 apply(frule grewrite_cases_middle)
+ − 643 apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")
+ − 644 using simp_flatten3 apply auto[1]
+ − 645 apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")
+ − 646 apply (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.set_intros(1) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) simp_removes_duplicate3)
+ − 647 by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)
476
+ − 648
+ − 649
475
+ − 650 lemma grewrites_equal_rsimp:
+ − 651 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
476
+ − 652 apply (induct rs1 rs2 rule: grewrites.induct)
475
+ − 653 apply simp
476
+ − 654 using grewrite_equal_rsimp by presburger
+ − 655
+ − 656
+ − 657
+ − 658
+ − 659 lemma grewrites_equal_simp_2:
+ − 660 shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
478
+ − 661 oops
+ − 662
+ − 663
+ − 664
475
+ − 665
476
+ − 666 lemma grewrites_last:
+ − 667 shows "r # [RALTS rs] \<leadsto>g* r # rs"
+ − 668 by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
+ − 669
+ − 670 lemma simp_flatten2:
+ − 671 shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
+ − 672 using grewrites_equal_rsimp grewrites_last by blast
475
+ − 673
473
+ − 674 lemma frewrites_middle:
+ − 675 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"
+ − 676 by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3))
471
+ − 677
473
+ − 678 lemma frewrites_alt:
+ − 679 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"
+ − 680 by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)
471
+ − 681
+ − 682 lemma early_late_der_frewrites:
+ − 683 shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"
+ − 684 apply(induct rs)
+ − 685 apply simp
+ − 686 apply(case_tac a)
+ − 687 apply simp+
+ − 688 using frewrite.intros(1) many_steps_later apply blast
+ − 689 apply(case_tac "x = x3")
472
+ − 690 apply simp
+ − 691 using frewrites_cons apply presburger
+ − 692 using frewrite.intros(1) many_steps_later apply fastforce
+ − 693 apply(case_tac "rnullable x41")
473
+ − 694 apply simp+
+ − 695 apply (simp add: frewrites_alt)
+ − 696 apply (simp add: frewrites_cons)
+ − 697 apply (simp add: frewrites_append)
+ − 698 by (simp add: frewrites_cons)
471
+ − 699
+ − 700
+ − 701
+ − 702
473
+ − 703 lemma with_wo0_distinct:
+ − 704 shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
+ − 705 apply(induct rs arbitrary: rset)
+ − 706 apply simp
+ − 707 apply(case_tac a)
+ − 708 apply(case_tac "RZERO \<in> rset")
+ − 709 apply simp+
+ − 710 using fr_in_rstar frewrite.intros(1) apply presburger
+ − 711 apply (case_tac "RONE \<in> rset")
+ − 712 apply simp+
+ − 713 using frewrites_cons apply presburger
+ − 714 apply(case_tac "a \<in> rset")
+ − 715 apply simp
+ − 716 apply (simp add: frewrites_cons)
+ − 717 apply(case_tac "a \<in> rset")
+ − 718 apply simp
+ − 719 apply (simp add: frewrites_cons)
+ − 720 apply(case_tac "a \<in> rset")
+ − 721 apply simp
+ − 722 apply (simp add: frewrites_cons)
+ − 723 apply(case_tac "a \<in> rset")
+ − 724 apply simp
+ − 725 apply (simp add: frewrites_cons)
+ − 726 done
+ − 727
476
+ − 728 (*Interesting lemma: not obvious but easily proven by sledgehammer*)
473
+ − 729
476
+ − 730
+ − 731
+ − 732
+ − 733 (*lemma induction last rule not go through
+ − 734 example:
+ − 735 r #
+ − 736 rdistinct rs1
+ − 737 (insert RZERO
+ − 738 (insert r
+ − 739 (rset \<union>
+ − 740 \<Union> (alt_set `
+ − 741 rset)))) \<leadsto>g* r #
+ − 742 rdistinct rs2
+ − 743 (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset))))
+ − 744 rs2 = [+rs] rs3 = rs,
+ − 745 r = +rs
+ − 746 [] \<leadsto>g* rs which is wrong
+ − 747 *)
+ − 748
469
+ − 749
+ − 750
476
+ − 751
+ − 752
+ − 753
+ − 754
+ − 755 lemma frewrite_simpeq:
+ − 756 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ − 757 apply(induct rs1 rs2 rule: frewrite.induct)
+ − 758 apply simp
+ − 759 using simp_flatten apply presburger
478
+ − 760 by (metis (no_types, opaque_lifting) grewrites_equal_rsimp grewrites_last list.simps(9) rsimp.simps(2))
+ − 761
+ − 762 lemma gstar0:
+ − 763 shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"
+ − 764 apply(induct rs arbitrary: rsa)
+ − 765 apply simp
+ − 766 apply(case_tac "a = RZERO")
+ − 767 apply simp
+ − 768
+ − 769 using gr_in_rstar grewrite.intros(1) grewrites_append apply presburger
+ − 770 apply(case_tac "a \<in> set rsa")
+ − 771 apply simp+
+ − 772 apply(drule_tac x = "rsa @ [a]" in meta_spec)
+ − 773 by simp
+ − 774
+ − 775 lemma gstar01:
+ − 776 shows "rdistinct rs {} \<leadsto>g* rdistinct rs {RZERO}"
+ − 777 by (metis empty_set gstar0 self_append_conv2)
+ − 778
+ − 779
+ − 780 lemma grewrite_rdistinct_aux:
+ − 781 shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
480
+ − 782 apply(induct rsa arbitrary: rs rset)
+ − 783 apply simp
+ − 784 apply(case_tac " a \<in> rset")
+ − 785 apply simp
+ − 786 apply(case_tac "a \<in> set rs")
+ − 787 apply simp
+ − 788 apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)
+ − 789 apply simp
+ − 790 apply(drule_tac x = "rs @ [a]" in meta_spec)
+ − 791 by (metis Un_insert_left Un_insert_right append.assoc append.right_neutral append_Cons append_Nil insert_absorb2 list.simps(15) set_append)
+ − 792
478
+ − 793
+ − 794 lemma grewrite_rdistinct_worth1:
+ − 795 shows "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)"
+ − 796 by (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
+ − 797
+ − 798 lemma grewrite_rdisitinct:
+ − 799 shows "rs @ rdistinct rsa {RALTS rs} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))"
+ − 800 apply(induct rsa arbitrary: rs)
+ − 801 apply simp
+ − 802 apply(case_tac "a = RALTS rs")
+ − 803 apply simp
+ − 804 apply(case_tac "a \<in> set rs")
+ − 805 apply simp
+ − 806 apply(subgoal_tac "rs @
+ − 807 a # rdistinct rsa {RALTS rs, a} \<leadsto>g rs @ rdistinct rsa {RALTS rs, a}")
+ − 808 apply(subgoal_tac
+ − 809 "rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))")
+ − 810 using gmany_steps_later apply blast
+ − 811 apply(subgoal_tac
+ − 812 " rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa ({RALTS rs, a} \<union> set rs)")
+ − 813 apply (simp add: insert_absorb)
+ − 814 using grewrite_rdistinct_aux apply blast
+ − 815 using grewrite_variant1 apply blast
+ − 816 by (metis grewrite_rdistinct_aux insert_is_Un)
+ − 817
+ − 818
+ − 819 lemma frewrite_rd_grewrites_general:
+ − 820 shows "\<lbrakk>rs1 \<leadsto>f rs2; \<And>rs. \<exists>rs3.
+ − 821 (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3)\<rbrakk>
+ − 822 \<Longrightarrow>
+ − 823 \<exists>rs3. (rs @ (r # rdistinct rs1 (set rs \<union> {r})) \<leadsto>g* rs3) \<and> (rs @ (r # rdistinct rs2 (set rs \<union> {r})) \<leadsto>g* rs3)"
+ − 824 apply(drule_tac x = "rs @ [r]" in meta_spec )
+ − 825 by simp
+ − 826
+ − 827
479
+ − 828 lemma alts_g_can_flts:
+ − 829 shows "RALTS rs \<in> set rsb \<Longrightarrow> \<exists>rs1 rs2.( rflts rsb = rs1 @ rs @ rs2)"
+ − 830 by (metis flts_append rflts.simps(3) split_list_last)
+ − 831
+ − 832 lemma flts_gstar:
+ − 833 shows "rs \<leadsto>g* rflts rs"
480
+ − 834 apply(induct rs)
+ − 835 apply simp
+ − 836 apply(case_tac "a = RZERO")
+ − 837 apply simp
+ − 838 using gmany_steps_later grewrite.intros(1) apply blast
+ − 839 apply(case_tac "\<exists>rsa. a = RALTS rsa")
+ − 840 apply(erule exE)
+ − 841 apply simp
+ − 842 apply (meson grewrite.intros(2) grewrites.simps grewrites_cons)
+ − 843 by (simp add: grewrites_cons rflts_def_idiot)
+ − 844
479
+ − 845
480
+ − 846 lemma wrong1:
479
+ − 847 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))"
480
+ − 848
+ − 849 oops
+ − 850
+ − 851 lemma more_distinct1:
+ − 852 shows " \<lbrakk>\<And>rsb rset rset2.
+ − 853 rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2);
+ − 854 rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk>
+ − 855 \<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ − 856 apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)")
+ − 857 apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)")
+ − 858 apply (meson greal_trans)
+ − 859 apply (metis Un_iff Un_insert_left insert_absorb)
+ − 860 by (simp add: gr_in_rstar grewrite_variant1 in_mono)
+ − 861
+ − 862
+ − 863
+ − 864
478
+ − 865
479
+ − 866 lemma grewrites_in_distinct0:
+ − 867 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)"
+ − 868 apply(case_tac "a \<in> rset")
+ − 869 apply simp
+ − 870 apply simp
+ − 871 oops
+ − 872
+ − 873
+ − 874
+ − 875
+ − 876
+ − 877
+ − 878
478
+ − 879
+ − 880
+ − 881 lemma frewrite_rd_grewrites_aux:
480
+ − 882 shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 883 rsb @
+ − 884 RALTS rs #
+ − 885 rdistinct rsa
+ − 886 (insert (RALTS rs)
+ − 887 (set rsb)) \<leadsto>g* rflts rsb @
+ − 888 rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
478
+ − 889
480
+ − 890 apply simp
+ − 891 apply(subgoal_tac "rsb @
+ − 892 RALTS rs #
+ − 893 rdistinct rsa
+ − 894 (insert (RALTS rs)
+ − 895 (set rsb)) \<leadsto>g* rsb @
+ − 896 rs @
+ − 897 rdistinct rsa
+ − 898 (insert (RALTS rs)
+ − 899 (set rsb)) ")
+ − 900 apply(subgoal_tac " rsb @
+ − 901 rs @
+ − 902 rdistinct rsa
+ − 903 (insert (RALTS rs)
+ − 904 (set rsb)) \<leadsto>g*
+ − 905 rsb @
+ − 906 rdistinct rs (set rsb) @
+ − 907 rdistinct rsa
+ − 908 (insert (RALTS rs)
+ − 909 (set rsb)) ")
+ − 910 apply (smt (verit, ccfv_SIG) Un_insert_left flts_gstar greal_trans grewrite_rdistinct_aux grewritess_concat inf_sup_aci(5) rdistinct_concat_general rdistinct_set_equality set_append)
+ − 911 apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+ − 912 by (simp add: gr_in_rstar grewrite.intros(2) grewrites_append)
478
+ − 913
+ − 914
479
+ − 915
478
+ − 916
+ − 917 lemma list_dlist_union:
+ − 918 shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"
+ − 919 by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)
+ − 920
+ − 921 lemma subset_distinct_rewrite1:
+ − 922 shows "set1 \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs set1)"
+ − 923 apply(induct rs arbitrary: rsb)
+ − 924 apply simp
+ − 925 apply(case_tac "a \<in> set1")
+ − 926 apply simp
+ − 927
+ − 928 using gmany_steps_later grewrite_variant1 apply blast
+ − 929 apply simp
+ − 930 apply(drule_tac x = "rsb @ [a]" in meta_spec)
+ − 931 apply(subgoal_tac "set1 \<subseteq> set (rsb @ [a])")
+ − 932 apply (simp only:)
+ − 933 apply(subgoal_tac "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)")
+ − 934 apply (metis (no_types, opaque_lifting) append.assoc append_Cons append_Nil greal_trans)
+ − 935 apply (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
+ − 936 by auto
+ − 937
+ − 938
+ − 939 lemma subset_distinct_rewrite:
+ − 940 shows "set rsb' \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs (set rsb'))"
+ − 941 by (simp add: subset_distinct_rewrite1)
+ − 942
+ − 943
+ − 944
+ − 945 lemma distinct_3list:
+ − 946 shows "rsb @ (rdistinct rs (set rsb)) @ rsa \<leadsto>g*
+ − 947 rsb @ (rdistinct rs (set rsb)) @ (rdistinct rsa (set rs))"
+ − 948 by (metis append.assoc list_dlist_union set_append subset_distinct_rewrite)
+ − 949
+ − 950
+ − 951
+ − 952
+ − 953 lemma grewrites_shape1:
+ − 954 shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 955 rsb @
+ − 956 RALTS rs #
+ − 957 rdistinct rsa
+ − 958 (
+ − 959 (set rsb)) \<leadsto>g* rsb @
+ − 960 rdistinct rs (set rsb) @
+ − 961 rdistinct (rflts (rdistinct rsa ( (set rsb \<union> set rs)))) (set rs)"
+ − 962
+ − 963
+ − 964 apply (subgoal_tac " rsb @
+ − 965 RALTS rs #
+ − 966 rdistinct rsa
+ − 967 (
+ − 968 (set rsb)) \<leadsto>g* rsb @
+ − 969 rs @
+ − 970 rdistinct rsa
+ − 971 (
+ − 972 (set rsb)) ")
+ − 973 prefer 2
+ − 974 using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
+ − 975 apply(subgoal_tac "rsb @ rs @ rdistinct rsa ( (set rsb)) \<leadsto>g* rsb @
+ − 976 (rdistinct rs (set rsb) @ rdistinct rsa ( (set rsb)))")
+ − 977 prefer 2
+ − 978 apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+ − 979 apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct rsa ( (set rsb))
+ − 980 \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct rsa ( (set rsb) \<union> (set rs))")
+ − 981 prefer 2
+ − 982 apply (smt (verit, best) append.assoc append_assoc boolean_algebra_cancel.sup2 grewrite_rdistinct_aux inf_sup_aci(5) insert_is_Un rdistinct_concat_general rdistinct_set_equality set_append sup.commute sup.right_idem sup_commute)
+ − 983 apply(subgoal_tac "rdistinct rsa ( (set rsb) \<union> set rs) \<leadsto>g*
+ − 984 rflts (rdistinct rsa ( (set rsb) \<union> set rs))")
+ − 985 apply(subgoal_tac "rsb @ (rdistinct rs (set rsb)) @ rflts (rdistinct rsa ( (set rsb) \<union> set rs)) \<leadsto>g*
+ − 986 rsb @ (rdistinct rs (set rsb)) @ (rdistinct (rflts (rdistinct rsa ( (set rsb) \<union> set rs))) (set rs))")
+ − 987 apply (smt (verit, ccfv_SIG) Un_insert_left greal_trans grewrites_append)
+ − 988 using distinct_3list apply presburger
+ − 989 using flts_gstar apply blast
+ − 990 done
+ − 991
+ − 992 lemma r_finite1:
+ − 993 shows "r = RALTS (r # rs) = False"
+ − 994 apply(induct r)
+ − 995 apply simp+
+ − 996 apply (metis list.set_intros(1))
+ − 997 by blast
+ − 998
+ − 999
+ − 1000
+ − 1001 lemma grewrite_singleton:
+ − 1002 shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []"
+ − 1003 apply (induct "[r]" "r # rs" rule: grewrite.induct)
+ − 1004 apply simp
+ − 1005 apply (metis r_finite1)
+ − 1006 using grewrite.simps apply blast
+ − 1007 by simp
+ − 1008
+ − 1009 lemma impossible_grewrite1:
+ − 1010 shows "\<not>( [RONE] \<leadsto>g [])"
+ − 1011 using grewrite.cases by fastforce
+ − 1012
+ − 1013
+ − 1014 lemma impossible_grewrite2:
+ − 1015 shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)"
+ − 1016 using grewrite_singleton by blast
+ − 1017
+ − 1018
+ − 1019
+ − 1020
479
+ − 1021 lemma wront_sublist_grewrites:
478
+ − 1022 shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
+ − 1023 apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct)
+ − 1024 apply simp
+ − 1025 apply(drule_tac x = "[x] @ rs2" in meta_spec)
+ − 1026 apply(drule_tac x = "[x] @ rs3" in meta_spec)
+ − 1027 apply(simp)
+ − 1028
+ − 1029 oops
+ − 1030
+ − 1031
+ − 1032
+ − 1033
479
+ − 1034 lemma concat_rdistinct_equality1:
+ − 1035 shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \<union> (set rs))"
+ − 1036 apply(induct rs arbitrary: rsa rset)
478
+ − 1037 apply simp
479
+ − 1038 apply(case_tac "a \<in> rset")
+ − 1039 apply simp
+ − 1040 apply (simp add: insert_absorb)
+ − 1041 by auto
478
+ − 1042
480
+ − 1043 lemma middle_grewrites:
+ − 1044 "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsa @ rs1 @ rsb \<leadsto>g* rsa @ rs2 @ rsb "
+ − 1045 by (simp add: grewritess_concat)
+ − 1046
+ − 1047 lemma rdistinct_removes_all:
+ − 1048 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct rs rset = []"
+ − 1049
+ − 1050 by (metis append.right_neutral rdistinct.simps(1) rdistinct_concat)
478
+ − 1051
479
+ − 1052 lemma ends_removal:
+ − 1053 shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc"
480
+ − 1054 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g*
+ − 1055 rsb @ rdistinct rs (set rsb) @ rs @ rsc")
+ − 1056 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rs @ rsc \<leadsto>g*
+ − 1057 rsb @ rdistinct rs (set rsb) @ rdistinct rs (set (rsb @ rdistinct rs (set rsb))) @ rsc")
+ − 1058 apply (metis (full_types) append_Nil2 append_eq_appendI greal_trans list_dlist_union rdistinct_removes_all set_append)
+ − 1059 apply (metis append.assoc append_Nil gstar_rdistinct_general middle_grewrites)
+ − 1060 using gr_in_rstar grewrite.intros(2) grewrites_append by presburger
478
+ − 1061
479
+ − 1062 lemma grewrites_rev_append:
+ − 1063 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"
+ − 1064 using grewritess_concat by auto
478
+ − 1065
479
+ − 1066 lemma grewrites_inclusion:
+ − 1067 shows "set rs \<subseteq> set rs1 \<Longrightarrow> rs1 @ rs \<leadsto>g* rs1"
+ − 1068 apply(induct rs arbitrary: rs1)
+ − 1069 apply simp
+ − 1070 by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1))
478
+ − 1071
479
+ − 1072 lemma distinct_keeps_last:
+ − 1073 shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+ − 1074 by (simp add: concat_rdistinct_equality1)
478
+ − 1075
480
+ − 1076 lemma grewrites_shape2_aux:
478
+ − 1077 shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 1078 rsb @
+ − 1079 rdistinct (rs @ rsa)
+ − 1080 (set rsb) \<leadsto>g* rsb @
+ − 1081 rdistinct rs (set rsb) @
479
+ − 1082 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ − 1083 apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) = rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb)")
+ − 1084 apply (simp only:)
+ − 1085 prefer 2
+ − 1086 apply (simp add: Un_commute concat_rdistinct_equality1)
+ − 1087 apply(induct rsa arbitrary: rs rsb rule: rev_induct)
+ − 1088 apply simp
+ − 1089 apply(case_tac "x \<in> set rs")
+ − 1090 apply (simp add: distinct_removes_middle3)
+ − 1091 apply(case_tac "x = RALTS rs")
+ − 1092 apply simp
+ − 1093 apply(case_tac "x \<in> set rsb")
+ − 1094 apply simp
+ − 1095 apply (simp add: concat_rdistinct_equality1)
+ − 1096 apply (simp add: concat_rdistinct_equality1)
+ − 1097 apply simp
+ − 1098 apply(drule_tac x = "rs " in meta_spec)
+ − 1099 apply(drule_tac x = rsb in meta_spec)
+ − 1100 apply simp
+ − 1101 apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (insert (RALTS rs) (set rs \<union> set rsb))")
+ − 1102 prefer 2
+ − 1103 apply (simp add: concat_rdistinct_equality1)
+ − 1104 apply(case_tac "x \<in> set xs")
+ − 1105 apply simp
+ − 1106 apply (simp add: distinct_removes_last2)
+ − 1107 apply(case_tac "x \<in> set rsb")
+ − 1108 apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2))
+ − 1109 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (set rs \<union> set rsb) = rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x]")
+ − 1110 apply(simp only:)
+ − 1111 apply(case_tac "x = RALTS rs")
+ − 1112 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x] \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs")
+ − 1113 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) ")
+ − 1114 apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2))
+ − 1115 apply(subgoal_tac "set rs \<subseteq> set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb))")
+ − 1116 apply (metis append.assoc grewrites_inclusion)
+ − 1117 apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append)
+ − 1118 apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append)
+ − 1119 apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (insert (RALTS rs) (set rs \<union> set rsb)) = rsb @ rdistinct rs (set rsb) @ rdistinct (xs) (insert (RALTS rs) (set rs \<union> set rsb)) @ [x]")
+ − 1120 apply(simp only:)
+ − 1121 apply (metis append.assoc grewrites_rev_append)
+ − 1122 apply (simp add: insert_absorb)
+ − 1123 apply (simp add: distinct_keeps_last)+
+ − 1124 done
478
+ − 1125
480
+ − 1126 lemma grewrites_shape2:
+ − 1127 shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 1128 rsb @
+ − 1129 rdistinct (rs @ rsa)
+ − 1130 (set rsb) \<leadsto>g* rflts rsb @
+ − 1131 rdistinct rs (set rsb) @
+ − 1132 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ − 1133 apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat)
+ − 1134 done
+ − 1135
479
+ − 1136 lemma rdistinct_add_acc:
+ − 1137 shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ − 1138 apply(induct rs arbitrary: rsb rset rset2)
+ − 1139 apply simp
+ − 1140 apply (case_tac "a \<in> rset")
+ − 1141 apply simp
+ − 1142 apply(case_tac "a \<in> rset2")
480
+ − 1143 apply simp
+ − 1144 apply (simp add: more_distinct1)
479
+ − 1145 apply simp
+ − 1146 apply(drule_tac x = "rsb @ [a]" in meta_spec)
+ − 1147 by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)
+ − 1148
478
+ − 1149
479
+ − 1150 lemma frewrite_fun1:
+ − 1151 shows " RALTS rs \<in> set rsb \<Longrightarrow>
+ − 1152 rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)"
+ − 1153 apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb)")
+ − 1154 apply(subgoal_tac " set rs \<subseteq> set (rflts rsb)")
+ − 1155 prefer 2
+ − 1156 using spilled_alts_contained apply blast
+ − 1157 apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)")
+ − 1158 using greal_trans apply blast
+ − 1159 using rdistinct_add_acc apply presburger
+ − 1160 using flts_gstar grewritess_concat by auto
+ − 1161
478
+ − 1162
+ − 1163
+ − 1164
476
+ − 1165
+ − 1166 lemma frewrite_rd_grewrites:
+ − 1167 shows "rs1 \<leadsto>f rs2 \<Longrightarrow>
478
+ − 1168 \<exists>rs3. (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3) "
+ − 1169 apply(induct rs1 rs2 arbitrary: rs rule: frewrite.induct)
+ − 1170 apply(rule_tac x = "rsa @ (rdistinct rs ({RZERO} \<union> set rsa))" in exI)
476
+ − 1171 apply(rule conjI)
478
+ − 1172 apply(case_tac "RZERO \<in> set rsa")
+ − 1173 apply simp+
+ − 1174 using gstar0 apply fastforce
+ − 1175 apply (simp add: gr_in_rstar grewrite.intros(1) grewrites_append)
+ − 1176 apply (simp add: gstar0)
+ − 1177 prefer 2
+ − 1178 apply(case_tac "r \<in> set rs")
+ − 1179 apply simp
+ − 1180 apply(drule_tac x = "rs @ [r]" in meta_spec)
+ − 1181 apply(erule exE)
+ − 1182 apply(rule_tac x = "rs3" in exI)
+ − 1183 apply simp
+ − 1184 apply(case_tac "RALTS rs \<in> set rsb")
+ − 1185 apply simp
479
+ − 1186 apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" in exI)
478
+ − 1187 apply(rule conjI)
479
+ − 1188 using frewrite_fun1 apply force
+ − 1189 apply (metis frewrite_fun1 rdistinct_concat sup_ge2)
478
+ − 1190 apply(simp)
+ − 1191 apply(rule_tac x =
480
+ − 1192 "rflts rsb @
479
+ − 1193 rdistinct rs (set rsb) @
+ − 1194 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)
478
+ − 1195 apply(rule conjI)
+ − 1196 prefer 2
+ − 1197 using grewrites_shape2 apply force
480
+ − 1198 using frewrite_rd_grewrites_aux by blast
478
+ − 1199
473
+ − 1200
476
+ − 1201
+ − 1202 lemma frewrites_rd_grewrites:
+ − 1203 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
478
+ − 1204 rsimp (RALTS rs1) = rsimp (RALTS rs2)"
476
+ − 1205 apply(induct rs1 rs2 rule: frewrites.induct)
+ − 1206 apply simp
479
+ − 1207 using frewrite_simpeq by presburger
476
+ − 1208
+ − 1209 lemma frewrite_simpeq2:
+ − 1210 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
478
+ − 1211 apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")
+ − 1212 using grewrites_equal_rsimp apply fastforce
479
+ − 1213 by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))
+ − 1214
+ − 1215
+ − 1216
478
+ − 1217
492
+ − 1218 (*a more refined notion of h\<leadsto>* is needed,
473
+ − 1219 this lemma fails when rs1 contains some RALTS rs where elements
+ − 1220 of rs appear in later parts of rs1, which will be picked up by rs2
+ − 1221 and deduplicated*)
476
+ − 1222 lemma frewrites_simpeq:
473
+ − 1223 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
476
+ − 1224 rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
+ − 1225 apply(induct rs1 rs2 rule: frewrites.induct)
+ − 1226 apply simp
478
+ − 1227 using frewrite_simpeq2 by presburger
476
+ − 1228
473
+ − 1229
+ − 1230 lemma frewrite_single_step:
+ − 1231 shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
+ − 1232 apply(induct rs2 rs3 rule: frewrite.induct)
+ − 1233 apply simp
+ − 1234 using simp_flatten apply blast
+ − 1235 by (metis (no_types, opaque_lifting) list.simps(9) rsimp.simps(2) simp_flatten2)
+ − 1236
+ − 1237 lemma frewrites_equivalent_simp:
+ − 1238 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ − 1239 apply(induct rs1 rs2 rule: frewrites.induct)
+ − 1240 apply simp
+ − 1241 using frewrite_single_step by presburger
+ − 1242
476
+ − 1243 lemma grewrite_simpalts:
+ − 1244 shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ − 1245 apply(induct rs2 rs3 rule : grewrite.induct)
+ − 1246 using identity_wwo0 apply presburger
+ − 1247 apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten)
+ − 1248 apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3))
+ − 1249 apply simp
+ − 1250 apply(subst rsimp_alts_equal)
+ − 1251 apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []")
+ − 1252 apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]")
+ − 1253 apply (simp only:)
+ − 1254 apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2))
+ − 1255 apply simp
+ − 1256 by (smt (verit, best) append.assoc append_Cons frewrite.intros(1) frewrite_single_step identity_wwo0 in_set_conv_decomp rsimp_ALTs.simps(3) simp_removes_duplicate3)
+ − 1257
+ − 1258
+ − 1259 lemma grewrites_simpalts:
+ − 1260 shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ − 1261 apply(induct rs2 rs3 rule: grewrites.induct)
+ − 1262 apply simp
+ − 1263 using grewrite_simpalts by presburger
473
+ − 1264
476
+ − 1265
473
+ − 1266
+ − 1267
+ − 1268
467
+ − 1269 lemma simp_der_flts:
471
+ − 1270 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) =
+ − 1271 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
473
+ − 1272 apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
478
+ − 1273 using frewrites_simpeq apply presburger
+ − 1274 using early_late_der_frewrites by auto
+ − 1275
+ − 1276
476
+ − 1277
+ − 1278
+ − 1279
+ − 1280
+ − 1281
+ − 1282
+ − 1283
+ − 1284
+ − 1285 lemma simp_der_pierce_flts_prelim:
+ − 1286 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {}))
+ − 1287 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
478
+ − 1288 by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
467
+ − 1289
+ − 1290
465
+ − 1291 lemma simp_der_pierce_flts:
471
+ − 1292 shows " rsimp (
+ − 1293 rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
+ − 1294 ) =
+ − 1295 rsimp (
+ − 1296 rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
+ − 1297 )"
476
+ − 1298 using simp_der_pierce_flts_prelim by presburger
465
+ − 1299
453
+ − 1300
+ − 1301
+ − 1302 lemma simp_more_distinct:
465
+ − 1303 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
480
+ − 1304 oops
465
+ − 1305
453
+ − 1306
+ − 1307 lemma non_empty_list:
+ − 1308 shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
+ − 1309 by (metis empty_iff empty_set)
+ − 1310
456
+ − 1311 lemma distinct_comp:
+ − 1312 shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+ − 1313 apply(induct rs2 arbitrary: rs1)
+ − 1314 apply simp
+ − 1315 apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2")
+ − 1316 apply(simp only:)
+ − 1317 apply(case_tac "a \<in> set rs1")
+ − 1318 apply simp
+ − 1319 oops
453
+ − 1320
456
+ − 1321 lemma instantiate1:
+ − 1322 shows "\<lbrakk>\<And>ab rset1. rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow>
+ − 1323 rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset"
+ − 1324 apply(drule_tac x = "aa" in meta_spec)
+ − 1325 apply(drule_tac x = "rset" in meta_spec)
453
+ − 1326 apply simp
456
+ − 1327 done
+ − 1328
+ − 1329
+ − 1330 lemma not_head_elem:
+ − 1331 shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa"
+ − 1332
+ − 1333 by fastforce
+ − 1334
+ − 1335 (*
+ − 1336 apply simp
+ − 1337 apply (metis append_Cons)
+ − 1338 apply(case_tac "ab \<in> rset1")
+ − 1339 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+ − 1340 apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 =
+ − 1341 ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))")
+ − 1342 apply(simp only:)
+ − 1343 apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))")
+ − 1344 apply(simp only:)
+ − 1345 apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)")
+ − 1346 apply blast
+ − 1347 *)
+ − 1348
453
+ − 1349
+ − 1350 lemma flts_identity1:
+ − 1351 shows "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
+ − 1352 apply(induct rs)
+ − 1353 apply simp+
+ − 1354 apply(case_tac a)
+ − 1355 apply simp
+ − 1356 apply simp+
+ − 1357 done
+ − 1358
+ − 1359 lemma flts_identity10:
+ − 1360 shows " rflts (rs @ [RCHAR c]) = rflts rs @ [RCHAR c]"
+ − 1361 apply(induct rs)
+ − 1362 apply simp+
+ − 1363 apply(case_tac a)
+ − 1364 apply simp+
+ − 1365 done
+ − 1366
+ − 1367 lemma flts_identity11:
+ − 1368 shows " rflts (rs @ [RSEQ r1 r2]) = rflts rs @ [RSEQ r1 r2]"
+ − 1369 apply(induct rs)
+ − 1370 apply simp+
+ − 1371 apply(case_tac a)
+ − 1372 apply simp+
+ − 1373 done
+ − 1374
+ − 1375 lemma flts_identity12:
+ − 1376 shows " rflts (rs @ [RSTAR r0]) = rflts rs @ [RSTAR r0]"
+ − 1377 apply(induct rs)
+ − 1378 apply simp+
+ − 1379 apply(case_tac a)
+ − 1380 apply simp+
+ − 1381 done
+ − 1382
+ − 1383 lemma flts_identity2:
+ − 1384 shows "a \<noteq> RZERO \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (rs @ [a]) = rflts rs @ [a]"
+ − 1385 apply(case_tac a)
+ − 1386 apply simp
+ − 1387 using flts_identity1 apply auto[1]
+ − 1388 using flts_identity10 apply blast
+ − 1389 using flts_identity11 apply auto[1]
+ − 1390 apply blast
+ − 1391 using flts_identity12 by presburger
456
+ − 1392
+ − 1393 lemma flts_identity3:
+ − 1394 shows "a = RZERO \<Longrightarrow> rflts (rs @ [a]) = rflts rs"
+ − 1395 apply simp
+ − 1396 apply(induct rs)
+ − 1397 apply simp+
+ − 1398 apply(case_tac aa)
+ − 1399 apply simp+
+ − 1400 done
+ − 1401
+ − 1402 lemma distinct_removes_last3:
465
+ − 1403 shows "\<lbrakk>a \<in> set as\<rbrakk>
456
+ − 1404 \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
465
+ − 1405 by (simp add: distinct_removes_last2)
456
+ − 1406
+ − 1407 lemma set_inclusion_with_flts1:
+ − 1408 shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE \<in> set (rflts rs)"
+ − 1409 apply(induct rs)
+ − 1410 apply simp
+ − 1411 apply(case_tac " RONE \<in> set rs")
+ − 1412 apply simp
+ − 1413 apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append)
+ − 1414 apply(case_tac "RONE = a")
+ − 1415 apply simp
+ − 1416 apply simp
+ − 1417 done
+ − 1418
+ − 1419 lemma set_inclusion_with_flts10:
+ − 1420 shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x \<in> set (rflts rs)"
+ − 1421 apply(induct rs)
+ − 1422 apply simp
+ − 1423 apply(case_tac " RCHAR x \<in> set rs")
+ − 1424 apply simp
+ − 1425 apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+ − 1426 apply(case_tac "RCHAR x = a")
+ − 1427 apply simp
+ − 1428 apply fastforce
+ − 1429 apply simp
+ − 1430 done
+ − 1431
+ − 1432 lemma set_inclusion_with_flts11:
+ − 1433 shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2 \<in> set (rflts rs)"
+ − 1434 apply(induct rs)
+ − 1435 apply simp
+ − 1436 apply(case_tac " RSEQ r1 r2 \<in> set rs")
+ − 1437 apply simp
+ − 1438 apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+ − 1439 apply(case_tac "RSEQ r1 r2 = a")
+ − 1440 apply simp
+ − 1441 apply fastforce
+ − 1442 apply simp
+ − 1443 done
+ − 1444
+ − 1445
+ − 1446 lemma set_inclusion_with_flts:
+ − 1447 shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
+ − 1448 by (simp add: set_inclusion_with_flts1)
453
+ − 1449
480
+ − 1450 lemma can_spill_lst:"\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
456
+ − 1451 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =
+ − 1452 rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
480
+ − 1453
+ − 1454 using flts_append rflts_spills_last rsimp_inner_idem4 by presburger
+ − 1455
+ − 1456
+ − 1457
+ − 1458
+ − 1459
+ − 1460 lemma common_rewrites_equal:
+ − 1461 shows "(rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) \<Longrightarrow> rsimp (rsimp_ALTs rs1 ) = rsimp (rsimp_ALTs rs2)"
+ − 1462 using grewrites_simpalts by force
+ − 1463
+ − 1464
+ − 1465 lemma basic_regex_property1:
+ − 1466 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
484
+ − 1467 apply(induct r rule: rsimp.induct)
+ − 1468 apply(auto)
+ − 1469 apply (metis idiot idiot2 rrexp.distinct(5))
+ − 1470 by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
480
+ − 1471
+ − 1472
+ − 1473 thm rsimp_SEQ.elims
+ − 1474
+ − 1475
+ − 1476 lemma basic_rsimp_SEQ_property2:
+ − 1477 shows "\<lbrakk>r1 \<noteq> RZERO ; r1 \<noteq> RONE; r2 \<noteq> RZERO\<rbrakk> \<Longrightarrow>rsimp_SEQ r1 r2 = RSEQ r1 r2"
+ − 1478 apply(case_tac r1)
+ − 1479 apply simp+
+ − 1480 apply (simp add: idiot2)
+ − 1481 using idiot2 apply blast
+ − 1482 using idiot2 apply auto[1]
+ − 1483 using idiot2 by blast
+ − 1484
+ − 1485
+ − 1486 (*
+ − 1487 lemma rderssimp_same_rewrites_rder_induct1:
+ − 1488 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ − 1489 ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow>
+ − 1490 \<exists>rs3. ([rder x (rsimp (RSEQ r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RSEQ r1 r2)] \<leadsto>g* rs3) "
+ − 1491 sorry
+ − 1492
+ − 1493 lemma rderssimp_same_rewrites_rder_induct2:
+ − 1494 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) \<rbrakk> \<Longrightarrow>
+ − 1495 \<exists>rs3. ([rder x (rsimp (RSTAR r1))] \<leadsto>g* rs3) \<and> ([rder x (RSTAR r1)] \<leadsto>g* rs3) "
+ − 1496 sorry
+ − 1497
+ − 1498 lemma rderssimp_same_rewrites_rder_induct3:
+ − 1499 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ − 1500 ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow>
+ − 1501 \<exists>rs3. ([rder x (rsimp (RALT r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RALT r1 r2)] \<leadsto>g* rs3) "
+ − 1502 sorry
+ − 1503
+ − 1504 lemma rderssimp_same_rewrites_rder_induct4:
+ − 1505 shows "\<lbrakk>\<forall>r \<in> set rs. \<exists> rsa. ([rder x (rsimp r)] \<leadsto>g* rsa ) \<and> ([rder x r] \<leadsto>g* rsa) \<rbrakk> \<Longrightarrow>
+ − 1506 \<exists>rsb. ([rder x (rsimp (RALTS rs))] \<leadsto>g* rsb) \<and> ([rder x (RALTS rs)] \<leadsto>g* rsb) "
+ − 1507 sorry
+ − 1508
+ − 1509 lemma rderssimp_same_rewrites_rder_base1:
+ − 1510 shows "([rder x (rsimp RONE)] \<leadsto>g* [] ) \<and> ([rder x RONE] \<leadsto>g* [])"
+ − 1511 by (simp add: gr_in_rstar grewrite.intros(1))
+ − 1512
+ − 1513 lemma rderssimp_same_rewrites_rder_base2:
+ − 1514 shows " ([rder x (rsimp RZERO)] \<leadsto>g* [] ) \<and> ([rder x RZERO] \<leadsto>g* [])"
+ − 1515 using rderssimp_same_rewrites_rder_base1 by auto
+ − 1516
+ − 1517 lemma rderssimp_same_rewrites_rder_base3:
+ − 1518 shows " ([rder x (rsimp (RCHAR c))] \<leadsto>g* [] ) \<and> ([rder x (RCHAR c)] \<leadsto>g* [])"
+ − 1519 sorry
+ − 1520 *)
+ − 1521
+ − 1522 lemma inside_simp_seq_nullable:
+ − 1523 shows
+ − 1524 "\<And>r1 r2.
+ − 1525 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+ − 1526 rnullable r1\<rbrakk>
+ − 1527 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+ − 1528 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+ − 1529 apply(case_tac "rsimp r1 = RONE")
+ − 1530 apply(simp)
+ − 1531 apply(subst basic_rsimp_SEQ_property1)
+ − 1532 apply (simp add: idem_after_simp1)
+ − 1533 apply(case_tac "rsimp r1 = RZERO")
+ − 1534
+ − 1535 using basic_regex_property1 apply blast
+ − 1536 apply(case_tac "rsimp r2 = RZERO")
+ − 1537
+ − 1538 apply (simp add: basic_rsimp_SEQ_property3)
+ − 1539 apply(subst basic_rsimp_SEQ_property2)
+ − 1540 apply simp+
+ − 1541 apply(subgoal_tac "rnullable (rsimp r1)")
+ − 1542 apply simp
+ − 1543 using rsimp_idem apply presburger
482
+ − 1544 using der_simp_nullability by presburger
+ − 1545
456
+ − 1546
482
+ − 1547
+ − 1548 lemma grewrite_ralts:
492
+ − 1549 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
482
+ − 1550 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
+ − 1551
+ − 1552 lemma grewrites_ralts:
492
+ − 1553 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
488
+ − 1554 apply(induct rule: grewrites.induct)
482
+ − 1555 apply simp
+ − 1556 using grewrite_ralts hreal_trans by blast
488
+ − 1557
+ − 1558
+ − 1559 lemma distinct_grewrites_subgoal1:
+ − 1560 shows "
492
+ − 1561 \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"
+ − 1562 apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")
488
+ − 1563 apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+ − 1564 apply(subgoal_tac "rs1 \<leadsto>g* rs3")
+ − 1565 using grewrites_ralts apply blast
+ − 1566 using grewrites.intros(2) by presburger
+ − 1567
+ − 1568
+ − 1569
+ − 1570
482
+ − 1571
+ − 1572
+ − 1573 lemma grewrites_ralts_rsimpalts:
492
+ − 1574 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "
482
+ − 1575 apply(induct rs rs' rule: grewrites.induct)
+ − 1576 apply(case_tac rs)
+ − 1577 using hrewrite.intros(9) apply force
+ − 1578 apply(case_tac list)
+ − 1579 apply simp
+ − 1580 using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger
+ − 1581 apply simp
+ − 1582 apply(case_tac rs2)
+ − 1583 apply simp
+ − 1584 apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))
+ − 1585 apply(case_tac list)
+ − 1586 apply(simp)
+ − 1587 using distinct_grewrites_subgoal1 apply blast
+ − 1588 apply simp
+ − 1589 apply(case_tac rs3)
+ − 1590 apply simp
+ − 1591 using grewrites_ralts hrewrite.intros(9) apply blast
+ − 1592 by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+ − 1593
484
+ − 1594 lemma hrewrites_alts:
492
+ − 1595 shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS (rs1 @ [r'] @ rs2))"
484
+ − 1596 apply(induct r r' rule: hrewrites.induct)
+ − 1597 apply simp
+ − 1598 using hrewrite.intros(6) by blast
+ − 1599
+ − 1600 inductive
+ − 1601 srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
+ − 1602 where
+ − 1603 ss1: "[] scf\<leadsto>* []"
492
+ − 1604 | ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
484
+ − 1605
+ − 1606
+ − 1607 lemma hrewrites_alts_cons:
492
+ − 1608 shows " RALTS rs h\<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) h\<leadsto>* RALTS (r # rs')"
484
+ − 1609
+ − 1610
+ − 1611 oops
+ − 1612
+ − 1613
492
+ − 1614 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"
484
+ − 1615
+ − 1616 apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
+ − 1617 apply(rule rs1)
+ − 1618 apply(drule_tac x = "rsa@[r']" in meta_spec)
+ − 1619 apply simp
+ − 1620 apply(rule hreal_trans)
+ − 1621 prefer 2
+ − 1622 apply(assumption)
+ − 1623 apply(drule hrewrites_alts)
+ − 1624 by auto
+ − 1625
+ − 1626
+ − 1627 corollary srewritescf_alt1:
+ − 1628 assumes "rs1 scf\<leadsto>* rs2"
492
+ − 1629 shows "RALTS rs1 h\<leadsto>* RALTS rs2"
484
+ − 1630 using assms
+ − 1631 by (metis append_Nil srewritescf_alt)
+ − 1632
+ − 1633
+ − 1634
+ − 1635
+ − 1636 lemma trivialrsimp_srewrites:
492
+ − 1637 "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
484
+ − 1638
+ − 1639 apply(induction rs)
+ − 1640 apply simp
+ − 1641 apply(rule ss1)
+ − 1642 by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
+ − 1643
+ − 1644 lemma hrewrites_list:
+ − 1645 shows
492
+ − 1646 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"
484
+ − 1647 apply(induct x)
+ − 1648 apply(simp)+
+ − 1649 by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
492
+ − 1650 (* apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)
484
+ − 1651
+ − 1652
489
+ − 1653 lemma hrewrite_simpeq:
492
+ − 1654 shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
489
+ − 1655 apply(induct rule: hrewrite.induct)
+ − 1656 apply simp+
+ − 1657 apply (simp add: basic_rsimp_SEQ_property3)
+ − 1658 apply (simp add: basic_rsimp_SEQ_property1)
+ − 1659 using rsimp.simps(1) apply presburger
+ − 1660 apply simp+
+ − 1661 using flts_middle0 apply force
+ − 1662
+ − 1663
+ − 1664 using simp_flatten3 apply presburger
+ − 1665
+ − 1666 apply simp+
+ − 1667 apply (simp add: idem_after_simp1)
+ − 1668 using grewrite.intros(4) grewrite_equal_rsimp by presburger
+ − 1669
+ − 1670 lemma hrewrites_simpeq:
492
+ − 1671 shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
489
+ − 1672 apply(induct rule: hrewrites.induct)
+ − 1673 apply simp
+ − 1674 apply(subgoal_tac "rsimp r2 = rsimp r3")
+ − 1675 apply auto[1]
+ − 1676 using hrewrite_simpeq by presburger
+ − 1677
482
+ − 1678
+ − 1679
+ − 1680 lemma simp_hrewrites:
492
+ − 1681 shows "r1 h\<leadsto>* rsimp r1"
482
+ − 1682 apply(induct r1)
+ − 1683 apply simp+
+ − 1684 apply(case_tac "rsimp r11 = RONE")
+ − 1685 apply simp
+ − 1686 apply(subst basic_rsimp_SEQ_property1)
492
+ − 1687 apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")
482
+ − 1688 using hreal_trans hrewrite.intros(3) apply blast
+ − 1689 using hrewrites_seq_context apply presburger
+ − 1690 apply(case_tac "rsimp r11 = RZERO")
+ − 1691 apply simp
+ − 1692 using hrewrite.intros(1) hrewrites_seq_context apply blast
+ − 1693 apply(case_tac "rsimp r12 = RZERO")
+ − 1694 apply simp
+ − 1695 apply(subst basic_rsimp_SEQ_property3)
+ − 1696 apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)
+ − 1697 apply(subst basic_rsimp_SEQ_property2)
+ − 1698 apply simp+
+ − 1699 using hrewrites_seq_contexts apply presburger
+ − 1700 apply simp
492
+ − 1701 apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")
+ − 1702 apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
482
+ − 1703 using hreal_trans apply blast
+ − 1704 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
484
+ − 1705
+ − 1706 apply (simp add: grewrites_ralts hrewrites_list)
+ − 1707 by simp
+ − 1708
+ − 1709 lemma interleave_aux1:
492
+ − 1710 shows " RALT (RSEQ RZERO r1) r h\<leadsto>* r"
+ − 1711 apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")
+ − 1712 apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")
485
+ − 1713 apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
+ − 1714 using rs1 srewritescf_alt1 ss1 ss2 apply presburger
484
+ − 1715 by (simp add: hr_in_rstar hrewrite.intros(1))
+ − 1716
485
+ − 1717
+ − 1718
484
+ − 1719 lemma rnullable_hrewrite:
492
+ − 1720 shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
488
+ − 1721 apply(induct rule: hrewrite.induct)
+ − 1722 apply simp+
+ − 1723 apply blast
+ − 1724 apply simp+
+ − 1725 done
465
+ − 1726
453
+ − 1727
484
+ − 1728 lemma interleave1:
492
+ − 1729 shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
484
+ − 1730 apply(induct r r' rule: hrewrite.induct)
+ − 1731 apply (simp add: hr_in_rstar hrewrite.intros(1))
+ − 1732 apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
+ − 1733 apply simp
+ − 1734 apply(subst interleave_aux1)
+ − 1735 apply simp
+ − 1736 apply(case_tac "rnullable r1")
488
+ − 1737 apply simp
+ − 1738
+ − 1739 apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2)
+ − 1740
+ − 1741 apply (simp add: hrewrites_seq_context rnullable_hrewrite)
+ − 1742 apply(case_tac "rnullable r1")
+ − 1743 apply simp
+ − 1744
+ − 1745 using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger
+ − 1746 apply simp
+ − 1747 using hr_in_rstar hrewrites_seq_context2 apply blast
+ − 1748 apply simp
484
+ − 1749
488
+ − 1750 using hrewrites_alts apply auto[1]
+ − 1751 apply simp
+ − 1752 using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1]
+ − 1753 apply simp
+ − 1754 apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts)
+ − 1755 apply (simp add: hr_in_rstar hrewrite.intros(9))
+ − 1756 apply (simp add: hr_in_rstar hrewrite.intros(10))
+ − 1757 apply simp
+ − 1758 using hrewrite.intros(11) by auto
+ − 1759
+ − 1760 lemma interleave_star1:
492
+ − 1761 shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
488
+ − 1762 apply(induct rule : hrewrites.induct)
+ − 1763 apply simp
+ − 1764 by (meson hreal_trans interleave1)
+ − 1765
484
+ − 1766
+ − 1767
480
+ − 1768 lemma inside_simp_removal:
+ − 1769 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
+ − 1770 apply(induct r)
+ − 1771 apply simp+
+ − 1772 apply(case_tac "rnullable r1")
+ − 1773 apply simp
456
+ − 1774
480
+ − 1775 using inside_simp_seq_nullable apply blast
482
+ − 1776 apply simp
+ − 1777 apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
492
+ − 1778 apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
488
+ − 1779 using hrewrites_simpeq apply presburger
+ − 1780 using interleave_star1 simp_hrewrites apply presburger
+ − 1781 by simp
482
+ − 1782
451
+ − 1783
+ − 1784
482
+ − 1785
480
+ − 1786 lemma rders_simp_same_simpders:
+ − 1787 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+ − 1788 apply(induct s rule: rev_induct)
453
+ − 1789 apply simp
480
+ − 1790 apply(case_tac "xs = []")
453
+ − 1791 apply simp
480
+ − 1792 apply(simp add: rders_append rders_simp_append)
+ − 1793 using inside_simp_removal by blast
453
+ − 1794
480
+ − 1795
453
+ − 1796
+ − 1797
451
+ − 1798 lemma distinct_der:
480
+ − 1799 shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) =
+ − 1800 rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+ − 1801 by (metis grewrites_simpalts gstar_rdistinct inside_simp_removal rder_rsimp_ALTs_commute)
+ − 1802
451
+ − 1803
453
+ − 1804
+ − 1805
+ − 1806
+ − 1807 lemma rders_simp_lambda:
+ − 1808 shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"
+ − 1809 using rders_simp_append by auto
451
+ − 1810
453
+ − 1811 lemma rders_simp_nonempty_simped:
+ − 1812 shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"
+ − 1813 using rders_simp_same_simpders rsimp_idem by auto
+ − 1814
+ − 1815 lemma repeated_altssimp:
+ − 1816 shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
+ − 1817 rsimp_ALTs (rdistinct (rflts rs) {})"
+ − 1818 by (metis map_idI rsimp.simps(2) rsimp_idem)
451
+ − 1819
465
+ − 1820
+ − 1821 lemma add0_isomorphic:
+ − 1822 shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
484
+ − 1823 by (metis append.left_neutral append_Cons flts_removes0 idem_after_simp1)
465
+ − 1824
+ − 1825
484
+ − 1826
465
+ − 1827
444
+ − 1828 lemma alts_closed_form: shows
+ − 1829 "rsimp (rders_simp (RALTS rs) s) =
+ − 1830 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
+ − 1831 apply(induct s rule: rev_induct)
+ − 1832 apply simp
+ − 1833 apply simp
+ − 1834 apply(subst rders_simp_append)
+ − 1835 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) =
+ − 1836 rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
+ − 1837 prefer 2
+ − 1838 apply (metis inside_simp_removal rders_simp_one_char)
+ − 1839 apply(simp only: )
451
+ − 1840 apply(subst rders_simp_one_char)
+ − 1841 apply(subst rsimp_idem)
+ − 1842 apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
+ − 1843 rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
+ − 1844 prefer 2
+ − 1845 using rder_rsimp_ALTs_commute apply presburger
+ − 1846 apply(simp only:)
+ − 1847 apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
+ − 1848 = rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+ − 1849 prefer 2
+ − 1850
+ − 1851 using distinct_der apply presburger
+ − 1852 apply(simp only:)
453
+ − 1853 apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
+ − 1854 rsimp (rsimp_ALTs (rdistinct ( (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)))) {}))")
+ − 1855 apply(simp only:)
+ − 1856 apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
+ − 1857 rsimp (rsimp_ALTs (rdistinct (rflts ( (map (rsimp \<circ> (rder x) \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+ − 1858 apply(simp only:)
+ − 1859 apply(subst rders_simp_lambda)
+ − 1860 apply(subst rders_simp_nonempty_simped)
+ − 1861 apply simp
+ − 1862 apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (xs @ [x])) rs). rsimp r = r")
+ − 1863 prefer 2
+ − 1864 apply (simp add: rders_simp_same_simpders rsimp_idem)
+ − 1865 apply(subst repeated_altssimp)
+ − 1866 apply simp
+ − 1867 apply fastforce
465
+ − 1868 apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
476
+ − 1869 using simp_der_pierce_flts by blast
443
+ − 1870
444
+ − 1871 lemma alts_closed_form_variant: shows
+ − 1872 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s =
+ − 1873 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
478
+ − 1874 by (metis alts_closed_form comp_apply rders_simp_nonempty_simped)
443
+ − 1875
482
+ − 1876 thm vsuf.simps
443
+ − 1877
+ − 1878
482
+ − 1879
+ − 1880 lemma rsimp_seq_equal1:
+ − 1881 shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})"
+ − 1882 by (metis idem_after_simp1 rsimp.simps(1))
+ − 1883
+ − 1884
+ − 1885
483
+ − 1886
+ − 1887
485
+ − 1888 fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where
+ − 1889 "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs"
+ − 1890 | "sflat_aux (RALTS []) = []"
+ − 1891 | "sflat_aux r = [r]"
+ − 1892
+ − 1893
+ − 1894 fun sflat :: "rrexp \<Rightarrow> rrexp" where
+ − 1895 "sflat (RALTS (r # [])) = r"
+ − 1896 | "sflat (RALTS (r # rs)) = RALTS (sflat_aux r @ rs)"
+ − 1897 | "sflat r = r"
+ − 1898
+ − 1899 inductive created_by_seq:: "rrexp \<Rightarrow> bool" where
+ − 1900 "created_by_seq (RSEQ r1 r2) "
+ − 1901 | "created_by_seq r1 \<Longrightarrow> created_by_seq (RALT r1 r2)"
+ − 1902
+ − 1903 (*Why \<and> rnullable case would be provable.....?*)
+ − 1904 lemma seq_der_shape:
+ − 1905 shows "\<forall>r1 r2. \<exists>r3 r4. (rder c (RSEQ r1 r2) = RSEQ r3 r4 \<or> rder c (RSEQ r1 r2) = RALT r3 r4)"
+ − 1906 by (meson rder.simps(5))
+ − 1907
+ − 1908 lemma alt_der_shape:
+ − 1909 shows "\<forall>rs. \<exists> rs'. (rder c (RALTS rs)) = RALTS (map (rder c) rs)"
+ − 1910 by force
+ − 1911
+ − 1912 lemma seq_ders_shape1:
+ − 1913 shows "\<forall>r1 r2. \<exists>r3 r4. (rders (RSEQ r1 r2) s) = RSEQ r3 r4 \<or> (rders (RSEQ r1 r2) s) = RALT r3 r4"
+ − 1914 apply(induct s rule: rev_induct)
+ − 1915 apply auto[1]
+ − 1916 apply(rule allI)+
+ − 1917 apply(subst rders_append)+
+ − 1918 apply(subgoal_tac " \<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or> rders (RSEQ r1 r2) xs = RALT r3 r4 ")
+ − 1919 apply(erule exE)+
+ − 1920 apply(erule disjE)
+ − 1921 apply simp+
+ − 1922 done
+ − 1923
+ − 1924
+ − 1925 lemma seq_ders_shape2:
+ − 1926 shows "rders (RSEQ r1 r2) s = RALTS (ra # rb # rs) \<Longrightarrow> rs = []"
+ − 1927 using seq_ders_shape1
+ − 1928 by (metis list.inject rrexp.distinct(25) rrexp.inject(3))
+ − 1929
+ − 1930 lemma created_by_seq_der:
+ − 1931 shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)"
+ − 1932 apply(induct r)
+ − 1933 apply simp+
+ − 1934
+ − 1935 using created_by_seq.cases apply blast
+ − 1936
+ − 1937 apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21))
+ − 1938 apply (metis created_by_seq.simps rder.simps(5))
+ − 1939 apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3))
+ − 1940 using created_by_seq.intros(1) by force
+ − 1941
+ − 1942 lemma createdbyseq_left_creatable:
+ − 1943 shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1"
+ − 1944 using created_by_seq.cases by blast
+ − 1945
+ − 1946
+ − 1947
+ − 1948 lemma recursively_derseq:
+ − 1949 shows " created_by_seq (rders (RSEQ r1 r2) s)"
+ − 1950 apply(induct s rule: rev_induct)
+ − 1951 apply simp
+ − 1952 using created_by_seq.intros(1) apply force
+ − 1953 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) (xs @ [x]))")
+ − 1954 apply blast
+ − 1955 apply(subst rders_append)
+ − 1956 apply(subgoal_tac "\<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or>
+ − 1957 rders (RSEQ r1 r2) xs = RALT r3 r4")
+ − 1958 prefer 2
+ − 1959 using seq_ders_shape1 apply presburger
+ − 1960 apply(erule exE)+
+ − 1961 apply(erule disjE)
+ − 1962 apply(subgoal_tac "created_by_seq (rders (RSEQ r3 r4) [x])")
+ − 1963 apply presburger
+ − 1964 apply simp
+ − 1965 using created_by_seq.intros(1) created_by_seq.intros(2) apply presburger
+ − 1966 apply simp
+ − 1967 apply(subgoal_tac "created_by_seq r3")
+ − 1968 prefer 2
+ − 1969 using createdbyseq_left_creatable apply blast
+ − 1970 using created_by_seq.intros(2) created_by_seq_der by blast
482
+ − 1971
485
+ − 1972
+ − 1973 lemma recursively_derseq1:
+ − 1974 shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> created_by_seq r"
+ − 1975 using recursively_derseq by blast
+ − 1976
+ − 1977 lemma recursively_derseq2:
+ − 1978 shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) "
+ − 1979 by (meson created_by_seq.cases recursively_derseq)
+ − 1980
+ − 1981 lemma recursively_derseq3:
+ − 1982 shows "created_by_seq r \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) "
+ − 1983 by (meson created_by_seq.cases recursively_derseq)
+ − 1984
+ − 1985 lemma createdbyseq_prop1:
+ − 1986 shows "created_by_seq (RALTS xs) \<Longrightarrow> \<exists> ra rb. xs = [ra, rb]"
+ − 1987 by (metis created_by_seq.cases rrexp.inject(3) rrexp.simps(30))
+ − 1988
+ − 1989
+ − 1990 lemma sfau_head:
+ − 1991 shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs"
+ − 1992 apply(induction r rule: created_by_seq.induct)
+ − 1993 apply simp
+ − 1994 by fastforce
+ − 1995
+ − 1996
+ − 1997
+ − 1998
+ − 1999 lemma sfaux_eq10:
+ − 2000 shows "created_by_seq r3 \<Longrightarrow>
+ − 2001 rs \<noteq> [] \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) =
+ − 2002 RALTS (sflat_aux (rder c r3) @ (map (rder c ) rs) )"
+ − 2003 apply(induction r3 arbitrary: rs rule: created_by_seq.induct)
+ − 2004 apply simp
+ − 2005 apply(case_tac "rnullable r1")
+ − 2006 apply simp
+ − 2007
+ − 2008 apply (metis append_Cons list.exhaust map_is_Nil_conv self_append_conv2 sflat.simps(2) sflat_aux.simps(1) sflat_aux.simps(6))
+ − 2009 apply simp
+ − 2010
+ − 2011 apply (metis Nil_is_map_conv append_Cons append_Nil list.exhaust sflat.simps(2) sflat_aux.simps(6))
+ − 2012 apply simp
+ − 2013 by force
484
+ − 2014
485
+ − 2015 lemma sfaux_keeps_tail:
+ − 2016 shows "created_by_seq r3 \<Longrightarrow>
+ − 2017 sflat_aux (RALTS (map (rder c) (sflat_aux r3) @ xs )) =
+ − 2018 sflat_aux (RALTS (map (rder c) (sflat_aux r3))) @ xs "
+ − 2019 using sfau_head by fastforce
+ − 2020
+ − 2021
+ − 2022
484
+ − 2023
485
+ − 2024 lemma sfaux_eq00:
+ − 2025 shows "created_by_seq r3 \<Longrightarrow>
+ − 2026 sflat_aux (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) =
+ − 2027 (sflat_aux (rder c r3) @ (map (rder c ) rs) )"
+ − 2028 apply(induct rs rule: rev_induct)
+ − 2029 apply simp
+ − 2030 apply (smt (verit, del_insts) append_Cons created_by_seq.simps list.distinct(1) list.simps(9) map_append rder.simps(4) rrexp.inject(3) self_append_conv self_append_conv2 sfau_head sfaux_eq10 sflat_aux.simps(1) sflat_aux.simps(6))
+ − 2031 apply simp
+ − 2032 apply(subst sfaux_keeps_tail)
+ − 2033 apply simp
+ − 2034 apply(subst (asm) sfaux_keeps_tail)
+ − 2035 apply simp+
+ − 2036 done
+ − 2037
+ − 2038
+ − 2039 lemma sfaux_eq1:
+ − 2040 shows "created_by_seq r3 \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ [rder c r4])) = RALTS (sflat_aux (rder c r3) @ [rder c r4] )"
+ − 2041 by (metis (no_types, lifting) list.distinct(1) list.simps(9) map_append map_concat_cons self_append_conv sfaux_eq10)
+ − 2042
+ − 2043 lemma sflat_seq_induct:
+ − 2044 shows "sflat (rder c (sflat (rders (RSEQ r1 r2) s) )) = sflat (rders (RSEQ r1 r2) (s @ [c]))"
+ − 2045 apply(subst rders_append)
+ − 2046 apply(case_tac "rders (RSEQ r1 r2) s ")
+ − 2047 prefer 6
+ − 2048 apply simp+
+ − 2049 apply(subgoal_tac "\<exists>r3 r4. x5 = [r3, r4]")
+ − 2050 apply(erule exE)+
+ − 2051 apply(subgoal_tac "sflat (rder c (sflat (RALT r3 r4))) = sflat (RALTS (map (rder c) [r3, r4]))")
+ − 2052 apply meson
+ − 2053 apply simp
+ − 2054
+ − 2055 apply (metis createdbyseq_left_creatable recursively_derseq sfaux_eq1)
+ − 2056 by (metis created_by_seq.simps recursively_derseq rrexp.distinct(25) rrexp.inject(3))
484
+ − 2057
+ − 2058
483
+ − 2059
482
+ − 2060
+ − 2061
485
+ − 2062 lemma vsuf_prop1:
+ − 2063 shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs))
+ − 2064 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
+ − 2065 else (map (\<lambda>s. s @ [x]) (vsuf xs r)) )
+ − 2066 "
+ − 2067 apply(induct xs arbitrary: r)
+ − 2068 apply simp
+ − 2069 apply(case_tac "rnullable r")
+ − 2070 apply simp
+ − 2071 apply simp
+ − 2072 done
483
+ − 2073
485
+ − 2074 fun breakHead :: "rrexp list \<Rightarrow> rrexp list" where
+ − 2075 "breakHead [] = [] "
+ − 2076 | "breakHead (RALT r1 r2 # rs) = r1 # r2 # rs"
+ − 2077 | "breakHead (r # rs) = r # rs"
+ − 2078
+ − 2079
+ − 2080 lemma sfau_idem_der:
+ − 2081 shows "created_by_seq r \<Longrightarrow> sflat_aux (rder c r) = breakHead (map (rder c) (sflat_aux r))"
+ − 2082 apply(induct rule: created_by_seq.induct)
+ − 2083 apply simp+
+ − 2084 using sfau_head by fastforce
483
+ − 2085
485
+ − 2086 lemma vsuf_compose1:
+ − 2087 shows " \<not> rnullable (rders r1 xs)
+ − 2088 \<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)"
+ − 2089 apply(subst vsuf_prop1)
+ − 2090 apply simp
+ − 2091 by (simp add: rders_append)
483
+ − 2092
485
+ − 2093
+ − 2094
483
+ − 2095
485
+ − 2096 lemma seq_sfau0:
+ − 2097 shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) #
+ − 2098 (map (rders r2) (vsuf s r1)) "
+ − 2099 apply(induct s rule: rev_induct)
483
+ − 2100 apply simp
485
+ − 2101 apply(subst rders_append)+
+ − 2102 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)")
+ − 2103 prefer 2
+ − 2104 using recursively_derseq1 apply blast
+ − 2105 apply simp
+ − 2106 apply(subst sfau_idem_der)
+ − 2107
+ − 2108 apply blast
+ − 2109 apply(case_tac "rnullable (rders r1 xs)")
483
+ − 2110 apply simp
485
+ − 2111 apply(subst vsuf_prop1)
483
+ − 2112 apply simp
485
+ − 2113 apply (simp add: rders_append)
+ − 2114 apply simp
+ − 2115 using vsuf_compose1 by blast
+ − 2116
+ − 2117
+ − 2118
+ − 2119
+ − 2120
+ − 2121
+ − 2122
+ − 2123
483
+ − 2124
+ − 2125 thm sflat.elims
+ − 2126
+ − 2127
+ − 2128
482
+ − 2129
+ − 2130
+ − 2131 lemma sflat_rsimpeq:
486
+ − 2132 shows "created_by_seq r1 \<Longrightarrow> sflat_aux r1 = rs \<Longrightarrow> rsimp r1 = rsimp (RALTS rs)"
+ − 2133 apply(induct r1 arbitrary: rs rule: created_by_seq.induct)
+ − 2134 apply simp
+ − 2135 using rsimp_seq_equal1 apply force
+ − 2136 by (metis head_one_more_simp rsimp.simps(2) sflat_aux.simps(1) simp_flatten)
482
+ − 2137
+ − 2138
+ − 2139
+ − 2140 lemma seq_closed_form_general:
+ − 2141 shows "rsimp (rders (RSEQ r1 r2) s) =
+ − 2142 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
485
+ − 2143 apply(case_tac "s \<noteq> []")
486
+ − 2144 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) s)")
+ − 2145 apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))")
482
+ − 2146 using sflat_rsimpeq apply blast
486
+ − 2147 apply (simp add: seq_sfau0)
+ − 2148 using recursively_derseq1 apply blast
485
+ − 2149 apply simp
+ − 2150 by (metis idem_after_simp1 rsimp.simps(1))
482
+ − 2151
485
+ − 2152
486
+ − 2153
482
+ − 2154 lemma seq_closed_form_aux1:
+ − 2155 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) =
+ − 2156 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
+ − 2157 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem)
+ − 2158
+ − 2159 lemma add_simp_to_rest:
+ − 2160 shows "rsimp (RALTS (r # rs)) = rsimp (RALTS (r # map rsimp rs))"
+ − 2161 by (metis append_Nil2 grewrite.intros(2) grewrite_simpalts head_one_more_simp list.simps(9) rsimp_ALTs.simps(2) spawn_simp_rsimpalts)
+ − 2162
+ − 2163 lemma rsimp_compose_der:
+ − 2164 shows "map rsimp (map (rders r) ss) = map (\<lambda>s. rsimp (rders r s)) ss"
+ − 2165 apply simp
+ − 2166 done
+ − 2167
+ − 2168 lemma rsimp_compose_der2:
+ − 2169 shows "\<forall>s \<in> set ss. s \<noteq> [] \<Longrightarrow> map rsimp (map (rders r) ss) = map (\<lambda>s. (rders_simp r s)) ss"
+ − 2170 by (simp add: rders_simp_same_simpders)
+ − 2171
+ − 2172 lemma vsuf_nonempty:
+ − 2173 shows "\<forall>s \<in> set ( vsuf s1 r). s \<noteq> []"
+ − 2174 apply(induct s1 arbitrary: r)
+ − 2175 apply simp
+ − 2176 apply simp
+ − 2177 done
+ − 2178
+ − 2179 lemma rsimp_compose_der3:
+ − 2180 shows " map rsimp (map (rders r) (vsuf s1 r')) = map (\<lambda>s. rsimp (rders_simp r s)) (vsuf s1 r')"
+ − 2181 by (simp add: rders_simp_same_simpders rsimp_idem vsuf_nonempty)
+ − 2182
+ − 2183 thm rders_simp_same_simpders
+ − 2184
+ − 2185
+ − 2186
+ − 2187 lemma seq_closed_form_aux2:
+ − 2188 shows "s \<noteq> [] \<Longrightarrow> rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1)))))) =
+ − 2189 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))))"
+ − 2190
+ − 2191 by (metis add_simp_to_rest rsimp_compose_der2 vsuf_nonempty)
+ − 2192
+ − 2193
443
+ − 2194 lemma seq_closed_form: shows
+ − 2195 "rsimp (rders_simp (RSEQ r1 r2) s) =
+ − 2196 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) #
445
+ − 2197 (map (rders_simp r2) (vsuf s r1))
443
+ − 2198 )
+ − 2199 )"
482
+ − 2200 apply(case_tac s )
+ − 2201 apply simp
+ − 2202 apply (metis idem_after_simp1 rsimp.simps(1))
+ − 2203 apply(subgoal_tac " s \<noteq> []")
+ − 2204 using rders_simp_same_simpders rsimp_idem seq_closed_form_aux1 seq_closed_form_aux2 seq_closed_form_general apply presburger
+ − 2205 by fastforce
+ − 2206
+ − 2207
+ − 2208
443
+ − 2209
+ − 2210
444
+ − 2211 lemma seq_closed_form_variant: shows
+ − 2212 "s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) =
+ − 2213 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
445
+ − 2214 apply(induct s rule: rev_induct)
+ − 2215 apply simp
+ − 2216 apply(subst rders_simp_append)
+ − 2217 apply(subst rders_simp_one_char)
+ − 2218 apply(subst rsimp_idem[symmetric])
+ − 2219 apply(subst rders_simp_one_char[symmetric])
+ − 2220 apply(subst rders_simp_append[symmetric])
+ − 2221 apply(insert seq_closed_form)
+ − 2222 apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
+ − 2223 = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
+ − 2224 apply force
+ − 2225 by presburger
443
+ − 2226
486
+ − 2227
+ − 2228 lemma star_closed_form_seq1:
+ − 2229 shows "sflat_aux (rders (RSTAR r0) (c # s)) =
+ − 2230 RSEQ (rders (rder c r0) s) (RSTAR r0) #
+ − 2231 map (rders (RSTAR r0)) (vsuf s (rder c r0))"
+ − 2232 apply simp
+ − 2233 using seq_sfau0 by blast
+ − 2234
+ − 2235 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where
+ − 2236 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2"
+ − 2237 | "hflat_aux r = [r]"
+ − 2238
+ − 2239
+ − 2240 fun hflat :: "rrexp \<Rightarrow> rrexp" where
+ − 2241 "hflat (RALT r1 r2) = RALTS ((hflat_aux r1) @ (hflat_aux r2))"
+ − 2242 | "hflat r = r"
+ − 2243
+ − 2244 inductive created_by_star :: "rrexp \<Rightarrow> bool" where
+ − 2245 "created_by_star (RSEQ ra (RSTAR rb))"
+ − 2246 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)"
+ − 2247
+ − 2248 fun hElem :: "rrexp \<Rightarrow> rrexp list" where
+ − 2249 "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)"
+ − 2250 | "hElem r = [r]"
+ − 2251
+ − 2252
+ − 2253
+ − 2254
+ − 2255 lemma cbs_ders_cbs:
+ − 2256 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)"
+ − 2257 apply(induct r rule: created_by_star.induct)
+ − 2258 apply simp
+ − 2259 using created_by_star.intros(1) created_by_star.intros(2) apply auto[1]
+ − 2260 by (metis (mono_tags, lifting) created_by_star.simps list.simps(8) list.simps(9) rder.simps(4))
+ − 2261
+ − 2262 lemma star_ders_cbs:
+ − 2263 shows "created_by_star (rders (RSEQ r1 (RSTAR r2)) s)"
+ − 2264 apply(induct s rule: rev_induct)
+ − 2265 apply simp
+ − 2266 apply (simp add: created_by_star.intros(1))
+ − 2267 apply(subst rders_append)
+ − 2268 apply simp
+ − 2269 using cbs_ders_cbs by auto
+ − 2270
+ − 2271 lemma created_by_star_cases:
+ − 2272 shows "created_by_star r \<Longrightarrow> \<exists>ra rb. (r = RALT ra rb \<and> created_by_star ra \<and> created_by_star rb) \<or> r = RSEQ ra rb "
+ − 2273 by (meson created_by_star.cases)
+ − 2274
+ − 2275
+ − 2276
+ − 2277 lemma hfau_pushin:
+ − 2278 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))"
+ − 2279 apply(induct r rule: created_by_star.induct)
+ − 2280 apply simp
+ − 2281 apply(subgoal_tac "created_by_star (rder c r1)")
+ − 2282 prefer 2
+ − 2283 apply(subgoal_tac "created_by_star (rder c r2)")
+ − 2284 using cbs_ders_cbs apply blast
+ − 2285 using cbs_ders_cbs apply auto[1]
+ − 2286 apply simp
+ − 2287 done
+ − 2288
+ − 2289 lemma stupdate_induct1:
+ − 2290 shows " concat (map (hElem \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
+ − 2291 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"
+ − 2292 apply(induct Ss)
+ − 2293 apply simp+
+ − 2294 by (simp add: rders_append)
+ − 2295
+ − 2296
+ − 2297
+ − 2298 lemma stupdates_join_general:
+ − 2299 shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) =
+ − 2300 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)"
+ − 2301 apply(induct xs arbitrary: Ss)
+ − 2302 apply (simp)
+ − 2303 prefer 2
+ − 2304 apply auto[1]
+ − 2305 using stupdate_induct1 by blast
+ − 2306
+ − 2307
+ − 2308
+ − 2309
+ − 2310 lemma stupdates_join:
+ − 2311 shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) =
+ − 2312 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 [[c]])"
+ − 2313 using stupdates_join_general by auto
+ − 2314
+ − 2315
+ − 2316
+ − 2317 lemma star_hfau_induct:
+ − 2318 shows "hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) s) =
+ − 2319 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])"
+ − 2320 apply(induct s rule: rev_induct)
+ − 2321 apply simp
+ − 2322 apply(subst rders_append)+
+ − 2323 apply simp
+ − 2324 apply(subst stupdates_append)
+ − 2325 apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)")
+ − 2326 prefer 2
+ − 2327 apply (simp add: star_ders_cbs)
+ − 2328 apply(subst hfau_pushin)
+ − 2329 apply simp
+ − 2330 apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) =
+ − 2331 concat (map hElem (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ")
+ − 2332 apply(simp only:)
+ − 2333 prefer 2
+ − 2334 apply presburger
+ − 2335 apply(subst stupdates_append[symmetric])
+ − 2336 using stupdates_join_general by blast
+ − 2337
487
+ − 2338 lemma starders_hfau_also1:
+ − 2339 shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])"
+ − 2340 using star_hfau_induct by force
+ − 2341
+ − 2342 lemma hflat_aux_grewrites:
+ − 2343 shows "a # rs \<leadsto>g* hflat_aux a @ rs"
+ − 2344 apply(induct a arbitrary: rs)
+ − 2345 apply simp+
+ − 2346 apply(case_tac x)
+ − 2347 apply simp
+ − 2348 apply(case_tac list)
+ − 2349
+ − 2350 apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq)
+ − 2351 apply(case_tac lista)
+ − 2352 apply simp
+ − 2353 apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv)
+ − 2354 apply simp
+ − 2355 by simp
+ − 2356
+ − 2357
+ − 2358
+ − 2359
+ − 2360 lemma cbs_hfau_rsimpeq1:
+ − 2361 shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))"
+ − 2362 apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b")
+ − 2363 using grewrites_equal_rsimp apply presburger
488
+ − 2364 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites)
487
+ − 2365
+ − 2366
+ − 2367 lemma hfau_rsimpeq2:
+ − 2368 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
+ − 2369 apply(induct r)
+ − 2370 apply simp+
+ − 2371
+ − 2372 apply (metis rsimp_seq_equal1)
+ − 2373 prefer 2
486
+ − 2374 apply simp
487
+ − 2375 apply(case_tac x)
+ − 2376 apply simp
+ − 2377 apply(case_tac "list")
486
+ − 2378 apply simp
+ − 2379
487
+ − 2380 apply (metis idem_after_simp1)
+ − 2381 apply(case_tac "lista")
+ − 2382 prefer 2
+ − 2383 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))
+ − 2384 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")
+ − 2385 apply simp
+ − 2386 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")
+ − 2387 using hflat_aux.simps(1) apply presburger
+ − 2388 apply simp
+ − 2389 using cbs_hfau_rsimpeq1 by fastforce
+ − 2390
+ − 2391
+ − 2392 lemma hfau_rsimpeq1:
+ − 2393 shows "created_by_star r \<Longrightarrow> hflat_aux r = rs \<Longrightarrow> rsimp r = rsimp (RALTS rs)"
+ − 2394 apply(induct r arbitrary: rs rule: created_by_star.induct )
+ − 2395 apply (metis created_by_seq.intros(1) hflat_aux.simps(5) sflat_aux.simps(6) sflat_rsimpeq)
+ − 2396 apply simp
+ − 2397 oops
+ − 2398
+ − 2399
+ − 2400
+ − 2401
486
+ − 2402
+ − 2403
+ − 2404 lemma star_closed_form1:
487
+ − 2405 shows "rsimp (rders (RSTAR r0) (c#s)) =
+ − 2406 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 2407 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger
+ − 2408
+ − 2409 lemma star_closed_form2:
+ − 2410 shows "rsimp (rders_simp (RSTAR r0) (c#s)) =
+ − 2411 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 2412 by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem star_closed_form1)
+ − 2413
+ − 2414 lemma star_closed_form3:
+ − 2415 shows "rsimp (rders_simp (RSTAR r0) (c#s)) = (rders_simp (RSTAR r0) (c#s))"
+ − 2416 by (metis list.distinct(1) rders_simp_same_simpders star_closed_form1 star_closed_form2)
+ − 2417
+ − 2418 lemma star_closed_form4:
+ − 2419 shows " (rders_simp (RSTAR r0) (c#s)) =
+ − 2420 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 2421 using star_closed_form2 star_closed_form3 by presburger
+ − 2422
+ − 2423 lemma star_closed_form5:
+ − 2424 shows " rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) Ss )))) =
+ − 2425 rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ))))"
+ − 2426 by (metis (mono_tags, lifting) list.map_comp map_eq_conv o_apply rsimp.simps(2) rsimp_idem)
+ − 2427
+ − 2428 lemma star_closed_form6_hrewrites:
+ − 2429 shows "
+ − 2430 (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss )
+ − 2431 scf\<leadsto>*
+ − 2432 (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )"
+ − 2433 apply(induct Ss)
+ − 2434 apply simp
+ − 2435 apply (simp add: ss1)
+ − 2436 by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2)
+ − 2437
+ − 2438 lemma star_closed_form6:
+ − 2439 shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )))) =
+ − 2440 rsimp ( ( RALTS ( (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ))))"
+ − 2441 apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\<leadsto>*
+ − 2442 map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ")
+ − 2443 using hrewrites_simpeq srewritescf_alt1 apply fastforce
+ − 2444 using star_closed_form6_hrewrites by blast
+ − 2445
+ − 2446 lemma star_closed_form7:
+ − 2447 shows " (rders_simp (RSTAR r0) (c#s)) =
+ − 2448 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 2449 using star_closed_form4 star_closed_form5 star_closed_form6 by presburger
+ − 2450
+ − 2451 lemma derssimp_nonempty_list:
+ − 2452 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow>
+ − 2453 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) Ss)))) =
+ − 2454 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) Ss)))) "
486
+ − 2455
487
+ − 2456 by (metis (no_types, lifting) map_eq_conv rders_simp_same_simpders)
+ − 2457
+ − 2458 lemma stupdate_nonempty:
+ − 2459 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"
+ − 2460 apply(induct Ss)
+ − 2461 apply simp
+ − 2462 apply(case_tac "rnullable (rders r a)")
+ − 2463 apply simp+
+ − 2464 done
+ − 2465
+ − 2466
+ − 2467 lemma stupdates_nonempty:
+ − 2468 shows "\<forall>s \<in> set Ss. s\<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_updates s r Ss). s \<noteq> []"
+ − 2469 apply(induct s arbitrary: Ss)
+ − 2470 apply simp
+ − 2471 apply simp
+ − 2472 using stupdate_nonempty by presburger
+ − 2473
+ − 2474
+ − 2475
+ − 2476
+ − 2477 lemma star_closed_form8:
+ − 2478 shows
+ − 2479 "rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))) =
+ − 2480 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ ( (rders_simp r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 2481 by (metis derssimp_nonempty_list neq_Nil_conv non_empty_list set_ConsD stupdates_nonempty)
+ − 2482
+ − 2483
486
+ − 2484
+ − 2485 lemma star_closed_form:
+ − 2486 shows "rders_simp (RSTAR r0) (c#s) =
+ − 2487 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
+ − 2488 apply(induct s)
+ − 2489 apply simp
+ − 2490 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
487
+ − 2491 using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
486
+ − 2492
+ − 2493
476
+ − 2494
489
+ − 2495
444
+ − 2496 end