equal
deleted
inserted
replaced
87 val prems = goalw Values.thy [ve_dom_def,ve_owr_def] |
87 val prems = goalw Values.thy [ve_dom_def,ve_owr_def] |
88 "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"; |
88 "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"; |
89 by (cut_facts_tac prems 1); |
89 by (cut_facts_tac prems 1); |
90 by (etac ValEnvE 1); |
90 by (etac ValEnvE 1); |
91 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
91 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
92 by (rtac (map_domain_owr RS ssubst) 1); |
92 by (stac map_domain_owr 1); |
93 by (assume_tac 1); |
93 by (assume_tac 1); |
94 by (rtac Un_commute 1); |
94 by (rtac Un_commute 1); |
95 qed "ve_dom_owr"; |
95 qed "ve_dom_owr"; |
96 |
96 |
97 goalw Values.thy [ve_app_def,ve_owr_def] |
97 goalw Values.thy [ve_app_def,ve_owr_def] |