1 theory Rsimp imports "Lexer"

     2 begin

     3 

     4 datatype rrexp = 

     5   RZERO

     6 | RONE 

     7 | RCHAR char

     8 | RSEQ rrexp rrexp

     9 | RALTS "rrexp list"

    10 | RSTAR rrexp

    11 

    12 abbreviation

    13   "RALT r1 r2 \<equiv> RALTS [r1, r2]"

    14 

    15 

    16 fun

    17   RL :: "rrexp \<Rightarrow> string set"

    18 where

    19   "RL (RZERO) = {}"

    20 | "RL (RONE) = {[]}"

    21 | "RL (RCHAR c) = {[c]}"

    22 | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"

    23 | "RL (RALTS rs) = (\<Union> (set (map RL rs)))"

    24 | "RL (RSTAR r) = (RL r)\<star>"

    25 

    26 

    27 

    28 fun

    29  rnullable :: "rrexp \<Rightarrow> bool"

    30 where

    31   "rnullable (RZERO) = False"

    32 | "rnullable (RONE) = True"

    33 | "rnullable (RCHAR c) = False"

    34 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"

    35 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"

    36 | "rnullable (RSTAR r) = True"

    37 

    38 

    39 fun

    40  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"

    41 where

    42   "rder c (RZERO) = RZERO"

    43 | "rder c (RONE) = RZERO"

    44 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)"

    45 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"

    46 | "rder c (RSEQ r1 r2) = 

    47      (if rnullable r1

    48       then RALT   (RSEQ (rder c r1) r2) (rder c r2)

    49       else RSEQ   (rder c r1) r2)"

    50 | "rder c (RSTAR r) = RSEQ  (rder c r) (RSTAR r)"

    51 

    52 

    53 fun 

    54   rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"

    55 where

    56   "rders r [] = r"

    57 | "rders r (c#s) = rders (rder c r) s"

    58 

    59 fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list"

    60   where

    61   "rdistinct [] acc = []"

    62 | "rdistinct (x#xs)  acc = 

    63      (if x \<in> acc then rdistinct xs  acc 

    64       else x # (rdistinct xs  ({x} \<union> acc)))"

    65 

    66 

    67 fun rflts :: "rrexp list \<Rightarrow> rrexp list"

    68   where 

    69   "rflts [] = []"

    70 | "rflts (RZERO # rs) = rflts rs"

    71 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"

    72 | "rflts (r1 # rs) = r1 # rflts rs"

    73 

    74 fun nonalt :: "rrexp \<Rightarrow> bool"

    75   where

    76   "nonalt (RALTS  rs) = False"

    77 | "nonalt r = True"

    78 

    79 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"

    80   where

    81   "rsimp_ALTs  [] = RZERO"

    82 | "rsimp_ALTs [r] =  r"

    83 | "rsimp_ALTs rs = RALTS rs"

    84 

    85 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"

    86   where

    87   "rsimp_SEQ  RZERO _ = RZERO"

    88 | "rsimp_SEQ  _ RZERO = RZERO"

    89 | "rsimp_SEQ RONE r2 = r2"

    90 | "rsimp_SEQ r1 r2 = RSEQ r1 r2"

    91 

    92 

    93 fun rsimp :: "rrexp \<Rightarrow> rrexp" 

    94   where

    95   "rsimp (RSEQ r1 r2) = rsimp_SEQ  (rsimp r1) (rsimp r2)"

    96 | "rsimp (RALTS rs) = rsimp_ALTs  (rdistinct (rflts (map rsimp rs))  {}) "

    97 | "rsimp r = r"

    98 

    99 

   100 fun 

   101   rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"

   102 where

   103   "rders_simp r [] = r"

   104 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"

   105 

   106 fun rsize :: "rrexp \<Rightarrow> nat" where

   107   "rsize RZERO = 1"

   108 | "rsize (RONE) = 1" 

   109 | "rsize (RCHAR  c) = 1"

   110 | "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"

   111 | "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"

   112 | "rsize (RSTAR  r) = Suc (rsize r)"

   113 

   114 abbreviation rsizes where

   115   "rsizes rs \<equiv> sum_list (map rsize rs)"

   116 

   117 fun nonnested :: "rrexp \<Rightarrow> bool"

   118   where

   119   "nonnested (RALTS []) = True"

   120 | "nonnested (RALTS ((RALTS rs1) # rs2)) = False"

   121 | "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"

   122 | "nonnested r = True"

   123 

   124 

   125 fun good :: "rrexp \<Rightarrow> bool" where

   126   "good RZERO = False"

   127 | "good (RONE) = True" 

   128 | "good (RCHAR c) = True"

   129 | "good (RALTS []) = False"

   130 | "good (RALTS [r]) = False"

   131 | "good (RALTS (r1 # r2 # rs)) = 

   132     ((distinct ( (r1 # r2 # rs))) \<and>

   133      (\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"

   134 | "good (RSEQ RZERO _) = False"

   135 | "good (RSEQ RONE _) = False"

   136 | "good (RSEQ  _ RZERO) = False"

   137 | "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

   138 | "good (RSTAR r) = True"

   139 

   140 fun nonazero :: "rrexp \<Rightarrow> bool"

   141   where

   142   "nonazero RZERO = False"

   143 | "nonazero r = True"

   144 

   145 

   146 

   147 

   148 

   149 

   150 lemma basic_rsimp_SEQ_property1:

   151   shows "rsimp_SEQ RONE r = r"

   152   apply(induct r)

   153        apply simp+

   154   done

   155 

   156 

   157 lemma basic_rsimp_SEQ_property3:

   158   shows "rsimp_SEQ r RZERO = RZERO"  

   159   using rsimp_SEQ.elims by blast

   160 

   161 

   162 lemma rsimpalts_conscons:

   163   shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"

   164   by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))

   165 

   166 lemma rsimp_alts_equal:

   167   shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) "

   168   by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)

   169 

   170 

   171 end