[STATEMENT]
lemma assumes wf: "wf_prog p P"
  shows WT1_is_type: "P,E \<turnstile>1 e :: T \<Longrightarrow> set E \<subseteq> types P \<Longrightarrow> is_type P T"
  and WTs1_is_type: "P,E \<turnstile>1 es [::] Ts \<Longrightarrow> set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T) &&& (\<lbrakk>P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set Ts \<subseteq> types P)
[PROOF STEP]
apply(induct rule:WT1_WTs1.inducts)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P (Class C)
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P (T\<lfloor>\<rceil>)
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P U
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
A total of 24 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P (T\<lfloor>\<rceil>)
 2. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P U
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 4. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 8. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 9. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 10. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
A total of 23 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P U
 2. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 3. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 7. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 9. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 10. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
A total of 22 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 2. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 6. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 8. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 9. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 10. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
A total of 21 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 5. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 7. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 8. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 9. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 10. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
A total of 20 subgoals...
[PROOF STEP]
apply (simp add:typeof_lit_is_type)
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>E V T. \<lbrakk>E ! V = T; V < length E; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 4. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 6. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 7. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 9. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 10. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
A total of 19 subgoals...
[PROOF STEP]
apply (fastforce intro:nth_mem)
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; set E \<subseteq> types P \<Longrightarrow> is_type P T1; P,E \<turnstile>1 e2 :: T2; set E \<subseteq> types P \<Longrightarrow> is_type P T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 3. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 5. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 6. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 8. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 9. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 10. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
A total of 18 subgoals...
[PROOF STEP]
apply(simp add: WT_binop_is_type)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 2. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 4. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 5. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 7. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 8. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 9. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 10. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
A total of 17 subgoals...
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 3. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 4. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 6. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 7. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 9. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 10. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
A total of 16 subgoals...
[PROOF STEP]
apply(simp del: is_type_array add: is_type_ArrayD)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); P,E \<turnstile>1 i :: Integer; set E \<subseteq> types P \<Longrightarrow> is_type P Integer; P,E \<turnstile>1 e :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 2. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 3. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 5. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 6. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 8. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 9. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 10. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
A total of 15 subgoals...
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>E a T. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; set E \<subseteq> types P \<Longrightarrow> is_type P (T\<lfloor>\<rceil>); set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Integer
 2. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 4. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 5. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 7. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 8. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 9. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 10. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
A total of 14 subgoals...
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>E e U C F T fm D. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 3. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 4. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 6. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 7. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 8. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 9. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 10. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
A total of 13 subgoals...
[PROOF STEP]
apply (simp add:sees_field_is_type[OF _ wf])
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>E e1 U C F T fm D e2 T'. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 2. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 3. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 5. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 6. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 7. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 9. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 10. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
A total of 12 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>E e1 U C F T fm D e2 T' e3 T''. \<lbrakk>P,E \<turnstile>1 e1 :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees F:T (fm) in D; volatile fm; P,E \<turnstile>1 e2 :: T'; set E \<subseteq> types P \<Longrightarrow> is_type P T'; P \<turnstile> T' \<le> T; P,E \<turnstile>1 e3 :: T''; set E \<subseteq> types P \<Longrightarrow> is_type P T''; P \<turnstile> T'' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Boolean
 2. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 4. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 5. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 6. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 8. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 9. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 10. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
