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

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

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

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

   510 

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

   512   where

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

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

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

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

   517 

   518 

   519 inductive 

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

   521 where 

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

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

   524 (*

   525 inductive 

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

   527 where 

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

   529 *)

   563 

   583 lemma frewrites_middle:

   564 

   584   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"

   585   by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3))

   586 

   587 lemma frewrites_alt:

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

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

   584   apply simp

   608      apply simp+

   585 

   609      apply (simp add: frewrites_alt)

   586 

   610   apply (simp add: frewrites_cons)

   611    apply (simp add: frewrites_append)

   612   by (simp add: frewrites_cons)

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

   625 

   626   oops

   627 

   628 

   604   using frewrite.intros(2) by blast

   633   oops

   605 

   634 

   606 lemma rd_flts_incorrect:

   635 

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

   608   sledgehammer

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

   615 lemma rflts_fltsder_derflts:

   641 lemma with_wo0_distinct:

   616   shows "rflts (map rsimp (rdistinct (map (rder x3) (rflts rs)) rset)) = 

   642   shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"

   617          rflts (map rsimp (rdistinct (rflts (map (rder x3) rs)) rset))"

   643   apply(induct rs arbitrary: rset)

   618   sorry

   644    apply simp

   645   apply(case_tac a)

   646   apply(case_tac "RZERO \<in> rset")

   647         apply simp+

   648   using fr_in_rstar frewrite.intros(1) apply presburger

   649   apply (case_tac "RONE \<in> rset")

   650        apply simp+

   651   using frewrites_cons apply presburger

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

   653   apply simp

   654   apply (simp add: frewrites_cons)

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

   656   apply simp

   657   apply (simp add: frewrites_cons)

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

   659   apply simp

   660   apply (simp add: frewrites_cons)

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

   662   apply simp

   663   apply (simp add: frewrites_cons)

   664   done

   665 

   666 lemma rdistinct_concat:

   667   shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"

   668   apply(induct rs)

   669    apply simp+

   670   done

   671 

   672 lemma rdistinct_concat2:

   673   shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"

   674   by (simp add: rdistinct_concat subsetI)

   675 

   676 lemma frewrite_with_distinct:

   677   shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>

   678        \<Longrightarrow> rdistinct rs2

   679             (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* 

   680            rdistinct rs3 

   681             (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"

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

   683     apply(case_tac "RZERO \<in>  (rset \<union> \<Union> (alt_set ` rset))")

   684   apply simp

   685     apply simp

   686    apply(case_tac "RALTS rs \<in> rset")

   687     apply simp

   688   apply(subgoal_tac "\<forall>r \<in> set rs. r \<in> \<Union> (alt_set ` rset)")

   689   apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) = 

   690                        rdistinct rsa (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))")

   691   using frewrites.intros(1) apply presburger

   692      apply (simp add: rdistinct_concat2)

   693     apply simp

   694   using alt_set.simps(1) apply blast

   695    apply(case_tac "RALTS rs \<in> rset \<union> \<Union>(alt_set ` rset)")

   696   

   697 

   698   sorry

   699 

   700 

   701 lemma frewrites_with_distinct:

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

   703  rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>f* 

   704  rs2 @ (rdistinct rsb (insert RZERO (set rs2 \<union> \<Union>(alt_set ` (set rs2) ))))"

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

   706    apply simp

   707   

   708 

   709   sorry

   710 

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

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

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

   714 and deduplicated*)

   715 lemma wrong_frewrites_with_distinct2:

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

   717  (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}"

   718   oops

   719 

   720 lemma frewrite_single_step:

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

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

   723     apply simp

   724   using simp_flatten apply blast

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

   726 

   727 lemma frewrites_equivalent_simp:

   728   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"

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

   730    apply simp

   731   using frewrite_single_step by presburger

   732 

   733 lemma frewrites_dB_wwo0_simp:

   734   shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO} 

   735          \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"

   736 

   737   sorry

   738 

   624 

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

   625   apply(induct rs)

   745    apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} 

   626    apply simp

   746                     \<leadsto>f* rdistinct ( rflts (map (rder x) rs)) {RZERO}")

   627   apply(case_tac a)

   747   apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) 

   628        apply simp+

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

   629       prefer 2

   749   apply meson

   630   apply simp

   750   using frewrites_dB_wwo0_simp apply blast

   631       apply(case_tac "RZERO \<in> rset")

   751   using frewrites_with_distinct2 apply blast

   632        apply simp+

   752   using early_late_der_frewrites by blast

   633   using distinct_flts_no0 apply presburger

   634      apply (case_tac "x = x3")

   635   prefer 2

   636   apply simp

   637   using distinct_flts_no0 apply presburger

   638   apply(case_tac "RONE \<in> rset")

   639      apply simp+

   640   

   641   sorry