# HG changeset patch # User Christian Urban # Date 1643841041 0 # Node ID 01d1285b08ed61a7107f80ead6a4633460a7dd42 # Parent d73b722efe0e47789bc3a9e448b4f18a40b40f96# Parent 4511cc1bf1f03b95a4d8d88bf2eefbc1b9fb3d00 merged diff -r 4511cc1bf1f0 -r 01d1285b08ed thys2/SizeBound4.thy --- a/thys2/SizeBound4.thy Wed Feb 02 15:03:20 2022 +0000 +++ b/thys2/SizeBound4.thy Wed Feb 02 22:30:41 2022 +0000 @@ -561,7 +561,7 @@ | bs6: "AALTs bs [] \ AZERO" | bs7: "AALTs bs [r] \ fuse bs r" | bs8: "rs1 s\ rs2 \ AALTs bs rs1 \ AALTs bs rs2" -| ss1: "[] s\ []" +(*| ss1: "[] s\ []"*) | ss2: "rs1 s\ rs2 \ (r # rs1) s\ (r # rs2)" | ss3: "r1 \ r2 \ (r1 # rs) s\ (r2 # rs)" | ss4: "(AZERO # rs) s\ rs" @@ -954,9 +954,9 @@ have IH1: "map (bder c) rs1 s\* map (bder c) rs2" by fact then show "bder c (AALTs bs rs1) \* bder c (AALTs bs rs2)" using contextrewrites0 by force -next +(*next case ss1 - show "map (bder c) [] s\* map (bder c) []" by simp + show "map (bder c) [] s\* map (bder c) []" by simp*) next case (ss2 rs1 rs2 r) have IH1: "map (bder c) rs1 s\* map (bder c) rs2" by fact @@ -1034,6 +1034,215 @@ (* some tests *) +lemma asize_fuse: + shows "asize (fuse bs r) = asize r" + apply(induct r arbitrary: bs) + apply(auto) + done + +lemma asize_rewrite2: + shows "r1 \ r2 \ asize r1 \ asize r2" + and "rs1 s\ rs2 \ (sum_list (map asize rs1)) \ (sum_list (map asize rs2))" + apply(induct rule: rrewrite_srewrite.inducts) + apply(auto simp add: asize_fuse comp_def) + done + +lemma asize_rrewrites: + assumes "r1 \* r2" + shows "asize r1 \ asize r2" + using assms + apply(induct rule: rrewrites.induct) + apply(auto) + using asize_rewrite2(1) le_trans by blast + + + +fun asize2 :: "arexp \ nat" where + "asize2 AZERO = 1" +| "asize2 (AONE cs) = 1" +| "asize2 (ACHAR cs c) = 1" +| "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))" +| "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)" +| "asize2 (ASTAR cs r) = Suc (asize2 r)" + + +lemma asize2_fuse: + shows "asize2 (fuse bs r) = asize2 r" + apply(induct r arbitrary: bs) + apply(auto) + done + +lemma asize2_not_zero: + shows "0 < asize2 r" + apply(induct r) + apply(auto) + done + +lemma asize_rewrite: + shows "r1 \ r2 \ asize2 r1 > asize2 r2" + and "rs1 s\ rs2 \ (sum_list (map asize2 rs1)) > (sum_list (map asize2 rs2))" + apply(induct rule: rrewrite_srewrite.inducts) + apply(auto simp add: asize2_fuse comp_def) + apply(simp add: asize2_not_zero) + done + +lemma asize2_bsimp_ASEQ: + shows "asize2 (bsimp_ASEQ bs r1 r2) \ Suc (asize2 r1 + asize2 r2)" + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma asize2_bsimp_AALTs: + shows "asize2 (bsimp_AALTs bs rs) \ Suc (Suc (sum_list (map asize2 rs)))" + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(auto simp add: asize2_fuse) + done + +lemma distinctBy_asize2: + shows "sum_list (map asize2 (distinctBy rs f acc)) \ sum_list (map asize2 rs)" + apply(induct rs f acc rule: distinctBy.induct) + apply(auto) + done + +lemma flts_asize2: + shows "sum_list (map asize2 (flts rs)) \ sum_list (map asize2 rs)" + apply(induct rs rule: flts.induct) + apply(auto simp add: comp_def asize2_fuse) + done + +lemma sumlist_asize2: + assumes "\x. x \ set rs \ asize2 (f x) \ asize2 x" + shows "sum_list (map asize2 (map f rs)) \ sum_list (map asize2 rs)" + using assms + apply(induct rs) + apply(auto simp add: comp_def) + by (simp add: add_le_mono) + +lemma test0: + assumes "r1 \* r2" + shows "r1 = r2 \ (\r3. r1 \ r3 \ r3 \* r2)" + using assms + apply(induct r1 r2 rule: rrewrites.induct) + apply(auto) + done + +lemma test2: + assumes "r1 \* r2" + shows "asize2 r1 \ asize2 r2" +using assms + apply(induct r1 r2 rule: rrewrites.induct) + apply(auto) + using asize_rewrite(1) by fastforce + + +lemma test3: + shows "r = bsimp r \ (asize2 (bsimp r) < asize2 r)" +proof - + have "r \* bsimp r" + by (simp add: rewrites_to_bsimp) + then have "r = bsimp r \ (\r3. r \ r3 \ r3 \* bsimp r)" + using test0 by blast + then show ?thesis + by (meson asize_rewrite(1) dual_order.strict_trans2 test2) +qed + +lemma test3Q: + shows "r = bsimp r \ (asize (bsimp r) \ asize r)" +proof - + have "r \* bsimp r" + by (simp add: rewrites_to_bsimp) + then have "r = bsimp r \ (\r3. r \ r3 \ r3 \* bsimp r)" + using test0 by blast + then show ?thesis + using asize_rewrite2(1) asize_rrewrites le_trans by blast +qed + +lemma test4: + shows "asize2 (bsimp (bsimp r)) \ asize2 (bsimp r)" + apply(induct r rule: bsimp.induct) + apply(auto) + using rewrites_to_bsimp test2 apply fastforce + using rewrites_to_bsimp test2 by presburger + +lemma test4Q: + shows "asize (bsimp (bsimp r)) \ asize (bsimp r)" + apply(induct r rule: bsimp.induct) + apply(auto) + apply (metis order_refl test3Q) + by (metis le_refl test3Q) + + + +lemma testb0: + shows "fuse bs1 (bsimp_ASEQ bs r1 r2) = bsimp_ASEQ (bs1 @ bs) r1 r2" + apply(induct bs r1 r2 arbitrary: bs1 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma testb1: + shows "fuse bs1 (bsimp_AALTs bs rs) = bsimp_AALTs (bs1 @ bs) rs" + apply(induct bs rs arbitrary: bs1 rule: bsimp_AALTs.induct) + apply(auto simp add: fuse_append) + done + +lemma testb2: + shows "bsimp (bsimp_ASEQ bs r1 r2) = bsimp_ASEQ bs (bsimp r1) (bsimp r2)" + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(auto simp add: testb0 testb1) + done + +lemma testb3: + shows "\r'. (bsimp r \ r') \ asize2 (bsimp r) > asize2 r'" +apply(induct r rule: bsimp.induct) + apply(auto) + defer + defer + using rrewrite.cases apply blast + using rrewrite.cases apply blast + using rrewrite.cases apply blast + using rrewrite.cases apply blast + oops + +lemma testb4: + assumes "sum_list (map asize rs1) \ sum_list (map asize rs2)" + shows "asize (bsimp_AALTs bs1 rs1) \ Suc (asize (bsimp_AALTs bs1 rs2))" + using assms +apply(induct bs1 rs2 arbitrary: rs1 rule: bsimp_AALTs.induct) + apply(auto) + apply(case_tac rs1) + apply(auto) + using asize2.elims apply auto[1] + apply (metis One_nat_def Zero_not_Suc asize.elims) + apply(case_tac rs1) + apply(auto) + apply(case_tac list) + apply(auto) + using asize_fuse apply force + apply (simp add: asize_fuse) + by (smt (verit, ccfv_threshold) One_nat_def add.right_neutral asize.simps(1) asize.simps(4) asize_fuse bsimp_AALTs.elims le_Suc_eq list.map(1) list.map(2) not_less_eq_eq sum_list_simps(1) sum_list_simps(2)) + +lemma flts_asize: + shows "sum_list (map asize (flts rs)) \ sum_list (map asize rs)" + apply(induct rs rule: flts.induct) + apply(auto simp add: comp_def asize_fuse) + done + + +lemma test5: + shows "asize2 r \ asize2 (bsimp r)" + apply(induct r rule: bsimp.induct) + apply(auto) + apply (meson Suc_le_mono add_le_mono asize2_bsimp_ASEQ order_trans) + apply(rule order_trans) + apply(rule asize2_bsimp_AALTs) + apply(simp) + apply(rule order_trans) + apply(rule distinctBy_asize2) + apply(rule order_trans) + apply(rule flts_asize2) + using sumlist_asize2 by force + + fun awidth :: "arexp \ nat" where "awidth AZERO = 1" | "awidth (AONE cs) = 1" @@ -1071,11 +1280,7 @@ apply(auto) done -lemma asize_fuse: - shows "asize (fuse bs r) = asize r" - apply(induct r arbitrary: bs) - apply(auto) - done + lemma awidth_fuse: shows "awidth (fuse bs r) = awidth r" @@ -1096,19 +1301,6 @@ done lemma - "asize (bsimp (bder c (intern r))) \ Suc ((Suc (card (pder c r))) * (size r) * (size r))" - oops - -lemma - "card (pder c r) \ awidth (bsimp (bder c (intern r)))" - apply(induct c r rule: pder.induct) - apply(simp) - apply(simp) - apply(simp) - apply(simp) - oops - -lemma "card (pder c r) \ awidth (bder c (intern r))" apply(induct c r rule: pder.induct) apply(simp)