24 "Stars_add v (Stars vs) = Stars (v # vs)" |
24 "Stars_add v (Stars vs) = Stars (v # vs)" |
25 |
25 |
26 function |
26 function |
27 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
27 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
28 where |
28 where |
29 "decode' ds ZERO = (Void, [])" |
29 "decode' bs ZERO = (undefined, bs)" |
30 | "decode' ds ONE = (Void, ds)" |
30 | "decode' bs ONE = (Void, bs)" |
31 | "decode' ds (CH d) = (Char d, ds)" |
31 | "decode' bs (CH d) = (Char d, bs)" |
32 | "decode' [] (ALT r1 r2) = (Void, [])" |
32 | "decode' [] (ALT r1 r2) = (Void, [])" |
33 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
33 | "decode' (Z # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r1 in (Left v, bs'))" |
34 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
34 | "decode' (S # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r2 in (Right v, bs'))" |
35 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
35 | "decode' bs (SEQ r1 r2) = (let (v1, bs') = decode' bs r1 in |
36 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
36 let (v2, bs'') = decode' bs' r2 in (Seq v1 v2, bs''))" |
37 | "decode' [] (STAR r) = (Void, [])" |
37 | "decode' [] (STAR r) = (Void, [])" |
38 | "decode' (S # ds) (STAR r) = (Stars [], ds)" |
38 | "decode' (S # bs) (STAR r) = (Stars [], bs)" |
39 | "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in |
39 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
40 let (vs, ds'') = decode' ds' (STAR r) |
40 let (vs, bs'') = decode' bs' (STAR r) |
41 in (Stars_add v vs, ds''))" |
41 in (Stars_add v vs, bs''))" |
42 by pat_completeness auto |
42 by pat_completeness auto |
43 |
43 |
44 lemma decode'_smaller: |
44 lemma decode'_smaller: |
45 assumes "decode'_dom (ds, r)" |
45 assumes "decode'_dom (bs, r)" |
46 shows "length (snd (decode' ds r)) \<le> length ds" |
46 shows "length (snd (decode' bs r)) \<le> length bs" |
47 using assms |
47 using assms |
48 apply(induct ds r) |
48 apply(induct bs r) |
49 apply(auto simp add: decode'.psimps split: prod.split) |
49 apply(auto simp add: decode'.psimps split: prod.split) |
50 using dual_order.trans apply blast |
50 using dual_order.trans apply blast |
51 by (meson dual_order.trans le_SucI) |
51 by (meson dual_order.trans le_SucI) |
52 |
52 |
53 termination "decode'" |
53 termination "decode'" |
1030 theorem blexersimp_correctness: |
1030 theorem blexersimp_correctness: |
1031 shows "lexer r s = blexer_simp r s" |
1031 shows "lexer r s = blexer_simp r s" |
1032 using blexer_correctness main_blexer_simp by simp |
1032 using blexer_correctness main_blexer_simp by simp |
1033 |
1033 |
1034 |
1034 |
|
1035 (* some tests *) |
|
1036 |
|
1037 fun awidth :: "arexp \<Rightarrow> nat" where |
|
1038 "awidth AZERO = 1" |
|
1039 | "awidth (AONE cs) = 1" |
|
1040 | "awidth (ACHAR cs c) = 1" |
|
1041 | "awidth (AALTs cs rs) = (sum_list (map awidth rs))" |
|
1042 | "awidth (ASEQ cs r1 r2) = (awidth r1 + awidth r2)" |
|
1043 | "awidth (ASTAR cs r) = (awidth r)" |
|
1044 |
|
1045 |
|
1046 |
|
1047 lemma |
|
1048 shows "s \<notin> L r \<Longrightarrow> blexer_simp r s = None" |
|
1049 by (simp add: blexersimp_correctness lexer_correct_None) |
|
1050 |
|
1051 lemma g1: |
|
1052 "bders_simp AZERO s = AZERO" |
|
1053 apply(induct s) |
|
1054 apply(simp) |
|
1055 apply(simp) |
|
1056 done |
|
1057 |
|
1058 lemma g2: |
|
1059 "s \<noteq> Nil \<Longrightarrow> bders_simp (AONE bs) s = AZERO" |
|
1060 apply(induct s) |
|
1061 apply(simp) |
|
1062 apply(simp) |
|
1063 apply(case_tac s) |
|
1064 apply(simp) |
|
1065 apply(simp) |
|
1066 done |
|
1067 |
|
1068 lemma finite_pder: |
|
1069 shows "finite (pder c r)" |
|
1070 apply(induct c r rule: pder.induct) |
|
1071 apply(auto) |
|
1072 done |
|
1073 |
|
1074 lemma asize_fuse: |
|
1075 shows "asize (fuse bs r) = asize r" |
|
1076 apply(induct r arbitrary: bs) |
|
1077 apply(auto) |
|
1078 done |
|
1079 |
|
1080 lemma awidth_fuse: |
|
1081 shows "awidth (fuse bs r) = awidth r" |
|
1082 apply(induct r arbitrary: bs) |
|
1083 apply(auto) |
|
1084 done |
|
1085 |
|
1086 lemma pders_SEQs: |
|
1087 assumes "finite A" |
|
1088 shows "card (SEQs A (STAR r)) \<le> card A" |
|
1089 using assms |
|
1090 by (simp add: SEQs_eq_image card_image_le) |
|
1091 |
|
1092 lemma binullable_intern: |
|
1093 shows "bnullable (intern r) = nullable r" |
|
1094 apply(induct r) |
|
1095 apply(auto simp add: bnullable_fuse) |
|
1096 done |
|
1097 |
|
1098 lemma |
|
1099 "asize (bsimp (bder c (intern r))) \<le> Suc ((Suc (card (pder c r))) * (size r) * (size r))" |
|
1100 oops |
|
1101 |
|
1102 lemma |
|
1103 "card (pder c r) \<le> awidth (bsimp (bder c (intern r)))" |
|
1104 apply(induct c r rule: pder.induct) |
|
1105 apply(simp) |
|
1106 apply(simp) |
|
1107 apply(simp) |
|
1108 apply(simp) |
|
1109 oops |
|
1110 |
|
1111 lemma |
|
1112 "card (pder c r) \<le> awidth (bder c (intern r))" |
|
1113 apply(induct c r rule: pder.induct) |
|
1114 apply(simp) |
|
1115 apply(simp) |
|
1116 apply(simp) |
|
1117 apply(simp) |
|
1118 apply(rule order_trans) |
|
1119 apply(rule card_Un_le) |
|
1120 apply (simp add: awidth_fuse bder_fuse) |
|
1121 defer |
|
1122 apply(simp) |
|
1123 apply(rule order_trans) |
|
1124 apply(rule pders_SEQs) |
|
1125 using finite_pder apply presburger |
|
1126 apply (simp add: awidth_fuse) |
|
1127 apply(auto) |
|
1128 apply(rule order_trans) |
|
1129 apply(rule card_Un_le) |
|
1130 apply(simp add: awidth_fuse) |
|
1131 defer |
|
1132 using binullable_intern apply blast |
|
1133 using binullable_intern apply blast |
|
1134 apply (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2) |
|
1135 apply(subgoal_tac "card (SEQs (pder c r1) r2) \<le> card (pder c r1)") |
|
1136 apply(linarith) |
|
1137 by (simp add: UNION_singleton_eq_range card_image_le finite_pder) |
|
1138 |
|
1139 lemma |
|
1140 "card (pder c r) \<le> asize (bder c (intern r))" |
|
1141 apply(induct c r rule: pder.induct) |
|
1142 apply(simp) |
|
1143 apply(simp) |
|
1144 apply(simp) |
|
1145 apply(simp) |
|
1146 apply (metis add_mono_thms_linordered_semiring(1) asize_fuse bder_fuse card_Un_le le_Suc_eq order_trans) |
|
1147 defer |
|
1148 apply(simp) |
|
1149 apply(rule order_trans) |
|
1150 apply(rule pders_SEQs) |
|
1151 using finite_pder apply presburger |
|
1152 apply (simp add: asize_fuse) |
|
1153 apply(simp) |
|
1154 apply(auto) |
|
1155 apply(rule order_trans) |
|
1156 apply(rule card_Un_le) |
|
1157 apply (smt (z3) SEQs_eq_image add.commute add_Suc_right add_mono_thms_linordered_semiring(1) asize_fuse card_image_le dual_order.trans finite_pder le_add1) |
|
1158 apply(rule order_trans) |
|
1159 apply(rule card_Un_le) |
|
1160 using binullable_intern apply blast |
|
1161 using binullable_intern apply blast |
|
1162 by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2) |
|
1163 |
|
1164 lemma |
|
1165 "card (pder c r) \<le> asize (bsimp (bder c (intern r)))" |
|
1166 apply(induct c r rule: pder.induct) |
|
1167 apply(simp) |
|
1168 apply(simp) |
|
1169 apply(simp) |
|
1170 apply(simp) |
|
1171 apply(rule order_trans) |
|
1172 apply(rule card_Un_le) |
|
1173 prefer 3 |
|
1174 apply(simp) |
|
1175 apply(rule order_trans) |
|
1176 apply(rule pders_SEQs) |
|
1177 using finite_pder apply blast |
|
1178 oops |
|
1179 |
|
1180 |
1035 (* below is the idempotency of bsimp *) |
1181 (* below is the idempotency of bsimp *) |
1036 |
1182 |
1037 lemma bsimp_ASEQ_fuse: |
1183 lemma bsimp_ASEQ_fuse: |
1038 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
1184 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
1039 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |
1185 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |