[STATEMENT]
lemma WT1_fv: "\<lbrakk> P,E \<turnstile>1 e :: T; \<B> e (length E); syncvars e \<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}"
  and WTs1_fvs: "\<lbrakk> P,E \<turnstile>1 es [::] Ts; \<B>s es (length E); syncvarss es \<rbrakk> \<Longrightarrow> fvs es \<subseteq> {0..<length E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,E \<turnstile>1 e :: T; \<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}) &&& (\<lbrakk>P,E \<turnstile>1 es [::] Ts; \<B>s es (length E); syncvarss es\<rbrakk> \<Longrightarrow> fvs es \<subseteq> {0..<length E})
[PROOF STEP]
proof(induct rule: WT1_WTs1.inducts)
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
case (WT1Synchronized E e1 T e2 T' V)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile>1 e1 :: T
\<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}
is_refT T
T \<noteq> NT
P,E @ [Class Object] \<turnstile>1 e2 :: T'
\<lbrakk>\<B> e2 (length (E @ [Class Object])); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length (E @ [Class Object])}
\<B> (sync\<^bsub>V\<^esub> (e1) e2) (length E)
syncvars (sync\<^bsub>V\<^esub> (e1) e2)

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
note IH1 = \<open>\<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
note IH2 = \<open>\<lbrakk>\<B> e2 (length (E @ [Class Object])); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length (E @ [Class Object])}\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<B> e2 (length (E @ [Class Object])); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length (E @ [Class Object])}

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
from \<open>\<B> (sync\<^bsub>V\<^esub> (e1) e2) (length E)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<B> (sync\<^bsub>V\<^esub> (e1) e2) (length E)
[PROOF STEP]
have [simp]: "V = length E"
    and B1: "\<B> e1 (length E)" and B2: "\<B> e2 (Suc (length E))"
[PROOF STATE]
proof (prove)
using this:
\<B> (sync\<^bsub>V\<^esub> (e1) e2) (length E)

goal (1 subgoal):
 1. V = length E &&& \<B> e1 (length E) &&& \<B> e2 (Suc (length E))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V = length E
\<B> e1 (length E)
\<B> e2 (Suc (length E))

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
from \<open>syncvars (sync\<^bsub>V\<^esub> (e1) e2)\<close>
[PROOF STATE]
proof (chain)
picking this:
syncvars (sync\<^bsub>V\<^esub> (e1) e2)
[PROOF STEP]
have sync1: "syncvars e1" and sync2: "syncvars e2" and V: "V \<notin> fv e2"
[PROOF STATE]
proof (prove)
using this:
syncvars (sync\<^bsub>V\<^esub> (e1) e2)

goal (1 subgoal):
 1. syncvars e1 &&& syncvars e2 &&& V \<notin> fv e2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
syncvars e1
syncvars e2
V \<notin> fv e2

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
have "fv e2 \<subseteq> {0..<length E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv e2 \<subseteq> {0..<length E}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
assume x: "x \<in> fv e2"
[PROOF STATE]
proof (state)
this:
x \<in> fv e2

goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
with V
[PROOF STATE]
proof (chain)
picking this:
V \<notin> fv e2
x \<in> fv e2
[PROOF STEP]
have "x \<noteq> length E"
[PROOF STATE]
proof (prove)
using this:
V \<notin> fv e2
x \<in> fv e2

goal (1 subgoal):
 1. x \<noteq> length E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> length E

goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> length E

goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
from IH2 B2 sync2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<B> e2 (length (E @ [Class Object])); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length (E @ [Class Object])}
\<B> e2 (Suc (length E))
syncvars e2
[PROOF STEP]
have "fv e2 \<subseteq> {0..<Suc (length E)}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<B> e2 (length (E @ [Class Object])); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length (E @ [Class Object])}
\<B> e2 (Suc (length E))
syncvars e2

goal (1 subgoal):
 1. fv e2 \<subseteq> {0..<Suc (length E)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv e2 \<subseteq> {0..<Suc (length E)}

goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<in> fv e2
fv e2 \<subseteq> {0..<Suc (length E)}
[PROOF STEP]
have "x < Suc (length E)"
[PROOF STATE]
proof (prove)
using this:
x \<in> fv e2
fv e2 \<subseteq> {0..<Suc (length E)}

goal (1 subgoal):
 1. x < Suc (length E)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < Suc (length E)

goal (1 subgoal):
 1. \<And>x. x \<in> fv e2 \<Longrightarrow> x \<in> {0..<length E}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> length E
x < Suc (length E)
[PROOF STEP]
show "x \<in> {0..<length E}"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> length E
x < Suc (length E)

goal (1 subgoal):
 1. x \<in> {0..<length E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {0..<length E}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fv e2 \<subseteq> {0..<length E}

goal (24 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 24 subgoals...
[PROOF STEP]
with IH1[OF B1 sync1]
[PROOF STATE]
proof (chain)
picking this:
fv e1 \<subseteq> {0..<length E}
fv e2 \<subseteq> {0..<length E}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fv e1 \<subseteq> {0..<length E}
fv e2 \<subseteq> {0..<length E}

goal (1 subgoal):
 1. fv (sync\<^bsub>V\<^esub> (e1) e2) \<subseteq> {0..<length E}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
fv (sync\<^bsub>V\<^esub> (e1) e2) \<subseteq> {0..<length E}

goal (23 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 23 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 23 subgoals...
[PROOF STEP]
case (WT1Cond E e e1 T1 e2 T2 T)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile>1 e :: Boolean
\<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}
P,E \<turnstile>1 e1 :: T1
\<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}
P,E \<turnstile>1 e2 :: T2
\<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}
P \<turnstile> lub(T1, T2) = T
\<B> (if (e) e1 else e2) (length E)
syncvars (if (e) e1 else e2)

goal (23 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 23 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile>1 e :: Boolean
\<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}
P,E \<turnstile>1 e1 :: T1
\<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}
P,E \<turnstile>1 e2 :: T2
\<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}
P \<turnstile> lub(T1, T2) = T
\<B> (if (e) e1 else e2) (length E)
syncvars (if (e) e1 else e2)

goal (1 subgoal):
 1. fv (if (e) e1 else e2) \<subseteq> {0..<length E}
[PROOF STEP]
by(auto del: subsetI)
[PROOF STATE]
proof (state)
this:
fv (if (e) e1 else e2) \<subseteq> {0..<length E}

