1 theory ClosedForms 

     2   imports "BasicIdentities"

     3 begin

     4 

     5 lemma flts_middle0:

     6   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"

     7   apply(induct rsa)

     8   apply simp

     9   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)

    10 

    11 

    12 

    13 lemma simp_flatten_aux0:

    14   shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"

    15   by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)

    16   

    17 

    18 inductive 

    19   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)

    20 where

    21   "RSEQ  RZERO r2 h\<leadsto> RZERO"

    22 | "RSEQ  r1 RZERO h\<leadsto> RZERO"

    23 | "RSEQ  RONE r h\<leadsto>  r"

    24 | "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 h\<leadsto> RSEQ r2 r3"

    25 | "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"

    26 | "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"

    27 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)

    28 | "RALTS  (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS  (rsa @ rsb)"

    29 | "RALTS  (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"

    30 | "RALTS  [] h\<leadsto> RZERO"

    31 | "RALTS  [r] h\<leadsto> r"

    32 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"

    33 

    34 inductive 

    35   hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)

    36 where 

    37   rs1[intro, simp]:"r h\<leadsto>* r"

    38 | rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"

    39 

    40 

    41 lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"

    42   using hrewrites.intros(1) hrewrites.intros(2) by blast

    43  

    44 lemma hreal_trans[trans]: 

    45   assumes a1: "r1 h\<leadsto>* r2"  and a2: "r2 h\<leadsto>* r3"

    46   shows "r1 h\<leadsto>* r3"

    47   using a2 a1

    48   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 

    49   apply(auto)

    50   done

    51 

    52 lemma hrewrites_seq_context:

    53   shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"

    54   apply(induct r1 r2 rule: hrewrites.induct)

    55    apply simp

    56   using hrewrite.intros(4) by blast

    57 

    58 lemma hrewrites_seq_context2:

    59   shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"

    60   apply(induct r1 r2 rule: hrewrites.induct)

    61    apply simp

    62   using hrewrite.intros(5) by blast

    63 

    64 

    65 lemma hrewrites_seq_contexts:

    66   shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"

    67   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)

    68 

    69 

    70 lemma simp_removes_duplicate1:

    71   shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"

    72 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"

    73   apply(induct rsa arbitrary: a1)

    74      apply simp

    75     apply simp

    76   prefer 2

    77   apply(case_tac "a = aa")

    78      apply simp

    79     apply simp

    80   apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))

    81   apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))

    82   by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))

    83   

    84 lemma simp_removes_duplicate2:

    85   shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"

    86   apply(induct rsb arbitrary: rsa)

    87    apply simp

    88   using distinct_removes_duplicate_flts apply auto[1]

    89   by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))

    90 

    91 lemma simp_removes_duplicate3:

    92   shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"

    93   using simp_removes_duplicate2 by auto

    94 

    95 (*

    96 lemma distinct_removes_middle4:

    97   shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"

    98   using distinct_removes_middle(1) by fastforce

    99 *)

   100 

   101 (*

   102 lemma distinct_removes_middle_list:

   103   shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"

   104   apply(induct x)

   105    apply simp

   106   by (simp add: distinct_removes_middle3)

   107 *)

   108 

   109 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)

   110   where

   111   "(RZERO # rs) \<leadsto>f rs"

   112 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"

   113 | "rs1 \<leadsto>f rs2 \<Longrightarrow> (r # rs1) \<leadsto>f (r # rs2)"

   114 

   115 

   116 inductive 

   117   frewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f* _" [10, 10] 10)

   118 where 

   119   [intro, simp]:"rs \<leadsto>f* rs"

   120 | [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"

   121 

   122 inductive grewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g _" [10, 10] 10)

   123   where

   124   "(RZERO # rs) \<leadsto>g rs"

   125 | "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"

   126 | "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"

   127 | "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 

   128 

   129 lemma grewrite_variant1:

   130   shows "a \<in> set rs1 \<Longrightarrow> rs1 @ a # rs \<leadsto>g rs1 @ rs"

   131   apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)

   132   done

   133 

   134 

   135 inductive 

   136   grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)

   137 where 

   138   [intro, simp]:"rs \<leadsto>g* rs"

   139 | [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"

   140 

   141 

   142 

   143 (*

   144 inductive 

   145   frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)

   146 where 

   147  [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"

   148 *)

   149 

   150 lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"

   151   using frewrites.intros(1) frewrites.intros(2) by blast

   152  

   153 lemma freal_trans[trans]: 

   154   assumes a1: "r1 \<leadsto>f* r2"  and a2: "r2 \<leadsto>f* r3"

   155   shows "r1 \<leadsto>f* r3"

   156   using a2 a1

   157   apply(induct r2 r3 arbitrary: r1 rule: frewrites.induct) 

   158   apply(auto)

   159   done

   160 

   161 

   162 lemma  many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3"

   163   by (meson fr_in_rstar freal_trans)

   164 

   165 

   166 lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2"

   167   using grewrites.intros(1) grewrites.intros(2) by blast

   168  

   169 lemma greal_trans[trans]: 

   170   assumes a1: "r1 \<leadsto>g* r2"  and a2: "r2 \<leadsto>g* r3"

   171   shows "r1 \<leadsto>g* r3"

   172   using a2 a1

   173   apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct) 

   174   apply(auto)

   175   done

   176 

   177 

   178 lemma  gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"

   179   by (meson gr_in_rstar greal_trans)

   180 

   181 lemma gstar_rdistinct_general:

   182   shows "rs1 @  rs \<leadsto>g* rs1 @ (rdistinct rs (set rs1))"

   183   apply(induct rs arbitrary: rs1)

   184    apply simp

   185   apply(case_tac " a \<in> set rs1")

   186    apply simp

   187   apply(subgoal_tac "rs1 @ a # rs \<leadsto>g rs1 @ rs")

   188   using gmany_steps_later apply auto[1]

   189   apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)

   190   apply simp

   191   apply(drule_tac x = "rs1 @ [a]" in meta_spec)

   192   by simp

   193 

   194 

   195 lemma gstar_rdistinct:

   196   shows "rs \<leadsto>g* rdistinct rs {}"

   197   apply(induct rs)

   198    apply simp

   199   by (metis append.left_neutral empty_set gstar_rdistinct_general)

   200 

   201 

   202 lemma grewrite_append:

   203   shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb"

   204   apply(induct rs)

   205    apply simp+

   206   using grewrite.intros(3) by blast

   207   

   208 

   209 

   210 lemma frewrites_cons:

   211   shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"

   212   apply(induct rsa rsb rule: frewrites.induct)

   213    apply simp

   214   using frewrite.intros(3) by blast

   215 

   216 

   217 lemma grewrites_cons:

   218   shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb"

   219   apply(induct rsa rsb rule: grewrites.induct)

   220    apply simp

   221   using grewrite.intros(3) by blast

   222 

   223 

   224 lemma frewrites_append:

   225   shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"

   226   apply(induct rs)

   227    apply simp

   228   by (simp add: frewrites_cons)

   229 

   230 lemma grewrites_append:

   231   shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)"

   232   apply(induct rs)

   233    apply simp

   234   by (simp add: grewrites_cons)

   235 

   236 

   237 lemma grewrites_concat:

   238   shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)"

   239   apply(induct rs1 rs2 rule: grewrite.induct)

   240     apply(simp)

   241   apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)")

   242   prefer 2

   243   using grewrite.intros(1) apply blast

   244     apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)")

   245   using gmany_steps_later apply blast

   246   apply (simp add: grewrites_append)

   247   apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later)

   248   using grewrites_cons apply auto

   249   apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb")

   250   using grewrite.intros(4) grewrites.intros(2) apply force

   251   using grewrites_append by auto

   252 

   253 

   254 lemma grewritess_concat:

   255   shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)"

   256   apply(induct rsa rsb rule: grewrites.induct)

   257    apply(case_tac rs)

   258     apply simp

   259   using grewrites_append apply blast   

   260   by (meson greal_trans grewrites.simps grewrites_concat)

   261 

   262 fun alt_set:: "rrexp \<Rightarrow> rrexp set"

   263   where

   264   "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"

   265 | "alt_set r = {r}"

   266 

   267 

   268 lemma grewrite_cases_middle:

   269   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 

   270 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>

   271 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>

   272 (\<exists>rsa rsb rsc a. rs1 = rsa @ [a] @ rsb @ [a] @ rsc \<and> rs2 = rsa @ [a] @ rsb @ rsc)"

   273   apply( induct rs1 rs2 rule: grewrite.induct)

   274      apply simp

   275   apply blast

   276   apply (metis append_Cons append_Nil)

   277   apply (metis append_Cons)

   278   by blast

   279 

   280 

   281 lemma good_singleton:

   282   shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"

   283   using good.simps(1) k0b by blast

   284 

   285 

   286 

   287 

   288 

   289 

   290 

   291 lemma all_that_same_elem:

   292   shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>

   293        \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"

   294   apply(induct rs)

   295    apply simp

   296   apply(subgoal_tac "aa = a")

   297    apply simp

   298   by (metis empty_iff insert_iff list.discI rdistinct.simps(2))

   299 

   300 lemma distinct_early_app1:

   301   shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"

   302   apply(induct rs arbitrary: rset rset1)

   303    apply simp

   304   apply simp

   305   apply(case_tac "a \<in> rset1")

   306    apply simp

   307    apply(case_tac "a \<in> rset")

   308     apply simp+

   309   

   310    apply blast

   311   apply(case_tac "a \<in> rset1")

   312    apply simp+

   313   apply(case_tac "a \<in> rset")

   314    apply simp

   315    apply (metis insert_subsetI)

   316   apply simp

   317   by (meson insert_mono)

   318 

   319 

   320 lemma distinct_early_app:

   321   shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"

   322   apply(induct rsb)

   323    apply simp

   324   using distinct_early_app1 apply blast

   325   by (metis distinct_early_app1 distinct_once_enough empty_subsetI)

   326 

   327 

   328 lemma distinct_eq_interesting1:

   329   shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"

   330   apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")

   331    apply(simp only:)

   332   using distinct_early_app apply blast 

   333   by (metis append_Cons distinct_early_app rdistinct.simps(2))

   334 

   335 

   336 

   337 lemma good_flatten_aux_aux1:

   338   shows "\<lbrakk> size rs \<ge>2; 

   339 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>

   340        \<Longrightarrow> rdistinct (rs @ rsb) rset =

   341            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"

   342   apply(induct rs arbitrary: rset)

   343    apply simp

   344   apply(case_tac "a \<in> rset")

   345    apply simp

   346    apply(case_tac "rdistinct rs {a}")

   347     apply simp

   348     apply(subst good_singleton)

   349      apply force

   350   apply simp

   351     apply (meson all_that_same_elem)

   352    apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")

   353   prefer 2

   354   using k0a rsimp_ALTs.simps(3) apply presburger

   355   apply(simp only:)

   356   apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")

   357     apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))

   358    apply (meson distinct_eq_interesting1)

   359   apply simp

   360   apply(case_tac "rdistinct rs {a}")

   361   prefer 2

   362    apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")

   363   apply(simp only:)

   364   apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =

   365            rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")

   366    apply simp

   367   apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))

   368   using rsimp_ALTs.simps(3) apply presburger

   369   by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)

   370 

   371 

   372 

   373   

   374 

   375 lemma good_flatten_aux_aux:

   376   shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 

   377 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>

   378        \<Longrightarrow> rdistinct (rs @ rsb) rset =

   379            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"

   380   apply(erule exE)+

   381   apply(subgoal_tac "size rs \<ge> 2")

   382    apply (metis good_flatten_aux_aux1)

   383   by (simp add: Suc_leI length_Cons less_add_Suc1)

   384 

   385 

   386 

   387 lemma good_flatten_aux:

   388   shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; 

   389            \<forall>r\<in>set rsb. good r \<or> r = RZERO;

   390      rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});

   391      rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =

   392      rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});

   393      map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs;

   394      rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =

   395      rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));

   396      rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =

   397      rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>

   398     \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =

   399            rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"

   400   apply simp

   401   apply(case_tac "rflts rs ")

   402    apply simp

   403   apply(case_tac "list")

   404    apply simp

   405    apply(case_tac "a \<in> rset")

   406     apply simp

   407   apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2))

   408    apply simp

   409   apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)

   410   apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")

   411    prefer 2

   412   apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)  

   413   apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")

   414    prefer 2

   415   apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1)  

   416   by (smt (verit, ccfv_threshold) good_flatten_aux_aux)

   417 

   418   

   419 

   420 

   421 lemma good_flatten_middle:

   422   shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>

   423 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"

   424   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 

   425 map rsimp rs @ map rsimp rsb)) {})")

   426   prefer 2

   427   apply simp

   428   apply(simp only:)

   429     apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 

   430 [rsimp (RALTS rs)] @ map rsimp rsb)) {})")

   431   prefer 2

   432    apply simp

   433   apply(simp only:)

   434   apply(subgoal_tac "map rsimp rsa = rsa")

   435   prefer 2

   436   apply (metis map_idI rsimp.simps(3) test)

   437   apply(simp only:)

   438   apply(subgoal_tac "map rsimp rsb = rsb")

   439    prefer 2

   440   apply (metis map_idI rsimp.simps(3) test)

   441   apply(simp only:)

   442   apply(subst k00)+

   443   apply(subgoal_tac "map rsimp rs = rs")

   444    apply(simp only:)

   445    prefer 2

   446   apply (metis map_idI rsimp.simps(3) test)

   447   apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 

   448 rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")

   449    apply(simp only:)

   450   prefer 2

   451   using rdistinct_concat_general apply blast

   452   apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 

   453 rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")

   454    apply(simp only:)

   455   prefer 2

   456   using rdistinct_concat_general apply blast

   457   apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 

   458                      rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")

   459    apply presburger

   460   using good_flatten_aux by blast

   461 

   462 

   463 lemma simp_flatten3:

   464   shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"

   465   apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 

   466                      rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")

   467   prefer 2

   468    apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)

   469   apply (simp only:)

   470   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 

   471 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")

   472   prefer 2

   473    apply (metis map_append simp_flatten_aux0)

   474   apply(simp only:)

   475   apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =

   476  rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")

   477   

   478    apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)

   479   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")

   480    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")

   481     apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")

   482   

   483   using good_flatten_middle apply presburger

   484   

   485   apply (simp add: good1)

   486   apply (simp add: good1)

   487   apply (simp add: good1)

   488 

   489   done

   490 

   491 

   492 

   493   

   494 

   495 lemma grewrite_equal_rsimp:

   496   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"

   497   apply(frule grewrite_cases_middle)

   498   apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")  

   499   using simp_flatten3 apply auto[1]

   500   apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")

   501   apply (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.set_intros(1) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) simp_removes_duplicate3)

   502   by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)

   503 

   504 

   505 lemma grewrites_equal_rsimp:

   506   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"

   507   apply (induct rs1 rs2 rule: grewrites.induct)

   508   apply simp

   509   using grewrite_equal_rsimp by presburger

   510   

   511 

   512 

   513 lemma grewrites_last:

   514   shows "r # [RALTS rs] \<leadsto>g*  r # rs"

   515   by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)

   516 

   517 lemma simp_flatten2:

   518   shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"

   519   using grewrites_equal_rsimp grewrites_last by blast

   520 

   521 

   522 lemma frewrites_alt:

   523   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"  

   524   by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)

   525 

   526 lemma early_late_der_frewrites:

   527   shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"

   528   apply(induct rs)

   529    apply simp

   530   apply(case_tac a)

   531        apply simp+

   532   using frewrite.intros(1) many_steps_later apply blast

   533      apply(case_tac "x = x3")

   534       apply simp

   535   using frewrites_cons apply presburger

   536   using frewrite.intros(1) many_steps_later apply fastforce

   537   apply(case_tac "rnullable x41")

   538      apply simp+

   539      apply (simp add: frewrites_alt)

   540   apply (simp add: frewrites_cons)

   541    apply (simp add: frewrites_append)

   542   by (simp add: frewrites_cons)

   543 

   544 

   545 lemma gstar0:

   546   shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"

   547   apply(induct rs arbitrary: rsa)

   548    apply simp

   549   apply(case_tac "a = RZERO")

   550    apply simp

   551   

   552   using gr_in_rstar grewrite.intros(1) grewrites_append apply presburger

   553   apply(case_tac "a \<in> set rsa")

   554    apply simp+

   555   apply(drule_tac x = "rsa @ [a]" in meta_spec)

   556   by simp

   557 

   558 lemma grewrite_rdistinct_aux:

   559   shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"

   560   apply(induct rsa arbitrary: rs rset)

   561    apply simp

   562   apply(case_tac " a \<in> rset")

   563    apply simp

   564   apply(case_tac "a \<in> set rs")

   565   apply simp

   566    apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)

   567   apply simp

   568   apply(drule_tac x = "rs @ [a]" in meta_spec)

   569   by (metis Un_insert_left Un_insert_right append.assoc append.right_neutral append_Cons append_Nil insert_absorb2 list.simps(15) set_append)

   570   

   571  

   572 lemma flts_gstar:

   573   shows "rs \<leadsto>g* rflts rs"

   574   apply(induct rs)

   575    apply simp

   576   apply(case_tac "a = RZERO")

   577    apply simp

   578   using gmany_steps_later grewrite.intros(1) apply blast

   579   apply(case_tac "\<exists>rsa. a = RALTS rsa")

   580    apply(erule exE)

   581   apply simp

   582    apply (meson grewrite.intros(2) grewrites.simps grewrites_cons)

   583   by (simp add: grewrites_cons rflts_def_idiot)

   584 

   585 lemma more_distinct1:

   586   shows "       \<lbrakk>\<And>rsb rset rset2.

   587            rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2);

   588         rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk>

   589        \<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"

   590   apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)")

   591    apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)")

   592     apply (meson greal_trans)

   593    apply (metis Un_iff Un_insert_left insert_absorb)

   594   by (simp add: gr_in_rstar grewrite_variant1 in_mono)

   595   

   596 

   597 

   598 

   599 

   600 lemma frewrite_rd_grewrites_aux:

   601   shows     "       RALTS rs \<notin> set rsb \<Longrightarrow>

   602        rsb @

   603        RALTS rs #

   604        rdistinct rsa

   605         (insert (RALTS rs)

   606           (set rsb)) \<leadsto>g* rflts rsb @

   607                           rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"

   608 

   609    apply simp

   610   apply(subgoal_tac "rsb @

   611     RALTS rs #

   612     rdistinct rsa

   613      (insert (RALTS rs)

   614        (set rsb)) \<leadsto>g* rsb @

   615     rs @

   616     rdistinct rsa

   617      (insert (RALTS rs)

   618        (set rsb)) ")

   619   apply(subgoal_tac " rsb @

   620     rs @

   621     rdistinct rsa

   622      (insert (RALTS rs)

   623        (set rsb)) \<leadsto>g*

   624                       rsb @

   625     rdistinct rs (set rsb) @

   626     rdistinct rsa

   627      (insert (RALTS rs)

   628        (set rsb)) ")

   629     apply (smt (verit, ccfv_SIG) Un_insert_left flts_gstar greal_trans grewrite_rdistinct_aux grewritess_concat inf_sup_aci(5) rdistinct_concat_general rdistinct_set_equality set_append)

   630    apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)

   631   by (simp add: gr_in_rstar grewrite.intros(2) grewrites_append)

   632   

   633 

   634 

   635 

   636 lemma list_dlist_union:

   637   shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"

   638   by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)

   639 

   640 lemma r_finite1:

   641   shows "r = RALTS (r # rs) = False"

   642   apply(induct r)

   643   apply simp+

   644    apply (metis list.set_intros(1))

   645   by blast

   646   

   647 

   648 

   649 lemma grewrite_singleton:

   650   shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []"

   651   apply (induct "[r]" "r # rs" rule: grewrite.induct)

   652     apply simp

   653   apply (metis r_finite1)

   654   using grewrite.simps apply blast

   655   by simp

   656 

   657 

   658 

   659 lemma concat_rdistinct_equality1:

   660   shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \<union> (set rs))"

   661   apply(induct rs arbitrary: rsa rset)

   662    apply simp

   663   apply(case_tac "a \<in> rset")

   664    apply simp

   665   apply (simp add: insert_absorb)

   666   by auto

   667 

   668 

   669 lemma grewrites_rev_append:

   670   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"

   671   using grewritess_concat by auto

   672 

   673 lemma grewrites_inclusion:

   674   shows "set rs \<subseteq> set rs1 \<Longrightarrow> rs1 @ rs \<leadsto>g* rs1"

   675   apply(induct rs arbitrary: rs1)

   676   apply simp

   677   by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1))

   678 

   679 lemma distinct_keeps_last:

   680   shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"

   681   by (simp add: concat_rdistinct_equality1)

   682 

   683 lemma grewrites_shape2_aux:

   684   shows "       RALTS rs \<notin> set rsb \<Longrightarrow>

   685        rsb @

   686        rdistinct (rs @ rsa)

   687         (set rsb) \<leadsto>g* rsb @

   688                        rdistinct rs (set rsb) @

   689                        rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"

   690   apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) =  rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb)")

   691    apply (simp only:)

   692   prefer 2

   693   apply (simp add: Un_commute concat_rdistinct_equality1)

   694   apply(induct rsa arbitrary: rs rsb rule: rev_induct)

   695    apply simp

   696   apply(case_tac "x \<in> set rs")

   697   apply (simp add: distinct_removes_middle3)

   698   apply(case_tac "x = RALTS rs")

   699    apply simp

   700   apply(case_tac "x \<in> set rsb")

   701    apply simp

   702     apply (simp add: concat_rdistinct_equality1)

   703   apply (simp add: concat_rdistinct_equality1)

   704   apply simp

   705   apply(drule_tac x = "rs " in meta_spec)

   706   apply(drule_tac x = rsb in meta_spec)

   707   apply simp

   708   apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (insert (RALTS rs) (set rs \<union> set rsb))")

   709   prefer 2

   710    apply (simp add: concat_rdistinct_equality1)

   711   apply(case_tac "x \<in> set xs")

   712    apply simp

   713    apply (simp add: distinct_removes_last)

   714   apply(case_tac "x \<in> set rsb")

   715    apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2))

   716   apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (set rs \<union> set rsb) = rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x]")

   717   apply(simp only:)

   718   apply(case_tac "x = RALTS rs")

   719     apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x] \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs")

   720   apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) ")

   721       apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2))

   722   apply(subgoal_tac "set rs \<subseteq> set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb))")

   723   apply (metis append.assoc grewrites_inclusion)

   724      apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append)

   725   apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append)

   726    apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (insert (RALTS rs) (set rs \<union> set rsb)) =  rsb @ rdistinct rs (set rsb) @ rdistinct (xs) (insert (RALTS rs) (set rs \<union> set rsb)) @ [x]")

   727   apply(simp only:)

   728   apply (metis append.assoc grewrites_rev_append)

   729   apply (simp add: insert_absorb)

   730    apply (simp add: distinct_keeps_last)+

   731   done

   732 

   733 lemma grewrites_shape2:

   734   shows "       RALTS rs \<notin> set rsb \<Longrightarrow>

   735        rsb @

   736        rdistinct (rs @ rsa)

   737         (set rsb) \<leadsto>g* rflts rsb @

   738                        rdistinct rs (set rsb) @

   739                        rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"

   740   apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat)

   741   done

   742 

   743 lemma rdistinct_add_acc:

   744   shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"

   745   apply(induct rs arbitrary: rsb rset rset2)

   746    apply simp

   747   apply (case_tac "a \<in> rset")

   748    apply simp

   749   apply(case_tac "a \<in> rset2")

   750    apply simp

   751   apply (simp add: more_distinct1)

   752   apply simp

   753   apply(drule_tac x = "rsb @ [a]" in meta_spec)

   754   by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)

   755   

   756 

   757 lemma frewrite_fun1:

   758   shows "       RALTS rs \<in> set rsb \<Longrightarrow>

   759        rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)"

   760   apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb)")

   761    apply(subgoal_tac " set rs \<subseteq> set (rflts rsb)")

   762   prefer 2

   763   using spilled_alts_contained apply blast

   764    apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)")

   765   using greal_trans apply blast

   766   using rdistinct_add_acc apply presburger

   767   using flts_gstar grewritess_concat by auto

   768   

   769 lemma frewrite_rd_grewrites:

   770   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> 

   771 \<exists>rs3. (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3) "

   772   apply(induct rs1 rs2 arbitrary: rs rule: frewrite.induct)

   773     apply(rule_tac x = "rsa @ (rdistinct rs ({RZERO} \<union> set rsa))" in exI)

   774     apply(rule conjI)

   775   apply(case_tac "RZERO \<in> set rsa")

   776   apply simp+

   777   using gstar0 apply fastforce

   778      apply (simp add: gr_in_rstar grewrite.intros(1) grewrites_append)

   779     apply (simp add: gstar0)

   780     prefer 2

   781     apply(case_tac "r \<in> set rs")

   782   apply simp

   783     apply(drule_tac x = "rs @ [r]" in meta_spec)

   784     apply(erule exE)

   785     apply(rule_tac x = "rs3" in exI)

   786    apply simp

   787   apply(case_tac "RALTS rs \<in> set rsb")

   788    apply simp

   789    apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" in exI)

   790    apply(rule conjI)

   791   using frewrite_fun1 apply force

   792   apply (metis frewrite_fun1 rdistinct_concat sup_ge2)

   793   apply(simp)

   794   apply(rule_tac x = 

   795  "rflts rsb @

   796                        rdistinct rs (set rsb) @

   797                        rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)

   798   apply(rule conjI)

   799    prefer 2

   800   using grewrites_shape2 apply force

   801   using frewrite_rd_grewrites_aux by blast

   802 

   803 

   804 lemma frewrite_simpeq2:

   805   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"

   806   apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")

   807   using grewrites_equal_rsimp apply fastforce

   808   by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))

   809 

   810 

   811 

   812 

   813 (*a more refined notion of h\<leadsto>* is needed,

   814 this lemma fails when rs1 contains some RALTS rs where elements

   815 of rs appear in later parts of rs1, which will be picked up by rs2

   816 and deduplicated*)

   817 lemma frewrites_simpeq:

   818   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>

   819  rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "

   820   apply(induct rs1 rs2 rule: frewrites.induct)

   821    apply simp

   822   using frewrite_simpeq2 by presburger

   823 

   824 

   825 lemma frewrite_single_step:

   826   shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"

   827   apply(induct rs2 rs3 rule: frewrite.induct)

   828     apply simp

   829   using simp_flatten apply blast

   830   by (metis (no_types, opaque_lifting) list.simps(9) rsimp.simps(2) simp_flatten2)

   831 

   832 lemma grewrite_simpalts:

   833   shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"

   834   apply(induct rs2 rs3 rule : grewrite.induct)

   835   using identity_wwo0 apply presburger

   836   apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten)

   837   apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3))

   838   apply simp

   839   apply(subst rsimp_alts_equal)

   840   apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []")

   841    apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]")

   842   apply (simp only:)

   843   apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2))

   844    apply simp

   845   by (smt (verit, best) append.assoc append_Cons frewrite.intros(1) frewrite_single_step identity_wwo0 in_set_conv_decomp rsimp_ALTs.simps(3) simp_removes_duplicate3)

   846 

   847 

   848 lemma grewrites_simpalts:

   849   shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"

   850   apply(induct rs2 rs3 rule: grewrites.induct)

   851    apply simp

   852   using grewrite_simpalts by presburger

   853 

   854 

   855 lemma simp_der_flts:

   856   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 

   857          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"

   858   apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")

   859   using frewrites_simpeq apply presburger

   860   using early_late_der_frewrites by auto

   861 

   862 

   863 lemma simp_der_pierce_flts_prelim:

   864   shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) 

   865        = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"

   866   by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)

   867 

   868 

   869 lemma basic_regex_property1:

   870   shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"

   871   apply(induct r rule: rsimp.induct)

   872   apply(auto)

   873   apply (metis idiot idiot2 rrexp.distinct(5))

   874   by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))

   875 

   876 

   877 lemma inside_simp_seq_nullable:

   878   shows 

   879 "\<And>r1 r2.

   880        \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);

   881         rnullable r1\<rbrakk>

   882        \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =

   883            rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"

   884   apply(case_tac "rsimp r1 = RONE")

   885    apply(simp)

   886   apply(subst basic_rsimp_SEQ_property1)

   887    apply (simp add: idem_after_simp1)

   888   apply(case_tac "rsimp r1 = RZERO")

   889   

   890   using basic_regex_property1 apply blast

   891   apply(case_tac "rsimp r2 = RZERO")

   892   

   893   apply (simp add: basic_rsimp_SEQ_property3)

   894   apply(subst idiot2)

   895      apply simp+

   896   apply(subgoal_tac "rnullable (rsimp r1)")

   897    apply simp

   898   using rsimp_idem apply presburger

   899   using der_simp_nullability by presburger

   900   

   901 

   902 

   903 lemma grewrite_ralts:

   904   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"

   905   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))

   906 

   907 lemma grewrites_ralts:

   908   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"

   909   apply(induct rule: grewrites.induct)

   910   apply simp

   911   using grewrite_ralts hreal_trans by blast

   912   

   913 

   914 lemma distinct_grewrites_subgoal1:

   915   shows "  

   916        \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"

   917   apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")

   918   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))

   919   apply(subgoal_tac "rs1 \<leadsto>g* rs3")

   920   using grewrites_ralts apply blast

   921   using grewrites.intros(2) by presburger

   922 

   923 lemma grewrites_ralts_rsimpalts:

   924   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "

   925   apply(induct rs rs' rule: grewrites.induct)

   926    apply(case_tac rs)

   927   using hrewrite.intros(9) apply force

   928    apply(case_tac list)

   929   apply simp

   930   using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger

   931    apply simp

   932   apply(case_tac rs2)

   933    apply simp

   934    apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))

   935   apply(case_tac list)

   936    apply(simp)

   937   using distinct_grewrites_subgoal1 apply blast

   938   apply simp

   939   apply(case_tac rs3)

   940    apply simp

   941   using grewrites_ralts hrewrite.intros(9) apply blast

   942   by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))

   943 

   944 lemma hrewrites_alts:

   945   shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"

   946   apply(induct r r' rule: hrewrites.induct)

   947   apply simp

   948   using hrewrite.intros(6) by blast

   949 

   950 inductive 

   951   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)

   952 where

   953   ss1: "[] scf\<leadsto>* []"

   954 | ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"

   955 

   956 

   957 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"

   958 

   959   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)

   960    apply(rule rs1)

   961   apply(drule_tac x = "rsa@[r']" in meta_spec)

   962   apply simp

   963   apply(rule hreal_trans)

   964    prefer 2

   965    apply(assumption)

   966   apply(drule hrewrites_alts)

   967   by auto

   968 

   969 

   970 corollary srewritescf_alt1: 

   971   assumes "rs1 scf\<leadsto>* rs2"

   972   shows "RALTS rs1 h\<leadsto>* RALTS rs2"

   973   using assms

   974   by (metis append_Nil srewritescf_alt)

   975 

   976 

   977 

   978 

   979 lemma trivialrsimp_srewrites: 

   980   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"

   981 

   982   apply(induction rs)

   983    apply simp

   984    apply(rule ss1)

   985   by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)

   986 

   987 lemma hrewrites_list: 

   988   shows

   989 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"

   990   apply(induct x)

   991    apply(simp)+

   992   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)

   993 (*  apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)

   994 

   995   

   996 lemma hrewrite_simpeq:

   997   shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"

   998   apply(induct rule: hrewrite.induct)

   999             apply simp+

  1000   apply (simp add: basic_rsimp_SEQ_property3)

  1001   apply (simp add: basic_rsimp_SEQ_property1)

  1002   using rsimp.simps(1) apply presburger

  1003         apply simp+

  1004   using flts_middle0 apply force

  1005 

  1006   

  1007   using simp_flatten3 apply presburger

  1008 

  1009   apply simp+

  1010   apply (simp add: idem_after_simp1)

  1011   using grewrite.intros(4) grewrite_equal_rsimp by presburger

  1012 

  1013 lemma hrewrites_simpeq:

  1014   shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"

  1015   apply(induct rule: hrewrites.induct)

  1016    apply simp

  1017   apply(subgoal_tac "rsimp r2 = rsimp r3")

  1018    apply auto[1]

  1019   using hrewrite_simpeq by presburger

  1020   

  1021 

  1022 

  1023 lemma simp_hrewrites:

  1024   shows "r1 h\<leadsto>* rsimp r1"

  1025   apply(induct r1)

  1026        apply simp+

  1027     apply(case_tac "rsimp r11 = RONE")

  1028      apply simp

  1029      apply(subst basic_rsimp_SEQ_property1)

  1030   apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")

  1031   using hreal_trans hrewrite.intros(3) apply blast

  1032   using hrewrites_seq_context apply presburger

  1033     apply(case_tac "rsimp r11 = RZERO")

  1034      apply simp

  1035   using hrewrite.intros(1) hrewrites_seq_context apply blast

  1036     apply(case_tac "rsimp r12 = RZERO")

  1037      apply simp

  1038   apply(subst basic_rsimp_SEQ_property3)

  1039   apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)

  1040     apply(subst idiot2)

  1041        apply simp+

  1042   using hrewrites_seq_contexts apply presburger

  1043    apply simp

  1044    apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")

  1045   apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")

  1046   using hreal_trans apply blast

  1047     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)

  1048 

  1049    apply (simp add: grewrites_ralts hrewrites_list)

  1050   by simp

  1051 

  1052 lemma interleave_aux1:

  1053   shows " RALT (RSEQ RZERO r1) r h\<leadsto>*  r"

  1054   apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")

  1055   apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")

  1056   apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)

  1057   using rs1 srewritescf_alt1 ss1 ss2 apply presburger

  1058   by (simp add: hr_in_rstar hrewrite.intros(1))

  1059 

  1060 

  1061 

  1062 lemma rnullable_hrewrite:

  1063   shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"

  1064   apply(induct rule: hrewrite.induct)

  1065             apply simp+

  1066      apply blast

  1067     apply simp+

  1068   done

  1069 

  1070 

  1071 lemma interleave1:

  1072   shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"

  1073   apply(induct r r' rule: hrewrite.induct)

  1074             apply (simp add: hr_in_rstar hrewrite.intros(1))

  1075   apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)

  1076           apply simp

  1077           apply(subst interleave_aux1)

  1078           apply simp

  1079          apply(case_tac "rnullable r1")

  1080           apply simp

  1081   

  1082           apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2)

  1083   

  1084          apply (simp add: hrewrites_seq_context rnullable_hrewrite)

  1085         apply(case_tac "rnullable r1")

  1086   apply simp

  1087   

  1088   using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger

  1089   apply simp

  1090   using hr_in_rstar hrewrites_seq_context2 apply blast

  1091        apply simp

  1092   

  1093   using hrewrites_alts apply auto[1]

  1094   apply simp

  1095   using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1]

  1096   apply simp

  1097   apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts)

  1098   apply (simp add: hr_in_rstar hrewrite.intros(9))

  1099    apply (simp add: hr_in_rstar hrewrite.intros(10))

  1100   apply simp

  1101   using hrewrite.intros(11) by auto

  1102 

  1103 lemma interleave_star1:

  1104   shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"

  1105   apply(induct rule : hrewrites.induct)

  1106    apply simp

  1107   by (meson hreal_trans interleave1)

  1108 

  1109 

  1110 

  1111 lemma inside_simp_removal:

  1112   shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"

  1113   apply(induct r)

  1114        apply simp+

  1115     apply(case_tac "rnullable r1")

  1116      apply simp

  1117   

  1118   using inside_simp_seq_nullable apply blast

  1119     apply simp

  1120   apply (smt (verit, del_insts) idiot2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)

  1121    apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")

  1122   using hrewrites_simpeq apply presburger

  1123   using interleave_star1 simp_hrewrites apply presburger

  1124   by simp

  1125   

  1126 

  1127 

  1128 

  1129 lemma rders_simp_same_simpders:

  1130   shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"

  1131   apply(induct s rule: rev_induct)

  1132    apply simp

  1133   apply(case_tac "xs = []")

  1134    apply simp

  1135   apply(simp add: rders_append rders_simp_append)