diff -r 8b0b414e71b0 -r 3b8e3a156200 thys/BitCoded.thy --- a/thys/BitCoded.thy Wed Feb 20 00:00:30 2019 +0000 +++ b/thys/BitCoded.thy Sat Feb 23 21:52:06 2019 +0000 @@ -120,6 +120,7 @@ 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" @@ -135,7 +136,7 @@ | "erase (ACHAR _ c) = CHAR c" | "erase (AALTs _ []) = ZERO" | "erase (AALTs _ [r]) = (erase r)" -| "erase (AALTs _ (r#rs)) = ALT (erase r) (erase (AALTs [] rs))" +| "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)" @@ -154,6 +155,7 @@ 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]" @@ -226,9 +228,25 @@ assumes "\ v : (erase r)" shows "retrieve (fuse bs r) v = bs @ retrieve r v" using assms - apply(induct r arbitrary: v bs rule: erase.induct) - apply(auto elim: Prf_elims)[1] - sorry + 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" @@ -243,24 +261,135 @@ using assms apply(induct v r ) apply(simp_all add: retrieve_fuse retrieve_encode_STARS) - sorry + 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(auto simp add: bnullable_correctness) - sorry - + 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) + apply(induct r arbitrary: v rule: erase.induct) apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) - sorry + apply(case_tac va) + apply(simp) + apply(auto) + by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) + lemma MAIN_decode: assumes "\ v : ders s r"