1 theory BasicIdentities imports 

     2 "Lexer"  "PDerivs"

     3 begin

     4 

     5 datatype rrexp = 

     6   RZERO

     7 | RONE 

     8 | RCHAR char

     9 | RSEQ rrexp rrexp

    10 | RALTS "rrexp list"

    11 | RSTAR rrexp

    12 

    13 abbreviation

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

    15 

    16 

    17 

    18 fun

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

    20 where

    21   "rnullable (RZERO) = False"

    22 | "rnullable (RONE  ) = True"

    23 | "rnullable (RCHAR   c) = False"

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

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

    26 | "rnullable (RSTAR   r) = True"

    27 

    28 

    29 fun

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

    31 where

    32   "rder c (RZERO) = RZERO"

    33 | "rder c (RONE) = RZERO"

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

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

    36 | "rder c (RSEQ r1 r2) = 

    37      (if rnullable r1

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

    39       else RSEQ   (rder c r1) r2)"

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

    41 

    42 

    43 fun 

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

    45 where

    46   "rders r [] = r"

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

    48 

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

    50   where

    51   "rdistinct [] acc = []"

    52 | "rdistinct (x#xs)  acc = 

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

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

    55 

    56 

    57 

    58 

    59 

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

    61   where 

    62   "rflts [] = []"

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

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

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

    66 

    67 

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

    69   where

    70   "rsimp_ALTs  [] = RZERO"

    71 | "rsimp_ALTs [r] =  r"

    72 | "rsimp_ALTs rs = RALTS rs"

    73 

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

    75   where

    76   "rsimp_SEQ  RZERO _ = RZERO"

    77 | "rsimp_SEQ  _ RZERO = RZERO"

    78 | "rsimp_SEQ RONE r2 = r2"

    79 | "rsimp_SEQ r1 r2 = RSEQ r1 r2"

    80 

    81 

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

    83   where

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

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

    86 | "rsimp r = r"

    87 

    88 

    89 fun 

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

    91 where

    92   "rders_simp r [] = r"

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

    94 

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

    96   "rsize RZERO = 1"

    97 | "rsize (RONE) = 1" 

    98 | "rsize (RCHAR  c) = 1"

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

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

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

   102 

   103 

   104 lemma rder_rsimp_ALTs_commute:

   105   shows "  (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"

   106   apply(induct rs)

   107    apply simp

   108   apply(case_tac rs)

   109    apply simp

   110   apply auto

   111   done

   112 

   113 

   114 lemma rsimp_aalts_smaller:

   115   shows "rsize (rsimp_ALTs  rs) \<le> rsize (RALTS rs)"

   116   apply(induct rs)

   117    apply simp

   118   apply simp

   119   apply(case_tac "rs = []")

   120    apply simp

   121   apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp")

   122    apply(erule exE)+

   123    apply simp

   124   apply simp

   125   by(meson neq_Nil_conv)

   126   

   127 

   128 

   129 

   130 

   131 lemma rSEQ_mono:

   132   shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"

   133   apply auto

   134   apply(induct r1)

   135        apply auto

   136       apply(case_tac "r2")

   137        apply simp_all

   138      apply(case_tac r2)

   139           apply simp_all

   140      apply(case_tac r2)

   141          apply simp_all

   142      apply(case_tac r2)

   143         apply simp_all

   144      apply(case_tac r2)

   145   apply simp_all

   146   done

   147 

   148 lemma ralts_cap_mono:

   149   shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) "

   150   by simp

   151 

   152 lemma rflts_def_idiot:

   153   shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>

   154        \<Longrightarrow> rflts (a # rs) = a # rflts rs"

   155   apply(case_tac a)

   156        apply simp_all

   157   done

   158 

   159 

   160 lemma rflts_mono:

   161   shows "sum_list (map rsize (rflts rs))\<le> sum_list (map rsize rs)"

   162   apply(induct rs)

   163   apply simp

   164   apply(case_tac "a = RZERO")

   165    apply simp

   166   apply(case_tac "\<exists>rs1. a = RALTS rs1")

   167   apply(erule exE)

   168    apply simp

   169   apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)")

   170   prefer 2

   171   using rflts_def_idiot apply blast

   172   apply simp

   173   done

   174 

   175 lemma rdistinct_smaller: shows "sum_list (map rsize (rdistinct rs ss)) \<le>

   176 sum_list (map rsize rs )"

   177   apply (induct rs arbitrary: ss)

   178    apply simp

   179   by (simp add: trans_le_add2)

   180 

   181 lemma rdistinct_phi_smaller: "sum_list (map rsize (rdistinct rs {})) \<le> sum_list (map rsize rs)"

   182   by (simp add: rdistinct_smaller)

   183 

   184 

   185 lemma rsimp_alts_mono :

   186   shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa)  \<Longrightarrow>

   187 rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (sum_list (map rsize x))"

   188   apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) 

   189                     \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))")

   190   prefer 2

   191   using rsimp_aalts_smaller apply auto[1]

   192   apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc( sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})))")

   193   prefer 2

   194   using ralts_cap_mono apply blast

   195   apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})) \<le>

   196                      sum_list (map rsize ( (rflts (map rsimp x))))")

   197   prefer 2

   198   using rdistinct_smaller apply presburger

   199   apply(subgoal_tac "sum_list (map rsize (rflts (map rsimp x))) \<le> 

   200                      sum_list (map rsize (map rsimp x))")

   201   prefer 2

   202   using rflts_mono apply blast

   203   apply(subgoal_tac "sum_list (map rsize (map rsimp x)) \<le> sum_list (map rsize x)")

   204   prefer 2

   205   

   206   apply (simp add: sum_list_mono)

   207   by linarith

   208 

   209 

   210 

   211 

   212 

   213 lemma rsimp_mono:

   214   shows "rsize (rsimp r) \<le> rsize r"

   215   apply(induct r)

   216   apply simp_all

   217   apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))")

   218     apply force

   219   using rSEQ_mono

   220    apply presburger

   221   using rsimp_alts_mono by auto

   222 

   223 lemma idiot:

   224   shows "rsimp_SEQ RONE r = r"

   225   apply(case_tac r)

   226        apply simp_all

   227   done

   228 

   229 lemma no_alt_short_list_after_simp:

   230   shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"

   231   sorry

   232 

   233 lemma no_further_dB_after_simp:

   234   shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"

   235   sorry

   236 

   237 

   238 lemma idiot2:

   239   shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>

   240     \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"

   241   apply(case_tac r1)

   242        apply(case_tac r2)

   243   apply simp_all

   244      apply(case_tac r2)

   245   apply simp_all

   246      apply(case_tac r2)

   247   apply simp_all

   248    apply(case_tac r2)

   249   apply simp_all

   250   apply(case_tac r2)

   251        apply simp_all

   252   done

   253 

   254 lemma rders__onechar:

   255   shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"

   256   by simp

   257 

   258 lemma rders_append:

   259   "rders c (s1 @ s2) = rders (rders c s1) s2"

   260   apply(induct s1 arbitrary: c s2)

   261   apply(simp_all)

   262   done

   263 

   264 lemma rders_simp_append:

   265   "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"

   266   apply(induct s1 arbitrary: c s2)

   267   apply(simp_all)

   268   done

   269 

   270 lemma inside_simp_removal:

   271   shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"

   272   sorry

   273 

   274 lemma set_related_list:

   275   shows "distinct rs  \<Longrightarrow> length rs = card (set rs)"

   276   by (simp add: distinct_card)

   277 (*this section deals with the property of distinctBy: creates a list without duplicates*)

   278 lemma rdistinct_never_added_twice:

   279   shows "rdistinct (a # rs) {a} = rdistinct rs {a}"

   280   by force

   281 

   282 

   283 lemma rdistinct_does_the_job:

   284   shows "distinct (rdistinct rs s)"

   285   apply(induct rs arbitrary: s)

   286    apply simp

   287   apply simp

   288   sorry

   289 

   290 lemma rders_simp_same_simpders:

   291   shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"

   292   apply(induct s rule: rev_induct)

   293    apply simp

   294   apply(case_tac "xs = []")

   295    apply simp

   296   apply(simp add: rders_append rders_simp_append)

   297   using inside_simp_removal by blast

   298 

   299 lemma simp_helps_der_pierce:

   300   shows " rsimp

   301             (rder x

   302               (rsimp_ALTs rs)) = 

   303           rsimp 

   304             (rsimp_ALTs 

   305               (map (rder x )

   306                 rs

   307               )

   308             )"

   309   sorry

   310 

   311 

   312 lemma rders_simp_one_char:

   313   shows "rders_simp r [c] = rsimp (rder c r)"

   314   apply auto

   315   done

   316 

   317 lemma rsimp_idem:

   318   shows "rsimp (rsimp r) = rsimp r"

   319   sorry

   320 

   321 corollary rsimp_inner_idem1:

   322   shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"

   323   

   324   sorry

   325 

   326 corollary rsimp_inner_idem2:

   327   shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"

   328   sorry

   329 

   330 corollary rsimp_inner_idem3:

   331   shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"

   332   by (meson map_idI rsimp_inner_idem2)

   333 

   334 corollary rsimp_inner_idem4:

   335   shows "rsimp r = RALTS rs \<Longrightarrow> flts rs = rs"

   336   sorry

   337 

   338 

   339 lemma head_one_more_simp:

   340   shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"

   341   by (simp add: rsimp_idem)

   342 

   343 lemma head_one_more_dersimp:

   344   shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"

   345   using head_one_more_simp rders_simp_append rders_simp_one_char by presburger

   346 

   347 

   348 

   349 

   350 lemma ders_simp_nullability:

   351   shows "rnullable (rders r s) = rnullable (rders_simp r s)"

   352   sorry

   353 

   354 lemma  first_elem_seqder:

   355   shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2)

   356                    # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) "

   357   by auto

   358 

   359 lemma first_elem_seqder1:

   360   shows  "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = 

   361                                           map rsimp ( (RSEQ (rsimp (rder x (rders_simp r xs))) r2) # rs)"

   362   by (simp add: rsimp_idem)

   363 

   364 lemma first_elem_seqdersimps:

   365   shows "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = 

   366                                           map rsimp ( (RSEQ (rders_simp r (xs @ [x])) r2) # rs)"

   367   using first_elem_seqder1 rders_simp_append by auto

   368 

   369 

   370 

   371 

   372 

   373 

   374 lemma seq_ders_closed_form1:

   375   shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # 

   376 (map ( rders_simp r2 ) Ss)))"

   377   apply(case_tac "rnullable r1")

   378    apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = 

   379 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))")

   380     prefer 2

   381     apply (simp add: rsimp_idem)

   382    apply(rule_tac x = "[[c]]" in exI)

   383    apply simp

   384   apply(subgoal_tac  " rders_simp (RSEQ r1 r2) [c] = 

   385 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))")

   386    apply blast

   387   apply(simp add: rsimp_idem)

   388   sorry

   389 

   390 

   391 

   392 

   393 

   394 

   395 

   396 

   397 lemma simp_flatten2:

   398   shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"

   399   sorry

   400 

   401 

   402 lemma simp_flatten:

   403   shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"

   404 

   405   sorry

   406 

   407 

   408 

   409 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where

   410 "vsuf [] _ = []"

   411 |"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]

   412                                       else  (vsuf cs (rder c r1))

   413                    ) "

   414 

   415 

   416 

   417 

   418 

   419 

   420 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where

   421 "star_update c r [] = []"

   422 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 

   423                                 then (s@[c]) # [c] # (star_update c r Ss) 

   424                                else   (s@[c]) # (star_update c r Ss) )"

   425 

   426 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"

   427   where

   428 "star_updates [] r Ss = Ss"

   429 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"

   430 

   431 

   432 

   433 

   434 

   435 

   436 (*some basic facts about rsimp*)

   437 

   438 

   439 

   440 

   441 end