--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/Rsimp.thy	Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,171 @@
+theory Rsimp imports "Lexer"
+begin
+
+datatype rrexp = 
+  RZERO
+| RONE 
+| RCHAR char
+| RSEQ rrexp rrexp
+| RALTS "rrexp list"
+| RSTAR rrexp
+
+abbreviation
+  "RALT r1 r2 \<equiv> RALTS [r1, r2]"
+
+
+fun
+  RL :: "rrexp \<Rightarrow> string set"
+where
+  "RL (RZERO) = {}"
+| "RL (RONE) = {[]}"
+| "RL (RCHAR c) = {[c]}"
+| "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"
+| "RL (RALTS rs) = (\<Union> (set (map RL rs)))"
+| "RL (RSTAR r) = (RL r)\<star>"
+
+
+
+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 nonalt :: "rrexp \<Rightarrow> bool"
+  where
+  "nonalt (RALTS  rs) = False"
+| "nonalt r = True"
+
+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"
+
+fun rsize :: "rrexp \<Rightarrow> nat" where
+  "rsize RZERO = 1"
+| "rsize (RONE) = 1" 
+| "rsize (RCHAR  c) = 1"
+| "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"
+| "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"
+| "rsize (RSTAR  r) = Suc (rsize r)"
+
+abbreviation rsizes where
+  "rsizes rs \<equiv> sum_list (map rsize rs)"
+
+fun nonnested :: "rrexp \<Rightarrow> bool"
+  where
+  "nonnested (RALTS []) = True"
+| "nonnested (RALTS ((RALTS rs1) # rs2)) = False"
+| "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"
+| "nonnested r = True"
+
+
+fun good :: "rrexp \<Rightarrow> bool" where
+  "good RZERO = False"
+| "good (RONE) = True" 
+| "good (RCHAR c) = True"
+| "good (RALTS []) = False"
+| "good (RALTS [r]) = False"
+| "good (RALTS (r1 # r2 # rs)) = 
+    ((distinct ( (r1 # r2 # rs))) \<and>
+     (\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"
+| "good (RSEQ RZERO _) = False"
+| "good (RSEQ RONE _) = False"
+| "good (RSEQ  _ RZERO) = False"
+| "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+| "good (RSTAR r) = True"
+
+fun nonazero :: "rrexp \<Rightarrow> bool"
+  where
+  "nonazero RZERO = False"
+| "nonazero r = True"
+
+
+
+
+
+
+lemma basic_rsimp_SEQ_property1:
+  shows "rsimp_SEQ RONE r = r"
+  apply(induct r)
+       apply simp+
+  done
+
+
+lemma basic_rsimp_SEQ_property3:
+  shows "rsimp_SEQ r RZERO = RZERO"  
+  using rsimp_SEQ.elims by blast
+
+
+lemma rsimpalts_conscons:
+  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)
+
+
+end
\ No newline at end of file