thys2/ClosedForms.thy
author Chengsong
Wed, 30 Mar 2022 11:18:51 +0100
changeset 475 10fd25fba2ba
parent 473 37d14cbce020
child 476 56837303ce61
permissions -rw-r--r--
identities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
     1
theory ClosedForms imports
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
     2
"BasicIdentities"
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
     3
begin
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
     4
453
Chengsong
parents: 451
diff changeset
     5
465
Chengsong
parents: 456
diff changeset
     6
lemma idem_after_simp1:
Chengsong
parents: 456
diff changeset
     7
  shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
Chengsong
parents: 456
diff changeset
     8
  apply(case_tac "rsimp aa")
Chengsong
parents: 456
diff changeset
     9
  apply simp+
Chengsong
parents: 456
diff changeset
    10
  apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
Chengsong
parents: 456
diff changeset
    11
  by simp
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    12
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    13
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    14
lemma distinct_removes_last:
465
Chengsong
parents: 456
diff changeset
    15
  shows "\<lbrakk>a \<in> set as\<rbrakk>
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    16
    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    17
and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    18
  apply(induct as arbitrary: rset ab rset1 a)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    19
     apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    20
    apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    21
  apply(case_tac "aa \<in> rset")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    22
   apply(case_tac "a = aa")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    23
  apply (metis append_Cons)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    24
    apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    25
   apply(case_tac "a \<in> set as")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    26
  apply (metis append_Cons rdistinct.simps(2) set_ConsD)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    27
   apply(case_tac "a = aa")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    28
    prefer 2
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    29
    apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    30
   apply (metis append_Cons)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    31
  apply(case_tac "ab \<in> rset1")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    32
  prefer 2
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    33
   apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    34
               ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    35
  prefer 2
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    36
  apply force
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    37
  apply(simp only:)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    38
     apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    39
    apply(simp only:)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    40
    apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    41
     apply blast
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    42
    apply(case_tac "a \<in> insert ab rset1")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    43
     apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    44
     apply (metis insertI1)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    45
    apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    46
    apply (meson insertI1)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    47
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    48
  apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    49
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    50
  by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    51
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
    52
465
Chengsong
parents: 456
diff changeset
    53
lemma distinct_removes_middle:
Chengsong
parents: 456
diff changeset
    54
  shows  "\<lbrakk>a \<in> set as\<rbrakk>
Chengsong
parents: 456
diff changeset
    55
    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
Chengsong
parents: 456
diff changeset
    56
and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
Chengsong
parents: 456
diff changeset
    57
   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
Chengsong
parents: 456
diff changeset
    58
     apply simp
Chengsong
parents: 456
diff changeset
    59
    apply simp
Chengsong
parents: 456
diff changeset
    60
   apply(case_tac "a \<in> rset")
Chengsong
parents: 456
diff changeset
    61
    apply simp
Chengsong
parents: 456
diff changeset
    62
    apply metis
453
Chengsong
parents: 451
diff changeset
    63
   apply simp
465
Chengsong
parents: 456
diff changeset
    64
   apply (metis insertI1)
Chengsong
parents: 456
diff changeset
    65
  apply(case_tac "a = ab")
453
Chengsong
parents: 451
diff changeset
    66
   apply simp
465
Chengsong
parents: 456
diff changeset
    67
   apply(case_tac "ab \<in> rset")
453
Chengsong
parents: 451
diff changeset
    68
    apply simp
465
Chengsong
parents: 456
diff changeset
    69
    apply presburger
Chengsong
parents: 456
diff changeset
    70
   apply (meson insertI1)
Chengsong
parents: 456
diff changeset
    71
  apply(case_tac "a \<in> rset")
Chengsong
parents: 456
diff changeset
    72
  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
Chengsong
parents: 456
diff changeset
    73
  apply(case_tac "ab \<in> rset")
Chengsong
parents: 456
diff changeset
    74
  apply simp
Chengsong
parents: 456
diff changeset
    75
   apply (meson insert_iff)
Chengsong
parents: 456
diff changeset
    76
  apply simp
Chengsong
parents: 456
diff changeset
    77
  by (metis insertI1)
453
Chengsong
parents: 451
diff changeset
    78
Chengsong
parents: 451
diff changeset
    79
465
Chengsong
parents: 456
diff changeset
    80
lemma distinct_removes_middle3:
Chengsong
parents: 456
diff changeset
    81
  shows  "\<lbrakk>a \<in> set as\<rbrakk>
Chengsong
parents: 456
diff changeset
    82
    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
Chengsong
parents: 456
diff changeset
    83
  using distinct_removes_middle(1) by fastforce
Chengsong
parents: 456
diff changeset
    84
Chengsong
parents: 456
diff changeset
    85
lemma distinct_removes_last2:
Chengsong
parents: 456
diff changeset
    86
  shows "\<lbrakk>a \<in> set as\<rbrakk>
Chengsong
parents: 456
diff changeset
    87
    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
Chengsong
parents: 456
diff changeset
    88
  by (simp add: distinct_removes_last(1))
Chengsong
parents: 456
diff changeset
    89
Chengsong
parents: 456
diff changeset
    90
lemma distinct_removes_middle2:
Chengsong
parents: 456
diff changeset
    91
  shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
Chengsong
parents: 456
diff changeset
    92
  by (metis distinct_removes_middle(1))
Chengsong
parents: 456
diff changeset
    93
Chengsong
parents: 456
diff changeset
    94
lemma distinct_removes_list:
Chengsong
parents: 456
diff changeset
    95
  shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
Chengsong
parents: 456
diff changeset
    96
  apply(induct rs)
Chengsong
parents: 456
diff changeset
    97
   apply simp+
Chengsong
parents: 456
diff changeset
    98
  apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}")
Chengsong
parents: 456
diff changeset
    99
   prefer 2
Chengsong
parents: 456
diff changeset
   100
  apply (metis append_Cons append_Nil distinct_removes_middle(1))
Chengsong
parents: 456
diff changeset
   101
  by presburger
453
Chengsong
parents: 451
diff changeset
   102
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   103
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   104
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   105
lemma simp_rdistinct_f: shows 
465
Chengsong
parents: 456
diff changeset
   106
"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = 
Chengsong
parents: 456
diff changeset
   107
                      rsimp (rsimp_ALTs (rdistinct (map f rs) frset))  "
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   108
  apply(induct rs arbitrary: rset)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   109
   apply simp
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   110
   apply(case_tac "a \<in> rset")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   111
  apply(case_tac " f a \<in> frset")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   112
   apply simp
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   113
   apply blast
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   114
  apply(subgoal_tac "f a \<notin> frset")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   115
   apply(simp)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   116
   apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   117
  prefer 2
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   118
  apply (meson image_insert)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   119
  
453
Chengsong
parents: 451
diff changeset
   120
  oops
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
   121
453
Chengsong
parents: 451
diff changeset
   122
lemma spawn_simp_rsimpalts:
Chengsong
parents: 451
diff changeset
   123
  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
Chengsong
parents: 451
diff changeset
   124
  apply(cases rs)
Chengsong
parents: 451
diff changeset
   125
   apply simp
Chengsong
parents: 451
diff changeset
   126
  apply(case_tac list)
Chengsong
parents: 451
diff changeset
   127
   apply simp
Chengsong
parents: 451
diff changeset
   128
   apply(subst rsimp_idem[symmetric])
Chengsong
parents: 451
diff changeset
   129
   apply simp
Chengsong
parents: 451
diff changeset
   130
  apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
Chengsong
parents: 451
diff changeset
   131
   apply(simp only:)
Chengsong
parents: 451
diff changeset
   132
   apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
Chengsong
parents: 451
diff changeset
   133
    apply(simp only:)
Chengsong
parents: 451
diff changeset
   134
  prefer 2
Chengsong
parents: 451
diff changeset
   135
  apply simp
Chengsong
parents: 451
diff changeset
   136
   prefer 2
Chengsong
parents: 451
diff changeset
   137
  using rsimp_ALTs.simps(3) apply presburger
Chengsong
parents: 451
diff changeset
   138
  apply auto
Chengsong
parents: 451
diff changeset
   139
  apply(subst rsimp_idem)+
Chengsong
parents: 451
diff changeset
   140
  by (metis comp_apply rsimp_idem)
Chengsong
parents: 451
diff changeset
   141
Chengsong
parents: 451
diff changeset
   142
lemma spawn_simp_distinct:
Chengsong
parents: 451
diff changeset
   143
  shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))
Chengsong
parents: 451
diff changeset
   144
\<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))
Chengsong
parents: 451
diff changeset
   145
\<and> rsimp  (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"
Chengsong
parents: 451
diff changeset
   146
  apply(induct rs arbitrary: rsa rsa1 a1 rsc)
Chengsong
parents: 451
diff changeset
   147
   apply simp
Chengsong
parents: 451
diff changeset
   148
   apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")
Chengsong
parents: 451
diff changeset
   149
  prefer 2
Chengsong
parents: 451
diff changeset
   150
  
Chengsong
parents: 451
diff changeset
   151
Chengsong
parents: 451
diff changeset
   152
Chengsong
parents: 451
diff changeset
   153
Chengsong
parents: 451
diff changeset
   154
  oops
Chengsong
parents: 451
diff changeset
   155
Chengsong
parents: 451
diff changeset
   156
lemma inv_one_derx:
Chengsong
parents: 451
diff changeset
   157
  shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
Chengsong
parents: 451
diff changeset
   158
  apply(case_tac r2)
Chengsong
parents: 451
diff changeset
   159
       apply simp+
Chengsong
parents: 451
diff changeset
   160
  using rrexp.distinct(1) apply presburger
Chengsong
parents: 451
diff changeset
   161
    apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
Chengsong
parents: 451
diff changeset
   162
   apply simp+
Chengsong
parents: 451
diff changeset
   163
  done
Chengsong
parents: 451
diff changeset
   164
Chengsong
parents: 451
diff changeset
   165
lemma shape_of_derseq:
Chengsong
parents: 451
diff changeset
   166
  shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"
Chengsong
parents: 451
diff changeset
   167
  using rder.simps(5) by presburger
Chengsong
parents: 451
diff changeset
   168
lemma shape_of_derseq2:
Chengsong
parents: 451
diff changeset
   169
  shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"
Chengsong
parents: 451
diff changeset
   170
  by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)
Chengsong
parents: 451
diff changeset
   171
Chengsong
parents: 451
diff changeset
   172
lemma alts_preimage_case1:
Chengsong
parents: 451
diff changeset
   173
  shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"
Chengsong
parents: 451
diff changeset
   174
  apply(case_tac r)
Chengsong
parents: 451
diff changeset
   175
       apply simp+
Chengsong
parents: 451
diff changeset
   176
  apply (metis rrexp.simps(12) rrexp.simps(20))
Chengsong
parents: 451
diff changeset
   177
  apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)
Chengsong
parents: 451
diff changeset
   178
   apply auto[1]
Chengsong
parents: 451
diff changeset
   179
  by auto
Chengsong
parents: 451
diff changeset
   180
Chengsong
parents: 451
diff changeset
   181
lemma alts_preimage_case2:
Chengsong
parents: 451
diff changeset
   182
  shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"
Chengsong
parents: 451
diff changeset
   183
  apply(case_tac r)
Chengsong
parents: 451
diff changeset
   184
       apply simp+
Chengsong
parents: 451
diff changeset
   185
  apply (metis rrexp.distinct(15) rrexp.distinct(7))
Chengsong
parents: 451
diff changeset
   186
    apply simp
Chengsong
parents: 451
diff changeset
   187
  apply auto[1]
Chengsong
parents: 451
diff changeset
   188
  by auto
Chengsong
parents: 451
diff changeset
   189
Chengsong
parents: 451
diff changeset
   190
lemma alts_preimage_case2_2:
Chengsong
parents: 451
diff changeset
   191
  shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"
Chengsong
parents: 451
diff changeset
   192
  using alts_preimage_case2 by blast
Chengsong
parents: 451
diff changeset
   193
Chengsong
parents: 451
diff changeset
   194
lemma alts_preimage_case3:
Chengsong
parents: 451
diff changeset
   195
  shows "rder x r = RALT r1 r2 \<Longrightarrow>  (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"
Chengsong
parents: 451
diff changeset
   196
  using alts_preimage_case2 by blast
Chengsong
parents: 451
diff changeset
   197
Chengsong
parents: 451
diff changeset
   198
lemma star_seq:
Chengsong
parents: 451
diff changeset
   199
  shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"
Chengsong
parents: 451
diff changeset
   200
  using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger
Chengsong
parents: 451
diff changeset
   201
Chengsong
parents: 451
diff changeset
   202
lemma language_equality_id1:
Chengsong
parents: 451
diff changeset
   203
  shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"
Chengsong
parents: 451
diff changeset
   204
  apply (subst star_seq)
Chengsong
parents: 451
diff changeset
   205
  apply simp
Chengsong
parents: 451
diff changeset
   206
  done
Chengsong
parents: 451
diff changeset
   207
Chengsong
parents: 451
diff changeset
   208
Chengsong
parents: 451
diff changeset
   209
Chengsong
parents: 451
diff changeset
   210
lemma distinct_der_set:
Chengsong
parents: 451
diff changeset
   211
  shows "(rder x) ` rset = dset \<Longrightarrow>
Chengsong
parents: 451
diff changeset
   212
rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
Chengsong
parents: 451
diff changeset
   213
  apply(induct rs arbitrary: rset dset)
Chengsong
parents: 451
diff changeset
   214
   apply simp
Chengsong
parents: 451
diff changeset
   215
  apply(case_tac "a \<in> rset")
Chengsong
parents: 451
diff changeset
   216
   apply(subgoal_tac "rder x a \<in> dset")
Chengsong
parents: 451
diff changeset
   217
  prefer 2
Chengsong
parents: 451
diff changeset
   218
    apply blast
Chengsong
parents: 451
diff changeset
   219
   apply simp
Chengsong
parents: 451
diff changeset
   220
  apply(case_tac "rder x a \<notin> dset")
Chengsong
parents: 451
diff changeset
   221
   prefer 2
Chengsong
parents: 451
diff changeset
   222
   apply simp
Chengsong
parents: 451
diff changeset
   223
 
Chengsong
parents: 451
diff changeset
   224
  oops
Chengsong
parents: 451
diff changeset
   225
Chengsong
parents: 451
diff changeset
   226
lemma map_concat_cons:
Chengsong
parents: 451
diff changeset
   227
  shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
Chengsong
parents: 451
diff changeset
   228
  by simp
Chengsong
parents: 451
diff changeset
   229
Chengsong
parents: 451
diff changeset
   230
lemma neg_removal_element_of:
Chengsong
parents: 451
diff changeset
   231
  shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
Chengsong
parents: 451
diff changeset
   232
  by simp
Chengsong
parents: 451
diff changeset
   233
Chengsong
parents: 451
diff changeset
   234
lemma simp_more_flts:
Chengsong
parents: 451
diff changeset
   235
  shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))"
Chengsong
parents: 451
diff changeset
   236
Chengsong
parents: 451
diff changeset
   237
  oops
Chengsong
parents: 451
diff changeset
   238
465
Chengsong
parents: 456
diff changeset
   239
lemma simp_more_distinct1:
Chengsong
parents: 456
diff changeset
   240
  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))"
Chengsong
parents: 456
diff changeset
   241
  apply(induct rs)
Chengsong
parents: 456
diff changeset
   242
   apply simp
Chengsong
parents: 456
diff changeset
   243
  apply simp
Chengsong
parents: 456
diff changeset
   244
  oops
Chengsong
parents: 456
diff changeset
   245
Chengsong
parents: 456
diff changeset
   246
Chengsong
parents: 456
diff changeset
   247
(*
Chengsong
parents: 456
diff changeset
   248
\<and>
Chengsong
parents: 456
diff changeset
   249
  rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = 
Chengsong
parents: 456
diff changeset
   250
  rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))
Chengsong
parents: 456
diff changeset
   251
*)
Chengsong
parents: 456
diff changeset
   252
lemma simp_removes_duplicate2:
Chengsong
parents: 456
diff changeset
   253
  shows "a "
Chengsong
parents: 456
diff changeset
   254
Chengsong
parents: 456
diff changeset
   255
  oops
Chengsong
parents: 456
diff changeset
   256
Chengsong
parents: 456
diff changeset
   257
lemma flts_removes0:
Chengsong
parents: 456
diff changeset
   258
  shows "  rflts (rs @ [RZERO])  =
Chengsong
parents: 456
diff changeset
   259
           rflts rs"
Chengsong
parents: 456
diff changeset
   260
  apply(induct rs)
Chengsong
parents: 456
diff changeset
   261
   apply simp
Chengsong
parents: 456
diff changeset
   262
  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   263
  
Chengsong
parents: 456
diff changeset
   264
lemma flts_keeps1:
Chengsong
parents: 456
diff changeset
   265
  shows " rflts (rs @ [RONE]) = 
Chengsong
parents: 456
diff changeset
   266
          rflts  rs @ [RONE] "
Chengsong
parents: 456
diff changeset
   267
  apply (induct rs)
Chengsong
parents: 456
diff changeset
   268
   apply simp
Chengsong
parents: 456
diff changeset
   269
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   270
Chengsong
parents: 456
diff changeset
   271
lemma flts_keeps_others:
Chengsong
parents: 456
diff changeset
   272
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
Chengsong
parents: 456
diff changeset
   273
  apply(induct rs)
Chengsong
parents: 456
diff changeset
   274
   apply simp
