497 

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

   499   where

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

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

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

   503 

   504 

   505 inductive 

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

   507 where 

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

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

   510 

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

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

   513  

   514 lemma freal_trans[trans]: 

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

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

   517   using a2 a1

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

   519   apply(auto)

   520   done

   521 

   522 

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

   524   by (meson fr_in_rstar freal_trans)

   525 

   526 

   527 lemma frewrite_append:

   528   shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"

   529   apply(induct rs)

   530   apply simp+

   531   oops

   532 

   533 

   534 lemma frewrites_cons:

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

   536 

   537   oops

   538 

   539 lemma frewrites_append:

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

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

   542    apply simp

   543   oops

   544 

   545 

   546 

   547 lemma frewrites_concat:

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

   549   apply(induct rs1 rs2 rule: frewrite.induct)

   550     apply(simp)

   551   apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)")

   552   prefer 2

   553   using frewrite.intros(1) apply blast

   554     apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)")

   555   using many_steps_later apply blast

   556 

   557 

   558 

   559 

   560 

   561 

   562 

   563 lemma many_steps_later1:

   564   shows " \<lbrakk>rs1 \<leadsto>f* rs2\<rbrakk>

   565        \<Longrightarrow> (RONE # rs1) \<leadsto>f* (RONE # rs2)"

   566   oops

   567 

   568 lemma early_late_der_frewrites:

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

   570   apply(induct rs)

   571    apply simp

   572   apply(case_tac a)

   573        apply simp+

   574   using frewrite.intros(1) many_steps_later apply blast

   575      apply(case_tac "x = x3")

   576      apply simp

   577   

   578 

   579 

   580 

   581 

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

   583   where

   584   "alt_set (RALTS rs) = set rs"

   585 | "alt_set r = {r}"

   586 

   587 

   588 

   589 lemma rd_flts_set:

   590   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 (insert RZERO (rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f*  

   591                           rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))"

   592   by (meson frewrite.intros(2) frewrites.simps)

   593   

   594 lemma rd_flts_set2:

   595   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ((rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f*  

   596                           rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))"

   597   using frewrite.intros(2) by blast

   598 

   599 lemma rd_flts_incorrect:

   600   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 rset \<leadsto>f* rdistinct rs2 rset"

   601   sledgehammer

   602   by (smt (verit, ccfv_threshold) frewrites.simps)

   603 

   604 lemma flts_does_rewrite:

   605   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rflts rs1 = rflts rs2"

   606   oops

   607