[STATEMENT]
lemma assumes wf: "wf_prog wfmd P"
  shows WT1_unique: "P,E \<turnstile>1 e :: T1 \<Longrightarrow> P,E \<turnstile>1 e :: T2 \<Longrightarrow> T1 = T2"
  and WTs1_unique: "P,E \<turnstile>1 es [::] Ts1 \<Longrightarrow> P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts1 = Ts2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,E \<turnstile>1 e :: T1; P,E \<turnstile>1 e :: T2\<rbrakk> \<Longrightarrow> T1 = T2) &&& (\<lbrakk>P,E \<turnstile>1 es [::] Ts1; P,E \<turnstile>1 es [::] Ts2\<rbrakk> \<Longrightarrow> Ts1 = Ts2)
[PROOF STEP]
apply(induct arbitrary: T2 and Ts2 rule:WT1_WTs1.inducts)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>C E T2. \<lbrakk>is_class P C; P,E \<turnstile>1 new C :: T2\<rbrakk> \<Longrightarrow> Class C = T2
 2. \<And>E e T T2. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Integer = T2; is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 newA T\<lfloor>e\<rceil> :: T2\<rbrakk> \<Longrightarrow> T\<lfloor>\<rceil> = T2
 3. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; P,E \<turnstile>1 Cast U e :: T2\<rbrakk> \<Longrightarrow> U = T2
 4. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; P,E \<turnstile>1 e instanceof U :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 5. \<And>v T E T2. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; P,E \<turnstile>1 Val v :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 8. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 9. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 10. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
A total of 24 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>E e T T2. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Integer = T2; is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 newA T\<lfloor>e\<rceil> :: T2\<rbrakk> \<Longrightarrow> T\<lfloor>\<rceil> = T2
 2. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; P,E \<turnstile>1 Cast U e :: T2\<rbrakk> \<Longrightarrow> U = T2
 3. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; P,E \<turnstile>1 e instanceof U :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 4. \<And>v T E T2. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; P,E \<turnstile>1 Val v :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 7. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 10. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
A total of 23 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; P,E \<turnstile>1 Cast U e :: T2\<rbrakk> \<Longrightarrow> U = T2
 2. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; P,E \<turnstile>1 e instanceof U :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 3. \<And>v T E T2. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; P,E \<turnstile>1 Val v :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 6. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 8. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 9. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 10. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
A total of 22 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>E e T U T2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; P,E \<turnstile>1 e instanceof U :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 2. \<And>v T E T2. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; P,E \<turnstile>1 Val v :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 5. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 6. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 9. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 10. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
A total of 21 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. \<And>v T E T2. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; P,E \<turnstile>1 Val v :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 4. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 5. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 8. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 10. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
A total of 20 subgoals...
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>E V T T2. \<lbrakk>E ! V = T; V < length E; P,E \<turnstile>1 Var V :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 3. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 4. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 6. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 7. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 8. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 9. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 10. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
A total of 19 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>E e1 T1 e2 T2 bop T T2a. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> T1 = T2; P,E \<turnstile>1 e2 :: T2; \<And>T2a. P,E \<turnstile>1 e2 :: T2a \<Longrightarrow> T2 = T2a; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; P,E \<turnstile>1 e1 \<guillemotleft>bop\<guillemotright> e2 :: T2a\<rbrakk> \<Longrightarrow> T = T2a
 2. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 3. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 5. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 6. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 9. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 10. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
A total of 18 subgoals...
[PROOF STEP]
apply(blast dest: WT_binop_fun)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>E i T e T' T2. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 i:=e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 2. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 4. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 5. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 8. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 10. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
A total of 17 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>E a T i T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 a\<lfloor>i\<rceil> :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 3. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 4. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 6. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 7. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 8. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 9. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 10. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
A total of 16 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>E a T i e T' T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 i :: Integer; \<And>T2. P,E \<turnstile>1 i :: T2 \<Longrightarrow> Integer = T2; P,E \<turnstile>1 e :: T'; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 a\<lfloor>i\<rceil> := e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 2. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 3. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 5. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 6. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 8. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 9. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 10. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
A total of 15 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>E a T T2. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<And>T2. P,E \<turnstile>1 a :: T2 \<Longrightarrow> T\<lfloor>\<rceil> = T2; P,E \<turnstile>1 a\<bullet>length :: T2\<rbrakk> \<Longrightarrow> Integer = T2
 2. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 4. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 5. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 7. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 8. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 9. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 10. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
A total of 14 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>E e U C F T fm D T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e\<bullet>F{D} :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 3. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 4. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 6. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 7. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 8. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 10. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
A total of 13 subgoals...
[PROOF STEP]
apply (blast dest:sees_field_idemp sees_field_fun)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>E e1 U C F T fm D e2 T' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e1\<bullet>F{D} := e2 :: T2\<rbrakk> \<Longrightarrow> Void = T2
 2. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 3. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 5. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 6. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 7. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 8. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 9. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 10. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
