diff -r 232aa2f19a75 -r ec5e4fe4cc70 thys2/BitCoded.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys2/BitCoded.thy Sun Oct 10 18:35:21 2021 +0100 @@ -0,0 +1,3369 @@ + +theory BitCodedCT + imports "Lexer" +begin + +section \Bit-Encodings\ + +datatype bit = Z | S + +fun + code :: "val \ bit list" +where + "code Void = []" +| "code (Char c) = []" +| "code (Left v) = Z # (code v)" +| "code (Right v) = S # (code v)" +| "code (Seq v1 v2) = (code v1) @ (code v2)" +| "code (Stars []) = [S]" +| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" + + +fun + Stars_add :: "val \ val \ val" +where + "Stars_add v (Stars vs) = Stars (v # vs)" + +function + decode' :: "bit list \ rexp \ (val * bit list)" +where + "decode' ds ZERO = (Void, [])" +| "decode' ds ONE = (Void, ds)" +| "decode' ds (CHAR d) = (Char d, ds)" +| "decode' [] (ALT r1 r2) = (Void, [])" +| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" +| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" +| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in + let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" +| "decode' [] (STAR r) = (Void, [])" +| "decode' (S # ds) (STAR r) = (Stars [], ds)" +| "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in + let (vs, ds'') = decode' ds' (STAR r) + in (Stars_add v vs, ds''))" +by pat_completeness auto + +lemma decode'_smaller: + assumes "decode'_dom (ds, r)" + shows "length (snd (decode' ds r)) \ length ds" +using assms +apply(induct ds r) +apply(auto simp add: decode'.psimps split: prod.split) +using dual_order.trans apply blast +by (meson dual_order.trans le_SucI) + +termination "decode'" +apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") +apply(auto dest!: decode'_smaller) +by (metis less_Suc_eq_le snd_conv) + +definition + decode :: "bit list \ rexp \ val option" +where + "decode ds r \ (let (v, ds') = decode' ds r + in (if ds' = [] then Some v else None))" + +lemma decode'_code_Stars: + assumes "\v\set vs. \ v : r \ (\x. decode' (code v @ x) r = (v, x)) \ flat v \ []" + shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" + using assms + apply(induct vs) + apply(auto) + done + +lemma decode'_code: + assumes "\ v : r" + shows "decode' ((code v) @ ds) r = (v, ds)" +using assms + apply(induct v r arbitrary: ds) + apply(auto) + using decode'_code_Stars by blast + +lemma decode_code: + assumes "\ v : r" + shows "decode (code v) r = Some v" + using assms unfolding decode_def + by (smt append_Nil2 decode'_code old.prod.case) + + +section {* Annotated Regular Expressions *} + +datatype arexp = + AZERO +| AONE "bit list" +| ACHAR "bit list" char +| ASEQ "bit list" arexp arexp +| AALTs "bit list" "arexp list" +| ASTAR "bit list" arexp + +abbreviation + "AALT bs r1 r2 \ AALTs bs [r1, r2]" + +fun asize :: "arexp \ nat" where + "asize AZERO = 1" +| "asize (AONE cs) = 1" +| "asize (ACHAR cs c) = 1" +| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))" +| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)" +| "asize (ASTAR cs r) = Suc (asize r)" + +fun + erase :: "arexp \ rexp" +where + "erase AZERO = ZERO" +| "erase (AONE _) = ONE" +| "erase (ACHAR _ c) = CHAR c" +| "erase (AALTs _ []) = ZERO" +| "erase (AALTs _ [r]) = (erase r)" +| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" +| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" +| "erase (ASTAR _ r) = STAR (erase r)" + +lemma decode_code_erase: + assumes "\ v : (erase a)" + shows "decode (code v) (erase a) = Some v" + using assms + by (simp add: decode_code) + + +fun nonalt :: "arexp \ bool" + where + "nonalt (AALTs bs2 rs) = False" +| "nonalt r = True" + + +fun good :: "arexp \ bool" where + "good AZERO = False" +| "good (AONE cs) = True" +| "good (ACHAR cs c) = True" +| "good (AALTs cs []) = False" +| "good (AALTs cs [r]) = False" +| "good (AALTs cs (r1#r2#rs)) = (\r' \ set (r1#r2#rs). good r' \ nonalt r')" +| "good (ASEQ _ AZERO _) = False" +| "good (ASEQ _ (AONE _) _) = False" +| "good (ASEQ _ _ AZERO) = False" +| "good (ASEQ cs r1 r2) = (good r1 \ good r2)" +| "good (ASTAR cs r) = True" + + + + +fun fuse :: "bit list \ arexp \ arexp" where + "fuse bs AZERO = AZERO" +| "fuse bs (AONE cs) = AONE (bs @ cs)" +| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" +| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs" +| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" +| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" + +lemma fuse_append: + shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)" + apply(induct r) + apply(auto) + done + + +fun intern :: "rexp \ arexp" where + "intern ZERO = AZERO" +| "intern ONE = AONE []" +| "intern (CHAR c) = ACHAR [] c" +| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) + (fuse [S] (intern r2))" +| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" +| "intern (STAR r) = ASTAR [] (intern r)" + + +fun retrieve :: "arexp \ val \ bit list" where + "retrieve (AONE bs) Void = bs" +| "retrieve (ACHAR bs c) (Char d) = bs" +| "retrieve (AALTs bs [r]) v = bs @ retrieve r v" +| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" +| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" +| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" +| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" +| "retrieve (ASTAR bs r) (Stars (v#vs)) = + bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" + + + +fun + bnullable :: "arexp \ bool" +where + "bnullable (AZERO) = False" +| "bnullable (AONE bs) = True" +| "bnullable (ACHAR bs c) = False" +| "bnullable (AALTs bs rs) = (\r \ set rs. bnullable r)" +| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \ bnullable r2)" +| "bnullable (ASTAR bs r) = True" + +fun + bmkeps :: "arexp \ bit list" +where + "bmkeps(AONE bs) = bs" +| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" +| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)" +| "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))" +| "bmkeps(ASTAR bs r) = bs @ [S]" + + +fun + bder :: "char \ arexp \ arexp" +where + "bder c (AZERO) = AZERO" +| "bder c (AONE bs) = AZERO" +| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" +| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" +| "bder c (ASEQ bs r1 r2) = + (if bnullable r1 + then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) + else ASEQ bs (bder c r1) r2)" +| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" + + +fun + bders :: "arexp \ string \ arexp" +where + "bders r [] = r" +| "bders r (c#s) = bders (bder c r) s" + +lemma bders_append: + "bders r (s1 @ s2) = bders (bders r s1) s2" + apply(induct s1 arbitrary: r s2) + apply(simp_all) + done + +lemma bnullable_correctness: + shows "nullable (erase r) = bnullable r" + apply(induct r rule: erase.induct) + apply(simp_all) + done + +lemma erase_fuse: + shows "erase (fuse bs r) = erase r" + apply(induct r rule: erase.induct) + apply(simp_all) + done + +lemma erase_intern [simp]: + shows "erase (intern r) = r" + apply(induct r) + apply(simp_all add: erase_fuse) + done + +lemma erase_bder [simp]: + shows "erase (bder a r) = der a (erase r)" + apply(induct r rule: erase.induct) + apply(simp_all add: erase_fuse bnullable_correctness) + done + +lemma erase_bders [simp]: + shows "erase (bders r s) = ders s (erase r)" + apply(induct s arbitrary: r ) + apply(simp_all) + done + +lemma retrieve_encode_STARS: + assumes "\v\set vs. \ v : r \ code v = retrieve (intern r) v" + shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" + using assms + apply(induct vs) + apply(simp_all) + done + +lemma retrieve_fuse2: + assumes "\ v : (erase r)" + shows "retrieve (fuse bs r) v = bs @ retrieve r v" + using assms + apply(induct r arbitrary: v bs) + apply(auto elim: Prf_elims)[4] + defer + using retrieve_encode_STARS + apply(auto elim!: Prf_elims)[1] + apply(case_tac vs) + apply(simp) + apply(simp) + (* AALTs case *) + apply(simp) + apply(case_tac x2a) + apply(simp) + apply(auto elim!: Prf_elims)[1] + apply(simp) + apply(case_tac list) + apply(simp) + apply(auto) + apply(auto elim!: Prf_elims)[1] + done + +lemma retrieve_fuse: + assumes "\ v : r" + shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" + using assms + by (simp_all add: retrieve_fuse2) + + +lemma retrieve_code: + assumes "\ v : r" + shows "code v = retrieve (intern r) v" + using assms + apply(induct v r ) + apply(simp_all add: retrieve_fuse retrieve_encode_STARS) + done + +lemma r: + assumes "bnullable (AALTs bs (a # rs))" + shows "bnullable a \ (\ bnullable a \ bnullable (AALTs bs rs))" + using assms + apply(induct rs) + apply(auto) + done + +lemma r0: + assumes "bnullable a" + shows "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)" + using assms + by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust) + +lemma r1: + assumes "\ bnullable a" "bnullable (AALTs bs rs)" + shows "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)" + using assms + apply(induct rs) + apply(auto) + done + +lemma r2: + assumes "x \ set rs" "bnullable x" + shows "bnullable (AALTs bs rs)" + using assms + apply(induct rs) + apply(auto) + done + +lemma r3: + assumes "\ bnullable r" + " \ x \ set rs. bnullable x" + shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) = + retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))" + using assms + apply(induct rs arbitrary: r bs) + apply(auto)[1] + apply(auto) + using bnullable_correctness apply blast + apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2) + apply(subst retrieve_fuse2[symmetric]) + apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable) + apply(simp) + apply(case_tac "bnullable a") + apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2) + apply(drule_tac x="a" in meta_spec) + apply(drule_tac x="bs" in meta_spec) + apply(drule meta_mp) + apply(simp) + apply(drule meta_mp) + apply(auto) + apply(subst retrieve_fuse2[symmetric]) + apply(case_tac rs) + apply(simp) + apply(auto)[1] + apply (simp add: bnullable_correctness) + apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2) + apply (simp add: bnullable_correctness) + apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2) + apply(simp) + done + + +lemma t: + assumes "\r \ set rs. nullable (erase r) \ bmkeps r = retrieve r (mkeps (erase r))" + "nullable (erase (AALTs bs rs))" + shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" + using assms + apply(induct rs arbitrary: bs) + apply(simp) + apply(auto simp add: bnullable_correctness) + apply(case_tac rs) + apply(auto simp add: bnullable_correctness)[2] + apply(subst r1) + apply(simp) + apply(rule r2) + apply(assumption) + apply(simp) + apply(drule_tac x="bs" in meta_spec) + apply(drule meta_mp) + apply(auto)[1] + prefer 2 + apply(case_tac "bnullable a") + apply(subst r0) + apply blast + apply(subgoal_tac "nullable (erase a)") + prefer 2 + using bnullable_correctness apply blast + apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4)) + apply(subst r1) + apply(simp) + using r2 apply blast + apply(drule_tac x="bs" in meta_spec) + apply(drule meta_mp) + apply(auto)[1] + apply(simp) + using r3 apply blast + apply(auto) + using r3 by blast + +lemma bmkeps_retrieve: + assumes "nullable (erase r)" + shows "bmkeps r = retrieve r (mkeps (erase r))" + using assms + apply(induct r) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + defer + apply(simp) + apply(rule t) + apply(auto) + done + +lemma bder_retrieve: + assumes "\ v : der c (erase r)" + shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" + using assms + apply(induct r arbitrary: v rule: erase.induct) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(case_tac "c = ca") + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(case_tac rs) + apply(simp) + apply(simp) + apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) + apply(simp) + apply(case_tac "nullable (erase r1)") + apply(simp) + apply(erule Prf_elims) + apply(subgoal_tac "bnullable r1") + prefer 2 + using bnullable_correctness apply blast + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(subgoal_tac "bnullable r1") + prefer 2 + using bnullable_correctness apply blast + apply(simp) + apply(simp add: retrieve_fuse2) + apply(simp add: bmkeps_retrieve) + apply(simp) + apply(erule Prf_elims) + apply(simp) + using bnullable_correctness apply blast + apply(rename_tac bs r v) + apply(simp) + apply(erule Prf_elims) + apply(clarify) + apply(erule Prf_elims) + apply(clarify) + apply(subst injval.simps) + apply(simp del: retrieve.simps) + apply(subst retrieve.simps) + apply(subst retrieve.simps) + apply(simp) + apply(simp add: retrieve_fuse2) + done + + + +lemma MAIN_decode: + assumes "\ v : ders s r" + shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" + using assms +proof (induct s arbitrary: v rule: rev_induct) + case Nil + have "\ v : ders [] r" by fact + then have "\ v : r" by simp + then have "Some v = decode (retrieve (intern r) v) r" + using decode_code retrieve_code by auto + then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" + by simp +next + case (snoc c s v) + have IH: "\v. \ v : ders s r \ + Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact + have asm: "\ v : ders (s @ [c]) r" by fact + then have asm2: "\ injval (ders s r) c v : ders s r" + by (simp add: Prf_injval ders_append) + have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" + by (simp add: flex_append) + also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" + using asm2 IH by simp + also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" + using asm by (simp_all add: bder_retrieve ders_append) + finally show "Some (flex r id (s @ [c]) v) = + decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) +qed + + +definition blex where + "blex a s \ if bnullable (bders a s) then Some (bmkeps (bders a s)) else None" + + + +definition blexer where + "blexer r s \ if bnullable (bders (intern r) s) then + decode (bmkeps (bders (intern r) s)) r else None" + +lemma blexer_correctness: + shows "blexer r s = lexer r s" +proof - + { define bds where "bds \ bders (intern r) s" + define ds where "ds \ ders s r" + assume asm: "nullable ds" + have era: "erase bds = ds" + unfolding ds_def bds_def by simp + have mke: "\ mkeps ds : ds" + using asm by (simp add: mkeps_nullable) + have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" + using bmkeps_retrieve + using asm era by (simp add: bmkeps_retrieve) + also have "... = Some (flex r id s (mkeps ds))" + using mke by (simp_all add: MAIN_decode ds_def bds_def) + finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" + unfolding bds_def ds_def . + } + then show "blexer r s = lexer r s" + unfolding blexer_def lexer_flex + apply(subst bnullable_correctness[symmetric]) + apply(simp) + done +qed + + +fun distinctBy :: "'a list \ ('a \ 'b) \ 'b set \ 'a list" + where + "distinctBy [] f acc = []" +| "distinctBy (x#xs) f acc = + (if (f x) \ acc then distinctBy xs f acc + else x # (distinctBy xs f ({f x} \ acc)))" + +fun flts :: "arexp list \ arexp list" + where + "flts [] = []" +| "flts (AZERO # rs) = flts rs" +| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs" +| "flts (r1 # rs) = r1 # flts rs" + + + + +fun li :: "bit list \ arexp list \ arexp" + where + "li _ [] = AZERO" +| "li bs [a] = fuse bs a" +| "li bs as = AALTs bs as" + + + + +fun bsimp_ASEQ :: "bit list \ arexp \ arexp \ arexp" + where + "bsimp_ASEQ _ AZERO _ = AZERO" +| "bsimp_ASEQ _ _ AZERO = AZERO" +| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" +| "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" + + +fun bsimp_AALTs :: "bit list \ arexp list \ arexp" + where + "bsimp_AALTs _ [] = AZERO" +| "bsimp_AALTs bs1 [r] = fuse bs1 r" +| "bsimp_AALTs bs1 rs = AALTs bs1 rs" + + +fun bsimp :: "arexp \ arexp" + where + "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" +| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))" +| "bsimp r = r" + + + + +fun + bders_simp :: "arexp \ string \ arexp" +where + "bders_simp r [] = r" +| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s" + +definition blexer_simp where + "blexer_simp r s \ if bnullable (bders_simp (intern r) s) then + decode (bmkeps (bders_simp (intern r) s)) r else None" + + +lemma asize0: + shows "0 < asize r" + apply(induct r) + apply(auto) + done + + +lemma bders_simp_append: + shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" + apply(induct s1 arbitrary: r s2) + apply(simp) + apply(simp) + done + +lemma bsimp_ASEQ_size: + shows "asize (bsimp_ASEQ bs r1 r2) \ Suc (asize r1 + asize r2)" + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma fuse_size: + shows "asize (fuse bs r) = asize r" + apply(induct r) + apply(auto) + done + +lemma flts_size: + shows "sum_list (map asize (flts rs)) \ sum_list (map asize rs)" + apply(induct rs rule: flts.induct) + apply(simp_all) + by (metis (mono_tags, lifting) add_mono comp_apply eq_imp_le fuse_size le_SucI map_eq_conv) + + +lemma bsimp_AALTs_size: + shows "asize (bsimp_AALTs bs rs) \ Suc (sum_list (map asize rs))" + apply(induct rs rule: bsimp_AALTs.induct) + apply(auto simp add: fuse_size) + done + + +lemma bsimp_size: + shows "asize (bsimp r) \ asize r" + apply(induct r) + apply(simp_all) + apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans) + apply(rule le_trans) + apply(rule bsimp_AALTs_size) + apply(simp) + apply(rule le_trans) + apply(rule flts_size) + by (simp add: sum_list_mono) + +lemma bsimp_asize0: + shows "(\x\rs. asize (bsimp x)) \ sum_list (map asize rs)" + apply(induct rs) + apply(auto) + by (simp add: add_mono bsimp_size) + +lemma bsimp_AALTs_size2: + assumes "\r \ set rs. nonalt r" + shows "asize (bsimp_AALTs bs rs) \ sum_list (map asize rs)" + using assms + apply(induct rs rule: bsimp_AALTs.induct) + apply(simp_all add: fuse_size) + done + + +lemma qq: + shows "map (asize \ fuse bs) rs = map asize rs" + apply(induct rs) + apply(auto simp add: fuse_size) + done + +lemma flts_size2: + assumes "\bs rs'. AALTs bs rs' \ set rs" + shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)" + using assms + apply(induct rs) + apply(auto simp add: qq) + apply (simp add: flts_size less_Suc_eq_le) + apply(case_tac a) + apply(auto simp add: qq) + prefer 2 + apply (simp add: flts_size le_imp_less_Suc) + using less_Suc_eq by auto + +lemma bsimp_AALTs_size3: + assumes "\r \ set (map bsimp rs). \nonalt r" + shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)" + using assms flts_size2 + apply - + apply(clarify) + apply(simp) + apply(drule_tac x="map bsimp rs" in meta_spec) + apply(drule meta_mp) + apply (metis list.set_map nonalt.elims(3)) + apply(simp) + apply(rule order_class.order.strict_trans1) + apply(rule bsimp_AALTs_size) + apply(simp) + by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq) + + + + +lemma L_bsimp_ASEQ: + "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(simp_all) + by (metis erase_fuse fuse.simps(4)) + +lemma L_bsimp_AALTs: + "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))" + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(simp_all add: erase_fuse) + done + +lemma L_erase_AALTs: + shows "L (erase (AALTs bs rs)) = \ (L ` erase ` (set rs))" + apply(induct rs) + apply(simp) + apply(simp) + apply(case_tac rs) + apply(simp) + apply(simp) + done + +lemma L_erase_flts: + shows "\ (L ` erase ` (set (flts rs))) = \ (L ` erase ` (set rs))" + apply(induct rs rule: flts.induct) + apply(simp_all) + apply(auto) + using L_erase_AALTs erase_fuse apply auto[1] + by (simp add: L_erase_AALTs erase_fuse) + + +lemma L_bsimp_erase: + shows "L (erase r) = L (erase (bsimp r))" + apply(induct r) + apply(simp) + apply(simp) + apply(simp) + apply(auto simp add: Sequ_def)[1] + apply(subst L_bsimp_ASEQ[symmetric]) + apply(auto simp add: Sequ_def)[1] + apply(subst (asm) L_bsimp_ASEQ[symmetric]) + apply(auto simp add: Sequ_def)[1] + apply(simp) + apply(subst L_bsimp_AALTs[symmetric]) + defer + apply(simp) + apply(subst (2)L_erase_AALTs) + apply(subst L_erase_flts) + apply(auto) + apply (simp add: L_erase_AALTs) + using L_erase_AALTs by blast + +lemma bsimp_ASEQ0: + shows "bsimp_ASEQ bs r1 AZERO = AZERO" + apply(induct r1) + apply(auto) + done + + + +lemma bsimp_ASEQ1: + assumes "r1 \ AZERO" "r2 \ AZERO" "\bs. r1 \ AONE bs" + shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" + using assms + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma bsimp_ASEQ2: + shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2" + apply(induct r2) + apply(auto) + done + + +lemma L_bders_simp: + shows "L (erase (bders_simp r s)) = L (erase (bders r s))" + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply(simp) + apply(simp add: ders_append) + apply(simp add: bders_simp_append) + apply(simp add: L_bsimp_erase[symmetric]) + by (simp add: der_correctness) + +lemma b1: + "bsimp_ASEQ bs1 (AONE bs) r = fuse (bs1 @ bs) r" + apply(induct r) + apply(auto) + done + +lemma b2: + assumes "bnullable r" + shows "bmkeps (fuse bs r) = bs @ bmkeps r" + by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2) + +lemma b3: + shows "bnullable r = bnullable (bsimp r)" + using L_bsimp_erase bnullable_correctness nullable_correctness by auto + + +lemma b4: + shows "bnullable (bders_simp r s) = bnullable (bders r s)" + by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1)) + +lemma q1: + assumes "\r \ set rs. bmkeps(bsimp r) = bmkeps r" + shows "map (\r. bmkeps(bsimp r)) rs = map bmkeps rs" + using assms + apply(induct rs) + apply(simp) + apply(simp) + done + +lemma q3: + assumes "\r \ set rs. bnullable r" + shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)" + using assms + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(simp) + apply(simp) + apply (simp add: b2) + apply(simp) + done + +lemma qq1: + assumes "\r \ set rs. bnullable r" + shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)" + using assms + apply(induct rs arbitrary: rs1 bs) + apply(simp) + apply(simp) + by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last) + +lemma qq2: + assumes "\r \ set rs. \ bnullable r" "\r \ set rs1. bnullable r" + shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)" + using assms + apply(induct rs arbitrary: rs1 bs) + apply(simp) + apply(simp) + by (metis append_assoc in_set_conv_decomp r1 r2) + +lemma qq3: + shows "bnullable (AALTs bs rs) = (\r \ set rs. bnullable r)" + apply(induct rs arbitrary: bs) + apply(simp) + apply(simp) + done + +lemma fuse_empty: + shows "fuse [] r = r" + apply(induct r) + apply(auto) + done + +lemma flts_fuse: + shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)" + apply(induct rs arbitrary: bs rule: flts.induct) + apply(auto simp add: fuse_append) + done + +lemma bsimp_ASEQ_fuse: + shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" + apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma bsimp_AALTs_fuse: + assumes "\r \ set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r" + shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs" + using assms + apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct) + apply(auto) + done + + + +lemma bsimp_fuse: + shows "fuse bs (bsimp r) = bsimp (fuse bs r)" +apply(induct r arbitrary: bs) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply(simp) + apply (simp add: bsimp_ASEQ_fuse) + apply(simp) + by (simp add: bsimp_AALTs_fuse fuse_append) + +lemma bsimp_fuse_AALTs: + shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)" + apply(subst bsimp_fuse) + apply(simp) + done + +lemma bsimp_fuse_AALTs2: + shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs" + using bsimp_AALTs_fuse fuse_append by auto + + +lemma bsimp_ASEQ_idem: + assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2" + shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)" + using assms + apply(case_tac "bsimp r1 = AZERO") + apply(simp) + apply(case_tac "bsimp r2 = AZERO") + apply(simp) + apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6)) + apply(case_tac "\bs. bsimp r1 = AONE bs") + apply(auto)[1] + apply(subst bsimp_ASEQ2) + apply(subst bsimp_ASEQ2) + apply (metis assms(2) bsimp_fuse) + apply(subst bsimp_ASEQ1) + apply(auto) + done + + +fun nonnested :: "arexp \ bool" + where + "nonnested (AALTs bs2 []) = True" +| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" +| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)" +| "nonnested r = True" + + +lemma k0: + shows "flts (r # rs1) = flts [r] @ flts rs1" + apply(induct r arbitrary: rs1) + apply(auto) + done + +lemma k00: + shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2" + apply(induct rs1 arbitrary: rs2) + apply(auto) + by (metis append.assoc k0) + +lemma k0a: + shows "flts [AALTs bs rs] = map (fuse bs) rs" + apply(simp) + done + + +lemma k0b: + assumes "nonalt r" "r \ AZERO" + shows "flts [r] = [r]" + using assms + apply(case_tac r) + apply(simp_all) + done + +lemma nn1: + assumes "nonnested (AALTs bs rs)" + shows "\bs1 rs1. flts rs = [AALTs bs1 rs1]" + using assms + apply(induct rs rule: flts.induct) + apply(auto) + done + +lemma nn1q: + assumes "nonnested (AALTs bs rs)" + shows "\bs1 rs1. AALTs bs1 rs1 \ set (flts rs)" + using assms + apply(induct rs rule: flts.induct) + apply(auto) + done + +lemma nn1qq: + assumes "nonnested (AALTs bs rs)" + shows "\bs1 rs1. AALTs bs1 rs1 \ set rs" + using assms + apply(induct rs rule: flts.induct) + apply(auto) + done + +lemma nn10: + assumes "nonnested (AALTs cs rs)" + shows "nonnested (AALTs (bs @ cs) rs)" + using assms + apply(induct rs arbitrary: cs bs) + apply(simp_all) + apply(case_tac a) + apply(simp_all) + done + +lemma nn11a: + assumes "nonalt r" + shows "nonalt (fuse bs r)" + using assms + apply(induct r) + apply(auto) + done + + +lemma nn1a: + assumes "nonnested r" + shows "nonnested (fuse bs r)" + using assms + apply(induct bs r arbitrary: rule: fuse.induct) + apply(simp_all add: nn10) + done + +lemma n0: + shows "nonnested (AALTs bs rs) \ (\r \ set rs. nonalt r)" + apply(induct rs arbitrary: bs) + apply(auto) + apply (metis list.set_intros(1) nn1qq nonalt.elims(3)) + apply (metis list.set_intros(2) nn1qq nonalt.elims(3)) + by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7)) + + + + +lemma nn1c: + assumes "\r \ set rs. nonnested r" + shows "\r \ set (flts rs). nonalt r" + using assms + apply(induct rs rule: flts.induct) + apply(auto) + apply(rule nn11a) + by (metis nn1qq nonalt.elims(3)) + +lemma nn1bb: + assumes "\r \ set rs. nonalt r" + shows "nonnested (bsimp_AALTs bs rs)" + using assms + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(auto) + apply (metis nn11a nonalt.simps(1) nonnested.elims(3)) + using n0 by auto + +lemma nn1b: + shows "nonnested (bsimp r)" + apply(induct r) + apply(simp_all) + apply(case_tac "bsimp r1 = AZERO") + apply(simp) + apply(case_tac "bsimp r2 = AZERO") + apply(simp) + apply(subst bsimp_ASEQ0) + apply(simp) + apply(case_tac "\bs. bsimp r1 = AONE bs") + apply(auto)[1] + apply(subst bsimp_ASEQ2) + apply (simp add: nn1a) + apply(subst bsimp_ASEQ1) + apply(auto) + apply(rule nn1bb) + apply(auto) + by (metis (mono_tags, hide_lams) imageE nn1c set_map) + +lemma nn1d: + assumes "bsimp r = AALTs bs rs" + shows "\r1 \ set rs. \ bs. r1 \ AALTs bs rs2" + using nn1b assms + by (metis nn1qq) + +lemma nn_flts: + assumes "nonnested (AALTs bs rs)" + shows "\r \ set (flts rs). nonalt r" + using assms + apply(induct rs arbitrary: bs rule: flts.induct) + apply(auto) + done + + + +lemma rt: + shows "sum_list (map asize (flts (map bsimp rs))) \ sum_list (map asize rs)" + apply(induct rs) + apply(simp) + apply(simp) + apply(subst k0) + apply(simp) + by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1) + +lemma bsimp_AALTs_qq: + assumes "1 < length rs" + shows "bsimp_AALTs bs rs = AALTs bs rs" + using assms + apply(case_tac rs) + apply(simp) + apply(case_tac list) + apply(simp_all) + done + + +lemma bsimp_AALTs1: + assumes "nonalt r" + shows "bsimp_AALTs bs (flts [r]) = fuse bs r" + using assms + apply(case_tac r) + apply(simp_all) + done + +lemma bbbbs: + assumes "good r" "r = AALTs bs1 rs" + shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)" + using assms + by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast) + +lemma bbbbs1: + shows "nonalt r \ (\bs rs. r = AALTs bs rs)" + using nonalt.elims(3) by auto + + +lemma good_fuse: + shows "good (fuse bs r) = good r" + apply(induct r arbitrary: bs) + apply(auto) + apply(case_tac r1) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r1) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac x2a) + apply(simp_all) + apply(case_tac list) + apply(simp_all) + apply(case_tac x2a) + apply(simp_all) + apply(case_tac list) + apply(simp_all) + done + +lemma good0: + assumes "rs \ Nil" "\r \ set rs. nonalt r" + shows "good (bsimp_AALTs bs rs) \ (\r \ set rs. good r)" + using assms + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(auto simp add: good_fuse) + done + +lemma good0a: + assumes "flts (map bsimp rs) \ Nil" "\r \ set (flts (map bsimp rs)). nonalt r" + shows "good (bsimp (AALTs bs rs)) \ (\r \ set (flts (map bsimp rs)). good r)" + using assms + apply(simp) + apply(auto) + apply(subst (asm) good0) + apply(simp) + apply(auto) + apply(subst good0) + apply(simp) + apply(auto) + done + +lemma flts0: + assumes "r \ AZERO" "nonalt r" + shows "flts [r] \ []" + using assms + apply(induct r) + apply(simp_all) + done + +lemma flts1: + assumes "good r" + shows "flts [r] \ []" + using assms + apply(induct r) + apply(simp_all) + apply(case_tac x2a) + apply(simp) + apply(simp) + done + +lemma flts2: + assumes "good r" + shows "\r' \ set (flts [r]). good r' \ nonalt r'" + using assms + apply(induct r) + apply(simp) + apply(simp) + apply(simp) + prefer 2 + apply(simp) + apply(auto)[1] + apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse) + apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a) + apply fastforce + apply(simp) + done + + +lemma flts3: + assumes "\r \ set rs. good r \ r = AZERO" + shows "\r \ set (flts rs). good r" + using assms + apply(induct rs arbitrary: rule: flts.induct) + apply(simp_all) + by (metis UnE flts2 k0a set_map) + +lemma flts3b: + assumes "\r\set rs. good r" + shows "flts rs \ []" + using assms + apply(induct rs arbitrary: rule: flts.induct) + apply(simp) + apply(simp) + apply(simp) + apply(auto) + done + +lemma flts4: + assumes "bsimp_AALTs bs (flts rs) = AZERO" + shows "\r \ set rs. \ good r" + using assms + apply(induct rs arbitrary: bs rule: flts.induct) + apply(auto) + defer + apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2)) + apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3)) + apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject) + apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject) + apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject) + apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6)) + by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a) + + +lemma flts_nil: + assumes "\y. asize y < Suc (sum_list (map asize rs)) \ + good (bsimp y) \ bsimp y = AZERO" + and "\r\set rs. \ good (bsimp r)" + shows "flts (map bsimp rs) = []" + using assms + apply(induct rs) + apply(simp) + apply(simp) + apply(subst k0) + apply(simp) + by force + +lemma flts_nil2: + assumes "\y. asize y < Suc (sum_list (map asize rs)) \ + good (bsimp y) \ bsimp y = AZERO" + and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO" + shows "flts (map bsimp rs) = []" + using assms + apply(induct rs arbitrary: bs) + apply(simp) + apply(simp) + apply(subst k0) + apply(simp) + apply(subst (asm) k0) + apply(auto) + apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1)) + by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1)) + + + +lemma good_SEQ: + assumes "r1 \ AZERO" "r2 \ AZERO" "\bs. r1 \ AONE bs" + shows "good (ASEQ bs r1 r2) = (good r1 \ good r2)" + using assms + apply(case_tac r1) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + apply(case_tac r2) + apply(simp_all) + done + +lemma good1: + shows "good (bsimp a) \ bsimp a = AZERO" + apply(induct a taking: asize rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + prefer 2 + (* AALTs case *) + apply(simp only:) + apply(case_tac "x52") + apply(simp) + thm good0a + (* AALTs list at least one - case *) + apply(simp only: ) + apply(frule_tac x="a" in spec) + apply(drule mp) + apply(simp) + (* either first element is good, or AZERO *) + apply(erule disjE) + prefer 2 + apply(simp) + (* in the AZERO case, the size is smaller *) + apply(drule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(subst (asm) bsimp.simps) + apply(subst (asm) bsimp.simps) + apply(assumption) + (* in the good case *) + apply(frule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(erule disjE) + apply(rule disjI1) + apply(simp add: good0) + apply(subst good0) + apply (metis Nil_is_append_conv flts1 k0) + apply (metis ex_map_conv list.simps(9) nn1b nn1c) + apply(simp) + apply(subst k0) + apply(simp) + apply(auto)[1] + using flts2 apply blast + apply(subst (asm) good0) + prefer 3 + apply(auto)[1] + apply auto[1] + apply (metis ex_map_conv nn1b nn1c) + (* in the AZERO case *) + apply(simp) + apply(frule_tac x="a" in spec) + apply(drule mp) + apply(simp) + apply(erule disjE) + apply(rule disjI1) + apply(subst good0) + apply(subst k0) + using flts1 apply blast + apply(auto)[1] + apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c) + apply(auto)[1] + apply(subst (asm) k0) + apply(auto)[1] + using flts2 apply blast + apply(frule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(erule disjE) + apply(simp) + apply(simp) + apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject) + apply(subst (2) k0) + apply(simp) + (* SEQ case *) + apply(simp) + apply(case_tac "bsimp x42 = AZERO") + apply(simp) + apply(case_tac "bsimp x43 = AZERO") + apply(simp) + apply(subst (2) bsimp_ASEQ0) + apply(simp) + apply(case_tac "\bs. bsimp x42 = AONE bs") + apply(auto)[1] + apply(subst bsimp_ASEQ2) + using good_fuse apply force + apply(subst bsimp_ASEQ1) + apply(auto) + apply(subst good_SEQ) + apply(simp) + apply(simp) + apply(simp) + using less_add_Suc1 less_add_Suc2 by blast + +lemma good1a: + assumes "L(erase a) \ {}" + shows "good (bsimp a)" + using good1 assms + using L_bsimp_erase by force + + + +lemma flts_append: + "flts (xs1 @ xs2) = flts xs1 @ flts xs2" + apply(induct xs1 arbitrary: xs2 rule: rev_induct) + apply(auto) + apply(case_tac xs) + apply(auto) + apply(case_tac x) + apply(auto) + apply(case_tac x) + apply(auto) + done + +lemma g1: + assumes "good (bsimp_AALTs bs rs)" + shows "bsimp_AALTs bs rs = AALTs bs rs \ (\r. rs = [r] \ bsimp_AALTs bs [r] = fuse bs r)" +using assms + apply(induct rs arbitrary: bs) + apply(simp) + apply(case_tac rs) + apply(simp only:) + apply(simp) + apply(case_tac list) + apply(simp) + by simp + +lemma flts_0: + assumes "nonnested (AALTs bs rs)" + shows "\r \ set (flts rs). r \ AZERO" + using assms + apply(induct rs arbitrary: bs rule: flts.induct) + apply(simp) + apply(simp) + defer + apply(simp) + apply(simp) + apply(simp) +apply(simp) + apply(rule ballI) + apply(simp) + done + +lemma flts_0a: + assumes "nonnested (AALTs bs rs)" + shows "AZERO \ set (flts rs)" + using assms + using flts_0 by blast + +lemma qqq1: + shows "AZERO \ set (flts (map bsimp rs))" + by (metis ex_map_conv flts3 good.simps(1) good1) + + +fun nonazero :: "arexp \ bool" + where + "nonazero AZERO = False" +| "nonazero r = True" + +lemma flts_concat: + shows "flts rs = concat (map (\r. flts [r]) rs)" + apply(induct rs) + apply(auto) + apply(subst k0) + apply(simp) + done + +lemma flts_single1: + assumes "nonalt r" "nonazero r" + shows "flts [r] = [r]" + using assms + apply(induct r) + apply(auto) + done + +lemma flts_qq: + assumes "\y. asize y < Suc (sum_list (map asize rs)) \ good y \ bsimp y = y" + "\r'\set rs. good r' \ nonalt r'" + shows "flts (map bsimp rs) = rs" + using assms + apply(induct rs) + apply(simp) + apply(simp) + apply(subst k0) + apply(subgoal_tac "flts [bsimp a] = [a]") + prefer 2 + apply(drule_tac x="a" in spec) + apply(drule mp) + apply(simp) + apply(auto)[1] + using good.simps(1) k0b apply blast + apply(auto)[1] + done + +lemma test: + assumes "good r" + shows "bsimp r = r" + using assms + apply(induct r taking: "asize" rule: measure_induct) + apply(erule good.elims) + apply(simp_all) + apply(subst k0) + apply(subst (2) k0) + apply(subst flts_qq) + apply(auto)[1] + apply(auto)[1] + apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b) + apply force+ + apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2) + apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2) + apply force+ + apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2) + apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2) + apply force+ + done + +lemma test2: + assumes "good r" + shows "bsimp r = r" + using assms + apply(induct r taking: "asize" rule: measure_induct) + apply(case_tac x) + apply(simp_all) + defer + (* AALT case *) + apply(subgoal_tac "1 < length x52") + prefer 2 + apply(case_tac x52) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + apply(simp) + apply(subst bsimp_AALTs_qq) + prefer 2 + apply(subst flts_qq) + apply(auto)[1] + apply(auto)[1] + apply(case_tac x52) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + apply(simp) + apply(auto)[1] + apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff) + apply(simp) + apply(case_tac x52) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + apply(simp) + apply(subst k0) + apply(simp) + apply(subst (2) k0) + apply(simp) + apply (simp add: Suc_lessI flts1 one_is_add) + (* SEQ case *) + apply(case_tac "bsimp x42 = AZERO") + apply simp + apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1) + apply(case_tac "\bs'. bsimp x42 = AONE bs'") + apply(auto)[1] + defer + apply(case_tac "bsimp x43 = AZERO") + apply(simp) + apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2) + apply(auto) + apply (subst bsimp_ASEQ1) + apply(auto)[3] + apply(auto)[1] + apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1) + apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2) + apply (subst bsimp_ASEQ2) + apply(drule_tac x="x42" in spec) + apply(drule mp) + apply(simp) + apply(drule mp) + apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ) + apply(simp) + done + + +lemma bsimp_idem: + shows "bsimp (bsimp r) = bsimp r" + using test good1 + by force + + +lemma q3a: + assumes "\r \ set rs. bnullable r" + shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)" + using assms + apply(induct rs arbitrary: bs bs1) + apply(simp) + apply(simp) + apply(auto) + apply (metis append_assoc b2 bnullable_correctness erase_fuse r0) + apply(case_tac "bnullable a") + apply (metis append.assoc b2 bnullable_correctness erase_fuse r0) + apply(case_tac rs) + apply(simp) + apply(simp) + apply(auto)[1] + apply (metis bnullable_correctness erase_fuse)+ + done + +lemma qq4: + assumes "\x\set list. bnullable x" + shows "\x\set (flts list). bnullable x" + using assms + apply(induct list rule: flts.induct) + apply(auto) + by (metis UnCI bnullable_correctness erase_fuse imageI) + + +lemma qs3: + assumes "\r \ set rs. bnullable r" + shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))" + using assms + apply(induct rs arbitrary: bs taking: size rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(case_tac a) + apply(simp) + apply (simp add: r1) + apply(simp) + apply (simp add: r0) + apply(simp) + apply(case_tac "flts list") + apply(simp) + 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) + apply(simp) + apply (simp add: r1) + prefer 3 + apply(simp) + apply (simp add: r0) + prefer 2 + apply(simp) + apply(case_tac "\x\set x52. bnullable x") + apply(case_tac "list") + apply(simp) + apply (metis b2 fuse.simps(4) q3a r2) + apply(erule disjE) + apply(subst qq1) + apply(auto)[1] + apply (metis bnullable_correctness erase_fuse) + apply(simp) + apply (metis b2 fuse.simps(4) q3a r2) + apply(simp) + apply(auto)[1] + apply(subst qq1) + apply (metis bnullable_correctness erase_fuse image_eqI set_map) + apply (metis b2 fuse.simps(4) q3a r2) + apply(subst qq1) + apply (metis bnullable_correctness erase_fuse image_eqI set_map) + apply (metis b2 fuse.simps(4) q3a r2) + apply(simp) + apply(subst qq2) + apply (metis bnullable_correctness erase_fuse imageE set_map) + prefer 2 + apply(case_tac "list") + apply(simp) + apply(simp) + apply (simp add: qq4) + apply(simp) + apply(auto) + apply(case_tac list) + apply(simp) + apply(simp) + apply (simp add: r0) + apply(case_tac "bnullable (ASEQ x41 x42 x43)") + apply(case_tac list) + apply(simp) + apply(simp) + apply (simp add: r0) + apply(simp) + using qq4 r1 r2 by auto + + + +lemma k1: + assumes "\x2aa. \x2aa \ set x2a; bnullable x2aa\ \ bmkeps x2aa = bmkeps (bsimp x2aa)" + "\x\set x2a. bnullable x" + shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))" + using assms + apply(induct x2a) + apply fastforce + apply(simp) + apply(subst k0) + apply(subst (2) k0) + apply(auto)[1] + apply (metis b3 k0 list.set_intros(1) qs3 r0) + by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map) + + + +lemma bmkeps_simp: + assumes "bnullable r" + shows "bmkeps r = bmkeps (bsimp r)" + using assms + apply(induct r) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply(case_tac "bsimp r1 = AZERO") + apply(simp) + apply(auto)[1] + apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable) + apply(case_tac "bsimp r2 = AZERO") + apply(simp) + apply(auto)[1] + apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable) + apply(case_tac "\bs. bsimp r1 = AONE bs") + apply(auto)[1] + apply(subst b1) + apply(subst b2) + apply(simp add: b3[symmetric]) + apply(simp) + apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)") + prefer 2 + 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)) + apply(simp) + apply(simp) + thm q3 + apply(subst q3[symmetric]) + apply simp + using b3 qq4 apply auto[1] + apply(subst qs3) + apply simp + using k1 by blast + +thm bmkeps_retrieve bmkeps_simp bder_retrieve + +lemma bmkeps_bder_AALTs: + assumes "\r \ set rs. bnullable (bder c r)" + shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))" + using assms + apply(induct rs) + apply(simp) + apply(simp) + apply(auto) + apply(case_tac rs) + apply(simp) + apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2) + apply(simp) + apply(case_tac rs) + apply(simp_all) + done + +lemma bbs0: + shows "blexer_simp r [] = blexer r []" + apply(simp add: blexer_def blexer_simp_def) + done + +lemma bbs1: + shows "blexer_simp r [c] = blexer r [c]" + apply(simp add: blexer_def blexer_simp_def) + apply(auto) + defer + using b3 apply auto[1] + using b3 apply auto[1] + apply(subst bmkeps_simp[symmetric]) + apply(simp) + apply(simp) + done + +lemma oo: + shows "(case (blexer (der c r) s) of None \ None | Some v \ Some (injval r c v)) = blexer r (c # s)" + apply(simp add: blexer_correctness) + done + + +lemma bder_fuse: + shows "bder c (fuse bs a) = fuse bs (bder c a)" + apply(induct a arbitrary: bs c) + apply(simp_all) + done + + +fun flts2 :: "char \ arexp list \ arexp list" + where + "flts2 _ [] = []" +| "flts2 c (AZERO # rs) = flts2 c rs" +| "flts2 c (AONE _ # rs) = flts2 c rs" +| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)" +| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs" +| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \ r2 = AZERO) then + flts2 c rs + else ASEQ bs r1 r2 # flts2 c rs)" +| "flts2 c (r1 # rs) = r1 # flts2 c rs" + +lemma flts2_k0: + shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1" + apply(induct r arbitrary: c rs1) + apply(auto) + done + +lemma flts2_k00: + shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2" + apply(induct rs1 arbitrary: rs2 c) + apply(auto) + by (metis append.assoc flts2_k0) + + +lemma + shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))" + apply(induct c rs rule: flts2.induct) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + apply(auto simp add: bder_fuse)[1] + defer + apply(simp) + apply(simp del: flts2.simps) + apply(rule conjI) + prefer 2 + apply(auto)[1] + apply(rule impI) + apply(subst flts2_k0) + apply(subst map_append) + apply(subst flts2.simps) + apply(simp only: flts2.simps) + apply(auto) + + + +lemma XXX2_helper: + assumes "\y. asize y < Suc (sum_list (map asize rs)) \ good y \ bsimp y = y" + "\r'\set rs. good r' \ nonalt r'" + shows "flts (map (bsimp \ bder c) (flts (map bsimp rs))) = flts (map (bsimp \ bder c) rs)" + using assms + apply(induct rs arbitrary: c) + apply(simp) + apply(simp) + apply(subst k0) + apply(simp add: flts_append) + apply(subst (2) k0) + apply(simp add: flts_append) + apply(subgoal_tac "flts [a] = [a]") + prefer 2 + using good.simps(1) k0b apply blast + apply(simp) + done + +lemma bmkeps_good: + assumes "good a" + shows "bmkeps (bsimp a) = bmkeps a" + using assms + using test2 by auto + + +lemma xxx_bder: + assumes "good r" + shows "L (erase r) \ {}" + using assms + apply(induct r rule: good.induct) + apply(auto simp add: Sequ_def) + done + +lemma xxx_bder2: + assumes "L (erase (bsimp r)) = {}" + shows "bsimp r = AZERO" + using assms xxx_bder test2 good1 + by blast + +lemma XXX2aa: + assumes "good a" + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + using assms + by (simp add: test2) + +lemma XXX2aa_ders: + assumes "good a" + shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)" + using assms + by (simp add: test2) + +lemma XXX4a: + shows "good (bders_simp (bsimp r) s) \ bders_simp (bsimp r) s = AZERO" + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply (simp add: good1) + apply(simp add: bders_simp_append) + apply (simp add: good1) + done + +lemma XXX4a_good: + assumes "good a" + shows "good (bders_simp a s) \ bders_simp a s = AZERO" + using assms + apply(induct s arbitrary: a rule: rev_induct) + apply(simp) + apply(simp add: bders_simp_append) + apply (simp add: good1) + done + +lemma XXX4a_good_cons: + assumes "s \ []" + shows "good (bders_simp a s) \ bders_simp a s = AZERO" + using assms + apply(case_tac s) + apply(auto) + using XXX4a by blast + +lemma XXX4b: + assumes "good a" "L (erase (bders_simp a s)) \ {}" + shows "good (bders_simp a s)" + using assms + apply(induct s arbitrary: a) + apply(simp) + apply(simp) + apply(subgoal_tac "L (erase (bder a aa)) = {} \ L (erase (bder a aa)) \ {}") + prefer 2 + apply(auto)[1] + apply(erule disjE) + apply(subgoal_tac "bsimp (bder a aa) = AZERO") + prefer 2 + using L_bsimp_erase xxx_bder2 apply auto[1] + apply(simp) + apply (metis L.simps(1) XXX4a erase.simps(1)) + apply(drule_tac x="bsimp (bder a aa)" in meta_spec) + apply(drule meta_mp) + apply simp + apply(rule good1a) + apply(auto) + done + +lemma bders_AZERO: + shows "bders AZERO s = AZERO" + and "bders_simp AZERO s = AZERO" + apply (induct s) + apply(auto) + done + +lemma LA: + assumes "\ v : ders s (erase r)" + shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)" + using assms + apply(induct s arbitrary: r v rule: rev_induct) + apply(simp) + apply(simp add: bders_append ders_append) + apply(subst bder_retrieve) + apply(simp) + apply(drule Prf_injval) + by (simp add: flex_append) + + +lemma LB: + assumes "s \ (erase r) \ v" + shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" + using assms + apply(induct s arbitrary: r v rule: rev_induct) + apply(simp) + apply(subgoal_tac "v = mkeps (erase r)") + prefer 2 + apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness) + apply(simp) + apply(simp add: flex_append ders_append) + by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex) + +lemma LB_sym: + assumes "s \ (erase r) \ v" + shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))" + using assms + by (simp add: LB) + + +lemma LC: + assumes "s \ (erase r) \ v" + shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))" + apply(simp) + by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable) + + +lemma L0: + assumes "bnullable a" + shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))" + using assms + by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness) + +thm bmkeps_retrieve + +lemma L0a: + assumes "s \ L(erase a)" + shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) = + retrieve (bders a s) (mkeps (erase (bders a s)))" + using assms + by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex) + +lemma L0aa: + assumes "s \ L (erase a)" + shows "[] \ erase (bsimp (bders a s)) \ mkeps (erase (bsimp (bders a s)))" + using assms + by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex) + +lemma L0aaa: + assumes "[c] \ L (erase a)" + shows "[c] \ (erase a) \ flex (erase a) id [c] (mkeps (erase (bder c a)))" + using assms + by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject) + +lemma L0aaaa: + assumes "[c] \ L (erase a)" + shows "[c] \ (erase a) \ flex (erase a) id [c] (mkeps (erase (bders a [c])))" + using assms + using L0aaa by auto + + +lemma L02: + assumes "bnullable (bder c a)" + shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) = + retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))" + using assms + apply(simp) + using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0 LA LB + apply(subst bder_retrieve[symmetric]) + apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness) + apply(simp) + done + +lemma L02_bders: + assumes "bnullable (bders a s)" + shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = + retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))" + using assms + by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness) + + + + +lemma L03: + assumes "bnullable (bder c a)" + shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = + bmkeps (bsimp (bder c (bsimp a)))" + using assms + by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) + +lemma L04: + assumes "bnullable (bder c a)" + shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = + retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" + using assms + by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness) + +lemma L05: + assumes "bnullable (bder c a)" + shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = + retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" + using assms + using L04 by auto + +lemma L06: + assumes "bnullable (bder c a)" + shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))" + using assms + by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) + +lemma L07: + assumes "s \ L (erase r)" + shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) + = retrieve (bders r s) (mkeps (erase (bders r s)))" + using assms + using LB LC lexer_correct_Some by auto + +lemma LXXX: + assumes "s \ (erase r) \ v" "s \ (erase (bsimp r)) \ v'" + shows "retrieve r v = retrieve (bsimp r) v'" + using assms + apply - + thm LC + apply(subst LC) + apply(assumption) + apply(subst L0[symmetric]) + using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce + apply(subst (2) LC) + apply(assumption) + apply(subst (2) L0[symmetric]) + using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce + + oops + + +lemma L07a: + assumes "s \ L (erase r)" + shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r))))) + = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" + using assms + apply(induct s arbitrary: r) + apply(simp) + using L0a apply force + apply(drule_tac x="(bder a r)" in meta_spec) + apply(drule meta_mp) + apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) + apply(drule sym) + apply(simp) + apply(subst (asm) bder_retrieve) + apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex) + apply(simp only: flex_fun_apply) + apply(simp) + using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] + oops + +lemma L08: + assumes "s \ L (erase r)" + shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s))) + = retrieve (bders r s) (mkeps (erase (bders r s)))" + using assms + apply(induct s arbitrary: r) + apply(simp) + using L0 bnullable_correctness nullable_correctness apply blast + apply(simp add: bders_append) + apply(drule_tac x="(bder a (bsimp r))" in meta_spec) + apply(drule meta_mp) + apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) + apply(drule sym) + apply(simp) + apply(subst LA) + apply (metis L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness) + apply(subst LA) + using lexer_correct_None lexer_flex mkeps_nullable apply force + + using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] + +thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] + oops + +lemma test: + assumes "s = [c]" + shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)" + using assms + apply(simp only: bders.simps) + defer + using assms + apply(simp only: flex.simps id_simps) + using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] + find_theorems "retrieve (bders _ _) _" + find_theorems "retrieve _ (mkeps _)" + oops + +lemma L06X: + assumes "bnullable (bder c a)" + shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)" + using assms + apply(induct a arbitrary: c) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + prefer 2 + apply(simp) + + defer + oops + +lemma L06_2: + assumes "bnullable (bders a [c,d])" + shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))" + using assms + apply(simp) + by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness) + +lemma L06_bders: + assumes "bnullable (bders a s)" + shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))" + using assms + by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness) + +lemma LLLL: + shows "L (erase a) = L (erase (bsimp a))" + and "L (erase a) = {flat v | v. \ v: (erase a)}" + and "L (erase a) = {flat v | v. \ v: (erase (bsimp a))}" + using L_bsimp_erase apply(blast) + apply (simp add: L_flat_Prf) + using L_bsimp_erase L_flat_Prf apply(auto)[1] + done + + + +lemma L07XX: + assumes "s \ L (erase a)" + shows "s \ erase a \ flex (erase a) id s (mkeps (ders s (erase a)))" + using assms + by (meson lexer_correct_None lexer_correctness(1) lexer_flex) + +lemma LX0: + assumes "s \ L r" + shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))" + by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex) + + +lemma L02_bders2: + assumes "bnullable (bders a s)" "s = [c]" + shows "retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s))) = + retrieve (bders a s) (mkeps (erase (bders a s)))" + using assms + apply(simp) + + apply(induct s arbitrary: a) + apply(simp) + using L0 apply auto[1] + oops + +thm bmkeps_retrieve bmkeps_simp Posix_mkeps + +lemma WQ1: + assumes "s \ L (der c r)" + shows "s \ der c r \ mkeps (ders s (der c r))" + using assms + oops + +lemma L02_bsimp: + assumes "bnullable (bders a s)" + shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = + retrieve a (flex (erase a) id s (mkeps (erase (bders a s))))" + using assms + apply(induct s arbitrary: a) + apply(simp) + apply (simp add: L0) + apply(simp) + apply(drule_tac x="bder a aa" in meta_spec) + apply(simp) + apply(subst (asm) bder_retrieve) + using Posix_Prf Posix_flex Posix_mkeps bnullable_correctness apply fastforce + apply(simp add: flex_fun_apply) + apply(drule sym) + apply(simp) + apply(subst flex_injval) + apply(subst bder_retrieve[symmetric]) + apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps bders.simps(2) bnullable_correctness ders.simps(2) erase_bders lexer_correct_None lexer_flex option.distinct(1)) + apply(simp only: erase_bder[symmetric] erase_bders[symmetric]) + apply(subst LB_sym[symmetric]) + apply(simp) + oops + +lemma L1: + assumes "s \ r \ v" + shows "decode (bmkeps (bders (intern r) s)) r = Some v" + using assms + by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1)) + +lemma L2: + assumes "s \ (der c r) \ v" + shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)" + using assms + apply(subst bmkeps_retrieve) + using Posix1(1) lexer_correct_None lexer_flex apply fastforce + using MAIN_decode + apply(subst MAIN_decode[symmetric]) + apply(simp) + apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable) + apply(simp) + apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))") + prefer 2 + apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1)) + apply(simp) + apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) = + (flex (der c r) ((\v. injval r c v) o id) s (mkeps (ders s (der c r))))") + apply(simp) + using flex_fun_apply by blast + +lemma L3: + assumes "s2 \ (ders s1 r) \ v" + shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)" + using assms + apply(induct s1 arbitrary: r s2 v rule: rev_induct) + apply(simp) + using L1 apply blast + apply(simp add: ders_append) + apply(drule_tac x="r" in meta_spec) + apply(drule_tac x="x # s2" in meta_spec) + apply(drule_tac x="injval (ders xs r) x v" in meta_spec) + apply(drule meta_mp) + defer + apply(simp) + apply(simp add: flex_append) + by (simp add: Posix_injval) + + + +lemma bders_snoc: + "bder c (bders a s) = bders a (s @ [c])" + apply(simp add: bders_append) + done + + +lemma QQ1: + shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []" + apply(simp) + apply(simp add: bsimp_idem) + done + +lemma QQ2: + shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]" + apply(simp) + done + +lemma XXX2a_long: + assumes "good a" + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + using assms + apply(induct a arbitrary: c taking: asize rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply(simp) + apply(auto)[1] +apply(case_tac "x42 = AZERO") + apply(simp) + apply(case_tac "x43 = AZERO") + apply(simp) + using test2 apply force + apply(case_tac "\bs. x42 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ1) + apply(simp) + using b3 apply force + using bsimp_ASEQ0 test2 apply force + thm good_SEQ test2 + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + apply(case_tac "x42 = AZERO") + apply(simp) + apply(case_tac "x43 = AZERO") + apply(simp) + apply (simp add: bsimp_ASEQ0) + apply(case_tac "\bs. x42 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ1) + apply(simp) + using bsimp_ASEQ0 test2 apply force + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + (* AALTs case *) + apply(simp) + using test2 by fastforce + +lemma XXX2a_long_without_good: + assumes "a = AALTs bs0 [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]" + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + "bsimp (bder c (bsimp a)) = XXX" + "bsimp (bder c a) = YYY" + using assms + apply(simp) + using assms + apply(simp) + prefer 2 + using assms + apply(simp) + oops + +lemma bder_bsimp_AALTs: + shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)" + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(simp) + apply(simp) + apply (simp add: bder_fuse) + apply(simp) + done + +lemma flts_nothing: + assumes "\r \ set rs. r \ AZERO" "\r \ set rs. nonalt r" + shows "flts rs = rs" + using assms + apply(induct rs rule: flts.induct) + apply(auto) + done + +lemma flts_flts: + assumes "\r \ set rs. good r" + shows "flts (flts rs) = flts rs" + using assms + apply(induct rs taking: "\rs. sum_list (map asize rs)" rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(case_tac a) + apply(simp_all add: bder_fuse flts_append) + apply(subgoal_tac "\r \ set x52. r \ AZERO") + prefer 2 + apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2) + apply(subgoal_tac "\r \ set x52. nonalt r") + prefer 2 + apply (metis n0 nn1b test2) + by (metis flts_fuse flts_nothing) + + +lemma PP: + assumes "bnullable (bders r s)" + shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)" + using assms + apply(induct s arbitrary: r) + apply(simp) + using bmkeps_simp apply auto[1] + apply(simp add: bders_append bders_simp_append) + oops + +lemma PP: + assumes "bnullable (bders r s)" + shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)" + using assms + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + using bmkeps_simp apply auto[1] + apply(simp add: bders_append bders_simp_append) + apply(drule_tac x="bder a (bsimp r)" in meta_spec) + apply(drule_tac meta_mp) + defer + oops + + +lemma + assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]" + shows "bsimp a = a" + using assms + apply(simp) + oops + + +lemma iii: + assumes "bsimp_AALTs bs rs \ AZERO" + shows "rs \ []" + using assms + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(auto) + done + +lemma CT1_SEQ: + shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))" + apply(simp add: bsimp_idem) + done + +lemma CT1: + shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map bsimp as))" + apply(induct as arbitrary: bs) + apply(simp) + apply(simp) + by (simp add: bsimp_idem comp_def) + +lemma CT1a: + shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))" + by (metis CT1 list.simps(8) list.simps(9)) + +lemma WWW2: + shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) = + bsimp_AALTs bs1 (flts (map bsimp as1))" + by (metis bsimp.simps(2) bsimp_idem) + +lemma CT1b: + shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))" + apply(induct bs as rule: bsimp_AALTs.induct) + apply(auto simp add: bsimp_idem) + apply (simp add: bsimp_fuse bsimp_idem) + by (metis bsimp_idem comp_apply) + + + + +(* CT *) + +lemma CTU: + shows "bsimp_AALTs bs as = li bs as" + apply(induct bs as rule: li.induct) + apply(auto) + done + +find_theorems "bder _ (bsimp_AALTs _ _)" + +lemma CTa: + assumes "\r \ set as. nonalt r \ r \ AZERO" + shows "flts as = as" + using assms + apply(induct as) + apply(simp) + apply(case_tac as) + apply(simp) + apply (simp add: k0b) + using flts_nothing by auto + +lemma CT0: + assumes "\r \ set as1. nonalt r \ r \ AZERO" + shows "flts [bsimp_AALTs bs1 as1] = flts (map (fuse bs1) as1)" + using assms CTa + apply(induct as1 arbitrary: bs1) + apply(simp) + apply(simp) + apply(case_tac as1) + apply(simp) + apply(simp) +proof - +fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list" + assume a1: "nonalt a \ a \ AZERO \ nonalt aa \ aa \ AZERO \ (\r\set list. nonalt r \ r \ AZERO)" + assume a2: "\as. \r\set as. nonalt r \ r \ AZERO \ flts as = as" + assume a3: "as1a = aa # list" + have "flts [a] = [a]" +using a1 k0b by blast +then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)" + using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9)) +qed + + +lemma CT01: + assumes "\r \ set as1. nonalt r \ r \ AZERO" "\r \ set as2. nonalt r \ r \ AZERO" + shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] = flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))" + using assms CT0 + by (metis k0 k00) + + + +lemma CT_exp: + assumes "\a \ set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)" + shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))" + using assms + apply(induct as) + apply(auto) + done + +lemma asize_set: + assumes "a \ set as" + shows "asize a < Suc (sum_list (map asize as))" + using assms + apply(induct as arbitrary: a) + apply(auto) + using le_add2 le_less_trans not_less_eq by blast + + +lemma XXX2a_long_without_good: + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + apply(induct a arbitrary: c taking: "\a. asize a" rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + (* AALT case *) + prefer 2 + apply(simp del: bsimp.simps) + apply(subst (2) CT1) + apply(subst CT_exp) + apply(auto)[1] + using asize_set apply blast + apply(subst CT1[symmetric]) + apply(simp) + oops + +lemma YY: + assumes "flts (map bsimp as1) = xs" + shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs" + using assms + apply(induct as1 arbitrary: bs1 xs) + apply(simp) + apply(auto) + by (metis bsimp_fuse flts_fuse k0 list.simps(9)) + + +lemma flts_nonalt: + assumes "flts (map bsimp xs) = ys" + shows "\y \ set ys. nonalt y" + using assms + apply(induct xs arbitrary: ys) + apply(auto) + apply(case_tac xs) + apply(auto) + using flts2 good1 apply fastforce + by (smt ex_map_conv list.simps(9) nn1b nn1c) + + +lemma WWW3: + shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] = + flts (map bsimp (map (fuse bs1) as1))" + by (metis CT0 YY flts_nonalt flts_nothing qqq1) + +lemma WWW4: + shows "map (bder c \ fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)" + apply(induct as1) + apply(auto) + using bder_fuse by blast + +lemma WWW5: + shows "map (bsimp \ bder c) as1 = map bsimp (map (bder c) as1)" + apply(induct as1) + apply(auto) + done + +lemma WWW6: + shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) ) ) = + bsimp(bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) " + using bder_bsimp_AALTs by auto + +lemma WWW7: + shows "bsimp (bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) = + bsimp(bsimp_AALTs x51 (flts (map (bder c) [bsimp a1, bsimp a2])))" + sorry + + +lemma stupid: + assumes "a = b" + shows "bsimp(a) = bsimp(b)" + using assms + apply(auto) + done +(* +proving idea: +bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = bsimp_AALTs x51 (map (bder c) (flts [a1]++[a2])) += bsimp_AALTs x51 (map (bder c) ((flts [a1])++(flts [a2]))) = +bsimp_AALTs x51 (map (bder c) (flts [a1]))++(map (bder c) (flts [a2])) = A +and then want to prove that +map (bder c) (flts [a]) = flts [bder c a] under the condition +that a is either a seq with the first elem being not nullable, or a character equal to c, +or an AALTs, or a star +Then, A = bsimp_AALTs x51 (flts [bder c a]) ++ (map (bder c) (flts [a2])) = A1 +Using the same condition for a2, we get +A1 = bsimp_AALTs x51 (flts [bder c a1]) ++ (flts [bder c a2]) +=bsimp_AALTs x51 flts ([bder c a1] ++ [bder c a2]) +=bsimp_AALTs x51 flts ([bder c a1, bder c a2]) + *) +lemma manipulate_flts: + shows "bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = +bsimp_AALTs x51 ((map (bder c) (flts [a1])) @ (map (bder c) (flts [a2])))" + by (metis k0 map_append) + +lemma go_inside_flts: + assumes " (bder c a1 \ AZERO) " + "\(\ a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \ bnullable(a01) ) )" +shows "map (bder c) (flts [a1]) = flts [bder c a1]" + using assms + apply - + apply(case_tac a1) + apply(simp) + apply(simp) + apply(case_tac "x32 = c") + prefer 2 + apply(simp) + apply(simp) + apply(simp) + apply (simp add: WWW4) + apply(simp add: bder_fuse) + done + +lemma medium010: + assumes " (bder c a1 = AZERO) " + shows "map (bder c) (flts [a1]) = [AZERO] \ map (bder c) (flts [a1]) = []" + using assms + apply - + apply(case_tac a1) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + done + +lemma medium011: + assumes " (bder c a1 = AZERO) " + shows "flts (map (bder c) [a1, a2]) = flts [bder c a2]" + using assms + apply - + apply(simp) + done + +lemma medium01central: + shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [a2])) ) = bsimp(bsimp_AALTs x51 (flts [bder c a2]))" + sorry + + +lemma plus_bsimp: + assumes "bsimp( bsimp a) = bsimp (bsimp b)" + shows "bsimp a = bsimp b" + using assms + apply - + by (simp add: bsimp_idem) +lemma patience_good5: + assumes "bsimp r = AALTs x y" + shows " \ a aa list. y = a#aa#list" + by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a) + +(*SAD*) +(*this does not hold actually +lemma bsimp_equiv0: + shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))" + apply(simp) + apply(case_tac "bsimp r") + apply(simp) + apply(simp) + apply(simp) + apply(simp) + thm good1 + using good1 + apply - + apply(drule_tac x="r" in meta_spec) + apply(erule disjE) + + apply(simp only: bsimp_AALTs.simps) + apply(simp only:flts.simps) + apply(drule patience_good5) + apply(clarify) + apply(subst bsimp_AALTs_qq) + apply simp + prefer 2 + sorry*) + +(*exercise: try multiple ways of proving this*) +(*this lemma does not hold......... +lemma bsimp_equiv1: + shows "bsimp r = bsimp (AALTs [] [r])" + using plus_bsimp + apply - + using bsimp_equiv0 by blast + (*apply(simp) + apply(case_tac "bsimp r") + apply(simp) + apply(simp) + apply(simp) + apply(simp) +(*use lemma good1*) + thm good1 + using good1 + apply - + apply(drule_tac x="r" in meta_spec) + apply(erule disjE) + + apply(subst flts_single1) + apply(simp only: bsimp_AALTs.simps) + prefer 2 + + thm flts_single1 + + find_theorems "flts _ = _"*) +*) +lemma bsimp_equiv2: + shows "bsimp (AALTs x51 [r]) = bsimp (AALT x51 AZERO r)" + sorry + +lemma medium_stupid_isabelle: + assumes "rs = a # list" + shows "bsimp_AALTs x51 (AZERO # rs) = AALTs x51 (AZERO#rs)" + using assms + apply - + apply(simp) + done +(* +lemma mediumlittle: + shows "bsimp(bsimp_AALTs x51 rs) = bsimp(bsimp_AALTs x51 (AZERO # rs))" + apply(case_tac rs) + apply(simp) + apply(case_tac list) + apply(subst medium_stupid_isabelle) + apply(simp) + prefer 2 + apply simp + apply(rule_tac s="a#list" and t="rs" in subst) + apply(simp) + apply(rule_tac t="list" and s= "[]" in subst) + apply(simp) + (*dunno what is the rule for x#nil = x*) + apply(case_tac a) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply simp + apply(simp only:bsimp_AALTs.simps) + + apply simp + apply(case_tac "bsimp x42") + apply(simp) + apply simp + apply(case_tac "bsimp x43") + apply simp + apply simp + apply simp + apply simp + apply(simp only:bsimp_ASEQ.simps) + using good1 + apply - + apply(drule_tac x="x43" in meta_spec) + apply(erule disjE) + apply(subst bsimp_AALTs_qq) + using patience_good5 apply force + apply(simp only:bsimp_AALTs.simps) + apply(simp only:fuse.simps) + apply(simp only:flts.simps) +(*OK from here you actually realize this lemma doesnt hold*) + apply(simp) + apply(simp) + apply(rule_tac t="rs" and s="a#list" in subst) + apply(simp) + apply(rule_tac t="list" and s="[]" in subst) + apply(simp) + (*apply(simp only:bsimp_AALTs.simps)*) + (*apply(simp only:fuse.simps)*) + sorry +*) +lemma singleton_list_map: + shows"map f [a] = [f a]" + apply simp + done +lemma map_application2: + shows"map f [a,b] = [f a, f b]" + apply simp + done +(*SAD*) +(* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) = + bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*) +(*This equality does not hold*) +lemma medium01: + assumes " (bder c a1 = AZERO) " + shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [ a1, a2]))) = + bsimp(bsimp_AALTs x51 (flts (map (bder c) [ a1, a2])))" + apply(subst manipulate_flts) + using assms + apply - + apply(subst medium011) + apply(simp) + apply(case_tac "map (bder c) (flts [a1]) = []") + apply(simp) + using medium01central apply blast +apply(frule medium010) + apply(erule disjE) + prefer 2 + apply(simp) + apply(simp) + apply(case_tac a2) + apply simp + apply simp + apply simp + apply(simp only:flts.simps) +(*HOW do i say here to replace ASEQ ..... back into a2*) +(*how do i say here to use the definition of map function +without lemma, of course*) +(*how do i say here that AZERO#map (bder c) [ASEQ x41 x42 x43]'s list.len >1 +without a lemma, of course*) + apply(subst singleton_list_map) + apply(simp only: bsimp_AALTs.simps) + apply(case_tac "bder c (ASEQ x41 x42 x43)") + apply simp + apply simp + apply simp + prefer 3 + apply simp + apply(rule_tac t="bder c (ASEQ x41 x42 x43)" +and s="ASEQ x41a x42a x43a" in subst) + apply simp + apply(simp only: flts.simps) + apply(simp only: bsimp_AALTs.simps) + apply(simp only: fuse.simps) + apply(subst (2) bsimp_idem[symmetric]) + apply(subst (1) bsimp_idem[symmetric]) + apply(simp only:bsimp.simps) + apply(subst map_application2) + apply(simp only: bsimp.simps) + apply(simp only:flts.simps) +(*want to happily change between a2 and ASEQ x41 42 43, and eliminate now +redundant conditions such as map (bder c) (flts [a1]) = [AZERO] *) + apply(case_tac "bsimp x42a") + apply(simp) + apply(case_tac "bsimp x43a") + apply(simp) + apply(simp) + apply(simp) + apply(simp) + prefer 2 + apply(simp) + apply(rule_tac t="bsimp x43a" +and s="AALTs x51a x52" in subst) + apply simp + apply(simp only:bsimp_ASEQ.simps) + apply(simp only:fuse.simps) + apply(simp only:flts.simps) + + using medium01central mediumlittle by auto + + + +lemma medium1: + assumes " (bder c a1 \ AZERO) " + "\(\ a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \ bnullable(a01) ) )" +" (bder c a2 \ AZERO)" + "\(\ a11 a12 x12. ( (a2 = ASEQ x12 a11 a12) \ bnullable(a11) ) )" + shows "bsimp_AALTs x51 (map (bder c) (flts [ a1, a2])) = + bsimp_AALTs x51 (flts (map (bder c) [ a1, a2]))" + using assms + apply - + apply(subst manipulate_flts) + apply(case_tac "a1") + apply(simp) + apply(simp) + apply(case_tac "x32 = c") + prefer 2 + apply(simp) + prefer 2 + apply(case_tac "bnullable x42") + apply(simp) + apply(simp) + + apply(case_tac "a2") + apply(simp) + apply(simp) + apply(case_tac "x32 = c") + prefer 2 + apply(simp) + apply(simp) + apply(case_tac "bnullable x42a") + apply(simp) + apply(subst go_inside_flts) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + apply (simp add: WWW4) + apply(simp) + apply (simp add: WWW4) + apply (simp add: go_inside_flts) + apply (metis (no_types, lifting) go_inside_flts k0 list.simps(8) list.simps(9)) + by (smt bder.simps(6) flts.simps(1) flts.simps(6) flts.simps(7) go_inside_flts k0 list.inject list.simps(9)) + +lemma big0: + shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = + bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" + by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) + +lemma bignA: + shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) = + bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))" + apply(simp) + apply(subst k0) + apply(subst WWW3) + apply(simp add: flts_append) + done + +lemma XXX2a_long_without_good: + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + apply(induct a arbitrary: c taking: "\a. asize a" rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + (* SEQ case *) + apply(simp only:) + apply(subst CT1_SEQ) + apply(simp only: bsimp.simps) + + (* AALT case *) + prefer 2 + apply(simp only:) + apply(case_tac "\a1 a2. x52 = [a1, a2]") + apply(clarify) + apply(simp del: bsimp.simps) + apply(subst (2) CT1) + apply(simp del: bsimp.simps) + apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst) + apply(simp del: bsimp.simps) + apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst) + apply(simp del: bsimp.simps) + apply(subst CT1a[symmetric]) + (* \ *) + apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))" + and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst) + apply(simp) + apply(subst bsimp.simps) + apply(simp del: bsimp.simps bder.simps) + + apply(subst bder_bsimp_AALTs) + apply(subst bsimp.simps) + apply(subst WWW2[symmetric]) + apply(subst bsimp_AALTs_qq) + defer + apply(subst bsimp.simps) + + (* <- *) + apply(subst bsimp.simps) + apply(simp del: bsimp.simps) +(*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = + bsimp_AALTs x51 (flts (map (bder c) [a1, a2]))*) + apply(case_tac "\bs1 as1. bsimp a1 = AALTs bs1 as1") + apply(case_tac "\bs2 as2. bsimp a2 = AALTs bs2 as2") + apply(clarify) + apply(simp only:) + apply(simp del: bsimp.simps bder.simps) + apply(subst bsimp_AALTs_qq) + prefer 2 + apply(simp del: bsimp.simps) + apply(subst big0) + apply(simp add: WWW4) + apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq) + oops + +lemma XXX2a_long_without_good: + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + apply(induct a arbitrary: c taking: "\a. asize a" rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + (* AALT case *) + prefer 2 + apply(subgoal_tac "nonnested (bsimp x)") + prefer 2 + using nn1b apply blast + apply(simp only:) + apply(drule_tac x="AALTs x51 (flts x52)" in spec) + apply(drule mp) + defer + apply(drule_tac x="c" in spec) + apply(simp) + apply(rotate_tac 2) + + apply(drule sym) + apply(simp) + + apply(simp only: bder.simps) + apply(simp only: bsimp.simps) + apply(subst bder_bsimp_AALTs) + apply(case_tac x52) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + apply(case_tac a) + apply(simp) + apply(simp) + apply(simp) + defer + apply(simp) + + + (* case AALTs list is not empty *) + apply(simp) + apply(subst k0) + apply(subst (2) k0) + apply(simp) + apply(case_tac "bsimp a = AZERO") + apply(subgoal_tac "bsimp (bder c a) = AZERO") + prefer 2 + using less_iff_Suc_add apply auto[1] + apply(simp) + apply(drule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(drule_tac x="c" in spec) + apply(simp add: bder_bsimp_AALTs) + apply(case_tac "nonalt (bsimp a)") + prefer 2 + apply(drule_tac x="bsimp (AALTs x51 (a#list))" in spec) + apply(drule mp) + apply(rule order_class.order.strict_trans2) + apply(rule bsimp_AALTs_size3) + apply(auto)[1] + apply(simp) + apply(subst (asm) bsimp_idem) + apply(drule_tac x="c" in spec) + apply(simp) + find_theorems "_ < _ \ _ \ _ \_ < _" + apply(rule le_trans) + apply(subgoal_tac "flts [bsimp a] = [bsimp a]") + prefer 2 + using k0b apply blast + apply(simp) + find_theorems "asize _ < asize _" + + using bder_bsimp_AALTs + apply(case_tac list) + apply(simp) + sledgeha mmer [timeout=6000] + + apply(case_tac "\r \ set (map bsimp x52). \nonalt r") + apply(drule_tac x="bsimp (AALTs x51 x52)" in spec) + apply(drule mp) + using bsimp_AALTs_size3 apply blast + apply(drule_tac x="c" in spec) + apply(subst (asm) (2) test) + + apply(case_tac x52) + apply(simp) + apply(simp) + apply(case_tac "bsimp a = AZERO") + apply(simp) + apply(subgoal_tac "bsimp (bder c a) = AZERO") + prefer 2 + apply auto[1] + apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2) + apply(simp) + apply(drule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(simp) + apply(case_tac list) + prefer 2 + apply(simp) + apply(case_tac "bsimp aa = AZERO") + apply(simp) + apply(subgoal_tac "bsimp (bder c aa) = AZERO") + prefer 2 + apply auto[1] + apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1) + apply(simp) + apply(drule_tac x="AALTs x51 (a#lista)" in spec) + apply(drule mp) + apply(simp add: asize0) + apply(simp) + apply (metis flts.simps(2) k0) + apply(subst k0) + apply(subst (2) k0) + + + using less_add_Suc1 apply fastforce + apply(subst k0) + + + apply(simp) + apply(case_tac "bsimp a = AZERO") + apply(simp) + apply(subgoal_tac "bsimp (bder c a) = AZERO") + prefer 2 + apply auto[1] + apply(simp) + apply(case_tac "nonalt (bsimp a)") + apply(subst bsimp_AALTs1) + apply(simp) + using less_add_Suc1 apply fastforce + + apply(subst bsimp_AALTs1) + + using nn11a apply b last + + (* SEQ case *) + apply(clarify) + apply(subst bsimp.simps) + apply(simp del: bsimp.simps) + apply(auto simp del: bsimp.simps)[1] + apply(subgoal_tac "bsimp x42 \ AZERO") + prefer 2 + using b3 apply force + apply(case_tac "bsimp x43 = AZERO") + apply(simp) + apply (simp add: bsimp_ASEQ0) + apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2) + apply(case_tac "\bs. bsimp x42 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ2) + apply(subgoal_tac "bsimp (bder c x42) = AZERO") + prefer 2 + using less_add_Suc1 apply fastforce + apply(simp) + apply(frule_tac x="x43" in spec) + apply(drule mp) + apply(simp) + apply(drule_tac x="c" in spec) + apply(subst bder_fuse) + apply(subst bsimp_fuse[symmetric]) + apply(simp) + apply(subgoal_tac "bmkeps x42 = bs") + prefer 2 + apply (simp add: bmkeps_simp) + apply(simp) + apply(subst bsimp_fuse[symmetric]) + apply(case_tac "nonalt (bsimp (bder c x43))") + apply(subst bsimp_AALTs1) + using nn11a apply blast + using fuse_append apply blast + apply(subgoal_tac "\bs rs. bsimp (bder c x43) = AALTs bs rs") + prefer 2 + using bbbbs1 apply blast + apply(clarify) + apply(simp) + apply(case_tac rs) + apply(simp) + apply (metis arexp.distinct(7) good.simps(4) good1) + apply(simp) + apply(case_tac list) + apply(simp) + apply (metis arexp.distinct(7) good.simps(5) good1) + apply(simp del: bsimp_AALTs.simps) + apply(simp only: bsimp_AALTs.simps) + apply(simp) + + + + +(* HERE *) +apply(case_tac "x42 = AZERO") + apply(simp) + apply(case_tac "bsimp x43 = AZERO") + apply(simp) + apply (simp add: bsimp_ASEQ0) + apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO") + apply(simp) + apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2) + apply(case_tac "\bs. bsimp x42 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ2) + apply(subgoal_tac "bsimp (bder c x42) = AZERO") + apply(simp) + prefer 2 + using less_add_Suc1 apply fastforce + apply(subgoal_tac "bmkeps x42 = bs") + prefer 2 + apply (simp add: bmkeps_simp) + apply(simp) + apply(case_tac "nonalt (bsimp (bder c x43))") + apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a) + apply(subgoal_tac "nonnested (bsimp (bder c x43))") + prefer 2 + using nn1b apply blast + apply(case_tac x43) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6)) + apply(simp) + apply(auto)[1] + apply(case_tac "(bsimp (bder c x42a)) = AZERO") + apply(simp) + + apply(simp) + + + + apply(subgoal_tac "(\bs1 rs1. 1 < length rs1 \ bsimp (bder c x43) = AALTs bs1 rs1 ) \ + (\bs1 r. bsimp (bder c x43) = fuse bs1 r)") + prefer 2 + apply (metis fuse_empty) + apply(erule disjE) + prefer 2 + apply(clarify) + apply(simp only:) + apply(simp) + apply(simp add: fuse_append) + apply(subst bder_fuse) + apply(subst bsimp_fuse[symmetric]) + apply(subst bder_fuse) + apply(subst bsimp_fuse[symmetric]) + apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)") + prefer 2 + using less_add_Suc2 apply bl ast + apply(simp only: ) + apply(subst bsimp_fuse[symmetric]) + apply(simp only: ) + + apply(simp only: fuse.simps) + apply(simp) + apply(case_tac rs1) + apply(simp) + apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse) + apply(simp) + apply(case_tac list) + apply(simp) + apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse) + apply(simp only: bsimp_AALTs.simps map_cons.simps) + apply(auto)[1] + + + + apply(subst bsimp_fuse[symmetric]) + apply(subgoal_tac "bmkeps x42 = bs") + prefer 2 + apply (simp add: bmkeps_simp) + + + apply(simp) + + using b3 apply force + using bsimp_ASEQ0 test2 apply fo rce + thm good_SEQ test2 + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + apply(case_tac "x42 = AZERO") + apply(simp) + apply(case_tac "x43 = AZERO") + apply(simp) + apply (simp add: bsimp_ASEQ0) + apply(case_tac "\bs. x42 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ1) + apply(simp) + using bsimp_ASEQ0 test2 apply fo rce + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + apply (simp add: good_SEQ test2) + (* AALTs case *) + apply(simp) + using test2 by fa st force + + +lemma XXX4ab: + shows "good (bders_simp (bsimp r) s) \ bders_simp (bsimp r) s = AZERO" + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply (simp add: good1) + apply(simp add: bders_simp_append) + apply (simp add: good1) + done + +lemma XXX4: + assumes "good a" + shows "bders_simp a s = bsimp (bders a s)" + using assms + apply(induct s arbitrary: a rule: rev_induct) + apply(simp) + apply (simp add: test2) + apply(simp add: bders_append bders_simp_append) + oops + + +lemma MAINMAIN: + "blexer r s = blexer_simp r s" + apply(induct s arbitrary: r) + apply(simp add: blexer_def blexer_simp_def) + apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps) + apply(auto simp del: bders.simps bders_simp.simps) + prefer 2 + apply (metis b4 bders.simps(2) bders_simp.simps(2)) + prefer 2 + apply (metis b4 bders.simps(2)) + apply(subst bmkeps_simp) + apply(simp) + apply(case_tac s) + apply(simp only: bders.simps) + apply(subst bders_simp.simps) + apply(simp) + oops + + +lemma + fixes n :: nat + shows "(\i \ {0..n}. i) = n * (n + 1) div 2" + apply(induct n) + apply(simp) + apply(simp) + done + + + + + +end \ No newline at end of file