equal
deleted
inserted
replaced
1475 qed |
1475 qed |
1476 qed |
1476 qed |
1477 qed |
1477 qed |
1478 next |
1478 next |
1479 show "?Hd x y \<union> ?Tl xs ys \<subseteq> ?List x xs y ys" |
1479 show "?Hd x y \<union> ?Tl xs ys \<subseteq> ?List x xs y ys" |
1480 proof |
1480 proof (rule subsetI) |
1481 fix el |
1481 fix el |
1482 assume el_in_hd_tl: "el \<in> ?Hd x y \<union> ?Tl xs ys" |
1482 assume el_in_hd_tl: "el \<in> ?Hd x y \<union> ?Tl xs ys" |
1483 show "el \<in> ?List x xs y ys" |
1483 show "el \<in> ?List x xs y ys" |
1484 proof (cases el) |
1484 proof (cases el) |
1485 case This |
1485 case This |
2976 case True |
2976 case True |
2977 with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" |
2977 with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" |
2978 by simp |
2978 by simp |
2979 from da_e1 s0_s1 True obtain E1' where |
2979 from da_e1 s0_s1 True obtain E1' where |
2980 "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'" |
2980 "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'" |
2981 by - (rule da_weakenE,auto) |
2981 by - (rule da_weakenE, auto iff del: Un_subset_iff) |
2982 with conf_s1 wt_e1 |
2982 with conf_s1 wt_e1 |
2983 obtain |
2983 obtain |
2984 "s2\<Colon>\<preceq>(G, L)" |
2984 "s2\<Colon>\<preceq>(G, L)" |
2985 "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)" |
2985 "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)" |
2986 "error_free s2" |
2986 "error_free s2" |
2995 case False |
2995 case False |
2996 with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" |
2996 with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" |
2997 by simp |
2997 by simp |
2998 from da_e2 s0_s1 False obtain E2' where |
2998 from da_e2 s0_s1 False obtain E2' where |
2999 "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'" |
2999 "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'" |
3000 by - (rule da_weakenE,auto) |
3000 by - (rule da_weakenE, auto iff del: Un_subset_iff) |
3001 with conf_s1 wt_e2 |
3001 with conf_s1 wt_e2 |
3002 obtain |
3002 obtain |
3003 "s2\<Colon>\<preceq>(G, L)" |
3003 "s2\<Colon>\<preceq>(G, L)" |
3004 "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)" |
3004 "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)" |
3005 "error_free s2" |
3005 "error_free s2" |