# HG changeset patch # User Christian Urban # Date 1564399948 -3600 # Node ID c470f792022be4b16bbd43ccd3c37e4ca8863a3b # Parent 89e6605c4ca41c9ae734694cfd6255b0beb676ec checkpoint diff -r 89e6605c4ca4 -r c470f792022b thys/BitCoded.thy --- a/thys/BitCoded.thy Mon Jul 29 09:37:20 2019 +0100 +++ b/thys/BitCoded.thy Mon Jul 29 12:32:28 2019 +0100 @@ -2057,7 +2057,7 @@ 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)" @@ -2109,8 +2109,7 @@ prefer 2 apply(simp) - defer - apply(simp only: bnullable.simps) + defer oops lemma L06_2: @@ -2135,19 +2134,9 @@ using L_bsimp_erase L_flat_Prf apply(auto)[1] done - - -lemma LXX_bders: - assumes "" - shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" - using assms - apply(induct s arbitrary: a rule: rev_induct) - apply(simp add: bmkeps_simp) - apply(simp add: bders_append) - -lemma L07: +lemma L07XX: assumes "s \ L (erase a)" shows "s \ erase a \ flex (erase a) id s (mkeps (ders s (erase a)))" using assms @@ -2169,7 +2158,7 @@ apply(induct s arbitrary: a) apply(simp) using L0 apply auto[1] - apply(simp) + oops thm bmkeps_retrieve bmkeps_simp Posix_mkeps @@ -2177,7 +2166,7 @@ assumes "s \ L (der c r)" shows "s \ der c r \ mkeps (ders s (der c r))" using assms - sorry + oops lemma L02_bsimp: assumes "bnullable (bders a s)" @@ -2201,229 +2190,8 @@ apply(simp only: erase_bder[symmetric] erase_bders[symmetric]) apply(subst LB_sym[symmetric]) apply(simp) - apply(rule WQ1) - apply(simp only: erase_bder[symmetric]) - apply(rule L07) - apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder erase_bders lexer_correct_None lexer_flex option.simps(3)) - - apply(simp) - (*sledgehammer [timeout = 6000]*) - - - using bder_retrieve - - - -lemma LX0MAIN: - assumes "s \ r \ v" - shows "decode (bmkeps (bders_simp (intern r) s)) r = Some(flex r id s v)" - using assms - apply(induct s arbitrary: r v) - apply(simp) - apply (metis LX0 Posix1(1) bders.simps(1) lexer_correctness(1) lexer_flex option.simps(3)) - apply(simp add: bders_simp_append ders_append flex_append) - apply(subst bmkeps_simp[symmetric]) - apply (met is L_bders_simp Posix1(1) bnullable_correctness der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) - (*apply(subgoal_tac "v = flex r id xs (injval (ders xs r) x (mkeps (ders (xs @ [x]) r)))") - prefer 2 - apply (metis Posix1(1) flex.simps(1) flex.simps(2) flex_append lexer_correct_None lexer_correctness(1) lexer_flex option.inject) -*) apply(drule_tac x="r" in meta_spec) - apply(drule_tac x="(mkeps (ders xs r))" in meta_spec) - apply(drule meta_mp) - - defer - apply(simp) - apply(drule sym) - apply(simp) - using bder_retrieve MAIN_decode oops -lemma LXaa: - assumes "s \ L (erase a)" - shows "decode (bmkeps (bsimp (bders (bsimp a) s))) (erase a) = decode (bmkeps (bders a s)) (erase a)" - using assms - apply(induct s arbitrary: a) - apply(simp) - using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1] - apply(simp) - apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec) - apply(drule meta_mp) - apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) - apply(subst (asm) bsimp_idem) - apply(subst bmkeps_simp[symmetric]) - apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness) - apply(subst (asm) bmkeps_simp[symmetric]) - apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness) - apply(subst bmkeps_retrieve) - apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) nullable_correctness) - apply(subst LA) - apply(simp) - apply (metis L_bsimp_erase ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable) - - - -lemma LXaa: - assumes "s \ L (erase a)" - shows "bmkeps (bsimp (bders (bsimp a) s)) = bmkeps (bders a s)" - using assms - apply(induct s arbitrary: a) - apply(simp) - using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1] - apply(simp) - apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec) - apply(drule meta_mp) - apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) - apply(subst (asm) bsimp_idem) - apply(subst bmkeps_simp[symmetric]) - apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness) - apply(subst (asm) bmkeps_simp[symmetric]) - apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness) - - -lemma LXaa: - assumes "s \ L (erase a)" - shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" - using assms - apply(induct s arbitrary: a) - apply(simp) - using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1] - apply(simp) - apply(drule_tac x="bder a aa" 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) - (* transformation to retrieve *) - apply(subst bmkeps_retrieve) - apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) ders_correctness erase_bders nullable_correctness) - apply(subst bmkeps_retrieve) - apply (metis b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer_correct_None lexer_flex) - apply(subst (2) LC[symmetric]) - prefer 2 - apply(subst L0) - apply(subst LA) - apply(simp) - apply (m etis L_bsimp_erase bders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable) - apply(subst LA) - apply(simp) - apply (m etis L0aa b3 b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer.simps(1) lexer_correctness(2) mkeps_nullable) - apply(subst (2) LB_sym[symmetric]) - prefer 2 - apply(subst L0) - apply(simp) - using lexer_correct_None lexer_flex apply fastforce - apply(subst (asm) bmkeps_retrieve) - apply (metis L_bsimp_erase bders.simps(2) erase_bders lexer_correct_None lexer_flex) - apply(subst (asm) bmkeps_retrieve) - apply (metis L0aa L_bsimp_erase b3 b4 bders_simp.simps(2) bnullable_correctness lexer.simps(1) lexer_correctness(2)) - apply(subst LA) - apply (met is 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 L0aaaa LB[OF L0aaaa] - apply(subst LB[OF L0aaaa]) - using L0aaaa - apply(rule L0aaaa) - - - - - - - - -lemma L00: - assumes "s \ L (erase a)" - shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = - retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))" - using assms - apply(induct s arbitrary: a taking: length rule: measure_induct) - apply(case_tac x) - apply(simp) - using L0 b3 bnullable_correctness nullable_correctness apply blast - apply(simp) - apply(drule_tac x="[]" in spec) - apply(simp) - apply(drule_tac x="bders (bsimp a) (aa#list)" in spec) - apply(simp) - apply(drule mp) - apply (metis L_bsimp_erase ders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness) - using bder_retrieve bmkeps_simp bmkeps_retrieve L0 LA LB LC L02 L03 L04 L05 - - oops - -lemma L00: - assumes "s \ L (erase (bsimp a))" - shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = - retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))" - using assms - apply(induct s arbitrary: a) - apply(simp) - using L0 b3 bnullable_correctness nullable_correctness apply blast - apply(simp add: flex_append) - apply(drule_tac x="bder a aa" in meta_spec) - apply(drule meta_mp) - apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) - apply(simp) - - (*using bmkeps_retrieve bder_retrieve*) - apply(subst (asm) bder_retrieve) - apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex) - apply(simp add: flex_fun_apply) - apply(drule sym) - apply(simp) - using bmkeps_retrieve bder_retrieve - oops - -lemma L0a: - assumes "s \ L (erase a)" - shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = - retrieve (bders a s) (mkeps (erase (bders a s)))" - using assms - apply(induct s arbitrary: a) - apply(simp) - apply(simp) - apply(drule_tac x="bsimp (bder a aa)" in meta_spec) - apply(drule meta_mp) - using L_bsimp_erase lexer_correct_None apply fastforce - apply(simp) - apply(subst LA) - apply (metis L_bsimp_erase ders.simps(2) ders_correctness erase_bder lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) - apply(subst LA) - apply(simp) - apply (metis ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable) - - apply(simp) - (* MAIN *) - - apply(subst L00) - apply (met is L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) - apply(simp) - done - -lemma L0a: - assumes "s \ L (erase a)" - shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = - retrieve (bders a s) (mkeps (erase (bders a s)))" - using assms - apply(induct s arbitrary: a rule: rev_induct) - apply(simp) - apply(simp add: bders_simp_append) - apply(subst L0) - apply (metis L_bders_simp bnullable_correctness der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness) - apply(subst bder_retrieve) - apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) - apply(simp add: bders_append) - apply(subst bder_retrieve) - apply (metis ders_snoc erase_bders lexer_correct_None lexer_flex mkeps_nullable) - apply(simp add: ders_append) - using bder_retrieve - - find_theorems "retrieve _ (injval _ _ _)" -find_theorems "mkeps (erase _)" - - lemma L1: assumes "s \ r \ v" shows "decode (bmkeps (bders (intern r) s)) r = Some v" @@ -2467,178 +2235,6 @@ apply(simp add: flex_append) by (simp add: Posix_injval) -lemma L4: - assumes "[c] \ r \ v" - shows "bmkeps (bder c (bsimp (intern r))) = code (flex r id [c] v)" - using assms - apply(subst bmkeps_retrieve) - apply (metis L_bsimp_erase Posix1(1) bders.simps(1) bders.simps(2) erase_bders erase_intern lexer_correct_None lexer_flex) - apply(subst bder_retrieve) - apply (metis L_bsimp_erase Posix1(1) bders.simps(1) bders.simps(2) erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable) - apply(simp) - - - - - -lemma - assumes "s \ L r" - shows "bmkeps (bders_simp (intern r) s) = bmkeps (bders (intern r) s)" - using assms - apply(induct s arbitrary: r rule: rev_induct) - apply(simp) - apply(simp add: bders_simp_append bders_append) - apply(subst bmkeps_simp[symmetric]) - apply (metis b4 bders.simps(1) bders.simps(2) bders_simp_append blexer_correctness blexer_def lexer_correct_None) - apply(subst bmkeps_retrieve) - apply(simp) - apply (metis L_bders_simp der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) - apply(subst bmkeps_retrieve) - apply(simp) - apply (metis ders_snoc lexer_correct_None lexer_flex) - apply(subst bder_retrieve) - apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) - apply(subst bder_retrieve) - apply (metis ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable) - using bmkeps_retrieve - find_theorems "retrieve (bders _ _) = _" - find_theorems "retrieve _ _ = _" - oops - -lemma - assumes "s \ r \ v" - shows "decode (bmkeps (bders_simp (intern r) s)) = Some v" - using assms - apply(induct s arbitrary: r v taking: length rule: measure_induct) - apply(subgoal_tac "x = [] \ (\a xs. x = xs @ [a])") - prefer 2 - apply (meson rev_exhaust) - apply(erule disjE) - apply(simp add: blexer_simp_def) - apply (metis Posix1(1) Posix_Prf Posix_determ Posix_mkeps bmkeps_retrieve erase_intern lexer.simps(1) lexer_correct_None retrieve_code) - apply(clarify) - apply(simp add: bders_simp_append) - apply(subst bmkeps_simp[symmetric]) - apply (metis b3 b4 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def lexer_correctness(1) option.distinct(1)) - apply(subst bmkeps_retrieve) - apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) - apply(simp) - apply(subst bder_retrieve) - apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) - - - find_theorems "bmkeps _ = _" - - apply(subgoal_tac "lexer r (xs @ [a]) = Some v") - prefer 2 - using lexer_correctness(1) apply blast - apply(simp (no_asm_simp) add: bders_simp_append) - apply(subst bmkeps_simp[symmetric]) - apply (m etis b4 bders.simps(1) bders.simps(2) bders_simp_append bnullable_correctness erase_bders erase_intern lexer_flex option.distinct(1)) - apply(subgoal_tac "nullable (ders (xs @ [a]) r)") - prefer 2 - apply (metis lexer_flex option.distinct(1)) - apply(simp add: lexer_flex) - apply(simp add: flex_append ders_append) - apply(drule_tac sym) - apply(simp) - using Posix_flex flex.simps Posix_flex2 - apply(drule_tac Posix_flex2) - apply (simp add: Prf_injval mkeps_nullable) - apply(drule_tac x="[a]" in spec) - apply(drule mp) - defer - apply(drule_tac x="ders xs r" in spec) - apply(drule_tac x="injval (ders xs r) a (mkeps (der a (ders xs r)))" in spec) - apply(simp) - apply(subst (asm) bmkeps_simp[symmetric]) - using bnullable_correctness apply fastforce - - - find_theorems "good (bsimp _)" - oops - -lemma - assumes "s \ L (erase a)" - shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" - using assms - apply(induct s arbitrary: a taking : length rule: measure_induct) - apply(case_tac x) - apply(simp) - using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1] - using bsimp_idem apply auto[1] - apply(simp add: bders_append bders_simp_append) - apply(drule_tac x="bder a (bsimp aa)" in meta_spec) - apply(drule meta_mp) - defer - apply(simp) - oops - - -lemma - assumes "s \ L (erase r)" - shows "bmkeps (bders_simp r s) = bmkeps (bders r s)" - using assms - apply(induct s arbitrary: r) - apply(simp) - apply(simp add: bders_simp_append bders_append) - apply(drule_tac x="bsimp (bder a r)" in meta_spec) - apply(drule meta_mp) - defer - apply(simp) - - find_theorems "good (bsimp _)" - oops - -lemma - assumes "s \ L r" - shows "decode (bmkeps (bders_simp (intern r) s)) r = Some (flex r id s (mkeps (ders s r)))" - using assms - apply(induct s arbitrary: r) - apply(simp) - using bmkeps_retrieve decode_code mkeps_nullable nullable_correctness retrieve_code apply auto[1] - apply(simp add: bders_simp_append) - apply(subst bmkeps_simp[symmetric]) - apply(subgoal_tac "[] \ L (ders (xs @ [x]) r)") - prefer 2 - apply (meson Posix1(1) lexer_correct_None lexer_flex nullable_correctness) - apply(simp add: ders_append) - using L_bders_simp bnullable_correctness der_correctness nullable_correctness apply f orce - apply(simp add: flex_append ders_append) - apply(drule_tac x="der x r" in meta_spec) - apply(simp add: ders_append) - find_theorems "intern _" - find_theorems "bmkeps (bsimp _)" - - find_theorems "(_ # _) \ _ \ _" - oops - - -lemma ZZZ: - assumes "\y. asize y < Suc (sum_list (map asize x52)) \ bsimp (bder c (bsimp y)) = bsimp (bder c y)" - shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \ bder c) x52))" - using assms - apply(induct x52) - apply(simp) - apply(simp) - apply(case_tac "bsimp a = AZERO") - apply(simp) - apply(subgoal_tac "bsimp (bder c a) = AZERO") - prefer 2 - using less_add_Suc1 apply fastforce - apply(simp) - apply(case_tac "\bs rs. bsimp a = AALTs bs rs") - apply(clarify) - apply(simp) - apply(subst k0) - apply(case_tac "rs = []") - apply(simp) - apply(subgoal_tac "bsimp (bder c a) = AALTs bs []") - apply(simp) - apply (metis arexp.distinct(7) good.simps(4) good1) - oops - - lemma bders_snoc: @@ -2914,25 +2510,7 @@ apply(simp) oops -lemma - assumes "rs = [AALTs bs0 [AALTs bsa [AONE bsb, AONE bsb]]]" - shows "flts [bsimp_AALTs bs (flts rs)] = flts (map (fuse bs) rs)" - using assms - apply(simp only:) - apply(simp only: flts.simps append_Nil2 List.list.map fuse.simps) - apply(simp only: bsimp_AALTs.simps) - apply(simp only: fuse.simps) - apply(simp only: flts.simps append_Nil2) - find_theorems "nonnested (bsimp_AALTs _ _)" - find_theorems "map _ (_ # _) = _" - apply(induct rs arbitrary: bs rule: flts.induct) - apply(auto) - apply(case_tac rs) - apply(simp) - - oops - find_theorems "asize (bsimp _)" lemma CT1: shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map bsimp as))" @@ -2953,7 +2531,6 @@ apply(auto) done -thm flts.simps lemma CTa: @@ -2996,17 +2573,7 @@ by (metis k0 k00) -lemma CTT: - assumes "\r\set (flts (map (bsimp \ bder c) as1)). nonalt r \ r \ AZERO" - "\r\set (flts (map (bsimp \ bder c) as2)). nonalt r \ r \ AZERO" - shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) - = XXX" - apply(subst bsimp_idem[symmetric]) - apply(simp) - apply(subst CT01) - apply(rule assms) - apply(rule assms) - (* CT *) + lemma shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) @@ -3097,57 +2664,7 @@ apply (metis (no_types, lifting) Nil_is_append_conv Nil_is_map_conv One_nat_def Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_0_conv length_append length_greater_0_conv less_Suc0 less_add_same_cancel1) apply(simp add: comp_def bder_fuse) - thm bder_fuse - - find_theorems "1 < length _" - -(* CT *) -(* - under assumption that bsimp a1 = AALT; bsimp a = AALT - - bsimp (AALT x51 (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) = - bsimp (AALTs x51 (map (fuse bs1) (map (bder c) as1)) @ ( map (fuse bs2) (map (bder c) as2))) - - bsimp_AALTs x51 (flts (map bsimp [a1, a2]))) - = bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) - -*) - - apply(case_tac "bsimp a1") - prefer 5 - apply(simp only:) - apply(case_tac "bsimp a2") - apply(simp) - - prefer 5 - apply(simp only:) - apply(simp only: bder.simps) - apply(simp) - - - - - prefer 2 - using nn1b apply blast - apply(simp only:) - apply(case_tac x52) - apply(simp) - apply(simp only:) - apply(case_tac "\bsa rsa. a = AALTs bsa rsa") - apply(clarify) - apply(simp) - apply(frule_tac x="AALTs x51 ((map (fuse bsa) rsa) @ list)" in spec) - apply(drule mp) - apply(simp) - apply (simp add: qq) - apply(drule_tac x="c" in spec) - apply(simp only: bder.simps) - apply(simp) - apply(subst k0) - apply(subst (2) k0) - apply(subst (asm) (2) flts_append) - apply(rotate_tac 2) - + oops lemma XXX2a_long_without_good: shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"