--- a/exps/bit.scala	Sat Mar 16 11:15:22 2019 +0000
+++ b/exps/bit.scala	Thu Apr 11 17:37:00 2019 +0100
@@ -392,10 +392,10 @@
 def erase(r: ARexp) : Rexp = r match{
   case AZERO => ZERO
   case AONE(_) => ONE
-  case APRED(bs, f, s) => PRED(f, s)
-  case AALTS(bs, rs) => ALTS(rs.map(erase(_)))
-  case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
-  case ASTAR(cs, r)=> STAR(erase(r))
+  case APRED(_, f, s) => PRED(f, s)
+  case AALTS(_, rs) => ALTS(rs.map(erase(_)))
+  case ASEQ(_, r1, r2) => SEQ(erase(r1), erase(r2))
+  case ASTAR(_, r)=> STAR(erase(r))
 }
 
 
@@ -442,9 +442,9 @@
 
 def flats(rs: List[ARexp]): List[ARexp] = rs match {
     case Nil => Nil
-    case AZERO :: rs1 => flats(rs1)
-    case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
-    case r1 :: rs2 => r1 :: flats(rs2)
+    case AZERO::rs1 => flats(rs1)
+    case AALTS(bs, rs1)::rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
+    case r1::rs2 => r1::flats(rs2)
 }
 
 def stack(r1: ARexp, r2: ARexp) = r1 match {
@@ -738,6 +738,17 @@
 println(strings(pders_simp(qs.toList, q)))
 
 
+val w : Rexp = ((("a" | "b") | "b".%) | "ab") ~ ("a".% | ("b" | "b"))
+val ws = "ab"
+
+lexing(w, ws)
+blexing_simp(w, ws)
+
+
+        
+
+
+
 
 System.exit(0)
 

--- a/exps/both.scala	Sat Mar 16 11:15:22 2019 +0000
+++ b/exps/both.scala	Thu Apr 11 17:37:00 2019 +0100
@@ -352,15 +352,13 @@
   case (ONE, bs) => (Empty, bs)
   case (PRED(f, _), C(c)::bs) => (Chr(c), bs)
   case (ALTS(r::Nil), bs) => decode_aux(r, bs)
-  case (ALTS(rs), bs) => bs match {
-    case Z::bs1 => {
+  case (ALTS(rs), Z::bs1) => {
       val (v, bs2) = decode_aux(rs.head, bs1)
       (Left(v), bs2)
     }
-    case S::bs1 => {
+  case (ALTS(rs), S::bs1) => {
       val (v, bs2) = decode_aux(ALTS(rs.tail), bs1)
-      (Right(v), bs2)			
-    }
+      (Right(v), bs2)	
   }
   case (SEQ(r1, r2), bs) => {
     val (v1, bs1) = decode_aux(r1, bs)

--- a/progs/sml/README	Sat Mar 16 11:15:22 2019 +0000
+++ b/progs/sml/README	Thu Apr 11 17:37:00 2019 +0100
@@ -4,5 +4,8 @@
 
 or, call directly
 
+poly --use re.ML
 
-poly --use re.ML 
\ No newline at end of file
+
+
+poly --enable-compact32bit --use re.ML 
\ No newline at end of file

--- a/progs/sml/re-bit.ML	Sat Mar 16 11:15:22 2019 +0000
+++ b/progs/sml/re-bit.ML	Thu Apr 11 17:37:00 2019 +0100
@@ -1,20 +1,27 @@
+
+datatype bit =
+  Z | S | C of char
+
+type bits = bit list
 
 datatype rexp =
    ZERO
  | ONE 
- | CHAR of char
- | ALT  of rexp * rexp
+ | CHAR of char 
+ | ALTS of rexp list
  | SEQ  of rexp * rexp 
  | STAR of rexp 
  | RECD of string * rexp
 
+fun alt r1 r2 = ALTS [r1, r2]
+
 datatype arexp =
    AZERO
- | AONE  of (bool list)
- | ACHAR of (bool list) * char
- | AALT  of (bool list) * arexp * arexp
- | ASEQ  of (bool list) * arexp * arexp 
- | ASTAR of (bool list) * arexp 
+ | AONE  of bits
+ | ACHAR of bits * char
+ | AALTS of bits * (arexp list)
+ | ASEQ  of bits * arexp * arexp 
+ | ASTAR of bits * arexp 
 
 datatype value =
    Empty
@@ -44,269 +51,54 @@
 infix 9 --
 infix 9 $
 
-fun op ++ (r1, r2) = ALT(r1, r2)
+fun op ++ (r1, r2) = ALTS [r1, r2]
 
 fun op -- (r1, r2) = SEQ(r1, r2)
 
 fun op $ (x, r) = RECD(x, r)
 
-fun alts rs = case rs of
+fun alts rs = case rs of 
     [] => ZERO
   | [r] => r
-  | r::rs => List.foldl (op ++) r rs
+  | r::rs => ALTS([r, alts rs])
+
+
+fun sum (nil) = 0 
+  | sum (head::tail) = head + sum(tail);
 
 (* size of a regular expressions - for testing purposes *)
 fun size r = case r of
     ZERO => 1
   | ONE => 1
   | CHAR(_) => 1
-  | ALT(r1, r2) => 1 + (size r1) + (size r2)
+  | ALTS(rs) => 1 + sum (map size rs)
   | SEQ(r1, r2) => 1 + (size r1) + (size r2)
   | STAR(r) => 1 + (size r)
   | RECD(_, r) => 1 + (size r)
 
-(* nullable function: tests whether the regular 
-   expression can recognise the empty string *)
-fun nullable r = case r of
-    ZERO => false
-  | ONE => true
-  | CHAR(_) => false
-  | ALT(r1, r2) => nullable(r1) orelse nullable(r2)
-  | SEQ(r1, r2) => nullable(r1) andalso nullable(r2)
-  | STAR(_) => true
-  | RECD(_, r) => nullable(r)
 
-(* derivative of a regular expression r w.r.t. a character c *)
-fun der c r = case r of
-    ZERO => ZERO
-  | ONE => ZERO
-  | CHAR(d) => if c = d then ONE else ZERO
-  | ALT(r1, r2) => ALT(der c r1, der c r2)
-  | SEQ(r1, r2) => 
-      if nullable r1 then ALT(SEQ(der c r1, r2), der c r2)
-      else SEQ(der c r1, r2)
-  | STAR(r) => SEQ(der c r, STAR(r))
-  | RECD(_, r) => der c r
-
-(* derivative w.r.t. a list of chars (iterates der) *)
-fun ders s r = case s of 
-    [] => r
-  | c::s => ders s (der c r)
-
-(* extracts a string from value *)
-fun flatten v = case v of 
-    Empty => ""
-  | Chr(c) => Char.toString c
-  | Left(v) => flatten v
-  | Right(v) => flatten v
-  | Sequ(v1, v2) => flatten v1 ^ flatten v2
-  | Stars(vs) => String.concat (List.map flatten vs)
-  | Rec(_, v) => flatten v
-
-
-(* extracts an environment from a value *)
-fun env v = case v of 
-    Empty => []
-  | Chr(c) => []
-  | Left(v) => env v
-  | Right(v) => env v
-  | Sequ(v1, v2) => env v1 @ env v2
-  | Stars(vs) => List.foldr (op @) [] (List.map env vs)
-  | Rec(x, v) => (x, flatten v) :: env v
-
-fun string_of_pair (x, s) = "(" ^ x ^ "," ^ s ^ ")"
-fun string_of_env xs = String.concatWith "," (List.map string_of_pair xs)
+fun erase r = case r of
+    AZERO => ZERO
+  | AONE(_) => ONE
+  | ACHAR(_, c) => CHAR(c)
+  | AALTS(_, rs) => ALTS(map erase rs)
+  | ASEQ(_, r1, r2) => SEQ(erase r1, erase r2)
+  | ASTAR(_, r)=> STAR(erase r)
 
 
-(* the value for a nullable rexp *)
-fun mkeps r = case r of 
-    ONE => Empty
-  | ALT(r1, r2) => 
-      if nullable r1 then Left(mkeps r1) else Right(mkeps r2)
-  | SEQ(r1, r2) => Sequ(mkeps r1, mkeps r2)
-  | STAR(r) => Stars([])
-  | RECD(x, r) => Rec(x, mkeps r)
-
-exception Error
-
-(* injection of a char into a value *)
-fun inj r c v = case (r, v) of
-    (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj r c v1 :: vs)
-  | (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj r1 c v1, v2)
-  | (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj r1 c v1, v2)
-  | (SEQ(r1, r2), Right(v2)) => Sequ(mkeps r1, inj r2 c v2)
-  | (ALT(r1, r2), Left(v1)) => Left(inj r1 c v1)
-  | (ALT(r1, r2), Right(v2)) => Right(inj r2 c v2)
-  | (CHAR(d), Empty) => Chr(d) 
-  | (RECD(x, r1), _) => Rec(x, inj r1 c v)
-  | _ => (print ("\nr: " ^ PolyML.makestring r ^ "\n");
-          print ("v: " ^ PolyML.makestring v ^ "\n");
-          raise Error)
-
-(* some "rectification" functions for simplification *)
-fun f_id v = v
-fun f_right f = fn v => Right(f v)
-fun f_left f = fn v => Left(f v)
-fun f_alt f1 f2 = fn v => case v of
-    Right(v) => Right(f2 v)
-  | Left(v) => Left(f1 v)
-fun f_seq f1 f2 = fn v => case v of 
-  Sequ(v1, v2) => Sequ(f1 v1, f2 v2)
-fun f_seq_Empty1 f1 f2 = fn v => Sequ(f1 Empty, f2 v)
-fun f_seq_Empty2 f1 f2 = fn v => Sequ(f1 v, f2 Empty)
-fun f_rec f = fn v => case v of
-    Rec(x, v) => Rec(x, f v)
-
-exception ShouldNotHappen
-
-fun f_error v = raise ShouldNotHappen
-
-(* simplification of regular expressions returning also an 
-   rectification function; no simplification under STARs *)
-fun simp r = case r of
-    ALT(r1, r2) => 
-      let val (r1s, f1s) = simp r1  
-          val (r2s, f2s) = simp r2 in
-        (case (r1s, r2s) of
-            (ZERO, _) => (r2s, f_right f2s)
-          | (_, ZERO) => (r1s, f_left f1s)
-          | (_, _)    => if r1s = r2s then (r1s, f_left f1s)
-                         else (ALT (r1s, r2s), f_alt f1s f2s))
-      end 
-  | SEQ(r1, r2) => 
-      let val (r1s, f1s) = simp r1 
-          val (r2s, f2s) = simp r2 in
-        (case (r1s, r2s) of
-          (ZERO, _)  => (ZERO, f_error)
-        | (_, ZERO)  => (ZERO, f_error)
-        | (ONE, _) => (r2s, f_seq_Empty1 f1s f2s)
-        | (_, ONE) => (r1s, f_seq_Empty2 f1s f2s)
-        | (_, _)     => (SEQ(r1s, r2s), f_seq f1s f2s))
-      end  
-  | RECD(x, r1) => 
-      let val (r1s, f1s) = simp r1 in
-        (RECD(x, r1s), f_rec f1s)
-      end
-  | r => (r, f_id)
-
-fun der_simp c r = case r of
-    ZERO => (ZERO, f_id)
-  | ONE => (ZERO, f_id)
-  | CHAR(d) => ((if c = d then ONE else ZERO), f_id)
-  | ALT(r1, r2) => 
-      let 
-        val (r1d, f1d) = der_simp c r1 
-        val (r2d, f2d) = der_simp c r2 
-      in
-        case (r1d, r2d) of
-          (ZERO, _) => (r2d, f_right f2d)
-        | (_, ZERO) => (r1d, f_left f1d)
-        | (_, _)    => if r1d = r2d then (r1d, f_left f1d)
-                       else (ALT (r1d, r2d), f_alt f1d f2d)
-      end
-  | SEQ(r1, r2) => 
-      if nullable r1 
-      then 
-        let 
-          val (r1d, f1d) = der_simp c r1 
-          val (r2d, f2d) = der_simp c r2
-          val (r2s, f2s) = simp r2 
-        in
-          case (r1d, r2s, r2d) of
-            (ZERO, _, _)  => (r2d, f_right f2d)
-          | (_, ZERO, _)  => (r2d, f_right f2d)
-          | (_, _, ZERO)  => (SEQ(r1d, r2s), f_left (f_seq f1d f2s))
-          | (ONE, _, _) => (ALT(r2s, r2d), f_alt (f_seq_Empty1 f1d f2s) f2d)
-          | (_, ONE, _) => (ALT(r1d, r2d), f_alt (f_seq_Empty2 f1d f2s) f2d)
-          | (_, _, _)     => (ALT(SEQ(r1d, r2s), r2d), f_alt (f_seq f1d f2s) f2d)
-        end
-      else 
-        let 
-          val (r1d, f1d) = der_simp c r1 
-          val (r2s, f2s) = simp r2
-        in
-          case (r1d, r2s) of
-            (ZERO, _) => (ZERO, f_error)
-          | (_, ZERO) => (ZERO, f_error)
-          | (ONE, _) => (r2s, f_seq_Empty1 f1d f2s)
-          | (_, ONE) => (r1d, f_seq_Empty2 f1d f2s)
-          | (_, _) => (SEQ(r1d, r2s), f_seq f1d f2s)
-  	end	  
-  | STAR(r1) => 
-      let 
-        val (r1d, f1d) = der_simp c r1 
-      in
-        case r1d of
-          ZERO => (ZERO, f_error)
-        | ONE => (STAR r1, f_seq_Empty1 f1d f_id)
-        | _ => (SEQ(r1d, STAR(r1)), f_seq f1d f_id)
-      end
-  | RECD(x, r1) => der_simp c r1 
-
-(* matcher function *)
-fun matcher r s = nullable(ders (explode s) r)
-
-(* lexing function (produces a value) *)
-exception LexError
-
-fun lex r s = case s of 
-    [] => if (nullable r) then mkeps r else raise LexError
-  | c::cs => inj r c (lex (der c r) cs)
-
-fun lexing r s = lex r (explode s)
-
-(* lexing with simplification *)
-fun lex_simp r s = case s of 
-    [] => if (nullable r) then mkeps r else raise LexError
-  | c::cs => 
-    let val (r_simp, f_simp) = simp (der c r) in
-      inj r c (f_simp (lex_simp r_simp cs))
-    end
-
-fun lexing_simp r s = lex_simp r (explode s)
-
-fun lex_simp2 r s = case s of 
-    [] => if (nullable r) then mkeps r else raise LexError
-  | c::cs => 
-    let val (r_simp, f_simp) = der_simp c r in
-      inj r c (f_simp (lex_simp2 r_simp cs))
-    end
-
-fun lexing_simp2 r s = lex_simp2 r (explode s)
-
-fun lex_acc r s f = case s of 
-    [] => if (nullable r) then f (mkeps r) else raise LexError
-  | c::cs => 
-    let val (r_simp, f_simp) = simp (der c r) in
-      lex_acc r_simp cs (fn v => f (inj r c (f_simp v)))
-    end
-
-fun lexing_acc r s  = lex_acc r (explode s) (f_id)
-
-fun lex_acc2 r s f = case s of 
-    [] => if (nullable r) then f (mkeps r) else raise LexError
-  | c::cs => 
-    let val (r_simp, f_simp) = der_simp c r in
-      lex_acc2 r_simp cs (fn v => f (inj r c (f_simp v)))
-    end
-
-fun lexing_acc2 r s  = lex_acc2 r (explode s) (f_id)
-
-(* bit-coded version *)
-
 fun fuse bs r = case r of
-  AZERO => AZERO
-| AONE(cs) => AONE(bs @ cs)
-| ACHAR(cs, c) => ACHAR(bs @ cs, c)
-| AALT(cs, r1, r2) => AALT(bs @ cs, r1, r2)
-| ASEQ(cs, r1, r2) => ASEQ(bs @ cs, r1, r2)
-| ASTAR(cs, r) => ASTAR(bs @ cs, r)
+    AZERO => AZERO
+  | AONE(cs) => AONE(bs @ cs)
+  | ACHAR(cs, c) => ACHAR(bs @ cs, c)
+  | AALTS(cs, rs) => AALTS(bs @ cs, rs)
+  | ASEQ(cs, r1, r2) => ASEQ(bs @ cs, r1, r2)
+  | ASTAR(cs, r) => ASTAR(bs @ cs, r)
 
 fun internalise r = case r of
   ZERO => AZERO
 | ONE => AONE([])
 | CHAR(c) => ACHAR([], c)
-| ALT(r1, r2) => AALT([], fuse [false] (internalise r1), fuse [true] (internalise r2))
+| ALTS([r1, r2]) => AALTS([], [fuse [Z] (internalise r1), fuse [S] (internalise r2)])
 | SEQ(r1, r2) => ASEQ([], internalise r1, internalise r2)
 | STAR(r) => ASTAR([], internalise r)
 | RECD(x, r) => internalise r
@@ -314,21 +106,22 @@
 fun decode_aux r bs = case (r, bs) of
   (ONE, bs) => (Empty, bs)
 | (CHAR(c), bs) => (Chr(c), bs)
-| (ALT(r1, r2), false::bs) => 
-     let val (v, bs1) = decode_aux r1 bs
-     in (Left(v), bs1) end
-| (ALT(r1, r2), true::bs) => 
-     let val (v, bs1) = decode_aux r2 bs
-     in (Right(v), bs1) end
+| (ALTS([r1]), bs) => decode_aux r1 bs
+| (ALTS(rs), Z::bs1) => 
+     let val (v, bs2) = decode_aux (hd rs) bs1
+     in (Left(v), bs2) end
+| (ALTS(rs), S::bs1) => 
+     let val (v, bs2) = decode_aux (ALTS (tl rs)) bs1
+     in (Right(v), bs2) end
 | (SEQ(r1, r2), bs) => 
     let val (v1, bs1) = decode_aux r1 bs 
         val (v2, bs2) = decode_aux r2 bs1 
     in (Sequ(v1, v2), bs2) end
-| (STAR(r1), false::bs) => 
+| (STAR(r1), Z::bs) => 
     let val (v, bs1) = decode_aux r1 bs 
         val (Stars(vs), bs2) = decode_aux (STAR r1) bs1
     in (Stars(v::vs), bs2) end
-| (STAR(_), true::bs) => (Stars [], bs)
+| (STAR(_), S::bs) => (Stars [], bs)
 | (RECD(x, r1), bs) => 
     let val (v, bs1) = decode_aux r1 bs
     in (Rec(x, v), bs1) end
@@ -339,61 +132,95 @@
   (v, []) => v
 | _ => raise DecodeError
 
-fun anullable r = case r of
+fun bnullable r = case r of
   AZERO => false
 | AONE(_) => true
-| ACHAR(_,_) => false
-| AALT(_, r1, r2) => anullable(r1) orelse anullable(r2)
-| ASEQ(_, r1, r2) => anullable(r1) andalso anullable(r2)
+| ACHAR(_, _) => false
+| AALTS(_, rs) => List.exists bnullable rs
+| ASEQ(_, r1, r2) => bnullable(r1) andalso bnullable(r2)
 | ASTAR(_, _) => true
 
-fun mkepsBC r = case r of
+fun bmkeps r = case r of
   AONE(bs) => bs
-| AALT(bs, r1, r2) => 
-    if anullable(r1) then bs @ mkepsBC(r1) else bs @ mkepsBC(r2)
-| ASEQ(bs, r1, r2) => bs @ mkepsBC(r1) @ mkepsBC(r2)
-| ASTAR(bs, r) => bs @ [true]
+| AALTS(bs, rs) => 
+    let 
+      val SOME(r) = List.find bnullable rs
+    in bs @ bmkeps(r) end
+| ASEQ(bs, r1, r2) => bs @ bmkeps(r1) @ bmkeps(r2)
+| ASTAR(bs, r) => bs @ [S]
 
-fun ader c r = case r of
+fun bder c r = case r of
   AZERO => AZERO
 | AONE(_) => AZERO
 | ACHAR(bs, d) => if c = d then AONE(bs) else AZERO
-| AALT(bs, r1, r2) => AALT(bs, ader c r1, ader c r2)
+| AALTS(bs, rs) => AALTS(bs, map (bder c) rs)
 | ASEQ(bs, r1, r2) => 
-    if (anullable r1) then AALT(bs, ASEQ([], ader c r1, r2), fuse (mkepsBC r1) (ader c r2))
-    else ASEQ(bs, ader c r1, r2)
-| ASTAR(bs, r) => ASEQ(bs, fuse [false] (ader c r), ASTAR([], r))
+    if (bnullable r1) 
+    then AALTS(bs, [ASEQ([], bder c r1, r2), fuse (bmkeps r1) (bder c r2)])
+    else ASEQ(bs, bder c r1, r2)
+| ASTAR(bs, r) => ASEQ(bs, fuse [Z] (bder c r), ASTAR([], r))
 
-fun aders s r = case s of 
+fun bders s r = case s of 
   [] => r
-| c::s => aders s (ader c r)
+| c::s => bders s (bder c r)
+
+
+exception LexError
+
+fun blex r s = case s of 
+    [] => if (bnullable r) then bmkeps r else raise LexError
+  | c::cs => blex (bder c r) cs
+
+fun blexing r s = decode r (blex (internalise r) (explode s))
 
-fun alex r s = case s of 
-    [] => if (anullable r) then mkepsBC r else raise LexError
-  | c::cs => alex (ader c r) cs
+(* Simplification *)
 
-fun alexing r s = decode r (alex (internalise r) (explode s))
+fun distinctBy xs f acc = case xs of
+   [] => []
+ | x::xs =>
+    let   
+      val res = f x
+    in  if (List.exists (fn x => x = res) acc)
+        then distinctBy xs f acc  
+        else x::distinctBy xs f (res::acc)
+    end
 
-fun asimp r = case r of
-  ASEQ(bs1, r1, r2) => (case (asimp r1, asimp r2) of
-      (AZERO, _) => AZERO
-    | (_, AZERO) => AZERO
-    | (AONE(bs2), r2s) => fuse (bs1 @ bs2) r2s
-    | (r1s, r2s) => ASEQ(bs1, r1s, r2s)
-  )
-| AALT(bs1, r1, r2) => (case (asimp r1, asimp r2) of
-      (AZERO, r2s) => fuse bs1 r2s
-    | (r1s, AZERO) => fuse bs1 r1s
-    | (r1s, r2s) => AALT(bs1, r1s, r2s)
-  )
-| r => r
+fun flats rs = case rs of
+    [] => []
+  | AZERO::rs1 => flats rs1
+  | AALTS(bs, rs1)::rs2 => map (fuse bs) rs1 @ flats rs2
+  | r1::rs2 => r1::flats rs2
+
+
+fun stack r1 r2 = case r1 of
+    AONE(bs2) => fuse bs2 r2
+  | _ => ASEQ([], r1, r2)
+
 
-fun alex_simp r s = case s of 
-    [] => if (anullable r) then mkepsBC r else raise LexError
-  | c::cs => alex_simp (asimp (ader c r)) cs
+fun bsimp r = case r of
+    ASEQ(bs1, r1, r2) => (case (bsimp r1, bsimp r2) of
+        (AZERO, _) => AZERO
+      | (_, AZERO) => AZERO
+      | (AONE(bs2), r2s) => fuse (bs1 @ bs2) r2s
+      | (AALTS(bs2, rs), r2s) =>  
+           AALTS(bs1 @ bs2, map (fn r => stack r r2s) rs)
+      | (r1s, r2s) => ASEQ(bs1, r1s, r2s)) 
+  | AALTS(bs1, rs) => (case distinctBy (flats (map bsimp rs)) erase [] of
+        [] => AZERO
+      | [r] => fuse bs1 r
+      | rs2 => AALTS(bs1, rs2))  
+  | r => r
 
-fun alexing_simp r s = decode r (alex_simp (internalise r) (explode s))
+fun bders_simp r s = case s of 
+  [] => r
+| c::s => bders_simp (bsimp (bder c r)) s
 
+fun blex_simp r s = case s of 
+    [] => if (bnullable r) then bmkeps r else raise LexError
+  | c::cs => blex_simp (bsimp (bder c r)) cs
+
+fun blexing_simp r s = 
+    decode r (blex_simp (internalise r) (explode s))
 
 
 (* Lexing rules for a small WHILE language *)
@@ -428,45 +255,12 @@
 fun time f x =
   let
   val t_start = Timer.startCPUTimer()
-  val f_x = (f x; f x; f x; f x; f x; f x; f x; f x; f x; f x)
-  val t_end = Time.toReal(#usr(Timer.checkCPUTimer(t_start))) / 10.0
+  val f_x = (f x; f x; f x; f x; f x)
+  val t_end = Time.toReal(#usr(Timer.checkCPUTimer(t_start))) / 5.0
 in
   (print ((Real.toString t_end) ^ "\n"); f_x)
 end
 
-val prog = "ab";
-val reg = ("x" $ ((str "a") -- (str "b")));
-print("Simp: " ^ PolyML.makestring (lexing_simp reg prog) ^ "\n");
-print("Acc:  " ^ PolyML.makestring (lexing_acc  reg prog) ^ "\n");
-print("Env   " ^ string_of_env (env (lexing_acc reg prog)) ^ "\n");
-
-fun fst (x, y) = x;
-fun snd (x, y) = y;
-
-val derS = [reg,
-            der #"a" reg,
-            fst (simp (der #"a" reg)),
-            fst (der_simp #"a" reg)];
-
-val vS = [(snd (simp (der #"a" reg))) (Chr(#"b")),
-          (snd (der_simp #"a" reg)) (Chr(#"b"))
-         ];
-
-print("Ders: \n" ^ 
-       String.concatWith "\n" (List.map PolyML.makestring derS)
-       ^ "\n\n");
-print("Vs: \n" ^ 
-       String.concatWith "\n" (List.map PolyML.makestring vS)
-       ^ "\n\n");
-
-
-val prog0 = "read n";
-print("Env0 is: \n" ^  string_of_env (env (lexing_acc while_regs prog0)) ^ "\n");
-
-val prog1 = "read  n; write (n)";
-print("Env1 is: \n" ^ string_of_env (env (lexing_acc while_regs prog1)) ^ "\n");
-print("Env1 is: \n" ^ string_of_env (env (alexing while_regs prog1)) ^ "\n");
-
 
 val prog2 = String.concatWith "\n" 
   ["i := 2;",
@@ -483,12 +277,6 @@
    "}"];
 
 
-let 
-  val tst = (lexing_simp while_regs prog2 = lexing_acc while_regs prog2)
-in
-  print("Sanity test: >>" ^ (PolyML.makestring tst) ^ "<<\n")
-end;
-
 (* loops in ML *)
 datatype for = to of int * int
 infix to 
@@ -510,28 +298,7 @@
 
 fun step_simp i = 
   (print ((Int.toString i) ^ ": ") ;
-   time (lexing_simp while_regs) (string_repeat prog2 i)); 
-
-fun step_simp2 i = 
-  (print ((Int.toString i) ^ ": ") ;
-   time (lexing_simp2 while_regs) (string_repeat prog2 i));
-
-fun step_acc i = 
-  (print ((Int.toString i) ^ ": ") ;
-   time (lexing_acc while_regs) (string_repeat prog2 i));
-
-fun step_acc2 i = 
-  (print ((Int.toString i) ^ ": ") ;
-   time (lexing_acc2 while_regs) (string_repeat prog2 i));
-
-fun astep_basic i = 
-  (print ((Int.toString i) ^ ": ") ;
-   time (alexing while_regs) (string_repeat prog2 i)); 
-
-fun astep_simp i = 
-  (print ((Int.toString i) ^ ": ") ;
-   time (alexing_simp while_regs) (string_repeat prog2 i)); 
-
+   time (blexing_simp while_regs) (string_repeat prog2 i)); 
 
 (*
 val main1 = forby 1000 (1000 to 5000) step_simp;
@@ -544,4 +311,11 @@
 *)
 
 print "\n";
-val main5 = forby 1 (1 to 5) astep_simp; 
\ No newline at end of file
+val main5 = forby 10 (10 to 50) step_simp; 
+
+print("Size after 50: " ^ 
+  PolyML.makestring(size (erase (bders_simp (internalise while_regs) (explode (string_repeat prog2 50))))) ^ "\n");
+
+print("Size after 100: " ^ 
+  PolyML.makestring(size (erase (bders_simp (internalise while_regs) (explode (string_repeat prog2 100))))) ^ "\n");
+

--- a/progs/sml/re.ML	Sat Mar 16 11:15:22 2019 +0000
+++ b/progs/sml/re.ML	Thu Apr 11 17:37:00 2019 +0100
@@ -237,7 +237,6 @@
   | RECD(x, r1) => der_simp c r1 
 
 
-
 (* matcher function *)
 fun matcher r s = nullable(ders (explode s) r)
 
@@ -251,6 +250,14 @@
 fun lexing r s = lex r (explode s)
 
 (* lexing with simplification *)
+
+fun fst (a, b) = a
+
+fun ders_simp r s = case s of 
+  [] => r
+| c::s => ders_simp (fst (simp (der c r))) s
+
+
 fun lex_simp r s = case s of 
     [] => if (nullable r) then mkeps r else raise LexError
   | c::cs => 
@@ -260,6 +267,7 @@
 
 fun lexing_simp r s = lex_simp r (explode s)
 
+(* does derivatives and simplificatiomn in one step *)
 fun lex_simp2 r s = case s of 
     [] => if (nullable r) then mkeps r else raise LexError
   | c::cs => 
@@ -269,6 +277,7 @@
 
 fun lexing_simp2 r s = lex_simp2 r (explode s)
 
+(* uses an accumulator for the rectification functions *)
 fun lex_acc r s f = case s of 
     [] => if (nullable r) then f (mkeps r) else raise LexError
   | c::cs => 
@@ -285,7 +294,7 @@
       lex_acc2 r_simp cs (fn v => f (inj r c (f_simp v)))
     end
 
-fun lexing_acc2 r s  = lex_acc2 r (explode s) (f_id)
+fun lexing_acc2 r s  = lex_acc2 r (explode s) f_id
 
 
 (* Lexing rules for a small WHILE language *)
@@ -317,11 +326,12 @@
 (* Some Tests
   ============ *)
 
+
 fun time f x =
   let
   val t_start = Timer.startCPUTimer()
-  val f_x = (f x; f x; f x; f x; f x; f x; f x; f x; f x; f x)
-  val t_end = Time.toReal(#usr(Timer.checkCPUTimer(t_start))) / 10.0
+  val f_x = (f x; f x; f x; f x; f x)
+  val t_end = Time.toReal(#usr(Timer.checkCPUTimer(t_start))) / 5.0
 in
   (print ((Real.toString t_end) ^ "\n"); f_x)
 end
@@ -374,12 +384,21 @@
    "}"];
 
 
+print("The prog2 string is of length: >>" ^ (PolyML.makestring (String.size prog2)) ^ "<<\n");
+
 let 
   val tst = (lexing_simp while_regs prog2 = lexing_acc while_regs prog2)
 in
   print("Sanity test: >>" ^ (PolyML.makestring tst) ^ "<<\n")
 end;
 
+print("Size after 50: " ^ 
+  PolyML.makestring(size (ders_simp while_regs (explode (string_repeat prog2 50)))) ^ "\n");
+
+print("Size after 5000: " ^ 
+  PolyML.makestring(size (ders_simp while_regs (explode (string_repeat prog2 5000)))) ^ "\n");
+
+
 (* loops in ML *)
 datatype for = to of int * int
 infix to 
@@ -389,38 +408,47 @@
     (fn f => 
        let fun loop lo = 
          if lo > up then () else (f lo; loop (lo + 1))
-       in loop lo end)
+       in loop lo end);
 
 fun forby n =
   fn lo to up =>
     (fn f => 
        let fun loop lo = 
          if lo > up then () else (f lo; loop (lo + n))
-       in loop lo end)
+       in loop lo end);
 
 
 fun step_simp i = 
   (print ((Int.toString i) ^ ": ") ;
-   time (lexing_simp while_regs) (string_repeat prog2 i)) 
+   time (lexing_simp while_regs) (string_repeat prog2 i)); 
 
 fun step_simp2 i = 
   (print ((Int.toString i) ^ ": ") ;
-   time (lexing_simp2 while_regs) (string_repeat prog2 i)) 
+   time (lexing_simp2 while_regs) (string_repeat prog2 i)); 
 
 fun step_acc i = 
   (print ((Int.toString i) ^ ": ") ;
-   time (lexing_acc while_regs) (string_repeat prog2 i))
+   time (lexing_acc while_regs) (string_repeat prog2 i));
 
 fun step_acc2 i = 
   (print ((Int.toString i) ^ ": ") ;
-   time (lexing_acc2 while_regs) (string_repeat prog2 i)) 
+   time (lexing_acc2 while_regs) (string_repeat prog2 i)); 
 
-val main1 = forby 1000 (1000 to 5000) step_simp;
-print "\n";
-val main2 = forby 1000 (1000 to 5000) step_simp2;
-print "\n";
-val main3 = forby 1000 (1000 to 5000) step_acc;
-print "\n";
-val main4 = forby 1000 (1000 to 5000) step_acc2; 
 
 
+print("\nTest step_simp\n");
+val main1 = forby 1000 (1000 to 5000) step_simp;
+
+print("\nTest step_simp2\n");
+val main2 = forby 1000 (1000 to 5000) step_simp2;
+
+(*
+print("\nTest step_acc\n"); 
+val main3 = forby 1000 (1000 to 5000) step_acc;
+
+print("\nTest step_acc2\n");
+val main4 = forby 1000 (1000 to 5000) step_acc2;
+*)
+
+
+

--- a/thys/BitCoded.thy	Sat Mar 16 11:15:22 2019 +0000
+++ b/thys/BitCoded.thy	Thu Apr 11 17:37:00 2019 +0100
@@ -98,6 +98,15 @@
 abbreviation
   "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
 
+fun asize :: "arexp \<Rightarrow> nat" where
+  "asize AZERO = 1"
+| "asize (AONE cs) = 1" 
+| "asize (ACHAR cs c) = 1"
+| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
+| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
+| "asize (ASTAR cs r) = Suc (asize r)"
+
+
 
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
@@ -472,17 +481,6 @@
 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 | "flts (r1 # rs) = r1 # flts rs"
 
-(*
-lemma flts_map:
-  assumes "\<forall>r \<in> set rs. f r = r"
-  shows "map f (flts rs) = flts (map f rs)"
-  using assms
-  apply(induct rs rule: flts.induct)
-        apply(simp_all)
-       apply(case_tac rs)
-  apply(simp)
-*)
-
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -515,6 +513,13 @@
                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
 
+lemma asize0:
+  shows "0 < asize r"
+  apply(induct  r)
+       apply(auto)
+  done
+
+
 lemma bders_simp_append:
   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
   apply(induct s1 arbitrary: r s2)
@@ -522,7 +527,78 @@
   apply(simp)
   done
 
+lemma bsimp_ASEQ_size:
+  shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
+  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
 
+lemma fuse_size:
+  shows "asize (fuse bs r) = asize r"
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma flts_size:
+  shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
+  apply(induct rs rule: flts.induct)
+        apply(simp_all)
+  by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong)
+  
+
+lemma bsimp_AALTs_size:
+  shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
+  apply(induct rs rule: bsimp_AALTs.induct)
+  apply(auto simp add: fuse_size)
+  done
+  
+lemma bsimp_size:
+  shows "asize (bsimp r) \<le> asize r"
+  apply(induct r)
+       apply(simp_all)
+   apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
+  apply(rule le_trans)
+   apply(rule bsimp_AALTs_size)
+  apply(simp)
+   apply(rule le_trans)
+   apply(rule flts_size)
+  by (simp add: sum_list_mono)
+
+fun nonalt :: "arexp \<Rightarrow> bool"
+  where
+  "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+
+
+lemma bsimp_AALTs_size2:
+  assumes "\<forall>r \<in> set  rs. nonalt r"
+  shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
+  using assms
+  apply(induct rs rule: bsimp_AALTs.induct)
+    apply(simp_all add: fuse_size)
+  done
+
+lemma qq:
+  shows "map (asize \<circ> fuse bs) rs = map asize rs"
+  apply(induct rs)
+   apply(auto simp add: fuse_size)
+  done
+
+lemma flts_size2:
+  assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"
+  shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
+  using assms
+  apply(induct rs)
+   apply(auto simp add: qq)
+   apply (simp add: flts_size less_Suc_eq_le)
+  apply(case_tac a)
+       apply(auto simp add: qq)
+   prefer 2
+   apply (simp add: flts_size le_imp_less_Suc)
+  using less_Suc_eq by auto
+  
 lemma L_bsimp_ASEQ:
   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -575,6 +651,13 @@
    apply (simp add: L_erase_AALTs)
   using L_erase_AALTs by blast
 
+lemma bsimp_ASEQ0:
+  shows "bsimp_ASEQ bs r1 AZERO = AZERO"
+  apply(induct r1)
+  apply(auto)
+  done
+
+
 
 lemma bsimp_ASEQ1:
   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
@@ -620,7 +703,6 @@
 lemma b4:
   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
-  
 
 lemma q1:
   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
@@ -667,6 +749,427 @@
   apply(simp)
   done
 
+lemma fuse_empty:
+  shows "fuse [] r = r"
+  apply(induct r)
+       apply(auto)
+  done
+
+lemma flts_fuse:
+  shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(auto simp add: fuse_append)
+  done
+
+lemma bsimp_ASEQ_fuse:
+  shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
+  apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
+
+lemma bsimp_AALTs_fuse:
+  assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+  shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+  using assms
+  apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+  apply(auto)
+  done
+
+
+
+lemma bsimp_fuse:
+  shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+apply(induct r arbitrary: bs)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   apply(simp)
+   apply (simp add: bsimp_ASEQ_fuse)
+  apply(simp)
+  by (simp add: bsimp_AALTs_fuse fuse_append)
+
+lemma bsimp_fuse_AALTs:
+  shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
+  apply(subst bsimp_fuse) 
+  apply(simp)
+  done
+
+lemma bsimp_fuse_AALTs2:
+  shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
+  using bsimp_AALTs_fuse fuse_append by auto
+  
+
+lemma bsimp_ASEQ_idem:
+  assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+  shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+  using assms
+  apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+    apply(simp)
+  apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))  
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+   apply(subst bsimp_ASEQ2)
+  apply (metis assms(2) bsimp_fuse)
+      apply(subst bsimp_ASEQ1)
+      apply(auto)
+  done
+
+
+fun nonnested :: "arexp \<Rightarrow> bool"
+  where
+  "nonnested (AALTs bs2 []) = True"
+| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
+| "nonnested r = True"
+
+
+lemma  k0:
+  shows "flts (r # rs1) = flts [r] @ flts rs1"
+  apply(induct r arbitrary: rs1)
+   apply(auto)
+  done
+
+lemma  k00:
+  shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
+  apply(induct rs1 arbitrary: rs2)
+   apply(auto)
+  by (metis append.assoc k0)
+
+lemma  k0a:
+  shows "flts [AALTs bs rs] = map (fuse bs)  rs"
+  apply(simp)
+  done
+
+fun spill where
+ "spill (AALTs bs rs) =  map (fuse bs) rs"
+
+lemma  k0a2:
+  assumes "\<not> nonalt r"  
+  shows "flts [r] = spill r"
+  using  assms
+  apply(case_tac r)
+  apply(simp_all)
+  done
+
+lemma  k0b:
+  assumes "nonalt r" "r \<noteq> AZERO"
+  shows "flts [r] = [r]"
+  using assms
+  apply(case_tac  r)
+  apply(simp_all)
+  done
+
+lemma nn1:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn1q:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn1qq:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn10:
+  assumes "nonnested (AALTs cs rs)" 
+  shows "nonnested (AALTs (bs @ cs) rs)"
+  using assms
+  apply(induct rs arbitrary: cs bs)
+   apply(simp_all)
+  apply(case_tac a)
+       apply(simp_all)
+  done
+
+lemma nn11a:
+  assumes "nonalt r"
+  shows "nonalt (fuse bs r)"
+  using assms
+  apply(induct r)
+       apply(auto)
+  done
+
+
+lemma nn1a:
+  assumes "nonnested r"
+  shows "nonnested (fuse bs r)"
+  using assms
+  apply(induct bs r arbitrary: rule: fuse.induct)
+       apply(simp_all add: nn10)
+  done  
+
+lemma n0:
+  shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+  apply(induct rs  arbitrary: bs)
+   apply(auto)
+    apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+   apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
+  by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+
+  
+  
+
+lemma nn1c:
+  assumes "\<forall>r \<in> set rs. nonnested r"
+  shows "\<forall>r \<in> set (flts rs). nonalt r"
+  using assms
+  apply(induct rs rule: flts.induct)
+        apply(auto)
+  apply(rule nn11a)
+  by (metis nn1qq nonalt.elims(3))
+
+lemma nn1bb:
+  assumes "\<forall>r \<in> set rs. nonalt r"
+  shows "nonnested (bsimp_AALTs bs rs)"
+  using assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply(auto)
+   apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
+  using n0 by auto
+    
+lemma nn1b:
+  shows "nonnested (bsimp r)"
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+   apply(simp)
+    apply(subst bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+  apply (simp add: nn1a)    
+   apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(rule nn1bb)
+  apply(auto)
+  by (metis (mono_tags, hide_lams) imageE nn1c set_map)
+
+lemma rt:
+  shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst  k0)
+  apply(simp)
+  by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
+
+lemma flts_idem:
+  assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+  shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0) 
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+  thm k0 k0a k0b
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(subst k0)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(simp)
+  apply(simp add: k00)
+  apply(subst k0a2)
+   apply(simp)
+  apply(subst k0a2)
+   apply(simp)
+  apply(case_tac a)
+  apply(simp_all)
+  sorry
+
+lemma bsimp_AALTs_idem:
+  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
+  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
+  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
+  apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+  apply(simp)
+  apply(case_tac "\<exists>bs'  rs'. a = AALTs bs' rs'")
+   apply(clarify)
+  apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+
+  apply(drule_tac x="flts (rs' @ list)" in spec)
+  apply(erule impE)
+  prefer 2
+  apply(case_tac a)
+       apply(simp)
+       apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+   apply(case_tac list)
+        apply(simp)
+      apply(simp) 
+   apply(case_tac list)
+        apply(simp)
+     apply(simp) 
+  prefer 3
+   apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+   apply(case_tac list)
+    apply(simp)
+      
+
+       apply(simp) 
+
+      apply(case_tac "flts (map bsimp list)")
+       apply(simp)
+      apply(simp)
+  
+  
+
+   prefer 2
+   apply(simp)
+  
+   apply(subst k0)
+   apply(subst (2) k0)
+  
+  apply(case_tac a)
+       apply(simp_all)
+  
+  prefer 2
+   apply(simp)
+  apply(case_tac r)
+       apply(auto)
+   apply(case_tac "bsimp x42 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp x43 = AZERO")
+   apply(simp)
+   apply(subst bsimp_ASEQ0)
+   apply(subst bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+   apply(subst bsimp_ASEQ2)
+  prefer 2
+      apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(subst (asm) bsimp_ASEQ2)
+   apply(subst (asm) bsimp_ASEQ2)
+  using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
+    
+   apply(case_tac x43)
+        apply(simp_all)
+    prefer 3
+  oops
+
+lemma bsimp_idem:
+  shows "bsimp (bsimp r) = bsimp r"
+apply(induct r taking: "asize" rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   apply(simp)
+   apply (simp add: bsimp_ASEQ_idem)
+  apply(clarify)
+  apply(case_tac x52)
+  apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0)
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+   apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec)
+   apply(drule mp)
+    apply(simp)
+  apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2)
+  apply(simp)
+    apply(subst (asm) flts_idem)
+     apply(auto)[1]
+     apply(drule_tac  x="r" in spec)
+  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
+  apply(simp)
+  apply(subst flts_idem)
+   apply(auto)[1]
+     apply(drule_tac  x="r" in spec)
+  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
+   apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(auto)[1]
+  apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec)
+   apply(drule mp)
+    apply(simp)
+    prefer 2
+    apply(simp)
+  apply(subst (asm) k0)
+  apply(subst (asm) flts_idem)
+     apply(auto)[1]
+  apply (simp add: sum_list_map_remove1)
+  apply(subst (asm) k0b)
+     apply(simp)
+    apply(simp)
+    apply(simp)
+   apply(subst k0)
+  apply(subst flts_idem)
+     apply(auto)[1]
+     apply (simp add: sum_list_map_remove1)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+  apply(simp)
+lemma XX_bder:
+  shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r"
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+  prefer 2
+   apply(simp)
+   apply(case_tac x2a)
+    apply(simp)
+  apply(simp)
+  apply(auto)[1]
+
+
 lemma q3a:
   assumes "\<exists>r \<in> set rs. bnullable r"
   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
@@ -758,11 +1261,7 @@
   apply(simp)
   using qq4 r1 r2 by auto
 
-lemma  k0:
-  shows "flts (r # rs1) = flts [r] @ flts rs1"
-  apply(induct r arbitrary: rs1)
-   apply(auto)
-  done
+
 
 lemma k1:
   assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
@@ -836,6 +1335,16 @@
   done
 
 
+fun extr :: "arexp  \<Rightarrow> (bit list) set" where
+  "extr (AONE bs) = {bs}"
+| "extr (ACHAR bs c) = {bs}"
+| "extr (AALTs bs (r#rs)) = 
+     {bs @ bs' | bs'.  bs' \<in> extr r} \<union>
+     {bs @ bs' | bs'.  bs' \<in> extr (AALTs [] rs)}"
+| "extr (ASEQ bs r1 r2) = 
+     {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}"
+| "extr (ASTAR bs r) = {bs @ [S]} \<union>
+     {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR  [] r)}"
 
 
 lemma MAIN_decode:
@@ -959,7 +1468,16 @@
      apply(simp)
      apply(subst bsimp_ASEQ2)
      apply(subst bsimp_ASEQ2)
-  apply(simp add: erase_fuse)
+     apply(simp add: erase_fuse)
+     apply(case_tac r1)
+          apply(simp_all)
+  using Prf_elims(4) apply fastforce
+      apply(erule Prf_elims)
+      apply(simp)
+  
+      apply(simp)
+  
+  
      defer
      apply(subst bsimp_ASEQ1)
   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce