1035 by (simp add: rmlab_def) |
1035 by (simp add: rmlab_def) |
1036 |
1036 |
1037 lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'" |
1037 lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'" |
1038 by (auto simp add: rmlab_def) |
1038 by (auto simp add: rmlab_def) |
1039 |
1039 |
1040 lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B" |
1040 lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B" |
1041 by (auto simp add: range_inter_ts_def) |
1041 by (auto simp add: range_inter_ts_def) |
1042 |
1042 |
1043 lemma range_inter_ts_subseteq': |
1043 lemma range_inter_ts_subseteq': "\<forall> k. A k \<subseteq> B k \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>A \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B" |
1044 "\<lbrakk>\<forall> k. A k \<subseteq> B k; x \<in> \<Rightarrow>\<Inter>A\<rbrakk> \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B" |
|
1045 by (auto simp add: range_inter_ts_def) |
1044 by (auto simp add: range_inter_ts_def) |
1046 |
1045 |
1047 lemma da_monotone: |
1046 lemma da_monotone: |
1048 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and |
1047 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and |
1049 "B \<subseteq> B'" and |
1048 "B \<subseteq> B'" and |
1070 moreover |
1069 moreover |
1071 obtain C' |
1070 obtain C' |
1072 where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
1071 where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
1073 and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')" |
1072 and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')" |
1074 using Lab.prems |
1073 using Lab.prems |
1075 by - (erule da_elim_cases,simp) |
1074 by cases simp |
1076 ultimately |
1075 ultimately |
1077 have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto |
1076 have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto |
1078 then |
1077 then |
1079 have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto |
1078 have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto |
1080 moreover |
1079 moreover |
1093 from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'` |
1092 from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'` |
1094 obtain C1' C2' |
1093 obtain C1' C2' |
1095 where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1094 where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1096 da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1095 da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1097 A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1096 A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1098 by (rule da_elim_cases) auto |
1097 by cases auto |
1099 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1098 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1100 moreover note `B \<subseteq> B'` |
1099 moreover note `B \<subseteq> B'` |
1101 moreover note da_c1 |
1100 moreover note da_c1 |
1102 ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1101 ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1103 by auto |
1102 by auto |
1114 from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'` |
1113 from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'` |
1115 obtain C1' C2' |
1114 obtain C1' C2' |
1116 where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1115 where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1117 da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1116 da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1118 A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1117 A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1119 by (rule da_elim_cases) auto |
1118 by cases auto |
1120 note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1` |
1119 note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1` |
1121 moreover note B' = `B \<subseteq> B'` |
1120 moreover note B' = `B \<subseteq> B'` |
1122 moreover note da_c1 |
1121 moreover note da_c1 |
1123 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1122 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1124 by blast |
1123 by blast |
1136 obtain C' |
1135 obtain C' |
1137 where |
1136 where |
1138 da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and |
1137 da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and |
1139 A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)" |
1138 A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)" |
1140 "brk A' = brk C'" |
1139 "brk A' = brk C'" |
1141 by (rule da_elim_cases) auto |
1140 by cases auto |
1142 note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C` |
1141 note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C` |
1143 moreover note B' = `B \<subseteq> B'` |
1142 moreover note B' = `B \<subseteq> B'` |
1144 moreover note da_c' |
1143 moreover note da_c' |
1145 ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)" |
1144 ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)" |
1146 by blast |
1145 by blast |
1166 by auto |
1165 by auto |
1167 next |
1166 next |
1168 case (Jmp jump B A Env B' A') |
1167 case (Jmp jump B A Env B' A') |
1169 thus ?case by (elim da_elim_cases) (auto split: jump.splits) |
1168 thus ?case by (elim da_elim_cases) (auto split: jump.splits) |
1170 next |
1169 next |
1171 case Throw thus ?case by - (erule da_elim_cases, auto) |
1170 case Throw thus ?case by (elim da_elim_cases) auto |
1172 next |
1171 next |
1173 case (Try Env B c1 C1 vn C c2 C2 A B' A') |
1172 case (Try Env B c1 C1 vn C c2 C2 A B' A') |
1174 note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2` |
1173 note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2` |
1175 from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'` |
1174 from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'` |
1176 obtain C1' C2' |
1175 obtain C1' C2' |
1177 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1176 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1178 da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} |
1177 da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} |
1179 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1178 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1180 A': "nrm A' = nrm C1' \<inter> nrm C2'" |
1179 A': "nrm A' = nrm C1' \<inter> nrm C2'" |
1181 "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1180 "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
1182 by (rule da_elim_cases) auto |
1181 by cases auto |
1183 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1182 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1184 moreover note B' = `B \<subseteq> B'` |
1183 moreover note B' = `B \<subseteq> B'` |
1185 moreover note da_c1' |
1184 moreover note da_c1' |
1186 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1185 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1187 by blast |
1186 by blast |
1201 obtain C1' C2' |
1200 obtain C1' C2' |
1202 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1201 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
1203 da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1202 da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
1204 A': "nrm A' = nrm C1' \<union> nrm C2'" |
1203 A': "nrm A' = nrm C1' \<union> nrm C2'" |
1205 "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')" |
1204 "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')" |
1206 by (rule da_elim_cases) auto |
1205 by cases auto |
1207 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1206 note `PROP ?Hyp Env B \<langle>c1\<rangle> C1` |
1208 moreover note B' = `B \<subseteq> B'` |
1207 moreover note B' = `B \<subseteq> B'` |
1209 moreover note da_c1' |
1208 moreover note da_c1' |
1210 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1209 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
1211 by blast |
1210 by blast |
1215 by - (drule hyp_c2,auto) |
1214 by - (drule hyp_c2,auto) |
1216 with A A' C1' |
1215 with A A' C1' |
1217 show ?case |
1216 show ?case |
1218 by auto |
1217 by auto |
1219 next |
1218 next |
1220 case Init thus ?case by - (erule da_elim_cases, auto) |
1219 case Init thus ?case by (elim da_elim_cases) auto |
1221 next |
1220 next |
1222 case NewC thus ?case by - (erule da_elim_cases, auto) |
1221 case NewC thus ?case by (elim da_elim_cases) auto |
1223 next |
1222 next |
1224 case NewA thus ?case by - (erule da_elim_cases, auto) |
1223 case NewA thus ?case by (elim da_elim_cases) auto |
1225 next |
1224 next |
1226 case Cast thus ?case by - (erule da_elim_cases, auto) |
1225 case Cast thus ?case by (elim da_elim_cases) auto |
1227 next |
1226 next |
1228 case Inst thus ?case by - (erule da_elim_cases, auto) |
1227 case Inst thus ?case by (elim da_elim_cases) auto |
1229 next |
1228 next |
1230 case Lit thus ?case by - (erule da_elim_cases, auto) |
1229 case Lit thus ?case by (elim da_elim_cases) auto |
1231 next |
1230 next |
1232 case UnOp thus ?case by - (erule da_elim_cases, auto) |
1231 case UnOp thus ?case by (elim da_elim_cases) auto |
1233 next |
1232 next |
1234 case (CondAnd Env B e1 E1 e2 E2 A B' A') |
1233 case (CondAnd Env B e1 E1 e2 E2 A B' A') |
1235 note A = `nrm A = B \<union> |
1234 note A = `nrm A = B \<union> |
1236 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
1235 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
1237 assigns_if False (BinOp CondAnd e1 e2)` |
1236 assigns_if False (BinOp CondAnd e1 e2)` |
1239 from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'` |
1238 from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'` |
1240 obtain A': "nrm A' = B' \<union> |
1239 obtain A': "nrm A' = B' \<union> |
1241 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
1240 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
1242 assigns_if False (BinOp CondAnd e1 e2)" |
1241 assigns_if False (BinOp CondAnd e1 e2)" |
1243 "brk A' = (\<lambda>l. UNIV)" |
1242 "brk A' = (\<lambda>l. UNIV)" |
1244 by (rule da_elim_cases) auto |
1243 by cases auto |
1245 note B' = `B \<subseteq> B'` |
1244 note B' = `B \<subseteq> B'` |
1246 with A A' show ?case |
1245 with A A' show ?case |
1247 by auto |
1246 by auto |
1248 next |
1247 next |
1249 case CondOr thus ?case by - (erule da_elim_cases, auto) |
1248 case CondOr thus ?case by (elim da_elim_cases) auto |
1250 next |
1249 next |
1251 case BinOp thus ?case by - (erule da_elim_cases, auto) |
1250 case BinOp thus ?case by (elim da_elim_cases) auto |
1252 next |
1251 next |
1253 case Super thus ?case by - (erule da_elim_cases, auto) |
1252 case Super thus ?case by (elim da_elim_cases) auto |
1254 next |
1253 next |
1255 case AccLVar thus ?case by - (erule da_elim_cases, auto) |
1254 case AccLVar thus ?case by (elim da_elim_cases) auto |
1256 next |
1255 next |
1257 case Acc thus ?case by - (erule da_elim_cases, auto) |
1256 case Acc thus ?case by (elim da_elim_cases) auto |
1258 next |
1257 next |
1259 case AssLVar thus ?case by - (erule da_elim_cases, auto) |
1258 case AssLVar thus ?case by (elim da_elim_cases) auto |
1260 next |
1259 next |
1261 case Ass thus ?case by - (erule da_elim_cases, auto) |
1260 case Ass thus ?case by (elim da_elim_cases) auto |
1262 next |
1261 next |
1263 case (CondBool Env c e1 e2 B C E1 E2 A B' A') |
1262 case (CondBool Env c e1 e2 B C E1 E2 A B' A') |
1264 note A = `nrm A = B \<union> |
1263 note A = `nrm A = B \<union> |
1265 assigns_if True (c ? e1 : e2) \<inter> |
1264 assigns_if True (c ? e1 : e2) \<inter> |
1266 assigns_if False (c ? e1 : e2)` |
1265 assigns_if False (c ? e1 : e2)` |
1271 ultimately |
1270 ultimately |
1272 obtain A': "nrm A' = B' \<union> |
1271 obtain A': "nrm A' = B' \<union> |
1273 assigns_if True (c ? e1 : e2) \<inter> |
1272 assigns_if True (c ? e1 : e2) \<inter> |
1274 assigns_if False (c ? e1 : e2)" |
1273 assigns_if False (c ? e1 : e2)" |
1275 "brk A' = (\<lambda>l. UNIV)" |
1274 "brk A' = (\<lambda>l. UNIV)" |
1276 by - (erule da_elim_cases,auto simp add: inj_term_simps) |
1275 by (elim da_elim_cases) (auto simp add: inj_term_simps) |
1277 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
1276 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
1278 note B' = `B \<subseteq> B'` |
1277 note B' = `B \<subseteq> B'` |
1279 with A A' show ?case |
1278 with A A' show ?case |
1280 by auto |
1279 by auto |
1281 next |
1280 next |
1287 where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and |
1286 where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and |
1288 da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and |
1287 da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and |
1289 A': "nrm A' = nrm E1' \<inter> nrm E2'" |
1288 A': "nrm A' = nrm E1' \<inter> nrm E2'" |
1290 "brk A' = (\<lambda>l. UNIV)" |
1289 "brk A' = (\<lambda>l. UNIV)" |
1291 using not_bool |
1290 using not_bool |
1292 by - (erule da_elim_cases, auto simp add: inj_term_simps) |
1291 by (elim da_elim_cases) (auto simp add: inj_term_simps) |
1293 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
1292 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
1294 note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1` |
1293 note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1` |
1295 moreover note B' = `B \<subseteq> B'` |
1294 moreover note B' = `B \<subseteq> B'` |
1296 moreover note da_e1' |
1295 moreover note da_e1' |
1297 ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)" |
1296 ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)" |
1306 next |
1305 next |
1307 case Call |
1306 case Call |
1308 from Call.prems and Call.hyps |
1307 from Call.prems and Call.hyps |
1309 show ?case by cases auto |
1308 show ?case by cases auto |
1310 next |
1309 next |
1311 case Methd thus ?case by - (erule da_elim_cases, auto) |
1310 case Methd thus ?case by (elim da_elim_cases) auto |
1312 next |
1311 next |
1313 case Body thus ?case by - (erule da_elim_cases, auto) |
1312 case Body thus ?case by (elim da_elim_cases) auto |
1314 next |
1313 next |
1315 case LVar thus ?case by - (erule da_elim_cases, auto) |
1314 case LVar thus ?case by (elim da_elim_cases) auto |
1316 next |
1315 next |
1317 case FVar thus ?case by - (erule da_elim_cases, auto) |
1316 case FVar thus ?case by (elim da_elim_cases) auto |
1318 next |
1317 next |
1319 case AVar thus ?case by - (erule da_elim_cases, auto) |
1318 case AVar thus ?case by (elim da_elim_cases) auto |
1320 next |
1319 next |
1321 case Nil thus ?case by - (erule da_elim_cases, auto) |
1320 case Nil thus ?case by (elim da_elim_cases) auto |
1322 next |
1321 next |
1323 case Cons thus ?case by - (erule da_elim_cases, auto) |
1322 case Cons thus ?case by (elim da_elim_cases) auto |
1324 qed |
1323 qed |
1325 qed (rule da', rule `B \<subseteq> B'`) |
1324 qed (rule da', rule `B \<subseteq> B'`) |
1326 |
1325 |
1327 lemma da_weaken: |
1326 lemma da_weaken: |
1328 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" |
1327 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" |