goal (22 subgoals):
 1. \<And>C E. \<lbrakk>is_class P C; \<B> (new C) (length E); syncvars (new C)\<rbrakk> \<Longrightarrow> fv (new C) \<subseteq> {0..<length E}
 2. \<And>E e T. \<lbrakk>P,E \<turnstile>1 e :: Integer; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; is_type P (T\<lfloor>\<rceil>); \<B> (newA T\<lfloor>e\<rceil>) (length E); syncvars (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> fv (newA T\<lfloor>e\<rceil>) \<subseteq> {0..<length E}
 3. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; \<B> (Cast U e) (length E); syncvars (Cast U e)\<rbrakk> \<Longrightarrow> fv (Cast U e) \<subseteq> {0..<length E}
 4. \<And>E e T U. \<lbrakk>P,E \<turnstile>1 e :: T; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U; \<B> (e instanceof U) (length E); syncvars (e instanceof U)\<rbrakk> \<Longrightarrow> fv (e instanceof U) \<subseteq> {0..<length E}
 5. \<And>v T E. \<lbrakk>typeof v = \<lfloor>T\<rfloor>; \<B> (Val v) (length E); syncvars (Val v)\<rbrakk> \<Longrightarrow> fv (Val v) \<subseteq> {0..<length E}
 6. \<And>E V T. \<lbrakk>E ! V = T; V < length E; \<B> (Var V) (length E); syncvars (Var V)\<rbrakk> \<Longrightarrow> fv (Var V) \<subseteq> {0..<length E}
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>P,E \<turnstile>1 e1 :: T1; \<lbrakk>\<B> e1 (length E); syncvars e1\<rbrakk> \<Longrightarrow> fv e1 \<subseteq> {0..<length E}; P,E \<turnstile>1 e2 :: T2; \<lbrakk>\<B> e2 (length E); syncvars e2\<rbrakk> \<Longrightarrow> fv e2 \<subseteq> {0..<length E}; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T; \<B> (e1 \<guillemotleft>bop\<guillemotright> e2) (length E); syncvars (e1 \<guillemotleft>bop\<guillemotright> e2)\<rbrakk> \<Longrightarrow> fv (e1 \<guillemotleft>bop\<guillemotright> e2) \<subseteq> {0..<length E}
 8. \<And>E i T e T'. \<lbrakk>E ! i = T; i < length E; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (i:=e) (length E); syncvars (i:=e)\<rbrakk> \<Longrightarrow> fv (i:=e) \<subseteq> {0..<length E}
 9. \<And>E a T i. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; \<B> (a\<lfloor>i\<rceil>) (length E); syncvars (a\<lfloor>i\<rceil>)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil>) \<subseteq> {0..<length E}
 10. \<And>E a T i e T'. \<lbrakk>P,E \<turnstile>1 a :: T\<lfloor>\<rceil>; \<lbrakk>\<B> a (length E); syncvars a\<rbrakk> \<Longrightarrow> fv a \<subseteq> {0..<length E}; P,E \<turnstile>1 i :: Integer; \<lbrakk>\<B> i (length E); syncvars i\<rbrakk> \<Longrightarrow> fv i \<subseteq> {0..<length E}; P,E \<turnstile>1 e :: T'; \<lbrakk>\<B> e (length E); syncvars e\<rbrakk> \<Longrightarrow> fv e \<subseteq> {0..<length E}; P \<turnstile> T' \<le> T; \<B> (a\<lfloor>i\<rceil> := e) (length E); syncvars (a\<lfloor>i\<rceil> := e)\<rbrakk> \<Longrightarrow> fv (a\<lfloor>i\<rceil> := e) \<subseteq> {0..<length E}
A total of 22 subgoals...
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma top_mult_right_one:
  "x * top = x * top * 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top = x * top * (1::'a)
[PROOF STEP]
by (metis order.antisym mult_sub_right_one mult_sup_associative_one surjective_one_closed)


[STATEMENT]
lemma mult_left_sub_dist_inf_left:
  "x * (y \<sqinter> z) \<le> x * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z) \<le> x * y
[PROOF STEP]
by (simp add: mult_right_isotone)


[STATEMENT]
lemma mult_left_sub_dist_inf_right:
  "x * (y \<sqinter> z) \<le> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z) \<le> x * z
[PROOF STEP]
by (simp add: mult_right_isotone)


[STATEMENT]
lemma mult_right_sub_dist_inf_left:
  "(x \<sqinter> y) * z \<le> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * z \<le> x * z
[PROOF STEP]
by (simp add: mult_left_isotone)


[STATEMENT]
lemma mult_right_sub_dist_inf_right:
  "(x \<sqinter> y) * z \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * z \<le> y * z
[PROOF STEP]
by (simp add: mult_left_isotone)


[STATEMENT]
lemma mult_right_sub_dist_inf:
  "(x \<sqinter> y) * z \<le> x * z \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * z \<le> x * z \<sqinter> y * z
[PROOF STEP]
by (simp add: mult_right_sub_dist_inf_left mult_right_sub_dist_inf_right)


[STATEMENT]
lemma reflexive_total:
  "reflexive x \<Longrightarrow> total x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x \<Longrightarrow> times_top_class.total x
[PROOF STEP]
using sup_left_divisibility total_sup_closed
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (\<exists>z. ?x \<squnion> z = ?y)
times_top_class.total ?x \<Longrightarrow> times_top_class.total (?x \<squnion> ?y)

goal (1 subgoal):
 1. reflexive x \<Longrightarrow> times_top_class.total x
[PROOF STEP]
by force


[STATEMENT]
lemma reflexive_dense:
  "reflexive x \<Longrightarrow> dense_rel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x \<Longrightarrow> dense_rel x
[PROOF STEP]
using mult_left_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z

goal (1 subgoal):
 1. reflexive x \<Longrightarrow> dense_rel x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma reflexive_transitive_up_closed:
  "reflexive x \<Longrightarrow> transitive x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; transitive x\<rbrakk> \<Longrightarrow> up_closed x
[PROOF STEP]
by (metis antisym_conv mult_isotone mult_sub_right_one reflexive_dense up_closed_def)


[STATEMENT]
lemma coreflexive_co_total:
  "coreflexive x \<Longrightarrow> co_total x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> co_total x
[PROOF STEP]
by (metis co_total_def order.eq_iff mult_left_isotone mult_left_one bot_least)


[STATEMENT]
lemma idempotent_transitive_dense:
  "idempotent x \<longleftrightarrow> transitive x \<and> dense_rel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent x = (transitive x \<and> dense_rel x)
[PROOF STEP]
by (simp add: order.eq_iff)


[STATEMENT]
lemma contact_reflexive:
  "contact x \<Longrightarrow> reflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x \<Longrightarrow> reflexive x
[PROOF STEP]
using contact_def sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
contact ?x \<equiv> ?x * ?x \<squnion> (1::'a) = ?x
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)

goal (1 subgoal):
 1. contact x \<Longrightarrow> reflexive x
[PROOF STEP]
by auto


[STATEMENT]
lemma contact_transitive:
  "contact x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x \<Longrightarrow> transitive x
