5 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list"

     6   where

     7   "distinctWith [] eq acc = []"

     8 | "distinctWith (x # xs) eq acc = 

     9      (if (\<exists> y \<in> acc. eq x y) then distinctWith xs eq acc 

    10       else x # (distinctWith xs eq ({x} \<union> acc)))"

    11 

    12 

    13 fun eq1 ("_ ~1 _" [80, 80] 80) where  

    14   "AZERO ~1 AZERO = True"

    15 | "(AONE bs1) ~1 (AONE bs2) = True"

    16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)"

    17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)"

    18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True"

    19 | "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))"

    20 | "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2"

    21 | "_ ~1 _ = False"

    22 

    23 

    24 

    25 lemma eq1_L:

    26   assumes "x ~1 y"

    27   shows "L (erase x) = L (erase y)"

    28   using assms

    29   apply(induct rule: eq1.induct)

    30   apply(auto elim: eq1.elims)

    31   apply presburger

    32   done

    72 

    73 

    74 

    75 

    76 fun bsimp :: "arexp \<Rightarrow> arexp" 

    77   where

    78   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"

    79 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) "

    80 | "bsimp r = r"

    81 

    82 

    83 fun 

    84   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

    85 where

    86   "bders_simp r [] = r"

    87 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"

    88 

    89 definition blexer_simp where

    90  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 

    91                     decode (bmkeps (bders_simp (intern r) s)) r else None"

    92 

    93 

    94 

    95 lemma bders_simp_append:

    96   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"

    97   apply(induct s1 arbitrary: r s2)

    98   apply(simp_all)

    99   done

   100 

   101