867 |
867 |
868 lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==> |
868 lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==> |
869 ve + {ev |-> v} hastyenv te + {ev |=> t}" |
869 ve + {ev |-> v} hastyenv te + {ev |=> t}" |
870 apply (unfold hasty_env_def) |
870 apply (unfold hasty_env_def) |
871 apply (simp del: mem_simps add: ve_dom_owr te_dom_owr) |
871 apply (simp del: mem_simps add: ve_dom_owr te_dom_owr) |
872 apply (tactic {* safe_tac HOL_cs *}) |
872 apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *}) |
873 apply (case_tac "ev=x") |
873 apply (case_tac "ev=x") |
874 apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1) |
874 apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1) |
875 apply (simp add: ve_app_owr2 te_app_owr2) |
875 apply (simp add: ve_app_owr2 te_app_owr2) |
876 done |
876 done |
877 |
877 |
904 te |- fix ev2 ev1 = e ===> t |
904 te |- fix ev2 ev1 = e ===> t |
905 |] ==> |
905 |] ==> |
906 v_clos(cl) hasty t" |
906 v_clos(cl) hasty t" |
907 apply (unfold hasty_env_def hasty_def) |
907 apply (unfold hasty_env_def hasty_def) |
908 apply (drule elab_fix_elim) |
908 apply (drule elab_fix_elim) |
909 apply (tactic {* safe_tac HOL_cs *}) |
909 apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *}) |
910 (*Do a single unfolding of cl*) |
910 (*Do a single unfolding of cl*) |
911 apply (frule ssubst) prefer 2 apply assumption |
911 apply (frule ssubst) prefer 2 apply assumption |
912 apply (rule hasty_rel_clos_coind) |
912 apply (rule hasty_rel_clos_coind) |
913 apply (erule elab_fn) |
913 apply (erule elab_fn) |
914 apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr) |
914 apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr) |
915 |
915 |
916 apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr) |
916 apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr) |
917 apply (tactic {* safe_tac HOL_cs *}) |
917 apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *}) |
918 apply (case_tac "ev2=ev1a") |
918 apply (case_tac "ev2=ev1a") |
919 apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1) |
919 apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1) |
920 apply blast |
920 apply blast |
921 apply (simp add: ve_app_owr2 te_app_owr2) |
921 apply (simp add: ve_app_owr2 te_app_owr2) |
922 done |
922 done |