Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys2/ClosedForms.thy
changeset 478 51af5f882350
parent 476 56837303ce61
child 479 b2a8610cf110
equal deleted inserted replaced
477:ab6aaf8d7649 478:51af5f882350 
     1 theory ClosedForms imports
 
     1 theory ClosedForms imports
 
     2 "BasicIdentities"
 
     2 "BasicIdentities"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 
       
     6 lemma idem_after_simp1:
 
       
     7   shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
 
       
     8   apply(case_tac "rsimp aa")
 
       
     9   apply simp+
 
       
    10   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
 
       
    11   by simp
 
       
    12 
       
    13 lemma identity_wwo0:
 
       
    14   shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
 
       
    15   by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
       
    16 
       
    17 
       
    18 lemma distinct_removes_last:
 
       
    19   shows "\<lbrakk>a \<in> set as\<rbrakk>
 
       
    20     \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
 
       
    21 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
 
       
    22   apply(induct as arbitrary: rset ab rset1 a)
 
       
    23      apply simp
 
       
    24     apply simp
 
       
    25   apply(case_tac "aa \<in> rset")
 
       
    26    apply(case_tac "a = aa")
 
       
    27   apply (metis append_Cons)
 
       
    28     apply simp
 
       
    29    apply(case_tac "a \<in> set as")
 
       
    30   apply (metis append_Cons rdistinct.simps(2) set_ConsD)
 
       
    31    apply(case_tac "a = aa")
 
       
    32     prefer 2
 
       
    33     apply simp
 
       
    34    apply (metis append_Cons)
 
       
    35   apply(case_tac "ab \<in> rset1")
 
       
    36   prefer 2
 
       
    37    apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
       
    38                ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
 
       
    39   prefer 2
 
       
    40   apply force
 
       
    41   apply(simp only:)
 
       
    42      apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
 
       
    43     apply(simp only:)
 
       
    44     apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
 
       
    45      apply blast
 
       
    46     apply(case_tac "a \<in> insert ab rset1")
 
       
    47      apply simp
 
       
    48      apply (metis insertI1)
 
       
    49     apply simp
 
       
    50     apply (meson insertI1)
 
       
    51    apply simp
 
       
    52   apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
 
       
    53    apply simp
 
       
    54   by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
 
       
    55 
       
    56 
       
    57 lemma distinct_removes_middle:
 
       
    58   shows  "\<lbrakk>a \<in> set as\<rbrakk>
 
       
    59     \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
 
       
    60 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
 
       
    61    apply(induct as arbitrary: rset rset1 ab as2 as3 a)
 
       
    62      apply simp
 
       
    63     apply simp
 
       
    64    apply(case_tac "a \<in> rset")
 
       
    65     apply simp
 
       
    66     apply metis
 
       
    67    apply simp
 
       
    68    apply (metis insertI1)
 
       
    69   apply(case_tac "a = ab")
 
       
    70    apply simp
 
       
    71    apply(case_tac "ab \<in> rset")
 
       
    72     apply simp
 
       
    73     apply presburger
 
       
    74    apply (meson insertI1)
 
       
    75   apply(case_tac "a \<in> rset")
 
       
    76   apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
 
       
    77   apply(case_tac "ab \<in> rset")
 
       
    78   apply simp
 
       
    79    apply (meson insert_iff)
 
       
    80   apply simp
 
       
    81   by (metis insertI1)
 
       
    82 
       
    83 
       
    84 lemma distinct_removes_middle3:
 
       
    85   shows  "\<lbrakk>a \<in> set as\<rbrakk>
 
       
    86     \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
 
       
    87   using distinct_removes_middle(1) by fastforce
 
       
    88 
       
    89 lemma distinct_removes_last2:
 
       
    90   shows "\<lbrakk>a \<in> set as\<rbrakk>
 
       
    91     \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
 
       
    92   by (simp add: distinct_removes_last(1))
 
       
    93 
       
    94 lemma distinct_removes_middle2:
 
       
    95   shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
 
       
    96   by (metis distinct_removes_middle(1))
 
       
    97 
       
    98 lemma distinct_removes_list:
 
       
    99   shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
 
       
   100   apply(induct rs)
 
       
   101    apply simp+
 
       
   102   apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
 
       
   103    prefer 2
 
       
   104   apply (metis append_Cons append_Nil distinct_removes_middle(1))
 
       
   105   by presburger
 
       
   106 
       
   107 
       
   108 lemma spawn_simp_rsimpalts:
 
       
   109   shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
 
       
   110   apply(cases rs)
 
       
   111    apply simp
 
       
   112   apply(case_tac list)
 
       
   113    apply simp
 
       
   114    apply(subst rsimp_idem[symmetric])
 
       
   115    apply simp
 
       
   116   apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
 
       
   117    apply(simp only:)
 
       
   118    apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
 
       
   119     apply(simp only:)
 
       
   120   prefer 2
 
       
   121   apply simp
 
       
   122    prefer 2
 
       
   123   using rsimp_ALTs.simps(3) apply presburger
 
       
   124   apply auto
 
       
   125   apply(subst rsimp_idem)+
 
       
   126   by (metis comp_apply rsimp_idem)
 
       
   127 
       
   128 lemma map_concat_cons:
 
     5 lemma map_concat_cons:
 
   129   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
 
     6   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
 
   130   by simp
 
     7   by simp
 
   131 
     8 
   132 lemma neg_removal_element_of:
 
     9 lemma neg_removal_element_of:
 
   133   shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
 
    10   shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
 
   134   by simp
 
    11   by simp
 
   135 
    12 
   136 lemma flts_removes0:
 
    13 
   137   shows "  rflts (rs @ [RZERO])  =
 
    14 
   138            rflts rs"
 
    15 
   139   apply(induct rs)
 
    16 
   140    apply simp
 
    17 
   141   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
    18 
   142   
    19 
   143 lemma flts_keeps1:
 
    20 
   144   shows " rflts (rs @ [RONE]) = 
       
   145           rflts  rs @ [RONE] "
 
       
   146   apply (induct rs)
 
       
   147    apply simp
 
       
   148   by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   149 
       
   150 lemma flts_keeps_others:
 
       
   151   shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
 
       
   152   apply(induct rs)
 
       
   153    apply simp
 
       
   154   apply (simp add: rflts_def_idiot)
 
       
   155   apply(case_tac a)
 
       
   156        apply simp
 
       
   157   using flts_keeps1 apply blast
 
       
   158      apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   159   apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   160   apply blast
 
       
   161   by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   162 
       
   163 
       
   164 lemma rflts_def_idiot2:
 
       
   165   shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
 
       
   166   apply(induct rs)
 
       
   167    apply simp
 
       
   168   by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   169 
       
   170 lemma rflts_spills_last:
 
       
   171   shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
 
       
   172   apply (induct rs1)
 
       
   173   apply simp
 
       
   174   by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   175 
       
   176 
       
   177 lemma spilled_alts_contained:
 
       
   178   shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
 
       
   179   apply(induct rs1)
 
       
   180    apply simp 
       
   181   apply(case_tac "a = aa")
 
       
   182    apply simp
 
       
   183   apply(subgoal_tac " a \<in> set rs1")
 
       
   184   prefer 2
 
       
   185    apply (meson set_ConsD)
 
       
   186   apply(case_tac aa)
 
       
   187   using rflts.simps(2) apply presburger
 
       
   188       apply fastforce
 
       
   189   apply fastforce
 
       
   190   apply fastforce
 
       
   191   apply fastforce
 
       
   192   by fastforce
 
       
   193 
       
   194 lemma distinct_removes_duplicate_flts:
 
       
   195   shows " a \<in> set rsa
 
       
   196        \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
 
       
   197            rdistinct (rflts (map rsimp rsa)) {}"
 
       
   198   apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
 
       
   199   prefer 2
 
       
   200   apply simp
 
       
   201   apply(induct "rsimp a")
 
       
   202        apply simp
 
       
   203   using flts_removes0 apply presburger
 
       
   204       apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
       
   205                           rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
 
       
   206       apply (simp only:)
 
       
   207        apply(subst flts_keeps1)
 
       
   208   apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
 
       
   209       apply presburger
 
       
   210         apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
       
   211                             rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
 
       
   212       apply (simp only:)
 
       
   213       prefer 2
 
       
   214       apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
 
       
   215   apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
 
       
   216 
       
   217     apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
 
       
   218    prefer 2
 
       
   219    apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
 
       
   220   apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
 
       
   221   prefer 2
 
       
   222   apply (simp add: rflts_spills_last)
 
       
   223   apply(simp only:)
 
       
   224   apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
 
       
   225   prefer 2
 
       
   226   using spilled_alts_contained apply presburger
 
       
   227   by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust)
 
       
   228 
    21 
   229 lemma flts_middle0:
 
    22 lemma flts_middle0:
 
   230   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
 
    23   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
 
   231   apply(induct rsa)
 
    24   apply(induct rsa)
 
   232   apply simp
 
    25   apply simp
 
   244   using rflts_def_idiot apply presburger
 
    37   using rflts_def_idiot apply presburger
 
   245   apply(case_tac aa)  
    38   apply(case_tac aa)  
   246        apply simp+
 
    39        apply simp+
 
   247   done
 
    40   done
 
   248 
    41 
   249 lemma flts_append:
 
    42 
   250   shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
 
       
   251   apply(induct rs1)
 
       
   252    apply simp
 
       
   253   apply(case_tac a)
 
       
   254        apply simp+
 
       
   255   done
 
       
   256 
    43 
   257 lemma simp_removes_duplicate1:
 
    44 lemma simp_removes_duplicate1:
 
   258   shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
 
    45   shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
 
   259 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
 
    46 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
 
   260   apply(induct rsa arbitrary: a1)
 
    47   apply(induct rsa arbitrary: a1)
 
   349   using rsimpalts_conscons by presburger
 
   136   using rsimpalts_conscons by presburger
 
   350 
   137 
   351 
   138 
   352 
   139 
   353 
   140 
   354 lemma distinct_flts_no0:
 
       
   355   shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =
 
       
   356            rflts (map rsimp (rdistinct rs rset))  "
 
       
   357   
       
   358   apply(induct rs arbitrary: rset)
 
       
   359    apply simp
 
       
   360   apply(case_tac a)
 
       
   361   apply simp+
 
       
   362     apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
   363   prefer 2
 
       
   364   apply simp  
       
   365   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))
 
       
   366 
   141 
   367 
   142 
   368 
   143 
   369 
   144 
   370 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
 
   145 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
 
   385   "(RZERO # rs) \<leadsto>g rs"
 
   160   "(RZERO # rs) \<leadsto>g rs"
 
   386 | "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"
 
   161 | "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"
 
   387 | "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
 
   162 | "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
 
   388 | "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 
   163 | "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 
   389 
   164 
       
   165 lemma grewrite_variant1:
 
       
   166   shows "a \<in> set rs1 \<Longrightarrow> rs1 @ a # rs \<leadsto>g rs1 @ rs"
 
       
   167   apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
 
       
   168   done
 
       
   169 
   390 
   170 
   391 inductive 
   171 inductive 
   392   grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)
 
   172   grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)
 
   393 where 
   173 where 
   394   [intro, simp]:"rs \<leadsto>g* rs"
 
   174   [intro, simp]:"rs \<leadsto>g* rs"
 
   395 | [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"
 
   175 | [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"
 
       
   176 
       
   177 
       
   178 
   396 (*
 
   179 (*
 
   397 inductive 
   180 inductive 
   398   frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)
 
   181   frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)
 
   399 where 
   182 where 
   400  [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"
 
   183  [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"
 
   428   done
 
   211   done
 
   429 
   212 
   430 
   213 
   431 lemma  gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"
 
   214 lemma  gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"
 
   432   by (meson gr_in_rstar greal_trans)
 
   215   by (meson gr_in_rstar greal_trans)
 
       
   216 
       
   217 lemma gstar_rdistinct_general:
 
       
   218   shows "rs1 @  rs \<leadsto>g* rs1 @ (rdistinct rs (set rs1))"
 
       
   219   apply(induct rs arbitrary: rs1)
 
       
   220    apply simp
 
       
   221   apply(case_tac " a \<in> set rs1")
 
       
   222    apply simp
 
       
   223   apply(subgoal_tac "rs1 @ a # rs \<leadsto>g rs1 @ rs")
 
       
   224   using gmany_steps_later apply auto[1]
 
       
   225   apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
 
       
   226   apply simp
 
       
   227   apply(drule_tac x = "rs1 @ [a]" in meta_spec)
 
       
   228   by simp
 
       
   229 
       
   230 
       
   231 lemma gstar_rdistinct:
 
       
   232   shows "rs \<leadsto>g* rdistinct rs {}"
 
       
   233   apply(induct rs)
 
       
   234    apply simp
 
       
   235   by (metis append.left_neutral empty_set gstar_rdistinct_general)
 
   433 
   236 
   434 
   237 
   435 
   238 
   436 lemma frewrite_append:
 
   239 lemma frewrite_append:
 
   437   shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
 
   240   shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
 
   538   apply (metis append_Cons append_Nil flts_middle0)
 
   341   apply (metis append_Cons append_Nil flts_middle0)
 
   539     apply(case_tac "rsimp r \<in> rset")
 
   342     apply(case_tac "rsimp r \<in> rset")
 
   540      apply simp
 
   343      apply simp
 
   541   oops
 
   344   oops
 
   542 
   345 
       
   346 lemma grewrite_cases_middle:
 
       
   347   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
       
   348 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
 
       
   349 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
 
       
   350 (\<exists>rsa rsb rsc a. rs1 = rsa @ [a] @ rsb @ [a] @ rsc \<and> rs2 = rsa @ [a] @ rsb @ rsc)"
 
       
   351   apply( induct rs1 rs2 rule: grewrite.induct)
 
       
   352      apply simp
 
       
   353   apply blast
 
       
   354   apply (metis append_Cons append_Nil)
 
       
   355   apply (metis append_Cons)
 
       
   356   by blast
 
   543 
   357 
   544 
   358 
   545 lemma grewrite_equal_rsimp:
 
   359 lemma grewrite_equal_rsimp:
 
   546   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   360   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   547   apply(induct rs1 rs2 rule: grewrite.induct)
 
   361   apply(frule grewrite_cases_middle)
 
   548   apply simp
 
   362   apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")  
   549   using simp_flatten apply blast
 
   363   using simp_flatten3 apply auto[1]
 
   550    prefer 2
 
   364   apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")
 
   551    apply (smt (verit) append.assoc append_Cons in_set_conv_decomp simp_removes_duplicate2)
 
   365   apply (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.set_intros(1) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) simp_removes_duplicate3)
 
   552   apply simp
 
   366   by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)
 
   553   apply(case_tac "rdistinct (rflts (map rsimp rs1)) {}")
 
       
   554   apply(case_tac "rsimp r = RZERO")
 
       
   555     apply simp
 
       
   556    apply(case_tac "\<exists>rs. rsimp r = RALTS rs")
 
       
   557     prefer 2
 
       
   558    
       
   559     apply(subgoal_tac "rdistinct (rflts (rsimp r # map rsimp rs1)) {} = 
       
   560                     rsimp r # rdistinct (rflts (map rsimp rs1)) {rsimp r}")
 
       
   561   prefer 2
 
       
   562   apply (simp add: list.inject rflts_def_idiot)
 
       
   563     apply(simp only:)
 
       
   564 
       
   565   sorry
 
       
   566 
   367 
   567 
   368 
   568 lemma grewrites_equal_rsimp:
 
   369 lemma grewrites_equal_rsimp:
 
   569   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   370   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   570   apply (induct rs1 rs2 rule: grewrites.induct)
 
   371   apply (induct rs1 rs2 rule: grewrites.induct)
 
   574 
   375 
   575 
   376 
   576 
   377 
   577 lemma grewrites_equal_simp_2:
 
   378 lemma grewrites_equal_simp_2:
 
   578   shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
 
   379   shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
 
   579   sorry
 
   380   oops
 
       
   381 
       
   382 
       
   383 
   580 
   384 
   581 lemma grewrites_last:
 
   385 lemma grewrites_last:
 
   582   shows "r # [RALTS rs] \<leadsto>g*  r # rs"
 
   386   shows "r # [RALTS rs] \<leadsto>g*  r # rs"
 
   583   by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
 
   387   by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
 
   584 
   388 
   609      apply simp+
 
   413      apply simp+
 
   610      apply (simp add: frewrites_alt)
 
   414      apply (simp add: frewrites_alt)
 
   611   apply (simp add: frewrites_cons)
 
   415   apply (simp add: frewrites_cons)
 
   612    apply (simp add: frewrites_append)
 
   416    apply (simp add: frewrites_append)
 
   613   by (simp add: frewrites_cons)
 
   417   by (simp add: frewrites_cons)
 
   614 
       
   615 
   418 
   616 
   419 
   617 
   420 
   618 
   421 
   619 lemma with_wo0_distinct:
 
   422 lemma with_wo0_distinct:
 
   659                                     (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset))))
 
   462                                     (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset))))
 
   660  rs2 = [+rs] rs3 = rs,
 
   463  rs2 = [+rs] rs3 = rs,
 
   661 r = +rs
 
   464 r = +rs
 
   662 [] \<leadsto>g* rs which is wrong
 
   465 [] \<leadsto>g* rs which is wrong
 
   663 *)
 
   466 *)
 
   664 lemma frewrite_with_distinct:
 
   467 
   665   shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>
 
   468 
   666        \<Longrightarrow> rdistinct rs2
 
   469 
   667             (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>g* 
   470 
   668            rdistinct rs3 
   471 
   669             (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
 
   472 
   670   apply(induct rs2 rs3  arbitrary: rset rule: frewrite.induct)
 
       
   671     apply(case_tac "RZERO \<in>  (rset \<union> \<Union> (alt_set ` rset))")
 
       
   672   apply simp
 
       
   673     apply simp
 
       
   674 
       
   675 
       
   676   oops
 
       
   677 
       
   678 
       
   679 
       
   680 lemma frewrites_with_distinct:
 
       
   681   shows "\<lbrakk>rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow>
 
       
   682 ( (rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g* 
       
   683  rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))
 
       
   684 \<or> ( rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g*
 
       
   685     rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))  
       
   686  )
 
       
   687 "
 
       
   688   apply(induct rsa rsb arbitrary: rs1 rule: frewrite.induct)
 
       
   689     apply simp
 
       
   690    apply(case_tac "RALTS rs \<in> set rs1")
 
       
   691     apply(subgoal_tac "set rs \<subseteq> \<Union> (alt_set `set rs1)")
 
       
   692      apply (metis (full_types) Un_iff Un_insert_left 
       
   693 Un_insert_right grewrites.intros(1) le_supI2 rdistinct.simps(2) rdistinct_concat)
 
       
   694   apply (metis Un_subset_iff Union_upper alt_set.simps(1) imageI)
 
       
   695 
       
   696    apply(case_tac "RALTS rs \<in> \<Union> (alt_set ` set rs1)")
 
       
   697   apply simp
 
       
   698   apply (smt (z3) UN_insert Un_iff alt_set.simps(1) alt_set_has_all dual_order.trans grewrites.intros(1) insert_absorb rdistinct_concat subset_insertI)
 
       
   699   
       
   700 
       
   701   oops
 
       
   702 
       
   703 
       
   704 
       
   705 lemma rd_flts_set:
 
       
   706   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union>  (rset \<union>  \<Union>(alt_set ` rset))) \<leadsto>g* 
       
   707                           rdistinct rs2 ({RZERO} \<union>  (rset \<union>  \<Union>(alt_set ` rset)))"
 
       
   708   apply(induct rs1 rs2 rule: frewrites.induct)
 
       
   709    apply simp
 
       
   710   oops
 
       
   711 
   473 
   712 lemma frewrite_simpeq:
 
   474 lemma frewrite_simpeq:
 
   713   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   475   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   714   apply(induct rs1 rs2 rule: frewrite.induct)
 
   476   apply(induct rs1 rs2 rule: frewrite.induct)
 
   715     apply simp
 
   477     apply simp
 
   716   using simp_flatten apply presburger
 
   478   using simp_flatten apply presburger
 
   717   by (meson grewrites_cons grewrites_equal_rsimp grewrites_equal_simp_2)
 
   479   by (metis (no_types, opaque_lifting) grewrites_equal_rsimp grewrites_last list.simps(9) rsimp.simps(2))
 
       
   480 
       
   481 lemma gstar0:
 
       
   482   shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"
 
       
   483   apply(induct rs arbitrary: rsa)
 
       
   484    apply simp
 
       
   485   apply(case_tac "a = RZERO")
 
       
   486    apply simp
 
       
   487   
       
   488   using gr_in_rstar grewrite.intros(1) grewrites_append apply presburger
 
       
   489   apply(case_tac "a \<in> set rsa")
 
       
   490    apply simp+
 
       
   491   apply(drule_tac x = "rsa @ [a]" in meta_spec)
 
       
   492   by simp
 
       
   493   
       
   494 lemma gstar01:
 
       
   495   shows "rdistinct rs {} \<leadsto>g* rdistinct rs {RZERO}"
 
       
   496   by (metis empty_set gstar0 self_append_conv2)
 
       
   497 
       
   498 
       
   499 lemma grewrite_rdistinct_aux:
 
       
   500   shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
 
       
   501   sorry
 
       
   502 
       
   503 lemma grewrite_rdistinct_worth1:
 
       
   504   shows "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)"
 
       
   505   by (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
 
       
   506 
       
   507 lemma grewrite_rdisitinct:
 
       
   508   shows "rs @ rdistinct rsa {RALTS rs} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))"
 
       
   509   apply(induct rsa arbitrary: rs)
 
       
   510    apply simp
 
       
   511   apply(case_tac "a = RALTS rs")
 
       
   512   apply simp
 
       
   513   apply(case_tac "a \<in> set rs")
 
       
   514    apply simp
 
       
   515   apply(subgoal_tac "rs @
 
       
   516            a # rdistinct rsa {RALTS rs, a} \<leadsto>g rs @ rdistinct rsa {RALTS rs, a}")
 
       
   517     apply(subgoal_tac 
       
   518 "rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))")
 
       
   519   using gmany_steps_later apply blast
 
       
   520     apply(subgoal_tac 
       
   521 " rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa ({RALTS rs, a} \<union> set rs)")
 
       
   522      apply (simp add: insert_absorb)
 
       
   523   using grewrite_rdistinct_aux apply blast
 
       
   524   using grewrite_variant1 apply blast
 
       
   525   by (metis grewrite_rdistinct_aux insert_is_Un)
 
       
   526 
       
   527   
       
   528 lemma frewrite_rd_grewrites_general:
 
       
   529   shows "\<lbrakk>rs1 \<leadsto>f rs2; \<And>rs. \<exists>rs3. 
       
   530 (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3)\<rbrakk>
 
       
   531        \<Longrightarrow> 
       
   532 \<exists>rs3. (rs @ (r # rdistinct rs1 (set rs \<union> {r})) \<leadsto>g* rs3) \<and> (rs @ (r # rdistinct rs2 (set rs \<union> {r})) \<leadsto>g* rs3)"
 
       
   533   apply(drule_tac x = "rs @ [r]" in meta_spec )
 
       
   534   by simp
 
       
   535 
       
   536 
       
   537 lemma grewrites_middle_distinct:
 
       
   538   shows "RALTS rs \<in> set rsb \<Longrightarrow> 
       
   539          rsb @
 
       
   540        rdistinct ( rs @ rsa)
 
       
   541         (set rsb) \<leadsto>g* rsb @ rdistinct rsa (set rsb)"
 
       
   542   sorry
 
       
   543 
       
   544 
       
   545 
       
   546 lemma frewrite_rd_grewrites_aux:
 
       
   547   shows     "  rsb @
 
       
   548        rdistinct (RALTS rs # rsa)
 
       
   549         (set rsb) \<leadsto>g* rsb @
 
       
   550                        rdistinct rs (set rsb) @ rdistinct rsa (insert (RALTS rs) (set rs) \<union> set rsb)"
 
       
   551 
       
   552   
       
   553   sorry
 
       
   554 
       
   555 lemma flts_gstar:
 
       
   556   shows "rs \<leadsto>g* rflts rs"
 
       
   557   sorry
 
       
   558 
       
   559 lemma list_dlist_union:
 
       
   560   shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"
 
       
   561   by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)
 
       
   562 
       
   563 lemma subset_distinct_rewrite1:
 
       
   564   shows "set1 \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs set1)"
 
       
   565   apply(induct rs arbitrary: rsb)
 
       
   566    apply simp
 
       
   567   apply(case_tac "a \<in> set1")
 
       
   568    apply simp
 
       
   569   
       
   570   using gmany_steps_later grewrite_variant1 apply blast
 
       
   571   apply simp
 
       
   572   apply(drule_tac x = "rsb @ [a]" in meta_spec)
 
       
   573   apply(subgoal_tac "set1 \<subseteq> set (rsb @ [a])")
 
       
   574    apply (simp only:)
 
       
   575   apply(subgoal_tac "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)")
 
       
   576     apply (metis (no_types, opaque_lifting) append.assoc append_Cons append_Nil greal_trans)
 
       
   577   apply (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
 
       
   578   by auto
 
       
   579 
       
   580 
       
   581 lemma subset_distinct_rewrite:
 
       
   582   shows "set rsb' \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs (set rsb'))"
 
       
   583   by (simp add: subset_distinct_rewrite1)
 
       
   584   
       
   585 
       
   586 
       
   587 lemma distinct_3list:
 
       
   588   shows "rsb @ (rdistinct rs (set rsb)) @ rsa \<leadsto>g* 
       
   589          rsb @ (rdistinct rs (set rsb)) @ (rdistinct rsa (set rs))"
 
       
   590   by (metis append.assoc list_dlist_union set_append subset_distinct_rewrite)
 
       
   591   
       
   592 
       
   593 
       
   594 
       
   595 lemma grewrites_shape1:
 
       
   596   shows "      RALTS rs \<notin> set rsb \<Longrightarrow>
 
       
   597        rsb @
 
       
   598        RALTS rs #
 
       
   599        rdistinct rsa
 
       
   600         (
 
       
   601           (set rsb)) \<leadsto>g* rsb @
 
       
   602                           rdistinct rs (set rsb) @
 
       
   603                           rdistinct (rflts (rdistinct rsa ( (set rsb \<union> set rs)))) (set rs)"
 
       
   604 
       
   605 
       
   606   apply (subgoal_tac "       rsb @
 
       
   607        RALTS rs #
 
       
   608        rdistinct rsa
 
       
   609         (
 
       
   610           (set rsb))  \<leadsto>g*        rsb @
 
       
   611        rs @
 
       
   612        rdistinct rsa
 
       
   613         (
 
       
   614           (set rsb)) ")
 
       
   615    prefer 2
 
       
   616   using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
 
       
   617   apply(subgoal_tac "rsb @ rs @ rdistinct rsa (  (set rsb)) \<leadsto>g* rsb @ 
       
   618 (rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb)))")
 
       
   619   prefer 2
 
       
   620   apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
 
       
   621   apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb))
 
       
   622 \<leadsto>g*  rsb @ rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb) \<union> (set rs))")
 
       
   623   prefer 2
 
       
   624   apply (smt (verit, best) append.assoc append_assoc boolean_algebra_cancel.sup2 grewrite_rdistinct_aux inf_sup_aci(5) insert_is_Un rdistinct_concat_general rdistinct_set_equality set_append sup.commute sup.right_idem sup_commute)
 
       
   625   apply(subgoal_tac "rdistinct rsa (  (set rsb)  \<union> set rs) \<leadsto>g*
 
       
   626 rflts (rdistinct rsa (  (set rsb) \<union> set rs))")
 
       
   627    apply(subgoal_tac "rsb @ (rdistinct rs (set rsb)) @ rflts (rdistinct rsa (  (set rsb) \<union> set rs)) \<leadsto>g* 
       
   628 rsb @ (rdistinct rs (set rsb)) @ (rdistinct (rflts (rdistinct rsa (  (set rsb) \<union> set rs))) (set rs))")
 
       
   629   apply (smt (verit, ccfv_SIG) Un_insert_left greal_trans grewrites_append)
 
       
   630   using distinct_3list apply presburger
 
       
   631   using flts_gstar apply blast
 
       
   632   done
 
       
   633 
       
   634 lemma r_finite1:
 
       
   635   shows "r = RALTS (r # rs) = False"
 
       
   636   apply(induct r)
 
       
   637   apply simp+
 
       
   638    apply (metis list.set_intros(1))
 
       
   639   by blast
 
       
   640   
       
   641 
       
   642 
       
   643 lemma grewrite_singleton:
 
       
   644   shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []"
 
       
   645   apply (induct "[r]" "r # rs" rule: grewrite.induct)
 
       
   646     apply simp
 
       
   647   apply (metis r_finite1)
 
       
   648   using grewrite.simps apply blast
 
       
   649   by simp
 
       
   650 
       
   651 lemma impossible_grewrite1:
 
       
   652   shows "\<not>( [RONE] \<leadsto>g [])"
 
       
   653   using grewrite.cases by fastforce
 
       
   654 
       
   655 
       
   656 lemma impossible_grewrite2:
 
       
   657   shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)"
 
       
   658   
       
   659   using grewrite_singleton by blast
 
       
   660 thm grewrite.cases
 
       
   661 lemma impossible_grewrite3:
 
       
   662   shows "\<not> (RALTS rs # rs1 \<leadsto>g (RALTS rs) # a # rs1)"
 
       
   663   oops
 
       
   664 
       
   665 
       
   666 lemma grewrites_singleton:
 
       
   667   shows "[r] \<leadsto>g* r # rs \<Longrightarrow> rs = []"
 
       
   668   apply(induct "[r]" "r # rs" rule: grewrites.induct)
 
       
   669    apply simp
 
       
   670   
       
   671   oops
 
       
   672 
       
   673 lemma grewrite_nonequal_elem:
 
       
   674   shows "r # rs2 \<leadsto>g r # rs3 \<Longrightarrow> rs2 \<leadsto>g rs3"
 
       
   675   oops
 
       
   676 
       
   677 lemma grewrites_nonequal_elem:
 
       
   678   shows "r # rs2 \<leadsto>g* r # rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
 
       
   679   apply(induct r)
 
       
   680   
       
   681   oops
 
       
   682 
       
   683   
       
   684 
       
   685 
       
   686 lemma :
 
       
   687   shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
 
       
   688   apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct)
 
       
   689    apply simp
 
       
   690   apply(drule_tac x = "[x] @ rs2" in meta_spec)
 
       
   691   apply(drule_tac x = "[x] @ rs3" in meta_spec)
 
       
   692   apply(simp)
 
       
   693 
       
   694   oops
 
       
   695 
       
   696 
       
   697 
       
   698 lemma grewrites_shape3_aux:
 
       
   699   shows "rs @ (rdistinct rsa (insert (RALTS rs) rsc)) \<leadsto>g* rs @ rdistinct (rflts (rdistinct rsa rsc)) (set rs)"
 
       
   700   apply(induct rsa arbitrary: rsc rs)
 
       
   701    apply simp
 
       
   702   apply(case_tac "a \<in> rsc")
 
       
   703    apply simp
 
       
   704   apply(case_tac "a = RALTS rs")
 
       
   705    apply simp
 
       
   706   apply(subgoal_tac " rdistinct (rs @ rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs) \<leadsto>g*
 
       
   707  rdistinct (rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs)")
 
       
   708   apply (metis insertI1 insert_absorb rdistinct_concat2)
 
       
   709    apply (simp add: rdistinct_concat)
 
       
   710 
       
   711   apply simp
 
       
   712   apply(case_tac "a = RZERO")
 
       
   713   apply (metis gmany_steps_later grewrite.intros(1) grewrite_append rflts.simps(2))
 
       
   714   apply(case_tac "\<exists>rs1. a = RALTS rs1")
 
       
   715    prefer 2
 
       
   716    apply simp
 
       
   717    apply(subgoal_tac "rflts (a # rdistinct rsa (insert a rsc)) = a # rflts (rdistinct rsa (insert a rsc))")
 
       
   718     apply (simp  only:)
 
       
   719     apply(case_tac "a \<notin> set rs")
 
       
   720      apply simp
 
       
   721   apply(drule_tac x = "insert a rsc" in meta_spec)
 
       
   722   apply(drule_tac x = "rs " in meta_spec)
 
       
   723   
       
   724     apply(erule exE)
 
       
   725     apply simp
 
       
   726   apply(subgoal_tac "RALTS rs1 #
 
       
   727            rdistinct rsa
 
       
   728             (insert (RALTS rs)
 
       
   729               (insert (RALTS rs1)
 
       
   730                 rsc)) \<leadsto>g* rs1 @
 
       
   731            rdistinct rsa
 
       
   732             (insert (RALTS rs)
 
       
   733               (insert (RALTS rs1)
 
       
   734                 rsc)) ")
 
       
   735      apply(subgoal_tac " rs1 @
 
       
   736            rdistinct rsa
 
       
   737             (insert (RALTS rs)
 
       
   738               (insert (RALTS rs1)
 
       
   739                 rsc)) \<leadsto>g*
 
       
   740                         rs1 @
 
       
   741            rdistinct rsa
 
       
   742             (insert (RALTS rs)
 
       
   743               (insert (RALTS rs1)
 
       
   744                 rsc))")
 
       
   745   
       
   746   apply(case_tac "a \<in> set rs")
 
       
   747   
       
   748 
       
   749 
       
   750   sorry
 
       
   751 
       
   752 
       
   753 lemma grewrites_shape3:
 
       
   754   shows "      RALTS rs \<notin> set rsb \<Longrightarrow>
 
       
   755        rsb @
 
       
   756        RALTS rs #
 
       
   757        rdistinct rsa
 
       
   758         (insert (RALTS rs)
 
       
   759           (set rsb)) \<leadsto>g* rsb @
 
       
   760                           rdistinct rs (set rsb) @
 
       
   761                           rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
 
       
   762   apply(subgoal_tac "rsb @ RALTS rs # rdistinct rsa (insert (RALTS rs) (set rsb)) \<leadsto>g*
 
       
   763                      rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb))")
 
       
   764   prefer 2
 
       
   765   using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
 
       
   766   apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb )) \<leadsto>g*
 
       
   767                      rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs))")
 
       
   768   prefer 2
 
       
   769   apply (metis Un_insert_left grewrite_rdistinct_aux grewrites_append)
 
       
   770 
       
   771   apply(subgoal_tac "rsb @  rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs)) \<leadsto>g* 
       
   772 rsb @ rs @ rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)")
 
       
   773    prefer 2
 
       
   774   using grewrites_append grewrites_shape3_aux apply presburger
 
       
   775   apply(subgoal_tac "rsb @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb)")
 
       
   776   apply (smt (verit, ccfv_SIG) append_eq_appendI greal_trans grewrites.simps grewritess_concat)
 
       
   777   using gstar_rdistinct_general by blast
 
       
   778 
       
   779 
       
   780 lemma grewrites_shape2:
 
       
   781   shows "       RALTS rs \<notin> set rsb \<Longrightarrow>
 
       
   782        rsb @
 
       
   783        rdistinct (rs @ rsa)
 
       
   784         (set rsb) \<leadsto>g* rsb @
 
       
   785                        rdistinct rs (set rsb) @
 
       
   786                        rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
 
       
   787 
       
   788  (* by (smt (z3) append.assoc distinct_3list flts_gstar greal_trans grewrites_append rdistinct_concat_general same_append_eq set_append)
 
       
   789 *)
 
       
   790   sorry
 
       
   791 
       
   792 
       
   793 
       
   794 
   718 
   795 
   719 lemma frewrite_rd_grewrites:
 
   796 lemma frewrite_rd_grewrites:
 
   720   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> 
   797   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> 
   721 \<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) "
 
   798 \<exists>rs3. (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3) "
 
   722   apply(induct rs1 rs2 rule: frewrite.induct)
 
   799   apply(induct rs1 rs2 arbitrary: rs rule: frewrite.induct)
 
   723     apply(rule_tac x = "rs" in exI)
 
   800     apply(rule_tac x = "rsa @ (rdistinct rs ({RZERO} \<union> set rsa))" in exI)
 
   724     apply(rule conjI)
 
   801     apply(rule conjI)
 
   725      apply(rule gr_in_rstar)
 
   802   apply(case_tac "RZERO \<in> set rsa")
 
   726   apply(rule grewrite.intros)
 
   803   apply simp+
 
   727     apply(rule grewrites.intros)
 
   804   using gstar0 apply fastforce
 
   728   using grewrite.intros(2) apply blast
 
   805      apply (simp add: gr_in_rstar grewrite.intros(1) grewrites_append)
 
   729   by (meson grewrites_cons)
 
   806     apply (simp add: gstar0)
 
       
   807     prefer 2
 
       
   808     apply(case_tac "r \<in> set rs")
 
       
   809   apply simp
 
       
   810     apply(drule_tac x = "rs @ [r]" in meta_spec)
 
       
   811     apply(erule exE)
 
       
   812     apply(rule_tac x = "rs3" in exI)
 
       
   813    apply simp
 
       
   814   apply(case_tac "RALTS rs \<in> set rsb")
 
       
   815    apply simp
 
       
   816    apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb)" in exI)
 
       
   817    apply(rule conjI)
 
       
   818   apply (simp add: flts_gstar grewritess_concat)
 
       
   819   apply (meson flts_gstar greal_trans grewrites.intros(1) grewrites_middle_distinct grewritess_concat)
 
       
   820   apply(simp)
 
       
   821   apply(rule_tac x = 
       
   822 "rsb @ (rdistinct rs (set rsb)) @
 
       
   823  (rdistinct (rflts (rdistinct  rsa ( (set rsb \<union> set rs)) ) ) (set rs))" in exI)
 
       
   824   apply(rule conjI)
 
       
   825    prefer 2
 
       
   826   using grewrites_shape2 apply force
 
       
   827   using grewrites_shape3 by auto
 
       
   828 
       
   829 
       
   830 
       
   831 lemma frewrite_simprd:
 
       
   832   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
       
   833   by (meson frewrite_simpeq)
 
   730 
   834 
   731 
   835 
   732 lemma frewrites_rd_grewrites:
 
   836 lemma frewrites_rd_grewrites:
 
   733   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
   837   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
   734 \<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3)"
 
   838 rsimp (RALTS rs1) = rsimp (RALTS rs2)"
 
   735   apply(induct rs1 rs2 rule: frewrites.induct)
 
   839   apply(induct rs1 rs2 rule: frewrites.induct)
 
   736    apply simp
 
   840    apply simp
 
   737   apply(rule exI)
 
   841   using frewrite_simprd by presburger
 
   738   apply(rule grewrites.intros)
 
       
   739   by (metis frewrite_simpeq grewrites_equal_rsimp grewrites_equal_simp_2)
 
       
   740 
       
   741 
   842 
   742 
   843 
   743 
   844 
   744 
   845 
   745 lemma frewrite_simpeq2:
 
   846 lemma frewrite_simpeq2:
 
   746   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
 
   847   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
 
   747   apply(induct rs1 rs2 rule: frewrite.induct)
 
   848   apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")
 
   748     apply simp  
   849   using grewrites_equal_rsimp apply fastforce
 
   749     apply (simp add: distinct_flts_no0)
 
   850   using frewrite_rd_grewrites by presburger
 
   750   apply simp
 
   851 
   751 (*a more refined notion of \<leadsto>* is needed,
 
   852 (*a more refined notion of \<leadsto>* is needed,
 
   752 this lemma fails when rs1 contains some RALTS rs where elements
 
   853 this lemma fails when rs1 contains some RALTS rs where elements
 
   753 of rs appear in later parts of rs1, which will be picked up by rs2
 
   854 of rs appear in later parts of rs1, which will be picked up by rs2
 
   754 and deduplicated*)
 
   855 and deduplicated*)
 
   755 lemma frewrites_simpeq:
 
   856 lemma frewrites_simpeq:
 
   756   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
   857   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
   757  rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
 
   858  rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
 
   758   apply(induct rs1 rs2 rule: frewrites.induct)
 
   859   apply(induct rs1 rs2 rule: frewrites.induct)
 
   759    apply simp
 
   860    apply simp
 
   760   
   861   using frewrite_simpeq2 by presburger
 
   761   sorry
 
       
   762 
       
   763 
   862 
   764 
   863 
   765 lemma frewrite_single_step:
 
   864 lemma frewrite_single_step:
 
   766   shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
 
   865   shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
 
   767   apply(induct rs2 rs3 rule: frewrite.induct)
 
   866   apply(induct rs2 rs3 rule: frewrite.induct)
 
   812 
   911 
   813 lemma simp_der_flts:
 
   912 lemma simp_der_flts:
 
   814   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
   913   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
   815          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
 
   914          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
 
   816   apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
 
   915   apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
 
   817    apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} 
   916   using frewrites_simpeq apply presburger
 
   818                     \<leadsto>g* rdistinct ( rflts (map (rder x) rs)) {RZERO}")
 
   917   using early_late_der_frewrites by auto
 
   819   apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) 
   918 
   820                    = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))")
 
   919   
   821   apply meson
 
       
   822   apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2))
 
       
   823   sorry
 
       
   824 
   920 
   825 
   921 
   826 
   922 
   827 
   923 
   828  
   924  
   830 
   926 
   831 
   927 
   832 lemma simp_der_pierce_flts_prelim:
 
   928 lemma simp_der_pierce_flts_prelim:
 
   833   shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) 
   929   shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) 
   834        = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
 
   930        = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
 
   835   apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>g* rflts (map (rder x) rs)")
 
   931   by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
 
   836   apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} \<leadsto>g* rdistinct (rflts (map (rder x) rs)) {RZERO}")
 
       
   837   using grewrites_equal_simp_2 grewrites_simpalts simp_der_flts apply blast
 
       
   838   apply (simp add: early_late_der_frewrites frewrites_with_distinct2_grewrites)
 
       
   839   using early_late_der_frewrites frewrites_equivalent_simp grewrites_equal_simp_2 by blast
 
       
   840 
   932 
   841 
   933 
   842 lemma simp_der_pierce_flts:
 
   934 lemma simp_der_pierce_flts:
 
   843   shows " rsimp (
 
   935   shows " rsimp (
 
   844 rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
 
   936 rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
 
  1168   using simp_der_pierce_flts by blast
 
  1260   using simp_der_pierce_flts by blast
 
  1169 
  1261 
  1170 lemma alts_closed_form_variant: shows 
  1262 lemma alts_closed_form_variant: shows 
  1171 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
  1263 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
  1172 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
 
  1264 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
 
  1173   sorry
 
  1265   by (metis alts_closed_form comp_apply rders_simp_nonempty_simped)
 
       
  1266   
  1174 
  1267 
  1175 
  1268 
  1176 
  1269 
  1177 lemma star_closed_form:
 
  1270 lemma star_closed_form:
 
  1178   shows "rders_simp (RSTAR r0) (c#s) = 
  1271   shows "rders_simp (RSTAR r0) (c#s) =
lexing