Chengsong
parents: 456
diff changeset
   275
  apply (simp add: rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   276
  apply(case_tac a)
Chengsong
parents: 456
diff changeset
   277
       apply simp
Chengsong
parents: 456
diff changeset
   278
  using flts_keeps1 apply blast
Chengsong
parents: 456
diff changeset
   279
     apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   280
  apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   281
  apply blast
Chengsong
parents: 456
diff changeset
   282
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   283
Chengsong
parents: 456
diff changeset
   284
Chengsong
parents: 456
diff changeset
   285
lemma rflts_def_idiot2:
Chengsong
parents: 456
diff changeset
   286
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
Chengsong
parents: 456
diff changeset
   287
  apply(induct rs)
Chengsong
parents: 456
diff changeset
   288
   apply simp
Chengsong
parents: 456
diff changeset
   289
  by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   290
Chengsong
parents: 456
diff changeset
   291
lemma rflts_spills_last:
Chengsong
parents: 456
diff changeset
   292
  shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
Chengsong
parents: 456
diff changeset
   293
  apply (induct rs1)
Chengsong
parents: 456
diff changeset
   294
  apply simp
Chengsong
parents: 456
diff changeset
   295
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   296
Chengsong
parents: 456
diff changeset
   297
Chengsong
parents: 456
diff changeset
   298
lemma spilled_alts_contained:
Chengsong
parents: 456
diff changeset
   299
  shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
Chengsong
parents: 456
diff changeset
   300
  apply(induct rs1)
Chengsong
parents: 456
diff changeset
   301
   apply simp 
Chengsong
parents: 456
diff changeset
   302
  apply(case_tac "a = aa")
Chengsong
parents: 456
diff changeset
   303
   apply simp
Chengsong
parents: 456
diff changeset
   304
  apply(subgoal_tac " a \<in> set rs1")
Chengsong
parents: 456
diff changeset
   305
  prefer 2
Chengsong
parents: 456
diff changeset
   306
   apply (meson set_ConsD)
Chengsong
parents: 456
diff changeset
   307
  apply(case_tac aa)
Chengsong
parents: 456
diff changeset
   308
  using rflts.simps(2) apply presburger
Chengsong
parents: 456
diff changeset
   309
      apply fastforce
Chengsong
parents: 456
diff changeset
   310
  apply fastforce
Chengsong
parents: 456
diff changeset
   311
  apply fastforce
Chengsong
parents: 456
diff changeset
   312
  apply fastforce
Chengsong
parents: 456
diff changeset
   313
  by fastforce
Chengsong
parents: 456
diff changeset
   314
Chengsong
parents: 456
diff changeset
   315
lemma distinct_removes_duplicate_flts:
Chengsong
parents: 456
diff changeset
   316
  shows " a \<in> set rsa
Chengsong
parents: 456
diff changeset
   317
       \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
Chengsong
parents: 456
diff changeset
   318
           rdistinct (rflts (map rsimp rsa)) {}"
Chengsong
parents: 456
diff changeset
   319
  apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
Chengsong
parents: 456
diff changeset
   320
  prefer 2
Chengsong
parents: 456
diff changeset
   321
  apply simp
Chengsong
parents: 456
diff changeset
   322
  apply(induct "rsimp a")
Chengsong
parents: 456
diff changeset
   323
       apply simp
Chengsong
parents: 456
diff changeset
   324
  using flts_removes0 apply presburger
Chengsong
parents: 456
diff changeset
   325
      apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
Chengsong
parents: 456
diff changeset
   326
                          rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
Chengsong
parents: 456
diff changeset
   327
      apply (simp only:)
Chengsong
parents: 456
diff changeset
   328
       apply(subst flts_keeps1)
Chengsong
parents: 456
diff changeset
   329
  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
Chengsong
parents: 456
diff changeset
   330
      apply presburger
Chengsong
parents: 456
diff changeset
   331
        apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
Chengsong
parents: 456
diff changeset
   332
                            rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
Chengsong
parents: 456
diff changeset
   333
      apply (simp only:)
Chengsong
parents: 456
diff changeset
   334
      prefer 2
Chengsong
parents: 456
diff changeset
   335
      apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
Chengsong
parents: 456
diff changeset
   336
  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
Chengsong
parents: 456
diff changeset
   337
Chengsong
parents: 456
diff changeset
   338
    apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
Chengsong
parents: 456
diff changeset
   339
   prefer 2
Chengsong
parents: 456
diff changeset
   340
   apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
Chengsong
parents: 456
diff changeset
   341
  apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
Chengsong
parents: 456
diff changeset
   342
  prefer 2
Chengsong
parents: 456
diff changeset
   343
  apply (simp add: rflts_spills_last)
Chengsong
parents: 456
diff changeset
   344
  apply(simp only:)
Chengsong
parents: 456
diff changeset
   345
  apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
Chengsong
parents: 456
diff changeset
   346
  prefer 2
Chengsong
parents: 456
diff changeset
   347
  using spilled_alts_contained apply presburger
Chengsong
parents: 456
diff changeset
   348
  by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust)
Chengsong
parents: 456
diff changeset
   349
Chengsong
parents: 456
diff changeset
   350
lemma flts_middle0:
Chengsong
parents: 456
diff changeset
   351
  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
Chengsong
parents: 456
diff changeset
   352
  apply(induct rsa)
Chengsong
parents: 456
diff changeset
   353
  apply simp
Chengsong
parents: 456
diff changeset
   354
  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
Chengsong
parents: 456
diff changeset
   355
Chengsong
parents: 456
diff changeset
   356
lemma flts_middle01:
Chengsong
parents: 456
diff changeset
   357
  shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
Chengsong
parents: 456
diff changeset
   358
  by (simp add: flts_middle0)
Chengsong
parents: 456
diff changeset
   359
Chengsong
parents: 456
diff changeset
   360
lemma flts_append1:
Chengsong
parents: 456
diff changeset
   361
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk>  \<Longrightarrow>
Chengsong
parents: 456
diff changeset
   362
         rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)"
Chengsong
parents: 456
diff changeset
   363
  apply(induct rsa arbitrary: rsb)
Chengsong
parents: 456
diff changeset
   364
   apply simp
Chengsong
parents: 456
diff changeset
   365
  using rflts_def_idiot apply presburger
Chengsong
parents: 456
diff changeset
   366
  apply(case_tac aa)  
Chengsong
parents: 456
diff changeset
   367
       apply simp+
Chengsong
parents: 456
diff changeset
   368
  done
Chengsong
parents: 456
diff changeset
   369
Chengsong
parents: 456
diff changeset
   370
lemma flts_append:
Chengsong
parents: 456
diff changeset
   371
  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
Chengsong
parents: 456
diff changeset
   372
  apply(induct rs1)
Chengsong
parents: 456
diff changeset
   373
   apply simp
Chengsong
parents: 456
diff changeset
   374
  apply(case_tac a)
Chengsong
parents: 456
diff changeset
   375
       apply simp+
Chengsong
parents: 456
diff changeset
   376
  done
Chengsong
parents: 456
diff changeset
   377
Chengsong
parents: 456
diff changeset
   378
lemma simp_removes_duplicate1:
Chengsong
parents: 456
diff changeset
   379
  shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
Chengsong
parents: 456
diff changeset
   380
and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
Chengsong
parents: 456
diff changeset
   381
  apply(induct rsa arbitrary: a1)
Chengsong
parents: 456
diff changeset
   382
     apply simp
Chengsong
parents: 456
diff changeset
   383
    apply simp
Chengsong
parents: 456
diff changeset
   384
  prefer 2
Chengsong
parents: 456
diff changeset
   385
  apply(case_tac "a = aa")
Chengsong
parents: 456
diff changeset
   386
     apply simp
Chengsong
parents: 456
diff changeset
   387
    apply simp
Chengsong
parents: 456
diff changeset
   388
  apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
Chengsong
parents: 456
diff changeset
   389
  apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
Chengsong
parents: 456
diff changeset
   390
  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))
Chengsong
parents: 456
diff changeset
   391
  
Chengsong
parents: 456
diff changeset
   392
lemma simp_removes_duplicate2:
Chengsong
parents: 456
diff changeset
   393
  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
Chengsong
parents: 456
diff changeset
   394
  apply(induct rsb arbitrary: rsa)
Chengsong
parents: 456
diff changeset
   395
   apply simp
Chengsong
parents: 456
diff changeset
   396
  using distinct_removes_duplicate_flts apply auto[1]
Chengsong
parents: 456
diff changeset
   397
  by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
Chengsong
parents: 456
diff changeset
   398
Chengsong
parents: 456
diff changeset
   399
lemma simp_removes_duplicate3:
Chengsong
parents: 456
diff changeset
   400
  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
Chengsong
parents: 456
diff changeset
   401
  using simp_removes_duplicate2 by auto
Chengsong
parents: 456
diff changeset
   402
Chengsong
parents: 456
diff changeset
   403
lemma distinct_removes_middle4:
Chengsong
parents: 456
diff changeset
   404
  shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
Chengsong
parents: 456
diff changeset
   405
  using distinct_removes_middle(1) by fastforce
Chengsong
parents: 456
diff changeset
   406
Chengsong
parents: 456
diff changeset
   407
lemma distinct_removes_middle_list:
Chengsong
parents: 456
diff changeset
   408
  shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
Chengsong
parents: 456
diff changeset
   409
  apply(induct x)
Chengsong
parents: 456
diff changeset
   410
   apply simp
Chengsong
parents: 456
diff changeset
   411
  by (simp add: distinct_removes_middle3)
Chengsong
parents: 456
diff changeset
   412
Chengsong
parents: 456
diff changeset
   413
Chengsong
parents: 456
diff changeset
   414
lemma distinct_removes_duplicate_flts2:
Chengsong
parents: 456
diff changeset
   415
  shows " a \<in> set rsa
Chengsong
parents: 456
diff changeset
   416
       \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} =
