# HG changeset patch
# User Chengsong
# Date 1656007039 -3600
# Node ID 9972877a3f397820d8bc3b9076a042c3319b17f0
# Parent  e5db23c100ea195e22c81cab0cafabf3ba86ab19
bsimp def removed

diff -r e5db23c100ea -r 9972877a3f39 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jun 23 18:50:59 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 18:57:19 2022 +0100
@@ -2,34 +2,6 @@
   imports Blexer 
 begin
 
-fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list"
-  where
-  "distinctWith [] eq acc = []"
-| "distinctWith (x # xs) eq acc = 
-     (if (\<exists> y \<in> acc. eq x y) then distinctWith xs eq acc 
-      else x # (distinctWith xs eq ({x} \<union> acc)))"
-
-
-fun eq1 ("_ ~1 _" [80, 80] 80) where  
-  "AZERO ~1 AZERO = True"
-| "(AONE bs1) ~1 (AONE bs2) = True"
-| "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)"
-| "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)"
-| "(AALTs bs1 []) ~1 (AALTs bs2 []) = True"
-| "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))"
-| "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2"
-| "_ ~1 _ = False"
-
-
-
-lemma eq1_L:
-  assumes "x ~1 y"
-  shows "L (erase x) = L (erase y)"
-  using assms
-  apply(induct rule: eq1.induct)
-  apply(auto elim: eq1.elims)
-  apply presburger
-  done
 
 fun flts :: "arexp list \<Rightarrow> arexp list"
   where 
@@ -70,36 +42,6 @@
 | "bsimp_AALTs bs1 [r] = fuse bs1 r"
 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"
 
-
-
-
-fun bsimp :: "arexp \<Rightarrow> arexp" 
-  where
-  "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
-| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) "
-| "bsimp r = r"
-
-
-fun 
-  bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
-where
-  "bders_simp r [] = r"
-| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
-
-definition blexer_simp where
- "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
-                    decode (bmkeps (bders_simp (intern r) s)) r else None"
-
-
-
-lemma bders_simp_append:
-  shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
-  apply(induct s1 arbitrary: r s2)
-  apply(simp_all)
-  done
-
-
-
 lemma bmkeps_fuse:
   assumes "bnullable r"
   shows "bmkeps (fuse bs r) = bs @ bmkeps r"