[PROOF STEP]
using contact_def sup_left_divisibility
[PROOF STATE]
proof (prove)
using this:
contact ?x \<equiv> ?x * ?x \<squnion> (1::'a) = ?x
(?x \<le> ?y) = (\<exists>z. ?x \<squnion> z = ?y)

goal (1 subgoal):
 1. contact x \<Longrightarrow> transitive x
[PROOF STEP]
by blast


[STATEMENT]
lemma contact_dense:
  "contact x \<Longrightarrow> dense_rel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x \<Longrightarrow> dense_rel x
[PROOF STEP]
by (simp add: contact_reflexive reflexive_dense)


[STATEMENT]
lemma contact_idempotent:
  "contact x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x \<Longrightarrow> idempotent x
[PROOF STEP]
by (simp add: contact_dense contact_transitive idempotent_transitive_dense)


[STATEMENT]
lemma contact_up_closed:
  "contact x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x \<Longrightarrow> up_closed x
[PROOF STEP]
by (simp add: contact_reflexive contact_transitive reflexive_transitive_up_closed)


[STATEMENT]
lemma contact_reflexive_idempotent_up_closed:
  "contact x \<longleftrightarrow> reflexive x \<and> idempotent x \<and> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x = (reflexive x \<and> idempotent x \<and> up_closed x)
[PROOF STEP]
by (metis contact_def contact_idempotent contact_reflexive contact_up_closed sup_absorb2 sup_monoid.add_commute)


[STATEMENT]
lemma kernel_coreflexive:
  "kernel x \<Longrightarrow> coreflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x \<Longrightarrow> coreflexive x
[PROOF STEP]
by (metis kernel_def inf.boundedE mult_sub_right_one)


[STATEMENT]
lemma kernel_transitive:
  "kernel x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x \<Longrightarrow> transitive x
[PROOF STEP]
by (simp add: coreflexive_transitive kernel_coreflexive)


[STATEMENT]
lemma kernel_dense:
  "kernel x \<Longrightarrow> dense_rel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x \<Longrightarrow> dense_rel x
[PROOF STEP]
by (metis kernel_def inf.boundedE mult_sub_right_one)


[STATEMENT]
lemma kernel_idempotent:
  "kernel x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x \<Longrightarrow> idempotent x
[PROOF STEP]
by (simp add: idempotent_transitive_dense kernel_dense kernel_transitive)


[STATEMENT]
lemma kernel_up_closed:
  "kernel x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x \<Longrightarrow> up_closed x
[PROOF STEP]
by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)


[STATEMENT]
lemma kernel_coreflexive_idempotent_up_closed:
  "kernel x \<longleftrightarrow> coreflexive x \<and> idempotent x \<and> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel x = (coreflexive x \<and> idempotent x \<and> up_closed x)
[PROOF STEP]
by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)


[STATEMENT]
lemma test_coreflexive:
  "test x \<Longrightarrow> coreflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> coreflexive x
