--- a/thys2/BasicIdentities.thy Wed Mar 30 11:18:51 2022 +0100
+++ b/thys2/BasicIdentities.thy Fri Apr 01 23:17:40 2022 +0100
@@ -104,6 +104,10 @@
shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"
by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))
+lemma rsimp_alts_equal:
+ shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) "
+ by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)
+
fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
where
@@ -330,17 +334,7 @@
apply(simp add: rders_append rders_simp_append)
using inside_simp_removal by blast
-lemma simp_helps_der_pierce:
- shows " rsimp
- (rder x
- (rsimp_ALTs rs)) =
- rsimp
- (rsimp_ALTs
- (map (rder x )
- rs
- )
- )"
- sorry
+
lemma rders_simp_one_char:
@@ -428,9 +422,7 @@
-lemma simp_flatten2:
- shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
- sorry
+
lemma simp_flatten:
--- a/thys2/ClosedForms.thy Wed Mar 30 11:18:51 2022 +0100
+++ b/thys2/ClosedForms.thy Fri Apr 01 23:17:40 2022 +0100
@@ -10,6 +10,10 @@
apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
by simp
+lemma identity_wwo0:
+ shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
+ by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+
lemma distinct_removes_last:
shows "\<lbrakk>a \<in> set as\<rbrakk>
@@ -92,33 +96,15 @@
by (metis distinct_removes_middle(1))
lemma distinct_removes_list:
- shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+ shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
apply(induct rs)
apply simp+
- apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}")
+ apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
prefer 2
apply (metis append_Cons append_Nil distinct_removes_middle(1))
by presburger
-
-lemma simp_rdistinct_f: shows
-"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) =
- rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) "
- apply(induct rs arbitrary: rset)
- apply simp
- apply(case_tac "a \<in> rset")
- apply(case_tac " f a \<in> frset")
- apply simp
- apply blast
- apply(subgoal_tac "f a \<notin> frset")
- apply(simp)
- apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
- prefer 2
- apply (meson image_insert)
-
- oops
-
lemma spawn_simp_rsimpalts:
shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
apply(cases rs)
@@ -139,90 +125,6 @@
apply(subst rsimp_idem)+
by (metis comp_apply rsimp_idem)
-lemma spawn_simp_distinct:
- shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))
-\<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))
-\<and> rsimp (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"
- apply(induct rs arbitrary: rsa rsa1 a1 rsc)
- apply simp
- apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")
- prefer 2
-
-
-
-
- oops
-
-lemma inv_one_derx:
- shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
- apply(case_tac r2)
- apply simp+
- using rrexp.distinct(1) apply presburger
- apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
- apply simp+
- done
-
-lemma shape_of_derseq:
- shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"
- using rder.simps(5) by presburger
-lemma shape_of_derseq2:
- shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"
- by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)
-
-lemma alts_preimage_case1:
- shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"
- apply(case_tac r)
- apply simp+
- apply (metis rrexp.simps(12) rrexp.simps(20))
- apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)
- apply auto[1]
- by auto
-
-lemma alts_preimage_case2:
- shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"
- apply(case_tac r)
- apply simp+
- apply (metis rrexp.distinct(15) rrexp.distinct(7))
- apply simp
- apply auto[1]
- by auto
-
-lemma alts_preimage_case2_2:
- shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"
- using alts_preimage_case2 by blast
-
-lemma alts_preimage_case3:
- shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"
- using alts_preimage_case2 by blast
-
-lemma star_seq:
- shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"
- using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger
-
-lemma language_equality_id1:
- shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"
- apply (subst star_seq)
- apply simp
- done
-
-
-
-lemma distinct_der_set:
- shows "(rder x) ` rset = dset \<Longrightarrow>
-rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
- apply(induct rs arbitrary: rset dset)
- apply simp
- apply(case_tac "a \<in> rset")
- apply(subgoal_tac "rder x a \<in> dset")
- prefer 2
- apply blast
- apply simp
- apply(case_tac "rder x a \<notin> dset")
- prefer 2
- apply simp
-
- oops
-
lemma map_concat_cons:
shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
by simp
@@ -231,29 +133,6 @@
shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
by simp
-lemma simp_more_flts:
- shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))"
-
- oops
-
-lemma simp_more_distinct1:
- shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))"
- apply(induct rs)
- apply simp
- apply simp
- oops
-
-
-(*
-\<and>
- rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) =
- rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))
-*)
-lemma simp_removes_duplicate2:
- shows "a "
-
- oops
-
lemma flts_removes0:
shows " rflts (rs @ [RZERO]) =
rflts rs"
@@ -469,13 +348,6 @@
apply simp
using rsimpalts_conscons by presburger
-lemma no0_flts:
- shows "RZERO \<notin> set (rflts rs)"
- apply (induct rs)
- apply simp
- apply(case_tac a)
- apply simp+
- oops
@@ -641,11 +513,78 @@
using grewrites_append apply blast
by (meson greal_trans grewrites.simps grewrites_concat)
+fun alt_set:: "rrexp \<Rightarrow> rrexp set"
+ where
+ "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
+| "alt_set r = {r}"
+
+lemma alt_set_has_all:
+ shows "RALTS rs \<in> alt_set rx \<Longrightarrow> set rs \<subseteq> alt_set rx"
+ apply(induct rx arbitrary: rs)
+ apply simp_all
+ apply(rename_tac rSS rss)
+ using in_mono by fastforce
+
+
+
+
+lemma grewrite_equal_rsimp:
+ shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
+ rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk>
+ \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
+ rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))"
+ apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct)
+ apply simp
+ apply (metis append_Cons append_Nil flts_middle0)
+ apply(case_tac "rsimp r \<in> rset")
+ apply simp
+ oops
+
+
+
+lemma grewrite_equal_rsimp:
+ shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ apply(induct rs1 rs2 rule: grewrite.induct)
+ apply simp
+ using simp_flatten apply blast
+ prefer 2
+ apply (smt (verit) append.assoc append_Cons in_set_conv_decomp simp_removes_duplicate2)
+ apply simp
+ apply(case_tac "rdistinct (rflts (map rsimp rs1)) {}")
+ apply(case_tac "rsimp r = RZERO")
+ apply simp
+ apply(case_tac "\<exists>rs. rsimp r = RALTS rs")
+ prefer 2
+
+ apply(subgoal_tac "rdistinct (rflts (rsimp r # map rsimp rs1)) {} =
+ rsimp r # rdistinct (rflts (map rsimp rs1)) {rsimp r}")
+ prefer 2
+ apply (simp add: list.inject rflts_def_idiot)
+ apply(simp only:)
+
+ sorry
+
+
lemma grewrites_equal_rsimp:
shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ apply (induct rs1 rs2 rule: grewrites.induct)
apply simp
+ using grewrite_equal_rsimp by presburger
+
+
+
+
+lemma grewrites_equal_simp_2:
+ shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
sorry
+lemma grewrites_last:
+ shows "r # [RALTS rs] \<leadsto>g* r # rs"
+ by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
+
+lemma simp_flatten2:
+ shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
+ using grewrites_equal_rsimp grewrites_last by blast
lemma frewrites_middle:
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"
@@ -674,18 +613,9 @@
by (simp add: frewrites_cons)
-fun alt_set:: "rrexp \<Rightarrow> rrexp set"
- where
- "alt_set (RALTS rs) = set rs"
-| "alt_set r = {r}"
-lemma rd_flts_set:
- shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset))) \<leadsto>g*
- rdistinct rs2 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset)))"
- sorry
-
lemma with_wo0_distinct:
shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
apply(induct rs arbitrary: rset)
@@ -711,50 +641,126 @@
apply (simp add: frewrites_cons)
done
+(*Interesting lemma: not obvious but easily proven by sledgehammer*)
+
+
+
+(*lemma induction last rule not go through
+ example:
+r #
+ rdistinct rs1
+ (insert RZERO
+ (insert r
+ (rset \<union>
+ \<Union> (alt_set `
+ rset)))) \<leadsto>g* r #
+ rdistinct rs2
+ (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset))))
+ rs2 = [+rs] rs3 = rs,
+r = +rs
+[] \<leadsto>g* rs which is wrong
+*)
lemma frewrite_with_distinct:
shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>
\<Longrightarrow> rdistinct rs2
- (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f*
+ (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>g*
rdistinct rs3
(insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
- apply(induct rs2 rs3 rule: frewrite.induct)
+ apply(induct rs2 rs3 arbitrary: rset rule: frewrite.induct)
apply(case_tac "RZERO \<in> (rset \<union> \<Union> (alt_set ` rset))")
apply simp
apply simp
- apply(case_tac "RALTS rs \<in> rset")
- apply simp
- apply(subgoal_tac "\<forall>r \<in> set rs. r \<in> \<Union> (alt_set ` rset)")
- apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) =
- rdistinct rsa (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))")
- using frewrites.intros(1) apply presburger
- apply (simp add: rdistinct_concat2)
- apply simp
- using alt_set.simps(1) apply blast
- apply(case_tac "RALTS rs \<in> rset \<union> \<Union>(alt_set ` rset)")
-
+
- sorry
+ oops
+
lemma frewrites_with_distinct:
- shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
- rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>f*
- rs2 @ (rdistinct rsb (insert RZERO (set rs2 \<union> \<Union>(alt_set ` (set rs2) ))))"
+ shows "\<lbrakk>rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow>
+( (rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g*
+ rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))
+\<or> ( rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g*
+ rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))
+ )
+"
+ apply(induct rsa rsb arbitrary: rs1 rule: frewrite.induct)
+ apply simp
+ apply(case_tac "RALTS rs \<in> set rs1")
+ apply(subgoal_tac "set rs \<subseteq> \<Union> (alt_set `set rs1)")
+ apply (metis (full_types) Un_iff Un_insert_left
+Un_insert_right grewrites.intros(1) le_supI2 rdistinct.simps(2) rdistinct_concat)
+ apply (metis Un_subset_iff Union_upper alt_set.simps(1) imageI)
+
+ apply(case_tac "RALTS rs \<in> \<Union> (alt_set ` set rs1)")
+ apply simp
+ apply (smt (z3) UN_insert Un_iff alt_set.simps(1) alt_set_has_all dual_order.trans grewrites.intros(1) insert_absorb rdistinct_concat subset_insertI)
+
+
+ oops
+
+
+
+lemma rd_flts_set:
+ shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset))) \<leadsto>g*
+ rdistinct rs2 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset)))"
apply(induct rs1 rs2 rule: frewrites.induct)
apply simp
-
+ oops
+
+lemma frewrite_simpeq:
+ shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ apply(induct rs1 rs2 rule: frewrite.induct)
+ apply simp
+ using simp_flatten apply presburger
+ by (meson grewrites_cons grewrites_equal_rsimp grewrites_equal_simp_2)
+
+lemma frewrite_rd_grewrites:
+ shows "rs1 \<leadsto>f rs2 \<Longrightarrow>
+\<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) "
+ apply(induct rs1 rs2 rule: frewrite.induct)
+ apply(rule_tac x = "rs" in exI)
+ apply(rule conjI)
+ apply(rule gr_in_rstar)
+ apply(rule grewrite.intros)
+ apply(rule grewrites.intros)
+ using grewrite.intros(2) apply blast
+ by (meson grewrites_cons)
- sorry
+
+lemma frewrites_rd_grewrites:
+ shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
+\<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3)"
+ apply(induct rs1 rs2 rule: frewrites.induct)
+ apply simp
+ apply(rule exI)
+ apply(rule grewrites.intros)
+ by (metis frewrite_simpeq grewrites_equal_rsimp grewrites_equal_simp_2)
+
+
+
+
+lemma frewrite_simpeq2:
+ shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
+ apply(induct rs1 rs2 rule: frewrite.induct)
+ apply simp
+ apply (simp add: distinct_flts_no0)
+ apply simp
(*a more refined notion of \<leadsto>* is needed,
this lemma fails when rs1 contains some RALTS rs where elements
of rs appear in later parts of rs1, which will be picked up by rs2
and deduplicated*)
-lemma wrong_frewrites_with_distinct2:
+lemma frewrites_simpeq:
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
- (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}"
- oops
+ rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
+ apply(induct rs1 rs2 rule: frewrites.induct)
+ apply simp
+
+ sorry
+
+
lemma frewrite_single_step:
shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
@@ -769,11 +775,38 @@
apply simp
using frewrite_single_step by presburger
+lemma grewrite_simpalts:
+ shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ apply(induct rs2 rs3 rule : grewrite.induct)
+ using identity_wwo0 apply presburger
+ apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten)
+ apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3))
+ apply simp
+ apply(subst rsimp_alts_equal)
+ apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []")
+ apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]")
+ apply (simp only:)
+ apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2))
+ apply simp
+ 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)
+
+
+lemma grewrites_simpalts:
+ shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+ apply(induct rs2 rs3 rule: grewrites.induct)
+ apply simp
+ using grewrite_simpalts by presburger
+(*
lemma frewrites_dB_wwo0_simp:
shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO}
\<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
sorry
+*)
+lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) =
+ rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) "
+
+ sorry
@@ -782,13 +815,28 @@
rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO}
- \<leadsto>f* rdistinct ( rflts (map (rder x) rs)) {RZERO}")
+ \<leadsto>g* rdistinct ( rflts (map (rder x) rs)) {RZERO}")
apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {}))
= rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))")
apply meson
- using frewrites_dB_wwo0_simp apply blast
- using frewrites_with_distinct2 apply blast
- using early_late_der_frewrites by blast
+ apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2))
+ sorry
+
+
+
+
+
+
+
+
+lemma simp_der_pierce_flts_prelim:
+ shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {}))
+ = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
+ apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>g* rflts (map (rder x) rs)")
+ apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} \<leadsto>g* rdistinct (rflts (map (rder x) rs)) {RZERO}")
+ using grewrites_equal_simp_2 grewrites_simpalts simp_der_flts apply blast
+ apply (simp add: early_late_der_frewrites frewrites_with_distinct2_grewrites)
+ using early_late_der_frewrites frewrites_equivalent_simp grewrites_equal_simp_2 by blast
lemma simp_der_pierce_flts:
@@ -798,9 +846,7 @@
rsimp (
rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
)"
-
- sorry
-
+ using simp_der_pierce_flts_prelim by presburger
@@ -1119,10 +1165,7 @@
apply simp
apply fastforce
apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
- sledgehammer
- (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct)
-
- *)
+ using simp_der_pierce_flts by blast
lemma alts_closed_form_variant: shows
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s =
@@ -1167,4 +1210,16 @@
apply force
by presburger
+lemma simp_helps_der_pierce:
+ shows " rsimp
+ (rder x
+ (rsimp_ALTs rs)) =
+ rsimp
+ (rsimp_ALTs
+ (map (rder x )
+ rs
+ )
+ )"
+ sorry
+
end
\ No newline at end of file