A total of 11 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E e U C M Ts T m D es Ts'. \<lbrakk>P,E \<turnstile>1 e :: U; set E \<subseteq> types P \<Longrightarrow> is_type P U; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P,E \<turnstile>1 es [::] Ts'; set E \<subseteq> types P \<Longrightarrow> set Ts' \<subseteq> types P; P \<turnstile> Ts' [\<le>] Ts; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 3. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 4. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 5. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 7. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 8. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 9. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 10. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply(fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>T E e T' vo V. \<lbrakk>is_type P T; P,E @ [T] \<turnstile>1 e :: T'; set (E @ [T]) \<subseteq> types P \<Longrightarrow> is_type P T'; case vo of None \<Rightarrow> True | \<lfloor>v\<rfloor> \<Rightarrow> \<exists>T'. typeof v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 2. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 3. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 4. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 6. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 7. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 8. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 9. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>E o' T e T' V. \<lbrakk>P,E \<turnstile>1 o' :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; is_refT T; T \<noteq> NT; P,E @ [Class Object] \<turnstile>1 e :: T'; set (E @ [Class Object]) \<subseteq> types P \<Longrightarrow> is_type P T'; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T'
 2. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 3. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 5. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 6. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 7. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 8. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply(simp add: is_class_Object[OF wf])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>E e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T\<^sub>2
 2. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 4. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 5. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 6. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 7. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 e\<^sub>1 :: T\<^sub>1; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>1; P,E \<turnstile>1 e\<^sub>2 :: T\<^sub>2; set E \<subseteq> types P \<Longrightarrow> is_type P T\<^sub>2; P \<turnstile> lub(T\<^sub>1, T\<^sub>2) = T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 3. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 4. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 5. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 6. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply(blast dest: is_lub_is_type[OF wf])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>E e c T. \<lbrakk>P,E \<turnstile>1 e :: Boolean; set E \<subseteq> types P \<Longrightarrow> is_type P Boolean; P,E \<turnstile>1 c :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 2. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 3. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 4. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 5. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>E e C. \<lbrakk>P,E \<turnstile>1 e :: Class C; set E \<subseteq> types P \<Longrightarrow> is_type P (Class C); P \<turnstile> C \<preceq>\<^sup>* Throwable; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P Void
 2. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 3. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 4. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>E e\<^sub>1 T C e\<^sub>2 V. \<lbrakk>P,E \<turnstile>1 e\<^sub>1 :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E @ [Class C] \<turnstile>1 e\<^sub>2 :: T; set (E @ [Class C]) \<subseteq> types P \<Longrightarrow> is_type P T; is_class P C; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 3. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>E. set E \<subseteq> types P \<Longrightarrow> set [] \<subseteq> types P
 2. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>E e T es Ts. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P \<Longrightarrow> is_type P T; P,E \<turnstile>1 es [::] Ts; set E \<subseteq> types P \<Longrightarrow> set Ts \<subseteq> types P; set E \<subseteq> types P\<rbrakk> \<Longrightarrow> set (T # Ts) \<subseteq> types P
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma blocks1_WT:
  "\<lbrakk> P,Env @ Ts \<turnstile>1 body :: T; set Ts \<subseteq> types P \<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) Ts body :: T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,Env @ Ts \<turnstile>1 body :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) Ts body :: T
[PROOF STEP]
proof(induct n\<equiv>"length Env" Ts body arbitrary: Env rule: blocks1.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e Env. \<lbrakk>P,Env @ [] \<turnstile>1 e :: T; set [] \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) [] e :: T
 2. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
P,Env @ [] \<turnstile>1 e_ :: T
set [] \<subseteq> types P

goal (2 subgoals):
 1. \<And>e Env. \<lbrakk>P,Env @ [] \<turnstile>1 e :: T; set [] \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) [] e :: T
 2. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,Env @ [] \<turnstile>1 e_ :: T
set [] \<subseteq> types P

goal (1 subgoal):
 1. P,Env \<turnstile>1 blocks1 (length Env) [] e_ :: T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,Env \<turnstile>1 blocks1 (length Env) [] e_ :: T

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
case (2 T' Ts e)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Suc (length Env) = length ?Env; P,?Env @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,?Env \<turnstile>1 blocks1 (length ?Env) Ts e :: T
P,Env @ T' # Ts \<turnstile>1 e :: T
set (T' # Ts) \<subseteq> types P

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
note IH = \<open>\<And>Env'. \<lbrakk>Suc (length Env) = length Env'; P,Env' @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P \<rbrakk>
              \<Longrightarrow> P,Env' \<turnstile>1 blocks1 (length Env') Ts e :: T\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>Suc (length Env) = length ?Env'; P,?Env' @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,?Env' \<turnstile>1 blocks1 (length ?Env') Ts e :: T

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
from \<open>set (T' # Ts) \<subseteq> types P\<close>
[PROOF STATE]
proof (chain)
picking this:
set (T' # Ts) \<subseteq> types P
[PROOF STEP]
have "set Ts \<subseteq> types P" "is_type P T'"
[PROOF STATE]
proof (prove)
using this:
set (T' # Ts) \<subseteq> types P

goal (1 subgoal):
 1. set Ts \<subseteq> types P &&& is_type P T'
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P
is_type P T'

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P
is_type P T'

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
from \<open>P,Env @ T' # Ts \<turnstile>1 e :: T\<close>
[PROOF STATE]
proof (chain)
picking this:
P,Env @ T' # Ts \<turnstile>1 e :: T
[PROOF STEP]
have "P,(Env @ [T']) @ Ts \<turnstile>1 e :: T"
[PROOF STATE]
proof (prove)
using this:
P,Env @ T' # Ts \<turnstile>1 e :: T

goal (1 subgoal):
 1. P,(Env @ [T']) @ Ts \<turnstile>1 e :: T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,(Env @ [T']) @ Ts \<turnstile>1 e :: T

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
note IH[OF _ this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>Suc (length Env) = length (Env @ [T']); set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env @ [T'] \<turnstile>1 blocks1 (length (Env @ [T'])) Ts e :: T

goal (1 subgoal):
 1. \<And>Ta Ts e Env. \<lbrakk>\<And>Enva. \<lbrakk>Suc (length Env) = length Enva; P,Enva @ Ts \<turnstile>1 e :: T; set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Enva \<turnstile>1 blocks1 (length Enva) Ts e :: T; P,Env @ Ta # Ts \<turnstile>1 e :: T; set (Ta # Ts) \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env \<turnstile>1 blocks1 (length Env) (Ta # Ts) e :: T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set Ts \<subseteq> types P
is_type P T'
\<lbrakk>Suc (length Env) = length (Env @ [T']); set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env @ [T'] \<turnstile>1 blocks1 (length (Env @ [T'])) Ts e :: T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set Ts \<subseteq> types P
is_type P T'
\<lbrakk>Suc (length Env) = length (Env @ [T']); set Ts \<subseteq> types P\<rbrakk> \<Longrightarrow> P,Env @ [T'] \<turnstile>1 blocks1 (length (Env @ [T'])) Ts e :: T

goal (1 subgoal):
 1. P,Env \<turnstile>1 blocks1 (length Env) (T' # Ts) e :: T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,Env \<turnstile>1 blocks1 (length Env) (T' # Ts) e :: T

goal:
No subgoals!
[PROOF STEP]
qed