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