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   apply (simp add: frewrites_cons)

   543   apply (auto simp add: frewrites_cons)

   544   using frewrite.intros(1) many_steps_later by blast

   545   

   546 

   547 lemma gstar0:

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

   549   apply(induct rs arbitrary: rsa)

   550    apply simp

   551   apply(case_tac "a = RZERO")

   552    apply simp

   553   

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

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

   556    apply simp+

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

   558   by simp

   559 

   560 lemma grewrite_rdistinct_aux:

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

   562   apply(induct rsa arbitrary: rs rset)

   563    apply simp

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

   565    apply simp

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

   567   apply simp

   568    apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)

   569   apply simp

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

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

   572   

   573  

   574 lemma flts_gstar:

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

   576   apply(induct rs)

   577    apply simp

   578   apply(case_tac "a = RZERO")

   579    apply simp

   580   using gmany_steps_later grewrite.intros(1) apply blast

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

   582    apply(erule exE)

   583   apply simp

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

   585   by (simp add: grewrites_cons rflts_def_idiot)

   586 

   587 lemma more_distinct1:

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

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

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

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

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

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

   594     apply (meson greal_trans)

   595    apply (metis Un_iff Un_insert_left insert_absorb)

   596   by (simp add: gr_in_rstar grewrite_variant1 in_mono)

   597   

   598 

   599 

   600 

   601 

   602 lemma frewrite_rd_grewrites_aux:

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

   604        rsb @

   605        RALTS rs #

   606        rdistinct rsa

   607         (insert (RALTS rs)

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

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

   610 

   611    apply simp

   612   apply(subgoal_tac "rsb @

   613     RALTS rs #

   614     rdistinct rsa

   615      (insert (RALTS rs)

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

   617     rs @

   618     rdistinct rsa

   619      (insert (RALTS rs)

   620        (set rsb)) ")

   621   apply(subgoal_tac " rsb @

   622     rs @

   623     rdistinct rsa

   624      (insert (RALTS rs)

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

   626                       rsb @

   627     rdistinct rs (set rsb) @

   628     rdistinct rsa

   629      (insert (RALTS rs)

   630        (set rsb)) ")

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

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

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

   634   

   635 

   636 

   637 

   638 lemma list_dlist_union:

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

   640   by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)

   641 

   642 lemma r_finite1:

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

   644   apply(induct r)

   645   apply simp+

   646    apply (metis list.set_intros(1))

   647   apply blast

   648   by simp

   649   

   650 

   651 

   652 lemma grewrite_singleton:

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

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

   655     apply simp

   656   apply (metis r_finite1)

   657   using grewrite.simps apply blast

   658   by simp

   659 

   660 

   661 

   662 lemma concat_rdistinct_equality1:

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

   664   apply(induct rs arbitrary: rsa rset)

   665    apply simp

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

   667    apply simp

   668   apply (simp add: insert_absorb)

   669   by auto

   670 

   671 

   672 lemma grewrites_rev_append:

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

   674   using grewritess_concat by auto

   675 

   676 lemma grewrites_inclusion:

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

   678   apply(induct rs arbitrary: rs1)

   679   apply simp

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

   681 

   682 lemma distinct_keeps_last:

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

   684   by (simp add: concat_rdistinct_equality1)

   685 

   686 lemma grewrites_shape2_aux:

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

   688        rsb @

   689        rdistinct (rs @ rsa)

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

   691                        rdistinct rs (set rsb) @

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

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

   694    apply (simp only:)

   695   prefer 2

   696   apply (simp add: Un_commute concat_rdistinct_equality1)

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

   698    apply simp

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

   700   apply (simp add: distinct_removes_middle3)

   701   apply(case_tac "x = RALTS rs")

   702    apply simp

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

   704    apply simp

   705     apply (simp add: concat_rdistinct_equality1)

   706   apply (simp add: concat_rdistinct_equality1)

   707   apply simp

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

   709   apply(drule_tac x = rsb in meta_spec)

   710   apply simp

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

   712   prefer 2

   713    apply (simp add: concat_rdistinct_equality1)

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

   715    apply simp

   716    apply (simp add: distinct_removes_last)

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

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

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

   720   apply(simp only:)

   721   apply(case_tac "x = RALTS rs")

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

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

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

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

   726   apply (metis append.assoc grewrites_inclusion)

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

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

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

   730   apply(simp only:)

   731   apply (metis append.assoc grewrites_rev_append)

   732   apply (simp add: insert_absorb)

   733    apply (simp add: distinct_keeps_last)+

   734   done

   735 

   736 lemma grewrites_shape2:

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

   738        rsb @

   739        rdistinct (rs @ rsa)

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

   741                        rdistinct rs (set rsb) @

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

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

   744   done

   745 

   746 lemma rdistinct_add_acc:

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

   748   apply(induct rs arbitrary: rsb rset rset2)

   749    apply simp

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

   751    apply simp

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

   753    apply simp

   754   apply (simp add: more_distinct1)

   755   apply simp

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

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

   758   

   759 

   760 lemma frewrite_fun1:

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

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

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

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

   765   prefer 2

   766   using spilled_alts_contained apply blast

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

   768   using greal_trans apply blast

   769   using rdistinct_add_acc apply presburger

   770   using flts_gstar grewritess_concat by auto

   771   

   772 lemma frewrite_rd_grewrites:

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

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

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

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

   777     apply(rule conjI)

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

   779   apply simp+

   780   using gstar0 apply fastforce

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

   782     apply (simp add: gstar0)

   783     prefer 2

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

   785   apply simp

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

   787     apply(erule exE)

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

   789    apply simp

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

   791    apply simp

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

   793    apply(rule conjI)

   794   using frewrite_fun1 apply force

   795   apply (metis frewrite_fun1 rdistinct_concat sup_ge2)

   796   apply(simp)

   797   apply(rule_tac x = 

   798  "rflts rsb @

   799                        rdistinct rs (set rsb) @

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

   801   apply(rule conjI)

   802    prefer 2

   803   using grewrites_shape2 apply force

   804   using frewrite_rd_grewrites_aux by blast

   805 

   806 

   807 lemma frewrite_simpeq2:

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

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

   810   using grewrites_equal_rsimp apply fastforce

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

   812 

   813 

   814 

   815 

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

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

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

   819 and deduplicated*)

   820 lemma frewrites_simpeq:

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

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

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

   824    apply simp

   825   using frewrite_simpeq2 by presburger

   826 

   827 

   828 lemma frewrite_single_step:

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

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

   831     apply simp

   832   using simp_flatten apply blast

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

   834 

   835 lemma grewrite_simpalts:

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

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

   838   using identity_wwo0 apply presburger

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

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

   841   apply simp

   842   apply(subst rsimp_alts_equal)

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

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

   845   apply (simp only:)

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

   847    apply simp

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

   849 

   850 

   851 lemma grewrites_simpalts:

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

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

   854    apply simp

   855   using grewrite_simpalts by presburger

   856 

   857 

   858 lemma simp_der_flts:

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

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

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

   862   using frewrites_simpeq apply presburger

   863   using early_late_der_frewrites by auto

   864 

   865 

   866 lemma simp_der_pierce_flts_prelim:

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

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

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

   870 

   871 

   872 lemma basic_regex_property1:

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

   874   apply(induct r rule: rsimp.induct)

   875   apply(auto)

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

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

   878 

   879 

   880 lemma inside_simp_seq_nullable:

   881   shows 

   882 "\<And>r1 r2.

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

   884         rnullable r1\<rbrakk>

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

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

   887   apply(case_tac "rsimp r1 = RONE")

   888    apply(simp)

   889   apply(subst basic_rsimp_SEQ_property1)

   890    apply (simp add: idem_after_simp1)

   891   apply(case_tac "rsimp r1 = RZERO")

   892   

   893   using basic_regex_property1 apply blast

   894   apply(case_tac "rsimp r2 = RZERO")

   895   

   896   apply (simp add: basic_rsimp_SEQ_property3)

   897   apply(subst idiot2)

   898      apply simp+

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

   900    apply simp

   901   using rsimp_idem apply presburger

   902   using der_simp_nullability by presburger

   903   

   904 

   905 

   906 lemma grewrite_ralts:

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

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

   909 

   910 lemma grewrites_ralts:

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

   912   apply(induct rule: grewrites.induct)

   913   apply simp

   914   using grewrite_ralts hreal_trans by blast

   915   

   916 

   917 lemma distinct_grewrites_subgoal1:

   918   shows "  

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

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

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

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

   923   using grewrites_ralts apply blast

   924   using grewrites.intros(2) by presburger

   925 

   926 lemma grewrites_ralts_rsimpalts:

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

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

   929    apply(case_tac rs)

   930   using hrewrite.intros(9) apply force

   931    apply(case_tac list)

   932   apply simp

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

   934    apply simp

   935   apply(case_tac rs2)

   936    apply simp

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

   938   apply(case_tac list)

   939    apply(simp)

   940   using distinct_grewrites_subgoal1 apply blast

   941   apply simp

   942   apply(case_tac rs3)

   943    apply simp

   944   using grewrites_ralts hrewrite.intros(9) apply blast

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

   946 

   947 lemma hrewrites_alts:

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

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

   950   apply simp

   951   using hrewrite.intros(6) by blast

   952 

   953 inductive 

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

   955 where

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

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

   958 

   959 

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

   961 

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

   963    apply(rule rs1)

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

   965   apply simp

   966   apply(rule hreal_trans)

   967    prefer 2

   968    apply(assumption)

   969   apply(drule hrewrites_alts)

   970   by auto

   971 

   972 

   973 corollary srewritescf_alt1: 

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

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

   976   using assms

   977   by (metis append_Nil srewritescf_alt)

   978 

   979 

   980 

   981 

   982 lemma trivialrsimp_srewrites: 

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

   984 

   985   apply(induction rs)

   986    apply simp

   987    apply(rule ss1)

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

   989 

   990 lemma hrewrites_list: 

   991   shows

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

   993   apply(induct x)

   994    apply(simp)+

   995   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)

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

   997 

   998   

   999 lemma hrewrite_simpeq:

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

  1001   apply(induct rule: hrewrite.induct)

  1002             apply simp+

  1003   apply (simp add: basic_rsimp_SEQ_property3)

  1004   apply (simp add: basic_rsimp_SEQ_property1)

  1005   using rsimp.simps(1) apply presburger

  1006         apply simp+

  1007   using flts_middle0 apply force

  1008 

  1009   

  1010   using simp_flatten3 apply presburger

  1011 

  1012   apply simp+

  1013   apply (simp add: idem_after_simp1)

  1014   using grewrite.intros(4) grewrite_equal_rsimp by presburger

  1015 

  1016 lemma hrewrites_simpeq:

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

  1018   apply(induct rule: hrewrites.induct)

  1019    apply simp

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

  1021    apply auto[1]

  1022   using hrewrite_simpeq by presburger

  1023   

  1024 

  1025 

  1026 lemma simp_hrewrites:

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

  1028   apply(induct r1)

  1029        apply simp+

  1030     apply(case_tac "rsimp r11 = RONE")

  1031      apply simp

  1032      apply(subst basic_rsimp_SEQ_property1)

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

  1034   using hreal_trans hrewrite.intros(3) apply blast

  1035   using hrewrites_seq_context apply presburger

  1036     apply(case_tac "rsimp r11 = RZERO")

  1037      apply simp

  1038   using hrewrite.intros(1) hrewrites_seq_context apply blast

  1039     apply(case_tac "rsimp r12 = RZERO")

  1040      apply simp

  1041   apply(subst basic_rsimp_SEQ_property3)

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

  1043     apply(subst idiot2)

  1044        apply simp+

  1045   using hrewrites_seq_contexts apply presburger

  1046    apply simp

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

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

  1049   using hreal_trans apply blast

  1050     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)

  1051 

  1052    apply (simp add: grewrites_ralts hrewrites_list)

  1053   by simp_all

  1054 

  1055 lemma interleave_aux1:

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

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

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

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

  1060   using rs1 srewritescf_alt1 ss1 ss2 apply presburger

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

  1062 

  1063 

  1064 

  1065 lemma rnullable_hrewrite:

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

  1067   apply(induct rule: hrewrite.induct)

  1068             apply simp+

  1069      apply blast

  1070     apply simp+

  1071   done

  1072 

  1073 

  1074 lemma interleave1:

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

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

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

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

  1079           apply simp

  1080           apply(subst interleave_aux1)

  1081           apply simp

  1082          apply(case_tac "rnullable r1")

  1083           apply simp

  1084   

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

  1086   

  1087          apply (simp add: hrewrites_seq_context rnullable_hrewrite)

  1088         apply(case_tac "rnullable r1")

  1089   apply simp

  1090   

  1091   using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger

  1092   apply simp

  1093   using hr_in_rstar hrewrites_seq_context2 apply blast

  1094        apply simp

  1095   

  1096   using hrewrites_alts apply auto[1]

  1097   apply simp

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

  1099   apply simp

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

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

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

  1103   apply simp

  1104   using hrewrite.intros(11) by auto

  1105 

  1106 lemma interleave_star1:

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

  1108   apply(induct rule : hrewrites.induct)

  1109    apply simp

  1110   by (meson hreal_trans interleave1)

  1111 

  1112 

  1113 

  1114 lemma inside_simp_removal:

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

  1116   apply(induct r)

  1117        apply simp+

  1118     apply(case_tac "rnullable r1")

  1119      apply simp

  1120   

  1121   using inside_simp_seq_nullable apply blast

  1122     apply simp

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

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

  1125   using hrewrites_simpeq apply presburger

  1126   using interleave_star1 simp_hrewrites apply presburger

  1127   by simp_all

  1128   

  1129 

  1130 

  1131 

  1132 lemma rders_simp_same_simpders:

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

  1134   apply(induct s rule: rev_induct)

  1135    apply simp