109 

   110 lemma fuse_append:

   111   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"

   112   apply(induct r)

   113   apply(auto)

   114   done

   115 

   461 fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"

   462   where

   463   "distinctBy [] f acc = []"

   464 | "distinctBy (x#xs) f acc = 

   465      (if (f x) \<in> acc then distinctBy xs f acc 

   466       else x # (distinctBy xs f ({f x} \<union> acc)))"

   467 

   468 fun flts :: "arexp list \<Rightarrow> arexp list"

   469   where 

   470   "flts [] = []"

   471 | "flts (AZERO # rs) = flts rs"

   472 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"

   473 | "flts (r1 # rs) = r1 # flts rs"

   474 

   475 (*

   476 lemma flts_map:

   477   assumes "\<forall>r \<in> set rs. f r = r"

   478   shows "map f (flts rs) = flts (map f rs)"

   479   using assms

   480   apply(induct rs rule: flts.induct)

   481         apply(simp_all)

   482        apply(case_tac rs)

   483   apply(simp)

   484 *)

   485 

   486 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"

   487   where

   488   "bsimp_ASEQ _ AZERO _ = AZERO"

   489 | "bsimp_ASEQ _ _ AZERO = AZERO"

   490 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"

   491 | "bsimp_ASEQ bs1 r1 r2 = ASEQ  bs1 r1 r2"

   492 

   493 

   494 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"

   495   where

   496   "bsimp_AALTs _ [] = AZERO"

   497 | "bsimp_AALTs bs1 [r] = fuse bs1 r"

   498 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   499 

   500 

   501 fun bsimp :: "arexp \<Rightarrow> arexp" 

   502   where

   503   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"

   504 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"

   505 | "bsimp r = r"

   506 

   507 fun 

   508   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

   509 where

   510   "bders_simp r [] = r"

   511 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"

   512 

   513 definition blexer_simp where

   514  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 

   515                 decode (bmkeps (bders_simp (intern r) s)) r else None"

   516 

   517 

   518 lemma bders_simp_append:

   519   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"

   520   apply(induct s1 arbitrary: r s2)

   521    apply(simp)

   522   apply(simp)

   523   done

   524 

   525 

   526 lemma L_bsimp_ASEQ:

   527   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"

   528   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

   529   apply(simp_all)

   530   by (metis erase_fuse fuse.simps(4))

   531 

   532 lemma L_bsimp_AALTs:

   533   "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"

   534   apply(induct bs rs rule: bsimp_AALTs.induct)

   535   apply(simp_all add: erase_fuse)

   536   done

   537 

   538 lemma L_erase_AALTs:

   539   shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"

   540   apply(induct rs)

   541    apply(simp)

   542   apply(simp)

   543   apply(case_tac rs)

   544    apply(simp)

   545   apply(simp)

   546   done

   547 

   548 lemma L_erase_flts:

   549   shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"

   550   apply(induct rs rule: flts.induct)

   551         apply(simp_all)

   552   apply(auto)

   553   using L_erase_AALTs erase_fuse apply auto[1]

   554   by (simp add: L_erase_AALTs erase_fuse)

   555 

   556 

   557 lemma L_bsimp_erase:

   558   shows "L (erase r) = L (erase (bsimp r))"

   559   apply(induct r)

   560   apply(simp)

   561   apply(simp)

   562   apply(simp)

   563   apply(auto simp add: Sequ_def)[1]

   564   apply(subst L_bsimp_ASEQ[symmetric])

   565   apply(auto simp add: Sequ_def)[1]

   566   apply(subst (asm)  L_bsimp_ASEQ[symmetric])

   567   apply(auto simp add: Sequ_def)[1]

   568    apply(simp)

   569    apply(subst L_bsimp_AALTs[symmetric])

   570    defer

   571    apply(simp)

   572   apply(subst (2)L_erase_AALTs)

   573   apply(subst L_erase_flts)

   574   apply(auto)

   575    apply (simp add: L_erase_AALTs)

   576   using L_erase_AALTs by blast

   577 

   578 

   579 lemma bsimp_ASEQ1:

   580   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"

   581   shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"

   582   using assms

   583   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

   584   apply(auto)

   585   done

   586 

   587 lemma bsimp_ASEQ2:

   588   shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"

   589   apply(induct r2)

   590   apply(auto)

   591   done

   592 

   593 

   594 lemma L_bders_simp:

   595   shows "L (erase (bders_simp r s)) = L (erase (bders r s))"

   596   apply(induct s arbitrary: r rule: rev_induct)

   597    apply(simp)

   598   apply(simp)

   599   apply(simp add: ders_append)

   600   apply(simp add: bders_simp_append)

   601   apply(simp add: L_bsimp_erase[symmetric])

   602   by (simp add: der_correctness)

   603 

   604 lemma b1:

   605   "bsimp_ASEQ bs1 (AONE bs) r =  fuse (bs1 @ bs) r" 

   606   apply(induct r)

   607        apply(auto)

   608   done

   609 

   610 lemma b2:

   611   assumes "bnullable r"

   612   shows "bmkeps (fuse bs r) = bs @ bmkeps r"

   613   by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)

   614 

   615 lemma b3:

   616   shows "bnullable r = bnullable (bsimp r)"

   617   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

   618 

   619 

   620 lemma b4:

   621   shows "bnullable (bders_simp r s) = bnullable (bders r s)"

   622   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))

   623   

   624 

   625 lemma q1:

   626   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"

   627   shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"

   628   using assms

   629   apply(induct rs)

   630   apply(simp)

   631   apply(simp)

   632   done

   633 

   634 lemma q3:

   635   assumes "\<exists>r \<in> set rs. bnullable r"

   636   shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"

   637   using assms

   638   apply(induct bs rs rule: bsimp_AALTs.induct)

   639     apply(simp)

   640    apply(simp)

   641   apply (simp add: b2)

   642   apply(simp)

   643   done

   644 

   645 lemma qq1:

   646   assumes "\<exists>r \<in> set rs. bnullable r"

   647   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"

   648   using assms

   649   apply(induct rs arbitrary: rs1 bs)

   650   apply(simp)

   651   apply(simp)

   652   by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)

   653 

   654 lemma qq2:

   655   assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"

   656   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"

   657   using assms

   658   apply(induct rs arbitrary: rs1 bs)

   659   apply(simp)

   660   apply(simp)

   661   by (metis append_assoc in_set_conv_decomp r1 r2)

   662   

   663 lemma qq3:

   664   shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"

   665   apply(induct rs arbitrary: bs)

   666   apply(simp)

   667   apply(simp)

   668   done

   669 

   670 lemma q3a:

   671   assumes "\<exists>r \<in> set rs. bnullable r"

   672   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"

   673   using assms

   674   apply(induct rs arbitrary: bs bs1)

   675    apply(simp)

   676   apply(simp)

   677   apply(auto)

   678    apply (metis append_assoc b2 bnullable_correctness erase_fuse r0)

   679   apply(case_tac "bnullable a")

   680    apply (metis append.assoc b2 bnullable_correctness erase_fuse r0)

   681   apply(case_tac rs)

   682   apply(simp)

   683   apply(simp)

   684   apply(auto)[1]

   685    apply (metis bnullable_correctness erase_fuse)+

   686   done

   687 

   688 lemma qq4:

   689   assumes "\<exists>x\<in>set list. bnullable x"

   690   shows "\<exists>x\<in>set (flts list). bnullable x"

   691   using assms

   692   apply(induct list rule: flts.induct)

   693         apply(auto)

   694   by (metis UnCI bnullable_correctness erase_fuse imageI)

   695   

   696 

   697 lemma qs3:

   698   assumes "\<exists>r \<in> set rs. bnullable r"

   699   shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"

   700   using assms

   701   apply(induct rs arbitrary: bs taking: size rule: measure_induct)

   702   apply(case_tac x)

   703   apply(simp)

   704   apply(simp)

   705   apply(case_tac a)

   706        apply(simp)

   707        apply (simp add: r1)

   708       apply(simp)

   709       apply (simp add: r0)

   710      apply(simp)

   711      apply(case_tac "flts list")

   712       apply(simp)

   713   apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)

   714      apply(simp)

   715      apply (simp add: r1)

   716     prefer 3

   717     apply(simp)

   718     apply (simp add: r0)

   719    prefer 2

   720    apply(simp)

   721   apply(case_tac "\<exists>x\<in>set x52. bnullable x")

   722   apply(case_tac "list")

   723     apply(simp)

   724     apply (metis b2 fuse.simps(4) q3a r2)

   725    apply(erule disjE)

   726     apply(subst qq1)

   727      apply(auto)[1]

   728      apply (metis bnullable_correctness erase_fuse)

   729     apply(simp)

   730      apply (metis b2 fuse.simps(4) q3a r2)

   731     apply(simp)

   732     apply(auto)[1]

   733      apply(subst qq1)

   734       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

   735      apply (metis b2 fuse.simps(4) q3a r2)

   736   apply(subst qq1)

   737       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

   738     apply (metis b2 fuse.simps(4) q3a r2)

   739    apply(simp)

   740    apply(subst qq2)

   741      apply (metis bnullable_correctness erase_fuse imageE set_map)

   742   prefer 2

   743   apply(case_tac "list")

   744      apply(simp)

   745     apply(simp)

   746    apply (simp add: qq4)

   747   apply(simp)

   748   apply(auto)

   749    apply(case_tac list)

   750     apply(simp)

   751    apply(simp)

   752    apply (simp add: r0)

   753   apply(case_tac "bnullable (ASEQ x41 x42 x43)")

   754    apply(case_tac list)

   755     apply(simp)

   756    apply(simp)

   757    apply (simp add: r0)

   758   apply(simp)

   759   using qq4 r1 r2 by auto

   760 

   761 lemma  k0:

   762   shows "flts (r # rs1) = flts [r] @ flts rs1"

   763   apply(induct r arbitrary: rs1)

   764    apply(auto)

   765   done

   766 

   767 lemma k1:

   768   assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"

   769           "\<exists>x\<in>set x2a. bnullable x"

   770         shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"

   771   using assms

   772   apply(induct x2a)

   773   apply fastforce

   774   apply(simp)

   775   apply(subst k0)

   776   apply(subst (2) k0)

   777   apply(auto)[1]

   778   apply (metis b3 k0 list.set_intros(1) qs3 r0)

   779   by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map)

   780   

   781   

   782   

   783 lemma bmkeps_simp:

   784   assumes "bnullable r"

   785   shows "bmkeps r = bmkeps (bsimp r)"

   786   using  assms

   787   apply(induct r)

   788        apply(simp)

   789       apply(simp)

   790      apply(simp)

   791     apply(simp)

   792     prefer 3

   793   apply(simp)

   794    apply(case_tac "bsimp r1 = AZERO")

   795     apply(simp)

   796     apply(auto)[1]

   797   apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)

   798  apply(case_tac "bsimp r2 = AZERO")

   799     apply(simp)  

   800     apply(auto)[1]

   801   apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)

   802   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")

   803     apply(auto)[1]

   804     apply(subst b1)

   805     apply(subst b2)

   806   apply(simp add: b3[symmetric])

   807     apply(simp)

   808    apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)")

   809     prefer 2

   810   apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))

   811    apply(simp)

   812   apply(simp)

   813   apply(subst q3[symmetric])

   814    apply simp

   815   using b3 qq4 apply auto[1]

   816   apply(subst qs3)

   817    apply simp

   818   using k1 by blast

   819 

   820 thm bmkeps_retrieve bmkeps_simp bder_retrieve

   821 

   822 lemma bmkeps_bder_AALTs:

   823   assumes "\<exists>r \<in> set rs. bnullable (bder c r)" 

   824   shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))"

   825   using assms

   826   apply(induct rs)

   827    apply(simp)

   828   apply(simp)

   829   apply(auto)

   830   apply(case_tac rs)

   831     apply(simp)

   832   apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2)

   833    apply(simp)

   834   apply(case_tac  rs)

   835    apply(simp_all)

   836   done

   837 

   838 

   839 

   840 

   841 lemma MAIN_decode:

   842   assumes "\<Turnstile> v : ders s r"

   843   shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"

   844   using assms

   845 proof (induct s arbitrary: v rule: rev_induct)

   846   case Nil

   847   have "\<Turnstile> v : ders [] r" by fact

   848   then have "\<Turnstile> v : r" by simp

   849   then have "Some v = decode (retrieve (intern r) v) r"

   850     using decode_code retrieve_code by auto

   851   then show "Some (flex r id [] v) = decode (retrieve (bders_simp (intern r) []) v) r"

   852     by simp

   853 next

   854   case (snoc c s v)

   855   have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 

   856      Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r" by fact

   857   have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact

   858   then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 

   859     by(simp add: Prf_injval ders_append)

   860   have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"

   861     by (simp add: flex_append)

   862   also have "... = decode (retrieve (bders_simp (intern r) s) (injval (ders s r) c v)) r"

   863     using asm2 IH by simp

   864   also have "... = decode (retrieve (bder c (bders_simp (intern r) s)) v) r"

   865     using asm bder_retrieve ders_append 

   866     apply -

   867     apply(drule_tac x="v" in meta_spec)

   868     apply(drule_tac x="c" in meta_spec)

   869     apply(drule_tac x="bders_simp (intern r) s" in meta_spec)

   870     apply(drule_tac  meta_mp)

   871      apply(simp add: ders_append)

   872      defer

   873     apply(simp)

   874     oops

   875 

   876 function (sequential) bretrieve :: "arexp \<Rightarrow> bit list \<Rightarrow> (bit list) * (bit list)" where

   877   "bretrieve (AZERO) bs1 = ([], bs1)"

   878 | "bretrieve (AONE bs) bs1 = (bs, bs1)"

   879 | "bretrieve (ACHAR bs c) bs1 = (bs, bs1)"

   880 | "bretrieve (AALTs bs rs) [] = (bs, [])"

   881 | "bretrieve (AALTs bs [r]) bs1 = 

   882      (let (bs2, bs3) = bretrieve r bs1 in (bs @ bs2, bs3))"

   883 | "bretrieve (AALTs bs (r#rs)) (Z#bs1) = 

   884      (let (bs2, bs3) = bretrieve r bs1 in (bs @ [Z] @ bs2, bs3))"

   885 | "bretrieve (AALTs bs (r#rs)) (S#bs1) = 

   886      (let (bs2, bs3) = bretrieve (AALTs [] rs) bs1 in (bs @ [S] @ bs2, bs3))"

   887 | "bretrieve (ASEQ bs r1 r2) bs1 = 

   888      (let (bs2, bs3) = bretrieve r1 bs1 in 

   889       let (bs4, bs5) = bretrieve r2 bs3 in (bs @ bs2 @ bs4, bs5))"

   890 | "bretrieve (ASTAR bs r) [] = (bs, [])"

   891 | "bretrieve (ASTAR bs r) (S#bs1) = (bs @ [S], bs1)"

   892 | "bretrieve (ASTAR bs r) (Z#bs1) = 

   893      (let (bs2, bs3) = bretrieve r bs1 in 

   894       let (bs4, bs5) = bretrieve (ASTAR [] r) bs3 in (bs @ bs2 @ [Z] @ bs4, bs5))"

   895   by (pat_completeness) (auto)

   896 

   897 termination

   898   sorry

   899 

   900 thm Prf.intros

   901 

   902 

   903 lemma retrieve_XXX:

   904   assumes "\<Turnstile> v : erase r" 

   905   shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r)  \<and> retrieve (bsimp r) v' = retrieve r v"

   906   using assms

   907   apply(induct r arbitrary: v)

   908        apply(simp)

   909   using Prf_elims(1) apply blast

   910       apply(simp)

   911   using Prf_elims(4) apply fastforce

   912     apply(simp)

   913   apply blast

   914   apply simp

   915    apply(case_tac  "r1 = AZERO")

   916      apply(simp)

   917   apply (meson Prf_elims(1) Prf_elims(2))

   918   apply(case_tac  "r2 = AZERO")

   919      apply(simp)

   920      apply (meson Prf_elims(1) Prf_elims(2))

   921   apply(erule Prf_elims)

   922   apply(simp)

   923    apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")

   924      apply(clarify)

   925      apply(simp)

   926     apply(subst bsimp_ASEQ2)

   927      defer

   928      apply(subst bsimp_ASEQ1)

   929   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce

   930   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce

   931       apply(simp)

   932     apply(simp)

   933   apply(drule_tac  x="v1" in meta_spec)

   934   apply(drule_tac  x="v2" in meta_spec)

   935      apply(simp)

   936   apply(clarify)

   937      apply(rule_tac x="Seq v' v'a" in exI)

   938      apply(simp)

   939   apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))

   940     prefer 3

   941   apply(drule_tac  x="v1" in meta_spec)

   942   apply(drule_tac  x="v2" in meta_spec)

   943      apply(simp)

   944     apply(clarify)

   945     apply(rule_tac x="v'a" in exI)

   946     apply(subst bsimp_ASEQ2)

   947     apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)

   948    prefer 2  

   949    apply(auto)

   950   apply(case_tac "x2a")

   951    apply(simp)

   952   using Prf_elims(1) apply blast

   953   apply(simp)

   954   apply(case_tac "list")

   955    apply(simp)

   956   sorry

   957 

   958 

   959 lemma TEST:

   960   assumes "\<Turnstile> v : ders s r"

   961   shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v"

   962   using assms

   963   apply(induct s arbitrary: r v rule: rev_induct)

   964    apply(simp)

   965    defer

   966    apply(simp add: ders_append)

   967    apply(frule Prf_injval)

   968   apply(drule_tac x="r" in meta_spec)

   969    apply(drule_tac x="injval (ders xs r) x v" in meta_spec)

   970    apply(simp)

   971    apply(simp add: bders_append)

   972    apply(subst bder_retrieve)

   973     apply(simp)

   974    apply(simp)

   975   thm bder_retrieve

   976   thm bmkeps_retrieve

   977 

   978 

   979 lemma bmkeps_simp2:

   980   assumes "bnullable (bder c r)"

   981   shows "bmkeps (bder c (bsimp r)) = bmkeps (bder c r)"

   982   using  assms

   983   apply(induct r)

   984        apply(simp)

   985       apply(simp)

   986      apply(simp)

   987   prefer 3

   988     apply(simp)

   989    apply(simp)

   990    apply(auto)[1]

   991      prefer 2

   992      apply(case_tac "r1 = AZERO")

   993       apply(simp)

   994    apply(case_tac "r2 = AZERO")

   995       apply(simp)

   996      apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")

   997       apply(clarify)

   998       apply(simp)

   999       apply(subst bsimp_ASEQ2)

  1000   

  1001    apply(simp add: bmkeps_simp)

  1002   apply(simp add: bders_append)

  1003   apply(drule_tac x="bder a r" in meta_spec)

  1004        apply(simp)

  1005       apply(simp)

  1006      apply(simp)

  1007     prefer 3

  1008     apply(simp)

  1009    prefer 2

  1010    apply(simp)

  1011    apply(case_tac x2a)

  1012     apply(simp)

  1013   apply(simp add: )

  1014   apply(subst k0)

  1015    apply(auto)[1]

  1016     apply(case_tac list)

  1017      apply(simp)

  1018   

  1019 

  1020    apply(case_tac  "r1=AZERO")

  1021     apply(simp)

  1022    apply(case_tac  "r2=AZERO")

  1023     apply(simp)

  1024     apply(auto)[1]

  1025    apply(case_tac  "\<exists>bs. r1=AONE bs")

  1026   apply(simp)

  1027     apply(auto)[1]

  1028      apply(subst bsimp_ASEQ2)

  1029 

  1030   

  1031    prefer 2

  1032    apply(simp)

  1033   apply(subst  bmkeps_bder_AALTs)

  1034    apply(case_tac x2a)

  1035     apply(simp)

  1036    apply(simp)

  1037    apply(auto)[1]

  1038     apply(subst  bmkeps_bder_AALTs)

  1039   

  1040    apply(case_tac a)

  1041   apply(simp_all)

  1042    apply(auto)[1]

  1043     apply(case_tac list)

  1044          apply(simp)

  1045         apply(simp)

  1046   

  1047      prefer 2

  1048   apply(simp)

  1049 

  1050 

  1051 lemma bbs0:

  1052   shows "blexer_simp r [] = blexer r []"

  1053   apply(simp add: blexer_def blexer_simp_def)

  1054   done

  1055 

  1056 lemma bbs1:

  1057   shows "blexer_simp r [c] = blexer r [c]"

  1058   apply(simp add: blexer_def blexer_simp_def)

  1059   apply(auto)

  1060     defer

  1061   using b3 apply auto[1]

  1062   using b3 apply auto[1]  

  1063   apply(subst bmkeps_simp[symmetric])

  1064    apply(simp)

  1065   apply(simp)

  1066   done

  1067   

  1068 lemma bbs1:

  1069   shows "blexer_simp r [c1, c2] = blexer r [c1, c2]"

  1070   apply(simp add: blexer_def blexer_simp_def)

  1071   apply(auto)

  1072     defer

  1073   apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))

  1074   apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))

  1075   apply(subst bmkeps_simp[symmetric])

  1076   using b3 apply auto[1]

  1077   apply(subst bmkeps_retrieve)

  1078   using b3 bnullable_correctness apply blast

  1079   apply(subst bder_retrieve)

  1080   using b3 bnullable_correctness mkeps_nullable apply fastforce

  1081   apply(subst bmkeps_retrieve)

  1082   using bnullable_correctness apply blast

  1083   apply(subst bder_retrieve)

  1084   using bnullable_correctness mkeps_nullable apply force

  1085   

  1086   using bder_retrieve bmkeps_simp bmkeps_retrieve

  1087 

  1088   

  1089 

  1090 lemma bsimp_retrieve_bder:

  1091   assumes "\<Turnstile> v : der c (erase r)"

  1092   shows "retrieve (bder c r) v = retrieve (bsimp (bder c r)) v"

  1093   thm bder_retrieve bmkeps_simp

  1094   apply(induct  r arbitrary: c v)

  1095        apply(simp)

  1096       apply(simp)

  1097      apply(simp)

  1098     apply(auto)[1]

  1099      apply(case_tac "bsimp (bder c r1) = AZERO")

  1100       apply(simp)

  1101   

  1102     prefer 3

  1103     apply(simp)

  1104   apply(auto elim!: Prf_elims)[1]

  1105     apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO")

  1106      apply(simp)

  1107      apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)

  1108     apply(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs")

  1109      apply(clarify)

  1110      apply(subgoal_tac "L (der c (erase r)) = {[]}")

  1111       prefer 2

  1112       apply (metis L.simps(2) L_bsimp_erase erase.simps(2) erase_bder erase_fuse)

  1113      apply(simp)

  1114   

  1115   

  1116   

  1117     apply(subst bsimp_ASEQ1)

  1118        apply(simp)

  1119       apply(simp)

  1120   apply(auto)[1]

  1121   

  1122      prefer 2

  1123   

  1124 

  1125 lemma oo:

  1126   shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"

  1127   apply(simp add: blexer_correctness)

  1128   done

  1129 

  1130 lemma oo2a:

  1131   assumes "\<forall>r. bmkeps (bders_simp r s) = bmkeps (bders r s)" "c # s \<in> L r"

  1132           "bnullable (bders_simp (bsimp (bder c (intern r))) s)"

  1133   shows "(case (blexer_simp (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer_simp r (c # s)"

  1134   using assms

  1135   apply(simp add: blexer_simp_def)

  1136   apply(auto  split: option.split)

  1137     apply (metis blexer_correctness blexer_def lexer.simps(2) lexer_correct_None option.simps(4))

  1138    prefer 2

  1139   apply (metis L_bders_simp L_bsimp_erase Posix1(1) Posix_mkeps bnullable_correctness ders_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None)

  1140   apply(subst bmkeps_retrieve)

  1141   using L_bders_simp bnullable_correctness nullable_correctness apply blast

  1142   

  1143   thm bder_retrieve

  1144   

  1145   

  1146   apply(subst bder_retrieve[symmetric])

  1147   

  1148   

  1149 

  1150   apply(drule_tac x="bsimp (bder c (intern r))" in  spec)

  1151   apply(drule sym)

  1152    apply(simp)

  1153    apply(subst blexer_simp_def)

  1154   apply(case_tac "bnullable (bders_simp (intern (der c r)) s)")

  1155    apply(simp)

  1156   apply(auto split: option.split)

  1157   apply(subst oo)

  1158   apply(simp)

  1159   done

  1160 

  1161 

  1162 

  1163 lemma oo3:

  1164   assumes "\<forall>r. bders r s = bders_simp r s"

  1165   shows "blexer_simp r (s @ [c]) = blexer r (s @ [c])"

  1166   using assms

  1167   apply(simp (no_asm) add: blexer_simp_def)

  1168   apply(auto)

  1169    prefer 2

  1170   apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))

  1171   apply(simp add: bders_simp_append)

  1172   apply(subst bmkeps_simp[symmetric])

  1173   using b3 apply auto[1]

  1174   apply(simp add: blexer_def)

  1175   apply(auto)[1]

  1176    prefer 2

  1177   apply (metis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))

  1178   apply(simp add: bders_append)     

  1179   done

  1180 

  1181 lemma oo4:

  1182   assumes "\<forall>r. bmkeps (bders r s) = bmkeps (bders_simp r s)" "bnullable (bder c (bders r s))"

  1183   shows "bmkeps (bders_simp r (s @ [c])) = bmkeps (bders r (s @ [c]))"

  1184   using assms

  1185   apply(simp add: bders_simp_append)

  1186   apply(subst bmkeps_simp[symmetric])

  1187   apply (metis L_bders_simp bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))

  1188   apply(simp add: bders_append)

  1189   done

  1190 

  1191 lemma oo4:

  1192   shows "blexer_simp r s = blexer r s"

  1193   apply(induct s arbitrary: r rule: rev_induct)

  1194    apply(simp only: blexer_simp_def blexer_def)

  1195    apply(simp)

  1196   apply(simp only: blexer_simp_def blexer_def)

  1197   apply(subgoal_tac "bnullable (bders_simp (intern r) (xs @ [x])) = bnullable (bders (intern r) (xs @ [x]))")

  1198    prefer 2

  1199    apply (simp add: b4)

  1200   apply(simp)

  1201   apply(rule impI)

  1202   apply(simp add: bders_simp_append)

  1203   apply(subst bmkeps_simp[symmetric])

  1204   using b3 apply auto[1]

  1205   apply(subst bmkeps_retrieve)

  1206   using b3 bnullable_correctness apply blast

  1207   apply(subst bder_retrieve)

  1208   using b3 bnullable_correctness mkeps_nullable apply fastforce

  1209   apply(simp add: bders_append)

  1210   apply(subst bmkeps_retrieve)

  1211   using bnullable_correctness apply blast

  1212   apply(subst bder_retrieve)

  1213   using bnullable_correctness mkeps_nullable apply fastforce

  1214   apply(subst erase_bder)

  1215   apply(case_tac "xs \<in> L")

  1216   apply(subst (asm) (2) bmkeps_retrieve)

  1217   

  1218   

  1219   thm bmkeps_retrieve bmkeps_retrieve

  1220   apply(subst bmkeps_retrieve[symmetric])

  1221   

  1222    apply (simp add: bnullable_correctness)

  1223   apply(simp add: bders_simp_append)

  1224    

  1225   

  1226   apply(induct s arbitrary: r rule: rev_induct) 

  1227    apply(simp add: blexer_def blexer_simp_def)

  1228   apply(rule oo3)

  1229   apply(simp (no_asm) add: blexer_simp_def)

  1230   apply(auto)

  1231    prefer 2

  1232   apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))

  1233   apply(simp add: bders_simp_append)

  1234   apply(subst bmkeps_simp[symmetric])

  1235   using b3 apply auto[1]

  1236   apply(simp add: blexer_def)

  1237   apply(auto)[1]

  1238    prefer 2

  1239   apply (m etis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))

  1240   apply(simp add: bders_append)     

  1241   oops

  1242 

  1243 

  1244 lemma bnullable_simp:

  1245   assumes "s \<in> L (erase r)"

  1246   shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"

  1247   using assms

  1248   apply(induct s arbitrary: r rule: rev_induct)

  1249    apply(simp)

  1250   apply(simp add: bders_append bders_simp_append)

  1251   apply(subst bmkeps_simp[symmetric])

  1252   apply (metis L_bders_simp b3 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correct_Some lexer_correctness(1))

  1253   apply(subst bmkeps_retrieve)

  1254   apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer_correct_Some option.distinct(1))

  1255   apply(subst bmkeps_retrieve)

  1256   apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2))

  1257   apply(subst bder_retrieve)

  1258   apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer_correct_Some mkeps_nullable option.distinct(1))

  1259   apply(subst bder_retrieve)

  1260   apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2) mkeps_nullable)

  1261     

  1262   apply(drule_tac x="bder a r" in meta_spec)

  1263   apply(drule_tac  meta_mp)

  1264   apply (me tis erase_bder lexer.simps(2) lexer_correct_None option.simps(4))

  1265   apply(simp)

  1266   oops

  1267 

  1268 

  1269 lemma

  1270   shows "blexer r s = blexer_simp r s"

  1271   apply(induct s arbitrary: r rule: rev_induct)

  1272    apply(simp add: blexer_def blexer_simp_def)

  1273   apply(case_tac "xs @ [x] \<in> L r")

  1274    defer

  1275    apply(subgoal_tac "blexer (ders xs r) [x] = None")

  1276     prefer 2

  1277     apply(subst blexer_correctness)

  1278     apply(simp (no_asm) add: lexer_correct_None)

  1279     apply(simp add: nullable_correctness)

  1280     apply(simp add: der_correctness ders_correctness)

  1281   apply(simp add: Der_def Ders_def)

  1282 apply(subgoal_tac "blexer r (xs @ [x]) = None")

  1283     prefer 2

  1284     apply (simp add: blexer_correctness)

  1285   using lexer_correct_None apply auto[1]

  1286   apply(simp)

  1287    apply(subgoal_tac "blexer_simp (ders xs r) [x] = None")

  1288     prefer 2

  1289   apply (metis L_bders_simp Posix_injval Posix_mkeps bders.simps(2) blexer_correctness blexer_simp_def bnullable_correctness ders.simps(1) erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))

  1290    apply(subgoal_tac "[] \<notin> L (erase (bders_simp (intern r) (xs @ [x])))")

  1291   prefer 2

  1292   apply(metis L_bders_simp Posix_injval bders.simps(2) blexer_correctness ders.simps(1) ders_append erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))

  1293   using blexer_simp_def bnullable_correctness lexer_correct_None apply auto[1]

  1294 (* case xs @ [x] \<in> L r *)

  1295   apply(subgoal_tac "\<exists>v. blexer (ders xs r) [x] = Some v \<and> [x] \<in> (ders xs r) \<rightarrow> v")

  1296    prefer 2  

  1297   using blexer_correctness lexer_correct_Some apply auto[1]

  1298     apply (simp add: Posix_injval Posix_mkeps)

  1299   apply (metis ders.simps(1) ders.simps(2) ders_append lexer_correct_None lexer_flex)    

  1300   apply(clarify)

  1301   apply(subgoal_tac "blexer_simp (ders xs r) [x] = Some v")

  1302    prefer 2

  1303    apply(simp add: blexer_simp_def)

  1304    apply(auto)[1]

  1305     apply (metis bders.simps(1) bders.simps(2) blexer_def bmkeps_simp option.simps(3))

  1306   using b3 blexer_def apply fastforce

  1307   apply(subgoal_tac "blexer_simp (ders xs r) [x] = blexer_simp r (xs @ [x])")

  1308    prefer 2

  1309    apply(simp add: blexer_simp_def)

  1310   

  1311    apply(simp)

  1312   

  1313   

  1314   

  1315    apply(simp)

  1316   apply(subst blexer_simp_def)

  1317   apply(simp)

  1318   apply(auto)

  1319   apply(drule_tac x="der a r" in meta_spec)

  1320   apply(subst blexer_def)

  1321    apply(subgoal_tac "bnullable (bders (intern r) (a # s))")

  1322     prefer 2

  1323     apply (metis Posix_injval blexer_correctness blexer_def lexer_correctness(2))

  1324   apply(simp)

  1325   

  1326 

  1327 

  1328 lemma

  1329   shows "blexer r s = blexer_simp r s"

  1330   apply(induct s arbitrary: r)

  1331    apply(simp add: blexer_def blexer_simp_def)

  1332   apply(case_tac "s \<in> L (der a r)")

  1333    defer

  1334    apply(subgoal_tac "blexer (der a r) s = None")

  1335     prefer 2

  1336     apply (simp add: blexer_correctness lexer_correct_None)

  1337 apply(subgoal_tac "blexer r (a # s) = None")

  1338     prefer 2

  1339     apply (simp add: blexer_correctness)

  1340    apply(simp)

  1341   

  1342    apply(subst blexer_simp_def)

  1343    apply(simp)

  1344   apply(drule_tac  x="der a r" in  meta_spec)

  1345    apply(subgoal_tac "s \<notin> L(erase (bder a (intern  r)))")

  1346   prefer 2

  1347     apply simp

  1348    

  1349    apply(simp only:)

  1350    apply(subst blexer_simp_def)

  1351    apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))")

  1352     apply(simp)

  1353    apply(subst bnullable_correctness[symmetric])

  1354   apply(simp)

  1355   

  1356