Chengsong
parents: 456
diff changeset
   417
           rdistinct (rflts (rsa @ rsb)) {}"
Chengsong
parents: 456
diff changeset
   418
  apply(induct a arbitrary: rsb)
Chengsong
parents: 456
diff changeset
   419
  using flts_middle01 apply presburger
Chengsong
parents: 456
diff changeset
   420
      apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb")
Chengsong
parents: 456
diff changeset
   421
  prefer 2
Chengsong
parents: 456
diff changeset
   422
  using flts_append1 apply blast
Chengsong
parents: 456
diff changeset
   423
      apply simp
Chengsong
parents: 456
diff changeset
   424
      apply(subgoal_tac "RONE \<in> set (rflts rsa)")
Chengsong
parents: 456
diff changeset
   425
  prefer 2
Chengsong
parents: 456
diff changeset
   426
  using rflts_def_idiot2 apply blast
Chengsong
parents: 456
diff changeset
   427
      apply(subst distinct_removes_middle3)
Chengsong
parents: 456
diff changeset
   428
       apply simp
Chengsong
parents: 456
diff changeset
   429
  using flts_append apply presburger
Chengsong
parents: 456
diff changeset
   430
     apply simp
Chengsong
parents: 456
diff changeset
   431
  apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5))
Chengsong
parents: 456
diff changeset
   432
  apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
Chengsong
parents: 456
diff changeset
   433
   apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb")
Chengsong
parents: 456
diff changeset
   434
    prefer 2
Chengsong
parents: 456
diff changeset
   435
  apply (simp add: flts_append)
Chengsong
parents: 456
diff changeset
   436
   apply (simp only:)
Chengsong
parents: 456
diff changeset
   437
Chengsong
parents: 456
diff changeset
   438
   apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)")
Chengsong
parents: 456
diff changeset
   439
    prefer 2
Chengsong
parents: 456
diff changeset
   440
  using spilled_alts_contained apply blast
Chengsong
parents: 456
diff changeset
   441
  apply(subst flts_append)
Chengsong
parents: 456
diff changeset
   442
  using distinct_removes_middle_list apply blast
Chengsong
parents: 456
diff changeset
   443
  using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce
Chengsong
parents: 456
diff changeset
   444
Chengsong
parents: 456
diff changeset
   445
Chengsong
parents: 456
diff changeset
   446
lemma simp_removes_duplicate:
Chengsong
parents: 456
diff changeset
   447
  shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) =  rsimp (rsimp_ALTs (rsa @ rs))"
Chengsong
parents: 456
diff changeset
   448
  apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))")
Chengsong
parents: 456
diff changeset
   449
   prefer 2
Chengsong
parents: 456
diff changeset
   450
  apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims)
Chengsong
parents: 456
diff changeset
   451
  apply(simp only:)
Chengsong
parents: 456
diff changeset
   452
  apply simp
Chengsong
parents: 456
diff changeset
   453
  apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @  map rsimp rs)) {})")
Chengsong
parents: 456
diff changeset
   454
   apply(simp only:)
Chengsong
parents: 456
diff changeset
   455
  prefer 2
Chengsong
parents: 456
diff changeset
   456
   apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
Chengsong
parents: 456
diff changeset
   457
    prefer 2
Chengsong
parents: 456
diff changeset
   458
  apply simp
Chengsong
parents: 456
diff changeset
   459
  using distinct_removes_duplicate_flts2 apply force
Chengsong
parents: 456
diff changeset
   460
  apply(case_tac rsa)
Chengsong
parents: 456
diff changeset
   461
   apply simp
Chengsong
parents: 456
diff changeset
   462
  apply(case_tac rs)
Chengsong
parents: 456
diff changeset
   463
   apply simp
Chengsong
parents: 456
diff changeset
   464
   apply(case_tac list)
Chengsong
parents: 456
diff changeset
   465
    apply simp
Chengsong
parents: 456
diff changeset
   466
  using idem_after_simp1 apply presburger
Chengsong
parents: 456
diff changeset
   467
   apply simp+
Chengsong
parents: 456
diff changeset
   468
  apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")
Chengsong
parents: 456
diff changeset
   469
   apply simp
Chengsong
parents: 456
diff changeset
   470
  using rsimpalts_conscons by presburger
467
Chengsong
parents: 465
diff changeset
   471
468
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   472
lemma no0_flts:
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   473
  shows "RZERO \<notin> set (rflts rs)"
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   474
  apply (induct rs)
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   475
   apply simp
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   476
  apply(case_tac a)
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   477
       apply simp+
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   478
  oops
467
Chengsong
parents: 465
diff changeset
   479
Chengsong
parents: 465
diff changeset
   480
Chengsong
parents: 465
diff changeset
   481
Chengsong
parents: 465
diff changeset
   482
lemma distinct_flts_no0:
468
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   483
  shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   484
           rflts (map rsimp (rdistinct rs rset))  "
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   485
  
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   486
  apply(induct rs arbitrary: rset)
467
Chengsong
parents: 465
diff changeset
   487
   apply simp
Chengsong
parents: 465
diff changeset
   488
  apply(case_tac a)
468
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   489
  apply simp+
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   490
    apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   491
  prefer 2
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   492
  apply simp  
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   493
  by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7))
a0f27e21b42c all texrelated
Chengsong
parents: 467
diff changeset
   494
467
Chengsong
parents: 465
diff changeset
   495
Chengsong
parents: 465
diff changeset
   496
471
Chengsong
parents: 469
diff changeset
   497
Chengsong
parents: 469
diff changeset
   498
inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
Chengsong
parents: 469
diff changeset
   499
  where
Chengsong
parents: 469
diff changeset
   500
  "(RZERO # rs) \<leadsto>f rs"
Chengsong
parents: 469
diff changeset
   501
| "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"
Chengsong
parents: 469
diff changeset
   502
| "rs1 \<leadsto>f rs2 \<Longrightarrow> (r # rs1) \<leadsto>f (r # rs2)"
Chengsong
parents: 469
diff changeset
   503
Chengsong
parents: 469
diff changeset
   504
Chengsong
parents: 469
diff changeset
   505
inductive 
Chengsong
parents: 469
diff changeset
   506
  frewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f* _" [10, 10] 10)
Chengsong
parents: 469
diff changeset
   507
where 
473
Chengsong
parents: 472
diff changeset
   508
  [intro, simp]:"rs \<leadsto>f* rs"
Chengsong
parents: 472
diff changeset
   509
| [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"
Chengsong
parents: 472
diff changeset
   510
Chengsong
parents: 472
diff changeset
   511
inductive grewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g _" [10, 10] 10)
Chengsong
parents: 472
diff changeset
   512
  where
Chengsong
parents: 472
diff changeset
   513
  "(RZERO # rs) \<leadsto>g rs"
Chengsong
parents: 472
diff changeset
   514
| "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"
Chengsong
parents: 472
diff changeset
   515
| "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
Chengsong
parents: 472
diff changeset
   516
| "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 
Chengsong
parents: 472
diff changeset
   517
Chengsong
parents: 472
diff changeset
   518
Chengsong
parents: 472
diff changeset
   519
inductive 
Chengsong
parents: 472
diff changeset
   520
  grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)
Chengsong
parents: 472
diff changeset
   521
where 
Chengsong
parents: 472
diff changeset
   522
  [intro, simp]:"rs \<leadsto>g* rs"
Chengsong
parents: 472
diff changeset
   523
| [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"
Chengsong
parents: 472
diff changeset
   524
(*
Chengsong
parents: 472
diff changeset
   525
inductive 
Chengsong
parents: 472
diff changeset
   526
  frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)
Chengsong
parents: 472
diff changeset
   527
where 
Chengsong
parents: 472
diff changeset
   528
 [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"
Chengsong
parents: 472
diff changeset
   529
*)
471
Chengsong
parents: 469
diff changeset
   530
Chengsong
parents: 469
diff changeset
   531
lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"
Chengsong
parents: 469
diff changeset
   532
  using frewrites.intros(1) frewrites.intros(2) by blast
Chengsong
parents: 469
diff changeset
   533
 
Chengsong
parents: 469
diff changeset
   534
lemma freal_trans[trans]: 
Chengsong
parents: 469
diff changeset
   535
  assumes a1: "r1 \<leadsto>f* r2"  and a2: "r2 \<leadsto>f* r3"
Chengsong
parents: 469
diff changeset
   536
  shows "r1 \<leadsto>f* r3"
Chengsong
parents: 469
diff changeset
   537
  using a2 a1
Chengsong
parents: 469
diff changeset
   538
  apply(induct r2 r3 arbitrary: r1 rule: frewrites.induct) 
Chengsong
parents: 469
diff changeset
   539
  apply(auto)
Chengsong
parents: 469
diff changeset
   540
  done
Chengsong
parents: 469
diff changeset
   541
Chengsong
parents: 469
diff changeset
   542
Chengsong
parents: 469
diff changeset
   543
lemma  many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3"
Chengsong
parents: 469
diff changeset
   544
  by (meson fr_in_rstar freal_trans)
Chengsong
parents: 469
diff changeset
   545
Chengsong
parents: 469
diff changeset
   546
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   547
lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   548
  using grewrites.intros(1) grewrites.intros(2) by blast
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   549
 
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   550
lemma greal_trans[trans]: 
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   551
  assumes a1: "r1 \<leadsto>g* r2"  and a2: "r2 \<leadsto>g* r3"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   552
  shows "r1 \<leadsto>g* r3"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   553
  using a2 a1
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   554
  apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct) 
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   555
  apply(auto)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   556
  done
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   557
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   558
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   559
lemma  gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   560
  by (meson gr_in_rstar greal_trans)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   561
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   562
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   563
471
Chengsong
parents: 469
diff changeset
   564
