equal
deleted
inserted
replaced
1454 apply(subst append.simps(2)[symmetric]) |
1454 apply(subst append.simps(2)[symmetric]) |
1455 apply(rule PMatch.intros) |
1455 apply(rule PMatch.intros) |
1456 apply metis |
1456 apply metis |
1457 apply metis |
1457 apply metis |
1458 apply(auto)[1] |
1458 apply(auto)[1] |
1459 apply(simp add: L_flat_NPrf) |
1459 apply(simp add: der_correctness Der_def) |
1460 apply(auto)[1] |
1460 apply(auto)[1] |
1461 apply(frule_tac c="c" in v3_proj) |
|
1462 apply metis |
|
1463 apply(drule_tac x="s\<^sub>3" in spec) |
|
1464 apply(drule mp) |
|
1465 apply(rule_tac x="projval r1 c v" in exI) |
|
1466 apply(rule conjI) |
|
1467 apply (metis v4_proj2) |
|
1468 apply (metis NPrf_imp_Prf) |
|
1469 apply metis |
|
1470 (* nullable case *) |
1461 (* nullable case *) |
1471 apply(erule PMatch.cases) |
1462 apply(erule PMatch.cases) |
1472 apply(simp_all)[7] |
1463 apply(simp_all)[7] |
1473 apply(clarify) |
1464 apply(clarify) |
1474 apply(erule PMatch.cases) |
1465 apply(erule PMatch.cases) |