1 theory BasicIdentities 

     2   imports "Lexer" 

     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 | RNTIMES rrexp nat

    13 

    14 abbreviation

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

    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 | "rnullable (RNTIMES r n) = (if n = 0 then True else rnullable r)"

    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 | "rder c (RNTIMES r n) = (if n = 0 then RZERO else RSEQ (rder c r) (RNTIMES r (n - 1)))"

    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 lemma rdistinct1:

    57   assumes "a \<in> acc"

    58   shows "a \<notin> set (rdistinct rs acc)"

    59   using assms

    60   apply(induct rs arbitrary: acc a)

    61    apply(auto)

    62   done

    63 

    64 

    65 lemma rdistinct_does_the_job:

    66   shows "distinct (rdistinct rs s)"

    67   apply(induct rs s rule: rdistinct.induct)

    68   apply(auto simp add: rdistinct1)

    69   done

    70 

    71 

    72 

    73 lemma rdistinct_concat:

    74   assumes "set rs \<subseteq> rset"

    75   shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset"

    76   using assms

    77   apply(induct rs)

    78   apply simp+

    79   done

    80 

    81 lemma distinct_not_exist:

    82   assumes "a \<notin> set rs"

    83   shows "rdistinct rs rset = rdistinct rs (insert a rset)"

    84   using assms

    85   apply(induct rs arbitrary: rset)

    86   apply(auto)

    87   done

    88 

    89 lemma rdistinct_on_distinct:

    90   shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"

    91   apply(induct rs)

    92   apply simp

    93   using distinct_not_exist by fastforce

    94 

    95 lemma distinct_rdistinct_append:

    96   assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"

    97   shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"

    98   using assms

    99   apply(induct rs1 arbitrary: rsa acc)

   100    apply(auto)[1]

   101   apply(auto)[1]

   102   apply(drule_tac x="rsa" in meta_spec)

   103   apply(drule_tac x="{a} \<union> acc" in meta_spec)

   104   apply(simp)

   105   apply(drule meta_mp)

   106    apply(auto)[1]

   107   apply(simp)

   108   done

   109   

   110 

   111 lemma rdistinct_set_equality1:

   112   shows "set (rdistinct rs acc) = set rs - acc"

   113   apply(induct rs acc rule: rdistinct.induct)

   114   apply(auto)

   115   done

   116 

   117 

   118 lemma rdistinct_set_equality:

   119   shows "set (rdistinct rs {}) = set rs"

   120   by (simp add: rdistinct_set_equality1)

   121 

   122 

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

   124   where 

   125   "rflts [] = []"

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

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

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

   129 

   130 

   131 lemma rflts_def_idiot:

   132   shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs"

   133   apply(case_tac a)

   134   apply simp_all

   135   done

   136 

   137 lemma rflts_def_idiot2:

   138   shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"

   139   apply(induct rs rule: rflts.induct)

   140   apply(auto)

   141   done

   142 

   143 lemma flts_append:

   144   shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"

   145   apply(induct rs1)

   146    apply simp

   147   apply(case_tac a)

   148        apply simp+

   149   done

   150 

   151 

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

   153   where

   154   "rsimp_ALTs  [] = RZERO"

   155 | "rsimp_ALTs [r] =  r"

   156 | "rsimp_ALTs rs = RALTS rs"

   157 

   158 lemma rsimpalts_conscons:

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

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

   161 

   162 lemma rsimp_alts_equal:

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

   164   by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)

   165 

   166 

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

   168   where

   169   "rsimp_SEQ  RZERO _ = RZERO"

   170 | "rsimp_SEQ  _ RZERO = RZERO"

   171 | "rsimp_SEQ RONE r2 = r2"

   172 | "rsimp_SEQ r1 r2 = RSEQ r1 r2"

   173 

   174 

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

   176   where

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

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

   179 | "rsimp r = r"

   180 

   181 

   182 fun 

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

   184 where

   185   "rders_simp r [] = r"

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

   187 

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

   189   "rsize RZERO = 1"

   190 | "rsize (RONE) = 1" 

   191 | "rsize (RCHAR  c) = 1"

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

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

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

   195 | "rsize (RNTIMES  r n) = Suc (rsize r) + n"

   196 

   197 abbreviation rsizes where

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

   199 

   200 

   201 lemma rder_rsimp_ALTs_commute:

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

   203   apply(induct rs)

   204    apply simp

   205   apply(case_tac rs)

   206    apply simp

   207   apply auto

   208   done

   209 

   210 

   211 lemma rsimp_aalts_smaller:

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

   213   apply(induct rs)

   214    apply simp

   215   apply simp

   216   apply(case_tac "rs = []")

   217    apply simp

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

   219    apply(erule exE)+

   220    apply simp

   221   apply simp

   222   by(meson neq_Nil_conv)

   223   

   224 

   225 

   226 

   227 

   228 lemma rSEQ_mono:

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

   230   apply auto

   231   apply(induct r1)

   232        apply auto

   233       apply(case_tac "r2")

   234        apply simp_all

   235      apply(case_tac r2)

   236           apply simp_all

   237      apply(case_tac r2)

   238          apply simp_all

   239      apply(case_tac r2)

   240         apply simp_all

   241      apply(case_tac r2)

   242          apply simp_all

   243   apply(case_tac r2)

   244          apply simp_all

   245   done

   246 

   247 lemma ralts_cap_mono:

   248   shows "rsize (RALTS rs) \<le> Suc (rsizes rs)"

   249   by simp

   250 

   251 

   252 

   253 

   254 lemma rflts_mono:

   255   shows "rsizes (rflts rs) \<le> rsizes rs"

   256   apply(induct rs)

   257   apply simp

   258   apply(case_tac "a = RZERO")

   259    apply simp

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

   261   apply(erule exE)

   262    apply simp

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

   264    prefer 2

   265   

   266   using rflts_def_idiot apply blast

   267   apply simp

   268   done

   269 

   270 lemma rdistinct_smaller: 

   271   shows "rsizes (rdistinct rs ss) \<le> rsizes rs"

   272   apply (induct rs arbitrary: ss)

   273    apply simp

   274   by (simp add: trans_le_add2)

   275 

   276 

   277 lemma rsimp_alts_mono :

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

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

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

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

   282   prefer 2

   283   using rsimp_aalts_smaller apply auto[1]

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

   285   prefer 2

   286   using ralts_cap_mono apply blast

   287   apply(subgoal_tac "rsizes (rdistinct (rflts (map rsimp x)) {}) \<le> rsizes (rflts (map rsimp x))")

   288   prefer 2

   289   using rdistinct_smaller apply presburger

   290   apply(subgoal_tac "rsizes (rflts (map rsimp x)) \<le> rsizes (map rsimp x)")

   291   prefer 2

   292   using rflts_mono apply blast

   293   apply(subgoal_tac "rsizes (map rsimp x) \<le> rsizes x")

   294   prefer 2

   295   

   296   apply (simp add: sum_list_mono)

   297   by linarith

   298 

   299 

   300 

   301 

   302 

   303 lemma rsimp_mono:

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

   305   apply(induct r)

   306   apply simp_all

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

   308     apply force

   309   using rSEQ_mono

   310    apply presburger

   311   using rsimp_alts_mono by auto

   312 

   313 lemma idiot:

   314   shows "rsimp_SEQ RONE r = r"

   315   apply(case_tac r)

   316        apply simp_all

   317   done

   318 

   319 

   320 

   321 

   322 

   323 lemma idiot2:

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

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

   326   apply(case_tac r1)

   327        apply(case_tac r2)

   328   apply simp_all

   329      apply(case_tac r2)

   330   apply simp_all

   331      apply(case_tac r2)

   332   apply simp_all

   333    apply(case_tac r2)

   334   apply simp_all

   335   apply(case_tac r2)

   336          apply simp_all

   337 apply(case_tac r2)

   338          apply simp_all

   339   done

   340 

   341 lemma rders__onechar:

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

   343   by simp

   344 

   345 lemma rders_append:

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

   347   apply(induct s1 arbitrary: c s2)

   348   apply(simp_all)

   349   done

   350 

   351 lemma rders_simp_append:

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

   353   apply(induct s1 arbitrary: c s2)

   354    apply(simp_all)

   355   done

   356 

   357 

   358 lemma rders_simp_one_char:

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

   360   apply auto

   361   done

   362 

   363 

   364 

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

   366   where

   367   "nonalt (RALTS  rs) = False"

   368 | "nonalt r = True"

   369 

   370 

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

   372   "good RZERO = False"

   373 | "good (RONE) = True" 

   374 | "good (RCHAR c) = True"

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

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

   377 | "good (RALTS (r1 # r2 # rs)) = ((distinct ( (r1 # r2 # rs))) \<and>(\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"

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

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

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

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

   382 | "good (RSTAR r) = True"

   383 | "good (RNTIMES r n) = True"

   384 

   385 lemma  k0a:

   386   shows "rflts [RALTS rs] =   rs"

   387   apply(simp)

   388   done

   389 

   390 lemma bbbbs:

   391   assumes "good r" "r = RALTS rs"

   392   shows "rsimp_ALTs  (rflts [r]) = RALTS rs"

   393   using  assms

   394   by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)

   395 

   396 lemma bbbbs1:

   397   shows "nonalt r \<or> (\<exists> rs. r  = RALTS  rs)"

   398   by (meson nonalt.elims(3))

   399 

   400 

   401 

   402 lemma good0:

   403   assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"

   404   shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"

   405   using  assms

   406   apply(induct  rs rule: rsimp_ALTs.induct)

   407   apply(auto)

   408   done

   409 

   410 lemma flts1:

   411   assumes "good r" 

   412   shows "rflts [r] \<noteq> []"

   413   using  assms

   414   apply(induct r)

   415        apply(simp_all)

   416   using good.simps(4) by blast

   417 

   418 lemma flts2:

   419   assumes "good r" 

   420   shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"

   421   using  assms

   422   apply(induct r)

   423        apply(simp)

   424       apply(simp)

   425      apply(simp)

   426     prefer 2

   427     apply(simp)

   428     apply(auto)[1]

   429   

   430      apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

   431     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

   432    apply fastforce

   433    apply(simp)

   434   by simp

   435 

   436 

   437 lemma flts3:

   438   assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 

   439   shows "\<forall>r \<in> set (rflts rs). good r"

   440   using  assms

   441   apply(induct rs arbitrary: rule: rflts.induct)

   442         apply(simp_all)

   443   by (metis UnE flts2 k0a)

   444 

   445 

   446 lemma  k0:

   447   shows "rflts (r # rs1) = rflts [r] @ rflts rs1"

   448   apply(induct r arbitrary: rs1)

   449    apply(auto)

   450   done

   451 

   452 

   453 lemma good_SEQ:

   454   assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"

   455   shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

   456   using assms

   457   apply(case_tac r1)

   458        apply(simp_all)

   459   apply(case_tac r2)

   460           apply(simp_all)

   461   apply(case_tac r2)

   462          apply(simp_all)

   463   apply(case_tac r2)

   464         apply(simp_all)

   465   apply(case_tac r2)

   466          apply(simp_all)

   467 apply(case_tac r2)

   468          apply(simp_all)

   469   done

   470 

   471 lemma rsize0:

   472   shows "0 < rsize r"

   473   apply(induct  r)

   474        apply(auto)

   475   done

   476 

   477 

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

   479   where

   480   "nonnested (RALTS []) = True"

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

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

   483 | "nonnested r = True"

   484 

   485 

   486 

   487 lemma  k00:

   488   shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"

   489   apply(induct rs1 arbitrary: rs2)

   490    apply(auto)

   491   by (metis append.assoc k0)

   492 

   493 

   494 

   495 

   496 lemma k0b:

   497   assumes "nonalt r" "r \<noteq> RZERO"

   498   shows "rflts [r] = [r]"

   499   using assms

   500   apply(case_tac  r)

   501   apply(simp_all)

   502   done

   503 

   504 lemma nn1qq:

   505   assumes "nonnested (RALTS rs)"

   506   shows "\<nexists> rs1. RALTS rs1 \<in> set rs"

   507   using assms

   508   apply(induct rs rule: rflts.induct)

   509   apply(auto)

   510   done

   511 

   512  

   513 

   514 lemma n0:

   515   shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"

   516   apply(induct rs )

   517    apply(auto)

   518     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))

   519   apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7) nonnested.simps(8))

   520   using bbbbs1 apply fastforce

   521   by (metis bbbbs1 list.set_intros(2) nn1qq)

   522 

   523   

   524   

   525 

   526 lemma nn1c:

   527   assumes "\<forall>r \<in> set rs. nonnested r"

   528   shows "\<forall>r \<in> set (rflts rs). nonalt r"

   529   using assms

   530   apply(induct rs rule: rflts.induct)

   531         apply(auto)

   532   using n0 by blast

   533 

   534 lemma nn1bb:

   535   assumes "\<forall>r \<in> set rs. nonalt r"

   536   shows "nonnested (rsimp_ALTs  rs)"

   537   using assms

   538   apply(induct  rs rule: rsimp_ALTs.induct)

   539     apply(auto)

   540   using nonalt.simps(1) nonnested.elims(3) apply blast

   541   using n0 by auto

   542 

   543 lemma bsimp_ASEQ0:

   544   shows "rsimp_SEQ  r1 RZERO = RZERO"

   545   apply(induct r1)

   546   apply(auto)

   547   done

   548 

   549 lemma nn1b:

   550   shows "nonnested (rsimp r)"

   551   apply(induct r)

   552        apply(simp_all)

   553   apply(case_tac "rsimp r1 = RZERO")

   554     apply(simp)

   555  apply(case_tac "rsimp r2 = RZERO")

   556    apply(simp)

   557     apply(subst bsimp_ASEQ0)

   558   apply(simp)

   559   apply(case_tac "\<exists>bs. rsimp r1 = RONE")

   560     apply(auto)[1]

   561   using idiot apply fastforce

   562   apply (simp add: idiot2)

   563   by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality)

   564 

   565 lemma nonalt_flts_rd:

   566   shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>

   567        \<Longrightarrow> nonalt xa"

   568   by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1)

   569 

   570 

   571 lemma rsimpalts_implies1:

   572   shows " rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> a = RZERO"

   573   using rsimp_ALTs.elims by auto

   574 

   575 

   576 lemma rsimpalts_implies2:

   577   shows "rsimp_ALTs (a # rdistinct rs rset) = RZERO \<Longrightarrow> rdistinct rs rset = []"

   578   by (metis append_butlast_last_id rrexp.distinct(7) rsimpalts_conscons)

   579 

   580 lemma rsimpalts_implies21:

   581   shows "rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> rdistinct rs {a} = []"

   582   using rsimpalts_implies2 by blast

   583 

   584 

   585 lemma bsimp_ASEQ2:

   586   shows "rsimp_SEQ RONE r2 =  r2"

   587   apply(induct r2)

   588   apply(auto)

   589   done

   590 

   591 lemma elem_smaller_than_set:

   592   shows "xa \<in> set  list \<Longrightarrow> rsize xa < Suc (rsizes list)"

   593   apply(induct list)

   594    apply simp

   595   by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)

   596 

   597 lemma rsimp_list_mono:

   598   shows "rsizes (map rsimp rs) \<le> rsizes rs"

   599   apply(induct rs)

   600    apply simp+

   601   by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono)

   602 

   603 

   604 (*says anything coming out of simp+flts+db will be good*)

   605 lemma good2_obv_simplified:

   606   shows " \<lbrakk>\<forall>y. rsize y < Suc (rsizes rs) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;

   607            xa \<in> set (rdistinct (rflts (map rsimp rs)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk> \<Longrightarrow> good xa"

   608   apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")

   609   prefer 2

   610    apply (simp add: elem_smaller_than_set)

   611   by (metis Diff_empty flts3 rdistinct_set_equality1)

   612 

   613 thm Diff_empty flts3 rdistinct_set_equality1

   614   

   615 lemma good1:

   616   shows "good (rsimp a) \<or> rsimp a = RZERO"

   617   apply(induct a taking: rsize rule: measure_induct)

   618   apply(case_tac x)

   619   apply(simp)

   620   apply(simp)

   621   apply(simp)

   622   prefer 3

   623     apply(simp)

   624    prefer 2

   625    apply(simp only:)

   626    apply simp

   627   apply (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) elem_smaller_than_set good0 good2_obv_simplified le_eq_less_or_eq nonalt_flts_rd order_less_trans plus_1_eq_Suc rdistinct_does_the_job rdistinct_smaller rflts_mono rsimp_ALTs.simps(1) rsimp_list_mono)

   628   apply simp

   629   apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO")

   630    apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO")

   631     apply(case_tac "rsimp x41 = RZERO")

   632      apply simp

   633     apply(case_tac "rsimp x42 = RZERO")

   634      apply simp

   635   using bsimp_ASEQ0 apply blast

   636     apply(subgoal_tac "good (rsimp x41)")

   637      apply(subgoal_tac "good (rsimp x42)")

   638       apply simp

   639   apply (metis bsimp_ASEQ2 good_SEQ idiot2)

   640   apply blast

   641   apply fastforce

   642   using less_add_Suc2 apply blast  

   643   using less_iff_Suc_add apply blast

   644   using good.simps(45) rsimp.simps(7) by presburger

   645   

   646 

   647 

   648 fun

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

   650 where

   651   "RL (RZERO) = {}"

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

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

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

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

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

   657 | "RL (RNTIMES r n) = (RL r) ^^ n"

   658 

   659 lemma pow_rempty_iff:

   660   shows "[] \<in> (RL r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (RL r))"

   661   by (induct n) (auto simp add: Sequ_def)

   662 

   663 lemma RL_rnullable:

   664   shows "rnullable r = ([] \<in> RL r)"

   665   apply(induct r)

   666         apply(auto simp add: Sequ_def pow_rempty_iff)

   667   done

   668 

   669 lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A ;; B"

   670 by (metis append_Nil concI)

   671 

   672 

   673 lemma empty_pow_add:

   674   fixes A::"string set"

   675   assumes "[] \<in> A" "s \<in> A ^^ n"

   676   shows "s \<in> A ^^ (n + m)"

   677   using assms

   678   apply(induct m arbitrary: n)

   679    apply(auto simp add: Sequ_def)

   680   done

   681 

   682 (*

   683 lemma der_pow:

   684   shows "Der c (A ^^ n) = (if n = 0 then {} else (Der c A) ;; (A ^^ (n - 1)))"

   685   apply(induct n arbitrary: A)

   686    apply(auto)

   687   by (smt (verit, best) Suc_pred concE concI concI_if_Nil2 conc_pow_comm lang_pow.simps(2))

   688 *)

   689 

   690 lemma RL_rder:

   691   shows "RL (rder c r) = Der c (RL r)"

   692   apply(induct r)

   693   apply(auto simp add: Sequ_def Der_def)[5]

   694         apply (metis append_Cons)

   695   using RL_rnullable apply blast

   696   apply (metis append_eq_Cons_conv)

   697   apply (metis append_Cons)

   698     apply (metis RL_rnullable append_eq_Cons_conv)

   699   apply simp

   700   apply(simp)

   701   done

   702 

   703 lemma RL_rsimp_RSEQ:

   704   shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)"

   705   apply(induct r1 r2 rule: rsimp_SEQ.induct)

   706   apply(simp_all)

   707   done

   708 

   709 lemma RL_rsimp_RALTS:

   710   shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))"

   711   apply(induct rs rule: rsimp_ALTs.induct)

   712   apply(simp_all)

   713   done

   714 

   715 lemma RL_rsimp_rdistinct:

   716   shows "(\<Union> (set (map RL (rdistinct rs {})))) = (\<Union> (set (map RL rs)))"

   717   apply(auto)

   718   apply (metis Diff_iff rdistinct_set_equality1)

   719   by (metis Diff_empty rdistinct_set_equality1)

   720 

   721 lemma RL_rsimp_rflts:

   722   shows "(\<Union> (set (map RL (rflts rs)))) = (\<Union> (set (map RL rs)))"

   723   apply(induct rs rule: rflts.induct)

   724   apply(simp_all)

   725   done

   726 

   727 lemma RL_rsimp:

   728   shows "RL r = RL (rsimp r)"

   729   apply(induct r rule: rsimp.induct)

   730        apply(auto simp add: Sequ_def RL_rsimp_RSEQ)

   731   using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1]

   732   by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map)

   733 

   734   

   735 lemma qqq1:

   736   shows "RZERO \<notin> set (rflts (map rsimp rs))"

   737   by (metis ex_map_conv flts3 good.simps(1) good1)

   738 

   739 

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

   741   where

   742   "nonazero RZERO = False"

   743 | "nonazero r = True"

   744 

   745 

   746 lemma flts_single1:

   747   assumes "nonalt r" "nonazero r"

   748   shows "rflts [r] = [r]"

   749   using assms

   750   apply(induct r)

   751   apply(auto)

   752   done

   753 

   754 lemma nonalt0_flts_keeps:

   755   shows "(a \<noteq> RZERO) \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (a # xs) = a # rflts xs"

   756   apply(case_tac a)

   757        apply simp+

   758   done

   759 

   760 

   761 lemma nonalt0_fltseq:

   762   shows "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r \<Longrightarrow> rflts rs = rs"

   763   apply(induct rs)

   764    apply simp

   765   apply(case_tac "a = RZERO")

   766    apply fastforce

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

   768    apply(erule exE)

   769    apply simp+

   770   using nonalt0_flts_keeps by presburger

   771 

   772   

   773 

   774 

   775 lemma goodalts_nonalt:

   776   shows "good (RALTS rs) \<Longrightarrow> rflts rs = rs"

   777   apply(induct x == "RALTS rs" arbitrary: rs rule: good.induct)

   778     apply simp

   779   

   780   using good.simps(5) apply blast

   781   apply simp

   782   apply(case_tac "r1 = RZERO")

   783   using good.simps(1) apply force

   784   apply(case_tac "r2 = RZERO")

   785   using good.simps(1) apply force

   786   apply(subgoal_tac "rflts (r1 # r2 # rs) = r1 # r2 # rflts rs")

   787   prefer 2

   788    apply (metis nonalt.simps(1) rflts_def_idiot)

   789   apply(subgoal_tac "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r")

   790    apply(subgoal_tac "rflts rs = rs")

   791     apply presburger

   792   using nonalt0_fltseq apply presburger

   793   using good.simps(1) by blast

   794   

   795 

   796   

   797 

   798 

   799 lemma test:

   800   assumes "good r"

   801   shows "rsimp r = r"

   802 

   803   using assms

   804   apply(induct rule: good.induct)

   805                       apply simp

   806                       apply simp

   807                       apply simp

   808                       apply simp

   809                       apply simp

   810                       apply(subgoal_tac "distinct (r1 # r2 # rs)")

   811   prefer 2

   812   using good.simps(6) apply blast

   813   apply(subgoal_tac "rflts (r1 # r2 # rs ) = r1 # r2 # rs")

   814   prefer 2

   815   using goodalts_nonalt apply blast

   816 

   817                       apply(subgoal_tac "r1 \<noteq> r2")

   818   prefer 2

   819                       apply (meson distinct_length_2_or_more)

   820                       apply(subgoal_tac "r1 \<notin> set rs")

   821                       apply(subgoal_tac "r2 \<notin> set rs")

   822                       apply(subgoal_tac "\<forall>r \<in> set rs. rsimp r = r")

   823                       apply(subgoal_tac "map rsimp rs = rs")

   824   apply simp             

   825                       apply(subgoal_tac "\<forall>r \<in>  {r1, r2}. r \<notin> set rs")

   826   apply (metis distinct_not_exist rdistinct_on_distinct)

   827   

   828                       apply blast

   829                       apply (meson map_idI)

   830                       apply (metis good.simps(6) insert_iff list.simps(15))

   831 

   832   apply (meson distinct.simps(2))

   833                       apply (simp add: distinct_length_2_or_more)

   834                       apply simp+

   835   done

   836 

   837 

   838 

   839 lemma rsimp_idem:

   840   shows "rsimp (rsimp r) = rsimp r"

   841   using test good1

   842   by force

   843 

   844 corollary rsimp_inner_idem4:

   845   shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"

   846   by (metis good1 goodalts_nonalt rrexp.simps(12))

   847 

   848 

   849 lemma head_one_more_simp:

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

   851   by (simp add: rsimp_idem)

   852 

   853 

   854 lemma der_simp_nullability:

   855   shows "rnullable r = rnullable (rsimp r)"

   856   using RL_rnullable RL_rsimp by auto

   857   

   858 

   859 lemma no_alt_short_list_after_simp:

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

   861   by (metis bbbbs good1 k0a rrexp.simps(12))

   862 

   863 

   864 lemma no_further_dB_after_simp:

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

   866   apply(subgoal_tac "good (RALTS rs)")

   867   apply(subgoal_tac "distinct rs")

   868   using rdistinct_on_distinct apply blast

   869   apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2)

   870   using good1 by fastforce

   871 

   872 

   873 lemma idem_after_simp1:

   874   shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"

   875   apply(case_tac "rsimp aa")

   876   apply simp+

   877   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)

   878    apply(simp)

   879   apply(simp)

   880   done

   881 

   882 lemma identity_wwo0:

   883   shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"

   884   apply (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))

   885   done

   886 

   887 lemma distinct_removes_last:

   888   shows "\<lbrakk>a \<in> set as\<rbrakk>

   889     \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"

   890 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"

   891   apply(induct as arbitrary: rset ab rset1 a)

   892      apply simp

   893     apply simp

   894   apply(case_tac "aa \<in> rset")

   895    apply(case_tac "a = aa")

   896   apply (metis append_Cons)

   897     apply simp

   898    apply(case_tac "a \<in> set as")

   899   apply (metis append_Cons rdistinct.simps(2) set_ConsD)

   900    apply(case_tac "a = aa")

   901     prefer 2

   902     apply simp

   903    apply (metis append_Cons)

   904   apply(case_tac "ab \<in> rset1")

   905   prefer 2

   906    apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 

   907                ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")

   908   prefer 2

   909   apply force

   910   apply(simp only:)

   911      apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")

   912     apply(simp only:)

   913     apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")

   914      apply blast

   915     apply(case_tac "a \<in> insert ab rset1")

   916      apply simp

   917      apply (metis insertI1)

   918     apply simp

   919     apply (meson insertI1)

   920    apply simp

   921   apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")

   922    apply simp

   923   by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))

   924 

   925 

   926 lemma distinct_removes_middle:

   927   shows  "\<lbrakk>a \<in> set as\<rbrakk>

   928     \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"

   929 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"

   930    apply(induct as arbitrary: rset rset1 ab as2 as3 a)

   931      apply simp

   932     apply simp

   933    apply(case_tac "a \<in> rset")

   934     apply simp

   935     apply metis

   936    apply simp

   937    apply (metis insertI1)

   938   apply(case_tac "a = ab")

   939    apply simp

   940    apply(case_tac "ab \<in> rset")

   941     apply simp

   942     apply presburger

   943    apply (meson insertI1)

   944   apply(case_tac "a \<in> rset")

   945   apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)

   946   apply(case_tac "ab \<in> rset")

   947   apply simp

   948    apply (meson insert_iff)

   949   apply simp

   950   by (metis insertI1)

   951 

   952 

   953 lemma distinct_removes_middle3:

   954   shows  "\<lbrakk>a \<in> set as\<rbrakk>

   955     \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"

   956   using distinct_removes_middle(1) by fastforce

   957 

   958 

   959 lemma distinct_removes_list:

   960   shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"

   961   apply(induct rs)

   962    apply simp+

   963   apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")

   964    prefer 2

   965   apply (metis append_Cons append_Nil distinct_removes_middle(1))

   966   by presburger

   967 

   968 

   969 lemma spawn_simp_rsimpalts:

   970   shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"

   971   apply(cases rs)

   972    apply simp

   973   apply(case_tac list)

   974    apply simp

   975    apply(subst rsimp_idem[symmetric])

   976    apply simp

   977   apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")

   978    apply(simp only:)

   979    apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")

   980     apply(simp only:)

   981   prefer 2

   982   apply simp

   983    prefer 2

   984   using rsimp_ALTs.simps(3) apply presburger

   985   apply auto

   986   apply(subst rsimp_idem)+

   987   by (metis comp_apply rsimp_idem)

   988 

   989 

   990 lemma simp_singlealt_flatten:

   991   shows "rsimp (RALTS [RALTS rsa]) = rsimp (RALTS (rsa @ []))"

   992   apply(induct rsa)

   993    apply simp

   994   apply simp

   995   by (metis idem_after_simp1 list.simps(9) rsimp.simps(2))

   996 

   997 

   998 lemma good1_rsimpalts:

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

  1000   by (metis no_alt_short_list_after_simp) 

  1001   

  1002 

  1003 

  1004 

  1005 lemma good1_flatten:

  1006   shows "\<lbrakk> rsimp r =  (RALTS rs1)\<rbrakk>

  1007        \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)"

  1008   apply(subst good1_rsimpalts)

  1009    apply simp+

  1010   apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")

  1011    apply simp

  1012   using flts_append rsimp_inner_idem4 by presburger

  1013 

  1014   

  1015 lemma flatten_rsimpalts:

  1016   shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = 

  1017          rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"

  1018   apply(case_tac "map rsimp rsa")

  1019    apply simp

  1020   apply(case_tac "list")

  1021    apply simp

  1022    apply(case_tac a)

  1023         apply simp+

  1024     apply(rename_tac rs1)

  1025     apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)

  1026   

  1027   apply simp

  1028   

  1029   apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")

  1030    apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")

  1031      apply simp

  1032   apply auto[1]

  1033   apply simp

  1034   apply(simp)

  1035    apply(case_tac "lista")

  1036   apply simp_all

  1037  

  1038    apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)

  1039    by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)

  1040 

  1041 lemma last_elem_out:

  1042   shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"

  1043   apply(induct xs arbitrary: rset)

  1044   apply simp+

  1045   done

  1046 

  1047 

  1048 

  1049 

  1050 lemma rdistinct_concat_general:

  1051   shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"

  1052   apply(induct rs1 arbitrary: rs2 rule: rev_induct)

  1053    apply simp

  1054   apply(drule_tac x = "x # rs2" in meta_spec)

  1055   apply simp

  1056   apply(case_tac "x \<in> set xs")

  1057    apply simp

  1058   

  1059    apply (simp add: distinct_removes_middle3 insert_absorb)

  1060   apply simp

  1061   by (simp add: last_elem_out)

  1062 

  1063 

  1064   

  1065 

  1066 lemma distinct_once_enough:

  1067   shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"

  1068   apply(subgoal_tac "distinct (rdistinct rs {})")

  1069    apply(subgoal_tac 

  1070 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")

  1071   apply(simp only:)

  1072   using rdistinct_concat_general apply blast

  1073   apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)

  1074   by (simp add: rdistinct_does_the_job)

  1075   

  1076 

  1077 lemma simp_flatten:

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

  1079   apply simp

  1080   apply(subst flatten_rsimpalts)

  1081   apply(simp add: flts_append)

  1082   by (metis Diff_empty distinct_once_enough flts_append nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality1)

  1083 

  1084 lemma basic_rsimp_SEQ_property1:

  1085   shows "rsimp_SEQ RONE r = r"

  1086   by (simp add: idiot)

  1087 

  1088 

  1089 

  1090 lemma basic_rsimp_SEQ_property3:

  1091   shows "rsimp_SEQ r RZERO = RZERO"  

  1092   using rsimp_SEQ.elims by blast

  1093 

  1094 

  1095 

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

  1097 "vsuf [] _ = []"

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

  1099                                       else  (vsuf cs (rder c r1))

  1100                    ) "

  1101 

  1102 

  1103 

  1104 

  1105 

  1106 

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

  1108 "star_update c r [] = []"

  1109 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) 

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

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

  1112 

  1113 

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

  1115   where

  1116 "star_updates [] r Ss = Ss"

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

  1118 

  1119 lemma stupdates_append: shows 

  1120 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"

  1121   apply(induct s arbitrary: Ss)

  1122    apply simp

  1123   apply simp

  1124   done

  1125 

  1126 lemma flts_removes0:

  1127   shows "  rflts (rs @ [RZERO])  =

  1128            rflts rs"

  1129   apply(induct rs)

  1130    apply simp

  1131   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)

  1132   

  1133 

  1134 lemma rflts_spills_last:

  1135   shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs"