505
+ − 1
theory ClosedForms
+ − 2
imports "BasicIdentities"
+ − 3
begin
+ − 4
+ − 5
lemma flts_middle0:
+ − 6
shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+ − 7
apply(induct rsa)
+ − 8
apply simp
+ − 9
by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+ − 10
+ − 11
+ − 12
+ − 13
lemma simp_flatten_aux0:
+ − 14
shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
+ − 15
by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)
+ − 16
+ − 17
+ − 18
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
+ − 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))
+ − 90
+ − 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
+ − 94
+ − 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
*)
+ − 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
+ − 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
+ − 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
+ − 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))"
511
+ − 465
proof -
+ − 466
have "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ − 467
rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) "
+ − 468
by (metis append_Cons append_Nil list.simps(9) map_append simp_flatten_aux0)
+ − 469
apply(simp only:)
+ − 470
+ − 471
oops
+ − 472
+ − 473
lemma simp_flatten3:
+ − 474
shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
505
+ − 475
apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ − 476
rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
+ − 477
prefer 2
+ − 478
apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
+ − 479
apply (simp only:)
+ − 480
apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) =
+ − 481
rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
+ − 482
prefer 2
+ − 483
apply (metis map_append simp_flatten_aux0)
+ − 484
apply(simp only:)
+ − 485
apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
+ − 486
rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
+ − 487
+ − 488
apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
+ − 489
apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
+ − 490
apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
+ − 491
apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
+ − 492
+ − 493
using good_flatten_middle apply presburger
+ − 494
+ − 495
apply (simp add: good1)
+ − 496
apply (simp add: good1)
+ − 497
apply (simp add: good1)
+ − 498
+ − 499
done
+ − 500
+ − 501
+ − 502
+ − 503
+ − 504
+ − 505
lemma grewrite_equal_rsimp:
+ − 506
shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ − 507
apply(frule grewrite_cases_middle)
+ − 508
apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")
+ − 509
using simp_flatten3 apply auto[1]
+ − 510
apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")
+ − 511
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)
+ − 512
by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)
+ − 513
+ − 514
+ − 515
lemma grewrites_equal_rsimp:
+ − 516
shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ − 517
apply (induct rs1 rs2 rule: grewrites.induct)
+ − 518
apply simp
+ − 519
using grewrite_equal_rsimp by presburger
+ − 520
+ − 521
+ − 522
+ − 523
lemma grewrites_last:
+ − 524
shows "r # [RALTS rs] \<leadsto>g* r # rs"
+ − 525
by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
+ − 526
+ − 527
lemma simp_flatten2:
+ − 528
shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
+ − 529
using grewrites_equal_rsimp grewrites_last by blast
+ − 530
+ − 531
+ − 532
lemma frewrites_alt:
+ − 533
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"
+ − 534
by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)
+ − 535
+ − 536
lemma early_late_der_frewrites:
+ − 537
shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"
+ − 538
apply(induct rs)
+ − 539
apply simp
+ − 540
apply(case_tac a)
+ − 541
apply simp+
+ − 542
using frewrite.intros(1) many_steps_later apply blast
+ − 543
apply(case_tac "x = x3")
+ − 544
apply simp
+ − 545
using frewrites_cons apply presburger
+ − 546
using frewrite.intros(1) many_steps_later apply fastforce
+ − 547
apply(case_tac "rnullable x41")
+ − 548
apply simp+
+ − 549
apply (simp add: frewrites_alt)
+ − 550
apply (simp add: frewrites_cons)
+ − 551
apply (simp add: frewrites_append)
+ − 552
by (simp add: frewrites_cons)
+ − 553
+ − 554
+ − 555
lemma gstar0:
+ − 556
shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"
+ − 557
apply(induct rs arbitrary: rsa)
+ − 558
apply simp
+ − 559
apply(case_tac "a = RZERO")
+ − 560
apply simp
+ − 561
+ − 562
using gr_in_rstar grewrite.intros(1) grewrites_append apply presburger
+ − 563
apply(case_tac "a \<in> set rsa")
+ − 564
apply simp+
+ − 565
apply(drule_tac x = "rsa @ [a]" in meta_spec)
+ − 566
by simp
+ − 567
+ − 568
lemma grewrite_rdistinct_aux:
+ − 569
shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
+ − 570
apply(induct rsa arbitrary: rs rset)
+ − 571
apply simp
+ − 572
apply(case_tac " a \<in> rset")
+ − 573
apply simp
+ − 574
apply(case_tac "a \<in> set rs")
+ − 575
apply simp
+ − 576
apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)
+ − 577
apply simp
+ − 578
apply(drule_tac x = "rs @ [a]" in meta_spec)
+ − 579
by (metis Un_insert_left Un_insert_right append.assoc append.right_neutral append_Cons append_Nil insert_absorb2 list.simps(15) set_append)
+ − 580
+ − 581
+ − 582
lemma flts_gstar:
+ − 583
shows "rs \<leadsto>g* rflts rs"
+ − 584
apply(induct rs)
+ − 585
apply simp
+ − 586
apply(case_tac "a = RZERO")
+ − 587
apply simp
+ − 588
using gmany_steps_later grewrite.intros(1) apply blast
+ − 589
apply(case_tac "\<exists>rsa. a = RALTS rsa")
+ − 590
apply(erule exE)
+ − 591
apply simp
+ − 592
apply (meson grewrite.intros(2) grewrites.simps grewrites_cons)
+ − 593
by (simp add: grewrites_cons rflts_def_idiot)
+ − 594
+ − 595
lemma more_distinct1:
+ − 596
shows " \<lbrakk>\<And>rsb rset rset2.
+ − 597
rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2);
+ − 598
rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk>
+ − 599
\<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ − 600
apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)")
+ − 601
apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)")
+ − 602
apply (meson greal_trans)
+ − 603
apply (metis Un_iff Un_insert_left insert_absorb)
+ − 604
by (simp add: gr_in_rstar grewrite_variant1 in_mono)
+ − 605
+ − 606
+ − 607
+ − 608
+ − 609
+ − 610
lemma frewrite_rd_grewrites_aux:
+ − 611
shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 612
rsb @
+ − 613
RALTS rs #
+ − 614
rdistinct rsa
+ − 615
(insert (RALTS rs)
+ − 616
(set rsb)) \<leadsto>g* rflts rsb @
+ − 617
rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ − 618
+ − 619
apply simp
+ − 620
apply(subgoal_tac "rsb @
+ − 621
RALTS rs #
+ − 622
rdistinct rsa
+ − 623
(insert (RALTS rs)
+ − 624
(set rsb)) \<leadsto>g* rsb @
+ − 625
rs @
+ − 626
rdistinct rsa
+ − 627
(insert (RALTS rs)
+ − 628
(set rsb)) ")
+ − 629
apply(subgoal_tac " rsb @
+ − 630
rs @
+ − 631
rdistinct rsa
+ − 632
(insert (RALTS rs)
+ − 633
(set rsb)) \<leadsto>g*
+ − 634
rsb @
+ − 635
rdistinct rs (set rsb) @
+ − 636
rdistinct rsa
+ − 637
(insert (RALTS rs)
+ − 638
(set rsb)) ")
+ − 639
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)
+ − 640
apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+ − 641
by (simp add: gr_in_rstar grewrite.intros(2) grewrites_append)
+ − 642
+ − 643
+ − 644
+ − 645
+ − 646
lemma list_dlist_union:
+ − 647
shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"
+ − 648
by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)
+ − 649
+ − 650
lemma r_finite1:
+ − 651
shows "r = RALTS (r # rs) = False"
+ − 652
apply(induct r)
+ − 653
apply simp+
+ − 654
apply (metis list.set_intros(1))
+ − 655
by blast
+ − 656
+ − 657
+ − 658
+ − 659
lemma grewrite_singleton:
+ − 660
shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []"
+ − 661
apply (induct "[r]" "r # rs" rule: grewrite.induct)
+ − 662
apply simp
+ − 663
apply (metis r_finite1)
+ − 664
using grewrite.simps apply blast
+ − 665
by simp
+ − 666
+ − 667
+ − 668
+ − 669
lemma concat_rdistinct_equality1:
+ − 670
shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \<union> (set rs))"
+ − 671
apply(induct rs arbitrary: rsa rset)
+ − 672
apply simp
+ − 673
apply(case_tac "a \<in> rset")
+ − 674
apply simp
+ − 675
apply (simp add: insert_absorb)
+ − 676
by auto
+ − 677
+ − 678
+ − 679
lemma grewrites_rev_append:
+ − 680
shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"
+ − 681
using grewritess_concat by auto
+ − 682
+ − 683
lemma grewrites_inclusion:
+ − 684
shows "set rs \<subseteq> set rs1 \<Longrightarrow> rs1 @ rs \<leadsto>g* rs1"
+ − 685
apply(induct rs arbitrary: rs1)
+ − 686
apply simp
+ − 687
by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1))
+ − 688
+ − 689
lemma distinct_keeps_last:
+ − 690
shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+ − 691
by (simp add: concat_rdistinct_equality1)
+ − 692
+ − 693
lemma grewrites_shape2_aux:
+ − 694
shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 695
rsb @
+ − 696
rdistinct (rs @ rsa)
+ − 697
(set rsb) \<leadsto>g* rsb @
+ − 698
rdistinct rs (set rsb) @
+ − 699
rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ − 700
apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) = rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb)")
+ − 701
apply (simp only:)
+ − 702
prefer 2
+ − 703
apply (simp add: Un_commute concat_rdistinct_equality1)
+ − 704
apply(induct rsa arbitrary: rs rsb rule: rev_induct)
+ − 705
apply simp
+ − 706
apply(case_tac "x \<in> set rs")
+ − 707
apply (simp add: distinct_removes_middle3)
+ − 708
apply(case_tac "x = RALTS rs")
+ − 709
apply simp
+ − 710
apply(case_tac "x \<in> set rsb")
+ − 711
apply simp
+ − 712
apply (simp add: concat_rdistinct_equality1)
+ − 713
apply (simp add: concat_rdistinct_equality1)
+ − 714
apply simp
+ − 715
apply(drule_tac x = "rs " in meta_spec)
+ − 716
apply(drule_tac x = rsb in meta_spec)
+ − 717
apply simp
+ − 718
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))")
+ − 719
prefer 2
+ − 720
apply (simp add: concat_rdistinct_equality1)
+ − 721
apply(case_tac "x \<in> set xs")
+ − 722
apply simp
+ − 723
apply (simp add: distinct_removes_last)
+ − 724
apply(case_tac "x \<in> set rsb")
+ − 725
apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2))
+ − 726
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]")
+ − 727
apply(simp only:)
+ − 728
apply(case_tac "x = RALTS rs")
+ − 729
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")
+ − 730
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) ")
+ − 731
apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2))
+ − 732
apply(subgoal_tac "set rs \<subseteq> set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb))")
+ − 733
apply (metis append.assoc grewrites_inclusion)
+ − 734
apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append)
+ − 735
apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append)
+ − 736
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]")
+ − 737
apply(simp only:)
+ − 738
apply (metis append.assoc grewrites_rev_append)
+ − 739
apply (simp add: insert_absorb)
+ − 740
apply (simp add: distinct_keeps_last)+
+ − 741
done
+ − 742
+ − 743
lemma grewrites_shape2:
+ − 744
shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ − 745
rsb @
+ − 746
rdistinct (rs @ rsa)
+ − 747
(set rsb) \<leadsto>g* rflts rsb @
+ − 748
rdistinct rs (set rsb) @
+ − 749
rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ − 750
apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat)
+ − 751
done
+ − 752
+ − 753
lemma rdistinct_add_acc:
+ − 754
shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ − 755
apply(induct rs arbitrary: rsb rset rset2)
+ − 756
apply simp
+ − 757
apply (case_tac "a \<in> rset")
+ − 758
apply simp
+ − 759
apply(case_tac "a \<in> rset2")
+ − 760
apply simp
+ − 761
apply (simp add: more_distinct1)
+ − 762
apply simp
+ − 763
apply(drule_tac x = "rsb @ [a]" in meta_spec)
+ − 764
by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)
+ − 765
+ − 766
+ − 767
lemma frewrite_fun1:
+ − 768
shows " RALTS rs \<in> set rsb \<Longrightarrow>
+ − 769
rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)"
+ − 770
apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb)")
+ − 771
apply(subgoal_tac " set rs \<subseteq> set (rflts rsb)")
+ − 772
prefer 2
+ − 773
using spilled_alts_contained apply blast
+ − 774
apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)")
+ − 775
using greal_trans apply blast
+ − 776
using rdistinct_add_acc apply presburger
+ − 777
using flts_gstar grewritess_concat by auto
+ − 778
+ − 779
lemma frewrite_rd_grewrites:
+ − 780
shows "rs1 \<leadsto>f rs2 \<Longrightarrow>
+ − 781
\<exists>rs3. (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3) "
+ − 782
apply(induct rs1 rs2 arbitrary: rs rule: frewrite.induct)
+ − 783
apply(rule_tac x = "rsa @ (rdistinct rs ({RZERO} \<union> set rsa))" in exI)
+ − 784
apply(rule conjI)
+ − 785
apply(case_tac "RZERO \<in> set rsa")
+ − 786
apply simp+
+ − 787
using gstar0 apply fastforce
+ − 788
apply (simp add: gr_in_rstar grewrite.intros(1) grewrites_append)
+ − 789
apply (simp add: gstar0)
+ − 790
prefer 2
+ − 791
apply(case_tac "r \<in> set rs")
+ − 792
apply simp
+ − 793
apply(drule_tac x = "rs @ [r]" in meta_spec)
+ − 794
apply(erule exE)
+ − 795
apply(rule_tac x = "rs3" in exI)
+ − 796
apply simp
+ − 797
apply(case_tac "RALTS rs \<in> set rsb")
+ − 798
apply simp
+ − 799
apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" in exI)
+ − 800
apply(rule conjI)
+ − 801
using frewrite_fun1 apply force
+ − 802
apply (metis frewrite_fun1 rdistinct_concat sup_ge2)
+ − 803
apply(simp)
+ − 804
apply(rule_tac x =
+ − 805
"rflts rsb @
+ − 806
rdistinct rs (set rsb) @
+ − 807
rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)
+ − 808
apply(rule conjI)
+ − 809
prefer 2
+ − 810
using grewrites_shape2 apply force
+ − 811
using frewrite_rd_grewrites_aux by blast
+ − 812
+ − 813
+ − 814
lemma frewrite_simpeq2:
+ − 815
shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
+ − 816
apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")
+ − 817
using grewrites_equal_rsimp apply fastforce
+ − 818
by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))
+ − 819
+ − 820
+ − 821
+ − 822
+ − 823
(*a more refined notion of h\<leadsto>* is needed,
+ − 824
this lemma fails when rs1 contains some RALTS rs where elements
+ − 825
of rs appear in later parts of rs1, which will be picked up by rs2
+ − 826
and deduplicated*)
+ − 827
lemma frewrites_simpeq:
+ − 828
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
+ − 829
rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
+ − 830
apply(induct rs1 rs2 rule: frewrites.induct)
+ − 831
apply simp
+ − 832
using frewrite_simpeq2 by presburger
+ − 833
+ − 834
+ − 835
lemma frewrite_single_step:
+ − 836
shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
+ − 837
apply(induct rs2 rs3 rule: frewrite.induct)
+ − 838
apply simp
+ − 839
using simp_flatten apply blast
+ − 840
by (metis (no_types, opaque_lifting) list.simps(9) rsimp.simps(2) simp_flatten2)
+ − 841
+ − 842
lemma grewrite_simpalts:
+ − 843
shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ − 844
apply(induct rs2 rs3 rule : grewrite.induct)
+ − 845
using identity_wwo0 apply presburger
+ − 846
apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten)
+ − 847
apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3))
+ − 848
apply simp
+ − 849
apply(subst rsimp_alts_equal)
+ − 850
apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []")
+ − 851
apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]")
+ − 852
apply (simp only:)
+ − 853
apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2))
+ − 854
apply simp
+ − 855
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)
+ − 856
+ − 857
+ − 858
lemma grewrites_simpalts:
+ − 859
shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ − 860
apply(induct rs2 rs3 rule: grewrites.induct)
+ − 861
apply simp
+ − 862
using grewrite_simpalts by presburger
+ − 863
+ − 864
+ − 865
lemma simp_der_flts:
+ − 866
shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) =
+ − 867
rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
+ − 868
apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
+ − 869
using frewrites_simpeq apply presburger
+ − 870
using early_late_der_frewrites by auto
+ − 871
+ − 872
+ − 873
lemma simp_der_pierce_flts_prelim:
+ − 874
shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {}))
+ − 875
= rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
+ − 876
by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
+ − 877
+ − 878
+ − 879
lemma basic_regex_property1:
+ − 880
shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
+ − 881
apply(induct r rule: rsimp.induct)
+ − 882
apply(auto)
+ − 883
apply (metis idiot idiot2 rrexp.distinct(5))
+ − 884
by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
+ − 885
+ − 886
+ − 887
lemma inside_simp_seq_nullable:
+ − 888
shows
+ − 889
"\<And>r1 r2.
+ − 890
\<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+ − 891
rnullable r1\<rbrakk>
+ − 892
\<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+ − 893
rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+ − 894
apply(case_tac "rsimp r1 = RONE")
+ − 895
apply(simp)
+ − 896
apply(subst basic_rsimp_SEQ_property1)
+ − 897
apply (simp add: idem_after_simp1)
+ − 898
apply(case_tac "rsimp r1 = RZERO")
+ − 899
+ − 900
using basic_regex_property1 apply blast
+ − 901
apply(case_tac "rsimp r2 = RZERO")
+ − 902
+ − 903
apply (simp add: basic_rsimp_SEQ_property3)
+ − 904
apply(subst idiot2)
+ − 905
apply simp+
+ − 906
apply(subgoal_tac "rnullable (rsimp r1)")
+ − 907
apply simp
+ − 908
using rsimp_idem apply presburger
+ − 909
using der_simp_nullability by presburger
+ − 910
+ − 911
+ − 912
+ − 913
lemma grewrite_ralts:
+ − 914
shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
+ − 915
by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
+ − 916
+ − 917
lemma grewrites_ralts:
+ − 918
shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
+ − 919
apply(induct rule: grewrites.induct)
+ − 920
apply simp
+ − 921
using grewrite_ralts hreal_trans by blast
+ − 922
+ − 923
+ − 924
lemma distinct_grewrites_subgoal1:
+ − 925
shows "
+ − 926
\<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"
+ − 927
apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")
+ − 928
apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+ − 929
apply(subgoal_tac "rs1 \<leadsto>g* rs3")
+ − 930
using grewrites_ralts apply blast
+ − 931
using grewrites.intros(2) by presburger
+ − 932
+ − 933
lemma grewrites_ralts_rsimpalts:
+ − 934
shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "
+ − 935
apply(induct rs rs' rule: grewrites.induct)
+ − 936
apply(case_tac rs)
+ − 937
using hrewrite.intros(9) apply force
+ − 938
apply(case_tac list)
+ − 939
apply simp
+ − 940
using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger
+ − 941
apply simp
+ − 942
apply(case_tac rs2)
+ − 943
apply simp
+ − 944
apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))
+ − 945
apply(case_tac list)
+ − 946
apply(simp)
+ − 947
using distinct_grewrites_subgoal1 apply blast
+ − 948
apply simp
+ − 949
apply(case_tac rs3)
+ − 950
apply simp
+ − 951
using grewrites_ralts hrewrite.intros(9) apply blast
+ − 952
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))
+ − 953
+ − 954
lemma hrewrites_alts:
+ − 955
shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS (rs1 @ [r'] @ rs2))"
+ − 956
apply(induct r r' rule: hrewrites.induct)
+ − 957
apply simp
+ − 958
using hrewrite.intros(6) by blast
+ − 959
+ − 960
inductive
+ − 961
srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
+ − 962
where
+ − 963
ss1: "[] scf\<leadsto>* []"
+ − 964
| ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
+ − 965
+ − 966
+ − 967
lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"
+ − 968
+ − 969
apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
+ − 970
apply(rule rs1)
+ − 971
apply(drule_tac x = "rsa@[r']" in meta_spec)
+ − 972
apply simp
+ − 973
apply(rule hreal_trans)
+ − 974
prefer 2
+ − 975
apply(assumption)
+ − 976
apply(drule hrewrites_alts)
+ − 977
by auto
+ − 978
+ − 979
+ − 980
corollary srewritescf_alt1:
+ − 981
assumes "rs1 scf\<leadsto>* rs2"
+ − 982
shows "RALTS rs1 h\<leadsto>* RALTS rs2"
+ − 983
using assms
+ − 984
by (metis append_Nil srewritescf_alt)
+ − 985
+ − 986
+ − 987
+ − 988
+ − 989
lemma trivialrsimp_srewrites:
+ − 990
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
+ − 991
+ − 992
apply(induction rs)
+ − 993
apply simp
+ − 994
apply(rule ss1)
+ − 995
by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
+ − 996
+ − 997
lemma hrewrites_list:
+ − 998
shows
+ − 999
" (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"
+ − 1000
apply(induct x)
+ − 1001
apply(simp)+
+ − 1002
by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
+ − 1003
(* apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)
+ − 1004
+ − 1005
+ − 1006
lemma hrewrite_simpeq:
+ − 1007
shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ − 1008
apply(induct rule: hrewrite.induct)
+ − 1009
apply simp+
+ − 1010
apply (simp add: basic_rsimp_SEQ_property3)
+ − 1011
apply (simp add: basic_rsimp_SEQ_property1)
+ − 1012
using rsimp.simps(1) apply presburger
+ − 1013
apply simp+
+ − 1014
using flts_middle0 apply force
+ − 1015
+ − 1016
+ − 1017
using simp_flatten3 apply presburger
+ − 1018
+ − 1019
apply simp+
+ − 1020
apply (simp add: idem_after_simp1)
+ − 1021
using grewrite.intros(4) grewrite_equal_rsimp by presburger
+ − 1022
+ − 1023
lemma hrewrites_simpeq:
+ − 1024
shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ − 1025
apply(induct rule: hrewrites.induct)
+ − 1026
apply simp
+ − 1027
apply(subgoal_tac "rsimp r2 = rsimp r3")
+ − 1028
apply auto[1]
+ − 1029
using hrewrite_simpeq by presburger
+ − 1030
+ − 1031
+ − 1032
+ − 1033
lemma simp_hrewrites:
+ − 1034
shows "r1 h\<leadsto>* rsimp r1"
+ − 1035
apply(induct r1)
+ − 1036
apply simp+
+ − 1037
apply(case_tac "rsimp r11 = RONE")
+ − 1038
apply simp
+ − 1039
apply(subst basic_rsimp_SEQ_property1)
+ − 1040
apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")
+ − 1041
using hreal_trans hrewrite.intros(3) apply blast
+ − 1042
using hrewrites_seq_context apply presburger
+ − 1043
apply(case_tac "rsimp r11 = RZERO")
+ − 1044
apply simp
+ − 1045
using hrewrite.intros(1) hrewrites_seq_context apply blast
+ − 1046
apply(case_tac "rsimp r12 = RZERO")
+ − 1047
apply simp
+ − 1048
apply(subst basic_rsimp_SEQ_property3)
+ − 1049
apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)
+ − 1050
apply(subst idiot2)
+ − 1051
apply simp+
+ − 1052
using hrewrites_seq_contexts apply presburger
+ − 1053
apply simp
+ − 1054
apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")
+ − 1055
apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
+ − 1056
using hreal_trans apply blast
+ − 1057
apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
+ − 1058
+ − 1059
apply (simp add: grewrites_ralts hrewrites_list)
+ − 1060
by simp
+ − 1061
+ − 1062
lemma interleave_aux1:
+ − 1063
shows " RALT (RSEQ RZERO r1) r h\<leadsto>* r"
+ − 1064
apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")
+ − 1065
apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")
+ − 1066
apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
+ − 1067
using rs1 srewritescf_alt1 ss1 ss2 apply presburger
+ − 1068
by (simp add: hr_in_rstar hrewrite.intros(1))
+ − 1069
+ − 1070
+ − 1071
+ − 1072
lemma rnullable_hrewrite:
+ − 1073
shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
+ − 1074
apply(induct rule: hrewrite.induct)
+ − 1075
apply simp+
+ − 1076
apply blast
+ − 1077
apply simp+
+ − 1078
done
+ − 1079
+ − 1080
+ − 1081
lemma interleave1:
+ − 1082
shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
+ − 1083
apply(induct r r' rule: hrewrite.induct)
+ − 1084
apply (simp add: hr_in_rstar hrewrite.intros(1))
+ − 1085
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)
+ − 1086
apply simp
+ − 1087
apply(subst interleave_aux1)
+ − 1088
apply simp
+ − 1089
apply(case_tac "rnullable r1")
+ − 1090
apply simp
+ − 1091
+ − 1092
apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2)
+ − 1093
+ − 1094
apply (simp add: hrewrites_seq_context rnullable_hrewrite)
+ − 1095
apply(case_tac "rnullable r1")
+ − 1096
apply simp
+ − 1097
+ − 1098
using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger
+ − 1099
apply simp
+ − 1100
using hr_in_rstar hrewrites_seq_context2 apply blast
+ − 1101
apply simp
+ − 1102
+ − 1103
using hrewrites_alts apply auto[1]
+ − 1104
apply simp
+ − 1105
using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1]
+ − 1106
apply simp
+ − 1107
apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts)
+ − 1108
apply (simp add: hr_in_rstar hrewrite.intros(9))
+ − 1109
apply (simp add: hr_in_rstar hrewrite.intros(10))
+ − 1110
apply simp
+ − 1111
using hrewrite.intros(11) by auto
+ − 1112
+ − 1113
lemma interleave_star1:
+ − 1114
shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
+ − 1115
apply(induct rule : hrewrites.induct)
+ − 1116
apply simp
+ − 1117
by (meson hreal_trans interleave1)
+ − 1118
+ − 1119
+ − 1120
+ − 1121
lemma inside_simp_removal:
+ − 1122
shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
+ − 1123
apply(induct r)
+ − 1124
apply simp+
+ − 1125
apply(case_tac "rnullable r1")
+ − 1126
apply simp
+ − 1127
+ − 1128
using inside_simp_seq_nullable apply blast
+ − 1129
apply simp
+ − 1130
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)
+ − 1131
apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
+ − 1132
using hrewrites_simpeq apply presburger
+ − 1133
using interleave_star1 simp_hrewrites apply presburger
+ − 1134
by simp
+ − 1135
+ − 1136
+ − 1137
+ − 1138
+ − 1139
lemma rders_simp_same_simpders:
+ − 1140
shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+ − 1141
apply(induct s rule: rev_induct)
+ − 1142
apply simp
+ − 1143
apply(case_tac "xs = []")
+ − 1144
apply simp
+ − 1145
apply(simp add: rders_append rders_simp_append)
+ − 1146
using inside_simp_removal by blast
+ − 1147
+ − 1148
+ − 1149
+ − 1150
+ − 1151
lemma distinct_der:
+ − 1152
shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) =
+ − 1153
rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+ − 1154
by (metis grewrites_simpalts gstar_rdistinct inside_simp_removal rder_rsimp_ALTs_commute)
+ − 1155
+ − 1156
+ − 1157
+ − 1158
+ − 1159
+ − 1160
lemma rders_simp_lambda:
+ − 1161
shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"
+ − 1162
using rders_simp_append by auto
+ − 1163
+ − 1164
lemma rders_simp_nonempty_simped:
+ − 1165
shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"
+ − 1166
using rders_simp_same_simpders rsimp_idem by auto
+ − 1167
+ − 1168
lemma repeated_altssimp:
+ − 1169
shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
+ − 1170
rsimp_ALTs (rdistinct (rflts rs) {})"
+ − 1171
by (metis map_idI rsimp.simps(2) rsimp_idem)
+ − 1172
+ − 1173
+ − 1174
+ − 1175
lemma alts_closed_form:
+ − 1176
shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
+ − 1177
apply(induct s rule: rev_induct)
+ − 1178
apply simp
+ − 1179
apply simp
+ − 1180
apply(subst rders_simp_append)
+ − 1181
apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) =
+ − 1182
rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
+ − 1183
prefer 2
+ − 1184
apply (metis inside_simp_removal rders_simp_one_char)
+ − 1185
apply(simp only: )
+ − 1186
apply(subst rders_simp_one_char)
+ − 1187
apply(subst rsimp_idem)
+ − 1188
apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
+ − 1189
rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
+ − 1190
prefer 2
+ − 1191
using rder_rsimp_ALTs_commute apply presburger
+ − 1192
apply(simp only:)
+ − 1193
apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
+ − 1194
= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+ − 1195
prefer 2
+ − 1196
+ − 1197
using distinct_der apply presburger
+ − 1198
apply(simp only:)
+ − 1199
apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
+ − 1200
rsimp (rsimp_ALTs (rdistinct ( (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)))) {}))")
+ − 1201
apply(simp only:)
+ − 1202
apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
+ − 1203
rsimp (rsimp_ALTs (rdistinct (rflts ( (map (rsimp \<circ> (rder x) \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+ − 1204
apply(simp only:)
+ − 1205
apply(subst rders_simp_lambda)
+ − 1206
apply(subst rders_simp_nonempty_simped)
+ − 1207
apply simp
+ − 1208
apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (xs @ [x])) rs). rsimp r = r")
+ − 1209
prefer 2
+ − 1210
apply (simp add: rders_simp_same_simpders rsimp_idem)
+ − 1211
apply(subst repeated_altssimp)
+ − 1212
apply simp
+ − 1213
apply fastforce
+ − 1214
apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
+ − 1215
using simp_der_pierce_flts_prelim by blast
+ − 1216
+ − 1217
+ − 1218
lemma alts_closed_form_variant:
+ − 1219
shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
+ − 1220
by (metis alts_closed_form comp_apply rders_simp_nonempty_simped)
+ − 1221
+ − 1222
+ − 1223
lemma rsimp_seq_equal1:
+ − 1224
shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})"
+ − 1225
by (metis idem_after_simp1 rsimp.simps(1))
+ − 1226
+ − 1227
+ − 1228
fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where
+ − 1229
"sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs"
+ − 1230
| "sflat_aux (RALTS []) = []"
+ − 1231
| "sflat_aux r = [r]"
+ − 1232
+ − 1233
+ − 1234
fun sflat :: "rrexp \<Rightarrow> rrexp" where
+ − 1235
"sflat (RALTS (r # [])) = r"
+ − 1236
| "sflat (RALTS (r # rs)) = RALTS (sflat_aux r @ rs)"
+ − 1237
| "sflat r = r"
+ − 1238
+ − 1239
inductive created_by_seq:: "rrexp \<Rightarrow> bool" where
+ − 1240
"created_by_seq (RSEQ r1 r2) "
+ − 1241
| "created_by_seq r1 \<Longrightarrow> created_by_seq (RALT r1 r2)"
+ − 1242
+ − 1243
lemma seq_ders_shape1:
+ − 1244
shows "\<forall>r1 r2. \<exists>r3 r4. (rders (RSEQ r1 r2) s) = RSEQ r3 r4 \<or> (rders (RSEQ r1 r2) s) = RALT r3 r4"
+ − 1245
apply(induct s rule: rev_induct)
+ − 1246
apply auto[1]
+ − 1247
apply(rule allI)+
+ − 1248
apply(subst rders_append)+
+ − 1249
apply(subgoal_tac " \<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or> rders (RSEQ r1 r2) xs = RALT r3 r4 ")
+ − 1250
apply(erule exE)+
+ − 1251
apply(erule disjE)
+ − 1252
apply simp+
+ − 1253
done
+ − 1254
+ − 1255
lemma created_by_seq_der:
+ − 1256
shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)"
+ − 1257
apply(induct r)
+ − 1258
apply simp+
+ − 1259
+ − 1260
using created_by_seq.cases apply blast
+ − 1261
+ − 1262
apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21))
+ − 1263
apply (metis created_by_seq.simps rder.simps(5))
+ − 1264
apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3))
+ − 1265
using created_by_seq.intros(1) by force
+ − 1266
+ − 1267
lemma createdbyseq_left_creatable:
+ − 1268
shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1"
+ − 1269
using created_by_seq.cases by blast
+ − 1270
+ − 1271
+ − 1272
+ − 1273
lemma recursively_derseq:
+ − 1274
shows " created_by_seq (rders (RSEQ r1 r2) s)"
+ − 1275
apply(induct s rule: rev_induct)
+ − 1276
apply simp
+ − 1277
using created_by_seq.intros(1) apply force
+ − 1278
apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) (xs @ [x]))")
+ − 1279
apply blast
+ − 1280
apply(subst rders_append)
+ − 1281
apply(subgoal_tac "\<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or>
+ − 1282
rders (RSEQ r1 r2) xs = RALT r3 r4")
+ − 1283
prefer 2
+ − 1284
using seq_ders_shape1 apply presburger
+ − 1285
apply(erule exE)+
+ − 1286
apply(erule disjE)
+ − 1287
apply(subgoal_tac "created_by_seq (rders (RSEQ r3 r4) [x])")
+ − 1288
apply presburger
+ − 1289
apply simp
+ − 1290
using created_by_seq.intros(1) created_by_seq.intros(2) apply presburger
+ − 1291
apply simp
+ − 1292
apply(subgoal_tac "created_by_seq r3")
+ − 1293
prefer 2
+ − 1294
using createdbyseq_left_creatable apply blast
+ − 1295
using created_by_seq.intros(2) created_by_seq_der by blast
+ − 1296
+ − 1297
+ − 1298
lemma recursively_derseq1:
+ − 1299
shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> created_by_seq r"
+ − 1300
using recursively_derseq by blast
+ − 1301
+ − 1302
+ − 1303
lemma sfau_head:
+ − 1304
shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs"
+ − 1305
apply(induction r rule: created_by_seq.induct)
+ − 1306
apply simp
+ − 1307
by fastforce
+ − 1308
+ − 1309
+ − 1310
lemma vsuf_prop1:
+ − 1311
shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs))
+ − 1312
then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
+ − 1313
else (map (\<lambda>s. s @ [x]) (vsuf xs r)) )
+ − 1314
"
+ − 1315
apply(induct xs arbitrary: r)
+ − 1316
apply simp
+ − 1317
apply(case_tac "rnullable r")
+ − 1318
apply simp
+ − 1319
apply simp
+ − 1320
done
+ − 1321
+ − 1322
fun breakHead :: "rrexp list \<Rightarrow> rrexp list" where
+ − 1323
"breakHead [] = [] "
+ − 1324
| "breakHead (RALT r1 r2 # rs) = r1 # r2 # rs"
+ − 1325
| "breakHead (r # rs) = r # rs"
+ − 1326
+ − 1327
+ − 1328
lemma sfau_idem_der:
+ − 1329
shows "created_by_seq r \<Longrightarrow> sflat_aux (rder c r) = breakHead (map (rder c) (sflat_aux r))"
+ − 1330
apply(induct rule: created_by_seq.induct)
+ − 1331
apply simp+
+ − 1332
using sfau_head by fastforce
+ − 1333
+ − 1334
lemma vsuf_compose1:
+ − 1335
shows " \<not> rnullable (rders r1 xs)
+ − 1336
\<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)"
+ − 1337
apply(subst vsuf_prop1)
+ − 1338
apply simp
+ − 1339
by (simp add: rders_append)
+ − 1340
+ − 1341
thm sfau_idem_der
+ − 1342
+ − 1343
lemma oneCharvsuf:
+ − 1344
shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2) (vsuf [x] r1)"
+ − 1345
by simp
+ − 1346
+ − 1347
+ − 1348
lemma vsuf_compose2:
+ − 1349
shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = map (rders r2) (vsuf (xs @ [x]) r1)"
+ − 1350
proof(induct xs arbitrary: r1)
+ − 1351
case Nil
+ − 1352
then show ?case
+ − 1353
by simp
+ − 1354
next
+ − 1355
case (Cons a xs)
+ − 1356
have "rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) =
+ − 1357
map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
+ − 1358
proof
+ − 1359
assume nullableCond: "rnullable (rders r1 xs)"
+ − 1360
have "rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])"
+ − 1361
by (simp add: rders_append)
+ − 1362
show " map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) =
+ − 1363
map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
+ − 1364
using \<open>rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])\<close> local.Cons by auto
+ − 1365
qed
+ − 1366
then have "\<not> rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) =
+ − 1367
map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
+ − 1368
apply simp
+ − 1369
by (smt (verit, ccfv_threshold) append_Cons append_Nil list.map_comp list.simps(8) list.simps(9) local.Cons rders.simps(1) rders.simps(2) rders_append vsuf.simps(1) vsuf.simps(2))
+ − 1370
then show ?case
+ − 1371
using \<open>rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = map (rders r2) (vsuf ((a # xs) @ [x]) r1)\<close> by blast
+ − 1372
qed
+ − 1373
+ − 1374
+ − 1375
lemma seq_sfau0:
+ − 1376
shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) #
+ − 1377
(map (rders r2) (vsuf s r1)) "
+ − 1378
proof(induct s rule: rev_induct)
+ − 1379
case Nil
+ − 1380
then show ?case
+ − 1381
by simp
+ − 1382
next
+ − 1383
case (snoc x xs)
+ − 1384
then have LHS1:"sflat_aux (rders (RSEQ r1 r2) (xs @ [x])) = sflat_aux (rder x (rders (RSEQ r1 r2) xs)) "
+ − 1385
by (simp add: rders_append)
+ − 1386
then have LHS1A: "... = breakHead (map (rder x) (sflat_aux (rders (RSEQ r1 r2) xs)))"
+ − 1387
using recursively_derseq sfau_idem_der by auto
+ − 1388
then have LHS1B: "... = breakHead (map (rder x) (RSEQ (rders r1 xs) r2 # map (rders r2) (vsuf xs r1)))"
+ − 1389
using snoc by auto
+ − 1390
then have LHS1C: "... = breakHead (rder x (RSEQ (rders r1 xs) r2) # map (rder x) (map (rders r2) (vsuf xs r1)))"
+ − 1391
by simp
+ − 1392
then have LHS1D: "... = breakHead [rder x (RSEQ (rders r1 xs) r2)] @ map (rder x) (map (rders r2) (vsuf xs r1))"
+ − 1393
by simp
+ − 1394
then have LHS1E: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1))"
+ − 1395
by force
+ − 1396
then have LHS1F: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))"
+ − 1397
using vsuf_compose2 by blast
+ − 1398
then have LHS1G: "... = RSEQ (rders r1 (xs @ [x])) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))"
+ − 1399
using rders.simps(1) rders.simps(2) rders_append by presburger
+ − 1400
then show ?case
+ − 1401
using LHS1 LHS1A LHS1C LHS1D LHS1E LHS1F snoc by presburger
+ − 1402
qed
+ − 1403
+ − 1404
+ − 1405
+ − 1406
+ − 1407
+ − 1408
+ − 1409
lemma sflat_rsimpeq:
+ − 1410
shows "created_by_seq r1 \<Longrightarrow> sflat_aux r1 = rs \<Longrightarrow> rsimp r1 = rsimp (RALTS rs)"
+ − 1411
apply(induct r1 arbitrary: rs rule: created_by_seq.induct)
+ − 1412
apply simp
+ − 1413
using rsimp_seq_equal1 apply force
+ − 1414
by (metis head_one_more_simp rsimp.simps(2) sflat_aux.simps(1) simp_flatten)
+ − 1415
+ − 1416
+ − 1417
+ − 1418
lemma seq_closed_form_general:
+ − 1419
shows "rsimp (rders (RSEQ r1 r2) s) =
+ − 1420
rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
+ − 1421
apply(case_tac "s \<noteq> []")
+ − 1422
apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) s)")
+ − 1423
apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))")
+ − 1424
using sflat_rsimpeq apply blast
+ − 1425
apply (simp add: seq_sfau0)
+ − 1426
using recursively_derseq1 apply blast
+ − 1427
apply simp
+ − 1428
by (metis idem_after_simp1 rsimp.simps(1))
+ − 1429
+ − 1430
lemma seq_closed_form_aux1a:
+ − 1431
shows "rsimp (RALTS (RSEQ (rders r1 s) r2 # rs)) =
+ − 1432
rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # rs))"
+ − 1433
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)
+ − 1434
+ − 1435
+ − 1436
lemma seq_closed_form_aux1:
+ − 1437
shows "rsimp (RALTS (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))) =
+ − 1438
rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))"
+ − 1439
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)
+ − 1440
+ − 1441
lemma add_simp_to_rest:
+ − 1442
shows "rsimp (RALTS (r # rs)) = rsimp (RALTS (r # map rsimp rs))"
+ − 1443
by (metis append_Nil2 grewrite.intros(2) grewrite_simpalts head_one_more_simp list.simps(9) rsimp_ALTs.simps(2) spawn_simp_rsimpalts)
+ − 1444
+ − 1445
lemma rsimp_compose_der2:
+ − 1446
shows "\<forall>s \<in> set ss. s \<noteq> [] \<Longrightarrow> map rsimp (map (rders r) ss) = map (\<lambda>s. (rders_simp r s)) ss"
+ − 1447
by (simp add: rders_simp_same_simpders)
+ − 1448
+ − 1449
lemma vsuf_nonempty:
+ − 1450
shows "\<forall>s \<in> set ( vsuf s1 r). s \<noteq> []"
+ − 1451
apply(induct s1 arbitrary: r)
+ − 1452
apply simp
+ − 1453
apply simp
+ − 1454
done
+ − 1455
+ − 1456
+ − 1457
+ − 1458
lemma seq_closed_form_aux2:
+ − 1459
shows "s \<noteq> [] \<Longrightarrow> rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1)))))) =
+ − 1460
rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))))"
+ − 1461
+ − 1462
by (metis add_simp_to_rest rsimp_compose_der2 vsuf_nonempty)
+ − 1463
+ − 1464
+ − 1465
lemma seq_closed_form:
+ − 1466
shows "rsimp (rders_simp (RSEQ r1 r2) s) =
+ − 1467
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
+ − 1468
proof (cases s)
+ − 1469
case Nil
+ − 1470
then show ?thesis
+ − 1471
by (simp add: rsimp_seq_equal1[symmetric])
+ − 1472
next
+ − 1473
case (Cons a list)
+ − 1474
have "rsimp (rders_simp (RSEQ r1 r2) s) = rsimp (rsimp (rders (RSEQ r1 r2) s))"
+ − 1475
using local.Cons by (subst rders_simp_same_simpders)(simp_all)
+ − 1476
also have "... = rsimp (rders (RSEQ r1 r2) s)"
+ − 1477
by (simp add: rsimp_idem)
+ − 1478
also have "... = rsimp (RALTS (RSEQ (rders r1 s) r2 # map (rders r2) (vsuf s r1)))"
+ − 1479
using seq_closed_form_general by blast
+ − 1480
also have "... = rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders r2) (vsuf s r1)))"
+ − 1481
by (simp only: seq_closed_form_aux1)
+ − 1482
also have "... = rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))"
+ − 1483
using local.Cons by (subst seq_closed_form_aux2)(simp_all)
+ − 1484
finally show ?thesis .
+ − 1485
qed
+ − 1486
+ − 1487
lemma q: "s \<noteq> [] \<Longrightarrow> rders_simp (RSEQ r1 r2) s = rsimp (rders_simp (RSEQ r1 r2) s)"
+ − 1488
using rders_simp_same_simpders rsimp_idem by presburger
+ − 1489
+ − 1490
+ − 1491
lemma seq_closed_form_variant:
+ − 1492
assumes "s \<noteq> []"
+ − 1493
shows "rders_simp (RSEQ r1 r2) s =
543
+ − 1494
rsimp (RALTS (RSEQ (rders_simp r1 s) r2 #
+ − 1495
(map (rders_simp r2) (vsuf s r1))))"
505
+ − 1496
using assms q seq_closed_form by force
+ − 1497
+ − 1498
+ − 1499
fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where
+ − 1500
"hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2"
+ − 1501
| "hflat_aux r = [r]"
+ − 1502
+ − 1503
+ − 1504
fun hflat :: "rrexp \<Rightarrow> rrexp" where
+ − 1505
"hflat (RALT r1 r2) = RALTS ((hflat_aux r1) @ (hflat_aux r2))"
+ − 1506
| "hflat r = r"
+ − 1507
+ − 1508
inductive created_by_star :: "rrexp \<Rightarrow> bool" where
+ − 1509
"created_by_star (RSEQ ra (RSTAR rb))"
+ − 1510
| "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)"
+ − 1511
+ − 1512
+ − 1513
+ − 1514
+ − 1515
lemma cbs_ders_cbs:
+ − 1516
shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)"
+ − 1517
apply(induct r rule: created_by_star.induct)
+ − 1518
apply simp
+ − 1519
using created_by_star.intros(1) created_by_star.intros(2) apply auto[1]
+ − 1520
by (metis (mono_tags, lifting) created_by_star.simps list.simps(8) list.simps(9) rder.simps(4))
+ − 1521
+ − 1522
lemma star_ders_cbs:
+ − 1523
shows "created_by_star (rders (RSEQ r1 (RSTAR r2)) s)"
+ − 1524
apply(induct s rule: rev_induct)
+ − 1525
apply simp
+ − 1526
apply (simp add: created_by_star.intros(1))
+ − 1527
apply(subst rders_append)
+ − 1528
apply simp
+ − 1529
using cbs_ders_cbs by auto
+ − 1530
+ − 1531
(*
+ − 1532
lemma created_by_star_cases:
+ − 1533
shows "created_by_star r \<Longrightarrow> \<exists>ra rb. (r = RALT ra rb \<and> created_by_star ra \<and> created_by_star rb) \<or> r = RSEQ ra rb "
+ − 1534
by (meson created_by_star.cases)
+ − 1535
*)
+ − 1536
+ − 1537
+ − 1538
lemma hfau_pushin:
+ − 1539
shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))"
506
+ − 1540
+ − 1541
proof(induct r rule: created_by_star.induct)
+ − 1542
case (1 ra rb)
+ − 1543
then show ?case by simp
+ − 1544
next
+ − 1545
case (2 r1 r2)
+ − 1546
then have "created_by_star (rder c r1)"
+ − 1547
using cbs_ders_cbs by blast
+ − 1548
then have "created_by_star (rder c r2)"
+ − 1549
using "2.hyps"(3) cbs_ders_cbs by auto
+ − 1550
then show ?case
+ − 1551
by (simp add: "2.hyps"(2) "2.hyps"(4))
+ − 1552
qed
+ − 1553
513
+ − 1554
(*AALTS [a\x . b.c, b\x .c, c \x]*)
+ − 1555
(*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
505
+ − 1556
+ − 1557
lemma stupdate_induct1:
+ − 1558
shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
+ − 1559
map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"
+ − 1560
apply(induct Ss)
+ − 1561
apply simp+
+ − 1562
by (simp add: rders_append)
+ − 1563
+ − 1564
+ − 1565
+ − 1566
lemma stupdates_join_general:
+ − 1567
shows "concat (map hflat_aux (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) =
+ − 1568
map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)"
+ − 1569
apply(induct xs arbitrary: Ss)
+ − 1570
apply (simp)
+ − 1571
prefer 2
+ − 1572
apply auto[1]
+ − 1573
using stupdate_induct1 by blast
+ − 1574
+ − 1575
lemma star_hfau_induct:
+ − 1576
shows "hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) s) =
+ − 1577
map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])"
+ − 1578
apply(induct s rule: rev_induct)
+ − 1579
apply simp
+ − 1580
apply(subst rders_append)+
+ − 1581
apply simp
+ − 1582
apply(subst stupdates_append)
+ − 1583
apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)")
+ − 1584
prefer 2
+ − 1585
apply (simp add: star_ders_cbs)
+ − 1586
apply(subst hfau_pushin)
+ − 1587
apply simp
+ − 1588
apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) =
+ − 1589
concat (map hflat_aux (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ")
+ − 1590
apply(simp only:)
+ − 1591
prefer 2
+ − 1592
apply presburger
+ − 1593
apply(subst stupdates_append[symmetric])
+ − 1594
using stupdates_join_general by blast
+ − 1595
+ − 1596
lemma starders_hfau_also1:
+ − 1597
shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])"
+ − 1598
using star_hfau_induct by force
+ − 1599
+ − 1600
lemma hflat_aux_grewrites:
+ − 1601
shows "a # rs \<leadsto>g* hflat_aux a @ rs"
+ − 1602
apply(induct a arbitrary: rs)
+ − 1603
apply simp+
+ − 1604
apply(case_tac x)
+ − 1605
apply simp
+ − 1606
apply(case_tac list)
+ − 1607
+ − 1608
apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq)
+ − 1609
apply(case_tac lista)
+ − 1610
apply simp
+ − 1611
apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv)
+ − 1612
apply simp
+ − 1613
by simp
+ − 1614
+ − 1615
+ − 1616
+ − 1617
+ − 1618
lemma cbs_hfau_rsimpeq1:
+ − 1619
shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))"
+ − 1620
apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b")
+ − 1621
using grewrites_equal_rsimp apply presburger
+ − 1622
by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites)
+ − 1623
+ − 1624
+ − 1625
lemma hfau_rsimpeq2:
+ − 1626
shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
506
+ − 1627
apply(induct rule: created_by_star.induct)
+ − 1628
apply simp
+ − 1629
apply (metis rsimp.simps(6) rsimp_seq_equal1)
+ − 1630
using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger
+ − 1631
+ − 1632
+ − 1633
(*
+ − 1634
lemma hfau_rsimpeq2_oldproof: shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
505
+ − 1635
apply(induct r)
+ − 1636
apply simp+
+ − 1637
apply (metis rsimp_seq_equal1)
+ − 1638
prefer 2
+ − 1639
apply simp
+ − 1640
apply(case_tac x)
+ − 1641
apply simp
+ − 1642
apply(case_tac "list")
+ − 1643
apply simp
+ − 1644
apply (metis idem_after_simp1)
+ − 1645
apply(case_tac "lista")
+ − 1646
prefer 2
+ − 1647
apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))
+ − 1648
apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")
+ − 1649
apply simp
+ − 1650
apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")
+ − 1651
using hflat_aux.simps(1) apply presburger
+ − 1652
apply simp
+ − 1653
using cbs_hfau_rsimpeq1 by fastforce
506
+ − 1654
*)
505
+ − 1655
+ − 1656
lemma star_closed_form1:
+ − 1657
shows "rsimp (rders (RSTAR r0) (c#s)) =
+ − 1658
rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 1659
using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger
+ − 1660
+ − 1661
lemma star_closed_form2:
+ − 1662
shows "rsimp (rders_simp (RSTAR r0) (c#s)) =
+ − 1663
rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 1664
by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem star_closed_form1)
+ − 1665
+ − 1666
lemma star_closed_form3:
+ − 1667
shows "rsimp (rders_simp (RSTAR r0) (c#s)) = (rders_simp (RSTAR r0) (c#s))"
+ − 1668
by (metis list.distinct(1) rders_simp_same_simpders star_closed_form1 star_closed_form2)
+ − 1669
+ − 1670
lemma star_closed_form4:
+ − 1671
shows " (rders_simp (RSTAR r0) (c#s)) =
+ − 1672
rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 1673
using star_closed_form2 star_closed_form3 by presburger
+ − 1674
+ − 1675
lemma star_closed_form5:
+ − 1676
shows " rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) Ss )))) =
+ − 1677
rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ))))"
+ − 1678
by (metis (mono_tags, lifting) list.map_comp map_eq_conv o_apply rsimp.simps(2) rsimp_idem)
+ − 1679
+ − 1680
lemma star_closed_form6_hrewrites:
+ − 1681
shows "
+ − 1682
(map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss )
+ − 1683
scf\<leadsto>*
+ − 1684
(map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )"
+ − 1685
apply(induct Ss)
+ − 1686
apply simp
+ − 1687
apply (simp add: ss1)
+ − 1688
by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2)
+ − 1689
+ − 1690
lemma star_closed_form6:
+ − 1691
shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )))) =
+ − 1692
rsimp ( ( RALTS ( (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ))))"
+ − 1693
apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\<leadsto>*
+ − 1694
map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ")
+ − 1695
using hrewrites_simpeq srewritescf_alt1 apply fastforce
+ − 1696
using star_closed_form6_hrewrites by blast
+ − 1697
+ − 1698
lemma stupdate_nonempty:
+ − 1699
shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"
+ − 1700
apply(induct Ss)
+ − 1701
apply simp
+ − 1702
apply(case_tac "rnullable (rders r a)")
+ − 1703
apply simp+
+ − 1704
done
+ − 1705
+ − 1706
+ − 1707
lemma stupdates_nonempty:
+ − 1708
shows "\<forall>s \<in> set Ss. s\<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_updates s r Ss). s \<noteq> []"
+ − 1709
apply(induct s arbitrary: Ss)
+ − 1710
apply simp
+ − 1711
apply simp
+ − 1712
using stupdate_nonempty by presburger
+ − 1713
+ − 1714
+ − 1715
lemma star_closed_form8:
+ − 1716
shows
+ − 1717
"rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))) =
+ − 1718
rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ ( (rders_simp r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+ − 1719
by (smt (verit, ccfv_SIG) list.simps(8) map_eq_conv rders__onechar rders_simp_same_simpders set_ConsD stupdates_nonempty)
+ − 1720
+ − 1721
+ − 1722
lemma star_closed_form:
+ − 1723
shows "rders_simp (RSTAR r0) (c#s) =
+ − 1724
rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
+ − 1725
apply(induct s)
+ − 1726
apply simp
+ − 1727
apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
+ − 1728
using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
+ − 1729
+ − 1730
+ − 1731
unused_thms
+ − 1732
+ − 1733
end