lemma frewrite_append:
Chengsong
parents: 469
diff changeset
   565
  shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
Chengsong
parents: 469
diff changeset
   566
  apply(induct rs)
472
Chengsong
parents: 471
diff changeset
   567
   apply simp+
Chengsong
parents: 471
diff changeset
   568
  using frewrite.intros(3) by blast
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   569
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   570
lemma grewrite_append:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   571
  shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   572
  apply(induct rs)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   573
   apply simp+
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   574
  using grewrite.intros(3) by blast
472
Chengsong
parents: 471
diff changeset
   575
  
471
Chengsong
parents: 469
diff changeset
   576
Chengsong
parents: 469
diff changeset
   577
Chengsong
parents: 469
diff changeset
   578
lemma frewrites_cons:
Chengsong
parents: 469
diff changeset
   579
  shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"
472
Chengsong
parents: 471
diff changeset
   580
  apply(induct rsa rsb rule: frewrites.induct)
Chengsong
parents: 471
diff changeset
   581
   apply simp
Chengsong
parents: 471
diff changeset
   582
  using frewrite.intros(3) by blast
471
Chengsong
parents: 469
diff changeset
   583
Chengsong
parents: 469
diff changeset
   584
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   585
lemma grewrites_cons:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   586
  shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   587
  apply(induct rsa rsb rule: grewrites.induct)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   588
   apply simp
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   589
  using grewrite.intros(3) by blast
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   590
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   591
471
Chengsong
parents: 469
diff changeset
   592
lemma frewrites_append:
Chengsong
parents: 469
diff changeset
   593
  shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"
472
Chengsong
parents: 471
diff changeset
   594
  apply(induct rs)
471
Chengsong
parents: 469
diff changeset
   595
   apply simp
472
Chengsong
parents: 471
diff changeset
   596
  by (simp add: frewrites_cons)
471
Chengsong
parents: 469
diff changeset
   597
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   598
lemma grewrites_append:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   599
  shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   600
  apply(induct rs)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   601
   apply simp
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   602
  by (simp add: grewrites_cons)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   603
471
Chengsong
parents: 469
diff changeset
   604
Chengsong
parents: 469
diff changeset
   605
Chengsong
parents: 469
diff changeset
   606
lemma frewrites_concat:
Chengsong
parents: 469
diff changeset
   607
  shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)"
Chengsong
parents: 469
diff changeset
   608
  apply(induct rs1 rs2 rule: frewrite.induct)
Chengsong
parents: 469
diff changeset
   609
    apply(simp)
Chengsong
parents: 469
diff changeset
   610
  apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)")
Chengsong
parents: 469
diff changeset
   611
  prefer 2
Chengsong
parents: 469
diff changeset
   612
  using frewrite.intros(1) apply blast
Chengsong
parents: 469
diff changeset
   613
    apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)")
Chengsong
parents: 469
diff changeset
   614
  using many_steps_later apply blast
472
Chengsong
parents: 471
diff changeset
   615
  apply (simp add: frewrites_append)
Chengsong
parents: 471
diff changeset
   616
  apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)
Chengsong
parents: 471
diff changeset
   617
  using frewrites_cons by auto
471
Chengsong
parents: 469
diff changeset
   618
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   619
lemma grewrites_concat:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   620
  shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   621
  apply(induct rs1 rs2 rule: grewrite.induct)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   622
    apply(simp)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   623
  apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)")
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   624
  prefer 2
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   625
  using grewrite.intros(1) apply blast
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   626
    apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)")
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   627
  using gmany_steps_later apply blast
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   628
  apply (simp add: grewrites_append)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   629
  apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   630
  using grewrites_cons apply auto
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   631
  apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb")
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   632
  using grewrite.intros(4) grewrites.intros(2) apply force
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   633
  using grewrites_append by auto
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   634
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   635
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   636
lemma grewritess_concat:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   637
  shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   638
  apply(induct rsa rsb rule: grewrites.induct)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   639
   apply(case_tac rs)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   640
    apply simp
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   641
  using grewrites_append apply blast   
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   642
  by (meson greal_trans grewrites.simps grewrites_concat)
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   643
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   644
lemma grewrites_equal_rsimp:
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   645
  shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   646
  apply simp
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   647
  sorry
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   648
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   649
473
Chengsong
parents: 472
diff changeset
   650
lemma frewrites_middle:
Chengsong
parents: 472
diff changeset
   651
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"
Chengsong
parents: 472
diff changeset
   652
  by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3))
471
Chengsong
parents: 469
diff changeset
   653
473
Chengsong
parents: 472
diff changeset
   654
lemma frewrites_alt:
Chengsong
parents: 472
diff changeset
   655
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"  
Chengsong
parents: 472
diff changeset
   656
  by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)
471
Chengsong
parents: 469
diff changeset
   657
Chengsong
parents: 469
diff changeset
   658
lemma early_late_der_frewrites:
Chengsong
parents: 469
diff changeset
   659
  shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"
Chengsong
parents: 469
diff changeset
   660
  apply(induct rs)
Chengsong
parents: 469
diff changeset
   661
   apply simp
Chengsong
parents: 469
diff changeset
   662
  apply(case_tac a)
Chengsong
parents: 469
diff changeset
   663
       apply simp+
Chengsong
parents: 469
diff changeset
   664
  using frewrite.intros(1) many_steps_later apply blast
Chengsong
parents: 469
diff changeset
   665
     apply(case_tac "x = x3")
472
Chengsong
parents: 471
diff changeset
   666
      apply simp
Chengsong
parents: 471
diff changeset
   667
  using frewrites_cons apply presburger
Chengsong
parents: 471
diff changeset
   668
  using frewrite.intros(1) many_steps_later apply fastforce
Chengsong
parents: 471
diff changeset
   669
  apply(case_tac "rnullable x41")
473
Chengsong
parents: 472
diff changeset
   670
     apply simp+
Chengsong
parents: 472
diff changeset
   671
     apply (simp add: frewrites_alt)
Chengsong
parents: 472
diff changeset
   672
  apply (simp add: frewrites_cons)
Chengsong
parents: 472
diff changeset
   673
   apply (simp add: frewrites_append)
Chengsong
parents: 472
diff changeset
   674
  by (simp add: frewrites_cons)
471
Chengsong
parents: 469
diff changeset
   675
Chengsong
parents: 469
diff changeset
   676
Chengsong
parents: 469
diff changeset
   677
fun alt_set:: "rrexp \<Rightarrow> rrexp set"
Chengsong
parents: 469
diff changeset
   678
  where
Chengsong
parents: 469
diff changeset
   679
  "alt_set (RALTS rs) = set rs"
Chengsong
parents: 469
diff changeset
   680
| "alt_set r = {r}"
Chengsong
parents: 469
diff changeset
   681
Chengsong
parents: 469
diff changeset
   682
Chengsong
parents: 469
diff changeset
   683
Chengsong
parents: 469
diff changeset
   684
lemma rd_flts_set:
475
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   685
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union>  (rset \<union>  \<Union>(alt_set ` rset))) \<leadsto>g* 
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   686
                          rdistinct rs2 ({RZERO} \<union>  (rset \<union>  \<Union>(alt_set ` rset)))"
10fd25fba2ba identities
Chengsong
parents: 473
diff changeset
   687
  sorry
471
Chengsong
parents: 469
diff changeset
   688
473
Chengsong
parents: 472
diff changeset
   689
lemma with_wo0_distinct:
Chengsong
parents: 472
diff changeset
   690
  shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
Chengsong
parents: 472
diff changeset
   691
  apply(induct rs arbitrary: rset)
Chengsong
parents: 472
diff changeset
   692
   apply simp
Chengsong
parents: 472
diff changeset
   693
  apply(case_tac a)
Chengsong
parents: 472
diff changeset
   694
  apply(case_tac "RZERO \<in> rset")
Chengsong
parents: 472
diff changeset
   695
        apply simp+
Chengsong
parents: 472
diff changeset
   696
  using fr_in_rstar frewrite.intros(1) apply presburger
Chengsong
parents: 472
diff changeset
   697
  apply (case_tac "RONE \<in> rset")
Chengsong
parents: 472
diff changeset
   698
       apply simp+
Chengsong
parents: 472
diff changeset
   699
  using frewrites_cons apply presburger
Chengsong
parents: 472
diff changeset
   700
     apply(case_tac "a \<in> rset")
Chengsong
parents: 472
diff changeset
   701
  apply simp
Chengsong
parents: 472
diff changeset
   702
  apply (simp add: frewrites_cons)
Chengsong
parents: 472
diff changeset
   703
     apply(case_tac "a \<in> rset")
Chengsong
parents: 472
diff changeset
   704
  apply simp
