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 

    13 abbreviation

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

    15 

    16 

    17 fun

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

    19 where

    20   "rnullable (RZERO) = False"

    21 | "rnullable (RONE) = True"

    22 | "rnullable (RCHAR c) = False"

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

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

    25 | "rnullable (RSTAR r) = True"

    26 

    27 

    28 fun

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

    30 where

    31   "rder c (RZERO) = RZERO"

    32 | "rder c (RONE) = RZERO"

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

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

    35 | "rder c (RSEQ r1 r2) = 

    36      (if rnullable r1

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

    38       else RSEQ   (rder c r1) r2)"

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

    40 

    41 

    42 fun 

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

    44 where

    45   "rders r [] = r"

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

    47 

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

    49   where

    50   "rdistinct [] acc = []"

    51 | "rdistinct (x#xs)  acc = 

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

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

    54 

    55 lemma rdistinct1:

    56   assumes "a \<in> acc"

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

    58   using assms

    59   apply(induct rs arbitrary: acc a)

    60    apply(auto)

    61   done

    62 

    63 

    64 lemma rdistinct_does_the_job:

    65   shows "distinct (rdistinct rs s)"

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

    67   apply(auto simp add: rdistinct1)

    68   done

    69 

    70 

    71 

    72 lemma rdistinct_concat:

    73   assumes "set rs \<subseteq> rset"

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

    75   using assms

    76   apply(induct rs)

    77   apply simp+

    78   done

    79 

    80 lemma distinct_not_exist:

    81   assumes "a \<notin> set rs"

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

    83   using assms

    84   apply(induct rs arbitrary: rset)

    85   apply(auto)

    86   done

    87 

    88 lemma rdistinct_on_distinct:

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

    90   apply(induct rs)

    91   apply simp

    92   using distinct_not_exist by fastforce

    93 

    94 lemma distinct_rdistinct_append:

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

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

    97   using assms

    98   apply(induct rs1 arbitrary: rsa acc)

    99    apply(auto)[1]

   100   apply(auto)[1]

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

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

   103   apply(simp)

   104   apply(drule meta_mp)

   105    apply(auto)[1]

   106   apply(simp)

   107   done

   108   

   109 

   110 lemma rdistinct_set_equality1:

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

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

   113   apply(auto)

   114   done

   115 

   116 

   117 lemma rdistinct_set_equality:

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

   119   by (simp add: rdistinct_set_equality1)

   120 

   121 

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

   123   where 

   124   "rflts [] = []"

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

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

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

   128 

   129 

   130 lemma rflts_def_idiot:

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

   132   apply(case_tac a)

   133   apply simp_all

   134   done

   135 

   136 lemma rflts_def_idiot2:

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

   138   apply(induct rs rule: rflts.induct)

   139   apply(auto)

   140   done

   141 

   142 lemma flts_append:

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

   144   apply(induct rs1)

   145    apply simp

   146   apply(case_tac a)

   147        apply simp+

   148   done

   149 

   150 

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

   152   where

   153   "rsimp_ALTs  [] = RZERO"

   154 | "rsimp_ALTs [r] =  r"

   155 | "rsimp_ALTs rs = RALTS rs"

   156 

   157 lemma rsimpalts_conscons:

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

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

   160 

   161 lemma rsimp_alts_equal:

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

   163   by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)

   164 

   165 

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

   167   where

   168   "rsimp_SEQ  RZERO _ = RZERO"

   169 | "rsimp_SEQ  _ RZERO = RZERO"

   170 | "rsimp_SEQ RONE r2 = r2"

   171 | "rsimp_SEQ r1 r2 = RSEQ r1 r2"

   172 

   173 

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

   175   where

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

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

   178 | "rsimp r = r"

   179 

   180 

   181 fun 

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

   183 where

   184   "rders_simp r [] = r"

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

   186 

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

   188   "rsize RZERO = 1"

   189 | "rsize (RONE) = 1" 

   190 | "rsize (RCHAR  c) = 1"

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

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

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

   194 

   195 abbreviation rsizes where

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

   197 

   198 

   199 lemma rder_rsimp_ALTs_commute:

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

   201   apply(induct rs)

   202    apply simp

   203   apply(case_tac rs)

   204    apply simp

   205   apply auto

   206   done

   207 

   208 

   209 lemma rsimp_aalts_smaller:

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

   211   apply(induct rs)

   212    apply simp

   213   apply simp

   214   apply(case_tac "rs = []")

   215    apply simp

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

   217    apply(erule exE)+

   218    apply simp

   219   apply simp

   220   by(meson neq_Nil_conv)

   221   

   222 

   223 

   224 

   225 

   226 lemma rSEQ_mono:

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

   228   apply auto

   229   apply(induct r1)

   230        apply auto

   231       apply(case_tac "r2")

   232        apply simp_all

   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   done

   242 

   243 lemma ralts_cap_mono:

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

   245   by simp

   246 

   247 

   248 

   249 

   250 lemma rflts_mono:

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

   252   apply(induct rs)

   253   apply simp

   254   apply(case_tac "a = RZERO")

   255    apply simp

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

   257   apply(erule exE)

   258    apply simp

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

   260    prefer 2

   261   

   262   using rflts_def_idiot apply blast

   263   apply simp

   264   done

   265 

   266 lemma rdistinct_smaller: 

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

   268   apply (induct rs arbitrary: ss)

   269    apply simp

   270   by (simp add: trans_le_add2)

   271 

   272 

   273 lemma rsimp_alts_mono :

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

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

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

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

   278   prefer 2

   279   using rsimp_aalts_smaller apply auto[1]

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

   281   prefer 2

   282   using ralts_cap_mono apply blast

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

   284   prefer 2

   285   using rdistinct_smaller apply presburger

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

   287   prefer 2

   288   using rflts_mono apply blast

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

   290   prefer 2

   291   

   292   apply (simp add: sum_list_mono)

   293   by linarith

   294 

   295 

   296 

   297 

   298 

   299 lemma rsimp_mono:

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

   301   apply(induct r)

   302   apply simp_all

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

   304     apply force

   305   using rSEQ_mono

   306    apply presburger

   307   using rsimp_alts_mono by auto

   308 

   309 lemma idiot:

   310   shows "rsimp_SEQ RONE r = r"

   311   apply(case_tac r)

   312        apply simp_all

   313   done

   314 

   315 

   316 

   317 

   318 

   319 lemma idiot2:

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

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

   322   apply(case_tac r1)

   323        apply(case_tac r2)

   324   apply simp_all

   325      apply(case_tac r2)

   326   apply simp_all

   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   done

   334 

   335 lemma rders__onechar:

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

   337   by simp

   338 

   339 lemma rders_append:

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

   341   apply(induct s1 arbitrary: c s2)

   342   apply(simp_all)

   343   done

   344 

   345 lemma rders_simp_append:

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

   347   apply(induct s1 arbitrary: c s2)

   348    apply(simp_all)

   349   done

   350 

   351 

   352 lemma rders_simp_one_char:

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

   354   apply auto

   355   done

   356 

   357 

   358 

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

   360   where

   361   "nonalt (RALTS  rs) = False"

   362 | "nonalt r = True"

   363 

   364 

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

   366   "good RZERO = False"

   367 | "good (RONE) = True" 

   368 | "good (RCHAR c) = True"

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

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

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

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

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

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

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

   376 | "good (RSTAR r) = True"

   377 

   378 

   379 lemma  k0a:

   380   shows "rflts [RALTS rs] =   rs"

   381   apply(simp)

   382   done

   383 

   384 lemma bbbbs:

   385   assumes "good r" "r = RALTS rs"

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

   387   using  assms

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

   389 

   390 lemma bbbbs1:

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

   392   by (meson nonalt.elims(3))

   393 

   394 

   395 

   396 lemma good0:

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

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

   399   using  assms

   400   apply(induct  rs rule: rsimp_ALTs.induct)

   401   apply(auto)

   402   done

   403 

   404 lemma flts1:

   405   assumes "good r" 

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

   407   using  assms

   408   apply(induct r)

   409        apply(simp_all)

   410   using good.simps(4) by blast

   411 

   412 lemma flts2:

   413   assumes "good r" 

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

   415   using  assms

   416   apply(induct r)

   417        apply(simp)

   418       apply(simp)

   419      apply(simp)

   420     prefer 2

   421     apply(simp)

   422     apply(auto)[1]

   423   

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

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

   426    apply fastforce

   427   apply(simp)

   428   done  

   429 

   430 

   431 

   432 lemma flts3:

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

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

   435   using  assms

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

   437         apply(simp_all)

   438   by (metis UnE flts2 k0a)

   439 

   440 

   441 lemma  k0:

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

   443   apply(induct r arbitrary: rs1)

   444    apply(auto)

   445   done

   446 

   447 

   448 lemma good_SEQ:

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

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

   451   using assms

   452   apply(case_tac r1)

   453        apply(simp_all)

   454   apply(case_tac r2)

   455           apply(simp_all)

   456   apply(case_tac r2)

   457          apply(simp_all)

   458   apply(case_tac r2)

   459         apply(simp_all)

   460   apply(case_tac r2)

   461        apply(simp_all)

   462   done

   463 

   464 lemma rsize0:

   465   shows "0 < rsize r"

   466   apply(induct  r)

   467        apply(auto)

   468   done

   469 

   470 

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

   472   where

   473   "nonnested (RALTS []) = True"

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

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

   476 | "nonnested r = True"

   477 

   478 

   479 

   480 lemma  k00:

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

   482   apply(induct rs1 arbitrary: rs2)

   483    apply(auto)

   484   by (metis append.assoc k0)

   485 

   486 

   487 

   488 

   489 lemma k0b:

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

   491   shows "rflts [r] = [r]"

   492   using assms

   493   apply(case_tac  r)

   494   apply(simp_all)

   495   done

   496 

   497 lemma nn1qq:

   498   assumes "nonnested (RALTS rs)"

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

   500   using assms

   501   apply(induct rs rule: rflts.induct)

   502   apply(auto)

   503   done

   504 

   505  

   506 

   507 lemma n0:

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

   509   apply(induct rs )

   510    apply(auto)

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

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

   513   using bbbbs1 apply fastforce

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

   515 

   516   

   517   

   518 

   519 lemma nn1c:

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

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

   522   using assms

   523   apply(induct rs rule: rflts.induct)

   524         apply(auto)

   525   using n0 by blast

   526 

   527 lemma nn1bb:

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

   529   shows "nonnested (rsimp_ALTs  rs)"

   530   using assms

   531   apply(induct  rs rule: rsimp_ALTs.induct)

   532     apply(auto)

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

   534   using n0 by auto

   535 

   536 lemma bsimp_ASEQ0:

   537   shows "rsimp_SEQ  r1 RZERO = RZERO"

   538   apply(induct r1)

   539   apply(auto)

   540   done

   541 

   542 lemma nn1b:

   543   shows "nonnested (rsimp r)"

   544   apply(induct r)

   545        apply(simp_all)

   546   apply(case_tac "rsimp r1 = RZERO")

   547     apply(simp)

   548  apply(case_tac "rsimp r2 = RZERO")

   549    apply(simp)

   550     apply(subst bsimp_ASEQ0)

   551   apply(simp)

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

   553     apply(auto)[1]

   554   using idiot apply fastforce

   555   using idiot2 nonnested.simps(11) apply presburger

   556   by (metis (mono_tags, lifting) Diff_empty image_iff list.set_map nn1bb nn1c rdistinct_set_equality1)

   557 

   558 lemma nonalt_flts_rd:

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

   560        \<Longrightarrow> nonalt xa"

   561   by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1)

   562 

   563 

   564 lemma rsimpalts_implies1:

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

   566   using rsimp_ALTs.elims by auto

   567 

   568 

   569 lemma rsimpalts_implies2:

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

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

   572 

   573 lemma rsimpalts_implies21:

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

   575   using rsimpalts_implies2 by blast

   576 

   577 

   578 lemma bsimp_ASEQ2:

   579   shows "rsimp_SEQ RONE r2 =  r2"

   580   apply(induct r2)

   581   apply(auto)

   582   done

   583 

   584 lemma elem_smaller_than_set:

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

   586   apply(induct list)

   587    apply simp

   588   by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)

   589 

   590 lemma rsimp_list_mono:

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

   592   apply(induct rs)

   593    apply simp+

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

   595 

   596 

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

   598 lemma good2_obv_simplified:

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

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

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

   602   prefer 2

   603    apply (simp add: elem_smaller_than_set)

   604   by (metis Diff_empty flts3 rdistinct_set_equality1)

   605 

   606   

   607 lemma good1:

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

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

   610   apply(case_tac x)

   611   apply(simp)

   612   apply(simp)

   613   apply(simp)

   614   prefer 3

   615     apply(simp)

   616    prefer 2

   617    apply(simp only:)

   618    apply simp

   619   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)

   620   apply simp

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

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

   623     apply(case_tac "rsimp x41 = RZERO")

   624      apply simp

   625     apply(case_tac "rsimp x42 = RZERO")

   626      apply simp

   627   using bsimp_ASEQ0 apply blast

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

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

   630       apply simp

   631   apply (metis bsimp_ASEQ2 good_SEQ idiot2)

   632   apply blast

   633   apply fastforce

   634   using less_add_Suc2 apply blast  

   635   using less_iff_Suc_add by blast

   636 

   637 

   638 

   639 fun

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

   641 where

   642   "RL (RZERO) = {}"

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

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

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

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

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

   648 

   649 

   650 lemma RL_rnullable:

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

   652   apply(induct r)

   653   apply(auto simp add: Sequ_def)

   654   done

   655 

   656 lemma RL_rder:

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

   658   apply(induct r)

   659   apply(auto simp add: Sequ_def Der_def)

   660         apply (metis append_Cons)

   661   using RL_rnullable apply blast

   662   apply (metis append_eq_Cons_conv)

   663   apply (metis append_Cons)

   664   apply (metis RL_rnullable append_eq_Cons_conv)

   665   apply (metis Star.step append_Cons)

   666   using Star_decomp by auto

   667 

   668 

   669 

   670 

   671 lemma RL_rsimp_RSEQ:

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

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

   674   apply(simp_all)

   675   done

   676 

   677 lemma RL_rsimp_RALTS:

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

   679   apply(induct rs rule: rsimp_ALTs.induct)

   680   apply(simp_all)

   681   done

   682 

   683 lemma RL_rsimp_rdistinct:

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

   685   apply(auto)

   686   apply (metis Diff_iff rdistinct_set_equality1)

   687   by (metis Diff_empty rdistinct_set_equality1)

   688 

   689 lemma RL_rsimp_rflts:

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

   691   apply(induct rs rule: rflts.induct)

   692   apply(simp_all)

   693   done

   694 

   695 lemma RL_rsimp:

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

   697   apply(induct r rule: rsimp.induct)

   698        apply(auto simp add: Sequ_def RL_rsimp_RSEQ)

   699   using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1]

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

   701 

   702   

   703 lemma qqq1:

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

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

   706 

   707 

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

   709   where

   710   "nonazero RZERO = False"

   711 | "nonazero r = True"

   712 

   713 

   714 lemma flts_single1:

   715   assumes "nonalt r" "nonazero r"

   716   shows "rflts [r] = [r]"

   717   using assms

   718   apply(induct r)

   719   apply(auto)

   720   done

   721 

   722 lemma nonalt0_flts_keeps:

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

   724   apply(case_tac a)

   725        apply simp+

   726   done

   727 

   728 

   729 lemma nonalt0_fltseq:

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

   731   apply(induct rs)

   732    apply simp

   733   apply(case_tac "a = RZERO")

   734    apply fastforce

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

   736    apply(erule exE)

   737    apply simp+

   738   using nonalt0_flts_keeps by presburger

   739 

   740   

   741 

   742 

   743 lemma goodalts_nonalt:

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

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

   746     apply simp

   747   

   748   using good.simps(5) apply blast

   749   apply simp

   750   apply(case_tac "r1 = RZERO")

   751   using good.simps(1) apply force

   752   apply(case_tac "r2 = RZERO")

   753   using good.simps(1) apply force

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

   755   prefer 2

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

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

   758    apply(subgoal_tac "rflts rs = rs")

   759     apply presburger

   760   using nonalt0_fltseq apply presburger

   761   using good.simps(1) by blast

   762   

   763 

   764   

   765 

   766 

   767 lemma test:

   768   assumes "good r"

   769   shows "rsimp r = r"

   770 

   771   using assms

   772   apply(induct rule: good.induct)

   773                       apply simp

   774                       apply simp

   775                       apply simp

   776                       apply simp

   777                       apply simp

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

   779   prefer 2

   780   using good.simps(6) apply blast

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

   782   prefer 2

   783   using goodalts_nonalt apply blast

   784 

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

   786   prefer 2

   787                       apply (meson distinct_length_2_or_more)

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

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

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

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

   792   apply simp             

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

   794   apply (metis distinct_not_exist rdistinct_on_distinct)

   795   

   796                       apply blast

   797                       apply (meson map_idI)

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

   799 

   800   apply (meson distinct.simps(2))

   801                       apply (simp add: distinct_length_2_or_more)

   802                       apply simp+

   803   done

   804 

   805 

   806 

   807 lemma rsimp_idem:

   808   shows "rsimp (rsimp r) = rsimp r"

   809   using test good1

   810   by force

   811 

   812 corollary rsimp_inner_idem4:

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

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

   815 

   816 

   817 lemma head_one_more_simp:

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

   819   by (simp add: rsimp_idem)

   820 

   821 

   822 lemma der_simp_nullability:

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

   824   using RL_rnullable RL_rsimp by auto

   825   

   826 

   827 lemma no_alt_short_list_after_simp:

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

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

   830 

   831 

   832 lemma no_further_dB_after_simp:

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

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

   835   apply(subgoal_tac "distinct rs")

   836   using rdistinct_on_distinct apply blast

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

   838   using good1 by fastforce

   839 

   840 

   841 lemma idem_after_simp1:

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

   843   apply(case_tac "rsimp aa")

   844   apply simp+

   845   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)

   846   by simp

   847 

   848 lemma identity_wwo0:

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

   850   by (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))

   851 

   852 

   853 lemma distinct_removes_last:

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

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

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

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

   858      apply simp

   859     apply simp

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

   861    apply(case_tac "a = aa")

   862   apply (metis append_Cons)

   863     apply simp

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

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

   866    apply(case_tac "a = aa")

   867     prefer 2

   868     apply simp

   869    apply (metis append_Cons)

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

   871   prefer 2

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

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

   874   prefer 2

   875   apply force

   876   apply(simp only:)

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

   878     apply(simp only:)

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

   880      apply blast

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

   882      apply simp

   883      apply (metis insertI1)

   884     apply simp

   885     apply (meson insertI1)

   886    apply simp

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

   888    apply simp

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

   890 

   891 

   892 lemma distinct_removes_middle:

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

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

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

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

   897      apply simp

   898     apply simp

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

   900     apply simp

   901     apply metis

   902    apply simp

   903    apply (metis insertI1)

   904   apply(case_tac "a = ab")

   905    apply simp

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

   907     apply simp

   908     apply presburger

   909    apply (meson insertI1)

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

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

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

   913   apply simp

   914    apply (meson insert_iff)

   915   apply simp

   916   by (metis insertI1)

   917 

   918 

   919 lemma distinct_removes_middle3:

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

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

   922   using distinct_removes_middle(1) by fastforce

   923 

   924 

   925 lemma distinct_removes_list:

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

   927   apply(induct rs)

   928    apply simp+

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

   930    prefer 2

   931   apply (metis append_Cons append_Nil distinct_removes_middle(1))

   932   by presburger

   933 

   934 

   935 lemma spawn_simp_rsimpalts:

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

   937   apply(cases rs)

   938    apply simp

   939   apply(case_tac list)

   940    apply simp

   941    apply(subst rsimp_idem[symmetric])

   942    apply simp

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

   944    apply(simp only:)

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

   946     apply(simp only:)

   947   prefer 2

   948   apply simp

   949    prefer 2

   950   using rsimp_ALTs.simps(3) apply presburger

   951   apply auto

   952   apply(subst rsimp_idem)+

   953   by (metis comp_apply rsimp_idem)

   954 

   955 

   956 lemma simp_singlealt_flatten:

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

   958   apply(induct rsa)

   959    apply simp

   960   apply simp

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

   962 

   963 

   964 lemma good1_rsimpalts:

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

   966   by (metis no_alt_short_list_after_simp) 

   967   

   968 

   969 

   970 

   971 lemma good1_flatten:

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

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

   974   apply(subst good1_rsimpalts)

   975    apply simp+

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

   977    apply simp

   978   using flts_append rsimp_inner_idem4 by presburger

   979 

   980   

   981 lemma flatten_rsimpalts:

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

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

   984   apply(case_tac "map rsimp rsa")

   985    apply simp

   986   apply(case_tac "list")

   987    apply simp

   988    apply(case_tac a)

   989         apply simp+

   990     apply(rename_tac rs1)

   991     apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)

   992   

   993   apply simp

   994   

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

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

   997     apply simp

   998    apply(case_tac "listb")

   999     apply simp+

  1000   apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))

  1001   by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)

  1002 

  1003 

  1004 lemma last_elem_out:

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

  1006   apply(induct xs arbitrary: rset)

  1007   apply simp+

  1008   done

  1009 

  1010 

  1011 

  1012 

  1013 lemma rdistinct_concat_general:

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

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

  1016    apply simp

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

  1018   apply simp

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

  1020    apply simp

  1021   

  1022    apply (simp add: distinct_removes_middle3 insert_absorb)

  1023   apply simp

  1024   by (simp add: last_elem_out)

  1025 

  1026 

  1027   

  1028 

  1029 lemma distinct_once_enough:

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

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

  1032    apply(subgoal_tac 

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

  1034   apply(simp only:)

  1035   using rdistinct_concat_general apply blast

  1036   apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)

  1037   by (simp add: rdistinct_does_the_job)

  1038   

  1039 

  1040 lemma simp_flatten:

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

  1042   apply simp

  1043   apply(subst flatten_rsimpalts)

  1044   apply(simp add: flts_append)

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

  1046 

  1047 lemma basic_rsimp_SEQ_property1:

  1048   shows "rsimp_SEQ RONE r = r"

  1049   by (simp add: idiot)

  1050 

  1051 

  1052 

  1053 lemma basic_rsimp_SEQ_property3:

  1054   shows "rsimp_SEQ r RZERO = RZERO"  

  1055   using rsimp_SEQ.elims by blast

  1056 

  1057 

  1058 

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

  1060 "vsuf [] _ = []"

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

  1062                                       else  (vsuf cs (rder c r1))

  1063                    ) "

  1064 

  1065 

  1066 

  1067 

  1068 

  1069 

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

  1071 "star_update c r [] = []"

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

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

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

  1075 

  1076 

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

  1078   where

  1079 "star_updates [] r Ss = Ss"

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

  1081 

  1082 lemma stupdates_append: shows 

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

  1084   apply(induct s arbitrary: Ss)

  1085    apply simp

  1086   apply simp

  1087   done

  1088 

  1089 lemma flts_removes0:

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

  1091            rflts rs"

  1092   apply(induct rs)

  1093    apply simp

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

  1095   

  1096 

  1097 lemma rflts_spills_last:

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

  1099   apply (induct rs1 rule: rflts.induct)

  1100   apply(auto)

  1101   done

  1102 

  1103 lemma flts_keeps1:

  1104   shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]"

  1105   apply (induct rs rule: rflts.induct)

  1106   apply(auto)

  1107   done

  1108 

  1109 lemma flts_keeps_others:

  1110   shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"

  1111   apply(induct rs rule: rflts.induct)

  1112   apply(auto)

  1113   by (meson k0b nonalt.elims(3))

  1114 

  1115 lemma spilled_alts_contained:

  1116   shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"

  1117   apply(induct rs1)

  1118    apply simp 

  1119   apply(case_tac "a = aa")

  1120    apply simp

  1121   apply(subgoal_tac " a \<in> set rs1")

  1122   prefer 2

  1123    apply (meson set_ConsD)

  1124   apply(case_tac aa)

  1125   using rflts.simps(2) apply presburger

  1126       apply fastforce

  1127   apply fastforce

  1128   apply fastforce

  1129   apply fastforce

  1130   by fastforce

  1131 

  1132 

  1133 lemma distinct_removes_duplicate_flts:

  1134   shows " a \<in> set rsa

  1135        \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =