# HG changeset patch
# User Chengsong
# Date 1644165857 0
# Node ID a2887a9e853965ae46c941a419d7c14f00f913e0
# Parent  57182b36ec0193d8aa91f696e6169836bf971043
rdersetc.

diff -r 57182b36ec01 -r a2887a9e8539 thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Sun Feb 06 00:02:04 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Sun Feb 06 16:44:17 2022 +0000
@@ -1442,7 +1442,8 @@
   apply(induct r rule: bsimp.induct)
   apply(auto)
   using bsimp_ASEQ_idem apply presburger
-  oops
+  sorry
+
 
 lemma neg:
   shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and>  (r2 \<leadsto>* bsimp r1) )"
@@ -1453,7 +1454,6 @@
 
 
 
-
 lemma reduction_always_in_bsimp:
   shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False"
   apply(erule rrewrite.cases)
@@ -1462,6 +1462,8 @@
 
   oops
 
+
+
 (*
 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] 
 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto>
@@ -1478,10 +1480,173 @@
     r' \<leadsto>* bsimp bsimp r
 size bsimp r > size r' \<ge> size bsimp bsimp r*)
 
-export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
+fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list"
+  where
+"orderedSufAux (Suc 0) ss = Nil"
+|"orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)"
+|"orderedSufAux 0 ss = Nil"
+
+fun 
+orderedSuf :: "char list \<Rightarrow> char list list"
+where
+"orderedSuf s = orderedSufAux (length s) s"
+
+lemma shape_of_suf_2list:
+  shows "orderedSuf [c1, c2] = [[c2]]"
+  apply auto
+  done
+
+
+lemma shape_of_suf_3list:
+  shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3]]"
+  apply auto
+  done
+
+
+
+datatype rrexp = 
+  RZERO
+| RONE 
+| RCHAR char
+| RSEQ rrexp rrexp
+| RALTS "rrexp list"
+| RSTAR rrexp
+
+abbreviation
+  "RALT r1 r2 \<equiv> RALTS [r1, r2]"
+
+fun 
+  rerase :: "arexp \<Rightarrow> rrexp"
+where
+  "rerase AZERO = RZERO"
+| "rerase (AONE _) = RONE"
+| "rerase (ACHAR _ c) = RCHAR c"
+| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
+| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
+| "rerase (ASTAR _ r) = RSTAR (rerase r)"
+
+
+
+
+fun
+ rnullable :: "rrexp \<Rightarrow> bool"
+where
+  "rnullable (RZERO) = False"
+| "rnullable (RONE  ) = True"
+| "rnullable (RCHAR   c) = False"
+| "rnullable (RALTS   rs) = (\<exists>r \<in> set rs. rnullable r)"
+| "rnullable (RSEQ  r1 r2) = (rnullable r1 \<and> rnullable r2)"
+| "rnullable (RSTAR   r) = True"
+
+
+fun
+ rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
+where
+  "rder c (RZERO) = RZERO"
+| "rder c (RONE) = RZERO"
+| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
+| "rder c (RALTS rs) = RALTS (map (rder c) rs)"
+| "rder c (RSEQ r1 r2) = 
+     (if rnullable r1
+      then RALT   (RSEQ (rder c r1) r2) (rder c r2)
+      else RSEQ   (rder c r1) r2)"
+| "rder c (RSTAR r) = RSEQ  (rder c r) (RSTAR r)"
+
+
+fun 
+  rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+where
+  "rders r [] = r"
+| "rders r (c#s) = rders (rder c r) s"
+
+fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list"
+  where
+  "rdistinct [] acc = []"
+| "rdistinct (x#xs)  acc = 
+     (if x \<in> acc then rdistinct xs  acc 
+      else x # (rdistinct xs  ({x} \<union> acc)))"
+
+
+fun rflts :: "rrexp list \<Rightarrow> rrexp list"
+  where 
+  "rflts [] = []"
+| "rflts (RZERO # rs) = rflts rs"
+| "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"
+| "rflts (r1 # rs) = r1 # rflts rs"
+
+
+fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"
+  where
+  "rsimp_ALTs  [] = RZERO"
+| "rsimp_ALTs [r] =  r"
+| "rsimp_ALTs rs = RALTS rs"
+
+fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
+  where
+  "rsimp_SEQ  RZERO _ = RZERO"
+| "rsimp_SEQ  _ RZERO = RZERO"
+| "rsimp_SEQ RONE r2 = r2"
+| "rsimp_SEQ r1 r2 = RSEQ r1 r2"
+
+
+fun rsimp :: "rrexp \<Rightarrow> rrexp" 
+  where
+  "rsimp (RSEQ r1 r2) = rsimp_SEQ  (rsimp r1) (rsimp r2)"
+| "rsimp (RALTS rs) = rsimp_ALTs  (rdistinct (rflts (map rsimp rs))  {}) "
+| "rsimp r = r"
+
+
+fun 
+  rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+where
+  "rders_simp r [] = r"
+| "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"
+
+
+lemma rerase_bsimp:
+  shows "rerase (bsimp r) = rsimp (rerase r)"
+  apply(induct r)
+       apply auto
+
+
+  sorry
+
+lemma rerase_bder:
+  shows "rerase (bder c r) = rder c (rerase r)"
+  apply(induct r)
+       apply auto
+  sorry
+
+lemma rders_shape:
+  shows "rders_simp (RSEQ r1 r2) s = 
+         rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
+           (map (rders r2) (orderedSuf s))) )"
+  sorry
+
+  
+lemma ders_simp_commute:
+  shows "rerase (bsimp (bders_simp r s)) = rerase (bsimp (bders r s))"
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply simp
+  apply (simp add: bders_simp_append bders_append )
+  apply (simp add: rerase_bsimp)
+  apply (simp add: rerase_bder)
+  apply (simp add: rders_shape)
+  sledgehammer
+  oops
+
 
 
 unused_thms
+lemma seq_ders_shape:
+  shows "E"
+
+  oops
+
+(*rsimp (rders (RSEQ r1 r2) s) =
+         rsimp RALT [RSEQ (rders r1 s) r2, rders r2 si, ...]
+         where si is the i-th shortest suffix of s such that si \<in> L r2"
+*)
 
 
 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)