equal
deleted
inserted
replaced
711 {* |
711 {* |
712 fun rename_client_map_tac ctxt = |
712 fun rename_client_map_tac ctxt = |
713 EVERY [ |
713 EVERY [ |
714 simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, |
714 simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, |
715 rtac @{thm guarantees_PLam_I} 1, |
715 rtac @{thm guarantees_PLam_I} 1, |
716 assume_tac 2, |
716 assume_tac ctxt 2, |
717 (*preserves: routine reasoning*) |
717 (*preserves: routine reasoning*) |
718 asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, |
718 asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, |
719 (*the guarantee for "lift i (rename client_map Client)" *) |
719 (*the guarantee for "lift i (rename client_map Client)" *) |
720 asm_simp_tac |
720 asm_simp_tac |
721 (ctxt addsimps [@{thm lift_guarantees_eq_lift_inv}, |
721 (ctxt addsimps [@{thm lift_guarantees_eq_lift_inv}, |