# HG changeset patch # User Chengsong # Date 1656005534 -3600 # Node ID feae84f6647259bce970b8f0d891ae56c002fcec # Parent 6e97f4aa7cd0ffb9600f709afd0e7e871305c80b before alternating rewriting relation diff -r 6e97f4aa7cd0 -r feae84f66472 thys3/BlexerSimp.thy --- a/thys3/BlexerSimp.thy Thu Jun 23 16:59:58 2022 +0100 +++ b/thys3/BlexerSimp.thy Thu Jun 23 18:32:14 2022 +0100 @@ -572,6 +572,7 @@ done + lemma central: shows "bders r s \<leadsto>* bders_simp r s" proof(induct s arbitrary: r rule: rev_induct) @@ -757,6 +758,57 @@ *) +lemma rewrites_to_bsimpStrong: + shows "r \<leadsto>* bsimpStrong6 r" +proof (induction r rule: bsimpStrong6.induct) + case (1 bs1 r1 r2) + have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact + have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact + { assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO" + with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto + then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" + by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) + then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto + } + moreover + { assume "\<exists>bs. bsimpStrong6 r1 = AONE bs" + then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast + with IH1 have "r1 \<leadsto>* AONE bs" by simp + then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast + with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)" + using rewrites_fuse by (meson rrewrites_trans) + then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp + then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as) + } + moreover + { assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)" + then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" + by (simp add: bsimp_ASEQ1) + then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 + by (metis rrewrites_trans star_seq star_seq2) + then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp + } + ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry +next + case (2 bs1 rs) + have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact + then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) + also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) + also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger) + finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" + using contextrewrites0 by auto + also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" + by (simp add: bsimp_AALTs_rewrites) + finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry +qed (simp_all) + +lemma bders_simp_appendStrong : + shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" + apply(induct s1 arbitrary: s2 rule: rev_induct) + apply simp + apply auto + done + lemma centralStrong: shows "bders r s \<leadsto>* bdersStrong6 r s" @@ -770,9 +822,9 @@ also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH by (simp add: rewrites_preserves_bder) also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH - by (simp add: rewrites_to_bsimp) - finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" - by (simp add: bders_simp_append) + by (simp add: rewrites_to_bsimpStrong) + finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])" + by (simp add: bders_simp_appendStrong) qed lemma mainStrong: