equal
deleted
inserted
replaced
1222 assumes "s \<in> (der c r) \<rightarrow> v" |
1222 assumes "s \<in> (der c r) \<rightarrow> v" |
1223 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
1223 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
1224 using assms |
1224 using assms |
1225 apply(induct c r arbitrary: s v rule: der.induct) |
1225 apply(induct c r arbitrary: s v rule: der.induct) |
1226 apply(auto) |
1226 apply(auto) |
1227 apply(erule PMatch.cases) |
1227 (* NULL case *) |
1228 apply(simp_all)[7] |
1228 apply(erule PMatch.cases) |
1229 apply(erule PMatch.cases) |
1229 apply(simp_all)[7] |
1230 apply(simp_all)[7] |
1230 (* EMPTY case *) |
|
1231 apply(erule PMatch.cases) |
|
1232 apply(simp_all)[7] |
|
1233 (* CHAR case *) |
1231 apply(case_tac "c = c'") |
1234 apply(case_tac "c = c'") |
1232 apply(simp) |
1235 apply(simp) |
1233 apply(erule PMatch.cases) |
1236 apply(erule PMatch.cases) |
1234 apply(simp_all)[7] |
1237 apply(simp_all)[7] |
1235 apply (metis PMatch.intros(2)) |
1238 apply (metis PMatch.intros(2)) |
1236 apply(simp) |
1239 apply(simp) |
1237 apply(erule PMatch.cases) |
1240 apply(erule PMatch.cases) |
1238 apply(simp_all)[7] |
1241 apply(simp_all)[7] |
|
1242 (* ALT case *) |
1239 apply(erule PMatch.cases) |
1243 apply(erule PMatch.cases) |
1240 apply(simp_all)[7] |
1244 apply(simp_all)[7] |
1241 apply (metis PMatch.intros(3)) |
1245 apply (metis PMatch.intros(3)) |
1242 apply(clarify) |
1246 apply(clarify) |
1243 apply(rule PMatch.intros) |
1247 apply(rule PMatch.intros) |
1245 apply(simp add: der_correctness Der_def) |
1249 apply(simp add: der_correctness Der_def) |
1246 (* SEQ case *) |
1250 (* SEQ case *) |
1247 apply(case_tac "nullable r1") |
1251 apply(case_tac "nullable r1") |
1248 apply(simp) |
1252 apply(simp) |
1249 prefer 2 |
1253 prefer 2 |
|
1254 (* not-nullbale case *) |
1250 apply(simp) |
1255 apply(simp) |
1251 apply(erule PMatch.cases) |
1256 apply(erule PMatch.cases) |
1252 apply(simp_all)[7] |
1257 apply(simp_all)[7] |
1253 apply(clarify) |
1258 apply(clarify) |
1254 apply(subst append.simps(2)[symmetric]) |
1259 apply(subst append.simps(2)[symmetric]) |
1259 apply(simp add: der_correctness Der_def) |
1264 apply(simp add: der_correctness Der_def) |
1260 apply(auto)[1] |
1265 apply(auto)[1] |
1261 (* nullable case *) |
1266 (* nullable case *) |
1262 apply(erule PMatch.cases) |
1267 apply(erule PMatch.cases) |
1263 apply(simp_all)[7] |
1268 apply(simp_all)[7] |
|
1269 (* left case *) |
1264 apply(clarify) |
1270 apply(clarify) |
1265 apply(erule PMatch.cases) |
1271 apply(erule PMatch.cases) |
1266 apply(simp_all)[4] |
1272 apply(simp_all)[4] |
|
1273 prefer 2 |
|
1274 apply(clarify) |
|
1275 prefer 2 |
|
1276 apply(clarify) |
1267 apply(clarify) |
1277 apply(clarify) |
1268 apply(simp (no_asm)) |
1278 apply(simp (no_asm)) |
1269 apply(subst append.simps(2)[symmetric]) |
1279 apply(subst append.simps(2)[symmetric]) |
1270 apply(rule PMatch.intros) |
1280 apply(rule PMatch.intros) |
1271 apply metis |
1281 apply metis |
1273 apply(erule contrapos_nn) |
1283 apply(erule contrapos_nn) |
1274 apply(erule exE)+ |
1284 apply(erule exE)+ |
1275 apply(auto)[1] |
1285 apply(auto)[1] |
1276 apply(simp add: der_correctness Der_def) |
1286 apply(simp add: der_correctness Der_def) |
1277 apply metis |
1287 apply metis |
1278 apply(simp) |
1288 (* right interesting case *) |
1279 (* interesting case *) |
|
1280 apply(clarify) |
|
1281 apply(clarify) |
1289 apply(clarify) |
1282 apply(simp) |
1290 apply(simp) |
1283 apply(subst (asm) L.simps(4)[symmetric]) |
1291 apply(subst (asm) L.simps(4)[symmetric]) |
1284 apply(simp only: L_flat_Prf) |
1292 apply(simp only: L_flat_Prf) |
1285 apply(simp) |
1293 apply(simp) |