1037 lemma asize_fuse:

  1038   shows "asize (fuse bs r) = asize r"

  1039   apply(induct r arbitrary: bs)

  1040   apply(auto)

  1041   done

  1042 

  1043 lemma asize_rewrite2:

  1044   shows "r1 \<leadsto> r2 \<Longrightarrow> asize r1 \<ge> asize r2"

  1045   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize rs1)) \<ge> (sum_list (map asize rs2))"

  1046    apply(induct rule: rrewrite_srewrite.inducts)

  1047    apply(auto simp add: asize_fuse comp_def)

  1048   done

  1049 

  1050 lemma asize_rrewrites:

  1051   assumes "r1 \<leadsto>* r2"

  1052   shows "asize r1 \<ge> asize r2"

  1053   using assms

  1054   apply(induct rule: rrewrites.induct)

  1055    apply(auto)

  1056   using asize_rewrite2(1) le_trans by blast

  1057   

  1058 

  1059 

  1060 fun asize2 :: "arexp \<Rightarrow> nat" where

  1061   "asize2 AZERO = 1"

  1062 | "asize2 (AONE cs) = 1" 

  1063 | "asize2 (ACHAR cs c) = 1"

  1064 | "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"

  1065 | "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"

  1066 | "asize2 (ASTAR cs r) = Suc (asize2 r)"

  1067 

  1068 

  1069 lemma asize2_fuse:

  1070   shows "asize2 (fuse bs r) = asize2 r"

  1071   apply(induct r arbitrary: bs)

  1072   apply(auto)

  1073   done

  1074 

  1075 lemma asize2_not_zero:

  1076   shows "0 < asize2 r"

  1077   apply(induct r)

  1078   apply(auto)

  1079   done

  1080 

  1081 lemma asize_rewrite:

  1082   shows "r1 \<leadsto> r2 \<Longrightarrow> asize2 r1 > asize2 r2"

  1083   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize2 rs1)) > (sum_list (map asize2 rs2))"

  1084    apply(induct rule: rrewrite_srewrite.inducts)

  1085    apply(auto simp add: asize2_fuse comp_def)

  1086   apply(simp add: asize2_not_zero) 

  1087   done

  1088 

  1089 lemma asize2_bsimp_ASEQ:

  1090   shows "asize2 (bsimp_ASEQ bs r1 r2) \<le> Suc (asize2 r1 + asize2 r2)"

  1091   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

  1092   apply(auto)

  1093   done

  1094 

  1095 lemma asize2_bsimp_AALTs:

  1096   shows "asize2 (bsimp_AALTs bs rs) \<le> Suc (Suc (sum_list (map asize2 rs)))"

  1097   apply(induct bs rs rule: bsimp_AALTs.induct)

  1098   apply(auto simp add: asize2_fuse)

  1099   done

  1100 

  1101 lemma distinctBy_asize2:

  1102   shows "sum_list (map asize2 (distinctBy rs f acc)) \<le> sum_list (map asize2 rs)"

  1103   apply(induct rs f acc rule: distinctBy.induct)

  1104   apply(auto)

  1105   done

  1106 

  1107 lemma flts_asize2:

  1108   shows "sum_list (map asize2 (flts rs)) \<le> sum_list (map asize2 rs)"

  1109   apply(induct rs rule: flts.induct)

  1110   apply(auto simp add: comp_def asize2_fuse)

  1111   done

  1112 

  1113 lemma sumlist_asize2:

  1114   assumes "\<And>x. x \<in> set rs \<Longrightarrow> asize2 (f x) \<le> asize2 x"

  1115   shows "sum_list (map asize2 (map f rs)) \<le> sum_list (map asize2 rs)"

  1116   using assms

  1117   apply(induct rs)

  1118    apply(auto simp add: comp_def)

  1119   by (simp add: add_le_mono)

  1120 

  1121 lemma test0:

  1122   assumes "r1 \<leadsto>* r2"

  1123   shows "r1 = r2 \<or> (\<exists>r3. r1 \<leadsto> r3 \<and> r3 \<leadsto>* r2)"

  1124   using assms

  1125   apply(induct r1 r2 rule: rrewrites.induct)

  1126    apply(auto)

  1127   done

  1128 

  1129 lemma test2:

  1130   assumes "r1 \<leadsto>* r2"

  1131   shows "asize2 r1 \<ge> asize2 r2"

  1132 using assms

  1133   apply(induct r1 r2 rule: rrewrites.induct)

  1134   apply(auto)

  1135   using asize_rewrite(1) by fastforce

  1136   

  1137 

  1138 lemma test3:

  1139   shows "r = bsimp r \<or> (asize2 (bsimp r) < asize2 r)"

  1140 proof -

  1141   have "r \<leadsto>* bsimp r"

  1142     by (simp add: rewrites_to_bsimp)

  1143   then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"

  1144     using test0 by blast

  1145   then show ?thesis

  1146     by (meson asize_rewrite(1) dual_order.strict_trans2 test2)

  1147 qed

  1148 

  1149 lemma test3Q:

  1150   shows "r = bsimp r \<or> (asize (bsimp r) \<le> asize r)"

  1151 proof -

  1152   have "r \<leadsto>* bsimp r"

  1153     by (simp add: rewrites_to_bsimp)

  1154   then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"

  1155     using test0 by blast

  1156   then show ?thesis

  1157     using asize_rewrite2(1) asize_rrewrites le_trans by blast

  1158 qed

  1159 

  1160 lemma test4:

  1161   shows "asize2 (bsimp (bsimp r)) \<le> asize2 (bsimp r)"

  1162   apply(induct r rule: bsimp.induct)

  1163        apply(auto)

  1164   using rewrites_to_bsimp test2 apply fastforce

  1165   using rewrites_to_bsimp test2 by presburger

  1166 

  1167 lemma test4Q:

  1168   shows "asize (bsimp (bsimp r)) \<le> asize (bsimp r)"

  1169   apply(induct r rule: bsimp.induct)

  1170        apply(auto)

  1171   apply (metis order_refl test3Q)

  1172   by (metis le_refl test3Q)

  1173 

  1174 

  1175 

  1176 lemma testb0:

  1177   shows "fuse bs1 (bsimp_ASEQ bs r1 r2) =  bsimp_ASEQ (bs1 @ bs) r1 r2"

  1178   apply(induct bs r1 r2 arbitrary: bs1 rule: bsimp_ASEQ.induct)

  1179   apply(auto)

  1180   done

  1181 

  1182 lemma testb1:

  1183   shows "fuse bs1 (bsimp_AALTs bs rs) =  bsimp_AALTs (bs1 @ bs) rs"

  1184   apply(induct bs rs arbitrary: bs1 rule: bsimp_AALTs.induct)

  1185   apply(auto simp add: fuse_append)

  1186   done

  1187 

  1188 lemma testb2:

  1189   shows "bsimp (bsimp_ASEQ bs r1 r2) =  bsimp_ASEQ bs (bsimp r1) (bsimp r2)"

  1190   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

  1191   apply(auto simp add: testb0 testb1)

  1192   done  

  1193 

  1194 lemma testb3:

  1195   shows "\<nexists>r'. (bsimp r \<leadsto> r') \<and> asize2 (bsimp r) > asize2 r'"

  1196 apply(induct r rule: bsimp.induct)

  1197        apply(auto)

  1198        defer

  1199        defer

  1200   using rrewrite.cases apply blast

  1201   using rrewrite.cases apply blast

  1202   using rrewrite.cases apply blast

  1203   using rrewrite.cases apply blast

  1204   oops

  1205 

  1206 lemma testb4:

  1207   assumes "sum_list (map asize rs1) \<le> sum_list (map asize rs2)"

  1208   shows "asize (bsimp_AALTs bs1 rs1) \<le> Suc (asize (bsimp_AALTs bs1 rs2))"

  1209   using assms 

  1210 apply(induct bs1 rs2 arbitrary: rs1 rule: bsimp_AALTs.induct)

  1211     apply(auto)

  1212     apply(case_tac rs1)

  1213      apply(auto)

  1214   using asize2.elims apply auto[1]

  1215   apply (metis One_nat_def Zero_not_Suc asize.elims)

  1216       apply(case_tac rs1)

  1217     apply(auto)

  1218    apply(case_tac list)

  1219     apply(auto)

  1220   using asize_fuse apply force

  1221   apply (simp add: asize_fuse)

  1222   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))

  1223 

  1224 lemma flts_asize:

  1225   shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"

  1226   apply(induct rs rule: flts.induct)

  1227   apply(auto simp add: comp_def asize_fuse)

  1228   done

  1229 

  1230 

  1231 lemma test5:

  1232   shows "asize2 r \<ge> asize2 (bsimp r)"

  1233   apply(induct r rule: bsimp.induct)

  1234        apply(auto)

  1235   apply (meson Suc_le_mono add_le_mono asize2_bsimp_ASEQ order_trans)

  1236   apply(rule order_trans)

  1237    apply(rule asize2_bsimp_AALTs)

  1238   apply(simp)

  1239   apply(rule order_trans)

  1240    apply(rule distinctBy_asize2)

  1241   apply(rule order_trans)

  1242    apply(rule flts_asize2)

  1243   using sumlist_asize2 by force

  1244   

  1245