equal
deleted
inserted
replaced
530 apply (simplesubst method_rec, assumption+) |
530 apply (simplesubst method_rec, assumption+) |
531 apply (clarify) |
531 apply (clarify) |
532 apply (erule_tac x = "Da" in allE) |
532 apply (erule_tac x = "Da" in allE) |
533 apply (clarsimp) |
533 apply (clarsimp) |
534 apply (simp add: map_of_map) |
534 apply (simp add: map_of_map) |
535 apply (clarify) |
|
536 apply (subst method_rec, assumption+) |
535 apply (subst method_rec, assumption+) |
537 apply (simp add: map_add_def map_of_map split: option.split) |
536 apply (simp add: map_add_def map_of_map split: option.split) |
538 done |
537 done |
539 |
538 |
540 |
539 |
550 apply (simplesubst method_rec, assumption+) |
549 apply (simplesubst method_rec, assumption+) |
551 apply (clarify) |
550 apply (clarify) |
552 apply (erule_tac x = "Da" in allE) |
551 apply (erule_tac x = "Da" in allE) |
553 apply (clarsimp) |
552 apply (clarsimp) |
554 apply (simp add: map_of_map) |
553 apply (simp add: map_of_map) |
555 apply (clarify) |
|
556 apply (subst method_rec, assumption+) |
554 apply (subst method_rec, assumption+) |
557 apply (simp add: map_add_def map_of_map split: option.split) |
555 apply (simp add: map_add_def map_of_map split: option.split) |
558 done |
556 done |
559 |
557 |
560 lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> |
558 lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> |
597 apply clarify |
595 apply clarify |
598 apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)") |
596 apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)") |
599 apply (simp (no_asm_use) only: map_add_Some_iff) |
597 apply (simp (no_asm_use) only: map_add_Some_iff) |
600 apply (erule disjE) |
598 apply (erule disjE) |
601 apply (simp (no_asm_use) add: map_of_map) apply blast |
599 apply (simp (no_asm_use) add: map_of_map) apply blast |
602 apply blast |
|
603 apply (rule trans [symmetric], rule sym, assumption) |
600 apply (rule trans [symmetric], rule sym, assumption) |
604 apply (rule_tac x=vn in fun_cong) |
601 apply (rule_tac x=vn in fun_cong) |
605 apply (rule trans, rule field_rec, assumption+) |
602 apply (rule trans, rule field_rec, assumption+) |
606 apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
603 apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
607 apply (simp (no_asm_use)) apply blast |
604 apply (simp (no_asm_use)) apply blast |