Chengsong
parents: 472
diff changeset
   705
  apply (simp add: frewrites_cons)
Chengsong
parents: 472
diff changeset
   706
       apply(case_tac "a \<in> rset")
Chengsong
parents: 472
diff changeset
   707
  apply simp
Chengsong
parents: 472
diff changeset
   708
  apply (simp add: frewrites_cons)
Chengsong
parents: 472
diff changeset
   709
       apply(case_tac "a \<in> rset")
Chengsong
parents: 472
diff changeset
   710
  apply simp
Chengsong
parents: 472
diff changeset
   711
  apply (simp add: frewrites_cons)
Chengsong
parents: 472
diff changeset
   712
  done
Chengsong
parents: 472
diff changeset
   713
Chengsong
parents: 472
diff changeset
   714
Chengsong
parents: 472
diff changeset
   715
lemma frewrite_with_distinct:
Chengsong
parents: 472
diff changeset
   716
  shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>
Chengsong
parents: 472
diff changeset
   717
       \<Longrightarrow> rdistinct rs2
Chengsong
parents: 472
diff changeset
   718
            (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* 
Chengsong
parents: 472
diff changeset
   719
           rdistinct rs3 
Chengsong
parents: 472
diff changeset
   720
            (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
Chengsong
parents: 472
diff changeset
   721
  apply(induct rs2 rs3 rule: frewrite.induct)
Chengsong
parents: 472
diff changeset
   722
    apply(case_tac "RZERO \<in>  (rset \<union> \<Union> (alt_set ` rset))")
Chengsong
parents: 472
diff changeset
   723
  apply simp
Chengsong
parents: 472
diff changeset
   724
    apply simp
Chengsong
parents: 472
diff changeset
   725
   apply(case_tac "RALTS rs \<in> rset")
Chengsong
parents: 472
diff changeset
   726
    apply simp
Chengsong
parents: 472
diff changeset
   727
  apply(subgoal_tac "\<forall>r \<in> set rs. r \<in> \<Union> (alt_set ` rset)")
Chengsong
parents: 472
diff changeset
   728
  apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) = 
Chengsong
parents: 472
diff changeset
   729
                       rdistinct rsa (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))")
Chengsong
parents: 472
diff changeset
   730
  using frewrites.intros(1) apply presburger
Chengsong
parents: 472
diff changeset
   731
     apply (simp add: rdistinct_concat2)
Chengsong
parents: 472
diff changeset
   732
    apply simp
Chengsong
parents: 472
diff changeset
   733
  using alt_set.simps(1) apply blast
Chengsong
parents: 472
diff changeset
   734
   apply(case_tac "RALTS rs \<in> rset \<union> \<Union>(alt_set ` rset)")
Chengsong
parents: 472
diff changeset
   735
  
Chengsong
parents: 472
diff changeset
   736
469
e5dd8cc0aa82 all electron pics removed
Chengsong
parents: 468
diff changeset
   737
  sorry
e5dd8cc0aa82 all electron pics removed
Chengsong
parents: 468
diff changeset
   738
e5dd8cc0aa82 all electron pics removed
Chengsong
parents: 468
diff changeset
   739
473
Chengsong
parents: 472
diff changeset
   740
lemma frewrites_with_distinct:
Chengsong
parents: 472
diff changeset
   741
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
Chengsong
parents: 472
diff changeset
   742
 rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>f* 