[PROOF STEP]
using inf.sup_right_divisibility test_def
[PROOF STATE]
proof (prove)
using this:
(?y \<le> ?x) = (\<exists>z. z \<sqinter> ?x = ?y)
test ?x \<equiv> ?x * top \<sqinter> (1::'a) = ?x

goal (1 subgoal):
 1. test x \<Longrightarrow> coreflexive x
[PROOF STEP]
by blast


[STATEMENT]
lemma test_up_closed:
  "test x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> up_closed x
[PROOF STEP]
by (metis order.eq_iff mult_left_one mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one up_closed_def)


[STATEMENT]
lemma co_test_reflexive:
  "co_test x \<Longrightarrow> reflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> reflexive x
[PROOF STEP]
using co_test_def sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
co_test ?x \<equiv> ?x * bot \<squnion> (1::'a) = ?x
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)

goal (1 subgoal):
 1. co_test x \<Longrightarrow> reflexive x
[PROOF STEP]
by blast


[STATEMENT]
lemma co_test_transitive:
  "co_test x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> transitive x
[PROOF STEP]
by (smt co_test_def sup_assoc le_iff_sup mult_left_one mult_left_zero mult_right_dist_sup mult_semi_associative)


[STATEMENT]
lemma co_test_idempotent:
  "co_test x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> idempotent x
[PROOF STEP]
by (simp add: co_test_reflexive co_test_transitive idempotent_transitive_dense reflexive_dense)


[STATEMENT]
lemma co_test_up_closed:
  "co_test x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> up_closed x
[PROOF STEP]
by (simp add: co_test_reflexive co_test_transitive reflexive_transitive_up_closed)


[STATEMENT]
lemma co_test_contact:
  "co_test x \<Longrightarrow> contact x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> contact x
[PROOF STEP]
by (simp add: co_test_idempotent co_test_reflexive co_test_up_closed contact_reflexive_idempotent_up_closed)


[STATEMENT]
lemma vector_transitive:
  "vector x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> transitive x
[PROOF STEP]
by (metis mult_right_isotone top.extremum)


[STATEMENT]
lemma vector_up_closed:
  "vector x \<Longrightarrow> up_closed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> up_closed x
[PROOF STEP]
by (metis top_mult_right_one up_closed_def)


[STATEMENT]
lemma one_total:
  "total 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma top_total:
  "total top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_total:
  "total x \<Longrightarrow> total y \<Longrightarrow> total (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>times_top_class.total x; times_top_class.total y\<rbrakk> \<Longrightarrow> times_top_class.total (x \<squnion> y)
[PROOF STEP]
by (simp add: total_sup_closed)


[STATEMENT]
lemma zero_co_total:
  "co_total bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_total bot
[PROOF STEP]
by (simp add: co_total_def)


[STATEMENT]
lemma one_co_total:
  "co_total 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_total (1::'a)
[PROOF STEP]
by (simp add: co_total_def)


[STATEMENT]
lemma sup_co_total:
  "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_total x; co_total y\<rbrakk> \<Longrightarrow> co_total (x \<squnion> y)
[PROOF STEP]
by (simp add: co_total_def mult_right_dist_sup)


[STATEMENT]
lemma inf_co_total:
  "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_total x; co_total y\<rbrakk> \<Longrightarrow> co_total (x \<sqinter> y)
[PROOF STEP]
by (metis co_total_def order.antisym bot_least mult_right_sub_dist_inf_right)


[STATEMENT]
lemma comp_co_total:
  "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_total x; co_total y\<rbrakk> \<Longrightarrow> co_total (x * y)
[PROOF STEP]
by (metis co_total_def order.eq_iff mult_semi_associative bot_least)


[STATEMENT]
lemma zero_transitive:
  "transitive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive bot
[PROOF STEP]
by (simp add: vector_transitive)


[STATEMENT]
lemma one_transitive:
  "transitive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma top_transitive:
  "transitive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive top
[PROOF STEP]
by simp


[STATEMENT]
lemma inf_transitive:
  "transitive x \<Longrightarrow> transitive y \<Longrightarrow> transitive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transitive x; transitive y\<rbrakk> \<Longrightarrow> transitive (x \<sqinter> y)
[PROOF STEP]
by (meson inf_mono order_trans mult_left_sub_dist_inf_left mult_left_sub_dist_inf_right mult_right_sub_dist_inf)


[STATEMENT]
lemma zero_dense:
  "dense_rel bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel bot
[PROOF STEP]
by simp


[STATEMENT]
lemma one_dense:
  "dense_rel 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma top_dense:
  "dense_rel top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel top
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_dense:
  assumes "dense_rel x"
      and "dense_rel y"
    shows "dense_rel (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
have "x \<le> x * x \<and> y \<le> y * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel x \<and> dense_rel y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dense_rel x
dense_rel y

goal (1 subgoal):
 1. dense_rel x \<and> dense_rel y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dense_rel x \<and> dense_rel y

goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
hence "x \<le> (x \<squnion> y) * (x \<squnion> y) \<and> y \<le> (x \<squnion> y) * (x \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
dense_rel x \<and> dense_rel y

goal (1 subgoal):
 1. x \<le> (x \<squnion> y) * (x \<squnion> y) \<and> y \<le> (x \<squnion> y) * (x \<squnion> y)
[PROOF STEP]
by (meson dense_sup_closed order_trans sup.cobounded1 sup.cobounded2)
[PROOF STATE]
proof (state)
this:
x \<le> (x \<squnion> y) * (x \<squnion> y) \<and> y \<le> (x \<squnion> y) * (x \<squnion> y)

goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
hence "x \<squnion> y \<le> (x \<squnion> y) * (x \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> (x \<squnion> y) * (x \<squnion> y) \<and> y \<le> (x \<squnion> y) * (x \<squnion> y)

goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dense_rel (x \<squnion> y)

goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
thus "dense_rel (x \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
dense_rel (x \<squnion> y)

goal (1 subgoal):
 1. dense_rel (x \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dense_rel (x \<squnion> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reflexive:
  "reflexive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma top_reflexive:
  "reflexive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive top
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_reflexive:
  "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x \<squnion> y)
[PROOF STEP]
by (simp add: reflexive_sup_closed)


[STATEMENT]
lemma inf_reflexive:
  "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x \<sqinter> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma comp_reflexive:
  "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x * y)
[PROOF STEP]
using reflexive_mult_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reflexive ?x; reflexive ?y\<rbrakk> \<Longrightarrow> reflexive (?x * ?y)

goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_coreflexive:
  "coreflexive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive bot
[PROOF STEP]
by simp


[STATEMENT]
lemma one_coreflexive:
  "coreflexive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_coreflexive:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x \<squnion> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma inf_coreflexive:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x \<sqinter> y)
[PROOF STEP]
by (simp add: le_infI1)


[STATEMENT]
lemma comp_coreflexive:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x * y)
[PROOF STEP]
by (simp add: coreflexive_mult_closed)


[STATEMENT]
lemma zero_idempotent:
  "idempotent bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent bot
[PROOF STEP]
by simp


[STATEMENT]
lemma one_idempotent:
  "idempotent 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma top_idempotent:
  "idempotent top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma zero_up_closed:
  "up_closed bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed bot
[PROOF STEP]
by (simp add: up_closed_def)


[STATEMENT]
lemma one_up_closed:
  "up_closed 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed (1::'a)
[PROOF STEP]
by (simp add: up_closed_def)


[STATEMENT]
lemma top_up_closed:
  "up_closed top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed top
[PROOF STEP]
by (simp add: vector_up_closed)


[STATEMENT]
lemma sup_up_closed:
  "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>up_closed x; up_closed y\<rbrakk> \<Longrightarrow> up_closed (x \<squnion> y)
[PROOF STEP]
by (simp add: mult_right_dist_sup up_closed_def)


[STATEMENT]
lemma inf_up_closed:
  "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>up_closed x; up_closed y\<rbrakk> \<Longrightarrow> up_closed (x \<sqinter> y)
[PROOF STEP]
by (metis order.antisym mult_sub_right_one mult_right_sub_dist_inf up_closed_def)


[STATEMENT]
lemma comp_up_closed:
  "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>up_closed x; up_closed y\<rbrakk> \<Longrightarrow> up_closed (x * y)
[PROOF STEP]
by (metis order.antisym mult_semi_associative mult_sub_right_one up_closed_def)


[STATEMENT]
lemma zero_sup_distributive:
  "sup_distributive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive bot
[PROOF STEP]
by (simp add: sup_distributive_def)


[STATEMENT]
lemma one_sup_distributive:
  "sup_distributive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive (1::'a)
[PROOF STEP]
by (simp add: sup_distributive_def)


[STATEMENT]
lemma sup_sup_distributive:
  "sup_distributive x \<Longrightarrow> sup_distributive y \<Longrightarrow> sup_distributive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sup_distributive x; sup_distributive y\<rbrakk> \<Longrightarrow> sup_distributive (x \<squnion> y)
[PROOF STEP]
using sup_distributive_def mult_right_dist_sup sup_monoid.add_assoc sup_monoid.add_commute
[PROOF STATE]
proof (prove)
using this:
sup_distributive ?x \<equiv> \<forall>y z. ?x * (y \<squnion> z) = ?x * y \<squnion> ?x * z
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
?a \<squnion> ?b \<squnion> ?c = ?a \<squnion> (?b \<squnion> ?c)
?a \<squnion> ?b = ?b \<squnion> ?a

goal (1 subgoal):
 1. \<lbrakk>sup_distributive x; sup_distributive y\<rbrakk> \<Longrightarrow> sup_distributive (x \<squnion> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_inf_distributive:
  "inf_distributive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_distributive bot
[PROOF STEP]
by (simp add: inf_distributive_def)


[STATEMENT]
lemma one_inf_distributive:
  "inf_distributive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_distributive (1::'a)
[PROOF STEP]
by (simp add: inf_distributive_def)


[STATEMENT]
lemma one_contact:
  "contact 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact (1::'a)
[PROOF STEP]
by (simp add: contact_def)


[STATEMENT]
lemma top_contact:
  "contact top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact top
[PROOF STEP]
by (simp add: contact_def)


[STATEMENT]
lemma inf_contact:
  "contact x \<Longrightarrow> contact y \<Longrightarrow> contact (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>contact x; contact y\<rbrakk> \<Longrightarrow> contact (x \<sqinter> y)
[PROOF STEP]
by (meson contact_reflexive_idempotent_up_closed contact_transitive inf_reflexive inf_transitive inf_up_closed preorder_idempotent)


[STATEMENT]
lemma zero_kernel:
  "kernel bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel bot
[PROOF STEP]
by (simp add: kernel_def)


[STATEMENT]
lemma one_kernel:
  "kernel 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel (1::'a)
[PROOF STEP]
by (simp add: kernel_def)


[STATEMENT]
lemma sup_kernel:
  "kernel x \<Longrightarrow> kernel y \<Longrightarrow> kernel (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kernel x; kernel y\<rbrakk> \<Longrightarrow> kernel (x \<squnion> y)
[PROOF STEP]
using kernel_coreflexive_idempotent_up_closed order.antisym coreflexive_transitive sup_dense sup_up_closed
[PROOF STATE]
proof (prove)
using this:
kernel ?x = (coreflexive ?x \<and> idempotent ?x \<and> up_closed ?x)
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
coreflexive ?x \<Longrightarrow> transitive ?x
\<lbrakk>dense_rel ?x; dense_rel ?y\<rbrakk> \<Longrightarrow> dense_rel (?x \<squnion> ?y)
\<lbrakk>up_closed ?x; up_closed ?y\<rbrakk> \<Longrightarrow> up_closed (?x \<squnion> ?y)

goal (1 subgoal):
 1. \<lbrakk>kernel x; kernel y\<rbrakk> \<Longrightarrow> kernel (x \<squnion> y)
[PROOF STEP]
by force


[STATEMENT]
lemma one_sup_dist_contact:
  "sup_dist_contact 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_dist_contact (1::'a)
[PROOF STEP]
by (simp add: sup_dist_contact_def one_sup_distributive one_contact)


[STATEMENT]
lemma zero_inf_dist_kernel:
  "inf_dist_kernel bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_dist_kernel bot
[PROOF STEP]
by (simp add: inf_dist_kernel_def zero_kernel zero_inf_distributive)


[STATEMENT]
lemma one_inf_dist_kernel:
  "inf_dist_kernel 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_dist_kernel (1::'a)
[PROOF STEP]
by (simp add: inf_dist_kernel_def one_kernel one_inf_distributive)


[STATEMENT]
lemma zero_test:
  "test bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test bot
[PROOF STEP]
by (simp add: test_def)


[STATEMENT]
lemma one_test:
  "test 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (1::'a)
[PROOF STEP]
by (simp add: test_def)


[STATEMENT]
lemma sup_test:
  "test x \<Longrightarrow> test y \<Longrightarrow> test (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test x; test y\<rbrakk> \<Longrightarrow> test (x \<squnion> y)
[PROOF STEP]
by (simp add: inf_sup_distrib2 mult_right_dist_sup test_def)


[STATEMENT]
lemma inf_test:
  "test x \<Longrightarrow> test y \<Longrightarrow> test (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test x; test y\<rbrakk> \<Longrightarrow> test (x \<sqinter> y)
[PROOF STEP]
by (smt (z3) inf.left_commute idempotent_one_closed inf.le_iff_sup inf_top.right_neutral mult_right_isotone mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one)


[STATEMENT]
lemma one_co_test:
  "co_test 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test (1::'a)
[PROOF STEP]
by (simp add: co_test_def)


[STATEMENT]
lemma sup_co_test:
  "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_test x; co_test y\<rbrakk> \<Longrightarrow> co_test (x \<squnion> y)
[PROOF STEP]
by (smt (z3) co_test_def mult_right_dist_sup sup.left_idem sup_assoc sup_commute)


[STATEMENT]
lemma zero_vector:
  "vector bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector bot
[PROOF STEP]
by simp


[STATEMENT]
lemma top_vector:
  "vector top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_vector:
  "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector x; vector y\<rbrakk> \<Longrightarrow> vector (x \<squnion> y)
[PROOF STEP]
by (simp add: vector_sup_closed)


[STATEMENT]
lemma inf_vector:
  "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector x; vector y\<rbrakk> \<Longrightarrow> vector (x \<sqinter> y)
[PROOF STEP]
by (metis order.antisym top_right_mult_increasing mult_right_sub_dist_inf)


[STATEMENT]
lemma comp_vector:
  "vector y \<Longrightarrow> vector (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector y \<Longrightarrow> vector (x * y)
[PROOF STEP]
by (simp add: vector_mult_closed)


[STATEMENT]
lemma mult_zero_associative:
  "x * bot * y = x * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * bot * y = x * bot
[PROOF STEP]
by (metis mult_associative_one mult_left_zero)


[STATEMENT]
lemma mult_zero_sup_one_dist:
  "(x * bot \<squnion> 1) * z = x * bot \<squnion> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * bot \<squnion> (1::'a)) * z = x * bot \<squnion> z
[PROOF STEP]
by (simp add: mult_right_dist_sup mult_zero_associative)


[STATEMENT]
lemma mult_zero_sup_dist:
  "(x * bot \<squnion> y) * z = x * bot \<squnion> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * bot \<squnion> y) * z = x * bot \<squnion> y * z
[PROOF STEP]
by (simp add: mult_right_dist_sup mult_zero_associative)


[STATEMENT]
lemma vector_zero_inf_one_comp:
  "(x * bot \<sqinter> 1) * y = x * bot \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * bot \<sqinter> (1::'a)) * y = x * bot \<sqinter> y
[PROOF STEP]
by (metis mult_left_one mult_right_dist_inf_one mult_zero_associative)


[STATEMENT]
lemma co_test_inf_distributive:
  "co_test x \<Longrightarrow> inf_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> inf_distributive x
[PROOF STEP]
by (metis co_test_def distrib_imp1 inf_sup_distrib1 inf_distributive_def mult_zero_sup_one_dist)


[STATEMENT]
lemma co_test_sup_distributive:
  "co_test x \<Longrightarrow> sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> sup_distributive x
[PROOF STEP]
by (metis sup_sup_distributive sup_distributive_def co_test_def one_sup_distributive sup.idem mult_zero_associative)


[STATEMENT]
lemma co_test_sup_dist_contact:
  "co_test x \<Longrightarrow> sup_dist_contact x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
by (simp add: co_test_sup_distributive sup_dist_contact_def co_test_contact)


[STATEMENT]
lemma inf_co_test:
  "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_test x; co_test y\<rbrakk> \<Longrightarrow> co_test (x \<sqinter> y)
[PROOF STEP]
by (smt (z3) co_test_def co_test_up_closed mult_right_dist_inf_one sup_commute sup_inf_distrib1 up_closed_def)


[STATEMENT]
lemma comp_co_test:
  "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>co_test x; co_test y\<rbrakk> \<Longrightarrow> co_test (x * y)
[PROOF STEP]
by (metis co_test_def mult_associative_one sup_assoc mult_zero_sup_one_dist)


[STATEMENT]
lemma top_sup_distributive:
  "sup_distributive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive top
[PROOF STEP]
by (simp add: sup_distributive_def mult_left_top)


[STATEMENT]
lemma top_inf_distributive:
  "inf_distributive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_distributive top
[PROOF STEP]
by (simp add: inf_distributive_def mult_left_top)


[STATEMENT]
lemma top_sup_dist_contact:
  "sup_dist_contact top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_dist_contact top
[PROOF STEP]
by (simp add: sup_dist_contact_def top_contact top_sup_distributive)


[STATEMENT]
lemma top_co_test:
  "co_test top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test top
[PROOF STEP]
by (simp add: co_test_def mult_left_top)


[STATEMENT]
lemma mult_top_associative:
  "x * top * y = x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top * y = x * top
[PROOF STEP]
by (metis mult_left_top mult_associative_one)


[STATEMENT]
lemma vector_inf_one_comp:
  "(x * top \<sqinter> 1) * y = x * top \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * top \<sqinter> (1::'a)) * y = x * top \<sqinter> y
[PROOF STEP]
by (metis vector_zero_inf_one_comp mult_top_associative)


[STATEMENT]
lemma vector_left_annihilator:
  "vector x \<Longrightarrow> x * y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> x * y = x
[PROOF STEP]
by (metis mult_top_associative)


[STATEMENT]
lemma test_comp_inf:
  "test x \<Longrightarrow> test y \<Longrightarrow> x * y = x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test x; test y\<rbrakk> \<Longrightarrow> x * y = x \<sqinter> y
[PROOF STEP]
by (metis inf.absorb1 inf.left_commute test_coreflexive test_def vector_inf_one_comp)


[STATEMENT]
lemma test_sup_distributive:
  "test x \<Longrightarrow> sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> sup_distributive x
[PROOF STEP]
by (metis sup_distributive_def inf_sup_distrib1 test_def vector_inf_one_comp)


[STATEMENT]
lemma test_inf_distributive:
  "test x \<Longrightarrow> inf_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> inf_distributive x
[PROOF STEP]
by (smt (verit, ccfv_SIG) inf.commute inf.sup_monoid.add_assoc inf_distributive_def test_def inf.idem vector_inf_one_comp)


[STATEMENT]
lemma test_inf_dist_kernel:
  "test x \<Longrightarrow> inf_dist_kernel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> inf_dist_kernel x
[PROOF STEP]
by (simp add: kernel_def inf_dist_kernel_def one_test test_comp_inf test_inf_distributive)


[STATEMENT]
lemma vector_idempotent:
  "vector x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> idempotent x
[PROOF STEP]
using vector_left_annihilator
[PROOF STATE]
proof (prove)
using this:
vector ?x \<Longrightarrow> ?x * ?y = ?x

goal (1 subgoal):
 1. vector x \<Longrightarrow> idempotent x
[PROOF STEP]
by blast


[STATEMENT]
lemma vector_sup_distributive:
  "vector x \<Longrightarrow> sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> sup_distributive x
[PROOF STEP]
by (simp add: sup_distributive_def vector_left_annihilator)


[STATEMENT]
lemma vector_inf_distributive:
  "vector x \<Longrightarrow> inf_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> inf_distributive x
[PROOF STEP]
by (simp add: inf_distributive_def vector_left_annihilator)


[STATEMENT]
lemma vector_co_vector:
  "vector x \<longleftrightarrow> co_vector x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x = co_vector x
[PROOF STEP]
by (metis co_vector_def mult_zero_associative mult_top_associative)


[STATEMENT]
lemma comp_test:
  "test x \<Longrightarrow> test y \<Longrightarrow> test (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test x; test y\<rbrakk> \<Longrightarrow> test (x * y)
[PROOF STEP]
by (simp add: inf_test test_comp_inf)


[STATEMENT]
lemma dual_dist_inf:
  "(x \<sqinter> y)\<^sup>d = x\<^sup>d \<squnion> y\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y)\<^sup>d = x\<^sup>d \<squnion> y\<^sup>d
[PROOF STEP]
by (metis dual_dist_sup dual_involutive)


[STATEMENT]
lemma dual_antitone:
  "x \<le> y \<Longrightarrow> y\<^sup>d \<le> x\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> y\<^sup>d \<le> x\<^sup>d
[PROOF STEP]
using dual_dist_sup sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y)\<^sup>d = ?x\<^sup>d \<sqinter> ?y\<^sup>d
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> y\<^sup>d \<le> x\<^sup>d
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dual_zero:
  "bot\<^sup>d = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot\<^sup>d = top
[PROOF STEP]
by (metis dual_antitone bot_least dual_involutive top_le)


[STATEMENT]
lemma dual_top:
  "top\<^sup>d = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top\<^sup>d = bot
[PROOF STEP]
using dual_zero dual_involutive
[PROOF STATE]
proof (prove)
using this:
bot\<^sup>d = top
?x\<^sup>d\<^sup>d = ?x

goal (1 subgoal):
 1. top\<^sup>d = bot
[PROOF STEP]
by auto


[STATEMENT]
lemma reflexive_coreflexive_dual:
  "reflexive x \<longleftrightarrow> coreflexive (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x = coreflexive (x\<^sup>d)
[PROOF STEP]
using dual_antitone dual_involutive dual_one
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?y\<^sup>d \<le> ?x\<^sup>d
?x\<^sup>d\<^sup>d = ?x
(1::'a)\<^sup>d = (1::'a)

goal (1 subgoal):
 1. reflexive x = coreflexive (x\<^sup>d)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dual_sub_dist_comp_one:
  "(x * y)\<^sup>d \<le> (x * 1)\<^sup>d * y\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y)\<^sup>d \<le> (x * (1::'a))\<^sup>d * y\<^sup>d
[PROOF STEP]
by (metis dual_sub_dist_comp mult_one_associative)


[STATEMENT]
lemma co_total_total_dual:
  "co_total x \<Longrightarrow> total (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_total x \<Longrightarrow> times_top_class.total (x\<^sup>d)
[PROOF STEP]
by (metis co_total_def dual_sub_dist_comp dual_zero top_le)


[STATEMENT]
lemma transitive_dense_dual:
  "transitive x \<Longrightarrow> dense_rel (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive x \<Longrightarrow> dense_rel (x\<^sup>d)
[PROOF STEP]
using dual_antitone dual_sub_dist_comp inf.order_lesseq_imp
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?y\<^sup>d \<le> ?x\<^sup>d
(?x * ?y)\<^sup>d \<le> ?x\<^sup>d * ?y\<^sup>d
(\<forall>z\<le>?x. z \<le> ?y) = (?x \<le> ?y)

goal (1 subgoal):
 1. transitive x \<Longrightarrow> dense_rel (x\<^sup>d)
[PROOF STEP]
by blast


[STATEMENT]
lemma strong_up_closed:
  "x * 1 \<le> x \<Longrightarrow> x\<^sup>d * y\<^sup>d \<le> (x * y)\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (1::'a) \<le> x \<Longrightarrow> x\<^sup>d * y\<^sup>d \<le> (x * y)\<^sup>d
[PROOF STEP]
by (simp add: dual_dist_comp_one antisym_conv mult_sub_right_one)


[STATEMENT]
lemma strong_up_closed_2:
  "up_closed x \<Longrightarrow> (x * y)\<^sup>d = x\<^sup>d * y\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed x \<Longrightarrow> (x * y)\<^sup>d = x\<^sup>d * y\<^sup>d
[PROOF STEP]
by (simp add: dual_dist_comp_one up_closed_def)


[STATEMENT]
lemma contact_kernel_dual:
  "contact x \<longleftrightarrow> kernel (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contact x = kernel (x\<^sup>d)
[PROOF STEP]
by (metis contact_def contact_up_closed dual_dist_sup dual_involutive dual_one kernel_def kernel_up_closed up_closed_def strong_up_closed_2)


[STATEMENT]
lemma sup_dist_contact_inf_dist_kernel_dual:
  "sup_dist_contact x \<longleftrightarrow> inf_dist_kernel (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_dist_contact x = inf_dist_kernel (x\<^sup>d)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sup_dist_contact x \<Longrightarrow> inf_dist_kernel (x\<^sup>d)
 2. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
assume 1: "sup_dist_contact x"
[PROOF STATE]
proof (state)
this:
sup_dist_contact x

goal (2 subgoals):
 1. sup_dist_contact x \<Longrightarrow> inf_dist_kernel (x\<^sup>d)
 2. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
hence 2: "up_closed x"
[PROOF STATE]
proof (prove)
using this:
sup_dist_contact x

goal (1 subgoal):
 1. up_closed x
[PROOF STEP]
using sup_dist_contact_def contact_up_closed
[PROOF STATE]
proof (prove)
using this:
sup_dist_contact x
sup_dist_contact ?x \<equiv> sup_distributive ?x \<and> contact ?x
contact ?x \<Longrightarrow> up_closed ?x

goal (1 subgoal):
 1. up_closed x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
up_closed x

goal (2 subgoals):
 1. sup_dist_contact x \<Longrightarrow> inf_dist_kernel (x\<^sup>d)
 2. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
have "sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
using 1 sup_dist_contact_def
[PROOF STATE]
proof (prove)
using this:
sup_dist_contact x
sup_dist_contact ?x \<equiv> sup_distributive ?x \<and> contact ?x

goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sup_distributive x

goal (2 subgoals):
 1. sup_dist_contact x \<Longrightarrow> inf_dist_kernel (x\<^sup>d)
 2. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
hence "inf_distributive (x\<^sup>d)"
[PROOF STATE]
proof (prove)
using this:
sup_distributive x

goal (1 subgoal):
 1. inf_distributive (x\<^sup>d)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
sup_distributive x
up_closed x

goal (1 subgoal):
 1. inf_distributive (x\<^sup>d)
[PROOF STEP]
by (smt sup_distributive_def dual_dist_comp_one dual_dist_inf dual_involutive inf_distributive_def up_closed_def)
[PROOF STATE]
proof (state)
this:
inf_distributive (x\<^sup>d)

goal (2 subgoals):
 1. sup_dist_contact x \<Longrightarrow> inf_dist_kernel (x\<^sup>d)
 2. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
thus "inf_dist_kernel (x\<^sup>d)"
[PROOF STATE]
proof (prove)
using this:
inf_distributive (x\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d)
[PROOF STEP]
using 1 contact_kernel_dual sup_dist_contact_def inf_dist_kernel_def
[PROOF STATE]
proof (prove)
using this:
inf_distributive (x\<^sup>d)
sup_dist_contact x
contact ?x = kernel (?x\<^sup>d)
sup_dist_contact ?x \<equiv> sup_distributive ?x \<and> contact ?x
inf_dist_kernel ?x \<equiv> inf_distributive ?x \<and> kernel ?x

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inf_dist_kernel (x\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
assume 3: "inf_dist_kernel (x\<^sup>d)"
[PROOF STATE]
proof (state)
this:
inf_dist_kernel (x\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
hence 4: "up_closed (x\<^sup>d)"
[PROOF STATE]
proof (prove)
using this:
inf_dist_kernel (x\<^sup>d)

goal (1 subgoal):
 1. up_closed (x\<^sup>d)
[PROOF STEP]
using kernel_up_closed inf_dist_kernel_def
[PROOF STATE]
proof (prove)
using this:
inf_dist_kernel (x\<^sup>d)
kernel ?x \<Longrightarrow> up_closed ?x
inf_dist_kernel ?x \<equiv> inf_distributive ?x \<and> kernel ?x

goal (1 subgoal):
 1. up_closed (x\<^sup>d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
up_closed (x\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
have "inf_distributive (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_distributive (x\<^sup>d)
[PROOF STEP]
using 3 inf_dist_kernel_def
[PROOF STATE]
proof (prove)
using this:
inf_dist_kernel (x\<^sup>d)
inf_dist_kernel ?x \<equiv> inf_distributive ?x \<and> kernel ?x

goal (1 subgoal):
 1. inf_distributive (x\<^sup>d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_distributive (x\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
hence "sup_distributive (x\<^sup>d\<^sup>d)"
[PROOF STATE]
proof (prove)
using this:
inf_distributive (x\<^sup>d)

goal (1 subgoal):
 1. sup_distributive (x\<^sup>d\<^sup>d)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
inf_distributive (x\<^sup>d)
up_closed (x\<^sup>d)

goal (1 subgoal):
 1. sup_distributive (x\<^sup>d\<^sup>d)
[PROOF STEP]
by (smt inf_distributive_def sup_distributive_def dual_dist_sup dual_involutive strong_up_closed_2)
[PROOF STATE]
proof (state)
this:
sup_distributive (x\<^sup>d\<^sup>d)

goal (1 subgoal):
 1. inf_dist_kernel (x\<^sup>d) \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
thus "sup_dist_contact x"
[PROOF STATE]
proof (prove)
using this:
sup_distributive (x\<^sup>d\<^sup>d)

goal (1 subgoal):
 1. sup_dist_contact x
[PROOF STEP]
using 3 contact_kernel_dual sup_dist_contact_def dual_involutive inf_dist_kernel_def
[PROOF STATE]
proof (prove)
using this:
sup_distributive (x\<^sup>d\<^sup>d)
inf_dist_kernel (x\<^sup>d)
contact ?x = kernel (?x\<^sup>d)
sup_dist_contact ?x \<equiv> sup_distributive ?x \<and> contact ?x
?x\<^sup>d\<^sup>d = ?x
inf_dist_kernel ?x \<equiv> inf_distributive ?x \<and> kernel ?x

goal (1 subgoal):
 1. sup_dist_contact x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sup_dist_contact x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma test_co_test_dual:
  "test x \<longleftrightarrow> co_test (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x = co_test (x\<^sup>d)
[PROOF STEP]
by (smt (z3) co_test_def co_test_up_closed dual_dist_comp_one dual_dist_inf dual_involutive dual_one dual_top test_def test_up_closed up_closed_def)


[STATEMENT]
lemma vector_dual:
  "vector x \<longleftrightarrow> vector (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x = vector (x\<^sup>d)
[PROOF STEP]
by (metis dual_dist_comp_one dual_involutive mult_top_associative)


[STATEMENT]
lemma mult_right_dist_inf:
  "(x \<sqinter> y) * z = x * z \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * z = x * z \<sqinter> y * z
[PROOF STEP]
by (metis dual_dist_sup dual_dist_comp dual_involutive mult_right_dist_sup)


[STATEMENT]
lemma vector_inf_comp:
  "(x * top \<sqinter> y) * z = x * top \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * top \<sqinter> y) * z = x * top \<sqinter> y * z
[PROOF STEP]
by (simp add: vector_left_annihilator mult_right_dist_inf mult.assoc)


[STATEMENT]
lemma vector_zero_inf_comp:
  "(x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z
[PROOF STEP]
by (simp add: mult_right_dist_inf mult.assoc)


[STATEMENT]
lemma inf_total:
  "total x \<Longrightarrow> total y \<Longrightarrow> total (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>times_top_class.total x; times_top_class.total y\<rbrakk> \<Longrightarrow> times_top_class.total (x \<sqinter> y)
[PROOF STEP]
by (simp add: mult_right_dist_inf)


[STATEMENT]
lemma comp_total:
  "total x \<Longrightarrow> total y \<Longrightarrow> total (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>times_top_class.total x; times_top_class.total y\<rbrakk> \<Longrightarrow> times_top_class.total (x * y)
[PROOF STEP]
by (simp add: mult_assoc)


[STATEMENT]
lemma total_co_total_dual:
  "total x \<longleftrightarrow> co_total (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total x = co_total (x\<^sup>d)
[PROOF STEP]
by (metis co_total_def dual_dist_comp dual_involutive dual_top)


[STATEMENT]
lemma transitive_iff_dense_dual:
  "transitive x \<longleftrightarrow> dense_rel (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive x = dense_rel (x\<^sup>d)
[PROOF STEP]
by (metis dual_antitone dual_dist_comp dual_involutive)


[STATEMENT]
lemma idempotent_dual:
  "idempotent x \<longleftrightarrow> idempotent (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent x = idempotent (x\<^sup>d)
[PROOF STEP]
using dual_involutive idempotent_transitive_dense transitive_iff_dense_dual
[PROOF STATE]
proof (prove)
using this:
?x\<^sup>d\<^sup>d = ?x
idempotent ?x = (transitive ?x \<and> dense_rel ?x)
transitive ?x = dense_rel (?x\<^sup>d)

goal (1 subgoal):
 1. idempotent x = idempotent (x\<^sup>d)
[PROOF STEP]
by auto


[STATEMENT]
lemma comp_sup_distributive:
  "sup_distributive x \<Longrightarrow> sup_distributive y \<Longrightarrow> sup_distributive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sup_distributive x; sup_distributive y\<rbrakk> \<Longrightarrow> sup_distributive (x * y)
[PROOF STEP]
by (simp add: sup_distributive_def mult.assoc)


[STATEMENT]
lemma sup_inf_distributive_dual:
  "sup_distributive x \<longleftrightarrow> inf_distributive (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive x = inf_distributive (x\<^sup>d)
[PROOF STEP]
by (smt (verit, ccfv_threshold) sup_distributive_def dual_dist_sup dual_dist_comp dual_dist_inf dual_involutive inf_distributive_def)


[STATEMENT]
lemma inf_inf_distributive:
  "inf_distributive x \<Longrightarrow> inf_distributive y \<Longrightarrow> inf_distributive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inf_distributive x; inf_distributive y\<rbrakk> \<Longrightarrow> inf_distributive (x \<sqinter> y)
[PROOF STEP]
by (metis sup_inf_distributive_dual sup_sup_distributive dual_dist_inf dual_involutive)


[STATEMENT]
lemma comp_inf_distributive:
  "inf_distributive x \<Longrightarrow> inf_distributive y \<Longrightarrow> inf_distributive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inf_distributive x; inf_distributive y\<rbrakk> \<Longrightarrow> inf_distributive (x * y)
[PROOF STEP]
by (simp add: inf_distributive_def mult.assoc)


[STATEMENT]
lemma vector_zero_inf_comp:
  "(x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z
[PROOF STEP]
by (metis vector_inf_comp vector_mult_closed zero_vector)


[STATEMENT]
lemma test_sup_distributive:
  "test x \<Longrightarrow> sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> sup_distributive x
[PROOF STEP]
by (metis sup_distributive_def inf_sup_distrib1 mult_left_one test_def vector_inf_comp)


[STATEMENT]
lemma test_inf_distributive:
  "test x \<Longrightarrow> inf_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> inf_distributive x
[PROOF STEP]
by (smt (z3) inf.right_idem inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_distributive_def mult_left_one test_def vector_inf_comp)


[STATEMENT]
lemma test_inf_dist_kernel:
  "test x \<Longrightarrow> inf_dist_kernel x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test x \<Longrightarrow> inf_dist_kernel x
[PROOF STEP]
by (metis inf.idem inf.sup_monoid.add_assoc kernel_def inf_dist_kernel_def mult_left_one test_def test_inf_distributive vector_inf_comp)


[STATEMENT]
lemma co_test_inf_distributive:
  assumes "co_test x"
    shows "inf_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_distributive x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inf_distributive x
[PROOF STEP]
have "x = x * bot \<squnion> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x * bot \<squnion> (1::'a)
[PROOF STEP]
using assms co_test_def
[PROOF STATE]
proof (prove)
using this:
co_test x
co_test ?x \<equiv> ?x * bot \<squnion> (1::'a) = ?x

goal (1 subgoal):
 1. x = x * bot \<squnion> (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = x * bot \<squnion> (1::'a)

goal (1 subgoal):
 1. inf_distributive x
[PROOF STEP]
hence "\<forall>y z . x * y \<sqinter> x * z = x * (y \<sqinter> z)"
[PROOF STATE]
proof (prove)
using this:
x = x * bot \<squnion> (1::'a)

goal (1 subgoal):
 1. \<forall>y z. x * y \<sqinter> x * z = x * (y \<sqinter> z)
[PROOF STEP]
by (metis distrib_imp1 inf_sup_absorb inf_sup_distrib1 mult_left_one mult_left_top mult_right_dist_sup sup_top_right vector_zero_inf_comp)
[PROOF STATE]
proof (state)
this:
\<forall>y z. x * y \<sqinter> x * z = x * (y \<sqinter> z)

goal (1 subgoal):
 1. inf_distributive x
[PROOF STEP]
thus "inf_distributive x"
[PROOF STATE]
proof (prove)
using this:
\<forall>y z. x * y \<sqinter> x * z = x * (y \<sqinter> z)

goal (1 subgoal):
 1. inf_distributive x
[PROOF STEP]
by (simp add: inf_distributive_def)
[PROOF STATE]
proof (state)
this:
inf_distributive x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma co_test_sup_distributive:
  assumes "co_test x"
    shows "sup_distributive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
have "x = x * bot \<squnion> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x * bot \<squnion> (1::'a)
[PROOF STEP]
using assms co_test_def
[PROOF STATE]
proof (prove)
using this:
co_test x
co_test ?x \<equiv> ?x * bot \<squnion> (1::'a) = ?x

goal (1 subgoal):
 1. x = x * bot \<squnion> (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = x * bot \<squnion> (1::'a)

goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
hence "\<forall>y z . x * (y \<squnion> z) = x * y \<squnion> x * z"
[PROOF STATE]
proof (prove)
using this:
x = x * bot \<squnion> (1::'a)

goal (1 subgoal):
 1. \<forall>y z. x * (y \<squnion> z) = x * y \<squnion> x * z
[PROOF STEP]
by (metis sup_sup_distributive sup_distributive_def inf_sup_absorb mult_left_top one_sup_distributive sup.idem sup_top_right vector_zero_inf_comp)
[PROOF STATE]
proof (state)
this:
\<forall>y z. x * (y \<squnion> z) = x * y \<squnion> x * z

goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
thus "sup_distributive x"
[PROOF STATE]
proof (prove)
using this:
\<forall>y z. x * (y \<squnion> z) = x * y \<squnion> x * z

goal (1 subgoal):
 1. sup_distributive x
[PROOF STEP]
by (simp add: sup_distributive_def)
[PROOF STATE]
proof (state)
this:
sup_distributive x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma co_test_sup_dist_contact:
  "co_test x \<Longrightarrow> sup_dist_contact x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. co_test x \<Longrightarrow> sup_dist_contact x
[PROOF STEP]
by (simp add: sup_dist_contact_def co_test_sup_distributive co_test_contact)


[STATEMENT]
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace>
      \<lbrace>\<acute>A < 0\<rbrace> \<longmapsto> BASIC
       LET (a,b,c) = foo \<acute>A
       IN
            \<acute>A :== a,
            \<acute>B :== b,
            \<acute>C :== c
      END
      \<lbrace>\<acute>A = x \<and> \<acute>B = y \<and> \<acute>C = c\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace> (False, \<lbrace>\<acute>A < 0\<rbrace>)\<longmapsto> BASIC LET (a, b, c) = foo \<acute>A IN \<acute>A :== a, \<acute>B :== b, \<acute>C :== c END \<lbrace>\<acute>A = x \<and> \<acute>B = y \<and> \<acute>C = c\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. A = 0 \<Longrightarrow> A < 0 \<and> fst (foo A) = x \<and> fst (snd (foo A)) = y \<and> snd (snd (foo A)) = c
[PROOF STEP]
oops