A total of 12 subgoals...
[PROOF STEP]
apply (blast dest: sees_field_fun)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>E e1 U C F T fm D e2 T' e3 T'' T2. \<lbrakk>P,E \<turnstile>1 e1 :: U; \<And>T2. P,E \<turnstile>1 e1 :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; \<And>T2. P,E \<turnstile>1 e2 :: T2 \<Longrightarrow> T' = T2; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; \<And>T2. P,E \<turnstile>1 e3 :: T2 \<Longrightarrow> T'' = T2; P \<turnstile> T'' \<le> T; P,E \<turnstile>1 e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3) :: T2\<rbrakk> \<Longrightarrow> Boolean = T2
 2. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 4. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 5. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 6. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 9. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 10. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
A total of 11 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E e U C M Ts T m D es Ts' T2. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e\<bullet>M(es) :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 3. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 4. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 5. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 10. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply(erule WT1_WTs1_cases)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E e U C M Ts T m D es Ts' T2 Ua Ca Tsa ma Da Ts'a. \<lbrakk>P,E \<turnstile>1 e :: U; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts' [\<le>] Ts; P,E \<turnstile>1 e :: Ua; class_type_of' Ua = \<lfloor>Ca\<rfloor>; P \<turnstile> Ca sees M: Tsa\<rightarrow>T2 = ma in Da; P,E \<turnstile>1 es [::] Ts'a; P \<turnstile> Ts'a [\<le>] Tsa\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 3. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 4. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 5. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 10. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E e U C M Ts T m D es Ts' T2 Ua Ca Tsa ma Da Ts'a. \<lbrakk>\<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> U = T2; Ca = C; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts' = Ts2; P \<turnstile> Ts'a [\<le>] Ts; P,E \<turnstile>1 e :: Ua; class_type_of' Ua = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Tsa\<rightarrow>T2 = ma in Da; P,E \<turnstile>1 es [::] Ts'a; P \<turnstile> Ts'a [\<le>] Tsa\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 3. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 4. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 5. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 8. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 9. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 10. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply (blast dest:sees_method_idemp sees_method_fun)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>T E e T' vo V T2. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; \<And>T2. P,E @ [T] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P,E \<turnstile>1 {V:T=vo; e} :: T2\<rbrakk> \<Longrightarrow> T' = T2
 2. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 3. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 4. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 6. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 7. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 8. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 9. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>E o' T e T' V T2. \<lbrakk>P,E \<turnstile>1 o' :: T; \<And>T2. P,E \<turnstile>1 o' :: T2 \<Longrightarrow> T = T2; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; \<And>T2. P,E @ [Class Object] \<turnstile>1 e :: T2 \<Longrightarrow> T' = T2; P,E \<turnstile>1 sync\<^bsub>V\<^esub> (o') e :: T2\<rbrakk> \<Longrightarrow> T' = T2
 2. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 3. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 5. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 6. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 7. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 8. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P,E \<turnstile>1 e\<^sub>1;; e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T\<^sub>2 = T2
 2. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 4. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 5. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 6. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 7. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T\<^sub>1 = T2; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; \<And>T2. P,E \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T\<^sub>2 = T2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; P,E \<turnstile>1 if (e) e\<^sub>1 else e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 3. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 4. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 5. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 6. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply(blast dest: is_lub_unique[OF wf])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>E e c T T2. \<lbrakk>P,E \<turnstile>1 e :: Boolean; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Boolean = T2; P,E \<turnstile>1 c :: T; \<And>T2. P,E \<turnstile>1 c :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 while (e) c :: T2\<rbrakk> \<Longrightarrow> Void = T2
 2. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 3. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 4. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 5. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>E e C T2. \<lbrakk>P,E \<turnstile>1 e :: Class C; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> Class C = T2; P \<turnstile> C \<preceq>\<^sup>* Throwable; P,E \<turnstile>1 throw e :: T2\<rbrakk> \<Longrightarrow> Void = T2
 2. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 3. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 4. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>E e\<^sub>1 T C e\<^sub>2 V T2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; \<And>T2. P,E \<turnstile>1 e\<^sub>1 :: T2 \<Longrightarrow> T = T2; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; \<And>T2. P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T2 \<Longrightarrow> T = T2; is_class P C; P,E \<turnstile>1 try e\<^sub>1 catch(C V) e\<^sub>2 :: T2\<rbrakk> \<Longrightarrow> T = T2
 2. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 3. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>E Ts2. P,E \<turnstile>1 [] [::] Ts2 \<Longrightarrow> [] = Ts2
 2. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>E e T es Ts Ts2. \<lbrakk>P,E \<turnstile>1 e :: T; \<And>T2. P,E \<turnstile>1 e :: T2 \<Longrightarrow> T = T2; P,E \<turnstile>1 es [::] Ts; \<And>Ts2. P,E \<turnstile>1 es [::] Ts2 \<Longrightarrow> Ts = Ts2; P,E \<turnstile>1 e # es [::] Ts2\<rbrakk> \<Longrightarrow> T # Ts = Ts2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done