Chengsong
parents: 472
diff changeset
   743
 rs2 @ (rdistinct rsb (insert RZERO (set rs2 \<union> \<Union>(alt_set ` (set rs2) ))))"
Chengsong
parents: 472
diff changeset
   744
  apply(induct rs1 rs2 rule: frewrites.induct)
Chengsong
parents: 472
diff changeset
   745
   apply simp
Chengsong
parents: 472
diff changeset
   746
  
Chengsong
parents: 472
diff changeset
   747
Chengsong
parents: 472
diff changeset
   748
  sorry
Chengsong
parents: 472
diff changeset
   749
Chengsong
parents: 472
diff changeset
   750
(*a more refined notion of \<leadsto>* is needed,
Chengsong
parents: 472
diff changeset
   751
this lemma fails when rs1 contains some RALTS rs where elements
Chengsong
parents: 472
diff changeset
   752
of rs appear in later parts of rs1, which will be picked up by rs2
Chengsong
parents: 472
diff changeset
   753
and deduplicated*)
Chengsong
parents: 472
diff changeset
   754
lemma wrong_frewrites_with_distinct2:
Chengsong
parents: 472
diff changeset
   755
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
Chengsong
parents: 472
diff changeset
   756
 (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}"
Chengsong
parents: 472
diff changeset
   757
  oops
Chengsong
parents: 472
diff changeset
   758
Chengsong
parents: 472
diff changeset
   759
lemma frewrite_single_step:
Chengsong
parents: 472
diff changeset
   760
  shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
Chengsong
parents: 472
diff changeset
   761
  apply(induct rs2 rs3 rule: frewrite.induct)
Chengsong
parents: 472
diff changeset
   762
    apply simp
Chengsong
parents: 472
diff changeset
   763
  using simp_flatten apply blast
Chengsong
parents: 472
diff changeset
   764
  by (metis (no_types, opaque_lifting) list.simps(9) rsimp.simps(2) simp_flatten2)
Chengsong
parents: 472
diff changeset
   765
Chengsong
parents: 472
diff changeset
   766
lemma frewrites_equivalent_simp:
Chengsong
parents: 472
diff changeset
   767
  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
Chengsong
parents: 472
diff changeset
   768
  apply(induct rs1 rs2 rule: frewrites.induct)
Chengsong
parents: 472
diff changeset
   769
   apply simp
Chengsong
parents: 472
diff changeset
   770
  using frewrite_single_step by presburger
Chengsong
parents: 472
diff changeset
   771
Chengsong
parents: 472
diff changeset
   772
lemma frewrites_dB_wwo0_simp:
Chengsong
parents: 472
diff changeset
   773
  shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO} 
Chengsong
parents: 472
diff changeset
   774
         \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
Chengsong
parents: 472
diff changeset
   775
Chengsong
parents: 472
diff changeset
   776
  sorry
Chengsong
parents: 472
diff changeset
   777
Chengsong
parents: 472
diff changeset
   778
Chengsong
parents: 472
diff changeset
   779
467
Chengsong
parents: 465
diff changeset
   780
lemma simp_der_flts:
471
Chengsong
parents: 469
diff changeset
   781
  shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
Chengsong
parents: 469
diff changeset
   782
         rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
473
Chengsong
parents: 472
diff changeset
   783
  apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
Chengsong
parents: 472
diff changeset
   784
   apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} 
Chengsong
parents: 472
diff changeset
   785
                    \<leadsto>f* rdistinct ( rflts (map (rder x) rs)) {RZERO}")
Chengsong
parents: 472
diff changeset
   786
  apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) 
Chengsong
parents: 472
diff changeset
   787
                   = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))")
Chengsong
parents: 472
diff changeset
   788
  apply meson
Chengsong
parents: 472
diff changeset
   789
  using frewrites_dB_wwo0_simp apply blast
Chengsong
parents: 472
diff changeset
   790
  using frewrites_with_distinct2 apply blast
Chengsong
parents: 472
diff changeset
   791
  using early_late_der_frewrites by blast
467
Chengsong
parents: 465
diff changeset
   792
Chengsong
parents: 465
diff changeset
   793
465
Chengsong
parents: 456
diff changeset
   794
lemma simp_der_pierce_flts:
471
Chengsong
parents: 469
diff changeset
   795
  shows " rsimp (
Chengsong
parents: 469
diff changeset
   796
rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
Chengsong
parents: 469
diff changeset
   797
) =
Chengsong
parents: 469
diff changeset
   798
          rsimp (
Chengsong
parents: 469
diff changeset
   799
rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
Chengsong
parents: 469
diff changeset
   800
)"
Chengsong
parents: 469
diff changeset
   801
  
467
Chengsong
parents: 465
diff changeset
   802
  sorry
Chengsong
parents: 465
diff changeset
   803
465
Chengsong
parents: 456
diff changeset
   804
453
Chengsong
parents: 451
diff changeset
   805
Chengsong
parents: 451
diff changeset
   806
Chengsong
parents: 451
diff changeset
   807
lemma simp_more_distinct:
465
Chengsong
parents: 456
diff changeset
   808
  shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
467
Chengsong
parents: 465
diff changeset
   809
  
Chengsong
parents: 465
diff changeset
   810
465
Chengsong
parents: 456
diff changeset
   811
453
Chengsong
parents: 451
diff changeset
   812
Chengsong
parents: 451
diff changeset
   813
  sorry
Chengsong
parents: 451
diff changeset
   814
Chengsong
parents: 451
diff changeset
   815
lemma non_empty_list:
Chengsong
parents: 451
diff changeset
   816
  shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
Chengsong
parents: 451
diff changeset
   817
  by (metis empty_iff empty_set)
Chengsong
parents: 451
diff changeset
   818
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   819
lemma distinct_comp:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   820
  shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   821
  apply(induct rs2 arbitrary: rs1)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   822
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   823
  apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   824
   apply(simp only:)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   825
   apply(case_tac "a \<in> set rs1")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   826
    apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   827
  oops
453
Chengsong
parents: 451
diff changeset
   828
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   829
lemma instantiate1:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   830
  shows "\<lbrakk>\<And>ab rset1.  rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow>  
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   831
rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   832
  apply(drule_tac x = "aa" in meta_spec)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   833
  apply(drule_tac x = "rset" in meta_spec)
453
Chengsong
parents: 451
diff changeset
   834
  apply simp
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   835
  done
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   836
  
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   837
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   838
lemma not_head_elem:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   839
  shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   840
  
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   841
  by fastforce
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   842
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   843
(*
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   844
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   845
  apply (metis append_Cons)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   846
  apply(case_tac "ab \<in> rset1")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   847
  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   848
  apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 = 
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   849
               ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   850
   apply(simp only:)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   851
   apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   852
  apply(simp only:)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   853
    apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   854
  apply blast
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   855
*)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   856
  
453
Chengsong
parents: 451
diff changeset
   857
Chengsong
parents: 451
diff changeset
   858
lemma flts_identity1:
Chengsong
parents: 451
diff changeset
   859
  shows  "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
Chengsong
parents: 451
diff changeset
   860
  apply(induct rs)
Chengsong
parents: 451
diff changeset
   861
   apply simp+
Chengsong
parents: 451
diff changeset
   862
  apply(case_tac a)
Chengsong
parents: 451
diff changeset
   863
       apply simp
Chengsong
parents: 451
diff changeset
   864
      apply simp+
Chengsong
parents: 451
diff changeset
   865
  done
Chengsong
parents: 451
diff changeset
   866
Chengsong
parents: 451
diff changeset
   867
lemma flts_identity10:
Chengsong
parents: 451
diff changeset
   868
  shows " rflts (rs @ [RCHAR c]) = rflts rs @ [RCHAR c]"
Chengsong
parents: 451
diff changeset
   869
  apply(induct rs)
Chengsong
parents: 451
diff changeset
   870
   apply simp+
Chengsong
parents: 451
diff changeset
   871
  apply(case_tac a)
Chengsong
parents: 451
diff changeset
   872
       apply simp+
Chengsong
parents: 451
diff changeset
   873
  done
Chengsong
parents: 451
diff changeset
   874
Chengsong
parents: 451
diff changeset
   875
lemma flts_identity11:
Chengsong
parents: 451
diff changeset
   876
  shows " rflts (rs @ [RSEQ r1 r2]) = rflts rs @ [RSEQ r1 r2]"
Chengsong
parents: 451
diff changeset
   877
  apply(induct rs)
Chengsong
parents: 451
diff changeset
   878
   apply simp+
Chengsong
parents: 451
diff changeset
   879
  apply(case_tac a)
Chengsong
parents: 451
diff changeset
   880
       apply simp+
Chengsong
parents: 451
diff changeset
   881
  done
Chengsong
parents: 451
diff changeset
   882
Chengsong
parents: 451
diff changeset
   883
lemma flts_identity12:
Chengsong
parents: 451
diff changeset
   884
  shows " rflts (rs @ [RSTAR r0]) = rflts rs @ [RSTAR r0]"
Chengsong
parents: 451
diff changeset
   885
  apply(induct rs)
Chengsong
parents: 451
diff changeset
   886
   apply simp+
Chengsong
parents: 451
diff changeset
   887
  apply(case_tac a)
Chengsong
parents: 451
diff changeset
   888
       apply simp+
Chengsong
parents: 451
diff changeset
   889
  done
Chengsong
parents: 451
diff changeset
   890
Chengsong
parents: 451
diff changeset
   891
lemma flts_identity2:
Chengsong
parents: 451
diff changeset
   892
  shows "a \<noteq> RZERO \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow>  rflts (rs @ [a]) = rflts rs @ [a]"
Chengsong
parents: 451
diff changeset
   893
  apply(case_tac a)
Chengsong
parents: 451
diff changeset
   894
       apply simp
Chengsong
parents: 451
diff changeset
   895
  using flts_identity1 apply auto[1]
Chengsong
parents: 451
diff changeset
   896
  using flts_identity10 apply blast
Chengsong
parents: 451
diff changeset
   897
  using flts_identity11 apply auto[1]
Chengsong
parents: 451
diff changeset
   898
   apply blast
Chengsong
parents: 451
diff changeset
   899
  using flts_identity12 by presburger
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   900
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   901
lemma flts_identity3:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   902
  shows "a = RZERO  \<Longrightarrow> rflts (rs @ [a]) = rflts rs"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   903
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   904
  apply(induct rs)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   905
   apply simp+
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   906
  apply(case_tac aa)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   907
       apply simp+
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   908
  done
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   909
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   910
lemma distinct_removes_last3:
465
Chengsong
parents: 456
diff changeset
   911
  shows "\<lbrakk>a \<in> set as\<rbrakk>
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   912
    \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
465
Chengsong
parents: 456
diff changeset
   913
  by (simp add: distinct_removes_last2)
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   914
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   915
lemma set_inclusion_with_flts1:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   916
  shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE  \<in> set (rflts rs)"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   917
  apply(induct rs)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   918
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   919
  apply(case_tac " RONE \<in> set rs")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   920
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   921
  apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   922
  apply(case_tac "RONE = a")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   923
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   924
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   925
  done
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   926
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   927
lemma set_inclusion_with_flts10:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   928
  shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x  \<in> set (rflts rs)"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   929
  apply(induct rs)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   930
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   931
  apply(case_tac " RCHAR x \<in> set rs")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   932
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   933
  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   934
  apply(case_tac "RCHAR x = a")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   935
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   936
  apply fastforce
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   937
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   938
  done
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   939
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   940
lemma set_inclusion_with_flts11:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   941
  shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2  \<in> set (rflts rs)"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   942
  apply(induct rs)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   943
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   944
  apply(case_tac " RSEQ r1 r2 \<in> set rs")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   945
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   946
  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   947
  apply(case_tac "RSEQ r1 r2 = a")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   948
   apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   949
  apply fastforce
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   950
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   951
  done
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   952
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   953
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   954
lemma set_inclusion_with_flts:
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   955
  shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   956
  by (simp add: set_inclusion_with_flts1)
453
Chengsong
parents: 451
diff changeset
   957
  
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   958
lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   959
          \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = 
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   960
rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   961
465
Chengsong
parents: 456
diff changeset
   962
  sorry
Chengsong
parents: 456
diff changeset
   963
453
Chengsong
parents: 451
diff changeset
   964
Chengsong
parents: 451
diff changeset
   965
lemma last_elem_dup1:
Chengsong
parents: 451
diff changeset
   966
  shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
Chengsong
parents: 451
diff changeset
   967
  apply simp
Chengsong
parents: 451
diff changeset
   968
  apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
Chengsong
parents: 451
diff changeset
   969
  prefer 2
Chengsong
parents: 451
diff changeset
   970
   apply simp
456
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   971
  apply(case_tac "rsimp a")
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   972
       apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   973
  
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   974
  using flts_identity3 apply presburger
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   975
      apply(subst flts_identity2)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   976
  using rrexp.distinct(1) rrexp.distinct(15) apply presburger
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   977
      apply(subst distinct_removes_last3[symmetric])
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   978
  using set_inclusion_with_flts apply blast
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   979
  apply simp
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   980
  apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10)
26a5e640cdd7 realPhdThesis
Chengsong
parents: 453
diff changeset
   981
  apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11)
453
Chengsong
parents: 451
diff changeset
   982
  sorry
Chengsong
parents: 451
diff changeset
   983
Chengsong
parents: 451
diff changeset
   984
lemma last_elem_dup:
Chengsong
parents: 451
diff changeset
   985
  shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"
Chengsong
parents: 451
diff changeset
   986
  apply(induct as rule: rev_induct)
Chengsong
parents: 451
diff changeset
   987
   apply simp
Chengsong
parents: 451
diff changeset
   988
  apply simp
Chengsong
parents: 451
diff changeset
   989
  apply(subgoal_tac "xs \<noteq> []")
Chengsong
parents: 451
diff changeset
   990
  prefer 2
Chengsong
parents: 451
diff changeset
   991
  
Chengsong
parents: 451
diff changeset
   992
Chengsong
parents: 451
diff changeset
   993
  
Chengsong
parents: 451
diff changeset
   994
Chengsong
parents: 451
diff changeset
   995
  sorry
Chengsong
parents: 451
diff changeset
   996
Chengsong
parents: 451
diff changeset
   997
lemma appeared_before_remove_later:
Chengsong
parents: 451
diff changeset
   998
  shows "a \<in>  set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"
Chengsong
parents: 451
diff changeset
   999
and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"
Chengsong
parents: 451
diff changeset
  1000
  apply(induct rs arbitrary: as)
Chengsong
parents: 451
diff changeset
  1001
   apply simp
Chengsong
parents: 451
diff changeset
  1002
  
Chengsong
parents: 451
diff changeset
  1003
Chengsong
parents: 451
diff changeset
  1004
  sorry
Chengsong
parents: 451
diff changeset
  1005
Chengsong
parents: 451
diff changeset
  1006
lemma distinct_remove_later:
Chengsong
parents: 451
diff changeset
  1007
  shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>
Chengsong
parents: 451
diff changeset
  1008
       \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =
Chengsong
parents: 451
diff changeset
  1009
           rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1010
  
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1011
  sorry
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1012
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1013
453
Chengsong
parents: 451
diff changeset
  1014
lemma distinct_der_general:
Chengsong
parents: 451
diff changeset
  1015
  shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =
Chengsong
parents: 451
diff changeset
  1016
 rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"
Chengsong
parents: 451
diff changeset
  1017
  apply(induct rs arbitrary: rsa)
Chengsong
parents: 451
diff changeset
  1018
   apply simp
Chengsong
parents: 451
diff changeset
  1019
  apply(case_tac "a \<in> set rsa")
Chengsong
parents: 451
diff changeset
  1020
   apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")
Chengsong
parents: 451
diff changeset
  1021
  apply simp
Chengsong
parents: 451
diff changeset
  1022
   apply simp
Chengsong
parents: 451
diff changeset
  1023
  apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")
Chengsong
parents: 451
diff changeset
  1024
   apply(simp)
Chengsong
parents: 451
diff changeset
  1025
  apply(subst map_concat_cons)+
Chengsong
parents: 451
diff changeset
  1026
  apply(drule_tac x = "rsa @ [a]" in meta_spec)
Chengsong
parents: 451
diff changeset
  1027
   apply simp
Chengsong
parents: 451
diff changeset
  1028
  apply(drule neg_removal_element_of)
Chengsong
parents: 451
diff changeset
  1029
  apply simp
Chengsong
parents: 451
diff changeset
  1030
  apply(subst distinct_remove_later)
Chengsong
parents: 451
diff changeset
  1031
   apply simp
Chengsong
parents: 451
diff changeset
  1032
  apply(drule_tac x = "rsa" in meta_spec)
Chengsong
parents: 451
diff changeset
  1033
  by blast
Chengsong
parents: 451
diff changeset
  1034
Chengsong
parents: 451
diff changeset
  1035
  
Chengsong
parents: 451
diff changeset
  1036
Chengsong
parents: 451
diff changeset
  1037
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1038
lemma distinct_der:
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1039
  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
453
Chengsong
parents: 451
diff changeset
  1040
  by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1041
453
Chengsong
parents: 451
diff changeset
  1042
  
Chengsong
parents: 451
diff changeset
  1043
Chengsong
parents: 451
diff changeset
  1044
Chengsong
parents: 451
diff changeset
  1045
lemma rders_simp_lambda:
Chengsong
parents: 451
diff changeset
  1046
  shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"
Chengsong
parents: 451
diff changeset
  1047
  using rders_simp_append by auto
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1048
453
Chengsong
parents: 451
diff changeset
  1049
lemma rders_simp_nonempty_simped:
Chengsong
parents: 451
diff changeset
  1050
  shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"
Chengsong
parents: 451
diff changeset
  1051
  using rders_simp_same_simpders rsimp_idem by auto
Chengsong
parents: 451
diff changeset
  1052
Chengsong
parents: 451
diff changeset
  1053
lemma repeated_altssimp:
Chengsong
parents: 451
diff changeset
  1054
  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
Chengsong
parents: 451
diff changeset
  1055
           rsimp_ALTs (rdistinct (rflts rs) {})"
Chengsong
parents: 451
diff changeset
  1056
  by (metis map_idI rsimp.simps(2) rsimp_idem)
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1057
465
Chengsong
parents: 456
diff changeset
  1058
Chengsong
parents: 456
diff changeset
  1059
lemma add0_isomorphic:
Chengsong
parents: 456
diff changeset
  1060
  shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
Chengsong
parents: 456
diff changeset
  1061
  sorry
Chengsong
parents: 456
diff changeset
  1062
Chengsong
parents: 456
diff changeset
  1063
Chengsong
parents: 456
diff changeset
  1064
lemma distinct_append_simp:
Chengsong
parents: 456
diff changeset
  1065
  shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
Chengsong
parents: 456
diff changeset
  1066
           rsimp (rsimp_ALTs (f a # rs1)) =
Chengsong
parents: 456
diff changeset
  1067
           rsimp (rsimp_ALTs (f a # rs2))"
Chengsong
parents: 456
diff changeset
  1068
  apply(case_tac rs1)
Chengsong
parents: 456
diff changeset
  1069
   apply simp
Chengsong
parents: 456
diff changeset
  1070
   apply(case_tac rs2)
Chengsong
parents: 456
diff changeset
  1071
    apply simp
Chengsong
parents: 456
diff changeset
  1072
   apply simp
Chengsong
parents: 456
diff changeset
  1073
   prefer 2
Chengsong
parents: 456
diff changeset
  1074
   apply(case_tac list)
Chengsong
parents: 456
diff changeset
  1075
    apply(case_tac rs2)
Chengsong
parents: 456
diff changeset
  1076
     apply simp
Chengsong
parents: 456
diff changeset
  1077
  using add0_isomorphic apply blast 
Chengsong
parents: 456
diff changeset
  1078
    apply simp
467
Chengsong
parents: 465
diff changeset
  1079
  oops
465
Chengsong
parents: 456
diff changeset
  1080
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1081
lemma alts_closed_form: shows 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1082
"rsimp (rders_simp (RALTS rs) s) = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1083
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1084
  apply(induct s rule: rev_induct)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1085
   apply simp
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1086
  apply simp
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1087
  apply(subst rders_simp_append)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1088
  apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1089
 rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1090
   prefer 2
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1091
  apply (metis inside_simp_removal rders_simp_one_char)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1092
  apply(simp only: )
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1093
  apply(subst rders_simp_one_char)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1094
  apply(subst rsimp_idem)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1095
  apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1096
                     rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1097
  prefer 2
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1098
  using rder_rsimp_ALTs_commute apply presburger
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1099
  apply(simp only:)
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1100
  apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1101
= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1102
   prefer 2
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1103
  
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1104
  using distinct_der apply presburger
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1105
  apply(simp only:)
453
Chengsong
parents: 451
diff changeset
  1106
  apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
Chengsong
parents: 451
diff changeset
  1107
                      rsimp (rsimp_ALTs (rdistinct ( (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)))) {}))")
Chengsong
parents: 451
diff changeset
  1108
   apply(simp only:)
Chengsong
parents: 451
diff changeset
  1109
  apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = 
Chengsong
parents: 451
diff changeset
  1110
                      rsimp (rsimp_ALTs (rdistinct (rflts ( (map (rsimp \<circ> (rder x) \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
Chengsong
parents: 451
diff changeset
  1111
    apply(simp only:)
Chengsong
parents: 451
diff changeset
  1112
  apply(subst rders_simp_lambda)
Chengsong
parents: 451
diff changeset
  1113
    apply(subst rders_simp_nonempty_simped)
Chengsong
parents: 451
diff changeset
  1114
     apply simp
Chengsong
parents: 451
diff changeset
  1115
    apply(subgoal_tac "\<forall>r \<in> set  (map (\<lambda>r. rders_simp r (xs @ [x])) rs). rsimp r = r")
Chengsong
parents: 451
diff changeset
  1116
  prefer 2
Chengsong
parents: 451
diff changeset
  1117
     apply (simp add: rders_simp_same_simpders rsimp_idem)
Chengsong
parents: 451
diff changeset
  1118
    apply(subst repeated_altssimp)
Chengsong
parents: 451
diff changeset
  1119
     apply simp
Chengsong
parents: 451
diff changeset
  1120
  apply fastforce
465
Chengsong
parents: 456
diff changeset
  1121
   apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
Chengsong
parents: 456
diff changeset
  1122
  sledgehammer
Chengsong
parents: 456
diff changeset
  1123
 (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct)
451
7a016eeb118d finiteness
Chengsong
parents: 445
diff changeset
  1124
465
Chengsong
parents: 456
diff changeset
  1125
  *)
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1126
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1127
lemma alts_closed_form_variant: shows 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1128
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1129
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1130
  sorry
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1131
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1132
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1133
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1134
lemma star_closed_form:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1135
  shows "rders_simp (RSTAR r0) (c#s) = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1136
rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1137
  apply(induct s)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1138
   apply simp
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1139
  sorry
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1140
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1141
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1142
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1143
lemma seq_closed_form: shows 
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1144
"rsimp (rders_simp (RSEQ r1 r2) s) = 
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1145
rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 
445
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1146
                (map (rders_simp r2) (vsuf s r1)) 
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1147
              )  
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1148
      )"
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1149
  apply(induct s)
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1150
  apply simp
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1151
  sorry
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1152
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1153
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1154
lemma seq_closed_form_variant: shows
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1155
"s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1156
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
445
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1157
  apply(induct s rule: rev_induct)
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1158
   apply simp
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1159
  apply(subst rders_simp_append)
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1160
  apply(subst rders_simp_one_char)
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1161
  apply(subst rsimp_idem[symmetric])
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1162
  apply(subst rders_simp_one_char[symmetric])
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1163
  apply(subst rders_simp_append[symmetric])
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1164
  apply(insert seq_closed_form)
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1165
  apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1166
 = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1167
   apply force
e072cfc2f2ee closedforms
Chengsong
parents: 444
diff changeset
  1168
  by presburger
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents:
diff changeset
  1169
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
  1170
end